mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
118 lines
5.4 KiB
Markdown
118 lines
5.4 KiB
Markdown
<!--
|
||
```agda
|
||
open import Level
|
||
open import Categories.FreeObjects.Free using (FreeObject; FO⇒Functor; FO⇒LAdj)
|
||
open import Categories.Functor.Core using (Functor)
|
||
open import Categories.Adjoint using (_⊣_)
|
||
open import Categories.Adjoint.Properties using (adjoint⇒monad)
|
||
open import Categories.Monad using (Monad)
|
||
open import Categories.Monad.Relative using () renaming (Monad to RMonad)
|
||
open import Category.Ambient using (Ambient)
|
||
open import Categories.Monad.Construction.Kleisli
|
||
open import Categories.Category.Cartesian using (Cartesian)
|
||
open import Categories.Category.BinaryProducts using (BinaryProducts)
|
||
```
|
||
-->
|
||
|
||
# The Monad K
|
||
|
||
```agda
|
||
module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
|
||
open Ambient ambient
|
||
open import Category.Construction.ElgotAlgebras cocartesian
|
||
open import Algebra.Elgot cocartesian using (Elgot-Algebra)
|
||
open import Algebra.Elgot.Free cocartesian using (FreeElgotAlgebra; elgotForgetfulF)
|
||
open import Algebra.Elgot.Stable distributive using (IsStableFreeElgotAlgebra; IsStableFreeElgotAlgebraˡ; isStable⇒isStableˡ)
|
||
|
||
-- open Cartesian cartesian
|
||
-- open BinaryProducts products
|
||
|
||
open Equiv
|
||
open MR C
|
||
open M C
|
||
open HomReasoning
|
||
```
|
||
|
||
Existence of stable free Elgot algebras yields the monad K
|
||
|
||
```agda
|
||
record MonadK : Set (suc o ⊔ suc ℓ ⊔ suc e) where
|
||
field
|
||
freealgebras : ∀ X → FreeElgotAlgebra X
|
||
stable : ∀ X → IsStableFreeElgotAlgebra (freealgebras X)
|
||
|
||
-- helper for accessing elgot algebras
|
||
algebras : ∀ (X : Obj) → Elgot-Algebra
|
||
algebras X = FreeObject.FX (freealgebras X)
|
||
|
||
freeF : Functor C Elgot-Algebras
|
||
freeF = FO⇒Functor elgotForgetfulF freealgebras
|
||
|
||
adjoint : freeF ⊣ elgotForgetfulF
|
||
adjoint = FO⇒LAdj elgotForgetfulF freealgebras
|
||
|
||
monadK : Monad C
|
||
monadK = adjoint⇒monad adjoint
|
||
module monadK = Monad monadK
|
||
|
||
kleisliK : KleisliTriple C
|
||
kleisliK = Monad⇒Kleisli C monadK
|
||
module kleisliK = RMonad kleisliK
|
||
|
||
module K = Functor monadK.F
|
||
```
|
||
|
||
Some helper definitions to make our life easier
|
||
|
||
```agda
|
||
open Elgot-Algebra using (#-resp-≈; #-Fixpoint; #-Compositionality; #-Uniformity; #-Folding; #-Diamond; #-Stutter) renaming (A to ⟦_⟧) public
|
||
stableˡ = λ X → isStable⇒isStableˡ (freealgebras X) (stable X)
|
||
η = λ Z → FreeObject.η (freealgebras Z)
|
||
_♯ = λ {A X Y} f → IsStableFreeElgotAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f
|
||
_♯ˡ = λ {A X Y} f → IsStableFreeElgotAlgebraˡ.[_,_]♯ˡ {Y = X} (stableˡ X) {X = A} (algebras Y) f
|
||
_# = λ {A} {X} f → Elgot-Algebra._# (algebras A) {X = X} f
|
||
```
|
||
|
||
The kleisli star is iteration preserving:
|
||
|
||
```agda
|
||
open kleisliK using (extend)
|
||
open monadK using (μ)
|
||
|
||
extend-preserve : ∀ {X Y Z} (f : X ⇒ K.₀ Y) (h : Z ⇒ K.₀ X + Z) → extend f ∘ h # ≈ ((extend f +₁ idC) ∘ h) #
|
||
extend-preserve {X} {Y} {Z} f h = begin
|
||
(μ.η _ ∘ K.₁ f) ∘ h # ≈⟨ pullʳ (Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η _ ∘ f))) ⟩
|
||
μ.η _ ∘ ((K.₁ f +₁ idC) ∘ h) # ≈⟨ Elgot-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC) ⟩
|
||
((μ.η _ +₁ idC) ∘ (K.₁ f +₁ idC) ∘ h) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
|
||
((extend f +₁ idC) ∘ h) # ∎
|
||
```
|
||
|
||
Uniqueness of the stability operator gives us the following proof principle:
|
||
|
||
```agda
|
||
by-stability : ∀ {X Y} (A : Elgot-Algebra) {f g : X × ⟦ algebras Y ⟧ ⇒ ⟦ A ⟧} (i : X × Y ⇒ ⟦ A ⟧)
|
||
→ i ≈ f ∘ (idC ⁂ η Y)
|
||
→ i ≈ g ∘ (idC ⁂ η Y)
|
||
→ (∀ {Z} (h : Z ⇒ ⟦ algebras Y ⟧ + Z) → f ∘ (idC ⁂ (Elgot-Algebra._# (algebras Y) h)) ≈ Elgot-Algebra._# A ((f +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)))
|
||
→ (∀ {Z} (h : Z ⇒ ⟦ algebras Y ⟧ + Z) → g ∘ (idC ⁂ (Elgot-Algebra._# (algebras Y) h)) ≈ Elgot-Algebra._# A ((g +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)))
|
||
→ f ≈ g
|
||
by-stability {X} {Y} A {f} {g} i f-law g-law f-pres g-pres = begin
|
||
f ≈⟨ ♯-unique i f f-law f-pres ⟩
|
||
[ A , i ]♯ ≈⟨ sym (♯-unique i g g-law g-pres) ⟩
|
||
g ∎
|
||
where
|
||
open IsStableFreeElgotAlgebra (stable Y) using ([_,_]♯; ♯-unique)
|
||
|
||
by-stabilityˡ : ∀ {X Y} (A : Elgot-Algebra) {f g : ⟦ algebras Y ⟧ × X ⇒ ⟦ A ⟧} (i : Y × X ⇒ ⟦ A ⟧)
|
||
→ i ≈ f ∘ (η Y ⁂ idC)
|
||
→ i ≈ g ∘ (η Y ⁂ idC)
|
||
→ (∀ {Z} (h : Z ⇒ ⟦ algebras Y ⟧ + Z) → f ∘ ((Elgot-Algebra._# (algebras Y) h) ⁂ idC) ≈ Elgot-Algebra._# A ((f +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)))
|
||
→ (∀ {Z} (h : Z ⇒ ⟦ algebras Y ⟧ + Z) → g ∘ ((Elgot-Algebra._# (algebras Y) h) ⁂ idC) ≈ Elgot-Algebra._# A ((g +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)))
|
||
→ f ≈ g
|
||
by-stabilityˡ {X} {Y} A {f} {g} i f-law g-law f-pres g-pres = begin
|
||
f ≈⟨ ♯ˡ-unique i f f-law f-pres ⟩
|
||
[ A , i ]♯ˡ ≈⟨ sym (♯ˡ-unique i g g-law g-pres) ⟩
|
||
g ∎
|
||
where
|
||
open IsStableFreeElgotAlgebraˡ (stableˡ Y) using ([_,_]♯ˡ; ♯ˡ-unique)
|
||
```
|