From 86c5be9e2f37f08638bb8f1c2bcce86d77aae63b Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Fri, 8 Sep 2023 13:09:30 +0200 Subject: [PATCH] prepare for meeting, some progress on delay --- public/ElgotAlgebra.html | 17 +- public/ElgotAlgebras.html | 17 +- public/Monad.ElgotMonad.html | 25 ++- public/Monad.Instance.Delay.html | 307 ++++++++++++++++++--------- public/Monad.Instance.Delay.md | 291 ++++++++++++++++--------- public/MonadK.html | 36 ++-- public/UniformIterationAlgebra.html | 9 +- public/UniformIterationAlgebras.html | 9 +- src/Coalgebra.lagda.md | 25 +++ src/Monad/Instance/Delay.lagda.md | 199 ++++++++--------- 10 files changed, 570 insertions(+), 365 deletions(-) create mode 100644 src/Coalgebra.lagda.md diff --git a/public/ElgotAlgebra.html b/public/ElgotAlgebra.html index 80f4eee..acf1ccb 100644 --- a/public/ElgotAlgebra.html +++ b/public/ElgotAlgebra.html @@ -11,8 +11,11 @@ div.columns{display: flex; gap: min(4vw, 1.5em);} div.column{flex: auto; overflow-x: auto;} div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;} - ul.task-list{list-style: none;} + /* The extra [class] is a hack that increases specificity enough to + override a similar rule in reveal.js */ + ul.task-list[class]{list-style: none;} ul.task-list li input[type="checkbox"] { + font-size: inherit; width: 0.8em; margin: 0 0.8em 0.2em -1.6em; vertical-align: middle; @@ -40,13 +43,13 @@

Summary

This file introduces (guarded) elgot algebras

Code

module ElgotAlgebra where
diff --git a/public/ElgotAlgebras.html b/public/ElgotAlgebras.html
index ad65c42..e602a6c 100644
--- a/public/ElgotAlgebras.html
+++ b/public/ElgotAlgebras.html
@@ -11,8 +11,11 @@
     div.columns{display: flex; gap: min(4vw, 1.5em);}
     div.column{flex: auto; overflow-x: auto;}
     div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
-    ul.task-list{list-style: none;}
+    /* The extra [class] is a hack that increases specificity enough to
+       override a similar rule in reveal.js */
+    ul.task-list[class]{list-style: none;}
     ul.task-list li input[type="checkbox"] {
+      font-size: inherit;
       width: 0.8em;
       margin: 0 0.8em 0.2em -1.6em;
       vertical-align: middle;
@@ -48,12 +51,12 @@
 
This file introduces the category of unguarded elgot
 algebras

 
 
Code

 
module ElgotAlgebras where
diff --git a/public/Monad.ElgotMonad.html b/public/Monad.ElgotMonad.html
index 4df0531..628c103 100644
--- a/public/Monad.ElgotMonad.html
+++ b/public/Monad.ElgotMonad.html
@@ -11,8 +11,11 @@
     div.columns{display: flex; gap: min(4vw, 1.5em);}
     div.column{flex: auto; overflow-x: auto;}
     div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
-    ul.task-list{list-style: none;}
+    /* The extra [class] is a hack that increases specificity enough to
+       override a similar rule in reveal.js */
+    ul.task-list[class]{list-style: none;}
     ul.task-list li input[type="checkbox"] {
+      font-size: inherit;
       width: 0.8em;
       margin: 0 0.8em 0.2em -1.6em;
       vertical-align: middle;
@@ -44,16 +47,16 @@
 
Summary

 
This file introduces Elgot Monads.

 
    
-
  • Definition
-13 Pre-Elgot Monads
    • 
-
  • Definition 13 strong
-pre-Elgot
    • 
-
  • Definition
-14 Elgot Monads
    • 
-
  • Definition 14 strong
-Elgot
    • 
-
  • Proposition 15
-(Strong) Elgot monads are (strong) pre-Elgot
    • 
+
    • 
+
    • 
+
    • 
+
    • 
+
    • 
 

 
Code

 
module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
diff --git a/public/Monad.Instance.Delay.html b/public/Monad.Instance.Delay.html
index 21d3ca7..3765c49 100644
--- a/public/Monad.Instance.Delay.html
+++ b/public/Monad.Instance.Delay.html
@@ -11,8 +11,11 @@
     div.columns{display: flex; gap: min(4vw, 1.5em);}
     div.column{flex: auto; overflow-x: auto;}
     div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
-    ul.task-list{list-style: none;}
+    /* The extra [class] is a hack that increases specificity enough to
+       override a similar rule in reveal.js */
+    ul.task-list[class]{list-style: none;}
     ul.task-list li input[type="checkbox"] {
+      font-size: inherit;
       width: 0.8em;
       margin: 0 0.8em 0.2em -1.6em;
       vertical-align: middle;
@@ -26,136 +29,230 @@
 
 
 
 
Summary

 
This file introduces the delay monad D

 
    
-
  • Proposition
-1 Characterization of the delay monad D
-(here treated as definition)
    • 
-
  • Proposition 2
-D is commutative
    • 
+
    • 
+
    • 
 

 
Code

-
module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
-  open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
-  open Cocartesian (Extensive.cocartesian extensive)
-  open Cartesian (ExtensiveDistributiveCategory.cartesian ED)
-  open BinaryProducts products
+
module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
+  open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
+  open Cocartesian (Extensive.cocartesian extensive)
+  open Cartesian (ExtensiveDistributiveCategory.cartesian ED)
+  open BinaryProducts products
 
-  open M C
-  open MR C
-  open Equiv
-  open HomReasoning
-  open CoLambek
+  open M C
+  open MR C
+  open Equiv
+  open HomReasoning
+  open CoLambek
 

 
Proposition
 1: Characterization of the delay monad
 D

-
First I postulate the Functor D, maybe I should derive it…
-TODO: - how to define using final coalgebra(s)? - DX
-can be defined as retract of infinite streams, how? - how to express
-Theorem 8 in agda?

-
  record DelayFunctor : Set (o ⊔ ℓ ⊔ e) where
-    field
-      D : Endofunctor C
+
  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
+    }
 
-    open Functor D public renaming (F₀ to D₀; F₁ to D₁)
+  record DelayM : Set (o ⊔ ℓ ⊔ e) where
+    field
+      algebras : ∀ (A : Obj) → Terminal (F-Coalgebras (delayF A))
+    
+    module D A = Functor (delayF A)
 
-    field
-      now : ∀ {X} → X ⇒ D₀ X
-      later : ∀ {X} → D₀ X ⇒ D₀ X
-      isIso : ∀ {X} → IsIso [ now {X} , later {X} ]
+    module _ (X : Obj) where
+      open Terminal (algebras X) using (⊤; !)
+      open F-Coalgebra ⊤ renaming (A to DX)
 
-    out : ∀ {X} → D₀ X ⇒ X + D₀ X
-    out {X} = IsIso.inv (isIso {X})
+      D₀ = DX
 
-    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
+      out-≅ : DX ≅ X + DX
+      out-≅ = colambek {F = delayF X} (algebras X)
+
+      -- note: out-≅.from ≡ ⊤.α
+      open _≅_ out-≅ using () renaming (to to out⁻¹; from to out) public
+
+      now : X ⇒ DX
+      now = out⁻¹ ∘ i₁
+
+      later : DX ⇒ DX
+      later = out⁻¹ ∘ i₂
+
+      -- TODO inline
+      unitlaw : out ∘ now ≈ i₁
+      unitlaw = cancelˡ (_≅_.isoʳ out-≅)
+
+      module _ {Y : Obj} where 
+        coit : Y ⇒ X + Y → Y ⇒ DX
+        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 = F-Coalgebra-Morphism.commutes (! {A = record { A = Y ; α = f }})
+
+    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 
+        --   extend f ≈⟨ sym (Terminal.!-unique (algebras Y) (record { f = extend f ; commutes = F-Coalgebra-Morphism.commutes {!   !} })) ⟩ 
+        --   F-Coalgebra-Morphism.f ((Terminal.! (algebras Y) {A = alg' {X} {Y}})) ≈˘⟨ sym (Terminal.!-unique (algebras Y) (record { f = extend g ; commutes = {!   !} })) ⟩
+        --   extend g ∎
+      
+        -- let 
+        --   h : F-Coalgebra-Morphism (alg f) (alg g)
+        --   h = record { f = idC ; commutes = begin 
+        --     F-Coalgebra.α (alg g) ∘ idC ≈⟨ id-comm ⟩ 
+        --     idC ∘ F-Coalgebra.α (alg g) ≈⟨ refl⟩∘⟨ []-cong₂ (([]-cong₂ (refl⟩∘⟨ (refl⟩∘⟨ (sym eq))) refl) ⟩∘⟨refl) refl ⟩ 
+        --     idC ∘ F-Coalgebra.α (alg f) ≈˘⟨ ([]-cong₂ identityʳ identityʳ ○ +-η) ⟩∘⟨refl ⟩
+        --     (idC +₁ idC) ∘ F-Coalgebra.α (alg f) ∎ }
+        --   x : F-Coalgebra-Morphism (alg f) (Terminal.⊤ (algebras Y))
+        --   x = (F-Coalgebras (delayF Y)) [ Terminal.! (algebras Y) ∘ h ]
+        -- in Terminal.!-unique₂ (algebras Y) {f = Terminal.! (algebras Y)} {g = {!   !} } ⟩∘⟨refl
+        
+        -- extend f ≈⟨ insertˡ (_≅_.isoˡ (out-≅ Y)) ⟩ 
+        -- out⁻¹ Y ∘ out Y ∘ extend f ≈⟨ refl⟩∘⟨ pullˡ (F-Coalgebra-Morphism.commutes (Terminal.! (algebras Y) {A = alg f})) ⟩
+        -- out⁻¹ Y ∘ ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))) ∘ [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ]) ∘ i₁ ≈⟨ refl⟩∘⟨ ((+₁-cong₂ refl (Terminal.!-unique₂ (algebras Y) {f = Terminal.! (algebras Y) {A = alg f}} {g = Terminal.! (algebras Y) {A = alg f}}) ⟩∘⟨ ([]-cong₂ (([]-cong₂ (refl⟩∘⟨ (refl⟩∘⟨ eq)) refl) ⟩∘⟨refl) refl)) ⟩∘⟨refl) ⟩
+        -- out⁻¹ Y ∘ ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))) ∘ [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ g) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ]) ∘ i₁ ≈⟨ refl⟩∘⟨ (((+₁-cong₂ refl (Terminal.!-unique₂ (algebras Y) {f = Terminal.! (algebras Y)} {g = record { f = F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ; commutes = {!   !} }})) ⟩∘⟨refl) ⟩∘⟨refl) ⟩
+        -- out⁻¹ Y ∘ ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))) ∘ [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ g) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ]) ∘ i₁ ≈˘⟨ refl⟩∘⟨ pullˡ (F-Coalgebra-Morphism.commutes (Terminal.! (algebras Y) {A = alg g})) ⟩
+        -- out⁻¹ Y ∘ out Y ∘ extend g ≈˘⟨ insertˡ (_≅_.isoˡ (out-≅ Y)) ⟩
+        -- 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 ∎ 
 

