use coproduct functor from library, minor changes

.gitignore

@@ -1,4 +1,5 @@
 *.agdai
 *.pdf
 *.log
-Everything.agda
+Everything.agda
+public/

Makefile

@@ -20,7 +20,10 @@ open:
 
 push: all
 	mv public/Everything.html public/index.html
-	scp -r public hy84coky@cip2a7.cip.cs.fau.de:.www/public
+	chmod +w public/Agda.css
+	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,6 +1,5 @@
 <!--
 ```agda
-{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Categories.Category
 open import Categories.Monad
@@ -10,10 +9,12 @@ 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
+open import Categories.Category.Cartesian.Bundle
 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
@@ -29,50 +30,59 @@ 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
-      algebras : ∀ (A : Obj) → Terminal (F-Coalgebras (delayF A))
-    
-    module D A = Functor (delayF A)
+      coalgebras : ∀ (A : Obj) → Terminal (F-Coalgebras (A +-))
+```
+
+These are all the fields this record needs! 
+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 (algebras X) using (⊤; !)
+      open Terminal (coalgebras X) using (⊤; !; !-unique)
       open F-Coalgebra ⊤ renaming (A to DX)
 
       D₀ = DX
 
       out-≅ : DX ≅ X + DX
-      out-≅ = colambek {F = delayF X} (algebras X)
+      out-≅ = colambek {F = X +- } (coalgebras X)
 
       -- note: out-≅.from ≡ ⊤.α
       open _≅_ out-≅ using () renaming (to to out⁻¹; from to out) public
@@ -83,150 +93,204 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
       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 = F-Coalgebra-Morphism.f (! {A = record { A = Y ; α = f }})
+        coit f = u (! {A = record { A = Y ; α = f }})
 
         coit-commutes : ∀ (f : Y ⇒ X + Y) → out ∘ (coit f) ≈ (idC +₁ coit f) ∘ f
-        coit-commutes f = F-Coalgebra-Morphism.commutes (! {A = record { A = Y ; α = f }})
+        coit-commutes f = 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ʳ = λ {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 
-        out X ∘ extend (now X)                                                                                             ≈⟨ pullˡ ((F-Coalgebra-Morphism.commutes (Terminal.! (algebras X) {A = alg (now X)}))) ⟩ 
-        ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ F-Coalgebra.α (alg (now X))) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩
-        (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) 
-        ∘ [ [ 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₁ , i₂ ∘ i₁ ] ∘ out X           ≈⟨ pullˡ ∘[] ⟩
-        [ (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ i₁ 
-        , (idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras X) {A = alg (now X)}))) ∘ i₂ ∘ i₁ ] ∘ out X                ≈⟨ ([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩
-        [ i₁ ∘ idC , (i₂ ∘ (F-Coalgebra-Morphism.f (Terminal.! (algebras 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 ⟩
-        (idC +₁ extend (now X)) ∘ out X                                                                                    ∎ })
-      ; assoc = {!   !}
-      ; sym-assoc = {!   !}
-      ; extend-≈ = λ {X} {Y} {f} {g} eq → begin 
-          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 
-            F-Coalgebra.α (Terminal.⊤ (algebras Y)) ∘ F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ 
-            F-Coalgebra.α (Terminal.⊤ (algebras Y)) ∘ F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ≈⟨ F-Coalgebra-Morphism.commutes (Terminal.! (algebras Y)) ⟩ 
-            Functor.F₁ (delayF Y) (F-Coalgebra-Morphism.f (Terminal.! (algebras Y))) ∘ F-Coalgebra.α (alg g) ≈˘⟨ (Functor.F-resp-≈ (delayF Y) identityʳ) ⟩∘⟨ (αf≈αg eq) ⟩ 
-            Functor.F₁ (delayF Y) (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ∘ idC) ∘ F-Coalgebra.α (alg f) ∎ })) ⟩∘⟨refl ⟩ 
-          (F-Coalgebra-Morphism.f (Terminal.! (algebras Y) {A = alg g }) ∘ idC) ∘ i₁ {B = D₀ Y} ≈⟨ identityʳ ⟩∘⟨refl ⟩
-          extend g ∎
+      ; identityʳ = identityʳ'
+      ; identityˡ = identityˡ'
+      ; assoc = assoc'
+      ; sym-assoc = sym assoc'
+      ; extend-≈ = extend-≈'
       })
       where
-        alg' : ∀ {X Y} → F-Coalgebra (delayF Y)
-        alg' {X} {Y} = record { A = D₀ X ; α = i₂ }
+        open Terminal
         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)
+          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 = 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₂ } ] )
+          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ˡ (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)
+            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 (delayF Y)) (alg f) (alg g)
+
+        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 
-            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) ∎ } 
+            α (alg g) ∘ idC          ≈⟨ identityʳ ⟩ 
+            α (alg g)                ≈⟨ ⟺ (αf≈αg eq) ⟩ 
+            α (alg f)                ≈˘⟨ elimˡ identity ⟩ 
+            (idC +₁ idC) ∘ α (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) ∎ } 
+            α (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)
 
-### Old definitions:
+        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                                                         ∎
 
-```agda
-  record DelayMonad : Set (o ⊔ ℓ ⊔ e) where
-    field
-      D₀ : Obj → Obj
+        identityˡ' : ∀ {X} → extend (now X) ≈ idC
+        identityˡ' {X} = Terminal.⊤-id (coalgebras X) (record { f = extend (now X) ; commutes = begin 
+          out X ∘ extend (now X) ≈⟨ pullˡ ((commutes (! (coalgebras X) {A = alg (now X)}))) ⟩ 
+          ((idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ α (alg (now X))) ∘ i₁   ≈⟨ pullʳ inject₁ ⟩
+          (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) 
+          ∘ [ [ 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)}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩
+          [ (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ i₁ 
+          , (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 ⟩
+          (idC +₁ extend (now X)) ∘ out X                                            ∎ })
 
-    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-≈
-      }
+        assoc' : ∀ {X} {Y} {Z} {g} {h} → extend (extend h ∘ g) ≈ extend h ∘ extend g
+        assoc' {X} {Y} {Z} {g} {h} = extend-unique (extend h ∘ g) (extend h ∘ extend g) (begin 
+          out Z ∘ extend h ∘ extend g                                           ≈⟨ pullˡ (extendlaw h) ⟩
+          ([ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y) ∘ extend g                    ≈⟨ pullʳ (extendlaw g) ⟩
+          [ out Z ∘ h , i₂ ∘ extend h ] ∘ [ out Y ∘ g , i₂ ∘ extend g ] ∘ out X ≈⟨ pullˡ ∘[] ⟩
+          [ [ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y ∘ g 
+          , [ out Z ∘ h , i₂ ∘ extend h ] ∘ i₂ ∘ extend g ] ∘ out X             ≈⟨ []-cong₂ (pullˡ (⟺ (extendlaw h))) (pullˡ inject₂) ⟩∘⟨refl ⟩
+          [ (out Z ∘ extend h) ∘ g , (i₂ ∘ extend h) ∘ extend g ] ∘ out X       ≈⟨ ([]-cong₂ assoc assoc) ⟩∘⟨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                                                ∎
 ```
 
 ### Definition 30: Search-Algebras
 
 TODO
 
-### Proposition 31 : the category of uniform-iteration algebras coincides with the category of search-algebras
+### Proposition 31 : the category of uniform-iteration coalgebras coincides with the category of search-coalgebras
 
 TODO