move helper agda files

agda/Makefile

@@ -30,6 +30,5 @@ Everything.agda:
 	echo "{-# OPTIONS --guardedness #-}" > src/Everything.agda
 	git ls-files | egrep '^src/[^\.]*.l?agda(\.md)?' | grep -v 'index.lagda.md' | grep -v 'bsc.agda-lib' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' -e 's/..md//' | LC_COLLATE='C' sort >> src/Everything.agda
 
-
 open:
 	firefox public/index.html

agda/src/Category/Ambient.lagda.md

@@ -29,28 +29,22 @@ import Categories.Morphism.Properties as MP'
 -->
 
 ## Summary
-We work in an ambient category that
+We work in an ambient distributive category.
-
+This file contains some helper definitions that will be used throughout the development.
-- is extensive (has finite coproducts and pullbacks along injections)
-- is cartesian (has finite products, extensive + cartesian also gives a distributivity isomorphism)
-- has a parametrized NNO ℕ
-- has exponentials `X^ℕ`
 
 ```agda
 module Category.Ambient where
-  record Ambient (o ℓ e : Level) : Set (suc o ⊔ suc ℓ ⊔ suc e) where
+  record Ambient (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
     field
       C : Category o ℓ e
-      extensive : Extensive C
+      distributive : Distributive C
-      cartesian : Cartesian C
+
-      ℕ : ParametrizedNNO (record { U = C ; cartesian = cartesian })
+    open Distributive distributive public
-      -- _^ℕ : ∀ X → Exponential C (ParametrizedNNO.N ℕ) X
 
     cartesianCategory : CartesianCategory o ℓ e
     cartesianCategory = record { U = C ; cartesian = cartesian }
 
     open Category C renaming (id to idC) public
-    open Extensive extensive public
     open Cocartesian cocartesian renaming (+-unique to []-unique) public
     open Cartesian cartesian public
 
@@ -65,14 +59,9 @@ module Category.Ambient where
     braided = Symmetric.braided symmetric
 
     open BinaryProducts products renaming (η to ⁂-η; g-η to ⁂-g-η; unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′) public
-    open ParametrizedNNO ℕ public renaming (η to pnno-η)
-
     open CartesianMonoidal cartesian using (⊤×A≅A; A×⊤≅A) public
 
 
-    distributive : Distributive C
-    distributive = Extensive×Cartesian⇒Distributive C extensive cartesian
-    open Distributive distributive hiding (cartesian; cocartesian) public
     open M' C
     open HomReasoning
     open MR' C

agda/src/Category/Ambient/Setoids.lagda.md

@@ -1,114 +1,46 @@
 <!--
 ```agda
-open import Level using (lift; Lift) renaming (suc to ℓ-suc)
+open import Level using (_⊔_) renaming (suc to ℓ-suc)
 open import Category.Ambient
 open import Categories.Category.Instance.Setoids
-open import Categories.Category.Instance.Properties.Setoids.Extensive
+open import Categories.Category.Distributive
-open import Categories.Category.Instance.Properties.Setoids.CCC
 open import Categories.Category.Monoidal.Instance.Setoids
-open import Categories.Category.Instance.SingletonSet
-open import Categories.Object.NaturalNumbers
 open import Relation.Binary
-open import Data.Unit.Polymorphic using (tt; ⊤)
+open import Function.Bundles using () renaming (Func to _⟶_)
-open import Data.Empty.Polymorphic using (⊥)
+open import Data.Sum
-open import Function.Bundles using (_⟨$⟩_) renaming (Func to _⟶_)
+open import Data.Sum.Relation.Binary.Pointwise
-open import Function.Construct.Identity as idₛ
+open import Data.Product
-open import Function.Construct.Setoid renaming (setoid to _⇨_; _∙_ to _∘_)
+import Categories.Morphism as M
-open import Categories.Object.NaturalNumbers.Properties.Parametrized
-open import Categories.Category.Cocartesian
-import Relation.Binary.Reasoning.Setoid as SetoidR
-
-import Relation.Binary.PropositionalEquality as Eq
-open Eq using (_≡_)
 ```
 -->
 
 # The category of Setoids can be used as instance for ambient category
 
-Most of the required properties are already proven in the agda-categories library, we are only left to construct the natural numbers object.
+Most of the required properties are already proven in the agda-categories library, we are only left to show distributivity.
 
 ```agda
-module Category.Ambient.Setoids {ℓ} where
+module Category.Ambient.Setoids {c ℓ} where
-  open _⟶_ using (cong)
+  open M (Setoids c (c ⊔ ℓ))
+  open _⟶_ using (cong) renaming (to to <_>)
 
-  -- equality on setoid functions
+  refl : ∀ (A : Setoid c (c ⊔ ℓ)) {a} → Setoid._≈_ A a a
-  private
+  refl A = IsEquivalence.refl (Setoid.isEquivalence A)
-    _≋_ : ∀ {A B : Setoid ℓ ℓ} → A ⟶ B → A ⟶ B → Set ℓ
-    _≋_ {A} {B} f g = Setoid._≈_ (A ⇨ B) f g
-    ≋-sym : ∀ {A B : Setoid ℓ ℓ} {f g : A ⟶ B} → f ≋ g → g ≋ f
-    ≋-sym {A} {B} {f} {g} = IsEquivalence.sym (Setoid.isEquivalence (A ⇨ B)) {f} {g}
-    ≋-trans : ∀ {A B : Setoid ℓ ℓ} {f g h : A ⟶ B} → f ≋ g → g ≋ h → f ≋ h
-    ≋-trans {A} {B} {f} {g} {h} = IsEquivalence.trans (Setoid.isEquivalence (A ⇨ B)) {f} {g} {h}
 
