Last fixes, added comments, summaries and fixed pipeline

Makefile

@@ -1,17 +1,22 @@
-.PHONY: all clean
+.PHONY: all clean pandoc
 
-all: Everything.agda
+all: agda
+	make pandoc
+
+pandoc: out/*.md
+	@$(foreach file,$^, \
+		pandoc $(file) -s -c Agda.css -o $(file:.md=.html) ; \
+	)
+
+agda : Everything.agda
 	agda --html --html-dir=out Everything.agda --html-highlight=auto -i.
-	pandoc out/MonadK.md -s -c Agda.css -o out/MonadK.html
-	pandoc out/ElgotAlgebra.md -s -c Agda.css -o out/ElgotAlgebra.html
 
 clean:
 	rm Everything.agda
 	rm -rf out/*
 
 open:
-	firefox out/MonadK.html
+	firefox out/Everything.html
-	firefox out/ElgotAlgebra.html
 
 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/ElgotAlgebras.lagda.md

@@ -1,6 +1,7 @@
+<!--
+```agda
 {-# OPTIONS --allow-unsolved-metas #-}
 open import Level
-
 open import Categories.Category.Cocartesian using (Cocartesian)
 open import Categories.Category.Cartesian using (Cartesian)
 open import Categories.Category.BinaryProducts using (BinaryProducts)
@@ -16,7 +17,19 @@ open import Categories.Category.Extensive.Bundle
 open import Categories.Category.Extensive
 import Categories.Morphism as M
 import Categories.Morphism.Reasoning as MR
+```
+-->
 
+## Summary
+This file introduces the category of *unguarded* elgot algebras
+
+- [X] *Definition 7* Category of elgot algebras
+- [X] *Lemma 11* Products of elgot algebras
+- [ ] *Lemma 11* Exponentials of elgot algebras
+
+## Code
+
+```agda
 module ElgotAlgebras where
 
 private
@@ -32,10 +45,11 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
   open MR C
   open HomReasoning
   open Equiv
+```
 
-  --*
+### *Definition 7*: Category of elgot algebras
-  -- let's define the category of elgot-algebras
+
-  --*
+```agda
 
   -- iteration preversing morphism between two elgot-algebras
   module _ (E₁ E₂ : Elgot-Algebra D) where
@@ -81,21 +95,23 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
     ; ∘-resp-≈  = ∘-resp-≈
     }
     where open Elgot-Algebra-Morphism
+```
 
-  --*
+### *Lemma 11*: Products of elgot algebras
-  -- products and exponentials of elgot-algebras
-  --*
 
+```agda
   -- if the carrier contains a terminal, so does elgot-algebras
   Terminal-Elgot-Algebras : Terminal C → Terminal Elgot-Algebras
   Terminal-Elgot-Algebras T = record 
     { ⊤ = record
       { A = ⊤
-      ; _# = λ x → !
+      ; algebra = record
-      ; #-Fixpoint = λ {_ f} → !-unique ([ idC , ! ] ∘ f)
+        { _# = λ x → !
-      ; #-Uniformity = λ {_ _ _ _ h} _ → !-unique (! ∘ h)
+        ; #-Fixpoint = λ {_ f} → !-unique ([ idC , ! ] ∘ f)
-      ; #-Folding = refl
+        ; #-Uniformity = λ {_ _ _ _ h} _ → !-unique (! ∘ h)
-      ; #-resp-≈ = λ _ → refl
+        ; #-Folding = refl
+        ; #-resp-≈ = λ _ → refl
+        }
       } 
     ; ⊤-is-terminal = record 
       { ! = λ {A} → record { h = ! ; preserves = λ {X} {f} → sym (!-unique (! ∘ (A Elgot-Algebra.#) f))   } 
@@ -109,48 +125,50 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
   A×B-Helper : ∀ {EA EB : Elgot-Algebra D} → Elgot-Algebra D
   A×B-Helper {EA} {EB}  = record
     { A = A × B
-    ; _# = λ {X : Obj} (h : X ⇒ A×B + X) → ⟨ ((π₁ +₁ idC) ∘ h)#ᵃ , ((π₂ +₁ idC) ∘ h)#ᵇ ⟩
+    ; algebra = record
-    ; #-Fixpoint = λ {X} {f} → begin
+      { _# = λ {X : Obj} (h : X ⇒ A×B + X) → ⟨ ((π₁ +₁ idC) ∘ h)#ᵃ , ((π₂ +₁ idC) ∘ h)#ᵇ ⟩
-      ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩                                                             ≈⟨ ⟨⟩-cong₂ #ᵃ-Fixpoint #ᵇ-Fixpoint ⟩
+      ; #-Fixpoint = λ {X} {f} → begin
-      ⟨ [ idC , ((π₁ +₁ idC) ∘ f)#ᵃ ] ∘ ((π₁ +₁ idC) ∘ f) , [ idC , ((π₂ +₁ idC) ∘ f)#ᵇ ] ∘ ((π₂ +₁ idC) ∘ f) ⟩ ≈⟨ ⟨⟩-cong₂ (pullˡ []∘+₁) (pullˡ []∘+₁) ⟩
+        ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩                                                             ≈⟨ ⟨⟩-cong₂ #ᵃ-Fixpoint #ᵇ-Fixpoint ⟩
-      ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ∘ f , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ∘ f ⟩           ≈˘⟨ ⟨⟩∘ ⟩
+        ⟨ [ idC , ((π₁ +₁ idC) ∘ f)#ᵃ ] ∘ ((π₁ +₁ idC) ∘ f) , [ idC , ((π₂ +₁ idC) ∘ f)#ᵇ ] ∘ ((π₂ +₁ idC) ∘ f) ⟩ ≈⟨ ⟨⟩-cong₂ (pullˡ []∘+₁) (pullˡ []∘+₁) ⟩
-      (⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ∘ f)             ≈⟨ ∘-resp-≈ˡ (unique′ 
+        ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ∘ f , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ∘ f ⟩           ≈˘⟨ ⟨⟩∘ ⟩
-        (begin 
+        (⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ∘ f)             ≈⟨ ∘-resp-≈ˡ (unique′ 
-          π₁ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₁ ⟩ 
-          [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ]                                                     ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₁)) ⟩
-          [ π₁ ∘ idC , π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                            ≈˘⟨ ∘[] ⟩
-          π₁ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                                 ∎) 
-        (begin 
-          π₂ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₂ ⟩ 
-          [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ]                                                     ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₂)) ⟩
-          [ π₂ ∘ idC , π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                            ≈˘⟨ ∘[] ⟩
-          π₂ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                                 ∎)
-      )⟩
-      ([ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∘ f)                                             ∎
-    ; #-Uniformity = λ {X Y f g h} uni → unique′ 
-      (begin 
-        π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₁ ⟩ 
-          (((π₁ +₁ idC) ∘ f)#ᵃ)                            ≈⟨ #ᵃ-Uniformity 
-            (begin 
-            -- TODO factor these out or adjust +₁ swap... maybe call it +₁-id-comm
-              (idC +₁ h) ∘ (π₁ +₁ idC) ∘ f                     ≈⟨ pullˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm)) ⟩ 
-              (π₁ ∘ idC +₁ idC ∘ h) ∘ f                        ≈˘⟨ pullˡ +₁∘+₁ ⟩
-              (π₁ +₁ idC) ∘ (idC +₁ h) ∘ f                     ≈⟨ pushʳ uni ⟩
-              ((π₁ +₁ idC) ∘ g) ∘ h                            ∎)⟩
-      (((π₁ +₁ idC) ∘ g)#ᵃ ∘ h)                                  ≈˘⟨ pullˡ project₁ ⟩
-        π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h     ∎) 
-      (begin 
-        π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₂ ⟩ 
-        ((π₂ +₁ idC) ∘ f)#ᵇ                                ≈⟨ #ᵇ-Uniformity 
           (begin 
-            (idC +₁ h) ∘ (π₂ +₁ idC) ∘ f   ≈⟨ pullˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm))⟩
+            π₁ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₁ ⟩ 
-            ((π₂ ∘ idC +₁ idC ∘ h) ∘ f)    ≈˘⟨ pullˡ +₁∘+₁ ⟩
+            [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ]                                                     ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₁)) ⟩
-            (π₂ +₁ idC) ∘ ((idC +₁ h)) ∘ f ≈⟨ pushʳ uni ⟩
+            [ π₁ ∘ idC , π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                            ≈˘⟨ ∘[] ⟩
-            ((π₂ +₁ idC) ∘ g) ∘ h          ∎)⟩
+            π₁ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                                 ∎) 
-        ((π₂ +₁ idC) ∘ g)#ᵇ ∘ h                                    ≈˘⟨ pullˡ project₂ ⟩
+          (begin 
-        π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h     ∎)
+            π₂ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₂ ⟩ 
-    ; #-Folding = λ {X} {Y} {f} {h} → ⟨⟩-cong₂ (foldingˡ {X} {Y}) (foldingʳ {X} {Y})
+            [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ]                                                     ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₂)) ⟩
-    ; #-resp-≈ = λ fg → ⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ʳ fg)) (#ᵇ-resp-≈ (∘-resp-≈ʳ fg))
+            [ π₂ ∘ idC , π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                            ≈˘⟨ ∘[] ⟩
+            π₂ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                                 ∎)
+        )⟩
+        ([ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∘ f)                                             ∎
+      ; #-Uniformity = λ {X Y f g h} uni → unique′ 
+        (begin 
+          π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₁ ⟩ 
+            (((π₁ +₁ idC) ∘ f)#ᵃ)                            ≈⟨ #ᵃ-Uniformity 
+              (begin 
+              -- TODO factor these out or adjust +₁ swap... maybe call it +₁-id-comm
+                (idC +₁ h) ∘ (π₁ +₁ idC) ∘ f                     ≈⟨ pullˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm)) ⟩ 
+                (π₁ ∘ idC +₁ idC ∘ h) ∘ f                        ≈˘⟨ pullˡ +₁∘+₁ ⟩
+                (π₁ +₁ idC) ∘ (idC +₁ h) ∘ f                     ≈⟨ pushʳ uni ⟩
+                ((π₁ +₁ idC) ∘ g) ∘ h                            ∎)⟩
+        (((π₁ +₁ idC) ∘ g)#ᵃ ∘ h)                                  ≈˘⟨ pullˡ project₁ ⟩
+          π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h     ∎) 
+        (begin 
+          π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₂ ⟩ 
+          ((π₂ +₁ idC) ∘ f)#ᵇ                                ≈⟨ #ᵇ-Uniformity 
+            (begin 
+              (idC +₁ h) ∘ (π₂ +₁ idC) ∘ f   ≈⟨ pullˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm))⟩
+              ((π₂ ∘ idC +₁ idC ∘ h) ∘ f)    ≈˘⟨ pullˡ +₁∘+₁ ⟩
+              (π₂ +₁ idC) ∘ ((idC +₁ h)) ∘ f ≈⟨ pushʳ uni ⟩
+              ((π₂ +₁ idC) ∘ g) ∘ h          ∎)⟩
+          ((π₂ +₁ idC) ∘ g)#ᵇ ∘ h                                    ≈˘⟨ pullˡ project₂ ⟩
+          π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h     ∎)
+      ; #-Folding = λ {X} {Y} {f} {h} → ⟨⟩-cong₂ (foldingˡ {X} {Y}) (foldingʳ {X} {Y})
+      ; #-resp-≈ = λ fg → ⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ʳ fg)) (#ᵇ-resp-≈ (∘-resp-≈ʳ fg)) 
+      }
     }
     where 
     open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈)
@@ -205,19 +223,26 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where
     { terminal = Terminal-Elgot-Algebras terminal
     ; products = record { product = λ {EA EB} → Product-Elgot-Algebras EA EB }
     }
+```
 
+*Lemma 11*: Exponentials of elgot algebras
+
+```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} {X} exp = record
     { A = A^X
-    ; _# = λ {Z} f → λg product (((((eval +₁ idC) ∘ (Categories.Object.Product.repack C product product' +₁ idC)) ∘ dstl) ∘ (f ⁂ idC)) #ᵃ)
+    ; algebra = record
-    ; #-Fixpoint = λ {X} {f} → {!   !}
+      { _# = λ {Z} f → λg product (((((eval +₁ idC) ∘ (Categories.Object.Product.repack C product product' +₁ idC)) ∘ dstl) ∘ (f ⁂ idC)) #ᵃ) 
-    ; #-Uniformity = {!   !}
+      ; #-Fixpoint = {!   !}
-    ; #-Folding = {!   !}
+      ; #-Uniformity = {!   !}
-    ; #-resp-≈ = {!   !}
+      ; #-Folding = {!   !}
+      ; #-resp-≈ = {!   !}
+      }
     }
     where
     open Exponential exp renaming (B^A to A^X; product to product')
     open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈)
     dstr = λ {X Y Z} → IsIso.inv (isIsoˡ {X} {Y} {Z})
     dstl = λ {X Y Z} → IsIso.inv (isIsoʳ {X} {Y} {Z})
+```

src/Monad/ElgotMonad.lagda.md

@@ -1,3 +1,7 @@
+<!--
+```agda
+{-# OPTIONS --allow-unsolved-metas #-}
+
 open import Level
 open import Categories.Category.Core
 open import Categories.Category.Extensive.Bundle
@@ -5,10 +9,26 @@ open import Categories.Category.BinaryProducts
 open import Categories.Category.Cocartesian
 open import Categories.Category.Cartesian
 open import Categories.Category.Extensive
+open import Categories.Monad
+open import Categories.Functor
 open import ElgotAlgebra
 
 import Categories.Morphism.Reasoning as MR
+```
+-->
 
+## Summary
+This file introduces Elgot Monads.
+
+- [X] *Definition 13* Pre-Elgot Monads
+- [ ] *Definition 13* strong pre-Elgot
+- [X] *Definition 14* Elgot Monads
+- [ ] *Definition 14* strong Elgot
+- [ ] *Proposition 15* (Strong) Elgot monads are (strong) pre-Elgot
+
+## Code
+
+```agda
 module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
   open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
   open HomReasoning
@@ -17,10 +37,11 @@ module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) w
   open BinaryProducts products hiding (η)
   open MR C
   open Equiv
+```
 
-  open import Categories.Monad
+### *Definition 13*: Pre-Elgot Monads
-  open import Categories.Functor
 
+```agda
   record IsPreElgot (T : Monad C) : Set (o ⊔ ℓ ⊔ e) where
     open Monad T
     open Functor F renaming (F₀ to T₀; F₁ to T₁)
@@ -42,7 +63,10 @@ module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) w
       isPreElgot : IsPreElgot T
 
     open IsPreElgot isPreElgot public
+```
+### *Definition 14*: Elgot Monads
 
+```agda
   record IsElgot (T : Monad C) : Set (o ⊔ ℓ ⊔ e) where
     open Monad T
     open Functor F renaming (F₀ to T₀; F₁ to T₁)
@@ -69,7 +93,11 @@ module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) w
       isElgot : IsElgot T
 
     open IsElgot isElgot public
+```
 
+### *Proposition 15*: (Strong) Elgot monads are (strong) pre-Elgot
+
+```agda
   -- elgot monads are pre-elgot
   Elgot⇒PreElgot : ElgotMonad → PreElgotMonad
   Elgot⇒PreElgot EM = record 
@@ -126,3 +154,4 @@ module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) w
       module T = Monad T
       open T using (F; η; μ)
       open Functor F renaming (F₀ to T₀; F₁ to T₁)
+```

src/Monad/Instance/Delay.lagda.md

@@ -1,18 +1,3 @@
----
-title: Delay Monad
-author: Leon Vatthauer
-format: pdf
-output:
-  pdf_document:
-    md_extensions: +task-lists
-mainfont: DejaVu Serif
-monofont: mononoki
-geometry: margin=0.5cm
-header-includes:
- - \usepackage{fvextra}
- - \DefineVerbatimEnvironment{Highlighting}{Verbatim}{breaklines,commandchars=\\\{\}}
----
-
 <!--
 ```agda
 open import Level
@@ -33,6 +18,14 @@ import Categories.Morphism.Reasoning as MR
 ```
 -->
 
+## Summary
+This file introduces the delay monad ***D***
+
+- [X] *Proposition 1* Characterization of the delay monad ***D*** (here treated as definition)
+- [ ] *Proposition 2* ***D*** is commutative
+
+## Code
+
 ```agda
 module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
   open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
@@ -44,8 +37,9 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
   open MR C
   open Equiv
   open HomReasoning
-
+```
-  -- Proposition 1
+### *Proposition 1*: Characterization of the delay monad ***D***
+```agda
   record DelayMonad (D : Endofunctor C) : Set (o ⊔ ℓ ⊔ e) where
     open Functor D using () renaming (F₀ to D₀; F₁ to D₁)
 
@@ -86,6 +80,4 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ
       ; sym-assoc = λ {X} {Y} {Z} {f} {g} → *-unique ((g *) ∘ f) ((g *) ∘ (f *))
       ; extend-≈ = *-resp-≈
       }
-
-  -- record Search
 ```

src/UniformIterationAlgebra.lagda.md

@@ -1,13 +1,27 @@
+<!--
+```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
+```
+-->
+## Summary
+This file introduces *Uniform-Iteration Algebras*
 
+- [X] *Definition 12* 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)
+```
 
+### *Definition 12*: Uniform-Iteration Algebras
+```agda
   record Uniform-Iteration-Algebra-on (A : Obj) : Set (o ⊔ ℓ ⊔ e) where
     -- iteration operator
     field
@@ -27,3 +41,4 @@ module UniformIterationAlgebra {o ℓ e} (D : ExtensiveDistributiveCategory o
       A : Obj
       algebra : Uniform-Iteration-Algebra-on A
     open Uniform-Iteration-Algebra-on algebra public
+```

src/UniformIterationAlgebras.lagda.md

@@ -1,19 +1,34 @@
+<!--
+```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
+```
+-->
 
+## Summary
+This file introduces the category of Uniform-Iteration Algebras
+
+- [X] *Definition 12* 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)
   open HomReasoning
   open MR C
   open Equiv
+```
 
+### *Definition 12*: Uniform-Iteration Algebras
+
+```agda
   -- iteration preversing morphism between two elgot-algebras
   module _ (E₁ E₂ : Uniform-Iteration-Algebra D) where
     open Uniform-Iteration-Algebra E₁ renaming (_# to _#₁)
@@ -58,3 +73,4 @@ module UniformIterationAlgebras {o ℓ e} (D : ExtensiveDistributiveCategory o
     ; ∘-resp-≈  = ∘-resp-≈
     }
     where open Uniform-Iteration-Algebra-Morphism
+```