-
Now let’s define the monad:

-
  record DelayMonad : Set (o ⊔ ℓ ⊔ e) where
-    field
-      D : DelayFunctor
-    open DelayFunctor D
+
Old definitions:

+
  record DelayMonad : Set (o ⊔ ℓ ⊔ e) where
+    field
+      D₀ : Obj → Obj
 
-    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 * 
+    field
+      now : ∀ {X} → X ⇒ D₀ X
+      later : ∀ {X} → D₀ X ⇒ D₀ X
+      isIso : ∀ {X} → IsIso ([ now {X} , later {X} ])
 
-    unitLaw : ∀ {X} → out {X} ∘ now {X} ≈ i₁
-    unitLaw = begin 
-      out ∘ now ≈⟨ refl⟩∘⟨ sym inject₁ ⟩ 
-      out ∘ [ now , later ] ∘ i₁ ≈⟨ cancelˡ (IsIso.isoˡ isIso) ⟩
-      i₁ ∎
+    out : ∀ {X} → D₀ X ⇒ X + D₀ X
+    out {X} = IsIso.inv (isIso {X})
 
-    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-≈
-      }
+    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

-
  record SearchAlgebra (DF : DelayFunctor) : Set (o ⊔ ℓ ⊔ e) where
-    open DelayFunctor DF
-    
-    field
-      FA : F-Algebra D
-
-    open F-Algebra FA
-
-    field
-      now-id : α ∘ now ≈ idC    
-      later-same : α ∘ later ≈ α
-

