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

Add category of pre-Elgot monads

Browse source
This commit is contained in:
Leon Vatthauer 2023-11-15 14:34:30 +01:00
parent 344e08fc53
commit bac3d12e52
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 20 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
src/Category/Construction/PreElgotMonads.lagda.md
View file

@ -41,20 +41,20 @@ module _ (P S : PreElgotMonad) where
α-μ : ∀ {X}
→ α.η X ∘ TP.μ.η X ≈ TS.μ.η X ∘ TS.F.₁ (α.η X) ∘ α.η (TP.F.₀ X)
PreElgotMonads : Category {!!} {!!} {!!}
PreElgotMonads : Category (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) (o ⊔ e)
PreElgotMonads = record
{ Obj = PreElgotMonad
; _⇒_ = PreElgotMonad-Morphism
; _≈_ = λ f g → (PreElgotMonad-Morphism.α f) ≃ (PreElgotMonad-Morphism.α g)
; id = id'
; _∘_ = {!!}
; assoc = {!!}
; sym-assoc = {!!}
; identityˡ = {!!}
; identityʳ = {!!}
; identity² = {!!}
; equiv = {!!}
; ∘-resp-≈ = {!!}
; _∘_ = _∘'_
; assoc = assoc
; sym-assoc = sym-assoc
; identityˡ = identityˡ
; identityʳ = identityʳ
; identity² = identity²
; equiv = λ {A} {B} → record { refl = refl ; sym = λ f → sym f ; trans = λ f g → trans f g }
; ∘-resp-≈ = λ f≈h g≈i → ∘-resp-≈ f≈h g≈i
}
where
id' : ∀ {A : PreElgotMonad} → PreElgotMonad-Morphism A A
@ -76,21 +76,24 @@ PreElgotMonads = record
_∘'_ {X} {Y} {Z} f g = record
{ α = αf ∘ᵥ αg
; α-η = λ {A} → begin
(αf.η A ∘ αg.η A) ∘ TX.η.η A ≈⟨ {!!} ⟩
{!!} ≈⟨ {!!} ⟩
{!!} ≈⟨ {!!} ⟩
{!!} ≈⟨ {!!} ⟩
{!!} ≈⟨ {!!} ⟩
{!!} ≈⟨ {!!} ⟩
(αf.η A ∘ αg.η A) ∘ TX.η.η A ≈⟨ pullʳ (α-η g) ⟩
αf.η A ∘ TY.η.η A ≈⟨ α-η f ⟩
TZ.η.η A ∎
; α-μ = {!!}
; α-μ = λ {A} → begin
(αf.η A ∘ αg.η A) ∘ TX.μ.η A ≈⟨ pullʳ (α-μ g) ⟩
αf.η A ∘ TY.μ.η A ∘ TY.F.₁ (αg.η A) ∘ αg.η (TX.F.₀ A) ≈⟨ pullˡ (α-μ f) ⟩
(TZ.μ.η A ∘ TZ.F.₁ (αf.η A) ∘ αf.η (TY.F.₀ A)) ∘ TY.F.₁ (αg.η A) ∘ αg.η (TX.F.₀ A) ≈⟨ assoc ○ refl⟩∘⟨ pullʳ (pullˡ (NaturalTransformation.commute αf (αg.η A))) ⟩
TZ.μ.η A ∘ TZ.F.₁ (αf.η A) ∘ (TZ.F.₁ (αg.η A) ∘ αf.η (TX.F.₀ A)) ∘ αg.η (TX.F.₀ A) ≈⟨ refl⟩∘⟨ pullˡ (pullˡ (sym (Functor.homomorphism TZ.F))) ⟩
TZ.μ.η A ∘ (TZ.F.₁ (αf.η A ∘ αg.η A) ∘ αf.η (TX.F.₀ A)) ∘ αg.η (TX.F.₀ A) ≈⟨ refl⟩∘⟨ assoc ⟩
TZ.μ.η A ∘ TZ.F.₁ ((αf.η A ∘ αg.η A)) ∘ αf.η (TX.F.₀ A) ∘ αg.η (TX.F.₀ A) ∎
}
where
module TX = Monad (PreElgotMonad.T X)
module TY = Monad (PreElgotMonad.T Y)
module TZ = Monad (PreElgotMonad.T Z)
open PreElgotMonad-Morphism using (α-η; α-μ)
open PreElgotMonad-Morphism f using () renaming (α to αf)
open PreElgotMonad-Morphism g using () renaming (α to αg)
```