ncfavier

{-# OPTIONS --cubical #-}
open import Cubical.Data.Int
open import Cubical.Data.Int.Divisibility
open import Cubical.Data.Nat
open import Cubical.Foundations.Everything
open import Data.List
open import Data.List.NonEmpty as List⁺

data Vertex : Type where
  a b c : Vertex

ncfavier

module Lan where

open import Categories.Kan
open import Data.Product
open import Level
open import Function renaming (id to funId)
open import Categories.Functor
open import Categories.Category.Instance.Sets
open Functor
open import Relation.Binary.PropositionalEquality

ncfavier

import Data.Bits
import Data.Foldable

{-
Two implementations of A372325 (https://oeis.org/A372325).

The first one ties the knot on the sequence itself, but needs the first
three values in order to get bootstrapped.
Using a cleverer takeWhile we could produce the first 0, but in order to
produce 2 we need to know that 1 isn't in the sequence, which we only

ncfavier

{-# OPTIONS --without-K #-}
open import Agda.Primitive renaming (Set to Type)
open import Data.Product
open import Data.Product.Properties
open import Relation.Binary.PropositionalEquality

private variable
  ℓ ℓ' : Level
  A : Type ℓ
  B : A → Type ℓ

ncfavier

{-# LANGUAGE BlockArguments #-}

import Control.Monad
import Data.Foldable
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Sequence qualified as Seq
import Data.PriorityQueue.FingerTree qualified as PQ

ncfavier

open import 1Lab.Prelude
open import Data.Dec
open import Data.Nat

module Goat where

holds : ∀ {ℓ} (A : Type ℓ) ⦃ _ : Dec A ⦄ → Type
holds _ ⦃ yes _ ⦄ = ⊤
holds _ ⦃ no _ ⦄ = ⊥

ncfavier

open import Cat.Functor.Naturality
open import Cat.Functor.Bifunctor
open import Cat.Functor.Coherence
open import Cat.Instances.Product
open import Cat.Functor.Compose
open import Cat.Diagram.Monad
open import Cat.Monoidal.Base
open import Cat.Functor.Base
open import Cat.Prelude

ncfavier

L ⊣ R

adjunct : (L a → b) → (a → R b)
coadjunct : (a → R b) → (L a → b)
unit : a → RL a
counit : LR b → b
Lmap : (a → b) → (L a → L b)
Rmap : (a → b) → (R a → R b)

adjunct f = unit; Rmap f

ncfavier

instance Monoid a => MonadFix ((,) a) where
  mfix :: (b -> (a, b)) -> (a, b)
  mfix f = let (a, b) = f b in (a, b)
  -- or
  mfix f = fix (f . snd)

The laws are proved in section 4.5 of Value Recursion in Monadic Computations

ncfavier

-- Moved to https://agda.monade.li/TangentBundles.html