+
TODO

 
Proposition
 31 : the category of uniform-iteration algebras coincides with the
 category of search-algebras

-
TODOs:

-
    
-
  • Define SearchAlgebras (and
-SearchAlgebra morphisms)
    • 
-
  • show StrongEquivalence
    • 
-
  • Show
-‘ElgotAlgebra⇔Search+D’
    • 
-

-
  record SearchAlgebras (DF : DelayFunctor) : Set (o ⊔ ℓ ⊔ e) where
-    open DelayFunctor DF
-

+
TODO

 
 
diff --git a/public/Monad.Instance.Delay.md b/public/Monad.Instance.Delay.md
index e9bbe41..3f287e1 100644
--- a/public/Monad.Instance.Delay.md
+++ b/public/Monad.Instance.Delay.md
@@ -1,127 +1,222 @@
 
 
 ## Summary
 This file introduces the delay monad ***D***
 
-- [X] *Proposition 1* Characterization of the delay monad ***D*** (here treated as definition)
+- [ ] *Proposition 1* Characterization of the delay monad ***D***
 - [ ] *Proposition 2* ***D*** is commutative
 
 ## Code
 
-
module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
-  open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
-  open Cocartesian (Extensive.cocartesian extensive)
-  open Cartesian (ExtensiveDistributiveCategory.cartesian ED)
-  open BinaryProducts products
+
module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
+  open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
+  open Cocartesian (Extensive.cocartesian extensive)
+  open Cartesian (ExtensiveDistributiveCategory.cartesian ED)
+  open BinaryProducts products
 
