Add search-algebras, start work on elgot-algebra properties

Makefile

@@ -10,21 +10,25 @@ pandoc: public/*.md
 
 agda: Everything.agda
 	agda --html --html-dir=public Everything.agda --html-highlight=auto -i.
+	mv public/Everything.html public/index.html
 
 clean:
-	rm Everything.agda
+	rm -f  Everything.agda
 	rm -rf public/*
+	find . -name '*.agdai' -exec rm \{\} \;
 
 open:
 	firefox public/Everything.html
 
-push: all
-	mv public/Everything.html public/index.html
+# push compiled html to my cip directory
+push: all push'
+
+# just push without building
+push':
 	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:
 	git ls-tree --full-tree -r --name-only HEAD | egrep '^src/[^\.]*.l?agda(\.md)?' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' -e 's/..md//' | LC_COLLATE='C' sort > Everything.agda

src/Algebra/Elgot/Properties.lagda.md

@@ -0,0 +1,41 @@
+<!--
+```agda
+open import Level
+open import Category.Instance.AmbientCategory
+open import Categories.Functor
+open import Categories.Monad.Relative renaming (Monad to RMonad)
+```
+-->
+
+## Summary
+Some properties of elgot-algebras, namely:
+
+- Every elgot-algebra `(A, α : D₀ A ⇒ A)` satisfies `α (extend ι) ≈ α (D₁ π₁)` **[Lemma 32]**
+
+```agda 
+module Algebra.Elgot.Properties {o ℓ e} (ambient : Ambient o ℓ e) where
+  open Ambient ambient
+  open import Monad.Instance.Delay ambient using (DelayM)
+  open import Algebra.ElgotAlgebra ambient
+  open Equiv
+  open HomReasoning
+
+  module _ {D : DelayM} (algebra : Guarded-Elgot-Algebra (DelayM.functor D)) where
+    open DelayM D
+    open Functor functor renaming (F₁ to D₁)
+    open RMonad kleisli
+    open Guarded-Elgot-Algebra algebra
+
+    commutes : α ∘ extend ι ≈ α ∘ (D₁ π₁)
+    commutes = {!   !}
+      where
+        α∘ι : α ∘ ι ≈ π₁
+        α∘ι = sym (begin 
+          π₁ ≈⟨ unique {f = idC} {g = idC} (sym project₁) (sym project₁) ⟩ 
+          universal idC idC ≈⟨ {!   !} ⟩
+          {!   !} ≈⟨ {!   !} ⟩
+          universal {!   !} {!   !} ≈˘⟨ unique {!   !} {!   !} ⟩
+          α ∘ ι ∎)
+
+    
+```

src/Algebra/ElgotAlgebra.lagda.md

@@ -3,13 +3,7 @@
 open import Level
 open import Categories.Functor renaming (id to idF)
 open import Categories.Functor.Algebra
-open import Categories.Category
-open import Categories.Category.Cartesian
-open import Categories.Category.BinaryProducts
-open import Categories.Category.Cocartesian
-open import Categories.Category.Extensive.Bundle
-open import Categories.Category.Extensive
-import Categories.Morphism.Reasoning as MR
+open import Category.Instance.AmbientCategory using (Ambient)
 ```
 -->
 
@@ -23,24 +17,14 @@ This file introduces (guarded) elgot algebras
 ## Code
 
 ```agda
-module ElgotAlgebra where
-
-private
-  variable
-    o ℓ e : Level
-
-
-module _ (D : ExtensiveDistributiveCategory o ℓ e) where
-  open ExtensiveDistributiveCategory D renaming (U to C; id to idC)
-  open Cocartesian (Extensive.cocartesian extensive)
-  open Cartesian (ExtensiveDistributiveCategory.cartesian D)
+module Algebra.ElgotAlgebra {o ℓ e} (ambient : Ambient o ℓ e) where
+  open Ambient ambient
   open MR C
 ```
 
 ### *Definition 7* Guarded Elgot Algebras
 ```agda
-  module _ {F : Endofunctor C} (FA : F-Algebra F) where
-    record Guarded-Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where
+  record Guarded-Elgot-Algebra-on {F : Endofunctor C} (FA : F-Algebra F) : Set (o ⊔ ℓ ⊔ e) where
     open Functor F public
     open F-Algebra FA public
     -- iteration operator
@@ -60,6 +44,11 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
         → f ≈ g 
         → (f #) ≈ (g #)
 
+  record Guarded-Elgot-Algebra (F : Endofunctor C) : Set (o ⊔ ℓ ⊔ e) where
+    field
+      algebra : F-Algebra F
+      guarded-elgot-algebra-on : Guarded-Elgot-Algebra-on algebra
+    open Guarded-Elgot-Algebra-on guarded-elgot-algebra-on public
 ```
 
 ### *Proposition 10* Unguarded Elgot Algebras
@@ -151,21 +140,24 @@ Here we give a different Characterization and show that it is equal.
      where open Functor (idF {C = C})
 
   -- constructing an Id-Guarded Elgot-Algebra from an unguarded one
-  Unguarded→Id-Guarded : (EA : Elgot-Algebra) → Guarded-Elgot-Algebra (Id-Algebra (Elgot-Algebra.A EA))
+  Unguarded→Id-Guarded : (EA : Elgot-Algebra) → Guarded-Elgot-Algebra idF
   Unguarded→Id-Guarded ea = record
+    { algebra = Id-Algebra A
+    ; guarded-elgot-algebra-on = record
       { _# = _#
       ; #-Fixpoint = λ {X} {f} → trans #-Fixpoint (sym (∘-resp-≈ˡ ([]-congˡ identityˡ)))
       ; #-Uniformity = #-Uniformity
       ; #-Compositionality = #-Compositionality
       ; #-resp-≈ = #-resp-≈
       }
+    }
     where 
     open Elgot-Algebra ea
     open HomReasoning
     open Equiv
 
   -- constructing an unguarded Elgot-Algebra from an Id-Guarded one 
-  Id-Guarded→Unguarded : ∀ {A : Obj} → Guarded-Elgot-Algebra (Id-Algebra A) → Elgot-Algebra
+  Id-Guarded→Unguarded : ∀ {A} → Guarded-Elgot-Algebra-on (Id-Algebra A) → Elgot-Algebra
   Id-Guarded→Unguarded gea = record 
     { A = A 
     ; algebra = record
@@ -181,7 +173,7 @@ Here we give a different Characterization and show that it is equal.
       }
     }
     where 
-    open Guarded-Elgot-Algebra gea
+    open Guarded-Elgot-Algebra-on gea
     open HomReasoning
     open Equiv
     left : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} 

src/Algebra/Search.lagda.md

@@ -0,0 +1,29 @@
+<!--
+```agda
+open import Level
+open import Category.Instance.AmbientCategory using (Ambient)
+open import Categories.Functor.Algebra
+```
+-->
+## Summary
+A *D-Algebra* `(A, α : D₀ A ⇒ A)` is called a *search-algebra* if it satiesfies
+
+- α now ≈ id
+- α ▷ ≈ α
+
+## Code
+
+```agda
+module Algebra.Search {o ℓ e} (ambient : Ambient o ℓ e) where
+  open Ambient ambient
+  open import Monad.Instance.Delay ambient using (DelayM)
+
+  module _ (D : DelayM) where
+    open DelayM D
+
+    record IsSearchAlgebra (algebra : F-Algebra functor) : Set e where
+      open F-Algebra algebra using (A; α)
+      field
+        identity₁ : α ∘ now ≈ idC
+        identity₂ : α ∘ ▷ ≈ α 
+```

src/Algebra/UniformIterationAlgebra.lagda.md

@@ -1,10 +1,7 @@
 <!--
 ```agda
 open import Level
-open import Categories.Category.Core
-open import Categories.Category.Extensive.Bundle
-open import Categories.Category.Extensive
-open import Categories.Category.Cocartesian
+open import Category.Instance.AmbientCategory using (Ambient)
 ```
 -->
 ## Summary
@@ -15,9 +12,8 @@ This file introduces *Uniform-Iteration Algebras*
 ## Code
 
 ```agda
-module UniformIterationAlgebra {o ℓ e} (D : ExtensiveDistributiveCategory o ℓ e) where
-  open ExtensiveDistributiveCategory D renaming (U to C; id to idC)
-  open Cocartesian (Extensive.cocartesian extensive)
+module Algebra.UniformIterationAlgebra {o ℓ e} (ambient : Ambient o ℓ e) where
+  open Ambient ambient
 ```
 
 ### *Definition 12*: Uniform-Iteration Algebras

src/Category/Construction/ElgotAlgebras.lagda.md

@@ -11,12 +11,10 @@ open import Categories.Object.Product using (Product)
 open import Categories.Object.Coproduct using (Coproduct)
 open import Categories.Object.Exponential using (Exponential)
 open import Categories.Category
-open import ElgotAlgebra
 open import Categories.Category.Distributive
 open import Categories.Category.Extensive.Bundle
 open import Categories.Category.Extensive
-import Categories.Morphism as M
-import Categories.Morphism.Reasoning as MR
+open import Category.Instance.AmbientCategory using (Ambient)
 ```
 -->
 
@@ -30,17 +28,9 @@ This file introduces the category of *unguarded* elgot algebras
 ## Code
 
 ```agda
-module ElgotAlgebras where
-
-private
-  variable
-    o ℓ e : Level
-
-module _ (D : ExtensiveDistributiveCategory o ℓ e) where
-  open ExtensiveDistributiveCategory D renaming (U to C; id to idC)
-  open Cocartesian (Extensive.cocartesian extensive)
-  open Cartesian (ExtensiveDistributiveCategory.cartesian D)
-  open BinaryProducts products
+module Category.Construction.ElgotAlgebras {o ℓ e} (ambient : Ambient o ℓ e) where
+  open Ambient ambient
+  open import Algebra.ElgotAlgebra ambient
   open M C
   open MR C
   open HomReasoning
@@ -52,7 +42,7 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
 ```agda
 
   -- iteration preversing morphism between two elgot-algebras
-  module _ (E₁ E₂ : Elgot-Algebra D) where
+  module _ (E₁ E₂ : Elgot-Algebra) where
     open Elgot-Algebra E₁ renaming (_# to _#₁)
     open Elgot-Algebra E₂ renaming (_# to _#₂; A to B)
     record Elgot-Algebra-Morphism : Set (o ⊔ ℓ ⊔ e) where
@@ -63,7 +53,7 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
   -- the category of elgot algebras for a given category
   Elgot-Algebras : Category (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) e
   Elgot-Algebras = record
-    { Obj       = Elgot-Algebra D
+    { Obj       = Elgot-Algebra
     ; _⇒_       = Elgot-Algebra-Morphism
     ; _≈_       = λ f g → Elgot-Algebra-Morphism.h f ≈ Elgot-Algebra-Morphism.h g
     ; id        = λ {EB} → let open Elgot-Algebra EB in 
@@ -122,7 +112,7 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
     open Terminal T
 
   -- if the carriers of the algebra form a product, so do the algebras
-  A×B-Helper : ∀ {EA EB : Elgot-Algebra D} → Elgot-Algebra D
+  A×B-Helper : ∀ {EA EB : Elgot-Algebra} → Elgot-Algebra
   A×B-Helper {EA} {EB}  = record
     { A = A × B
     ; algebra = record
@@ -131,7 +121,7 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
         ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩                                                             ≈⟨ ⟨⟩-cong₂ #ᵃ-Fixpoint #ᵇ-Fixpoint ⟩
         ⟨ [ idC , ((π₁ +₁ idC) ∘ f)#ᵃ ] ∘ ((π₁ +₁ idC) ∘ f) , [ idC , ((π₂ +₁ idC) ∘ f)#ᵇ ] ∘ ((π₂ +₁ idC) ∘ f) ⟩ ≈⟨ ⟨⟩-cong₂ (pullˡ []∘+₁) (pullˡ []∘+₁) ⟩
         ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ∘ f , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ∘ f ⟩           ≈˘⟨ ⟨⟩∘ ⟩
-        (⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ∘ f)             ≈⟨ ∘-resp-≈ˡ (unique′ 
+        (⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ∘ f)             ≈⟨ ∘-resp-≈ˡ (⟨⟩-unique′ 
           (begin 
             π₁ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₁ ⟩ 
             [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ]                                                     ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₁)) ⟩
@@ -144,7 +134,7 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
             π₂ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                                 ∎)
         )⟩
         ([ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∘ f)                                             ∎
-      ; #-Uniformity = λ {X Y f g h} uni → unique′ 
+      ; #-Uniformity = λ {X Y f g h} uni → ⟨⟩-unique′ 
         (begin 
           π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₁ ⟩ 
             (((π₁ +₁ idC) ∘ f)#ᵃ)                            ≈⟨ #ᵃ-Uniformity 
@@ -192,7 +182,7 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
       [ (idC +₁ i₁) ∘ ((π₂ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵇ                        ≈⟨ #ᵇ-resp-≈ (+₁-id-swap π₂) ⟩
       ((π₂ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ                         ∎
 
-  Product-Elgot-Algebras : ∀ (EA EB : Elgot-Algebra D) → Product Elgot-Algebras EA EB
+  Product-Elgot-Algebras : ∀ (EA EB : Elgot-Algebra) → Product Elgot-Algebras EA EB
   Product-Elgot-Algebras EA EB = record
     { A×B = A×B-Helper {EA} {EB}
     ; π₁ = record { h = π₁ ; preserves = λ {X} {f} → project₁ }
@@ -209,7 +199,7 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
         ⟨ ((π₁ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC) ∘ h) #ᵃ , ((π₂ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC) ∘ h) #ᵇ ⟩     ∎ }
     ; project₁ = project₁
     ; project₂ = project₂
-    ; unique = unique
+    ; unique = ⟨⟩-unique
     }
     where
     open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈)
@@ -229,7 +219,7 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
 
 ```agda
   -- if the carriers of the algebra form a exponential, so do the algebras
-  B^A-Helper : ∀ {EA : Elgot-Algebra D} {X : Obj} → Exponential C X (Elgot-Algebra.A EA) → Elgot-Algebra D
+  B^A-Helper : ∀ {EA : Elgot-Algebra} {X : Obj} → Exponential C X (Elgot-Algebra.A EA) → Elgot-Algebra
   B^A-Helper {EA} {X} exp = record
     { A = A^X
     ; algebra = record

src/Category/Construction/UniformIterationAlgebras.lagda.md

@@ -2,11 +2,7 @@
 ```agda
 open import Level
 open import Categories.Category.Core
-open import Categories.Category.Extensive.Bundle
-open import Categories.Category.Extensive
-open import Categories.Category.Cocartesian
-import Categories.Morphism.Reasoning as MR
-open import UniformIterationAlgebra
+open import Category.Instance.AmbientCategory using (Ambient)
 ```
 -->
 
@@ -18,9 +14,9 @@ This file introduces the category of Uniform-Iteration Algebras
 ## Code
 
 ```agda
-module UniformIterationAlgebras {o ℓ e} (D : ExtensiveDistributiveCategory o ℓ e) where
-  open ExtensiveDistributiveCategory D renaming (U to C; id to idC)
-  open Cocartesian (Extensive.cocartesian extensive)
+module Category.Construction.UniformIterationAlgebras {o ℓ e} (ambient : Ambient o ℓ e) where
+  open Ambient ambient
+  open import Algebra.UniformIterationAlgebra ambient
   open HomReasoning
   open MR C
   open Equiv
@@ -30,7 +26,7 @@ module UniformIterationAlgebras {o ℓ e} (D : ExtensiveDistributiveCategory o
 
 ```agda
   -- iteration preversing morphism between two elgot-algebras
-  module _ (E₁ E₂ : Uniform-Iteration-Algebra D) where
+  module _ (E₁ E₂ : Uniform-Iteration-Algebra) where
     open Uniform-Iteration-Algebra E₁ renaming (_# to _#₁)
     open Uniform-Iteration-Algebra E₂ renaming (_# to _#₂; A to B)
     record Uniform-Iteration-Algebra-Morphism : Set (o ⊔ ℓ ⊔ e) where
@@ -41,7 +37,7 @@ module UniformIterationAlgebras {o ℓ e} (D : ExtensiveDistributiveCategory o
   -- the category of uniform-iteration algebras for a given category
   Uniform-Iteration-Algebras : Category (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) e
   Uniform-Iteration-Algebras = record
-    { Obj       = Uniform-Iteration-Algebra D
+    { Obj       = Uniform-Iteration-Algebra
     ; _⇒_       = Uniform-Iteration-Algebra-Morphism
     ; _≈_       = λ f g → Uniform-Iteration-Algebra-Morphism.h f ≈ Uniform-Iteration-Algebra-Morphism.h g
     ; id        = λ {EB} → let open Uniform-Iteration-Algebra EB in 

src/Category/Instance/AmbientCategory.lagda.md

@@ -0,0 +1,57 @@
+<!--
+```agda
+open import Level
+open import Categories.Category.Core
+
+open import Categories.Category.Extensive using (Extensive)
+open import Categories.Category.Extensive.Properties.Distributive using (Extensive×Cartesian⇒Distributive)
+open import Categories.Category.Distributive using (Distributive)
+open import Categories.Category.Cartesian using (Cartesian)
+open import Categories.Category.BinaryProducts using (BinaryProducts)
+open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
+open import Categories.Category.Cocartesian using (Cocartesian)
+open import Categories.Object.NaturalNumbers.Parametrized using (ParametrizedNNO)
+open import Categories.Object.Exponential using (Exponential)
+open import Categories.Object.Terminal
+import Categories.Morphism as M'
+import Categories.Morphism.Reasoning as MR'
+```
+-->
+
+## Summary
+We work in an ambient category that
+- 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.Instance.AmbientCategory where
+  record Ambient (o ℓ e : Level) : Set (suc o ⊔ suc ℓ ⊔ suc e) where
+    field
+      C : Category o ℓ e
+      extensive : Extensive C
+      cartesian : Cartesian C
+      ℕ : ParametrizedNNO (record { U = C ; cartesian = cartesian })
+      _^ℕ : ∀ 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
+    -- open Terminal terminal public
+    -- Don't open the terminal object, because we are interested in many different terminal objects stemming from multiple categories
+    open BinaryProducts products renaming (η to ⁂-η; g-η to ⁂-g-η; unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′) public
+    open ParametrizedNNO ℕ public
+
+
+    distributive : Distributive C
+    distributive = Extensive×Cartesian⇒Distributive C extensive cartesian
+    open Distributive distributive hiding (cartesian; cocartesian) public
+    
+    module M = M'
+    module MR = MR'
+```

src/Misc/Coalgebra.lagda.md

@@ -1,7 +1,7 @@
 ## Coproducts in the category of Coalgebras (needs proper imports to be compiled)
 
 ```agda
-module Coalgebra where
+module Misc.Coalgebra where
 ```
 
   Coalg-cop : (F : Endofunctor C) → (alg₁ : F-Coalgebra F) → (alg₂ : F-Coalgebra F) → Coproduct (F-Coalgebras F) alg₁ alg₂

src/Misc/FinalCoalgebras.lagda.md

@@ -1,3 +1,6 @@
+I thought briefly that I needed this, but I don't.
+Might still be interesting!
+
 ```agda
 open import Level
 open import Categories.Category
@@ -5,7 +8,7 @@ open import Categories.Functor
 import Categories.Morphism as M
 import Categories.Morphism.Reasoning as MR
 
-module FinalCoalgebras {o ℓ e} {C : Category o ℓ e} (F : Endofunctor C) where
+module Misc.FinalCoalgebras {o ℓ e} {C : Category o ℓ e} (F : Endofunctor C) where
 open Category C renaming (id to idC)
 open import Categories.Object.Terminal
 open import Categories.Functor.Coalgebra

src/Monad/ElgotMonad.lagda.md

@@ -3,17 +3,9 @@
 {-# OPTIONS --allow-unsolved-metas #-}
 
 open import Level
-open import Categories.Category.Core
-open import Categories.Category.Extensive.Bundle
-open import Categories.Category.BinaryProducts
-open import Categories.Category.Cocartesian
-open import Categories.Category.Cartesian
-open import Categories.Category.Extensive
+open import Category.Instance.AmbientCategory using (Ambient)
 open import Categories.Monad
 open import Categories.Functor
-open import ElgotAlgebra
-
-import Categories.Morphism.Reasoning as MR
 ```
 -->
 
@@ -29,14 +21,12 @@ This file introduces Elgot Monads.
 ## Code
 
 ```agda
-module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
-  open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
+module Monad.ElgotMonad {o ℓ e} (ambient : Ambient o ℓ e) where
+  open Ambient ambient
   open HomReasoning
-  open Cocartesian (Extensive.cocartesian extensive)
-  open Cartesian (ExtensiveDistributiveCategory.cartesian ED)
-  open BinaryProducts products hiding (η)
   open MR C
   open Equiv
+  open import Algebra.ElgotAlgebra ambient
 ```
 
 ### *Definition 13*: Pre-Elgot Monads
@@ -48,7 +38,7 @@ module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) w
 
     -- every TX needs to be equipped with an elgot algebra structure
     field
-      elgotalgebras : ∀ {X} → Elgot-Algebra-on ED (T₀ X)
+      elgotalgebras : ∀ {X} → Elgot-Algebra-on (T₀ X)
 
     module elgotalgebras {X} = Elgot-Algebra-on (elgotalgebras {X})
 

src/Monad/Instance/Delay.lagda.md

@@ -3,16 +3,7 @@
 open import Level
 open import Categories.Category
 open import Categories.Monad
-open import Categories.Category.Distributive
-open import Categories.Category.Extensive.Bundle
-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.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
@@ -20,10 +11,7 @@ open import Categories.Functor
 open import Categories.Functor.Algebra
 open import Categories.Monad.Construction.Kleisli
 open import Categories.Category.Construction.F-Coalgebras
-open import Categories.NaturalTransformation
-open import FinalCoalgebras
-import Categories.Morphism as M
-import Categories.Morphism.Reasoning as MR
+open import Category.Instance.AmbientCategory using (Ambient)
 ```
 -->
 
@@ -33,19 +21,11 @@ This file introduces the delay monad ***D***
 ## Code
 
 ```agda
-module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
+module Monad.Instance.Delay {o ℓ e} (ambient : Ambient o ℓ e) where
+  open Ambient ambient
 ```
 <!--
 ```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
@@ -75,11 +55,9 @@ We can now define these functions by bisecting the isomorphism `out : DX ≅ X +
 
 ```agda
 
-    module _ (X : Obj) where
+    module _ {X : Obj} where
       open Terminal (coalgebras X) using (⊤; !; !-unique)
-      open F-Coalgebra ⊤ renaming (A to DX)
-
-      D₀ = DX
+      open F-Coalgebra ⊤ using () renaming (A to DX) public
 
       out-≅ : DX ≅ X + DX
       out-≅ = colambek {F = X +- } (coalgebras X)
@@ -93,8 +71,12 @@ We can now define these functions by bisecting the isomorphism `out : DX ≅ X +
       later : DX ⇒ DX
       later = out⁻¹ ∘ i₂
 
+      -- convenient notation
+      ▷ = later
+
       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`:
@@ -115,14 +97,17 @@ At the same time the morphism `X × N ⇒ X + X × N` is a coalgebra for the `(Y
 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 })
+      iso = Lambek.lambek (record { ⊥ = PNNO-Algebra cartesianCategory coproducts X N z s ; ⊥-is-initial = PNNO⇒Initial₂ cartesianCategory coproducts ℕ X })
 
       ι : X × N ⇒ DX
       ι = u (! {A = record { A = X × N ; α = _≅_.from iso }})
+
+```
+Make `DX` conveniently accessible
+```agda
+    D₀ : Obj → Obj
+    D₀ X = DX {X}
 ```
 
 With these definitions at hand, we can now indeed construct a monad (in extension form) as the triple `(F₀, unit, extend)`.
@@ -132,23 +117,22 @@ TODO
 
 
 ```agda
-        
-    monad : Monad C
-    monad = Kleisli⇒Monad C (record
+    kleisli : KleisliTriple C
+    kleisli = record
       { F₀ = D₀ 
-      ; unit = λ {X} → now X
+      ; unit = now
       ; extend = extend
       ; identityʳ = identityʳ'
       ; identityˡ = identityˡ'
       ; 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 ] }
+          alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out , (idC +₁ i₂) ∘ out ] }
 
           extend : D₀ X ⇒ D₀ Y
           extend = u (! (coalgebras Y) {A = alg}) ∘ i₁ {B = D₀ Y}
@@ -156,39 +140,39 @@ TODO
           !∘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 : out ∘ extend ≈ [ out ∘ f , i₂ ∘ extend ] ∘ out
           extendlaw = begin 
-            out Y ∘ extend ≈⟨ pullˡ (commutes (! (coalgebras Y) {A = alg})) ⟩ 
+            out ∘ 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 ⟩
+            ∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out                   ≈⟨ pullˡ ∘[] ⟩
+            [ (idC +₁ (u (! (coalgebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f) 
+            , (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out ≈⟨ ([]-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₂ 
+              , (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out ∘ f) 
+            , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out        ≈⟨ ([]-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₂ 
+            [ [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₂ ] ∘ (out ∘ f) 
+            , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out        ≈⟨ ([]-cong₂ 
                                                                     (elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η))
                                                                     assoc) ⟩∘⟨refl ⟩
-            [ out Y ∘ f , i₂ ∘ extend ] ∘ out X                 ∎ 
+            [ out ∘ f , i₂ ∘ extend ] ∘ out                 ∎ 
 
-          extend-unique : (g : D₀ X ⇒ D₀ Y) → (out Y ∘ g ≈ [ out Y ∘ f , i₂ ∘ g ] ∘ out X) → extend ≈ g
+          extend-unique : (g : D₀ X ⇒ D₀ Y) → (out ∘ g ≈ [ out ∘ f , i₂ ∘ g ] ∘ out) → 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₂ 
+              out ∘ [ g , idC ]                                          ≈⟨ ∘[] ⟩ 
+              [ out ∘ g , out ∘ idC ]                                  ≈⟨ []-cong₂ g-commutes identityʳ ⟩ 
+              [ [ out ∘ f , i₂ ∘ g ] ∘ out , out ]                   ≈˘⟨ []-cong₂ 
                                                                                 (([]-cong₂ 
                                                                                   (([]-cong₂ refl identityʳ) ⟩∘⟨refl ○ (elimˡ +-η)) 
                                                                                   refl) 
                                                                                 ⟩∘⟨refl) 
                                                                                 refl ⟩ 
-              [ [ [ i₁ , i₂ ∘ idC ] ∘ (out Y ∘ f) 
-                , i₂ ∘ g ] ∘ out X 
-              , out Y ]                                                    ≈˘⟨ []-cong₂ 
+              [ [ [ i₁ , i₂ ∘ idC ] ∘ (out ∘ f) 
+                , i₂ ∘ g ] ∘ out 
+              , out ]                                                    ≈˘⟨ []-cong₂ 
                                                                                 (([]-cong₂ 
                                                                                   (([]-cong₂ identityʳ (pullʳ inject₂)) ⟩∘⟨refl) 
                                                                                   refl) 
@@ -196,9 +180,9 @@ TODO
                                                                                 refl 
                                                                               ⟩
               [ [ [ i₁ ∘ idC 
-                  , (i₂ ∘ [ g , idC ]) ∘ i₂ ] ∘ (out Y ∘ f) 
-                , i₂ ∘ g ] ∘ out X 
-              , out Y ]                                                    ≈˘⟨ []-cong₂ 
+                  , (i₂ ∘ [ g , idC ]) ∘ i₂ ] ∘ (out ∘ f) 
+                , i₂ ∘ g ] ∘ out 
+              , out ]                                                    ≈˘⟨ []-cong₂ 
                                                                                 (([]-cong₂ 
                                                                                   (([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl) 
                                                                                   (pullʳ inject₁)) 
@@ -206,16 +190,16 @@ TODO
                                                                                 (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₂ 
+                  , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₂ ] ∘ (out ∘ f) 
+                , (i₂ ∘ [ g , idC ]) ∘ i₁ ] ∘ out 
+              , (idC +₁ idC) ∘ out ]                                     ≈˘⟨ []-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 ]) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f) 
+                , (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₁ ] ∘ out 
+              , (idC ∘ idC +₁ [ g , idC ] ∘ i₂) ∘ out ]                  ≈˘⟨ []-cong₂ (pullˡ ∘[]) (pullˡ +₁∘+₁) ⟩
+              [ (idC +₁ [ g , idC ]) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out 
+              , (idC +₁ [ g , idC ]) ∘ (idC +₁ i₂) ∘ out ]               ≈˘⟨ ∘[] ⟩
               (idC +₁ [ g , idC ]) ∘ α alg ∎ })) ⟩∘⟨refl ⟩ 
             [ g , idC ] ∘ i₁                                               ≈⟨ inject₁ ⟩
             g ∎
@@ -242,38 +226,38 @@ TODO
           }
           where open Functor (Y +-) using (identity)
 
-        identityʳ' : ∀ {X} {Y} {f} → extend f ∘ now X ≈ f
+        identityʳ' : ∀ {X Y : Obj} {f : X ⇒ D₀ Y} → 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)) ⟩
+          extend f ∘ now                                          ≈⟨ insertˡ (_≅_.isoˡ out-≅) ⟩∘⟨refl ⟩ 
+          (out⁻¹ ∘ out ∘ extend f) ∘ now                      ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩
+          (out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend f ] ∘ out) ∘ now ≈⟨ pullʳ (pullʳ unitlaw) ⟩
+          out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend f ] ∘ i₁              ≈⟨ refl⟩∘⟨ inject₁ ⟩
+          out⁻¹ ∘ out ∘ f                                       ≈⟨ cancelˡ (_≅_.isoˡ out-≅) ⟩
           f                                                         ∎
 
-        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                                            ∎ })
+        identityˡ' : ∀ {X} → extend now ≈ idC
+        identityˡ' {X} = Terminal.⊤-id (coalgebras X) (record { f = extend now ; commutes = begin 
+          out ∘ extend now ≈⟨ pullˡ ((commutes (! (coalgebras X) {A = alg now}))) ⟩ 
+          ((idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ α (alg now)) ∘ i₁   ≈⟨ pullʳ inject₁ ⟩
+          (idC +₁ (u (! (coalgebras X) {A = alg now}))) 
+          ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ now) , i₂ ∘ i₁ ] ∘ out               ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw) ○ inject₁) refl ⟩∘⟨refl ⟩
+          (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out ≈⟨ pullˡ ∘[] ⟩
+          [ (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ i₁ 
+          , (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ i₂ ∘ i₁ ] ∘ out      ≈⟨ []-cong₂ +₁∘i₁ (pullˡ +₁∘i₂) ⟩∘⟨refl ⟩
+          [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras X) {A = alg now}))) ∘ i₁ ] ∘ out  ≈⟨ []-cong₂ refl assoc ⟩∘⟨refl ⟩
+          [ i₁ ∘ idC , i₂ ∘ (extend now) ] ∘ out                               ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
+          ([ i₁ , i₂ ] ∘ (idC +₁ extend now)) ∘ out                            ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩
+          (idC +₁ extend now) ∘ out                                            ∎ })
 
-        assoc' : ∀ {X} {Y} {Z} {g} {h} → extend (extend h ∘ g) ≈ extend h ∘ extend g
+        assoc' : ∀ {X Y Z : Obj} {g : X ⇒ D₀ Y} {h : Y ⇒ D₀ Z} → 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           ∎)
+          out ∘ extend h ∘ extend g                                           ≈⟨ pullˡ (extendlaw h) ⟩
+          ([ out ∘ h , i₂ ∘ extend h ] ∘ out) ∘ extend g                    ≈⟨ pullʳ (extendlaw g) ⟩
+          [ out ∘ h , i₂ ∘ extend h ] ∘ [ out ∘ g , i₂ ∘ extend g ] ∘ out ≈⟨ pullˡ ∘[] ⟩
+          [ [ out ∘ h , i₂ ∘ extend h ] ∘ out ∘ g 
+          , [ out ∘ h , i₂ ∘ extend h ] ∘ i₂ ∘ extend g ] ∘ out             ≈⟨ []-cong₂ (pullˡ (⟺ (extendlaw h))) (pullˡ inject₂) ⟩∘⟨refl ⟩
+          [ (out ∘ extend h) ∘ g , (i₂ ∘ extend h) ∘ extend g ] ∘ out       ≈⟨ ([]-cong₂ assoc assoc) ⟩∘⟨refl ⟩
+          [ out ∘ extend h ∘ g , i₂ ∘ extend h ∘ extend g ] ∘ out           ∎)
         
         extend-≈' : ∀ {X} {Y} {f g : X ⇒ D₀ Y} → f ≈ g → extend f ≈ extend g
         extend-≈' {X} {Y} {f} {g} eq = begin
@@ -285,6 +269,13 @@ TODO
             ⟩∘⟨refl ⟩ 
           (u (! (coalgebras Y) {A = alg g }) ∘ idC) ∘ i₁ {B = D₀ Y} ≈⟨ identityʳ ⟩∘⟨refl ⟩
           extend g                                                ∎
+
+    monad : Monad C
+    monad = Kleisli⇒Monad C kleisli
+
+    -- redundant but convenient to have
+    functor : Endofunctor C
+    functor = Monad.F monad
 ```
 
 ### Definition 30: Search-Algebras

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

@@ -0,0 +1,27 @@
+<!--
+```agda
+open import Level
+
+open import Categories.Functor
+open import Category.Instance.AmbientCategory using (Ambient)
+open import Categories.Monad.Construction.Kleisli
+open import Categories.Monad.Relative renaming (Monad to RMonad)
+```
+-->
+
+```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
+
+  module _ (D : DelayM) where
+    open DelayM D
+
+    open Functor functor using () renaming (F₁ to D₁)
+    open RMonad kleisli
+
+    module _ {X : Obj} (coeq : Coequalizer (extend (ι {X})) (D₁ π₁)) where
+      -- TODO
+```

src/Monad/Instance/K.lagda.md

@@ -1,12 +1,8 @@
 <!--
 ```agda
 open import Level
-open import Categories.Category.Core
 open import Categories.Category.Equivalence using (StrongEquivalence)
-open import Categories.Category.Extensive.Bundle
 open import Function using (id)
-open import UniformIterationAlgebras
-open import UniformIterationAlgebra
 open import Categories.FreeObjects.Free
 open import Categories.Functor.Core
 open import Categories.Adjoint
@@ -16,6 +12,7 @@ open import Categories.NaturalTransformation.Core renaming (id to idN)
 open import Categories.Monad
 open import Categories.Category.Construction.EilenbergMoore
 open import Categories.Category.Slice
+open import Category.Instance.AmbientCategory using (Ambient)
 ```
 -->
 
@@ -34,13 +31,15 @@ In this file I explore the monad ***K*** and its properties:
 ## Code
 
 ```agda
-module MonadK {o ℓ e} (D : ExtensiveDistributiveCategory o ℓ e) where
-  open ExtensiveDistributiveCategory D renaming (U to C; id to idC)
+module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
+  open Ambient ambient
+  open import Category.Construction.UniformIterationAlgebras ambient
+  open import Algebra.UniformIterationAlgebra ambient
   open Equiv
 
   -- TODO move this to a different file
 
-  forgetfulF : Functor (Uniform-Iteration-Algebras D) C
+  forgetfulF : Functor Uniform-Iteration-Algebras C
   forgetfulF = record
     { F₀ = λ X → Uniform-Iteration-Algebra.A X
     ; F₁ = λ f → Uniform-Iteration-Algebra-Morphism.h f
@@ -51,7 +50,7 @@ module MonadK {o ℓ e} (D : ExtensiveDistributiveCategory o ℓ e) where
 
   -- typedef
   FreeUniformIterationAlgebra : Obj → Set (suc o ⊔ suc ℓ ⊔ suc e)
-  FreeUniformIterationAlgebra X = FreeObject {C = C} {D = Uniform-Iteration-Algebras D} forgetfulF X
+  FreeUniformIterationAlgebra X = FreeObject {C = C} {D = Uniform-Iteration-Algebras} forgetfulF X
 
 ```
 
@@ -62,7 +61,7 @@ module MonadK {o ℓ e} (D : ExtensiveDistributiveCategory o ℓ e) where
     field
       algebras : ∀ X → FreeUniformIterationAlgebra X
 
-    freeF : Functor C (Uniform-Iteration-Algebras D)
+    freeF : Functor C Uniform-Iteration-Algebras
     freeF = FO⇒Functor forgetfulF algebras
     
     adjoint : freeF ⊣ forgetfulF