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

Added (pre) elgot monat

Browse source
This commit is contained in:
Leon Vatthauer 2023-08-17 18:07:26 +02:00
parent 8af4faf80c
commit 72560dfb59
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 49 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

63
Monad/ElgotMonad.agda
View file

@ -33,7 +33,8 @@ module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) w
-- with the following associativity
field
assoc : ∀ {X Y Z} (f : Z ⇒ T₀ X + Z) (h : X ⇒ T₀ Y) → elgotalgebras._# (((μ.η _ ∘ T₁ h) +₁ idC) ∘ f) ≈ (μ.η _ ∘ T₁ h) ∘ (elgotalgebras._# {X}) f
assoc : ∀ {X Y Z} (f : Z ⇒ T₀ X + Z) (h : X ⇒ T₀ Y)
→ elgotalgebras._# (((μ.η _ ∘ T₁ h) +₁ idC) ∘ f) ≈ (μ.η _ ∘ T₁ h) ∘ (elgotalgebras._# {X}) f
record PreElgotMonad : Set (o ⊔ ℓ ⊔ e) where
field
@ -49,13 +50,18 @@ module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) w
-- iteration operator
field
_† : ∀ {X Y} → X ⇒ T₀ (Y + X) → X ⇒ T₀ Y
†-resp-≈ : ∀ {X Y} {f g : X ⇒ T₀ (Y + X)} → f ≈ g → f † ≈ g †
-- laws
field
Fixpoint : ∀ {X Y} {f : X ⇒ T₀ (Y + X)} → f † ≈ (μ.η _ ∘ T₁ [ η.η _ , f † ]) ∘ f
Naturality : ∀ {X Y Z} {f : X ⇒ T₀ (Y + X)} {g : Y ⇒ T₀ Z} → (μ.η _ ∘ T₁ g) ∘ f † ≈ ((μ.η _ ∘ T₁ [ (T₁ i₁) ∘ g , η.η _ ∘ i₂ ]) ∘ f)†
Codiagonal : ∀ {X Y} {f : X ⇒ T₀ ((Y + X) + X)} → (T₁ [ idC , i₂ ] ∘ f )† ≈ f † †
Uniformity : ∀ {X Y Z} {f : X ⇒ T₀ (Y + X)} {g : Z ⇒ T₀ (Y + Z)} {h : Z ⇒ X} → f ∘ h ≈ (T₁ (idC +₁ h)) ∘ g → f † ∘ h ≈ g †
Fixpoint : ∀ {X Y} {f : X ⇒ T₀ (Y + X)}
→ f † ≈ (μ.η _ ∘ T₁ [ η.η _ , f † ]) ∘ f
Naturality : ∀ {X Y Z} {f : X ⇒ T₀ (Y + X)} {g : Y ⇒ T₀ Z}
→ (μ.η _ ∘ T₁ g) ∘ f † ≈ ((μ.η _ ∘ T₁ [ (T₁ i₁) ∘ g , η.η _ ∘ i₂ ]) ∘ f)†
Codiagonal : ∀ {X Y} {f : X ⇒ T₀ ((Y + X) + X)}
→ (T₁ [ idC , i₂ ] ∘ f )† ≈ f † †
Uniformity : ∀ {X Y Z} {f : X ⇒ T₀ (Y + X)} {g : Z ⇒ T₀ (Y + Z)} {h : Z ⇒ X}
→ f ∘ h ≈ (T₁ (idC +₁ h)) ∘ g → f † ∘ h ≈ g †
record ElgotMonad : Set (o ⊔ ℓ ⊔ e) where
field
@ -72,24 +78,51 @@ module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) w
{ elgotalgebras = λ {X} → record
{ _# = λ f → ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) †
; #-Fixpoint = λ {Y} {f} → begin
([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ≈⟨ Fixpoint ⟩
([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ≈⟨ Fixpoint ⟩
(μ.η _ ∘ T₁ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]) ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) ≈⟨ pullˡ ∘[] ⟩
[ (μ.η _ ∘ T₁ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]) ∘ T₁ i₁
, (μ.η _ ∘ T₁ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]) ∘ η.η _ ∘ i₂ ] ∘ f ≈⟨ []-cong₂ (pullʳ (sym homomorphism)) (pullˡ (pullʳ (η.sym-commute [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]))) ⟩∘⟨refl ⟩
, (μ.η _ ∘ T₁ [ η.η _
, ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]) ∘ η.η _ ∘ i₂ ] ∘ f ≈˘⟨ []-cong₂
(pushʳ (homomorphism))
(pushˡ (pushʳ (η.commute _)))
⟩∘⟨refl ⟩
[ μ.η _ ∘ T₁ ([ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ i₁)
, (μ.η _ ∘ (η.η _ ∘ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ])) ∘ i₂ ] ∘ f ≈⟨ []-cong₂ (∘-resp-≈ʳ (F-resp-≈ inject₁)) (pullʳ (pullʳ inject₂)) ⟩∘⟨refl ⟩
, (μ.η _ ∘ (η.η _ ∘ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ])) ∘ i₂ ] ∘ f ≈⟨ []-cong₂ (∘-resp-≈ʳ (F-resp-≈ inject₁)) (pullʳ (pullʳ inject₂)) ⟩∘⟨refl ⟩
[ μ.η _ ∘ (T₁ (η.η _))
, μ.η _ ∘ η.η _ ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ f ≈⟨ []-cong₂ (T.identityˡ) (cancelˡ T.identityʳ) ⟩∘⟨refl ⟩
[ idC , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ f ∎
; #-Uniformity = {! !}
; #-Folding = {! !}
; #-resp-≈ = {! !}
, μ.η _ ∘ η.η _ ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ f ≈⟨ []-cong₂ (T.identityˡ) (cancelˡ T.identityʳ) ⟩∘⟨refl ⟩
[ idC , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ f ∎
; #-Uniformity = λ {X} {Y} {f} {g} {h} H → sym (Uniformity (begin
([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ g) ∘ h ≈˘⟨ pushʳ H ⟩
[ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (idC +₁ h) ∘ f ≈⟨ pullˡ []∘+₁ ⟩
[ T₁ i₁ ∘ idC , (η.η _ ∘ i₂) ∘ h ] ∘ f ≈⟨ []-cong₂ (trans identityʳ (F-resp-≈ (sym identityʳ))) assoc ⟩∘⟨refl ⟩
[ T₁ (i₁ ∘ idC) , η.η _ ∘ i₂ ∘ h ] ∘ f ≈˘⟨ []-cong₂ (F-resp-≈ +₁∘i₁) (pullʳ +₁∘i₂) ⟩∘⟨refl ⟩
[ T₁ ((idC +₁ h) ∘ i₁) , (η.η _ ∘ (idC +₁ h)) ∘ i₂ ] ∘ f ≈⟨ []-cong₂ homomorphism ( pushˡ (η.commute _)) ⟩∘⟨refl ⟩
[ T₁ (idC +₁ h) ∘ T₁ i₁ , T₁ (idC +₁ h) ∘ η.η _ ∘ i₂ ] ∘ f ≈˘⟨ pullˡ ∘[] ⟩
T₁ (idC +₁ h) ∘ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f ∎))
; #-Folding = λ {X} {Y} {f} {h} → begin
([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ ((([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) †) +₁ h))† ≈⟨ †-resp-≈ []∘+₁ ⟩
[ T₁ i₁ ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † , (η.η _ ∘ i₂) ∘ h ] † ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
[ [ T₁ i₁ ∘ idC , (η.η _ ∘ i₂) ∘ i₁ ] ∘ f , (η.η _ ∘ i₂) ∘ h ] † ≈˘⟨ †-resp-≈ ([]-cong₂ (pullˡ []∘+₁) (pullˡ inject₂)) ⟩
[ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (idC +₁ i₁) ∘ f , [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ i₂ ∘ h ] † ≈˘⟨ †-resp-≈ ∘[] ⟩
([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])† ∎
; #-resp-≈ = λ fg → †-resp-≈ (∘-resp-≈ʳ fg)
}
; assoc = {! !}
; assoc = λ {X} {Y} {Z} f h → begin
-- TODO tidy up by moving doing sym outside, apply Naturality and then do `†-resp-≈ pullˡ` once.
([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (μ.η Y ∘ T₁ h +₁ idC) ∘ f)† ≈⟨ †-resp-≈ (pullˡ []∘+₁) ⟩
(([ T₁ i₁ ∘ μ.η _ ∘ T₁ h , (η.η _ ∘ i₂) ∘ idC ] ∘ f)†) ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-cong₂ assoc (sym identityʳ))) ⟩
([ (T₁ i₁ ∘ μ.η _) ∘ T₁ h , η.η _ ∘ i₂ ] ∘ f)† ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-congʳ (pullˡ (μ.commute _)))) ⟩
([ μ.η _ ∘ T₁ (T₁ i₁) ∘ T₁ h , η.η _ ∘ i₂ ] ∘ f)† ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ʳ homomorphism) (cancelˡ T.identityʳ))) ⟩
([ μ.η _ ∘ T₁ (T₁ i₁ ∘ h) , μ.η _ ∘ η.η _ ∘ η.η _ ∘ i₂ ] ∘ f)† ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ʳ (F-resp-≈ inject₁)) (∘-resp-≈ʳ (pullʳ inject₂)))) ⟩
([ μ.η _ ∘ T₁ ([ T₁ i₁ ∘ h , η.η _ ∘ i₂ ] ∘ i₁) , μ.η _ ∘ (η.η _ ∘ [ T₁ i₁ ∘ h , η.η _ ∘ i₂ ]) ∘ i₂ ] ∘ f)† ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-cong₂ (pullʳ (sym homomorphism)) (pullʳ (pullˡ (η.sym-commute _))))) ⟩
([ (μ.η _ ∘ T₁ [ T₁ i₁ ∘ h , η.η _ ∘ i₂ ]) ∘ T₁ i₁ , (μ.η _ ∘ T₁ [ T₁ i₁ ∘ h , η.η _ ∘ i₂ ]) ∘ η.η _ ∘ i₂ ] ∘ f)† ≈˘⟨ †-resp-≈ (pullˡ ∘[]) ⟩
((μ.η _ ∘ T₁ [ T₁ i₁ ∘ h , η.η _ ∘ i₂ ]) ∘ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f)† ≈˘⟨ Naturality ⟩
(μ.η Y ∘ T₁ h) ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f)† ∎
}
}
where
open ElgotMonad EM
module T = Monad T
open T
open T using (F; η; μ)
open Functor F renaming (F₀ to T₀; F₁ to T₁)