-  open M C
-  open MR C
-  open Equiv
-  open HomReasoning
-  open CoLambek
+  open M C
+  open MR C
+  open Equiv
+  open HomReasoning
+  open CoLambek
 
### *Proposition 1*: Characterization of the delay monad ***D***
 
-First I postulate the Functor *D*, maybe I should derive it...
-**TODO**: 
-- how to define using final coalgebra(s)?
-- DX can be defined as retract of infinite streams, how?
-- how to express **Theorem 8** in 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 DelayFunctor : Set (o ⊔ ℓ ⊔ e) where
-    field
-      D : Endofunctor C
+  record DelayM : Set (o ⊔ ℓ ⊔ e) where
+    field
+      algebras : ∀ (A : Obj) → Terminal (F-Coalgebras (delayF A))
+    
+    module D A = Functor (delayF A)
 
-    open Functor D public renaming (F₀ to D₀; F₁ to D₁)
+    module _ (X : Obj) where
+      open Terminal (algebras X) using (⊤; !)
+      open F-Coalgebra ⊤ renaming (A to DX)
 
-    field
-      now : ∀ {X} → X ⇒ D₀ X
-      later : ∀ {X} → D₀ X ⇒ D₀ X
-      isIso : ∀ {X} → IsIso [ now {X} , later {X} ]
+      D₀ = DX
 
