.gitignore

@@ -2,4 +2,3 @@
 *.pdf
 *.log
 Everything.agda
-public/

Makefile

@@ -20,10 +20,7 @@ open:
 
 push: all
 	mv public/Everything.html public/index.html
-	chmod +w public/Agda.css
+	scp -r public hy84coky@cip2a7.cip.cs.fau.de:.www/public
-	mv public bsc-thesis
-	scp -r bsc-thesis hy84coky@cip2a7.cip.cs.fau.de:.www/
-	mv bsc-thesis public
 
 
 Everything.agda:

src/Monad/Instance/Delay.lagda.md

@@ -1,5 +1,6 @@
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Categories.Category
 open import Categories.Monad
@@ -9,12 +10,10 @@ open import Categories.Category.Extensive
 open import Categories.Category.BinaryProducts
 open import Categories.Category.Cocartesian
 open import Categories.Category.Cartesian
-open import Categories.Category.Cartesian.Bundle
+open import Categories.Category.Cartesian
 open import Categories.Object.Terminal
-open import Categories.Object.Initial
 open import Categories.Object.Coproduct
 open import Categories.Category.Construction.F-Coalgebras
-open import Categories.Category.Construction.F-Algebras
 open import Categories.Functor.Coalgebra
 open import Categories.Functor
 open import Categories.Functor.Algebra
@@ -30,59 +29,50 @@ import Categories.Morphism.Reasoning as MR
 ## Summary
 This file introduces the delay monad ***D***
 
+- [ ] *Proposition 1* Characterization of the delay monad ***D***
+- [ ] *Proposition 2* ***D*** is commutative
+
 ## Code
 
 ```agda
 module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
-```
-<!--
-```agda
   open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
   open Cocartesian (Extensive.cocartesian extensive)
   open Cartesian (ExtensiveDistributiveCategory.cartesian ED)
   open BinaryProducts products
 
-  CC : CartesianCategory o ℓ e
-  CC = record { U = C ; cartesian = (ExtensiveDistributiveCategory.cartesian ED) }
-
-  open import Categories.Object.NaturalNumbers.Parametrized CC
-  open import Categories.Object.NaturalNumbers.Properties.F-Algebras using (PNNO⇒Initial₂; PNNO-Algebra)
-
   open M C
   open MR C
   open Equiv
   open HomReasoning
   open CoLambek
-  open F-Coalgebra-Morphism renaming (f to u)
-  open F-Coalgebra
 ```
--->
+### *Proposition 1*: Characterization of the delay monad ***D***
-
-The Delay monad is usually described by existence of final coalgebras for the functor `(X + -)` where `X` is some arbitrary object.
-This functor trivially sends objects `Y` to `X + Y` and functions `f` to `id + f`.
 
 ```agda
+  delayF : Obj → Endofunctor C
+  delayF Y = record
+    { F₀ = Y +_
+    ; F₁ = idC +₁_
+    ; identity = CC.coproduct.unique id-comm-sym id-comm-sym
+    ; homomorphism = ⟺ (+₁∘+₁ ○ +₁-cong₂ identity² refl) 
+    ; F-resp-≈ = +₁-cong₂ refl
+    }
+
   record DelayM : Set (o ⊔ ℓ ⊔ e) where
     field
-      coalgebras : ∀ (A : Obj) → Terminal (F-Coalgebras (A +-))
+      algebras : ∀ (A : Obj) → Terminal (F-Coalgebras (delayF A))
-```
     
-These are all the fields this record needs! 
+    module D A = Functor (delayF A)
-Of course this doesn't tell us very much, so our goal will be to extract a monad from this definition.
-
-Conventionally the delay monad is described via functions `now` and `later` where the former lifts a value into a computation and the latter postpones a computation by one time unit.
-We can now define these functions by bisecting the isomorphism `out : DX ≅ X + DX` which we get by Lambek's lemma. (Here `DX` is the element of the final coalgebra for `X`)
-
-```agda
 
     module _ (X : Obj) where
-      open Terminal (coalgebras X) using (⊤; !; !-unique)
+      open Terminal (algebras X) using (⊤; !)
       open F-Coalgebra ⊤ renaming (A to DX)
 
       D₀ = DX
 
       out-≅ : DX ≅ X + DX
-      out-≅ = colambek {F = X +- } (coalgebras X)
+      out-≅ = colambek {F = delayF X} (algebras X)
 
       -- note: out-≅.from ≡ ⊤.α
       open _≅_ out-≅ using () renaming (to to out⁻¹; from to out) public
@@ -93,204 +83,150 @@ We can now define these functions by bisecting the isomorphism `out : DX ≅ X +
       later : DX ⇒ DX
       later = out⁻¹ ∘ i₂
 
