🔨 refactor folder structure, define ambient category and use throughout

2024-05-31 07:28:34 +02:00 · 2023-09-12 16:03:20 +02:00 · 2023-09-12 16:03:20 +02:00 · 481e1011e5
commit 481e1011e5
parent 230b34da49
12 changed files with 151 additions and 121 deletions
--- a/12
+++ b/12
@ -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
--- a/src/Algebra/ElgotAlgebra.lagda.md
+++ b/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,17 +17,8 @@ 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
 ```

--- a/src/Algebra/UniformIterationAlgebra.lagda.md
+++ b/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
--- a/src/Category/Construction/ElgotAlgebras.lagda.md
+++ b/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
--- a/src/Category/Construction/UniformIterationAlgebras.lagda.md
+++ b/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 
--- a/src/Category/Instance/AmbientCategory.lagda.md
+++ b/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'
+```
--- a/src/Misc/Coalgebra.lagda.md
+++ b/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₂
--- a/src/Misc/FinalCoalgebras.lagda.md
+++ b/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
--- a/src/Monad/ElgotMonad.lagda.md
+++ b/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})

--- a/src/Monad/Instance/Delay.lagda.md
+++ b/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
@ -115,14 +95,11 @@ 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 cartesianCategory coproducts X N z s ; ⊥-is-initial = PNNO⇒Initial₂ cartesianCategory coproducts ℕ X })

-        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 }})
+      ι : 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)`.
@ -132,9 +109,8 @@ TODO


 ```agda
-        
-    monad : Monad C
-    monad = Kleisli⇒Monad C (record
+    kleisli : KleisliTriple C
+    kleisli = record
      { F₀ = D₀ 
      ; unit = λ {X} → now X
      ; extend = extend
@ -143,7 +119,7 @@ TODO
      ; assoc = assoc'
      ; sym-assoc = sym assoc'
      ; extend-≈ = extend-≈'
-      })
+      }
      where
        open Terminal
        module _ {X Y : Obj} (f : X ⇒ D₀ Y) where
@ -285,6 +261,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
--- a/src/Monad/Instance/Delay/Quotienting.lagda.md
+++ b/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
+```
--- a/src/Monad/Instance/K.lagda.md
+++ b/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