-    out : ∀ {X} → D₀ X ⇒ X + D₀ X
-    out {X} = IsIso.inv (isIso {X})
+      out-≅ : DX ≅ X + DX
+      out-≅ = colambek {F = delayF X} (algebras 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
+      -- note: out-≅.from ≡ ⊤.α
+      open _≅_ out-≅ using () renaming (to to out⁻¹; from to out) public
+
+      now : X ⇒ DX
+      now = out⁻¹ ∘ i₁
+
+      later : DX ⇒ DX
+      later = out⁻¹ ∘ i₂
+
+      -- TODO inline
+      unitlaw : out ∘ now ≈ i₁
+      unitlaw = cancelˡ (_≅_.isoʳ out-≅)
+
+      module _ {Y : Obj} where 
+        coit : Y ⇒ X + Y → Y ⇒ DX
+        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 = F-Coalgebra-Morphism.commutes (! {A = record { A = Y ; α = f }})
+
+    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 
+        --   extend f ≈⟨ sym (Terminal.!-unique (algebras Y) (record { f = extend f ; commutes = F-Coalgebra-Morphism.commutes {!   !} })) ⟩ 
+        --   F-Coalgebra-Morphism.f ((Terminal.! (algebras Y) {A = alg' {X} {Y}})) ≈˘⟨ sym (Terminal.!-unique (algebras Y) (record { f = extend g ; commutes = {!   !} })) ⟩
+        --   extend g ∎
+      
+        -- let 
+        --   h : F-Coalgebra-Morphism (alg f) (alg g)
+        --   h = record { f = idC ; commutes = begin 
+        --     F-Coalgebra.α (alg g) ∘ idC ≈⟨ id-comm ⟩ 
+        --     idC ∘ F-Coalgebra.α (alg g) ≈⟨ refl⟩∘⟨ []-cong₂ (([]-cong₂ (refl⟩∘⟨ (refl⟩∘⟨ (sym eq))) refl) ⟩∘⟨refl) refl ⟩ 
+        --     idC ∘ F-Coalgebra.α (alg f) ≈˘⟨ ([]-cong₂ identityʳ identityʳ ○ +-η) ⟩∘⟨refl ⟩
+        --     (idC +₁ idC) ∘ F-Coalgebra.α (alg f) ∎ }
+        --   x : F-Coalgebra-Morphism (alg f) (Terminal.⊤ (algebras Y))
+        --   x = (F-Coalgebras (delayF Y)) [ Terminal.! (algebras Y) ∘ h ]
+        -- in Terminal.!-unique₂ (algebras Y) {f = Terminal.! (algebras Y)} {g = {!   !} } ⟩∘⟨refl
+        
+        -- extend f ≈⟨ insertˡ (_≅_.isoˡ (out-≅ Y)) ⟩ 
+        -- out⁻¹ Y ∘ out Y ∘ extend f ≈⟨ refl⟩∘⟨ pullˡ (F-Coalgebra-Morphism.commutes (Terminal.! (algebras Y) {A = alg f})) ⟩
+        -- out⁻¹ Y ∘ ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))) ∘ [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ]) ∘ i₁ ≈⟨ refl⟩∘⟨ ((+₁-cong₂ refl (Terminal.!-unique₂ (algebras Y) {f = Terminal.! (algebras Y) {A = alg f}} {g = Terminal.! (algebras Y) {A = alg f}}) ⟩∘⟨ ([]-cong₂ (([]-cong₂ (refl⟩∘⟨ (refl⟩∘⟨ eq)) refl) ⟩∘⟨refl) refl)) ⟩∘⟨refl) ⟩
+        -- out⁻¹ Y ∘ ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))) ∘ [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ g) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ]) ∘ i₁ ≈⟨ refl⟩∘⟨ (((+₁-cong₂ refl (Terminal.!-unique₂ (algebras Y) {f = Terminal.! (algebras Y)} {g = record { f = F-Coalgebra-Morphism.f (Terminal.! (algebras Y)) ; commutes = {!   !} }})) ⟩∘⟨refl) ⟩∘⟨refl) ⟩
+        -- out⁻¹ Y ∘ ((idC +₁ (F-Coalgebra-Morphism.f (Terminal.! (algebras Y)))) ∘ [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ g) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ]) ∘ i₁ ≈˘⟨ refl⟩∘⟨ pullˡ (F-Coalgebra-Morphism.commutes (Terminal.! (algebras Y) {A = alg g})) ⟩
+        -- out⁻¹ Y ∘ out Y ∘ extend g ≈˘⟨ insertˡ (_≅_.isoˡ (out-≅ Y)) ⟩
+        -- 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 ∎ 
 

-Now let's define the monad:
+### Old definitions:
 
-
  record DelayMonad : Set (o ⊔ ℓ ⊔ e) where
-    field
-      D : DelayFunctor
-    open DelayFunctor D
+
  record DelayMonad : Set (o ⊔ ℓ ⊔ e) where
+    field
+      D₀ : Obj → Obj
 
-    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 * 
+    field
+      now : ∀ {X} → X ⇒ D₀ X
+      later : ∀ {X} → D₀ X ⇒ D₀ X
+      isIso : ∀ {X} → IsIso ([ now {X} , later {X} ])
 
-    unitLaw : ∀ {X} → out {X} ∘ now {X} ≈ i₁
-    unitLaw = begin 
-      out ∘ now ≈⟨ refl⟩∘⟨ sym inject₁ ⟩ 
-      out ∘ [ now , later ] ∘ i₁ ≈⟨ cancelˡ (IsIso.isoˡ isIso) ⟩
-      i₁ ∎
+    out : ∀ {X} → D₀ X ⇒ X + D₀ X
+    out {X} = IsIso.inv (isIso {X})
 
