mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
Merge branch 'main' of git8.cs.fau.de:theses/bsc-leon-vatthauer
This commit is contained in:
commit
08cf9b6f61
1 changed files with 20 additions and 17 deletions
|
@ -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)
|
||||
|
||||
```
|
||||
|
|
Loading…
Reference in a new issue