From 481e1011e5bfcd3bf3634ddda4e2189e175e949c Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Tue, 12 Sep 2023 16:03:20 +0200 Subject: [PATCH] =?UTF-8?q?=F0=9F=94=A8=20refactor=20folder=20structure,?= =?UTF-8?q?=20define=20ambient=20category=20and=20use=20throughout?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Makefile | 12 ++-- src/{ => Algebra}/ElgotAlgebra.lagda.md | 21 +------ .../UniformIterationAlgebra.lagda.md | 10 +--- .../Construction}/ElgotAlgebras.lagda.md | 34 ++++------- .../UniformIterationAlgebras.lagda.md | 16 ++---- .../Instance/AmbientCategory.lagda.md | 57 +++++++++++++++++++ src/{ => Misc}/Coalgebra.lagda.md | 2 +- src/{ => Misc}/FinalCoalgebras.lagda.md | 5 +- src/Monad/ElgotMonad.lagda.md | 20 ++----- src/Monad/Instance/Delay.lagda.md | 51 ++++++----------- src/Monad/Instance/Delay/Quotienting.lagda.md | 27 +++++++++ .../Instance/K.lagda.md} | 17 +++--- 12 files changed, 151 insertions(+), 121 deletions(-) rename src/{ => Algebra}/ElgotAlgebra.lagda.md (95%) rename src/{ => Algebra}/UniformIterationAlgebra.lagda.md (70%) rename src/{ => Category/Construction}/ElgotAlgebras.lagda.md (94%) rename src/{ => Category/Construction}/UniformIterationAlgebras.lagda.md (83%) create mode 100644 src/Category/Instance/AmbientCategory.lagda.md rename src/{ => Misc}/Coalgebra.lagda.md (98%) rename src/{ => Misc}/FinalCoalgebras.lagda.md (92%) create mode 100644 src/Monad/Instance/Delay/Quotienting.lagda.md rename src/{MonadK.lagda.md => Monad/Instance/K.lagda.md} (82%) diff --git a/Makefile b/Makefile index 02aca67..f2a2a0f 100644 --- a/Makefile +++ b/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 diff --git a/src/ElgotAlgebra.lagda.md b/src/Algebra/ElgotAlgebra.lagda.md similarity index 95% rename from src/ElgotAlgebra.lagda.md rename to src/Algebra/ElgotAlgebra.lagda.md index 127b0f2..d9234ea 100644 --- a/src/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 ``` diff --git a/src/UniformIterationAlgebra.lagda.md b/src/Algebra/UniformIterationAlgebra.lagda.md similarity index 70% rename from src/UniformIterationAlgebra.lagda.md rename to src/Algebra/UniformIterationAlgebra.lagda.md index 46b7892..6033409 100644 --- a/src/UniformIterationAlgebra.lagda.md +++ b/src/Algebra/UniformIterationAlgebra.lagda.md @@ -1,10 +1,7 @@ ## 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 diff --git a/src/ElgotAlgebras.lagda.md b/src/Category/Construction/ElgotAlgebras.lagda.md similarity index 94% rename from src/ElgotAlgebras.lagda.md rename to src/Category/Construction/ElgotAlgebras.lagda.md index 9b143db..cb16b80 100644 --- a/src/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 diff --git a/src/UniformIterationAlgebras.lagda.md b/src/Category/Construction/UniformIterationAlgebras.lagda.md similarity index 83% rename from src/UniformIterationAlgebras.lagda.md rename to src/Category/Construction/UniformIterationAlgebras.lagda.md index 43fe151..0bad10f 100644 --- a/src/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 diff --git a/src/Category/Instance/AmbientCategory.lagda.md b/src/Category/Instance/AmbientCategory.lagda.md new file mode 100644 index 0000000..f4ef477 --- /dev/null +++ b/src/Category/Instance/AmbientCategory.lagda.md @@ -0,0 +1,57 @@ + + +## 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' +``` \ No newline at end of file diff --git a/src/Coalgebra.lagda.md b/src/Misc/Coalgebra.lagda.md similarity index 98% rename from src/Coalgebra.lagda.md rename to src/Misc/Coalgebra.lagda.md index ead010d..79000ea 100644 --- a/src/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₂ diff --git a/src/FinalCoalgebras.lagda.md b/src/Misc/FinalCoalgebras.lagda.md similarity index 92% rename from src/FinalCoalgebras.lagda.md rename to src/Misc/FinalCoalgebras.lagda.md index afbfa6b..d7f173c 100644 --- a/src/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 diff --git a/src/Monad/ElgotMonad.lagda.md b/src/Monad/ElgotMonad.lagda.md index 96f94e9..01b7aaa 100644 --- 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}) diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md index d59f297..c1e0b46 100644 --- 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 +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 +``` \ No newline at end of file diff --git a/src/MonadK.lagda.md b/src/Monad/Instance/K.lagda.md similarity index 82% rename from src/MonadK.lagda.md rename to src/Monad/Instance/K.lagda.md index 6749755..fc29a53 100644 --- a/src/MonadK.lagda.md +++ b/src/Monad/Instance/K.lagda.md @@ -1,12 +1,8 @@ @@ -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