-    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-≈
-      }
+    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
 
-
  record SearchAlgebra (DF : DelayFunctor) : Set (o ⊔ ℓ ⊔ e) where
-    open DelayFunctor DF
-    
-    field
-      FA : F-Algebra D
+TODO
 
-    open F-Algebra FA
-
-    field
-      now-id : α ∘ now ≈ idC    
-      later-same : α ∘ later ≈ α
-

 ### Proposition 31 : the category of uniform-iteration algebras coincides with the category of search-algebras
-TODOs:
 
-- [ ] Define SearchAlgebras (and SearchAlgebra morphisms)
-- [ ] show StrongEquivalence
-- [ ] Show 'ElgotAlgebra⇔Search+***D***'
-
-
-
  record SearchAlgebras (DF : DelayFunctor) : Set (o ⊔ ℓ ⊔ e) where
-    open DelayFunctor DF
-

\ No newline at end of file
+TODO
diff --git a/public/MonadK.html b/public/MonadK.html
index 77e4533..4037deb 100644
--- a/public/MonadK.html
+++ b/public/MonadK.html
@@ -11,8 +11,11 @@
     div.columns{display: flex; gap: min(4vw, 1.5em);}
     div.column{flex: auto; overflow-x: auto;}
     div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
-    ul.task-list{list-style: none;}
+    /* The extra [class] is a hack that increases specificity enough to
+       override a similar rule in reveal.js */
+    ul.task-list[class]{list-style: none;}
     ul.task-list li input[type="checkbox"] {
+      font-size: inherit;
       width: 0.8em;
       margin: 0 0.8em 0.2em -1.6em;
       vertical-align: middle;
@@ -47,24 +50,25 @@
 
In this file I explore the monad K and its
 properties:

 
    
-
  • Lemma 16
-Definition of the monad
    • 
-
  • Lemma 16
+
    • 
+
    • 
-
  • Proposition 19
-K is strong
    • 
-
  • Theorem 22
-K is an equational lifting monad
    • 
-
  • Proposition 23 The
-Kleisli category of K is enriched over pointed
-partial orders and strict monotone maps
    • 
-
  • Proposition 25
-K is copyable and weakly discardable
    • 
-
  • Theorem 29
+monadicity theorem)
    • 
+
    • 
+
    • 
+
    • 
+
    • 
+
    • 
+strong pre-Elgot monad
 

 
Code

 
module MonadK {o ℓ e} (D : ExtensiveDistributiveCategory o ℓ e) where
diff --git a/public/UniformIterationAlgebra.html b/public/UniformIterationAlgebra.html
index 304387d..76bb2ea 100644
--- a/public/UniformIterationAlgebra.html
+++ b/public/UniformIterationAlgebra.html
@@ -11,8 +11,11 @@
     div.columns{display: flex; gap: min(4vw, 1.5em);}
     div.column{flex: auto; overflow-x: auto;}
     div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
