From eabc93af7707dc38f26f12610c03eef313f97bf9 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Tue, 21 Nov 2023 16:58:46 +0100 Subject: [PATCH] align proofs --- .../Construction/PreElgotMonads.lagda.md | 28 +++++++------- .../StrongPreElgotMonads.lagda.md | 38 +++++++++---------- 2 files changed, 33 insertions(+), 33 deletions(-) diff --git a/src/Category/Construction/PreElgotMonads.lagda.md b/src/Category/Construction/PreElgotMonads.lagda.md index 1309679..fd0c216 100644 --- a/src/Category/Construction/PreElgotMonads.lagda.md +++ b/src/Category/Construction/PreElgotMonads.lagda.md @@ -71,12 +71,12 @@ PreElgotMonads = record ; α-η = identityˡ ; α-μ = sym (begin T.μ.η _ ∘ T.F.₁ idC ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ - T.μ.η _ ∘ T.F.₁ idC ≈⟨ elimʳ T.F.identity ⟩ - T.μ.η _ ≈⟨ sym identityˡ ⟩ - idC ∘ T.μ.η _ ∎) + T.μ.η _ ∘ T.F.₁ idC ≈⟨ elimʳ T.F.identity ⟩ + T.μ.η _ ≈⟨ sym identityˡ ⟩ + idC ∘ T.μ.η _ ∎) ; preserves = λ f → begin - idC ∘ f # ≈⟨ identityˡ ⟩ - f # ≈⟨ sym (#-resp-≈ elgotalgebras (elimˡ ([]-unique id-comm-sym id-comm-sym))) ⟩ + idC ∘ f # ≈⟨ identityˡ ⟩ + f # ≈⟨ sym (#-resp-≈ elgotalgebras (elimˡ ([]-unique id-comm-sym id-comm-sym))) ⟩ ((idC +₁ idC) ∘ f) # ∎ } where @@ -88,20 +88,20 @@ PreElgotMonads = record { α = αf ∘ᵥ αg ; α-η = λ {A} → begin (αf.η A ∘ αg.η A) ∘ TX.η.η A ≈⟨ pullʳ (α-η g) ⟩ - αf.η A ∘ TY.η.η A ≈⟨ α-η f ⟩ - TZ.η.η A ∎ + α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) ⟩ + (α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) ∎ + 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) ∎ ; preserves = λ {A} {B} h → begin - (αf.η B ∘ αg.η B) ∘ (h #X) ≈⟨ pullʳ (preserves g h) ⟩ - αf.η B ∘ ((αg.η B +₁ idC) ∘ h) #Y ≈⟨ preserves f ((αg.η B +₁ idC) ∘ h) ⟩ + (αf.η B ∘ αg.η B) ∘ (h #X) ≈⟨ pullʳ (preserves g h) ⟩ + αf.η B ∘ ((αg.η B +₁ idC) ∘ h) #Y ≈⟨ preserves f ((αg.η B +₁ idC) ∘ h) ⟩ (((αf.η B +₁ idC) ∘ (αg.η B +₁ idC) ∘ h) #Z) ≈⟨ #-resp-≈ (PreElgotMonad.elgotalgebras Z) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ - (((αf.η B ∘ αg.η B +₁ idC) ∘ h) #Z) ∎ + (((αf.η B ∘ αg.η B +₁ idC) ∘ h) #Z) ∎ } where module TX = Monad (PreElgotMonad.T X) diff --git a/src/Category/Construction/StrongPreElgotMonads.lagda.md b/src/Category/Construction/StrongPreElgotMonads.lagda.md index 880a987..edb0019 100644 --- a/src/Category/Construction/StrongPreElgotMonads.lagda.md +++ b/src/Category/Construction/StrongPreElgotMonads.lagda.md @@ -72,17 +72,17 @@ StrongPreElgotMonads = record ; α-η = identityˡ ; α-μ = sym (begin M.μ.η _ ∘ M.F.₁ idC ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩ - M.μ.η _ ∘ M.F.₁ idC ≈⟨ elimʳ M.F.identity ⟩ - M.μ.η _ ≈⟨ sym identityˡ ⟩ - idC ∘ M.μ.η _ ∎) + M.μ.η _ ∘ M.F.₁ idC ≈⟨ elimʳ M.F.identity ⟩ + M.μ.η _ ≈⟨ sym identityˡ ⟩ + idC ∘ M.μ.η _ ∎) ; α-strength = λ {X} {Y} → sym (begin - strengthen.η (X , Y) ∘ (idC ⁂ idC) ≈⟨ refl⟩∘⟨ (⁂-cong₂ refl (sym M.F.identity)) ⟩ + strengthen.η (X , Y) ∘ (idC ⁂ idC) ≈⟨ refl⟩∘⟨ (⁂-cong₂ refl (sym M.F.identity)) ⟩ strengthen.η (X , Y) ∘ (idC ⁂ M.F.₁ idC) ≈⟨ strengthen.commute (idC , idC) ⟩ M.F.₁ (idC ⁂ idC) ∘ strengthen.η (X , Y) ≈⟨ (M.F.F-resp-≈ (⟨⟩-unique id-comm id-comm) ○ M.F.identity) ⟩∘⟨refl ⟩ - idC ∘ strengthen.η (X , Y) ∎) + idC ∘ strengthen.η (X , Y) ∎) ; α-preserves = λ f → begin - idC ∘ f # ≈⟨ identityˡ ⟩ - f # ≈⟨ sym (#-resp-≈ elgotalgebras (elimˡ ([]-unique id-comm-sym id-comm-sym))) ⟩ + idC ∘ f # ≈⟨ identityˡ ⟩ + f # ≈⟨ sym (#-resp-≈ elgotalgebras (elimˡ ([]-unique id-comm-sym id-comm-sym))) ⟩ ((idC +₁ idC) ∘ f) # ∎ } where @@ -94,25 +94,25 @@ StrongPreElgotMonads = record { α = αf ∘ᵥ αg ; α-η = λ {A} → begin (αf.η A ∘ αg.η A) ∘ MX.η.η A ≈⟨ pullʳ (α-η g) ⟩ - αf.η A ∘ MY.η.η A ≈⟨ α-η f ⟩ - MZ.η.η A ∎ + αf.η A ∘ MY.η.η A ≈⟨ α-η f ⟩ + MZ.η.η A ∎ ; α-μ = λ {A} → begin - (αf.η A ∘ αg.η A) ∘ MX.μ.η A ≈⟨ pullʳ (α-μ g) ⟩ - αf.η A ∘ MY.μ.η A ∘ MY.F.₁ (αg.η A) ∘ αg.η (MX.F.₀ A) ≈⟨ pullˡ (α-μ f) ⟩ + (αf.η A ∘ αg.η A) ∘ MX.μ.η A ≈⟨ pullʳ (α-μ g) ⟩ + αf.η A ∘ MY.μ.η A ∘ MY.F.₁ (αg.η A) ∘ αg.η (MX.F.₀ A) ≈⟨ pullˡ (α-μ f) ⟩ (MZ.μ.η A ∘ MZ.F.₁ (αf.η A) ∘ αf.η (MY.F.₀ A)) ∘ MY.F.₁ (αg.η A) ∘ αg.η (MX.F.₀ A) ≈⟨ assoc ○ refl⟩∘⟨ pullʳ (pullˡ (NaturalTransformation.commute αf (αg.η A))) ⟩ MZ.μ.η A ∘ MZ.F.₁ (αf.η A) ∘ (MZ.F.₁ (αg.η A) ∘ αf.η (MX.F.₀ A)) ∘ αg.η (MX.F.₀ A) ≈⟨ refl⟩∘⟨ pullˡ (pullˡ (sym (Functor.homomorphism MZ.F))) ⟩ - MZ.μ.η A ∘ (MZ.F.₁ (αf.η A ∘ αg.η A) ∘ αf.η (MX.F.₀ A)) ∘ αg.η (MX.F.₀ A) ≈⟨ refl⟩∘⟨ assoc ⟩ - MZ.μ.η A ∘ MZ.F.₁ ((αf.η A ∘ αg.η A)) ∘ αf.η (MX.F.₀ A) ∘ αg.η (MX.F.₀ A) ∎ + MZ.μ.η A ∘ (MZ.F.₁ (αf.η A ∘ αg.η A) ∘ αf.η (MX.F.₀ A)) ∘ αg.η (MX.F.₀ A) ≈⟨ refl⟩∘⟨ assoc ⟩ + MZ.μ.η A ∘ MZ.F.₁ ((αf.η A ∘ αg.η A)) ∘ αf.η (MX.F.₀ A) ∘ αg.η (MX.F.₀ A) ∎ ; α-strength = λ {A} {B} → begin - (αf.η (A × B) ∘ αg.η (A × B)) ∘ strengthenX.η (A , B) ≈⟨ pullʳ (α-strength g) ⟩ - αf.η (A × B) ∘ strengthenY.η (A , B) ∘ (idC ⁂ αg.η B) ≈⟨ pullˡ (α-strength f) ⟩ + (αf.η (A × B) ∘ αg.η (A × B)) ∘ strengthenX.η (A , B) ≈⟨ pullʳ (α-strength g) ⟩ + αf.η (A × B) ∘ strengthenY.η (A , B) ∘ (idC ⁂ αg.η B) ≈⟨ pullˡ (α-strength f) ⟩ (strengthenZ.η (A , B) ∘ (idC ⁂ αf.η B)) ∘ (idC ⁂ αg.η B) ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩ - strengthenZ.η (A , B) ∘ (idC ⁂ (αf.η B ∘ αg.η B)) ∎ + strengthenZ.η (A , B) ∘ (idC ⁂ (αf.η B ∘ αg.η B)) ∎ ; α-preserves = λ {A} {B} h → begin - (αf.η B ∘ αg.η B) ∘ (h #X) ≈⟨ pullʳ (α-preserves g h) ⟩ - αf.η B ∘ ((αg.η B +₁ idC) ∘ h) #Y ≈⟨ α-preserves f ((αg.η B +₁ idC) ∘ h) ⟩ + (αf.η B ∘ αg.η B) ∘ (h #X) ≈⟨ pullʳ (α-preserves g h) ⟩ + αf.η B ∘ ((αg.η B +₁ idC) ∘ h) #Y ≈⟨ α-preserves f ((αg.η B +₁ idC) ∘ h) ⟩ (((αf.η B +₁ idC) ∘ (αg.η B +₁ idC) ∘ h) #Z) ≈⟨ #-resp-≈ (StrongPreElgotMonad.elgotalgebras Z) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ - (((αf.η B ∘ αg.η B +₁ idC) ∘ h) #Z) ∎ + (((αf.η B ∘ αg.η B +₁ idC) ∘ h) #Z) ∎ } where open StrongPreElgotMonad X using () renaming (SM to SMX)