+      -- TODO inline
       unitlaw : out ∘ now ≈ i₁
       unitlaw = cancelˡ (_≅_.isoʳ out-≅)
-```
 
-Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use our terminal coalgebras to get a *coiteration operator* `coit`:
-
-TODO add diagram
-
-```agda
       module _ {Y : Obj} where 
         coit : Y ⇒ X + Y → Y ⇒ DX
-        coit f = u (! {A = record { A = Y ; α = f }})
+        coit f = F-Coalgebra-Morphism.f (! {A = record { A = Y ; α = f }})
 
         coit-commutes : ∀ (f : Y ⇒ X + Y) → out ∘ (coit f) ≈ (idC +₁ coit f) ∘ f
-        coit-commutes f = commutes (! {A = record { A = Y ; α = f }})
+        coit-commutes f = F-Coalgebra-Morphism.commutes (! {A = record { A = Y ; α = f }})
-```
-
-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.
-TODO add diagram
-
-```agda
-      module _ (ℕ : ParametrizedNNO) where
-        open ParametrizedNNO ℕ
-      
-        iso : X × N ≅ X + X × N
-        iso = Lambek.lambek (record { ⊥ = PNNO-Algebra CC coproducts X N z s ; ⊥-is-initial = PNNO⇒Initial₂ CC coproducts ℕ X })
-
-        ι : X × N ⇒ DX
-        ι = u (! {A = record { A = X × N ; α = _≅_.from iso }})
-```
-
-With these definitions at hand, we can now indeed construct a monad (in extension form) as the triple `(F₀, unit, extend)`.
-`F₀` corresponds to `D₀` of course and `unit` is `now`, the tricky part is kleisli lifting aka. `extend`.
-
-TODO
-
-
-```agda
-        
     monad : Monad C
     monad = Kleisli⇒Monad C (record
       { F₀ = D₀ 
       ; unit = λ {X} → now X
       ; extend = extend
-      ; identityʳ = identityʳ'
+      ; identityʳ = λ {X} {Y} {f} → begin 
-      ; identityˡ = identityˡ'
+        extend f ∘ now X                                          ≈⟨ (insertˡ (_≅_.isoˡ (out-≅ Y))) ⟩∘⟨refl ⟩ 
-      ; assoc = assoc'
-      ; sym-assoc = sym assoc'
-      ; extend-≈ = extend-≈'
-      })
-      where
-        open Terminal
-        module _ {X Y : Obj} (f : X ⇒ D₀ Y) where
-          alg : F-Coalgebra (Y +-)
-          alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ] }
-
-          extend : D₀ X ⇒ D₀ Y
-          extend = u (! (coalgebras Y) {A = alg}) ∘ i₁ {B = D₀ Y}
-
-          !∘i₂ : u (! (coalgebras Y) {A = alg}) ∘ i₂ ≈ idC
-          !∘i₂ = ⊤-id (coalgebras Y) (F-Coalgebras (Y +-) [ ! (coalgebras Y) ∘ record { f = i₂ ; commutes = inject₂ } ] )
-
-          extendlaw : out Y ∘ extend ≈ [ out Y ∘ f , i₂ ∘ extend ] ∘ out X
-          extendlaw = begin 
-            out Y ∘ extend ≈⟨ pullˡ (commutes (! (coalgebras Y) {A = alg})) ⟩ 
-            ((idC +₁ (u (! (coalgebras Y)))) ∘ α alg) ∘ i₁        ≈⟨ pullʳ inject₁ ⟩
-            (idC +₁ (u (! (coalgebras Y)))) ∘ [ [ i₁ , i₂ ∘ i₂ ] 
-            ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X                   ≈⟨ pullˡ ∘[] ⟩
-            [ (idC +₁ (u (! (coalgebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) 
-            , (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩
-            [ [ (idC +₁ (u (! (coalgebras Y)))) ∘ i₁ 
-              , (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) 
-            , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out X        ≈⟨ ([]-cong₂ 
-                                                                    (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) 
-                                                                    refl) ⟩∘⟨refl ⟩
-            [ [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₂ ] ∘ (out Y ∘ f) 
-            , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out X        ≈⟨ ([]-cong₂ 
-                                                                    (elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η))
-                                                                    assoc) ⟩∘⟨refl ⟩
-            [ out Y ∘ f , i₂ ∘ extend ] ∘ out X                 ∎ 
-
-          extend-unique : (g : D₀ X ⇒ D₀ Y) → (out Y ∘ g ≈ [ out Y ∘ f , i₂ ∘ g ] ∘ out X) → extend ≈ g
-          extend-unique g g-commutes = begin 
-            extend ≈⟨ (!-unique (coalgebras Y) (record { f = [ g , idC ] ; commutes = begin 
-              out Y ∘ [ g , idC ]                                          ≈⟨ ∘[] ⟩ 
-              [ out Y ∘ g , out Y ∘ idC ]                                  ≈⟨ []-cong₂ g-commutes identityʳ ⟩ 
-              [ [ out Y ∘ f , i₂ ∘ g ] ∘ out X , out Y ]                   ≈˘⟨ []-cong₂ 
-                                                                                (([]-cong₂ 
-                                                                                  (([]-cong₂ refl identityʳ) ⟩∘⟨refl ○ (elimˡ +-η)) 
-                                                                                  refl) 
-                                                                                ⟩∘⟨refl) 
-                                                                                refl ⟩ 
-              [ [ [ i₁ , i₂ ∘ idC ] ∘ (out Y ∘ f) 
-                , i₂ ∘ g ] ∘ out X 
-              , out Y ]                                                    ≈˘⟨ []-cong₂ 
-                                                                                (([]-cong₂ 
-                                                                                  (([]-cong₂ identityʳ (pullʳ inject₂)) ⟩∘⟨refl) 
-                                                                                  refl) 
-                                                                                ⟩∘⟨refl) 
-                                                                                refl 
-                                                                              ⟩
-              [ [ [ i₁ ∘ idC 
-                  , (i₂ ∘ [ g , idC ]) ∘ i₂ ] ∘ (out Y ∘ f) 
-                , i₂ ∘ g ] ∘ out X 
-              , out Y ]                                                    ≈˘⟨ []-cong₂ 
-                                                                                (([]-cong₂ 
-                                                                                  (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) 
-                                                                                  (pullʳ inject₁)) 
-                                                                                ⟩∘⟨refl) 
-                                                                                (elimˡ (Functor.identity (Y +-))) 
-                                                                              ⟩
-              [ [ [ (idC +₁ [ g , idC ]) ∘ i₁ 
-                  , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) 
-                , (i₂ ∘ [ g , idC ]) ∘ i₁ ] ∘ out X 
-              , (idC +₁ idC) ∘ out Y ]                                     ≈˘⟨ []-cong₂ 
-                                                                                (([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl) 
-                                                                                ((+₁-cong₂ identity² inject₂) ⟩∘⟨refl) ⟩
-              [ [ (idC +₁ [ g , idC ]) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) 
-                , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₁ ] ∘ out X 
-              , (idC ∘ idC +₁ [ g , idC ] ∘ i₂) ∘ out Y ]                  ≈˘⟨ []-cong₂ (pullˡ ∘[]) (pullˡ +₁∘+₁) ⟩
-              [ (idC +₁ [ g , idC ]) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X 
-              , (idC +₁ [ g , idC ]) ∘ (idC +₁ i₂) ∘ out Y ]               ≈˘⟨ ∘[] ⟩
-              (idC +₁ [ g , idC ]) ∘ α alg ∎ })) ⟩∘⟨refl ⟩ 
-            [ g , idC ] ∘ i₁                                               ≈⟨ inject₁ ⟩
-            g ∎
-
-        αf≈αg : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → α (alg f) ≈ α (alg g)
-        αf≈αg {X} {Y} {f} {g} eq = []-cong₂ ([]-cong₂ (refl⟩∘⟨ refl⟩∘⟨ eq) refl ⟩∘⟨refl) refl
-
-        alg-f≈alg-g : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → M._≅_ (F-Coalgebras (Y +-)) (alg f) (alg g)
-        alg-f≈alg-g {X} {Y} {f} {g} eq = record 
-          { from = record { f = idC ; commutes = begin 
-            α (alg g) ∘ idC          ≈⟨ identityʳ ⟩ 
-            α (alg g)                ≈⟨ ⟺ (αf≈αg eq) ⟩ 
-            α (alg f)                ≈˘⟨ elimˡ identity ⟩ 
-            (idC +₁ idC) ∘ α (alg f) ∎ } 
-          ; to = record { f = idC ; commutes = begin 
-            α (alg f) ∘ idC          ≈⟨ identityʳ ⟩ 
-            α (alg f)                ≈⟨ αf≈αg eq ⟩ 
-            α (alg g)                ≈˘⟨ elimˡ identity ⟩ 
-            (idC +₁ idC) ∘ α (alg g) ∎ } 
-          ; iso = record 
-            { isoˡ = identity² 
-            ; isoʳ = identity² 
-            } 
-          }
-          where open Functor (Y +-) using (identity)
-
-        identityʳ' : ∀ {X} {Y} {f} → extend f ∘ now X ≈ f
-        identityʳ' {X} {Y} {f} = begin 
-          extend f ∘ now X                                          ≈⟨ insertˡ (_≅_.isoˡ (out-≅ Y)) ⟩∘⟨refl ⟩ 
         (out⁻¹ Y ∘ out Y ∘ extend f) ∘ now X                      ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩
         (out⁻¹ Y ∘ [ out Y ∘ f , i₂ ∘ extend f ] ∘ out X) ∘ now X ≈⟨ pullʳ (pullʳ (unitlaw X)) ⟩
         out⁻¹ Y ∘ [ out Y ∘ f , i₂ ∘ extend f ] ∘ i₁              ≈⟨ refl⟩∘⟨ inject₁ ⟩
         out⁻¹ Y ∘ out Y ∘ f                                       ≈⟨ cancelˡ (_≅_.isoˡ (out-≅ Y)) ⟩
         f                                                         ∎
-
+      ; identityˡ = λ {X} → Terminal.⊤-id (algebras X) (record { f = extend (now X) ; commutes = begin 
-        identityˡ' : ∀ {X} → extend (now X) ≈ idC
+        out X ∘ extend (now X)                                                                                             ≈⟨ pullˡ ((F-Coalgebra-Morphism.commutes (Terminal.! (algebras X) {A = alg (now X)}))) ⟩ 
-        identityˡ' {X} = Terminal.⊤-id (coalgebras X) (record { f = extend (now X) ; commutes = begin 
+        ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ F-Coalgebra.α (alg (now X))) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩
-          out X ∘ extend (now X) ≈⟨ pullˡ ((commutes (! (coalgebras X) {A = alg (now X)}))) ⟩ 
+        (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) 
-          ((idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ α (alg (now X))) ∘ i₁   ≈⟨ pullʳ inject₁ ⟩
+        ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out X ∘ (now X)) , i₂ ∘ i₁ ] ∘ out X                                                       ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ (unitlaw X)) ○ inject₁) refl ⟩∘⟨refl ⟩
-          (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) 
+        (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out X           ≈⟨ pullˡ ∘[] ⟩
-          ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out X ∘ (now X)) , i₂ ∘ i₁ ] ∘ out X               ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw X) ○ inject₁) refl ⟩∘⟨refl ⟩
+        [ (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ i₁ 
-          (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩
+        , (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ i₂ ∘ i₁ ] ∘ out X                ≈⟨ ([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩
-          [ (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ i₁ 
+        [ i₁ ∘ idC , (i₂ ∘ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ i₁ ] ∘ out X            ≈⟨ ([]-cong₂ refl assoc) ⟩∘⟨refl ⟩
-          , (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ i₂ ∘ i₁ ] ∘ out X      ≈⟨ []-cong₂ +₁∘i₁ (pullˡ +₁∘i₂) ⟩∘⟨refl ⟩
-          [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras X) {A = alg (now X)}))) ∘ i₁ ] ∘ out X  ≈⟨ []-cong₂ refl assoc ⟩∘⟨refl ⟩
         [ i₁ ∘ idC , i₂ ∘ (extend (now X)) ] ∘ out X                                                                       ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
-          ([ i₁ , i₂ ] ∘ (idC +₁ extend (now X))) ∘ out X                            ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩
+        ([ i₁ , i₂ ] ∘ (idC +₁ extend (now X))) ∘ out X                                                                    ≈⟨ (elimˡ +-η) ⟩∘⟨refl ⟩
         (idC +₁ extend (now X)) ∘ out X                                                                                    ∎ })
-
+      ; assoc = {!   !}
-        assoc' : ∀ {X} {Y} {Z} {g} {h} → extend (extend h ∘ g) ≈ extend h ∘ extend g
+      ; sym-assoc = {!   !}
-        assoc' {X} {Y} {Z} {g} {h} = extend-unique (extend h ∘ g) (extend h ∘ extend g) (begin 
+      ; extend-≈ = λ {X} {Y} {f} {g} eq → begin 
-          out Z ∘ extend h ∘ extend g                                           ≈⟨ pullˡ (extendlaw h) ⟩
+          F-Coalgebra-Morphism.f (Terminal.! (algebras Y) {A = alg f }) ∘ i₁ {B = D₀ Y} ≈⟨ (Terminal.!-unique (algebras Y) (record { f = (F-Coalgebra-Morphism.f (Terminal.! (algebras Y) {A = alg g }) ∘ idC) ; commutes = begin 
-          ([ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y) ∘ extend g                    ≈⟨ pullʳ (extendlaw g) ⟩
+            F-Coalgebra.α (Terminal.⊤ (algebras Y)) ∘ F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ 
-          [ out Z ∘ h , i₂ ∘ extend h ] ∘ [ out Y ∘ g , i₂ ∘ extend g ] ∘ out X ≈⟨ pullˡ ∘[] ⟩
+            F-Coalgebra.α (Terminal.⊤ (algebras Y)) ∘ F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ≈⟨ F-Coalgebra-Morphism.commutes (Terminal.! (algebras Y)) ⟩ 
-          [ [ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y ∘ g 
+            Functor.F₁ (delayF Y) (F-Coalgebra-Morphism.f (Terminal.! (algebras Y))) ∘ F-Coalgebra.α (alg g) ≈˘⟨ (Functor.F-resp-≈ (delayF Y) identityʳ) ⟩∘⟨ (αf≈αg eq) ⟩ 
-          , [ out Z ∘ h , i₂ ∘ extend h ] ∘ i₂ ∘ extend g ] ∘ out X             ≈⟨ []-cong₂ (pullˡ (⟺ (extendlaw h))) (pullˡ inject₂) ⟩∘⟨refl ⟩
+            Functor.F₁ (delayF Y) (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ∘ idC) ∘ F-Coalgebra.α (alg f) ∎ })) ⟩∘⟨refl ⟩ 
-          [ (out Z ∘ extend h) ∘ g , (i₂ ∘ extend h) ∘ extend g ] ∘ out X       ≈⟨ ([]-cong₂ assoc assoc) ⟩∘⟨refl ⟩
+          (F-Coalgebra-Morphism.f (Terminal.! (algebras Y) {A = alg g }) ∘ idC) ∘ i₁ {B = D₀ Y} ≈⟨ identityʳ ⟩∘⟨refl ⟩
-          [ out Z ∘ extend h ∘ g , i₂ ∘ extend h ∘ extend g ] ∘ out X           ∎)
-        
-        extend-≈' : ∀ {X} {Y} {f g : X ⇒ D₀ Y} → f ≈ g → extend f ≈ extend g
-        extend-≈' {X} {Y} {f} {g} eq = begin
-          u (! (coalgebras Y) {A = alg f }) ∘ i₁ {B = D₀ Y}         ≈⟨ (!-unique (coalgebras Y) (record { f = (u (! (coalgebras Y) {A = alg g }) ∘ idC) ; commutes = begin 
-            α (⊤ (coalgebras Y)) ∘ u (! (coalgebras Y)) ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ 
-            α (⊤ (coalgebras Y)) ∘ u (! (coalgebras Y))       ≈⟨ commutes (! (coalgebras Y)) ⟩ 
-            (idC +₁ u (! (coalgebras Y))) ∘ α (alg g)       ≈˘⟨ Functor.F-resp-≈ (Y +-) identityʳ ⟩∘⟨ αf≈αg eq ⟩ 
-            (idC +₁ u (! (coalgebras Y)) ∘ idC) ∘ α (alg f) ∎ }))
-            ⟩∘⟨refl ⟩ 
-          (u (! (coalgebras Y) {A = alg g }) ∘ idC) ∘ i₁ {B = D₀ Y} ≈⟨ identityʳ ⟩∘⟨refl ⟩
           extend g ∎
+      })
+      where
+        alg' : ∀ {X Y} → F-Coalgebra (delayF Y)
+        alg' {X} {Y} = record { A = D₀ X ; α = i₂ }
+        module _ {X Y : Obj} (f : X ⇒ D₀ Y) where
+          open Terminal (algebras Y) using (!; ⊤-id)
+          alg : F-Coalgebra (delayF Y)
+          alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ] }  -- (idC +₁ (idC +₁ [ idC , idC ]) ∘ _≅_.to +-assoc ∘ _≅_.to +-comm)
+          extend : D₀ X ⇒ D₀ Y
+          extend = F-Coalgebra-Morphism.f (! {A = alg}) ∘ i₁ {B = D₀ Y}
+          !∘i₂ : F-Coalgebra-Morphism.f (! {A = alg}) ∘ i₂ ≈ idC
+          !∘i₂ = ⊤-id (F-Coalgebras (delayF Y) [ ! ∘ record { f = i₂ ; commutes = inject₂ } ] )
+          extendlaw : out Y ∘ extend ≈ [ out Y ∘ f , i₂ ∘ extend ] ∘ out X
+          extendlaw = begin 
+            out Y ∘ extend ≈⟨ pullˡ (F-Coalgebra-Morphism.commutes (! {A = alg})) ⟩ 
+            ((idC +₁ (F-Coalgebra-Morphism.f !)) ∘ F-Coalgebra.α alg) ∘ coproduct.i₁                   ≈⟨ pullʳ inject₁ ⟩
+            (idC +₁ (F-Coalgebra-Morphism.f !)) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩
+            [ (idC +₁ (F-Coalgebra-Morphism.f !)) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) 
+            , (idC +₁ (F-Coalgebra-Morphism.f !)) ∘ i₂ ∘ i₁ ] ∘ out X                                  ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩
+            [ [ (idC +₁ (F-Coalgebra-Morphism.f !)) ∘ i₁ 
+              , (idC +₁ (F-Coalgebra-Morphism.f !)) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f) 
+            , (i₂ ∘ (F-Coalgebra-Morphism.f !)) ∘ i₁ ] ∘ out X                                         ≈⟨ ([]-cong₂ (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) refl) ⟩∘⟨refl ⟩
+            [ [ i₁ ∘ idC , (i₂ ∘ (F-Coalgebra-Morphism.f !)) ∘ i₂ ] ∘ (out Y ∘ f) 
+            , (i₂ ∘ (F-Coalgebra-Morphism.f !)) ∘ i₁ ] ∘ out X                                         ≈⟨ ([]-cong₂ (elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η)) assoc) ⟩∘⟨refl ⟩
+            [ out Y ∘ f , i₂ ∘ extend ] ∘ out X ∎ 
+        αf≈αg : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → F-Coalgebra.α (alg f) ≈ F-Coalgebra.α (alg g)
+        αf≈αg {X} {Y} {f} {g} eq = []-cong₂ ([]-cong₂ (refl⟩∘⟨ refl⟩∘⟨ eq) refl ⟩∘⟨refl) refl
+        alg-f≈alg-g : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → M._≅_ (F-Coalgebras (delayF Y)) (alg f) (alg g)
+        alg-f≈alg-g {X} {Y} {f} {g} eq = record 
+          { from = record { f = idC ; commutes = begin 
+            F-Coalgebra.α (alg g) ∘ idC ≈⟨ identityʳ ⟩ 
+            F-Coalgebra.α (alg g) ≈⟨ ⟺ (αf≈αg eq) ⟩ 
+            F-Coalgebra.α (alg f) ≈˘⟨ elimˡ (Functor.identity (delayF Y)) ⟩ 
+            Functor.F₁ (delayF Y) idC ∘ F-Coalgebra.α (alg f) ∎ } 
+          ; to = record { f = idC ; commutes = begin 
+            F-Coalgebra.α (alg f) ∘ idC ≈⟨ identityʳ ⟩ 
+            F-Coalgebra.α (alg f) ≈⟨ αf≈αg eq ⟩ 
+            F-Coalgebra.α (alg g) ≈˘⟨ elimˡ (Functor.identity (delayF Y)) ⟩ 
+            Functor.F₁ (delayF Y) idC ∘ F-Coalgebra.α (alg g) ∎ } 
+          ; iso = record 
+            { isoˡ = identity² 
+            ; isoʳ = identity² 
+            } 
+          }
+```
+
+### Old definitions:
+
+```agda
+  record DelayMonad : Set (o ⊔ ℓ ⊔ e) where
+    field
+      D₀ : Obj → Obj
+
+    field
+      now : ∀ {X} → X ⇒ D₀ X
+      later : ∀ {X} → D₀ X ⇒ D₀ X
+      isIso : ∀ {X} → IsIso ([ now {X} , later {X} ])
+
+    out : ∀ {X} → D₀ X ⇒ X + D₀ X
+    out {X} = IsIso.inv (isIso {X})
+
+    field
+      coit : ∀ {X Y} → Y ⇒ X + Y → Y ⇒ D₀ X
+      coit-law : ∀ {X Y} {f : Y ⇒ X + Y} → out ∘ (coit f) ≈ (idC +₁ (coit f)) ∘ f
+
+    field
+      _* : ∀ {X Y} → X ⇒ D₀ Y → D₀ X ⇒ D₀ Y
+      *-law : ∀ {X Y} {f : X ⇒ D₀ Y} → out ∘ (f *) ≈ [ out ∘ f , i₂ ∘ (f *) ] ∘ out
+      *-unique : ∀ {X Y} (f : X ⇒ D₀ Y) (h : D₀ X ⇒ D₀ Y) → h ≈ f *
+      *-resp-≈ : ∀ {X Y} {f h : X ⇒ D₀ Y} → f ≈ h → f * ≈ h * 
+
+    unitLaw : ∀ {X} → out {X} ∘ now {X} ≈ i₁
+    unitLaw = begin 
+      out ∘ now                  ≈⟨ refl⟩∘⟨ sym inject₁ ⟩ 
+      out ∘ [ now , later ] ∘ i₁ ≈⟨ cancelˡ (IsIso.isoˡ isIso) ⟩
+      i₁ ∎
+
+    toMonad : KleisliTriple C
+    toMonad = record
+      { F₀ = D₀
+      ; unit = now
+      ; extend = _*
+      ; identityʳ = λ {X} {Y} {k} → begin 
+        k * ∘ now                                                ≈⟨ introˡ (IsIso.isoʳ isIso) ⟩∘⟨refl ⟩ 
+        (([ now , later ] ∘ out) ∘ k *) ∘ now                    ≈⟨ pullʳ *-law ⟩∘⟨refl ⟩
+        ([ now , later ] ∘ [ out ∘ k , i₂ ∘ (k *) ] ∘ out) ∘ now ≈⟨ pullʳ (pullʳ unitLaw) ⟩
+        [ now , later ] ∘ [ out ∘ k , i₂ ∘ (k *) ] ∘ i₁          ≈⟨ refl⟩∘⟨ inject₁ ⟩
+        [ now , later ] ∘ out ∘ k                                ≈⟨ cancelˡ (IsIso.isoʳ isIso) ⟩
+        k ∎
+      ; identityˡ = λ {X} → sym (*-unique now idC)
+      ; assoc = λ {X} {Y} {Z} {f} {g} → sym (*-unique ((g *) ∘ f) ((g *) ∘ (f *)))
+      ; sym-assoc = λ {X} {Y} {Z} {f} {g} → *-unique ((g *) ∘ f) ((g *) ∘ (f *))
+      ; extend-≈ = *-resp-≈
+      }
 ```
 
 ### Definition 30: Search-Algebras
 
 TODO
 
-### Proposition 31 : the category of uniform-iteration coalgebras coincides with the category of search-coalgebras
+### Proposition 31 : the category of uniform-iteration algebras coincides with the category of search-algebras
 
 TODO