From 758f5c4ac360ce89ab5974368ec14dd90014f332 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Sat, 19 Aug 2023 16:01:48 +0200 Subject: [PATCH] Last fixes, added comments, summaries and fixed pipeline --- Makefile | 17 ++- ...otAlgebras.agda => ElgotAlgebras.lagda.md} | 143 ++++++++++-------- .../{ElgotMonad.agda => ElgotMonad.lagda.md} | 35 ++++- src/Monad/Instance/Delay.lagda.md | 32 ++-- ....agda => UniformIterationAlgebra.lagda.md} | 17 ++- ...agda => UniformIterationAlgebras.lagda.md} | 20 ++- 6 files changed, 173 insertions(+), 91 deletions(-) rename src/{ElgotAlgebras.agda => ElgotAlgebras.lagda.md} (65%) rename src/Monad/{ElgotMonad.agda => ElgotMonad.lagda.md} (93%) rename src/{UniformIterationAlgebra.agda => UniformIterationAlgebra.lagda.md} (79%) rename src/{UniformIterationAlgebras.agda => UniformIterationAlgebras.lagda.md} (91%) diff --git a/Makefile b/Makefile index 40114b9..b435fb1 100644 --- a/Makefile +++ b/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/ElgotAlgebra.html + firefox out/Everything.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 \ No newline at end of file diff --git a/src/ElgotAlgebras.agda b/src/ElgotAlgebras.lagda.md similarity index 65% rename from src/ElgotAlgebras.agda rename to src/ElgotAlgebras.lagda.md index f0ce382..9b143db 100644 --- a/src/ElgotAlgebras.agda +++ b/src/ElgotAlgebras.lagda.md @@ -1,6 +1,7 @@ + +## 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 +``` - --* - -- let's define the category of elgot-algebras - --* +### *Definition 7*: 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 +``` - --* - -- products and exponentials of elgot-algebras - --* +### *Lemma 11*: Products 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 → ! - ; #-Fixpoint = λ {_ f} → !-unique ([ idC , ! ] ∘ f) - ; #-Uniformity = λ {_ _ _ _ h} _ → !-unique (! ∘ h) - ; #-Folding = refl - ; #-resp-≈ = λ _ → refl + ; algebra = record + { _# = λ x → ! + ; #-Fixpoint = λ {_ f} → !-unique ([ idC , ! ] ∘ f) + ; #-Uniformity = λ {_ _ _ _ h} _ → !-unique (! ∘ h) + ; #-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)#ᵇ ⟩ - ; #-Fixpoint = λ {X} {f} → begin - ⟨ ((π₁ +₁ 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′ - (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)#ᵇ ⟩ ] ∎) - (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 + ; algebra = record + { _# = λ {X : Obj} (h : X ⇒ A×B + X) → ⟨ ((π₁ +₁ idC) ∘ h)#ᵃ , ((π₂ +₁ idC) ∘ h)#ᵇ ⟩ + ; #-Fixpoint = λ {X} {f} → begin + ⟨ ((π₁ +₁ 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′ (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)) + π₁ ∘ ⟨ [ 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 ∘ 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)) #ᵃ) - ; #-Fixpoint = λ {X} {f} → {! !} - ; #-Uniformity = {! !} - ; #-Folding = {! !} - ; #-resp-≈ = {! !} + ; algebra = record + { _# = λ {Z} f → λg product (((((eval +₁ idC) ∘ (Categories.Object.Product.repack C product product' +₁ idC)) ∘ dstl) ∘ (f ⁂ idC)) #ᵃ) + ; #-Fixpoint = {! !} + ; #-Uniformity = {! !} + ; #-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}) \ No newline at end of file + dstl = λ {X Y Z} → IsIso.inv (isIsoʳ {X} {Y} {Z}) +``` diff --git a/src/Monad/ElgotMonad.agda b/src/Monad/ElgotMonad.lagda.md similarity index 93% rename from src/Monad/ElgotMonad.agda rename to src/Monad/ElgotMonad.lagda.md index dc4299c..96f94e9 100644 --- a/src/Monad/ElgotMonad.agda +++ b/src/Monad/ElgotMonad.lagda.md @@ -1,3 +1,7 @@ + +## 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 - open import Categories.Functor +``` +### *Definition 13*: Pre-Elgot Monads + +```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₁) +``` diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md index 08fc44b..fafe8d8 100644 --- a/src/Monad/Instance/Delay.lagda.md +++ b/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=\\\{\}} ---- - +## 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 -``` \ No newline at end of file +``` diff --git a/src/UniformIterationAlgebra.agda b/src/UniformIterationAlgebra.lagda.md similarity index 79% rename from src/UniformIterationAlgebra.agda rename to src/UniformIterationAlgebra.lagda.md index 26b6749..46b7892 100644 --- a/src/UniformIterationAlgebra.agda +++ b/src/UniformIterationAlgebra.lagda.md @@ -1,13 +1,27 @@ + +## 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 @@ -26,4 +40,5 @@ module UniformIterationAlgebra {o ℓ e} (D : ExtensiveDistributiveCategory o field A : Obj algebra : Uniform-Iteration-Algebra-on A - open Uniform-Iteration-Algebra-on algebra public \ No newline at end of file + open Uniform-Iteration-Algebra-on algebra public +``` diff --git a/src/UniformIterationAlgebras.agda b/src/UniformIterationAlgebras.lagda.md similarity index 91% rename from src/UniformIterationAlgebras.agda rename to src/UniformIterationAlgebras.lagda.md index c8c5489..43fe151 100644 --- a/src/UniformIterationAlgebras.agda +++ b/src/UniformIterationAlgebras.lagda.md @@ -1,19 +1,34 @@ + +## 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 _#₁) @@ -57,4 +72,5 @@ module UniformIterationAlgebras {o ℓ e} (D : ExtensiveDistributiveCategory o } ; ∘-resp-≈ = ∘-resp-≈ } - where open Uniform-Iteration-Algebra-Morphism \ No newline at end of file + where open Uniform-Iteration-Algebra-Morphism +```