diff --git a/.gitignore b/.gitignore index 02091f1..bbc4346 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,5 @@ -*.agdai \ No newline at end of file +*.agdai +out/ +*.pdf +*.log +Everything.agda \ No newline at end of file diff --git a/ElgotAlgebra.agda b/ElgotAlgebra.lagda.md similarity index 96% rename from ElgotAlgebra.agda rename to ElgotAlgebra.lagda.md index 62a9113..127b0f2 100644 --- a/ElgotAlgebra.agda +++ b/ElgotAlgebra.lagda.md @@ -1,7 +1,6 @@ + + +## Summary +This file introduces (guarded) elgot algebras + +- [X] *Definition 7* Guarded Elgot Algebras +- [ ] *Theorem 8* Existence of final coalgebras is equivalent to existence of free H-guarded Elgot algebras +- [X] *Proposition 10* Characterization of unguarded elgot algebras + +## Code + +```agda +module ElgotAlgebra where private variable @@ -22,10 +35,10 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where open Cocartesian (Extensive.cocartesian extensive) open Cartesian (ExtensiveDistributiveCategory.cartesian D) open MR C +``` - --* - -- F-guarded Elgot Algebra - --* +### *Definition 7* Guarded Elgot Algebras +```agda module _ {F : Endofunctor C} (FA : F-Algebra F) where record Guarded-Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where open Functor F public @@ -47,10 +60,13 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where → f ≈ g → (f #) ≈ (g #) +``` - --* - -- (unguarded) Elgot-Algebra - --* +### *Proposition 10* Unguarded Elgot Algebras +Unguarded elgot algebras are `Id`-guarded elgot algebras. +Here we give a different Characterization and show that it is equal. + +```agda record Elgot-Algebra-on (A : Obj) : Set (o ⊔ ℓ ⊔ e) where -- iteration operator field @@ -231,3 +247,4 @@ module _ (D : ExtensiveDistributiveCategory o ℓ e) where [ idC , idC ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂) ≈˘⟨ pushˡ #-Fixpoint ⟩ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂ ∎ +``` \ No newline at end of file diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..25fbf27 --- /dev/null +++ b/Makefile @@ -0,0 +1,17 @@ +.PHONY: all clean + +all: MonadK.lagda.md + agda --html --html-dir=out MonadK.lagda.md --html-highlight=auto + agda --html --html-dir=out ElgotAlgebra.lagda.md --html-highlight=auto + 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 -rf out/* + +open: + firefox out/MonadK.html + firefox out/ElgotAlgebra.html + +Everything.agda: + git ls-tree --full-tree -r --name-only HEAD | grep '^[^\.]*.agda' | sed -e 's|^[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' | LC_COLLATE='C' sort > Everything.agda \ No newline at end of file diff --git a/Monad/Instance/Delay.agda b/Monad/Instance/Delay.lagda.md similarity index 88% rename from Monad/Instance/Delay.agda rename to Monad/Instance/Delay.lagda.md index b9621c8..08fc44b 100644 --- a/Monad/Instance/Delay.agda +++ b/Monad/Instance/Delay.lagda.md @@ -1,3 +1,20 @@ +--- +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 module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where open ExtensiveDistributiveCategory ED renaming (U to C; id to idC) open Cocartesian (Extensive.cocartesian extensive) @@ -65,4 +85,7 @@ module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ ; assoc = λ {X} {Y} {Z} {f} {g} → sym (*-unique ((g *) ∘ f) ((g *) ∘ (f *))) ; sym-assoc = λ {X} {Y} {Z} {f} {g} → *-unique ((g *) ∘ f) ((g *) ∘ (f *)) ; extend-≈ = *-resp-≈ - } \ No newline at end of file + } + + -- record Search +``` \ No newline at end of file diff --git a/MonadK.agda b/MonadK.agda deleted file mode 100644 index 7d2ac5f..0000000 --- a/MonadK.agda +++ /dev/null @@ -1,40 +0,0 @@ -open import Level -open import Categories.Category.Core -open import Categories.Category.Extensive.Bundle -open import Function using (id) - -module MonadK {o ℓ e} (D : ExtensiveDistributiveCategory o ℓ e) where - open ExtensiveDistributiveCategory D renaming (U to C; id to idC) - open import UniformIterationAlgebras - open import UniformIterationAlgebra - open import Categories.FreeObjects.Free - open import Categories.Functor.Core - open import Categories.Adjoint - open import Categories.Adjoint.Properties - open import Categories.NaturalTransformation.Core renaming (id to idN) - open import Categories.Monad - open Equiv - - record MonadK : Set (suc o ⊔ suc ℓ ⊔ suc e) where - forgetfulF : Functor (Uniform-Iteration-Algebras D) C - forgetfulF = record - { F₀ = λ X → Uniform-Iteration-Algebra.A X - ; F₁ = λ f → Uniform-Iteration-Algebra-Morphism.h f - ; identity = refl - ; homomorphism = refl - ; F-resp-≈ = id - } - - field - algebras : ∀ X → FreeObject {C = C} {D = Uniform-Iteration-Algebras D} forgetfulF X - - freeF : Functor C (Uniform-Iteration-Algebras D) - freeF = FO⇒Functor forgetfulF algebras - - adjoint : freeF ⊣ forgetfulF - adjoint = FO⇒LAdj forgetfulF algebras - - K : Monad C - K = adjoint⇒monad adjoint - - -- TODO show that the category of K-Algebras is the category of uniform-iteration algebras \ No newline at end of file diff --git a/MonadK.lagda.md b/MonadK.lagda.md new file mode 100644 index 0000000..6749755 --- /dev/null +++ b/MonadK.lagda.md @@ -0,0 +1,76 @@ + + +## Summary +In this file I explore the monad ***K*** and its properties: + +- [X] *Lemma 16* Definition of the monad +- [ ] *Lemma 16* EilenbergMoore⇒UniformIterationAlgebras (use [crude monadicity theorem](https://agda.github.io/agda-categories/Categories.Adjoint.Monadic.Crude.html)) +- [ ] *Proposition 19* ***K*** is strong +- [ ] *Theorem 22* ***K*** is an equational lifting monad +- [ ] *Proposition 23* The Kleisli category of ***K*** is enriched over pointed partial orders and strict monotone maps +- [ ] *Proposition 25* ***K*** is copyable and weakly discardable +- [ ] *Theorem 29* ***K*** is an initial pre-Elgot monad and an initial strong pre-Elgot monad + + +## Code + +```agda +module MonadK {o ℓ e} (D : ExtensiveDistributiveCategory o ℓ e) where + open ExtensiveDistributiveCategory D renaming (U to C; id to idC) + open Equiv + + -- TODO move this to a different file + + forgetfulF : Functor (Uniform-Iteration-Algebras D) C + forgetfulF = record + { F₀ = λ X → Uniform-Iteration-Algebra.A X + ; F₁ = λ f → Uniform-Iteration-Algebra-Morphism.h f + ; identity = refl + ; homomorphism = refl + ; F-resp-≈ = id + } + + -- typedef + FreeUniformIterationAlgebra : Obj → Set (suc o ⊔ suc ℓ ⊔ suc e) + FreeUniformIterationAlgebra X = FreeObject {C = C} {D = Uniform-Iteration-Algebras D} forgetfulF X + +``` + +### *Lemma 16*: definition of monad ***K*** + +```agda + record MonadK : Set (suc o ⊔ suc ℓ ⊔ suc e) where + field + algebras : ∀ X → FreeUniformIterationAlgebra X + + freeF : Functor C (Uniform-Iteration-Algebras D) + freeF = FO⇒Functor forgetfulF algebras + + adjoint : freeF ⊣ forgetfulF + adjoint = FO⇒LAdj forgetfulF algebras + + K : Monad C + K = adjoint⇒monad adjoint + + -- EilenbergMoore⇒UniformIterationAlgebras : StrongEquivalence (EilenbergMoore K) (Uniform-Iteration-Algebras D) + -- EilenbergMoore⇒UniformIterationAlgebras = {! !} +```