From 28cee7138e59a925810682fe473a17389984b024 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Sat, 4 Nov 2023 09:52:36 +0100 Subject: [PATCH] =?UTF-8?q?=E2=9C=A8=20Show=20equational=20lifting=20law,?= =?UTF-8?q?=20added=20proof=20principle?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Monad/Instance/K/Commutative.lagda.md | 55 +++++++++++----- .../Instance/K/EquationalLifting.lagda.md | 65 ++++++++++++++----- 2 files changed, 85 insertions(+), 35 deletions(-) diff --git a/src/Monad/Instance/K/Commutative.lagda.md b/src/Monad/Instance/K/Commutative.lagda.md index 3ce0eb4..1a0189f 100644 --- a/src/Monad/Instance/K/Commutative.lagda.md +++ b/src/Monad/Instance/K/Commutative.lagda.md @@ -8,6 +8,7 @@ open import Categories.Monad.Strong open import Data.Product using (_,_) renaming (_×_ to _×f_) open import Categories.FreeObjects.Free import Monad.Instance.K as MIK +open import Categories.Morphism.Properties ``` --> @@ -24,7 +25,7 @@ open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; unifo open Equiv open HomReasoning open MR C - -- open M C +open M C ``` # K is a commutative monad @@ -53,26 +54,35 @@ private proof-principle : ∀ {X Y} (f g : K.₀ X × K.₀ Y ⇒ K.₀ (X × Y)) → f ∘ (η _ ⁂ η _) ≈ g ∘ (η _ ⁂ η _) → (∀ {A} (h : A ⇒ K.₀ Y + A) → f ∘ (idC ⁂ h #) ≈ ((f +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#) → (∀ {A} (h : A ⇒ K.₀ X + A) → f ∘ (h # ⁂ idC) ≈ ((f +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) → (∀ {A} (h : A ⇒ K.₀ Y + A) → g ∘ (idC ⁂ h #) ≈ ((g +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#) → (∀ {A} (h : A ⇒ K.₀ X + A) → g ∘ (h # ⁂ idC) ≈ ((g +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) → f ≈ g proof-principle {X} {Y} f g η-eq f-iter₁ f-iter₂ g-iter₁ g-iter₂ = begin f ≈⟨ ♯-unique (stable _) (f ∘ (idC ⁂ η Y)) f refl (λ h → f-iter₁ h) ⟩ - (f ∘ (idC ⁂ η _)) ♯ ≈⟨ sym (♯-unique (stable _) (f ∘ (idC ⁂ η Y)) g helper₁ {! !}) ⟩ + (f ∘ (idC ⁂ η _)) ♯ ≈⟨ sym (♯-unique (stable _) (f ∘ (idC ⁂ η Y)) g helper₁ g-iter₁) ⟩ g ∎ where helper₁ : f ∘ (idC ⁂ η Y) ≈ g ∘ (idC ⁂ η Y) helper₁ = begin - f ∘ (idC ⁂ η Y) ≈⟨ ♯ˡ-unique (stable _) (f ∘ (η X ⁂ η Y)) (f ∘ (idC ⁂ η Y)) (sym (pullʳ (⁂∘⁂ ○ (⁂-cong₂ identityˡ identityʳ)))) {! !} ⟩ - (f ∘ (η X ⁂ η Y)) ♯ˡ ≈⟨ {! !} ⟩ + f ∘ (idC ⁂ η Y) ≈⟨ ♯ˡ-unique (stable _) (f ∘ (η X ⁂ η Y)) (f ∘ (idC ⁂ η Y)) (sym (pullʳ (⁂∘⁂ ○ (⁂-cong₂ identityˡ identityʳ)))) (comm₁ f f-iter₂) ⟩ + (f ∘ (η X ⁂ η Y)) ♯ˡ ≈⟨ sym (♯ˡ-unique (stable _) (f ∘ (η X ⁂ η Y)) (g ∘ (idC ⁂ η Y)) (sym (pullʳ (⁂∘⁂ ○ (⁂-cong₂ identityˡ identityʳ)) ○ sym η-eq)) (comm₁ g g-iter₂)) ⟩ g ∘ (idC ⁂ η Y) ∎ where - comm₁ : ∀ {Z : Obj} (h : Z ⇒ K.₀ X + Z) → (f ∘ (idC ⁂ η Y)) ∘ (h # ⁂ idC) ≈ ((f ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # - comm₁ {Z} h = begin - (f ∘ (idC ⁂ η Y)) ∘ (h # ⁂ idC) ≈⟨ pullʳ ⁂∘⁂ ⟩ - f ∘ (idC ∘ h # ⁂ η Y ∘ idC) ≈⟨ refl⟩∘⟨ (⁂-cong₂ id-comm-sym id-comm) ⟩ - f ∘ (h # ∘ idC ⁂ idC ∘ η Y) ≈⟨ refl⟩∘⟨ sym ⁂∘⁂ ⟩ - f ∘ (h # ⁂ idC) ∘ (idC ⁂ η Y) ≈⟨ pullˡ (f-iter₂ h) ⟩ - (((f +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) ∘ (idC ⁂ η Y) ≈⟨ sym (#-Uniformity (algebras _) uni-helper) ⟩ - ((f ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # ∎ + comm₁ : ∀ (k : K.₀ X × K.₀ Y ⇒ K.₀ (X × Y)) (k-iter₂ : ∀ {A} (h : A ⇒ K.₀ X + A) → k ∘ (h # ⁂ idC) ≈ ((k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) {Z : Obj} (h : Z ⇒ K.₀ X + Z) → (k ∘ (idC ⁂ η Y)) ∘ (h # ⁂ idC) ≈ ((k ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # + comm₁ k k-iter₂ {Z} h = begin + (k ∘ (idC ⁂ η Y)) ∘ (h # ⁂ idC) ≈⟨ pullʳ ⁂∘⁂ ⟩ + k ∘ (idC ∘ h # ⁂ η Y ∘ idC) ≈⟨ refl⟩∘⟨ (⁂-cong₂ id-comm-sym id-comm) ⟩ + k ∘ (h # ∘ idC ⁂ idC ∘ η Y) ≈⟨ refl⟩∘⟨ sym ⁂∘⁂ ⟩ + k ∘ (h # ⁂ idC) ∘ (idC ⁂ η Y) ≈⟨ pullˡ (k-iter₂ h) ⟩ + (((k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) ∘ (idC ⁂ η Y) ≈⟨ sym (#-Uniformity (algebras _) uni-helper) ⟩ + ((k ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # ∎ where - uni-helper : (idC +₁ idC ⁂ η Y) ∘ (f ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈ ((f +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) ∘ (idC ⁂ η Y) - uni-helper = {! !} + uni-helper : (idC +₁ idC ⁂ η Y) ∘ (k ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈ ((k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) ∘ (idC ⁂ η Y) + uni-helper = begin + (idC +₁ idC ⁂ η Y) ∘ (k ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ pullˡ +₁∘+₁ ⟩ + (idC ∘ k ∘ (idC ⁂ η Y) +₁ (idC ⁂ η Y) ∘ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩ + (k ∘ (idC ⁂ η Y) +₁ idC ∘ (idC ⁂ η Y)) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩ + ((k +₁ idC) ∘ ((idC ⁂ η Y) +₁ (idC ⁂ η Y))) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ pullʳ (pullˡ (distribute₁' (η Y) idC idC)) ⟩ + (k +₁ idC) ∘ (distributeʳ⁻¹ ∘ ((idC +₁ idC) ⁂ η Y)) ∘ (h ⁂ idC) ≈⟨ refl⟩∘⟨ pullʳ ⁂∘⁂ ⟩ + (k +₁ idC) ∘ distributeʳ⁻¹ ∘ ((idC +₁ idC) ∘ h ⁂ η Y ∘ idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) identityʳ ⟩ + (k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ η Y) ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ identityʳ identityˡ ⟩ + (k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ∘ idC ⁂ idC ∘ η Y) ≈˘⟨ pullʳ (pullʳ ⁂∘⁂) ⟩ + ((k +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) ∘ (idC ⁂ η Y) ∎ KCommutative : CommutativeMonad {C = C} {V = monoidal} symmetric KStrong KCommutative = record { commutes = commutes' } @@ -115,9 +125,20 @@ KCommutative = record { commutes = commutes' } comm₄ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# comm₄ {Z} h = begin (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ h #) ≈⟨ {! !} ⟩ - (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ ((i₁ # ∘ idC) ⁂ h #) ≈˘⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ + (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ ⟨ ((π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # , ((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ⟩ ≈⟨ {! !} ⟩ {! !} ≈⟨ {! !} ⟩ ((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎ + where + π₁-iter : ((π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈ π₁ ∘ (idC ⁂ h #) + π₁-iter = {! !} + distrib : (π₁ +₁ idC) ∘ distributeˡ⁻¹ ≈ i₁ ∘ π₁ + distrib = Iso⇒Epi C (IsIso.iso isIsoˡ) ((π₁ +₁ idC) ∘ distributeˡ⁻¹) (i₁ ∘ π₁) (begin + ((π₁ +₁ idC) ∘ distributeˡ⁻¹) ∘ distributeˡ ≈⟨ cancelʳ {! !} ⟩ + (π₁ +₁ idC) ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + i₁ ∘ [ π₁ , π₁ ] ≈˘⟨ {! !} ⟩ + [ i₁ ∘ π₁ , i₁ ∘ π₁ ] ≈˘⟨ {! !} ⟩ + [ i₁ ∘ idC ∘ π₁ , i₁ ∘ idC ∘ π₁ ] ≈˘⟨ []-cong₂ (pullʳ π₁∘⁂) (pullʳ π₁∘⁂) ⟩ + [ (i₁ ∘ π₁) ∘ (idC ⁂ i₁) , (i₁ ∘ π₁) ∘ (idC ⁂ i₂) ] ≈˘⟨ ∘[] ⟩ + (i₁ ∘ π₁) ∘ distributeˡ ∎) ``` \ No newline at end of file diff --git a/src/Monad/Instance/K/EquationalLifting.lagda.md b/src/Monad/Instance/K/EquationalLifting.lagda.md index 8e385d9..20d6bd2 100644 --- a/src/Monad/Instance/K/EquationalLifting.lagda.md +++ b/src/Monad/Instance/K/EquationalLifting.lagda.md @@ -8,6 +8,8 @@ open import Categories.FreeObjects.Free open import Categories.Category.Construction.Kleisli open import Categories.Category.Restriction import Monad.Instance.K as MIK +open import Categories.Morphism.Properties + ``` --> @@ -24,9 +26,12 @@ open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; unifo open HomReasoning open Equiv +open M C open MR C open kleisliK using (extend) open monadK using (μ) +open FreeObject using (*-uniq) +open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈) -- some helper definitions to make our life easier private @@ -39,29 +44,53 @@ private ```agda equationalLifting : ∀ {X} → τ (K.₀ X , X) ∘ Δ {K.₀ X} ≈ K.₁ ⟨ η X , idC ⟩ -equationalLifting = {! !} +equationalLifting {X} = *-uniq (freealgebras _) (η _ ∘ ⟨ η X , idC ⟩) (record { h = τ (K.₀ X , X) ∘ Δ ; preserves = preserves' }) commute + where + preserves' : ∀ {Z} {f : Z ⇒ K.₀ X + Z} → (τ (K.₀ X , X) ∘ Δ) ∘ f # ≈ ((τ (K.₀ X , X) ∘ Δ +₁ idC) ∘ f) # + preserves' {Z} {f} = begin + (τ (K.₀ X , X) ∘ Δ) ∘ f # ≈⟨ pullʳ Δ∘ ⟩ + τ (K.₀ X , X) ∘ ⟨ f # , f # ⟩ ≈⟨ helper₁ ⟩ + ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f))# ∘ ⟨ f # , idC ⟩ ≈⟨ helper₂ ⟩ -- lemma20 + ((τ (K.₀ X , X) ∘ Δ +₁ idC) ∘ f) # ∎ + where + helper₁ : τ (K.₀ X , X) ∘ ⟨ f # , f # ⟩ ≈ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f))# ∘ ⟨ f # , idC ⟩ + helper₁ = begin + τ (K.₀ X , X) ∘ ⟨ f # , f # ⟩ ≈⟨ refl⟩∘⟨ ((⟨⟩-cong₂ (sym identityˡ) (sym identityʳ)) ○ sym ⁂∘⟨⟩) ⟩ + τ (K.₀ X , X) ∘ (idC ⁂ f #) ∘ ⟨ f # , idC ⟩ ≈⟨ pullˡ (τ-comm f) ⟩ + ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f))# ∘ ⟨ f # , idC ⟩ ∎ + helper₂ : ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f))# ∘ ⟨ f # , idC ⟩ ≈ ((τ (K.₀ X , X) ∘ Δ +₁ idC) ∘ f) # + helper₂ = sym (#-Uniformity (algebras _) (begin + (idC +₁ ⟨ f # , idC ⟩) ∘ (τ (K.₀ X , X) ∘ Δ +₁ idC) ∘ f ≈⟨ pullˡ +₁∘+₁ ⟩ + (idC ∘ τ (K.₀ X , X) ∘ Δ +₁ ⟨ f # , idC ⟩ ∘ idC) ∘ f ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩ + (τ (K.₀ X , X) ∘ Δ +₁ idC ∘ ⟨ f # , idC ⟩) ∘ f ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩ + ((τ _ +₁ idC) ∘ (Δ +₁ ⟨ f # , idC ⟩)) ∘ f ≈⟨ assoc ⟩ + (τ _ +₁ idC) ∘ (Δ +₁ ⟨ f # , idC ⟩) ∘ f ≈⟨ refl⟩∘⟨ distrib ⟩ + (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ ⟨ f # , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ identityˡ identityʳ ⟩ + (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ ⟨ idC ∘ f # , f ∘ idC ⟩ ≈˘⟨ pullʳ (pullʳ ⁂∘⟨⟩) ⟩ + ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ f)) ∘ ⟨ f # , idC ⟩ ∎)) + where + distrib : (Δ +₁ ⟨ f # , idC ⟩) ∘ f ≈ distributeˡ⁻¹ ∘ ⟨ f # , f ⟩ + distrib = Iso⇒Mono C (IsIso.iso isIsoˡ) ((Δ +₁ ⟨ f # , idC ⟩) ∘ f) (distributeˡ⁻¹ ∘ ⟨ f # , f ⟩) (begin + distributeˡ ∘ (Δ +₁ ⟨ f # , idC ⟩) ∘ f ≈⟨ pullˡ []∘+₁ ⟩ + [ (idC ⁂ i₁) ∘ Δ , (idC ⁂ i₂) ∘ ⟨ f # , idC ⟩ ] ∘ f ≈⟨ ([]-cong₂ ⁂∘Δ ⁂∘⟨⟩) ⟩∘⟨refl ⟩ + [ ⟨ idC , i₁ ⟩ , ⟨ idC ∘ f # , i₂ ∘ idC ⟩ ] ∘ f ≈⟨ ([]-unique + (⟨⟩∘ ○ (⟨⟩-cong₂ inject₁ identityˡ)) + (⟨⟩∘ ○ (⟨⟩-cong₂ (inject₂ ○ sym identityˡ) id-comm-sym))) ⟩∘⟨refl ⟩ + ⟨ [ idC , f # ] , idC ⟩ ∘ f ≈⟨ ⟨⟩∘ ⟩ + ⟨ [ idC , f # ] ∘ f , idC ∘ f ⟩ ≈˘⟨ ⟨⟩-cong₂ (#-Fixpoint (algebras _)) (sym identityˡ) ⟩ + ⟨ f # , f ⟩ ≈˘⟨ cancelˡ (IsIso.isoʳ isIsoˡ) ⟩ + distributeˡ ∘ distributeˡ⁻¹ ∘ ⟨ f # , f ⟩ ∎) + commute : (τ (K.₀ X , X) ∘ Δ) ∘ η _ ≈ η _ ∘ ⟨ η X , idC ⟩ + commute = begin + (τ (K.₀ X , X) ∘ Δ) ∘ η _ ≈⟨ pullʳ Δ∘ ⟩ + τ (K.₀ X , X) ∘ ⟨ η X , η X ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (sym identityʳ) ○ sym ⁂∘⟨⟩) ⟩ + τ (K.₀ X , X) ∘ (idC ⁂ η X) ∘ ⟨ η X , idC ⟩ ≈⟨ pullˡ (τ-η _) ⟩ + η _ ∘ ⟨ η X , idC ⟩ ∎ ``` From this we can follow that the kleisli category of **K** is a *restriction category*. ```agda --- TODO this a trivial restriction structure, since η is identity in the kleisli category... -kleisli-restriction : Restriction (Kleisli monadK) -kleisli-restriction = record - { _↓ = λ f → η _ - ; pidʳ = kleisliK.identityʳ - ; ↓-comm = refl - ; ↓-denestʳ = begin - η _ ≈˘⟨ cancelˡ monadK.identityʳ ⟩ - μ.η _ ∘ η _ ∘ η _ ≈˘⟨ pullʳ (K₁η (η _)) ⟩ - (μ.η _ ∘ K.₁ (η _)) ∘ η _ ∎ - ; ↓-skew-comm = λ {A} {B} {C} {g} {f} → begin - (μ.η _ ∘ K.₁ (η _)) ∘ f ≈⟨ elimˡ monadK.identityˡ ⟩ - f ≈˘⟨ kleisliK.identityʳ ⟩ - extend f ∘ η _ ∎ - ; ↓-cong = λ _ → refl - } - kleisli-restriction' : Restriction (Kleisli monadK) kleisli-restriction' = record { _↓ = λ f → K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