-  -- we define ℕ ourselves, instead of importing it, to avoid lifting the universe levels (builtin Nats are defined on Set₀)
+  setoidDistributive : Distributive (Setoids c (c ⊔ ℓ))
-  data ℕ : Set ℓ where
+  Distributive.cartesian setoidDistributive = Setoids-Cartesian
-    zero : ℕ
+  Distributive.cocartesian setoidDistributive = Setoids-Cocartesian {c} {(c ⊔ ℓ)}
-    suc : ℕ → ℕ
+  < IsIso.inv (Distributive.isIsoˡ setoidDistributive {A} {B} {C}) > (x , (inj₁ y)) = inj₁ (x , y)
+  < IsIso.inv (Distributive.isIsoˡ setoidDistributive {A} {B} {C}) > (x , (inj₂ y)) = inj₂ (x , y)
+  cong (IsIso.inv (Distributive.isIsoˡ setoidDistributive {A} {B} {C})) {(x , inj₁ y)} {(a , inj₁ b)} (x≈a , inj₁ y≈b) = inj₁ (x≈a , y≈b)
+  cong (IsIso.inv (Distributive.isIsoˡ setoidDistributive {A} {B} {C})) {(x , inj₂ y)} {(a , inj₂ b)} (x≈a , inj₂ y≈b) = inj₂ (x≈a , y≈b)
+  Iso.isoˡ (IsIso.iso (Distributive.isIsoˡ setoidDistributive {A} {B} {C})) {inj₁ (a , b)} = inj₁ (refl A , refl B)
+  Iso.isoˡ (IsIso.iso (Distributive.isIsoˡ setoidDistributive {A} {B} {C})) {inj₂ (a , c)} = inj₂ (refl A , refl C)
+  Iso.isoʳ (IsIso.iso (Distributive.isIsoˡ setoidDistributive {A} {B} {C})) {a , inj₁ b} = refl A , inj₁ (refl B)
+  Iso.isoʳ (IsIso.iso (Distributive.isIsoˡ setoidDistributive {A} {B} {C})) {a , inj₂ c} = (refl A) , (inj₂ (refl C))
 