-    ul.task-list{list-style: none;}
+    /* The extra [class] is a hack that increases specificity enough to
+       override a similar rule in reveal.js */
+    ul.task-list[class]{list-style: none;}
     ul.task-list li input[type="checkbox"] {
+      font-size: inherit;
       width: 0.8em;
       margin: 0 0.8em 0.2em -1.6em;
       vertical-align: middle;
@@ -35,8 +38,8 @@
 
Summary

 
This file introduces Uniform-Iteration Algebras

 
    
-
  • Definition
-12 Uniform-Iteration Algebras
    • 
+
    • 
 

 
Code

 
module UniformIterationAlgebra {o ℓ e} (D : ExtensiveDistributiveCategory o ℓ e) where
diff --git a/public/UniformIterationAlgebras.html b/public/UniformIterationAlgebras.html
index a78a1e3..68df02e 100644
--- a/public/UniformIterationAlgebras.html
+++ b/public/UniformIterationAlgebras.html
@@ -11,8 +11,11 @@
     div.columns{display: flex; gap: min(4vw, 1.5em);}
     div.column{flex: auto; overflow-x: auto;}
     div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
-    ul.task-list{list-style: none;}
+    /* The extra [class] is a hack that increases specificity enough to
+       override a similar rule in reveal.js */
+    ul.task-list[class]{list-style: none;}
     ul.task-list li input[type="checkbox"] {
+      font-size: inherit;
       width: 0.8em;
       margin: 0 0.8em 0.2em -1.6em;
       vertical-align: middle;
@@ -37,8 +40,8 @@
 
Summary

 
This file introduces the category of Uniform-Iteration Algebras

 
    
-
  • Definition
-12 Uniform-Iteration Algebras
    • 
+
    • 
 

 
Code

 
module UniformIterationAlgebras {o ℓ e} (D : ExtensiveDistributiveCategory o ℓ e) where
diff --git a/src/Coalgebra.lagda.md b/src/Coalgebra.lagda.md
new file mode 100644
index 0000000..ead010d
--- /dev/null
+++ b/src/Coalgebra.lagda.md
@@ -0,0 +1,25 @@
+## Coproducts in the category of Coalgebras (needs proper imports to be compiled)
+
+```agda
+module Coalgebra where
+```
+
+  Coalg-cop : (F : Endofunctor C) → (alg₁ : F-Coalgebra F) → (alg₂ : F-Coalgebra F) → Coproduct (F-Coalgebras F) alg₁ alg₂
+  Coalg-cop F alg₁ alg₂ = record
+    { A+B = record { A = A + B ; α = [ (F₁ i₁ ∘ α) , F₁ i₂ ∘ β ] }
+    ; i₁ = record { f = i₁ ; commutes = inject₁ }
+    ; i₂ = record { f = i₂ ; commutes = inject₂ }
+    ; [_,_] = λ {CA} h i → record { f = [ F-Coalgebra-Morphism.f h , F-Coalgebra-Morphism.f i ] ; commutes = begin 
+      F-Coalgebra.α CA ∘ [ F-Coalgebra-Morphism.f h , F-Coalgebra-Morphism.f i ] ≈⟨ ∘[] ⟩ 
+      [ F-Coalgebra.α CA ∘ F-Coalgebra-Morphism.f h , F-Coalgebra.α CA ∘ F-Coalgebra-Morphism.f i ] ≈⟨ ⟺ ([]-cong₂ (⟺ (F-Coalgebra-Morphism.commutes h)) ((⟺ (F-Coalgebra-Morphism.commutes i)))) ⟩
+      [ F₁ (F-Coalgebra-Morphism.f h) ∘ α , F₁ (F-Coalgebra-Morphism.f i) ∘ β ] ≈⟨ ⟺ ([]-cong₂ ((F-resp-≈ inject₁) ⟩∘⟨refl) ((F-resp-≈ inject₂) ⟩∘⟨refl)) ⟩
+      [ F₁ ([ F-Coalgebra-Morphism.f h , F-Coalgebra-Morphism.f i ] ∘ i₁) ∘ α , F₁ ([ F-Coalgebra-Morphism.f h , F-Coalgebra-Morphism.f i ] ∘ i₂) ∘ β ] ≈⟨ ⟺ ([]-cong₂ (pullˡ (⟺ homomorphism)) (pullˡ (⟺ homomorphism))) ⟩
+      [ F₁ ([ F-Coalgebra-Morphism.f h , F-Coalgebra-Morphism.f i ]) ∘ F₁ i₁ ∘ α , F₁ ([ F-Coalgebra-Morphism.f h , F-Coalgebra-Morphism.f i ]) ∘ F₁ i₂ ∘ β ] ≈⟨ ⟺ ∘[] ⟩
+      F₁ ([ F-Coalgebra-Morphism.f h , F-Coalgebra-Morphism.f i ]) ∘ [ F₁ i₁ ∘ α , F₁ i₂ ∘ β ] ∎ }
+    ; inject₁ = inject₁
+    ; inject₂ = inject₂
+    ; unique = λ eq₁ eq₂ → +-unique eq₁ eq₂
+    }
+    where open Functor F
+          open F-Coalgebra alg₁
+          open F-Coalgebra alg₂ renaming (A to B; α to β)
\ No newline at end of file
diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md
index 49617b6..7cf811c 100644
--- a/src/Monad/Instance/Delay.lagda.md
+++ b/src/Monad/Instance/Delay.lagda.md
@@ -1,5 +1,6 @@