From 7f336282ed08ea77bdf40a76028cbb04352cd6a9 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Fri, 3 Nov 2023 17:33:44 +0100 Subject: [PATCH] work on new proof principle --- src/Algebra/Properties.lagda.md | 52 ++++- .../Instance/AmbientCategory.lagda.md | 9 + src/Monad/Instance/K/Commutative.lagda.md | 199 +++++++++--------- 3 files changed, 154 insertions(+), 106 deletions(-) diff --git a/src/Algebra/Properties.lagda.md b/src/Algebra/Properties.lagda.md index 68beb07..763c39b 100644 --- a/src/Algebra/Properties.lagda.md +++ b/src/Algebra/Properties.lagda.md @@ -66,7 +66,57 @@ This file contains some typedefs and records concerning different algebras. → f ≈ g ∘ (idC ⁂ η) → (∀ {Z : Obj} (h : Z ⇒ Uniform-Iteration-Algebra.A FY + Z) → g ∘ (idC ⁂ h #) ≈ Uniform-Iteration-Algebra._# B ((g +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))) → g ≈ [ B , f ]♯ - + [_,_]♯ˡ : ∀ {X : Obj} (A : Uniform-Iteration-Algebra) (f : Y × X ⇒ Uniform-Iteration-Algebra.A A) → Uniform-Iteration-Algebra.A FY × X ⇒ Uniform-Iteration-Algebra.A A + [_,_]♯ˡ {X} A f = [ A , (f ∘ swap) ]♯ ∘ swap + ♯ˡ-law : ∀ {X : Obj} {A : Uniform-Iteration-Algebra} (f : Y × X ⇒ Uniform-Iteration-Algebra.A A) → f ≈ [ A , f ]♯ˡ ∘ (η ⁂ idC) + ♯ˡ-law {X} {A} f = begin + f ≈⟨ introʳ swap∘swap ⟩ + f ∘ swap ∘ swap ≈⟨ pullˡ (♯-law (f ∘ swap)) ⟩ + ([ A , f ∘ swap ]♯ ∘ (idC ⁂ η)) ∘ swap ≈⟨ pullʳ (sym swap∘⁂) ⟩ + [ A , (f ∘ swap) ]♯ ∘ swap ∘ (η ⁂ idC) ≈⟨ sym-assoc ⟩ + ([ A , (f ∘ swap) ]♯ ∘ swap) ∘ (η ⁂ idC) ∎ + ♯ˡ-preserving : ∀ {X : Obj} {B : Uniform-Iteration-Algebra} (f : Y × X ⇒ Uniform-Iteration-Algebra.A B) {Z : Obj} (h : Z ⇒ Uniform-Iteration-Algebra.A FY + Z) → [ B , f ]♯ˡ ∘ (h # ⁂ idC) ≈ Uniform-Iteration-Algebra._# B (([ B , f ]♯ˡ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) + ♯ˡ-preserving {X} {B} f {Z} h = begin + ([ B , (f ∘ swap) ]♯ ∘ swap) ∘ ((h #) ⁂ idC) ≈⟨ pullʳ swap∘⁂ ⟩ + [ B , (f ∘ swap) ]♯ ∘ (idC ⁂ h #) ∘ swap ≈⟨ pullˡ (♯-preserving (f ∘ swap) h) ⟩ + (([ B , (f ∘ swap) ]♯ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #ᵇ ∘ swap ≈⟨ sym (#ᵇ-Uniformity uni-helper) ⟩ + ((([ B , (f ∘ swap) ]♯ ∘ swap) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #ᵇ ∎ + where + open Uniform-Iteration-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity) + uni-helper : (idC +₁ swap) ∘ ([ B , f ∘ swap ]♯ ∘ swap +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈ (([ B , f ∘ swap ]♯ coproducts.+₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ swap + uni-helper = begin + (idC +₁ swap) ∘ ([ B , f ∘ swap ]♯ ∘ swap +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ pullˡ +₁∘+₁ ⟩ + (idC ∘ [ B , f ∘ swap ]♯ ∘ swap +₁ swap ∘ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩ + ([ B , f ∘ swap ]♯ ∘ swap +₁ idC ∘ swap) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩ + (([ B , f ∘ swap ]♯ +₁ idC) ∘ (swap +₁ swap)) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ pullʳ (pullˡ (sym distributeˡ⁻¹∘swap)) ⟩ + ([ B , f ∘ swap ]♯ +₁ idC) ∘ (distributeˡ⁻¹ ∘ swap) ∘ (h ⁂ idC) ≈⟨ (refl⟩∘⟨ (pullʳ swap∘⁂ ○ sym-assoc)) ○ sym-assoc ⟩ + (([ B , f ∘ swap ]♯ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ swap ∎ + ♯ˡ-unique : ∀ {X : Obj} {B : Uniform-Iteration-Algebra} (f : Y × X ⇒ Uniform-Iteration-Algebra.A B) (g : Uniform-Iteration-Algebra.A FY × X ⇒ Uniform-Iteration-Algebra.A B) + → f ≈ g ∘ (η ⁂ idC) + → ({Z : Obj} (h : Z ⇒ Uniform-Iteration-Algebra.A FY + Z) → g ∘ (h # ⁂ idC) ≈ Uniform-Iteration-Algebra._# B ((g +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))) + → g ≈ [ B , f ]♯ˡ + ♯ˡ-unique {X} {B} f g g-law g-preserving = begin + g ≈⟨ introʳ swap∘swap ⟩ + g ∘ swap ∘ swap ≈⟨ sym-assoc ⟩ + (g ∘ swap) ∘ swap ≈⟨ (♯-unique (f ∘ swap) (g ∘ swap) helper₁ helper₂) ⟩∘⟨refl ⟩ + [ B , (f ∘ swap) ]♯ ∘ swap ∎ + where + open Uniform-Iteration-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity) + helper₁ : f ∘ swap ≈ (g ∘ swap) ∘ (idC ⁂ η) + helper₁ = begin + f ∘ swap ≈⟨ g-law ⟩∘⟨refl ⟩ + (g ∘ (η ⁂ idC)) ∘ swap ≈⟨ pullʳ (sym swap∘⁂) ⟩ + g ∘ swap ∘ (idC ⁂ η) ≈⟨ sym-assoc ⟩ + (g ∘ swap) ∘ (idC ⁂ η) ∎ + helper₂ : ∀ {Z : Obj} (h : Z ⇒ Uniform-Iteration-Algebra.A FY + Z) → (g ∘ swap) ∘ (idC ⁂ h #) ≈ ((g ∘ swap +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #ᵇ + helper₂ {Z} h = begin + (g ∘ swap) ∘ (idC ⁂ h #) ≈⟨ pullʳ swap∘⁂ ⟩ + g ∘ (h # ⁂ idC) ∘ swap ≈⟨ pullˡ (g-preserving h) ⟩ + ((g +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #ᵇ ∘ swap ≈⟨ sym (#ᵇ-Uniformity uni-helper) ⟩ + ((g ∘ swap +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #ᵇ ∎ + where + uni-helper : (idC +₁ swap) ∘ (g ∘ swap +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈ ((g +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) ∘ swap + uni-helper = pullˡ +₁∘+₁ ○ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ○ (sym +₁∘+₁) ⟩∘⟨refl ○ pullʳ (pullˡ (sym distributeʳ⁻¹∘swap)) ○ (refl⟩∘⟨ (pullʳ swap∘⁂ ○ sym-assoc)) ○ sym-assoc record StableFreeUniformIterationAlgebra : Set (suc o ⊔ suc ℓ ⊔ suc e) where field Y : Obj diff --git a/src/Category/Instance/AmbientCategory.lagda.md b/src/Category/Instance/AmbientCategory.lagda.md index f030136..fc50d95 100644 --- a/src/Category/Instance/AmbientCategory.lagda.md +++ b/src/Category/Instance/AmbientCategory.lagda.md @@ -88,6 +88,15 @@ module Category.Instance.AmbientCategory where [ (idC ⁂ i₁) ∘ swap , (idC ⁂ i₂) ∘ swap ] ∘ distributeʳ⁻¹ ≈⟨ sym (pullˡ []∘+₁) ⟩ distributeˡ ∘ (swap +₁ swap) ∘ distributeʳ⁻¹ ∎) + distributeʳ⁻¹∘swap : ∀ {A B C : Obj} → distributeʳ⁻¹ ∘ swap ≈ (swap +₁ swap) ∘ distributeˡ⁻¹ {A} {B} {C} + distributeʳ⁻¹∘swap = Iso⇒Mono C (IsIso.iso isIsoʳ) (distributeʳ⁻¹ ∘ swap) ((swap +₁ swap) ∘ distributeˡ⁻¹) (begin + (distributeʳ ∘ distributeʳ⁻¹ ∘ swap) ≈⟨ cancelˡ (IsIso.isoʳ isIsoʳ) ⟩ + swap ≈⟨ sym (cancelʳ (IsIso.isoʳ isIsoˡ)) ⟩ + ((swap ∘ distributeˡ) ∘ distributeˡ⁻¹) ≈⟨ (∘[] ⟩∘⟨refl) ⟩ + [ swap ∘ (idC ⁂ i₁) , swap ∘ (idC ⁂ i₂) ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ (sym swap∘⁂) (sym swap∘⁂)) ⟩∘⟨refl) ⟩ + [ (i₁ ⁂ idC) ∘ swap , (i₂ ⁂ idC) ∘ swap ] ∘ distributeˡ⁻¹ ≈⟨ sym (pullˡ []∘+₁) ⟩ + (distributeʳ ∘ (swap +₁ swap) ∘ distributeˡ⁻¹) ∎) + dstr-law₁ : ∀ {A B C} → distributeˡ⁻¹ {A} {B} {C} ∘ (idC ⁂ i₁) ≈ i₁ dstr-law₁ = (refl⟩∘⟨ (sym inject₁)) ○ (cancelˡ (IsIso.isoˡ isIsoˡ)) dstr-law₂ : ∀ {A B C} → distributeˡ⁻¹ {A} {B} {C} ∘ (idC ⁂ i₂) ≈ i₂ diff --git a/src/Monad/Instance/K/Commutative.lagda.md b/src/Monad/Instance/K/Commutative.lagda.md index e496038..3ce0eb4 100644 --- a/src/Monad/Instance/K/Commutative.lagda.md +++ b/src/Monad/Instance/K/Commutative.lagda.md @@ -13,17 +13,17 @@ import Monad.Instance.K as MIK ```agda module Monad.Instance.K.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where - open Ambient ambient - open MIK ambient - open MonadK MK - open import Monad.Instance.K.Strong ambient MK - open import Category.Construction.UniformIterationAlgebras ambient - open import Algebra.UniformIterationAlgebra ambient - open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra) +open Ambient ambient +open MIK ambient +open MonadK MK +open import Monad.Instance.K.Strong ambient MK +open import Category.Construction.UniformIterationAlgebras ambient +open import Algebra.UniformIterationAlgebra ambient +open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra) - open Equiv - open HomReasoning - open MR C +open Equiv +open HomReasoning +open MR C -- open M C ``` @@ -34,101 +34,90 @@ The proof is analogous to the ones for strength, the relevant diagram is: ```agda - KCommutative : CommutativeMonad {C = C} {V = monoidal} symmetric KStrong - KCommutative = record { commutes = commutes' } - where - open monadK using (μ) - open StrongMonad KStrong using (strengthen) - open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving; ♯-unique) - open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈) - - -- some helper definitions to make our life easier - η = λ Z → FreeObject.η (freealgebras Z) - _♯ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f - _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f - σ : ∀ ((X , Y) : Obj ×f Obj) → K.₀ X × Y ⇒ K.₀ (X × Y) - σ _ = K.₁ swap ∘ (τ _) ∘ swap +open monadK using (μ) +open StrongMonad KStrong using (strengthen) +open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving; ♯-unique; ♯ˡ-unique; ♯ˡ-preserving; ♯ˡ-law) +open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈) - σ-preserve : ∀ {X Y Z : Obj} (h : Z ⇒ K.₀ Y + Z) → σ (Y , X) ∘ (h # ⁂ idC) ≈ ((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))# - {- - K.₁ swap ∘ τ ∘ swap ∘ (h # ⁂ idC) - ≈ K.₁ swap ∘ τ ∘ (idC ⁂ h #) ∘ swap - ≈ K.₁ swap ∘ ()# ∘ swap - ≈ ((K.₁ swap +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ swap - -} - σ-preserve {Z} h = {! !} - σ-preserve' : ∀ {X Y Z : Obj} (h : Z ⇒ K.₀ Y + Z) → σ (X , K.₀ Y) ∘ (idC ⁂ h #) ≈ ((σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# - σ-preserve' {Z} h = {! !} - commutes' : ∀ {X Y : Obj} → μ.η _ ∘ K.₁ (σ _) ∘ τ (K.₀ X , Y) ≈ μ.η _ ∘ K.₁ (τ _) ∘ σ _ - commutes' {X} {Y} = begin - μ.η _ ∘ K.₁ (σ _) ∘ τ _ ≈⟨ ♯-unique (stable _) (σ _) (μ.η (X × Y) ∘ K.₁ (σ _) ∘ τ _) comm₁ comm₂ ⟩ - (σ _) ♯ ≈⟨ sym (♯-unique (stable _) (σ _) (μ.η _ ∘ K.₁ (τ _) ∘ σ _) comm₃ comm₄) ⟩ - {! !} ≈⟨ {! !} ⟩ - μ.η _ ∘ K.₁ (τ _) ∘ σ _ ∎ - where - comm₁ : σ _ ≈ (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ η _) - comm₁ = sym (begin - (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (τ-η _)) ⟩ - μ.η _ ∘ K.₁ (σ _) ∘ η _ ≈⟨ refl⟩∘⟨ (K₁η _) ⟩ - μ.η _ ∘ η _ ∘ σ _ ≈⟨ cancelˡ monadK.identityʳ ⟩ - σ _ ∎) - comm₂ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K.₁ (σ _) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# - comm₂ {Z} h = begin - (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (pullʳ (♯-preserving (stable _) (η _) h)) ⟩ - μ.η _ ∘ K.₁ (σ _) ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ refl⟩∘⟨ (Uniform-Iteration-Algebra-Morphism.preserves ((freealgebras _ FreeObject.*) (η _ ∘ σ _))) ⟩ - μ.η _ ∘ ((K.₁ (σ _) +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC) ⟩ - ((μ.η _ +₁ idC) ∘ (K.₁ (σ _) +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩ - ((μ.η _ ∘ K.₁ (σ _) +₁ idC ∘ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩ - (((μ.η _ ∘ K.₁ (σ _)) ∘ τ _ +₁ (idC ∘ idC) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ assoc (elimˡ identity²)) ⟩∘⟨refl) ⟩ - ((μ.η _ ∘ K.₁ (σ _) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎ - comm₃ : σ _ ≈ (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ η _) - comm₃ = sym (begin - (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (pullʳ (pullʳ swap∘⁂))) ⟩ - μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (η _ ⁂ idC) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (sym K.identity) ⟩∘⟨refl ⟩ - μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (η _ ⁂ K.₁ idC) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (strengthen.commute (η _ , idC)) ⟩ - μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ (K.₁ (η _ ⁂ idC) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (pullˡ (sym K.homomorphism)) ⟩ - μ.η _ ∘ K.₁ (τ _) ∘ (K.₁ (swap ∘ (η _ ⁂ idC)) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (pullˡ (pullˡ (sym K.homomorphism))) ⟩ - μ.η _ ∘ (K.₁ (τ _ ∘ swap ∘ (η _ ⁂ idC)) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (((K.F-resp-≈ (refl⟩∘⟨ swap∘⁂)) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ - μ.η _ ∘ (K.₁ (τ _ ∘ (idC ⁂ η _) ∘ swap) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (K.F-resp-≈ (pullˡ (τ-η _))) ⟩∘⟨refl ⟩∘⟨refl ⟩ - μ.η _ ∘ (K.₁ (η _ ∘ swap) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ ((K.homomorphism ⟩∘⟨refl) ⟩∘⟨refl) ⟩ - μ.η _ ∘ ((K.₁ (η _) ∘ K.₁ swap) ∘ τ _) ∘ swap ≈⟨ pullˡ (pullˡ (cancelˡ monadK.identityˡ)) ⟩ - (K.₁ swap ∘ τ _) ∘ swap ≈⟨ assoc ⟩ - σ _ ∎) - 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.₁ (τ _) ∘ σ _) ∘ (((i₁ #) ⁂ h #)) ≈˘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (#-Uniformity (algebras _) helper₁) {! !} ⟩ - (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ ⟨ ((π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # , ((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ⟩ ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - ((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎ - where - -- this leads nowhere - helper₁ : (idC +₁ π₁) ∘ (π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈ i₁ ∘ π₁ - helper₁ = begin - (idC +₁ π₁) ∘ (π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ - (π₁ +₁ π₁) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ {! !} ⟩ - i₁ ∘ π₁ ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ π₁∘⁂ ⟩ - i₁ ∘ idC ∘ π₁ ≈⟨ refl⟩∘⟨ identityˡ ⟩ - i₁ ∘ π₁ ∎ - test : ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ swap ≈ ((τ (X , Y) ∘ swap +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # - test = sym (#-Uniformity (algebras _) (sym (begin - ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ swap ≈⟨ pullʳ (pullʳ (sym swap∘⁂)) ⟩ - (τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ swap ∘ (h ⁂ idC) ≈⟨ refl⟩∘⟨ (pullˡ distributeˡ⁻¹∘swap) ⟩ - (τ (X , Y) +₁ idC) ∘ ((swap +₁ swap) ∘ distributeʳ⁻¹) ∘ (h ⁂ idC) ≈⟨ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (sym identityˡ) id-comm-sym)) ⟩ - ((idC ∘ τ (X , Y) ∘ swap +₁ swap ∘ idC) ∘ distributeʳ⁻¹) ∘ (h ⁂ idC) ≈⟨ assoc ○ (sym +₁∘+₁) ⟩∘⟨refl ⟩ - ((idC +₁ swap) ∘ (τ (X , Y) ∘ swap +₁ idC)) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ assoc ⟩ - (idC +₁ swap) ∘ (τ (X , Y) ∘ swap +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ∎))) - helper : τ _ ∘ (h # ⁂ idC) ∘ swap ≈ ((τ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # ∘ swap - helper = {! !} - τ∘swap-preserving : τ (K.₀ Y , X) ∘ (h # ⁂ idC) ≈ ((τ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # - τ∘swap-preserving = begin - τ (K.₀ Y , X) ∘ (h # ⁂ idC) ≈⟨ {! !} ⟩ - τ (K.₀ Y , X) ∘ (h # ⁂ K.₁ idC) ≈⟨ {! !} ⟩ - K.₁ (h # ⁂ idC) ∘ τ _ ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - ((τ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # ∎ +-- some helper definitions to make our life easier +private + η = λ Z → FreeObject.η (freealgebras Z) + _♯ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f + _♯ˡ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ˡ {Y = X} (stable X) {X = A} (algebras Y) f + _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f + +σ : ∀ ((X , Y) : Obj ×f Obj) → K.₀ X × Y ⇒ K.₀ (X × Y) +σ _ = K.₁ swap ∘ (τ _) ∘ swap + +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₁ {! !}) ⟩ + 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)) ♯ˡ ≈⟨ {! !} ⟩ + 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)) # ∎ + where + uni-helper : (idC +₁ idC ⁂ η Y) ∘ (f ∘ (idC ⁂ η Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈ ((f +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) ∘ (idC ⁂ η Y) + uni-helper = {! !} + +KCommutative : CommutativeMonad {C = C} {V = monoidal} symmetric KStrong +KCommutative = record { commutes = commutes' } + where + commutes' : ∀ {X Y : Obj} → μ.η _ ∘ K.₁ (σ _) ∘ τ (K.₀ X , Y) ≈ μ.η _ ∘ K.₁ (τ _) ∘ σ _ + commutes' {X} {Y} = begin + μ.η _ ∘ K.₁ (σ _) ∘ τ _ ≈⟨ ♯-unique (stable _) (σ _) (μ.η (X × Y) ∘ K.₁ (σ _) ∘ τ _) comm₁ comm₂ ⟩ + (σ _) ♯ ≈⟨ sym (♯-unique (stable _) (σ _) (μ.η _ ∘ K.₁ (τ _) ∘ σ _) comm₃ comm₄) ⟩ + {! !} ≈⟨ {! !} ⟩ + μ.η _ ∘ K.₁ (τ _) ∘ σ _ ∎ + where + comm₁ : σ _ ≈ (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ η _) + comm₁ = sym (begin + (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (τ-η _)) ⟩ + μ.η _ ∘ K.₁ (σ _) ∘ η _ ≈⟨ refl⟩∘⟨ (K₁η _) ⟩ + μ.η _ ∘ η _ ∘ σ _ ≈⟨ cancelˡ monadK.identityʳ ⟩ + σ _ ∎) + comm₂ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K.₁ (σ _) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# + comm₂ {Z} h = begin + (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (pullʳ (♯-preserving (stable _) (η _) h)) ⟩ + μ.η _ ∘ K.₁ (σ _) ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ refl⟩∘⟨ (Uniform-Iteration-Algebra-Morphism.preserves ((freealgebras _ FreeObject.*) (η _ ∘ σ _))) ⟩ + μ.η _ ∘ ((K.₁ (σ _) +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC) ⟩ + ((μ.η _ +₁ idC) ∘ (K.₁ (σ _) +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩ + ((μ.η _ ∘ K.₁ (σ _) +₁ idC ∘ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩ + (((μ.η _ ∘ K.₁ (σ _)) ∘ τ _ +₁ (idC ∘ idC) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ assoc (elimˡ identity²)) ⟩∘⟨refl) ⟩ + ((μ.η _ ∘ K.₁ (σ _) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎ + comm₃ : σ _ ≈ (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ η _) + comm₃ = sym (begin + (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (pullʳ (pullʳ swap∘⁂))) ⟩ + μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (η _ ⁂ idC) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (sym K.identity) ⟩∘⟨refl ⟩ + μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (η _ ⁂ K.₁ idC) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (strengthen.commute (η _ , idC)) ⟩ + μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ (K.₁ (η _ ⁂ idC) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (pullˡ (sym K.homomorphism)) ⟩ + μ.η _ ∘ K.₁ (τ _) ∘ (K.₁ (swap ∘ (η _ ⁂ idC)) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (pullˡ (pullˡ (sym K.homomorphism))) ⟩ + μ.η _ ∘ (K.₁ (τ _ ∘ swap ∘ (η _ ⁂ idC)) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (((K.F-resp-≈ (refl⟩∘⟨ swap∘⁂)) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ + μ.η _ ∘ (K.₁ (τ _ ∘ (idC ⁂ η _) ∘ swap) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (K.F-resp-≈ (pullˡ (τ-η _))) ⟩∘⟨refl ⟩∘⟨refl ⟩ + μ.η _ ∘ (K.₁ (η _ ∘ swap) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ ((K.homomorphism ⟩∘⟨refl) ⟩∘⟨refl) ⟩ + μ.η _ ∘ ((K.₁ (η _) ∘ K.₁ swap) ∘ τ _) ∘ swap ≈⟨ pullˡ (pullˡ (cancelˡ monadK.identityˡ)) ⟩ + (K.₁ swap ∘ τ _) ∘ swap ≈⟨ assoc ⟩ + σ _ ∎) + 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))# ∎ ``` \ No newline at end of file