-  suc-cong : ∀ {n m} → n ≡ m → suc n ≡ suc m
+  setoidAmbient : Ambient (ℓ-suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
-  suc-cong n≡m rewrite n≡m = Eq.refl
+  setoidAmbient = record 
-
+    { C = Setoids c (c ⊔ ℓ)
-  suc-inj : ∀ {n m} → suc n ≡ suc m → n ≡ m
+    ; distributive = setoidDistributive
-  suc-inj Eq.refl = Eq.refl
-
-  ℕ-eq : Rel ℕ ℓ
-  ℕ-eq zero zero = ⊤
-  ℕ-eq zero (suc m) = ⊥
-  ℕ-eq (suc n) zero = ⊥
-  ℕ-eq (suc n) (suc m) = ℕ-eq n m
-
-  ⊤-setoid : Setoid ℓ ℓ
-  ⊤-setoid = record { Carrier = ⊤ ; _≈_ = _≡_ ; isEquivalence = Eq.isEquivalence }
-
-  ℕ-setoid : Setoid ℓ ℓ
-  ℕ-setoid = record 
-    { Carrier = ℕ 
-    ; _≈_ = _≡_ -- ℕ-eq 
-    ; isEquivalence = Eq.isEquivalence 
     }
-  
-  zero⟶ : SingletonSetoid {ℓ} {ℓ} ⟶ ℕ-setoid
-  zero⟶ = record { to = λ _ → zero ; cong = λ x → Eq.refl } 
-  suc⟶ : ℕ-setoid ⟶ ℕ-setoid
-  suc⟶ = record { to = suc ; cong = suc-cong }
-
-  ℕ-universal : ∀ {A : Setoid ℓ ℓ} → SingletonSetoid {ℓ} {ℓ} ⟶ A → A ⟶ A → ℕ-setoid ⟶ A
-  ℕ-universal {A} z s = record { to = app ; cong = cong' }
-    where
-      app : ℕ → Setoid.Carrier A
-      app zero = z ⟨$⟩ tt
-      app (suc n) = s ⟨$⟩ (app n)
-      cong' : ∀ {n m : ℕ} → n ≡ m → Setoid._≈_ A (app n) (app m)
-      cong' Eq.refl = IsEquivalence.refl (Setoid.isEquivalence A)
-    
-  ℕ-z-commute : ∀ {A : Setoid ℓ ℓ} {q : SingletonSetoid {ℓ} {ℓ} ⟶ A} {f : A ⟶ A} → q ≋ (ℕ-universal q f ∘ zero⟶)
-  ℕ-z-commute {A} {q} {f} {lift t} = IsEquivalence.refl (Setoid.isEquivalence A)
-
-  ℕ-s-commute : ∀ {A : Setoid ℓ ℓ} {q : SingletonSetoid {ℓ} {ℓ} ⟶ A} {f : A ⟶ A} → (f ∘ (ℕ-universal q f)) ≋ (ℕ-universal q f ∘ suc⟶)
-  ℕ-s-commute {A} {q} {f} {n} = IsEquivalence.refl (Setoid.isEquivalence A)
-
-  ℕ-unique : ∀ {A : Setoid ℓ ℓ} {q : SingletonSetoid {ℓ} {ℓ} ⟶ A} {f : A ⟶ A} {u : ℕ-setoid ⟶ A} → q ≋ (u ∘ zero⟶) → (f ∘ u) ≋ (u ∘ suc⟶) → u ≋ ℕ-universal q f
-  ℕ-unique {A} {q} {f} {u} qz fs {zero} = ≋-sym {SingletonSetoid} {A} {q} {u ∘ zero⟶} qz
-  ℕ-unique {A} {q} {f} {u} qz fs {suc n} = AR.begin 
-    u ⟨$⟩ suc n                                            AR.≈⟨ ≋-sym {ℕ-setoid} {A} {f ∘ u} {u ∘ suc⟶} fs ⟩ 
-    f ∘ u ⟨$⟩ n                                            AR.≈⟨ cong f (ℕ-unique {A} {q} {f} {u} qz fs {n}) ⟩ 
-    f ∘ ℕ-universal q f ⟨$⟩ n                              AR.≈⟨ ℕ-s-commute {A} {q} {f} {n} ⟩ 
-    ℕ-universal q f ⟨$⟩ suc n                              AR.∎
-    where module AR = SetoidR A
-
-  setoidNNO : NNO (Setoids ℓ ℓ) SingletonSetoid-⊤
-  setoidNNO = record 
-    { N = ℕ-setoid 
-    ; isNNO = record
-      { z = zero⟶
-      ; s = suc⟶
-      ; universal = ℕ-universal
-      ; z-commute = λ {A} {q} {f} → ℕ-z-commute {A} {q} {f}
-      ; s-commute = λ {A} {q} {f} {n} → ℕ-s-commute {A} {q} {f} {n}
-      ; unique = λ {A} {q} {f} {u} qz fs → ℕ-unique {A} {q} {f} {u} qz fs
-      }
-    }
-
-  setoidAmbient : Ambient (ℓ-suc ℓ) ℓ ℓ
-  setoidAmbient = record { C = Setoids ℓ ℓ ; extensive = Setoids-Extensive ℓ ; cartesian = Setoids-Cartesian ; ℕ = NNO×CCC⇒PNNO (record { U = Setoids ℓ ℓ ; cartesianClosed = Setoids-CCC ℓ }) (Cocartesian.coproducts (Setoids-Cocartesian {ℓ} {ℓ})) setoidNNO }
 ```

agda/src/Monad/Instance/Delay.lagda.md

@@ -96,25 +96,6 @@ Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use the fina
           (idC +₁ coit g) ∘ f ∎ })
 ```
 
-Furthermore if we combine the internal algebra structure of Parametrized NNOs with Lambek's lemma, we get the isomorphism `X × N ≅ X + X × N`.
-At the same time the morphism `X × N ⇒ X + X × N` is a coalgebra for the `(Y + \_)`-functor defined above, this gives us another morphism `ι : X × N ⇒ DX` by using the final coalgebras.
-
-<!-- https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgXFxtYXRoYmJ7Tn0iXSxbMiwwLCJYICsgKFggXFx0aW1lcyBcXG1hdGhiYntOfSkiXSxbMCwxLCJEIFgiXSxbMiwxLCJYICsgRCBYIl0sWzAsMSwi4omFIl0sWzAsMiwiISA9OiBcXGlvdGEiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMiwzLCJvdXQiXSxbMSwzLCJGIFxcaW90YSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ== -->
-<iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgXFxtYXRoYmJ7Tn0iXSxbMiwwLCJYICsgKFggXFx0aW1lcyBcXG1hdGhiYntOfSkiXSxbMCwxLCJEIFgiXSxbMiwxLCJYICsgRCBYIl0sWzAsMSwi4omFIl0sWzAsMiwiISA9OiBcXGlvdGEiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMiwzLCJvdXQiXSxbMSwzLCJGIFxcaW90YSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==&embed" width="575" height="304" style="border-radius: 8px; border: none;"></iframe>
-```agda
-      nno-iso : X × N ≅ X + X × N
-      nno-iso = Lambek.lambek (record { ⊥ = PNNO-Algebra cartesianCategory coproducts X N z s ; ⊥-is-initial = PNNO⇒Initial₂ cartesianCategory coproducts ℕ X })
-
-      ι-coalg : F-Coalgebra-Morphism (record { A = X × N ; α = _≅_.from nno-iso }) (record { A = DX ; α = out })
-      ι-coalg = ! {A = record { A = X × N ; α = _≅_.from nno-iso }}
-
-      ι : X × N ⇒ DX
-      ι = u ι-coalg
-
-      ι-commutes : out ∘ ι ≈ (idC +₁ ι) ∘ _≅_.from nno-iso
-      ι-commutes = commutes ι-coalg
-```
-
 ## Delay is a monad
 
 The next step is showing that this actually yields a monad. Some parts for this are already given, we can construct `D X` from `X` and `now : D X ⇒ D X` is the monad unit.
@@ -254,7 +235,7 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
         [ [ (idC +₁ extend' ([ now , f ])) ∘ i₁ , (idC +₁ extend' ([ now , f ])) ∘ h ] , i₂ ∘ extend' ([ now , f ]) ] ∘ out ≈˘⟨ ([]-cong₂ ∘[] +₁∘i₂) ⟩∘⟨refl ⟩ 
         [ (idC +₁ extend' ([ now , f ])) ∘ [ i₁ , h ] , (idC +₁ extend' ([ now , f ])) ∘ i₂ ] ∘ out                         ≈˘⟨ pullˡ ∘[] ⟩ 
         (idC +₁ extend' ([ now , f ])) ∘ [ [ i₁ , h ] , i₂ ] ∘ out                                                          ∎ }))) ⟩∘⟨refl ⟩ 
-      u (Terminal.! (coalgebras Y)) ∘ g ≈⟨ (Terminal.!-unique (coalgebras Y) (record { f = extend' ([ now , i ]) ; commutes = begin 
+      u (Terminal.! (coalgebras Y)) ∘ g ≈⟨ (Terminal.!-unique (coalgebras Y) {A = record { A = A (Terminal.⊤ (coalgebras (Y + X))) ; α = [ [ i₁ , h ] , i₂ ] ∘ out }} (record { f = extend' ([ now , i ]) ; commutes = begin 
         out ∘ extend' ([ now , i ])                                                                                         ≈⟨ extendlaw ([ now , i ]) ⟩ 
         [ out ∘ [ now , i ] , i₂ ∘ extend' ([ now , i ]) ] ∘ out                                                            ≈⟨ ([]-cong₂ ∘[] refl) ⟩∘⟨refl ⟩ 
         [ [ out ∘ now , out ∘ i ] , i₂ ∘ extend' ([ now , i ]) ] ∘ out                                                      ≈⟨ ([]-cong₂ ([]-cong₂ unitlaw (helper i eqi)) refl) ⟩∘⟨refl ⟩ 

agda/src/Monad/Instance/Delay/Quotienting.lagda.md

@@ -1,159 +0,0 @@
-<!--
-```agda
-open import Level
-
-open import Categories.Functor
-open import Category.Ambient using (Ambient)
-open import Categories.Monad
-open import Categories.Monad.Construction.Kleisli
-open import Categories.Monad.Relative renaming (Monad to RMonad)
-open import Data.Product using (_,_; Σ; Σ-syntax)
-open import Categories.Functor.Algebra
-open import Categories.Functor.Coalgebra
-open import Categories.Object.Terminal
-open import Categories.NaturalTransformation.Core
-```
--->
-
-```agda
-module Monad.Instance.Delay.Quotienting {o ℓ e} (ambient : Ambient o ℓ e) where
-  open Ambient ambient
-  open import Categories.Diagram.Coequalizer C 
-  open import Monad.Instance.Delay ambient
-  open F-Coalgebra-Morphism using () renaming (f to u; commutes to coalg-commutes)
-```
-
-
-# Quotienting the delay monad by weak bisimilarity
-
-The coinductive definition of the delay monad yields a 'wrong' kind of equality called *strong bisimilarity*, which differentiates between computations with different execution times, instead we want two computations to be equal, when they both terminate with the same result (or don't terminate at all).
-This is called *weak bisimilarity*. The ideas is then to quotient the delay monad with this 'right' kind of equality and show that the result $\tilde{D}$ is again a (strong) monad.
-
-In category theory existence of **coequalizers** corresponds to qoutienting, so we will express the quotiented delay monad via the following coequalizer:
-
-<!-- https://q.uiver.app/#q=WzAsMyxbMCwwLCJEKFggXFx0aW1lcyBcXG1hdGhiYntOfSkiXSxbMiwwLCJEWCJdLFs0LDAsIlxcdGlsZGV7RH1YIl0sWzEsMiwiXFxyaG9fWCJdLFswLDEsIkQgXFxwaV8xIiwyLHsib2Zmc2V0IjoxfV0sWzAsMSwiXFxpb3RhXioiLDAseyJvZmZzZXQiOi0xfV1d -->
-<iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsMyxbMCwwLCJEKFggXFx0aW1lcyBcXG1hdGhiYntOfSkiXSxbMiwwLCJEWCJdLFs0LDAsIlxcdGlsZGV7RH1YIl0sWzEsMiwiXFxyaG9fWCJdLFswLDEsIkQgXFxwaV8xIiwyLHsib2Zmc2V0IjoxfV0sWzAsMSwiXFxpb3RhXioiLDAseyJvZmZzZXQiOi0xfV1d&embed" width="765" height="176" style="border-radius: 8px; border: none;"></iframe>
-
-## Preliminaries
-
-Existence of the coequalizer doesn't suffice, we will need some conditions having to do with preservation of the coequalizer, so let's first define what it means for a coequalizer to be preserved by an endofunctor:
-
-```agda
-  preserves : ∀ {X Y} {f g : X ⇒ Y} → Endofunctor C → Coequalizer f g → Set (o ⊔ ℓ ⊔ e)
-  preserves {X} {Y} {f} {g} F coeq = IsCoequalizer (Functor.₁ F f) (Functor.₁ F g) (Functor.₁ F (Coequalizer.arr coeq))
-```
-
-We will now show that the following conditions are equivalent:
-
-1. For every $X$, the coequalizer is preserved by $D$
-2. every $\tilde{D}X$ extends to a search-algebra, so that each $ρ_X$ is a D-algebra morphism
-3. for every $X$, $(\tilde{D}X, ρ ∘ now : X → \tilde{D}X)$ is a stable free elgot algebra on X, $ρ_X$ is a D-algebra morphism and $ρ_X = ((ρ_X ∘ now + id) ∘ out)^\#$
-4. $\tilde{D}$ extends to a strong monad, so that $ρ$ is a strong monad morphism
-
-```agda
-  module _ (D : DelayM) where
-    open DelayM D renaming (functor to D-Functor; monad to D-Monad; kleisli to D-Kleisli)
-
-    open Functor D-Functor using () renaming (F₁ to D₁; homomorphism to D-homomorphism; F-resp-≈ to D-resp-≈; identity to D-identity)
-    open RMonad D-Kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ; identityˡ to k-identityˡ)
-    open Monad D-Monad using () renaming (assoc to M-assoc; identityʳ to M-identityʳ)
-    open HomReasoning
-    open M C
-    open MR C
-    open Equiv
-
-    module Quotiented (coeqs : ∀ X → Coequalizer (extend (ι {X})) (D₁ π₁)) where
-
-      Ď₀ : Obj → Obj
-      Ď₀ X = Coequalizer.obj (coeqs X)
-
-      ρ : ∀ {X} → D₀ X ⇒ Ď₀ X
-      ρ {X} = Coequalizer.arr (coeqs X)
-
-      ρ-epi : ∀ {X} → Epi (ρ {X})
-      ρ-epi {X} = Coequalizer⇒Epi (coeqs X)
-
-      ρ▷ : ∀ {X} → ρ ∘ ▷ ≈ ρ {X}
-      ρ▷ {X} = sym (begin 
-        ρ ≈⟨ introʳ intro-helper ⟩ 
-        ρ ∘ D₁ π₁ ∘ D₁ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ pullˡ (sym equality) ⟩ 
-        (ρ ∘ extend ι) ∘ D₁ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ pullʳ (sym k-assoc) ⟩ 
-        ρ ∘ extend (extend ι ∘ now ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩) ≈⟨ (refl⟩∘⟨ extend-≈ (pullˡ k-identityʳ)) ⟩ 
-        ρ ∘ extend (ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩) ≈⟨ (refl⟩∘⟨ extend-≈ helper) ⟩ 
-        ρ ∘ extend (▷ ∘ now) ≈⟨ (refl⟩∘⟨ sym (▷∘extendʳ now)) ⟩ 
-        ρ ∘ extend now ∘ ▷ ≈⟨ elim-center k-identityˡ ⟩ 
-        ρ ∘ ▷ ∎)
-        where
-          open Coequalizer (coeqs X) using (equality; coequalize; id-coequalize; coequalize-resp-≈) renaming (universal to coeq-universal; unique to coeq-unique; unique′ to coeq-unique′)
-          intro-helper : D₁ π₁ ∘ D₁ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈ idC
-          intro-helper = sym D-homomorphism ○ D-resp-≈ project₁ ○ D-identity
-          helper : ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈ ▷ ∘ now
-          helper = begin 
-            ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ 
-            (out⁻¹ ∘ out) ∘ ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ pullʳ (pullˡ (coalg-commutes ((Terminal.! (coalgebras X) {A = record { A = X × N ; α = _≅_.from nno-iso }})))) ⟩
-            out⁻¹ ∘ ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl)) ⟩
-            out⁻¹ ∘ ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ (idC ⁂ s) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym inject₂ ⟩∘⟨refl) ⟩
-            out⁻¹ ∘ ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ (_≅_.to nno-iso ∘ i₂) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ (pullʳ (pullˡ (cancelˡ (_≅_.isoʳ nno-iso))))) ⟩
-            out⁻¹ ∘ (idC +₁ ι) ∘ i₂ ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ pullˡ +₁∘i₂) ⟩
-            out⁻¹ ∘ (i₂ ∘ ι) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym inject₁) ⟩
-            out⁻¹ ∘ (i₂ ∘ ι) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ (refl⟩∘⟨ intro-center (_≅_.isoˡ out-≅) ⟩∘⟨refl) ⟩
-            out⁻¹ ∘ (i₂ ∘ (out⁻¹ ∘ out) ∘ ι) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ (refl⟩∘⟨ (refl⟩∘⟨ pullʳ (coalg-commutes ((Terminal.! (coalgebras X) {A = record { A = X × N ; α = _≅_.from nno-iso }})))) ⟩∘⟨refl) ⟩
-            out⁻¹ ∘ (i₂ ∘ out⁻¹ ∘ (idC +₁ ι) ∘ _≅_.from nno-iso) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ (refl⟩∘⟨ (pullʳ (pullˡ (pullʳ (cancelʳ (_≅_.isoʳ nno-iso)))))) ⟩
-            out⁻¹ ∘ i₂ ∘ (out⁻¹ ∘ (idC +₁ ι)) ∘ i₁ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ pullʳ +₁∘i₁) ⟩
-            out⁻¹ ∘ i₂ ∘ out⁻¹ ∘ i₁ ∘ idC ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ) ⟩
-            out⁻¹ ∘ i₂ ∘ out⁻¹ ∘ i₁ ≈⟨ ((refl⟩∘⟨ sym-assoc) ○ assoc²'') ⟩
-            ▷ ∘ now ∎
-
-      Ď-Functor : Endofunctor C
-      Ď-Functor = record
-        { F₀ = Ď₀
-        ; F₁ = F₁'
-        ; identity = λ {X} → Coequalizer.coequalize-resp-≈ (coeqs X) (elimʳ D-identity) ○ sym (Coequalizer.id-coequalize (coeqs X))
-        ; homomorphism = λ {X} {Y} {Z} {f} {g} → sym (Coequalizer.unique (coeqs X) (sym (begin 
-          (F₁' g ∘ F₁' f) ∘ ρ ≈⟨ pullʳ (sym (Coequalizer.universal (coeqs X))) ⟩ 
-          F₁' g ∘ ρ ∘ D₁ f ≈⟨ pullˡ (sym (Coequalizer.universal (coeqs Y))) ⟩
-          (ρ ∘ D₁ g) ∘ D₁ f ≈⟨ pullʳ (sym D-homomorphism) ⟩
-          ρ ∘ D₁ (g ∘ f) ∎)))
-        ; F-resp-≈ = λ {X} {Y} {f} {g} eq → Coequalizer.coequalize-resp-≈ (coeqs X) (refl⟩∘⟨ (D-resp-≈ eq))
-        }
-        where
-          F₁' : ∀ {X} {Y} (f : X ⇒ Y) → Ď₀ X ⇒ Ď₀ Y
-          F₁' {X} {Y} f = coequalize {h = ρ ∘ D₁ f} (begin 
-            (ρ ∘ D₁ f) ∘ extend ι ≈⟨ pullʳ (sym k-assoc) ⟩ 
-            ρ ∘ extend (extend (now ∘ f) ∘ ι) ≈⟨ refl⟩∘⟨ (extend-≈ (sym (Terminal.!-unique (coalgebras Y) (record { f = extend (now ∘ f) ∘ ι ; commutes = begin 
-              out ∘ extend (now ∘ f) ∘ ι ≈⟨ pullˡ (extendlaw (now ∘ f)) ⟩ 
-              ([ out ∘ now ∘ f , i₂ ∘ D₁ f ] ∘ out) ∘ ι ≈⟨ pullʳ (coalg-commutes (Terminal.! (coalgebras X) {A = record { A = X × N ; α = _≅_.from nno-iso }})) ⟩ 
-              [ out ∘ now ∘ f , i₂ ∘ D₁ f ] ∘ (idC +₁ ι) ∘  _≅_.from nno-iso ≈⟨ (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl) ⟩ 
-              (f +₁ D₁ f) ∘ (idC +₁ ι) ∘ _≅_.from nno-iso ≈⟨ pullˡ +₁∘+₁ ⟩ 
-              (f ∘ idC +₁ D₁ f ∘ ι) ∘ _≅_.from nno-iso ≈⟨ ((+₁-cong₂ id-comm (sym identityʳ)) ⟩∘⟨refl) ⟩ 
-              (idC ∘ f +₁ (D₁ f ∘ ι) ∘ idC) ∘ _≅_.from nno-iso ≈⟨ sym (pullˡ +₁∘+₁) ⟩ 
-              (idC +₁ extend (now ∘ f) ∘ ι) ∘ (f +₁ idC) ∘ _≅_.from nno-iso ∎ })))) ⟩
-            ρ ∘ extend (u (Terminal.! (coalgebras Y) {A = record { A = X × N ; α = (f +₁ idC) ∘ _≅_.from nno-iso }})) ≈⟨ (refl⟩∘⟨ (extend-≈ (Terminal.!-unique (coalgebras Y) (record { f = ι ∘ (f ⁂ idC) ; commutes = begin 
-              out ∘ ι ∘ (f ⁂ idC) ≈⟨ pullˡ (coalg-commutes (Terminal.! (coalgebras Y) {A = record { A = Y × N ; α = _≅_.from nno-iso }})) ⟩ 
-              ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ (f ⁂ idC) ≈⟨ assoc ⟩ 
-              (idC +₁ ι) ∘ _≅_.from nno-iso ∘ (f ⁂ idC) ≈⟨ (refl⟩∘⟨ (introʳ (_≅_.isoˡ nno-iso))) ⟩ 
-              (idC +₁ ι) ∘ (_≅_.from nno-iso ∘ (f ⁂ idC)) ∘ [ ⟨ idC , z ∘ Terminal.! terminal ⟩ , idC ⁂ s ] ∘ _≅_.from nno-iso ≈⟨ (refl⟩∘⟨ pullʳ (pullˡ ∘[])) ⟩ 
-              (idC +₁ ι) ∘ _≅_.from nno-iso ∘ [ (f ⁂ idC) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ , (f ⁂ idC) ∘ (idC ⁂ s) ] ∘ _≅_.from nno-iso ≈⟨ (refl⟩∘⟨ (refl⟩∘⟨ (([]-cong₂ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) (⁂∘⁂ ○ ⁂-cong₂ identityʳ identityˡ)) ⟩∘⟨refl))) ⟩ 
-              (idC +₁ ι) ∘ _≅_.from nno-iso ∘ [ ⟨ f , z ∘ Terminal.! terminal ⟩ , (f ⁂ s) ] ∘ _≅_.from nno-iso ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ refl (refl⟩∘⟨ Terminal.!-unique terminal (Terminal.! terminal ∘ f))) refl ⟩∘⟨refl) ⟩ 
-              (idC +₁ ι) ∘ _≅_.from nno-iso ∘ [ ⟨ f , z ∘ Terminal.! terminal ∘ f ⟩ , (f ⁂ s) ] ∘ _≅_.from nno-iso ≈⟨ sym (refl⟩∘⟨ refl⟩∘⟨ []-cong₂ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ assoc) (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ) ⟩∘⟨refl) ⟩ 
-              (idC +₁ ι) ∘ _≅_.from nno-iso ∘ [ ⟨ idC , z ∘ Terminal.! terminal ⟩ ∘ f , (idC ⁂ s) ∘ (f ⁂ idC) ] ∘ _≅_.from nno-iso ≈⟨ sym (refl⟩∘⟨ (pullʳ (pullˡ []∘+₁))) ⟩ 
-              (idC +₁ ι) ∘ (_≅_.from nno-iso ∘ [ ⟨ idC , z ∘ Terminal.! terminal ⟩ , idC ⁂ s ]) ∘ (f +₁ (f ⁂ idC)) ∘ _≅_.from nno-iso ≈⟨ sym (refl⟩∘⟨ introˡ (_≅_.isoʳ nno-iso)) ⟩ 
-              (idC +₁ ι) ∘ (f +₁ (f ⁂ idC)) ∘ _≅_.from nno-iso ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl) ⟩ 
-              (f +₁ ι ∘ (f ⁂ idC)) ∘ _≅_.from nno-iso ≈⟨ sym (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ)) ⟩
-              (idC +₁ ι ∘ (f ⁂ idC)) ∘ (f +₁ idC) ∘ _≅_.from nno-iso ∎ })))) ⟩
-            ρ ∘ extend (ι ∘ (f ⁂ idC)) ≈⟨ (refl⟩∘⟨ extend-≈ (pushˡ (sym k-identityʳ))) ⟩
-            ρ ∘ extend (extend ι ∘ now ∘ (f ⁂ idC)) ≈⟨ pushʳ k-assoc ⟩
-            (ρ ∘ extend ι) ∘ D₁ (f ⁂ idC) ≈⟨ pushˡ (Coequalizer.equality (coeqs Y)) ⟩
-            ρ ∘ D₁ π₁ ∘ D₁ (f ⁂ idC) ≈⟨ refl⟩∘⟨ sym D-homomorphism ⟩
-            ρ ∘ D₁ (π₁ ∘ (f ⁂ idC)) ≈⟨ (refl⟩∘⟨ (D-resp-≈ project₁)) ⟩
-            ρ ∘ D₁ (f ∘ π₁) ≈⟨ pushʳ D-homomorphism ⟩
-            (ρ ∘ D₁ f) ∘ D₁ π₁ ∎)
-            where 
-              open Coequalizer (coeqs X) using (coequalize; equality) renaming (universal to coeq-universal)
-
-      ρ-natural : NaturalTransformation D-Functor Ď-Functor
-      ρ-natural = ntHelper (record 
-        { η = λ X → ρ {X} 
-        ; commute = λ {X} {Y} f → Coequalizer.universal (coeqs X)
-        })
-```

agda/src/Monad/Instance/Delay/Strong.lagda.md

@@ -100,7 +100,7 @@ module Monad.Instance.Delay.Strong {o ℓ e} (ambient : Ambient o ℓ e) (D : De
             out ∘ extend (now ∘ π₂) ∘ τ _ ∘ idC                                                                                           ≈⟨ pullˡ diag₃ ⟩ 
             ((π₂ +₁ extend (now ∘ π₂)) ∘ out) ∘ τ _ ∘ idC                                                                                 ≈⟨ pullʳ (pullˡ (diag₂ (Terminal.⊤ terminal , X))) ⟩ 
             (π₂ +₁ extend (now ∘ π₂)) ∘ ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ idC                                                ≈⟨ refl⟩∘⟨ (pullʳ (assoc ○ sym diag₁)) ⟩ 
-            (π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _) ∘ (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (_≅_.isoˡ ⊤×A≅A) identity² ○ CC.+-unique ((identity² ⟩∘⟨refl) ○ id-comm-sym) ((identity² ⟩∘⟨refl) ○ id-comm-sym)) ) ⟩ 
+            (π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _) ∘ (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (_≅_.isoˡ ⊤×A≅A) identity² ○ []-unique ((identity² ⟩∘⟨refl) ○ id-comm-sym) ((identity² ⟩∘⟨refl) ○ id-comm-sym)) ) ⟩ 
             (π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)                                          ≈⟨ pullˡ +₁∘+₁ ⟩ 
             (π₂ ∘ idC +₁ extend (now ∘ π₂) ∘ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)                                             ≈⟨ (+₁-cong₂ id-comm refl) ⟩∘⟨refl ⟩ 
             (idC ∘ π₂ +₁ extend (now ∘ π₂) ∘ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)                                             ≈˘⟨ pullˡ +₁∘+₁ ⟩ 
@@ -121,7 +121,7 @@ module Monad.Instance.Delay.Strong {o ℓ e} (ambient : Ambient o ℓ e) (D : De
             diag₁ = begin 
               (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩ 
               (⟨ Terminal.! terminal , idC ⟩ ∘ π₂ +₁ idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)    ≈⟨ +₁-cong₂ (_≅_.isoˡ ⊤×A≅A) identity² ⟩∘⟨ (refl⟩∘⟨ sym identityʳ) ⟩ 
-              (idC +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ idC                                   ≈⟨ elimˡ (CC.+-unique id-comm-sym id-comm-sym) ⟩ 
+              (idC +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ idC                                   ≈⟨ elimˡ ([]-unique id-comm-sym id-comm-sym) ⟩ 
               distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ idC                                                  ∎
             diag₂ = τ-law
             diag₃ : out {X} ∘ extend (now ∘ π₂ {A = Terminal.⊤ terminal} {B = X}) ≈ (π₂ +₁ extend (now ∘ π₂)) ∘ out

agda/src/Monad/Instance/Setoids/Delay.lagda.md

@@ -375,6 +375,24 @@ module DelayMonad where
 
 open DelayMonad
 
+-- custom definition of natural numbers together with the setoid on ℕ with propositional equality
+module nat {ℓ} where
+  data ℕ : Set ℓ where
+    zero : ℕ
+    suc : ℕ → ℕ
+
+  ℕ-setoid : Setoid ℓ ℓ
+  ℕ-setoid = record 
+    { Carrier = ℕ 
+    ; _≈_ = _≡_ 
+    ; isEquivalence = Eq.isEquivalence 
+    }
+
+  suc-inj : ∀ {n m} → suc n ≡ suc m → n ≡ m
+  suc-inj Eq.refl = Eq.refl
+
+open nat
+
 module extra {A : Setoid c (c ⊔ ℓ)} where
   ≲→≈  : {x y : Delay ∣ A ∣}  → [ A ][ x ≲ y ] → [ A ][ x ≈ y ]
   ≲→≈′ : {x y : Delay ∣ A ∣} → [ A ][ x ≲′ y ] → [ A ][ x ≈′ y ]

agda/src/Monad/Instance/Setoids/K.lagda.md

@@ -30,17 +30,18 @@ open import Categories.Category.Instance.Properties.Setoids.CCC using (Setoids-C
 module Monad.Instance.Setoids.K {ℓ : Level} where
   open _⟶_ using (cong)
   open import Category.Ambient.Setoids
-  open Ambient (setoidAmbient {ℓ}) using (cocartesian; distributive)
+  open Ambient (setoidAmbient {ℓ} {ℓ}) using (cocartesian; distributive)
   open import Monad.Instance.Setoids.Delay {ℓ} {ℓ}
-  open import Monad.Instance.K (setoidAmbient {ℓ})
+  open import Monad.Instance.K (setoidAmbient {ℓ} {ℓ})
   open import Algebra.Elgot cocartesian
   open import Algebra.Elgot.Free cocartesian
   open import Algebra.Elgot.Stable distributive
   open import Category.Construction.ElgotAlgebras {C = Setoids ℓ ℓ} cocartesian
-  open import Monad.PreElgot (setoidAmbient {ℓ})
+  open import Monad.PreElgot (setoidAmbient {ℓ} {ℓ})
   open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _↓_ to [_][_↓_])
   open DelayMonad
   open extra
+  open nat
   open Setoid using () renaming (Carrier to ∣_∣; _≈_ to [_][_≡_])
   open eq using () renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans)
 
@@ -297,6 +298,14 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
 
     delay-lift' = record { to = < helper # > ; cong = helper#≈-cong }
 
+
+    -- interesting note:
+    -- the following definition prevents more general universe levels, i.e. we would like to parametrize this module by two levels c and ℓ, one for carriers and one for proofs.
+    -- but adopting this approach would force us to talk about setoids of type Setoid ℓ (c ⊔ ℓ), this does not work with the definition below,
+    -- since propositional equality lives on the same level as values, this means the type below would have to look like:
+    -- ‖_‖ : Setoid c (c ⊔ ℓ) → Setoid c c
+    -- this in turn does not play together nicely with later definition.
+
     -- discretize a setoid
     ‖_‖ : Setoid ℓ ℓ → Setoid ℓ ℓ
     ∣_∣ ‖ X ‖      = ∣ X ∣

agda/src/index.lagda.md

@@ -35,12 +35,6 @@ open import Monad.Instance.Delay.Strong
 open import Monad.Instance.Delay.Commutative
 ```
 
-The next step is to quotient the delay monad by weak bisimilarity, but this quotiented structure is not monadic, so we postulate conditions under which it extends to a monad.
-
-```agda
-open import Monad.Instance.Delay.Quotienting
-```
-
 ### Monad K
 
 The goal of this last section is to formalize an equational lifting monad **K** that generalizes both the maybe monad and the delay monad.
@@ -103,7 +97,7 @@ open import Monad.Instance.K.StrongPreElgot
 ### A case study on setoids
 Lastly we do a case study on the category of setoids.
 
-First we look at the (quotiented delay monad) on setoids:
+First we look at the (quotiented) delay monad on setoids:
 
 ```agda
 open import Monad.Instance.Setoids.Delay

thesis/agda/motivation.agda

@@ -1,75 +0,0 @@
-{-# OPTIONS --guardedness #-}
-
--- Take this example as motivation:
--- https://stackoverflow.com/questions/21808186/agda-reading-a-line-of-standard-input-as-a-string-instead-of-a-costring
-
-open import Level
-open import Agda.Builtin.Coinduction
-module thesis.motivation where
-
-module old-delay where
-  private
-    variable
-      a : Level
-  data _⊥ (A : Set a) : Set a where
-    now : A → A ⊥
-    later : ∞ (A ⊥) → A ⊥
-
-  never : ∀ {A : Set a} → A ⊥
-  never = later (♯ never)
-
-module ReverseInput where
-  open import Data.Char
-  open import Data.Nat
-  open import Data.List using (List; []; _∷_)
-  open import Data.String
-  open import Data.Unit.Polymorphic
-  open import Codata.Musical.Costring
-  open import Codata.Musical.Colist using ([]; _∷_)
-  -- open import IO using (IO; seq; bind; return; Main; run; putStrLn)
-  open import IO.Primitive
-  open import IO.Primitive.Infinite using (getContents)
-  open import Agda.Builtin.IO using ()
-
-  open old-delay
-  -- IDEA: start in haskell, then motivate in agda and define delay type
-  -- next talk about bisimilarity.
-  -- idea for slide title: dlrowolleh.hs and dlrowolleh.agda
-
-  private
-    variable
-      a : Level
-
-  -- reverse : Costring → String ⊥
-  -- reverse = go []
-  --   where
-  --   go : List Char → Costring → String ⊥
-  --   go acc []       = now (fromList acc)
-  --   go acc (x ∷ xs) = later (♯ go (x ∷ acc) (♭ xs))
-
-  -- putStrLn⊥ : String ⊥ → IO {a} ⊤
-  -- putStrLn⊥ (now   s) = putStrLn s
-  -- putStrLn⊥ (later s) = seq (♯ return tt) (♯ putStrLn⊥ (♭ s))
-
-  -- main : Main
-  -- main = run (bind (♯ {!  getContents !}) {!   !}) --(λ c → ♯ putStrLn⊥ (reverse c)))
-
--- NOTE: This is not very understandable... Better stick to the outdated syntax
-module delay where
-  mutual
-    data _⊥ (A : Set) : Set where
-      now : A → A ⊥
-      later : A ⊥' → A ⊥
-    
-    record _⊥' (A : Set) : Set where
-      coinductive
-      field
-        force : A ⊥
-  open _⊥'
-
-  mutual
-    never : ∀ {A : Set} → A ⊥
-    never = later never'
-
-    never' : ∀ {A : Set} → A ⊥'
-    force never' = never

thesis/agda/setoids.agda

@@ -0,0 +1,47 @@
+module Foo where
+  open import Level
+
+  record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
+    constructor _,_
+    field
+      fst : A
+      snd : B
+  open _×_
+
+  <_,_> : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} 
+          → (A → B) → (A → C) → A → (B × C)
+  < f , g > x = (f x , g x)
+
+  record ⊤ {l} : Set l where
+    constructor tt
+  
+  ! : ∀ {l} {X : Set l} → X → ⊤ {l}
+  ! _ = tt
+
+  data _+_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
+    i₁ : A → A + B
+    i₂ : B → A + B 
+
+  [_,_] : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
+          → (A → C) → (B → C) → (A + B) → C
+  [ f , g ] (i₁ x) = f x
+  [ f , g ] (i₂ x) = g x
+
+  data ⊥ {l} : Set l where
+
+  ¡ : ∀ {l} {X : Set l} → ⊥ {l} → X
+  ¡ ()
+
+  distributeˡ⁻¹ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → (A × B) + (A × C) → A × (B + C)
+  distributeˡ⁻¹ (i₁ (x , y)) = (x , i₁ y)
+  distributeˡ⁻¹ (i₂ (x , y)) = (x , i₂ y)
+
+  distributeˡ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → A × (B + C) → (A × B) + (A × C)
+  distributeˡ (x , i₁ y) = i₁ (x , y)
+  distributeˡ (x , i₂ y) = i₂ (x , y) 
+
+  curry : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → (C × A → B) → C → A → B
+  curry f x y = f (x , y)
+
+  eval : ∀ {a b} {A : Set a} {B : Set b} → ((A → B) × A) → B
+  eval (f , x) = f x

thesis/bib.bib

@@ -240,3 +240,10 @@
   biburl     = {https://dblp.org/rec/journals/corr/GoncharovSR14.bib},
   bibsource  = {dblp computer science bibliography, https://dblp.org}
 }
+
+@online{nad-delay,
+  author = {Nils Anders Danielsson},
+  title = {The delay monad, defined coinductively},
+  url = {https://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.html},
+  urldate = {2024-15-02}
+}

thesis/main.tex

@@ -10,7 +10,8 @@
   breaklines=true,
   encoding=utf8,
   fontsize=\small,
-  frame=lines
+  frame=lines,
+  autogobble
 }
 \usepackage[dvipsnames]{xcolor}  % Coloured text etc.
 \usepackage{amssymb}

thesis/src/05_setoids.tex

@@ -18,9 +18,88 @@ Morphisms between setoids are functions that respect the equivalence relation:
 
 Setoids and setoid morphisms form a category that we call $\setoids$.
 
+\improvement[inline]{Talk about equality between setoid morphisms}
 \improvement[inline]{Text is not good}
-\todo[inline]{sketch the proof that setoids is CCC and cocartesian}
 
+\begin{lemma}
+  $\setoids$ is a distributive category.
+\end{lemma}
+\begin{proof}
+  To show that $\setoids$ is (co-)cartesian we will give the respective datatypes and unique morphisms, this also introduces notation we will use for the rest of the chapter. We will not include the proofs that the morphisms are setoid morphisms, these can be looked up in the agda standard library.
+
+  \begin{itemize}
+    \item \textbf{Products}:
+    \begin{minted}{agda}
+      record _×_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
+        constructor _,_
+        field
+          fst : A
+          snd : B
+  
+      <_,_> : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} 
+              → (A → B) → (A → C) → A → (B × C)
+      < f , g > x = (f x , g x)
+    \end{minted}
+    \item \textbf{Terminal Object}:
+    \begin{minted}{agda}
+      record ⊤ {l} : Set l where
+        constructor tt
+    
+      ! : ∀ {l} {X : Set l} → X → ⊤ {l}
+      ! _ = tt
+    \end{minted}
+    \item \textbf{Coproducts}:
+    \begin{minted}{agda}
+      data _+_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
+        i₁ : A → A + B
+        i₂ : B → A + B 
+    
+      [_,_] : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
+              → (A → C) → (B → C) → (A + B) → C
+      [ f , g ] (i₁ x) = f x
+      [ f , g ] (i₂ x) = g x
+    \end{minted}
+    \item \textbf{Initial Object}:
+    \begin{minted}{agda}
+      data ⊥ {l} : Set l where
+
+      ¡ : ∀ {l} {X : Set l} → ⊥ {l} → X
+      ¡ ()    
+    \end{minted}
+  \end{itemize}
+
+  Lastly we need to show that the canonical distributivity morphism is an iso. Recall that the canonical distributive morphism is defined as $dstl^{-1} = [ id \times i_1 , id \times i_2 ] : A \times B + A \times C \rightarrow A \times (B + C)$. This corresponds to the following definition using pattern matching:
+  \begin{minted}{agda}
+    distributeˡ⁻¹ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} 
+                    → (A × B) + (A × C) → A × (B + C)
+    distributeˡ⁻¹ (i₁ (x , y)) = (x , i₁ y)
+    distributeˡ⁻¹ (i₂ (x , y)) = (x , i₂ y)
+  \end{minted}
+  The inverse can be defined similarly:
+  \begin{minted}{agda}
+    distributeˡ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} 
+                  → A × (B + C) → (A × B) + (A × C)
+    distributeˡ (x , i₁ y) = i₁ (x , y)
+    distributeˡ (x , i₂ y) = i₂ (x , y)
+  \end{minted}
+  Then these functions are inverse by definition and it is easy to show that they are setoid morphisms.
+\end{proof}
+
+\begin{lemma}
+  $\setoids$ is cartesian closed.
+\end{lemma}
+\begin{proof}
+  We have already shown that $\setoids$ is cartesian, we need to show that given two setoids $(A, =^A), (B, =^B)$ we can construct an exponential object.
+  Indeed take the function space setoid $(A \rightarrow B, \doteq)$ where $\doteq$ is pointwise equality of setoid morphisms i.e. $f , g : A \rightarrow B$ are pointwise equal $f \doteq g$ \textit{iff} $f x =^B g x$ for any $x : A$. $curry$ and $eval$ are then defined as usual:
+  \begin{minted}{agda}
+    curry : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} 
+            → (C × A → B) → C → A → B
+    curry f x y = f (x , y) 
+
+    eval : ∀ {a b} {A : Set a} {B : Set b} → ((A → B) × A) → B
+    eval (f , x) = f x
+  \end{minted}
+\end{proof}
 
 \section{Quotienting the Delay Monad}
 % TODO merge this into introduction
@@ -31,14 +110,14 @@ Setoids and setoid morphisms form a category that we call $\setoids$.
 Originally the delay monad has been introduced as a coinductive datatype with two constructors, in pseudo Agda-like code this would look something like:
 \begin{minted}{agda}
 codata (A : Set) : Set where
-  now   : A → Delay A
+  now   : A       → Delay A
   later : Delay A → Delay A
 \end{minted}
 
-This style is sometimes called \textit{positively coinductive} and is nowadays advised against in the manuals of both Agda and Coq\todo{cite}. Instead one is advised to use coinductive records, we will heed this advice and use the following representation of the delay monad in Agda:
+This style is sometimes called \textit{positively coinductive} and is nowadays advised against in the manuals of both Agda and Coq\todo{cite}. Instead one is advised to use coinductive records, we will heed this advice and use the following representation of the delay monad in Agda:\change{rephrase}
 
 \todo[inline]{cite https://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.html somehow}
-
+\cite{nad-delay}
 \begin{minted}{agda}
 mutual
 data Delay (A : Set) : Set where