leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

Compare commits

base: leonv:7f3351dd6cf51e01c9f91cd9f9cf3ea2f6ecbefc
Branches Tags
leonv:main
leonv:Abgabe
..
compare: leonv:230b34da49d39e09ee5b76c3c87ee38bfe2bebca
Branches Tags
leonv:main
leonv:Abgabe

No commits in common. "7f3351dd6cf51e01c9f91cd9f9cf3ea2f6ecbefc" and "230b34da49d39e09ee5b76c3c87ee38bfe2bebca" have entirely different histories.
7f3351dd6c ... 230b34da49

14 changed files with 209 additions and 324 deletions
Show stats Expand all files Collapse all files

12
Makefile
View file

@ -10,25 +10,21 @@ 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 -f Everything.agda
rm Everything.agda
rm -rf public/*
find . -name '*.agdai' -exec rm \{\} \;
open:
firefox public/Everything.html
# push compiled html to my cip directory
push: all push'
# just push without building
push':
push: all
mv public/Everything.html public/index.html
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

41
src/Algebra/Elgot/Properties.lagda.md
View file

@ -1,41 +0,0 @@
<!--
```agda
open import Level
open import Category.Instance.AmbientCategory
open import Categories.Functor
open import Categories.Monad.Relative renaming (Monad to RMonad)
```
-->
## Summary
Some properties of elgot-algebras, namely:
- Every elgot-algebra `(A, α : D₀ A ⇒ A)` satisfies `α (extend ι) ≈ α (D₁ π₁)` **[Lemma 32]**
```agda
module Algebra.Elgot.Properties {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
open import Monad.Instance.Delay ambient using (DelayM)
open import Algebra.ElgotAlgebra ambient
open Equiv
open HomReasoning
module _ {D : DelayM} (algebra : Guarded-Elgot-Algebra (DelayM.functor D)) where
open DelayM D
open Functor functor renaming (F₁ to D₁)
open RMonad kleisli
open Guarded-Elgot-Algebra algebra
commutes : α ∘ extend ι ≈ α ∘ (D₁ π₁)
commutes = {! !}
where
α∘ι : α ∘ ι ≈ π₁
α∘ι = sym (begin
π₁ ≈⟨ unique {f = idC} {g = idC} (sym project₁) (sym project₁) ⟩
universal idC idC ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
universal {! !} {! !} ≈˘⟨ unique {! !} {! !} ⟩
α ∘ ι ∎)
```

29
src/Algebra/Search.lagda.md
View file

@ -1,29 +0,0 @@
<!--
```agda
open import Level
open import Category.Instance.AmbientCategory using (Ambient)
open import Categories.Functor.Algebra
```
-->
## Summary
A *D-Algebra* `(A, α : D₀ A ⇒ A)` is called a *search-algebra* if it satiesfies
- α now ≈ id
- α ▷ ≈ α
## Code
```agda
module Algebra.Search {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
open import Monad.Instance.Delay ambient using (DelayM)
module _ (D : DelayM) where
open DelayM D
record IsSearchAlgebra (algebra : F-Algebra functor) : Set e where
open F-Algebra algebra using (A; α)
field
identity₁ : α ∘ now ≈ idC
identity₂ : α ∘ ▷ ≈ α
```

57
src/Category/Instance/AmbientCategory.lagda.md
View file

@ -1,57 +0,0 @@
<!--
```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'
```

2
src/Misc/Coalgebra.lagda.md → src/Coalgebra.lagda.md
View file

@ -1,7 +1,7 @@
## Coproducts in the category of Coalgebras (needs proper imports to be compiled)
```agda
module Misc.Coalgebra where
module Coalgebra where
```
Coalg-cop : (F : Endofunctor C) → (alg₁ : F-Coalgebra F) → (alg₂ : F-Coalgebra F) → Coproduct (F-Coalgebras F) alg₁ alg₂

82
src/Algebra/ElgotAlgebra.lagda.md → src/ElgotAlgebra.lagda.md
View file

@ -3,7 +3,13 @@
open import Level
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Algebra
open import Category.Instance.AmbientCategory using (Ambient)
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
```
-->
@ -17,38 +23,43 @@ This file introduces (guarded) elgot algebras
## Code
```agda
module Algebra.ElgotAlgebra {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
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)
open MR C
```
### *Definition 7* Guarded Elgot Algebras
```agda
record Guarded-Elgot-Algebra-on {F : Endofunctor C} (FA : F-Algebra F) : Set (o ⊔ ℓ ⊔ e) where
open Functor F public
open F-Algebra FA public
-- iteration operator
field
_# : ∀ {X} → (X ⇒ A + F₀ X) → (X ⇒ A)
module _ {F : Endofunctor C} (FA : F-Algebra F) where
record Guarded-Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where
open Functor F public
open F-Algebra FA public
-- iteration operator
field
_# : ∀ {X} → (X ⇒ A + F₀ X) → (X ⇒ A)
-- _# properties
field
#-Fixpoint : ∀ {X} {f : X ⇒ A + F₀ X }
→ f # ≈ [ idC , α ∘ F₁ (f #) ] ∘ f
#-Uniformity : ∀ {X Y} {f : X ⇒ A + F₀ X} {g : Y ⇒ A + F₀ Y} {h : X ⇒ Y}
→ (idC +₁ F₁ h) ∘ f ≈ g ∘ h
→ f # ≈ g # ∘ h
#-Compositionality : ∀ {X Y} {f : X ⇒ A + F₀ X} {h : Y ⇒ X + F₀ Y}
→ (((f #) +₁ idC) ∘ h)# ≈ ([ (idC +₁ (F₁ i₁)) ∘ f , i₂ ∘ (F₁ i₂) ] ∘ [ i₁ , h ])# ∘ i₂
#-resp-≈ : ∀ {X} {f g : X ⇒ A + F₀ X}
→ f ≈ g
→ (f #) ≈ (g #)
-- _# properties
field
#-Fixpoint : ∀ {X} {f : X ⇒ A + F₀ X }
→ f # ≈ [ idC , α ∘ F₁ (f #) ] ∘ f
#-Uniformity : ∀ {X Y} {f : X ⇒ A + F₀ X} {g : Y ⇒ A + F₀ Y} {h : X ⇒ Y}
→ (idC +₁ F₁ h) ∘ f ≈ g ∘ h
→ f # ≈ g # ∘ h
#-Compositionality : ∀ {X Y} {f : X ⇒ A + F₀ X} {h : Y ⇒ X + F₀ Y}
→ (((f #) +₁ idC) ∘ h)# ≈ ([ (idC +₁ (F₁ i₁)) ∘ f , i₂ ∘ (F₁ i₂) ] ∘ [ i₁ , h ])# ∘ i₂
#-resp-≈ : ∀ {X} {f g : X ⇒ A + F₀ X}
→ f ≈ g
→ (f #) ≈ (g #)
record Guarded-Elgot-Algebra (F : Endofunctor C) : Set (o ⊔ ℓ ⊔ e) where
field
algebra : F-Algebra F
guarded-elgot-algebra-on : Guarded-Elgot-Algebra-on algebra
open Guarded-Elgot-Algebra-on guarded-elgot-algebra-on public
```
### *Proposition 10* Unguarded Elgot Algebras
@ -140,16 +151,13 @@ Here we give a different Characterization and show that it is equal.
where open Functor (idF {C = C})
-- constructing an Id-Guarded Elgot-Algebra from an unguarded one
Unguarded→Id-Guarded : (EA : Elgot-Algebra) → Guarded-Elgot-Algebra idF
Unguarded→Id-Guarded : (EA : Elgot-Algebra) → Guarded-Elgot-Algebra (Id-Algebra (Elgot-Algebra.A EA))
Unguarded→Id-Guarded ea = record
{ algebra = Id-Algebra A
; guarded-elgot-algebra-on = record
{ _# = _#
; #-Fixpoint = λ {X} {f} → trans #-Fixpoint (sym (∘-resp-≈ˡ ([]-congˡ identityˡ)))
; #-Uniformity = #-Uniformity
; #-Compositionality = #-Compositionality
; #-resp-≈ = #-resp-≈
}
{ _# = _#
; #-Fixpoint = λ {X} {f} → trans #-Fixpoint (sym (∘-resp-≈ˡ ([]-congˡ identityˡ)))
; #-Uniformity = #-Uniformity
; #-Compositionality = #-Compositionality
; #-resp-≈ = #-resp-≈
}
where
open Elgot-Algebra ea
@ -157,7 +165,7 @@ Here we give a different Characterization and show that it is equal.
open Equiv
-- constructing an unguarded Elgot-Algebra from an Id-Guarded one
Id-Guarded→Unguarded : ∀ {A} → Guarded-Elgot-Algebra-on (Id-Algebra A) → Elgot-Algebra
Id-Guarded→Unguarded : ∀ {A : Obj} → Guarded-Elgot-Algebra (Id-Algebra A) → Elgot-Algebra
Id-Guarded→Unguarded gea = record
{ A = A
; algebra = record
@ -173,7 +181,7 @@ Here we give a different Characterization and show that it is equal.
}
}
where
open Guarded-Elgot-Algebra-on gea
open Guarded-Elgot-Algebra gea
open HomReasoning
open Equiv
left : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y}

34
src/Category/Construction/ElgotAlgebras.lagda.md → src/ElgotAlgebras.lagda.md
View file

@ -11,10 +11,12 @@ 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
open import Category.Instance.AmbientCategory using (Ambient)
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
```
-->
@ -28,9 +30,17 @@ This file introduces the category of *unguarded* elgot algebras
## Code
```agda
module Category.Construction.ElgotAlgebras {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
open import Algebra.ElgotAlgebra ambient
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
open M C
open MR C
open HomReasoning
@ -42,7 +52,7 @@ module Category.Construction.ElgotAlgebras {o ℓ e} (ambient : Ambient o ℓ e)
```agda
-- iteration preversing morphism between two elgot-algebras
module _ (E₁ E₂ : Elgot-Algebra) where
module _ (E₁ E₂ : Elgot-Algebra D) where
open Elgot-Algebra E₁ renaming (_# to _#₁)
open Elgot-Algebra E₂ renaming (_# to _#₂; A to B)
record Elgot-Algebra-Morphism : Set (o ⊔ ℓ ⊔ e) where
@ -53,7 +63,7 @@ module Category.Construction.ElgotAlgebras {o ℓ e} (ambient : Ambient o ℓ e)
-- the category of elgot algebras for a given category
Elgot-Algebras : Category (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) e
Elgot-Algebras = record
{ Obj = Elgot-Algebra
{ Obj = Elgot-Algebra D
; _⇒_ = Elgot-Algebra-Morphism
; _≈_ = λ f g → Elgot-Algebra-Morphism.h f ≈ Elgot-Algebra-Morphism.h g
; id = λ {EB} → let open Elgot-Algebra EB in
@ -112,7 +122,7 @@ module Category.Construction.ElgotAlgebras {o ℓ e} (ambient : Ambient o ℓ e)
open Terminal T
-- if the carriers of the algebra form a product, so do the algebras
A×B-Helper : ∀ {EA EB : Elgot-Algebra} → Elgot-Algebra
A×B-Helper : ∀ {EA EB : Elgot-Algebra D} → Elgot-Algebra D
A×B-Helper {EA} {EB} = record
{ A = A × B
; algebra = record
@ -121,7 +131,7 @@ module Category.Construction.ElgotAlgebras {o ℓ e} (ambient : Ambient o ℓ e)
⟨ ((π₁ +₁ 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₁)) ⟩
@ -134,7 +144,7 @@ module Category.Construction.ElgotAlgebras {o ℓ e} (ambient : Ambient o ℓ e)
π₂ ∘ [ 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
@ -182,7 +192,7 @@ module Category.Construction.ElgotAlgebras {o ℓ e} (ambient : Ambient o ℓ e)
[ (idC +₁ i₁) ∘ ((π₂ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵇ ≈⟨ #ᵇ-resp-≈ (+₁-id-swap π₂) ⟩
((π₂ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ ∎
Product-Elgot-Algebras : ∀ (EA EB : Elgot-Algebra) → Product Elgot-Algebras EA EB
Product-Elgot-Algebras : ∀ (EA EB : Elgot-Algebra D) → Product Elgot-Algebras EA EB
Product-Elgot-Algebras EA EB = record
{ A×B = A×B-Helper {EA} {EB}
; π₁ = record { h = π₁ ; preserves = λ {X} {f} → project₁ }
@ -199,7 +209,7 @@ module Category.Construction.ElgotAlgebras {o ℓ e} (ambient : Ambient o ℓ e)
⟨ ((π₁ +₁ 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-≈)
@ -219,7 +229,7 @@ module Category.Construction.ElgotAlgebras {o ℓ e} (ambient : Ambient o ℓ e)
```agda
-- if the carriers of the algebra form a exponential, so do the algebras
B^A-Helper : ∀ {EA : Elgot-Algebra} {X : Obj} → Exponential C X (Elgot-Algebra.A EA) → Elgot-Algebra
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
; algebra = record

5
src/Misc/FinalCoalgebras.lagda.md → src/FinalCoalgebras.lagda.md
View file

@ -1,6 +1,3 @@
I thought briefly that I needed this, but I don't.
Might still be interesting!
```agda
open import Level
open import Categories.Category
@ -8,7 +5,7 @@ open import Categories.Functor
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
module Misc.FinalCoalgebras {o ℓ e} {C : Category o ℓ e} (F : Endofunctor C) where
module 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

20
src/Monad/ElgotMonad.lagda.md
View file

@ -3,9 +3,17 @@
{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Category.Instance.AmbientCategory using (Ambient)
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 Categories.Monad
open import Categories.Functor
open import ElgotAlgebra
import Categories.Morphism.Reasoning as MR
```
-->
@ -21,12 +29,14 @@ This file introduces Elgot Monads.
## Code
```agda
module Monad.ElgotMonad {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
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
@ -38,7 +48,7 @@ module Monad.ElgotMonad {o ℓ e} (ambient : Ambient o ℓ e) where
-- every TX needs to be equipped with an elgot algebra structure
field
elgotalgebras : ∀ {X} → Elgot-Algebra-on (T₀ X)
elgotalgebras : ∀ {X} → Elgot-Algebra-on ED (T₀ X)
module elgotalgebras {X} = Elgot-Algebra-on (elgotalgebras {X})

181
src/Monad/Instance/Delay.lagda.md
View file

@ -3,7 +3,16 @@
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
@ -11,7 +20,10 @@ open import Categories.Functor
open import Categories.Functor.Algebra
open import Categories.Monad.Construction.Kleisli
open import Categories.Category.Construction.F-Coalgebras
open import Category.Instance.AmbientCategory using (Ambient)
open import Categories.NaturalTransformation
open import FinalCoalgebras
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
```
-->
@ -21,11 +33,19 @@ This file introduces the delay monad ***D***
## Code
```agda
module Monad.Instance.Delay {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
```
<!--
```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
@ -55,9 +75,11 @@ We can now define these functions by bisecting the isomorphism `out : DX ≅ X +
```agda
module _ {X : Obj} where
module _ (X : Obj) where
open Terminal (coalgebras X) using (⊤; !; !-unique)
open F-Coalgebra ⊤ using () renaming (A to DX) public
open F-Coalgebra ⊤ renaming (A to DX)
D₀ = DX
out-≅ : DX ≅ X + DX
out-≅ = colambek {F = X +- } (coalgebras X)
@ -71,12 +93,8 @@ We can now define these functions by bisecting the isomorphism `out : DX ≅ X +
later : DX ⇒ DX
later = out⁻¹ ∘ i₂
-- convenient notation
▷ = later
unitlaw : out ∘ now ≈ i₁
unitlaw = cancelˡ (_≅_.isoʳ out-≅)
```
Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use our terminal coalgebras to get a *coiteration operator* `coit`:
@ -97,17 +115,14 @@ At the same time the morphism `X × N ⇒ X + X × N` is a coalgebra for the `(Y
TODO add diagram
```agda
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 })
module _ (ℕ : ParametrizedNNO) where
open ParametrizedNNO ℕ
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 }})
```
Make `DX` conveniently accessible
```agda
D₀ : Obj → Obj
D₀ X = DX {X}
ι : 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)`.
@ -117,22 +132,23 @@ TODO
```agda
kleisli : KleisliTriple C
kleisli = record
monad : Monad C
monad = Kleisli⇒Monad C (record
{ F₀ = D₀
; unit = now
; unit = λ {X} → now X
; extend = extend
; identityʳ = identityʳ'
; identityˡ = identityˡ'
; assoc = assoc'
; sym-assoc = sym assoc'
; extend-≈ = extend-≈'
}
})
where
open Terminal
module _ {X Y : Obj} (f : X ⇒ D₀ Y) where
alg : F-Coalgebra (Y +-)
alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out , (idC +₁ i₂) ∘ out ] }
alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X , (idC +₁ i₂) ∘ out Y ] }
extend : D₀ X ⇒ D₀ Y
extend = u (! (coalgebras Y) {A = alg}) ∘ i₁ {B = D₀ Y}
@ -140,39 +156,39 @@ TODO
!∘i₂ : u (! (coalgebras Y) {A = alg}) ∘ i₂ ≈ idC
!∘i₂ = ⊤-id (coalgebras Y) (F-Coalgebras (Y +-) [ ! (coalgebras Y) ∘ record { f = i₂ ; commutes = inject₂ } ] )
extendlaw : out ∘ extend ≈ [ out ∘ f , i₂ ∘ extend ] ∘ out
extendlaw : out Y ∘ extend ≈ [ out Y ∘ f , i₂ ∘ extend ] ∘ out X
extendlaw = begin
out ∘ extend ≈⟨ pullˡ (commutes (! (coalgebras Y) {A = alg})) ⟩
out Y ∘ extend ≈⟨ pullˡ (commutes (! (coalgebras Y) {A = alg})) ⟩
((idC +₁ (u (! (coalgebras Y)))) ∘ α alg) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩
(idC +₁ (u (! (coalgebras Y)))) ∘ [ [ i₁ , i₂ ∘ i₂ ]
∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out ≈⟨ pullˡ ∘[] ⟩
[ (idC +₁ (u (! (coalgebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f)
, (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩
∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩
[ (idC +₁ (u (! (coalgebras Y)))) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f)
, (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl ⟩
[ [ (idC +₁ (u (! (coalgebras Y)))) ∘ i₁
, (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out ∘ f)
, (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out ≈⟨ ([]-cong₂
, (idC +₁ (u (! (coalgebras Y)))) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f)
, (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂
(([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl)
refl) ⟩∘⟨refl ⟩
[ [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₂ ] ∘ (out ∘ f)
, (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out ≈⟨ ([]-cong₂
[ [ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₂ ] ∘ (out Y ∘ f)
, (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out X ≈⟨ ([]-cong₂
(elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η))
assoc) ⟩∘⟨refl ⟩
[ out ∘ f , i₂ ∘ extend ] ∘ out ∎
[ out Y ∘ f , i₂ ∘ extend ] ∘ out X ∎
extend-unique : (g : D₀ X ⇒ D₀ Y) → (out ∘ g ≈ [ out ∘ f , i₂ ∘ g ] ∘ out) → extend ≈ g
extend-unique : (g : D₀ X ⇒ D₀ Y) → (out Y ∘ g ≈ [ out Y ∘ f , i₂ ∘ g ] ∘ out X) → extend ≈ g
extend-unique g g-commutes = begin
extend ≈⟨ (!-unique (coalgebras Y) (record { f = [ g , idC ] ; commutes = begin
out ∘ [ g , idC ] ≈⟨ ∘[] ⟩
[ out ∘ g , out ∘ idC ] ≈⟨ []-cong₂ g-commutes identityʳ ⟩
[ [ out ∘ f , i₂ ∘ g ] ∘ out , out ] ≈˘⟨ []-cong₂
out Y ∘ [ g , idC ] ≈⟨ ∘[] ⟩
[ out Y ∘ g , out Y ∘ idC ] ≈⟨ []-cong₂ g-commutes identityʳ ⟩
[ [ out Y ∘ f , i₂ ∘ g ] ∘ out X , out Y ] ≈˘⟨ []-cong₂
(([]-cong₂
(([]-cong₂ refl identityʳ) ⟩∘⟨refl ○ (elimˡ +-η))
refl)
⟩∘⟨refl)
refl ⟩
[ [ [ i₁ , i₂ ∘ idC ] ∘ (out ∘ f)
, i₂ ∘ g ] ∘ out
, out ] ≈˘⟨ []-cong₂
[ [ [ i₁ , i₂ ∘ idC ] ∘ (out Y ∘ f)
, i₂ ∘ g ] ∘ out X
, out Y ] ≈˘⟨ []-cong₂
(([]-cong₂
(([]-cong₂ identityʳ (pullʳ inject₂)) ⟩∘⟨refl)
refl)
@ -180,9 +196,9 @@ TODO
refl
⟩
[ [ [ i₁ ∘ idC
, (i₂ ∘ [ g , idC ]) ∘ i₂ ] ∘ (out ∘ f)
, i₂ ∘ g ] ∘ out
, out ] ≈˘⟨ []-cong₂
, (i₂ ∘ [ g , idC ]) ∘ i₂ ] ∘ (out Y ∘ f)
, i₂ ∘ g ] ∘ out X
, out Y ] ≈˘⟨ []-cong₂
(([]-cong₂
(([]-cong₂ +₁∘i₁ (pullˡ +₁∘i₂)) ⟩∘⟨refl)
(pullʳ inject₁))
@ -190,16 +206,16 @@ TODO
(elimˡ (Functor.identity (Y +-)))
⟩
[ [ [ (idC +₁ [ g , idC ]) ∘ i₁
, (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₂ ] ∘ (out ∘ f)
, (i₂ ∘ [ g , idC ]) ∘ i₁ ] ∘ out
, (idC +₁ idC) ∘ out ] ≈˘⟨ []-cong₂
, (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₂ ] ∘ (out Y ∘ f)
, (i₂ ∘ [ g , idC ]) ∘ i₁ ] ∘ out X
, (idC +₁ idC) ∘ out Y ] ≈˘⟨ []-cong₂
(([]-cong₂ (pullˡ ∘[]) (pullˡ +₁∘i₂)) ⟩∘⟨refl)
((+₁-cong₂ identity² inject₂) ⟩∘⟨refl) ⟩
[ [ (idC +₁ [ g , idC ]) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f)
, (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₁ ] ∘ out
, (idC ∘ idC +₁ [ g , idC ] ∘ i₂) ∘ out ] ≈˘⟨ []-cong₂ (pullˡ ∘[]) (pullˡ +₁∘+₁) ⟩
[ (idC +₁ [ g , idC ]) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out
, (idC +₁ [ g , idC ]) ∘ (idC +₁ i₂) ∘ out ] ≈˘⟨ ∘[] ⟩
[ [ (idC +₁ [ g , idC ]) ∘ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f)
, (idC +₁ [ g , idC ]) ∘ i₂ ∘ i₁ ] ∘ out X
, (idC ∘ idC +₁ [ g , idC ] ∘ i₂) ∘ out Y ] ≈˘⟨ []-cong₂ (pullˡ ∘[]) (pullˡ +₁∘+₁) ⟩
[ (idC +₁ [ g , idC ]) ∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out Y ∘ f) , i₂ ∘ i₁ ] ∘ out X
, (idC +₁ [ g , idC ]) ∘ (idC +₁ i₂) ∘ out Y ] ≈˘⟨ ∘[] ⟩
(idC +₁ [ g , idC ]) ∘ α alg ∎ })) ⟩∘⟨refl ⟩
[ g , idC ] ∘ i₁ ≈⟨ inject₁ ⟩
g ∎
@ -226,38 +242,38 @@ TODO
}
where open Functor (Y +-) using (identity)
identityʳ' : ∀ {X Y : Obj} {f : X ⇒ D₀ Y} → extend f ∘ now {X} ≈ f
identityʳ' : ∀ {X} {Y} {f} → extend f ∘ now X ≈ f
identityʳ' {X} {Y} {f} = begin
extend f ∘ now ≈⟨ insertˡ (_≅_.isoˡ out-≅) ⟩∘⟨refl ⟩
(out⁻¹ ∘ out ∘ extend f) ∘ now ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩
(out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend f ] ∘ out) ∘ now ≈⟨ pullʳ (pullʳ unitlaw) ⟩
out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend f ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩
out⁻¹ ∘ out ∘ f ≈⟨ cancelˡ (_≅_.isoˡ out-≅) ⟩
extend f ∘ now X ≈⟨ insertˡ (_≅_.isoˡ (out-≅ Y)) ⟩∘⟨refl ⟩
(out⁻¹ Y ∘ out Y ∘ extend f) ∘ now X ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩
(out⁻¹ Y ∘ [ out Y ∘ f , i₂ ∘ extend f ] ∘ out X) ∘ now X ≈⟨ pullʳ (pullʳ (unitlaw X)) ⟩
out⁻¹ Y ∘ [ out Y ∘ f , i₂ ∘ extend f ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩
out⁻¹ Y ∘ out Y ∘ f ≈⟨ cancelˡ (_≅_.isoˡ (out-≅ Y)) ⟩
f ∎
identityˡ' : ∀ {X} → extend now ≈ idC
identityˡ' {X} = Terminal.⊤-id (coalgebras X) (record { f = extend now ; commutes = begin
out ∘ extend now ≈⟨ pullˡ ((commutes (! (coalgebras X) {A = alg now}))) ⟩
((idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ α (alg now)) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩
(idC +₁ (u (! (coalgebras X) {A = alg now})))
∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ now) , i₂ ∘ i₁ ] ∘ out ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw) ○ inject₁) refl ⟩∘⟨refl ⟩
(idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out ≈⟨ pullˡ ∘[] ⟩
[ (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ i₁
, (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ i₂ ∘ i₁ ] ∘ out ≈⟨ []-cong₂ +₁∘i₁ (pullˡ +₁∘i₂) ⟩∘⟨refl ⟩
[ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras X) {A = alg now}))) ∘ i₁ ] ∘ out ≈⟨ []-cong₂ refl assoc ⟩∘⟨refl ⟩
[ i₁ ∘ idC , i₂ ∘ (extend now) ] ∘ out ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
([ i₁ , i₂ ] ∘ (idC +₁ extend now)) ∘ out ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩
(idC +₁ extend now) ∘ out ∎ })
identityˡ' : ∀ {X} → extend (now X) ≈ idC
identityˡ' {X} = Terminal.⊤-id (coalgebras X) (record { f = extend (now X) ; commutes = begin
out X ∘ extend (now X) ≈⟨ pullˡ ((commutes (! (coalgebras X) {A = alg (now X)}))) ⟩
((idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ α (alg (now X))) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩
(idC +₁ (u (! (coalgebras X) {A = alg (now X)})))
∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out X ∘ (now X)) , i₂ ∘ i₁ ] ∘ out X ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw X) ○ inject₁) refl ⟩∘⟨refl ⟩
(idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ [ i₁ , i₂ ∘ i₁ ] ∘ out X ≈⟨ pullˡ ∘[] ⟩
[ (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ i₁
, (idC +₁ (u (! (coalgebras X) {A = alg (now X)}))) ∘ i₂ ∘ i₁ ] ∘ out X ≈⟨ []-cong₂ +₁∘i₁ (pullˡ +₁∘i₂) ⟩∘⟨refl ⟩
[ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras X) {A = alg (now X)}))) ∘ i₁ ] ∘ out X ≈⟨ []-cong₂ refl assoc ⟩∘⟨refl ⟩
[ i₁ ∘ idC , i₂ ∘ (extend (now X)) ] ∘ out X ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
([ i₁ , i₂ ] ∘ (idC +₁ extend (now X))) ∘ out X ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩
(idC +₁ extend (now X)) ∘ out X ∎ })
assoc' : ∀ {X Y Z : Obj} {g : X ⇒ D₀ Y} {h : Y ⇒ D₀ Z} → extend (extend h ∘ g) ≈ extend h ∘ extend g
assoc' : ∀ {X} {Y} {Z} {g} {h} → extend (extend h ∘ g) ≈ extend h ∘ extend g
assoc' {X} {Y} {Z} {g} {h} = extend-unique (extend h ∘ g) (extend h ∘ extend g) (begin
out ∘ extend h ∘ extend g ≈⟨ pullˡ (extendlaw h) ⟩
([ out ∘ h , i₂ ∘ extend h ] ∘ out) ∘ extend g ≈⟨ pullʳ (extendlaw g) ⟩
[ out ∘ h , i₂ ∘ extend h ] ∘ [ out ∘ g , i₂ ∘ extend g ] ∘ out ≈⟨ pullˡ ∘[] ⟩
[ [ out ∘ h , i₂ ∘ extend h ] ∘ out ∘ g
, [ out ∘ h , i₂ ∘ extend h ] ∘ i₂ ∘ extend g ] ∘ out ≈⟨ []-cong₂ (pullˡ (⟺ (extendlaw h))) (pullˡ inject₂) ⟩∘⟨refl ⟩
[ (out ∘ extend h) ∘ g , (i₂ ∘ extend h) ∘ extend g ] ∘ out ≈⟨ ([]-cong₂ assoc assoc) ⟩∘⟨refl ⟩
[ out ∘ extend h ∘ g , i₂ ∘ extend h ∘ extend g ] ∘ out ∎)
out Z ∘ extend h ∘ extend g ≈⟨ pullˡ (extendlaw h) ⟩
([ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y) ∘ extend g ≈⟨ pullʳ (extendlaw g) ⟩
[ out Z ∘ h , i₂ ∘ extend h ] ∘ [ out Y ∘ g , i₂ ∘ extend g ] ∘ out X ≈⟨ pullˡ ∘[] ⟩
[ [ out Z ∘ h , i₂ ∘ extend h ] ∘ out Y ∘ g
, [ out Z ∘ h , i₂ ∘ extend h ] ∘ i₂ ∘ extend g ] ∘ out X ≈⟨ []-cong₂ (pullˡ (⟺ (extendlaw h))) (pullˡ inject₂) ⟩∘⟨refl ⟩
[ (out Z ∘ extend h) ∘ g , (i₂ ∘ extend h) ∘ extend g ] ∘ out X ≈⟨ ([]-cong₂ assoc assoc) ⟩∘⟨refl ⟩
[ out Z ∘ extend h ∘ g , i₂ ∘ extend h ∘ extend g ] ∘ out X ∎)
extend-≈' : ∀ {X} {Y} {f g : X ⇒ D₀ Y} → f ≈ g → extend f ≈ extend g
extend-≈' {X} {Y} {f} {g} eq = begin
@ -269,13 +285,6 @@ 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

27
src/Monad/Instance/Delay/Quotienting.lagda.md
View file

@ -1,27 +0,0 @@
<!--
```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
```

17
src/Monad/Instance/K.lagda.md → src/MonadK.lagda.md
View file

@ -1,8 +1,12 @@
<!--
```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
@ -12,7 +16,6 @@ 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)
```
-->
@ -31,15 +34,13 @@ In this file I explore the monad ***K*** and its properties:
## Code
```agda
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
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 C
forgetfulF : Functor (Uniform-Iteration-Algebras D) C
forgetfulF = record
{ F₀ = λ X → Uniform-Iteration-Algebra.A X
; F₁ = λ f → Uniform-Iteration-Algebra-Morphism.h f
@ -50,7 +51,7 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
-- typedef
FreeUniformIterationAlgebra : Obj → Set (suc o ⊔ suc ℓ ⊔ suc e)
FreeUniformIterationAlgebra X = FreeObject {C = C} {D = Uniform-Iteration-Algebras} forgetfulF X
FreeUniformIterationAlgebra X = FreeObject {C = C} {D = Uniform-Iteration-Algebras D} forgetfulF X
```
@ -61,7 +62,7 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
field
algebras : ∀ X → FreeUniformIterationAlgebra X
freeF : Functor C Uniform-Iteration-Algebras
freeF : Functor C (Uniform-Iteration-Algebras D)
freeF = FO⇒Functor forgetfulF algebras
adjoint : freeF ⊣ forgetfulF

10
src/Algebra/UniformIterationAlgebra.lagda.md → src/UniformIterationAlgebra.lagda.md
View file

@ -1,7 +1,10 @@
<!--
```agda
open import Level
open import Category.Instance.AmbientCategory using (Ambient)
open import Categories.Category.Core
open import Categories.Category.Extensive.Bundle
open import Categories.Category.Extensive
open import Categories.Category.Cocartesian
```
-->
## Summary
@ -12,8 +15,9 @@ This file introduces *Uniform-Iteration Algebras*
## Code
```agda
module Algebra.UniformIterationAlgebra {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
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

16
src/Category/Construction/UniformIterationAlgebras.lagda.md → src/UniformIterationAlgebras.lagda.md
View file

@ -2,7 +2,11 @@
```agda
open import Level
open import Categories.Category.Core
open import Category.Instance.AmbientCategory using (Ambient)
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
```
-->
@ -14,9 +18,9 @@ This file introduces the category of Uniform-Iteration Algebras
## Code
```agda
module Category.Construction.UniformIterationAlgebras {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
open import Algebra.UniformIterationAlgebra ambient
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
@ -26,7 +30,7 @@ module Category.Construction.UniformIterationAlgebras {o ℓ e} (ambient : Ambie
```agda
-- iteration preversing morphism between two elgot-algebras
module _ (E₁ E₂ : Uniform-Iteration-Algebra) where
module _ (E₁ E₂ : Uniform-Iteration-Algebra D) 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
@ -37,7 +41,7 @@ module Category.Construction.UniformIterationAlgebras {o ℓ e} (ambient : Ambie
-- 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
{ Obj = Uniform-Iteration-Algebra D
; _⇒_ = 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