From 82cd7c9aa600f6ff5e968490e1e34eab8d448632 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Tue, 28 Nov 2023 15:07:40 +0100 Subject: [PATCH] work on commutativity --- .../Instance/AmbientCategory.lagda.md | 3 + src/Monad/Instance/K/Commutative.lagda.md | 69 +++++++++++++------ 2 files changed, 50 insertions(+), 22 deletions(-) diff --git a/src/Category/Instance/AmbientCategory.lagda.md b/src/Category/Instance/AmbientCategory.lagda.md index edb88f1..085f25b 100644 --- a/src/Category/Instance/AmbientCategory.lagda.md +++ b/src/Category/Instance/AmbientCategory.lagda.md @@ -233,4 +233,7 @@ module Category.Instance.AmbientCategory where where open Monad M using (F) open RMonad (Monad⇒Kleisli C M) using (extend; unit; extend-≈) renaming (sym-assoc to k-sym-assoc; identityʳ to k-identityʳ) + + ∇ : ∀ {X} → X + X ⇒ X + ∇ = [ idC , idC ] ``` \ No newline at end of file diff --git a/src/Monad/Instance/K/Commutative.lagda.md b/src/Monad/Instance/K/Commutative.lagda.md index 7a29860..7ab4623 100644 --- a/src/Monad/Instance/K/Commutative.lagda.md +++ b/src/Monad/Instance/K/Commutative.lagda.md @@ -148,29 +148,54 @@ private g' = (η _ +₁ idC) ∘ g w = [ i₁ ∘ K.₁ i₁ ∘ τ _ , (K.₁ i₂ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g') w-law₁ : f' # ∘ π₁ ≈ extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # - w-law₁ = sym (begin - extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # ≈⟨ extend-preserve [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] w ⟩ - ((extend [ f' # ∘ π₁ , η _ ∘ π₁ ] +₁ idC) ∘ w) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (∘[] ○ []-cong₂ (pullˡ +₁∘i₁) (pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullˡ (extend∘F₁ monadK [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] i₂ ○ kleisliK.extend-≈ inject₂)) identity²)))) ⟩ - ([ (i₁ ∘ extend [ f' # ∘ π₁ , η _ ∘ π₁ ]) ∘ K.₁ i₁ ∘ τ _ , ((extend (η (K.₀ Y) ∘ π₁) ∘ σ _ +₁ idC)) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (pullʳ (pullˡ (extend∘F₁ monadK [ f' # ∘ π₁ , η _ ∘ π₁ ] i₁ ○ kleisliK.extend-≈ inject₁))) ((+₁-cong₂ ((refl⟩∘⟨ monadK.F.homomorphism) ⟩∘⟨refl ○ (cancelˡ kleisliK.identityˡ) ⟩∘⟨refl) refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩ - ([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ identity² refl)) ⟩ - ([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC)) ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distribute₁ idC (η (K.₀ U)) idC)) ○ assoc)) ⟩ - ([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ (idC ⁂ η _ +₁ idC ⁂ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc²' (elimʳ (⟨⟩-unique id-comm id-comm)))) ⟩ - ([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ ∘ (idC ⁂ η _) , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ (refl⟩∘⟨ (τ-η _) ○ kleisliK.identityʳ)) ((+₁-cong₂ {! !} refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩ -- K.₁ π₁ law for σ - ([ i₁ ∘ f' # ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ ((#-Fixpoint (algebras _)) ⟩∘⟨refl ○ assoc ○ refl⟩∘⟨ (sym π₁∘⁂))) refl) ⟩∘⟨refl) ⟩ - ([ i₁ ∘ [ idC , f' # ] ∘ π₁ ∘ (f' ⁂ idC) , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc²' assoc)) ⟩ - ([ i₁ ∘ [ idC , f' # ] ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ ((f' ⁂ idC) +₁ (f' ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (distribute₁ f' idC idC))) ⟩ - ([ i₁ ∘ [ idC , f' # ] ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ (distributeˡ⁻¹ ∘ (f' ⁂ (idC +₁ idC))) ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identityʳ (elimˡ ([]-unique id-comm-sym id-comm-sym))))) ⟩ - ([ i₁ ∘ [ idC , f' # ] ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ refl⟩∘⟨ sym distribute₂') refl) ⟩∘⟨refl) ⟩ - ([ i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁) ∘ distributeʳ⁻¹ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f' ⁂ g)) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc²' refl)) ⟩ - ([ i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁) , (π₁ +₁ idC) ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ pullˡ distribute₄) ⟩ - ([ i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁) , (π₁ +₁ idC) ] ∘ ([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (pullˡ (∘[] ○ []-cong₂ []∘+₁ []∘+₁))) ⟩ - (([ [ ((i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁)) ∘ i₁) , (((π₁ +₁ idC)) ∘ i₁) ] , [ ((i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁)) ∘ i₂) , (((π₁ +₁ idC)) ∘ i₂) ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (assoc ○ ([]-cong₂ ([]-cong₂ ((refl⟩∘⟨ []∘+₁) ⟩∘⟨refl ○ pullʳ inject₁) +₁∘i₁) ([]-cong₂ ((refl⟩∘⟨ []∘+₁) ⟩∘⟨refl ○ pullʳ inject₂) +₁∘i₂)) ⟩∘⟨refl) ⟩ - ([ [ (i₁ ∘ idC ∘ π₁) , i₁ ∘ π₁ ] , [ i₁ ∘ f' # ∘ π₁ , i₂ ∘ idC ] ] ∘ ((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ ([]-cong₂ (refl⟩∘⟨ identityˡ) refl ○ sym ∘[]) refl) ⟩∘⟨ assoc) ⟩ - ([ i₁ ∘ [ π₁ , π₁ ] , f' # ∘ π₁ +₁ idC ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc refl)) ⟩ - ([ i₁ ∘ [ π₁ , π₁ ] ∘ distributeˡ⁻¹ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))# ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ distribute₃) refl) ⟩∘⟨refl) ⟩ + w-law₁ = sym (begin + extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # ≈⟨ step₁ ⟩ ([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))# ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - {! !} ∎) + ([ (i₁ ∘ π₁) , ((f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹) ] ∘ distributeʳ⁻¹ ∘ {! !} ∘ (f' ⁂ idC)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ {! !}) ⟩ + -- TODO whatever is going wrong here????? + ([ (i₁ ∘ π₁) , ((f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹) ] ∘ ({! idC ⁂ idC !} +₁ {! !}) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ {! elimʳ !} {! !})) ⟩ + ([ (i₁ ∘ π₁) , ((f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ ⟨ π₁ , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈˘⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ)))) ⟩∘⟨refl) ⟩ + ([ (i₁ ∘ π₁) , ((f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ∘ (π₁ ⁂ idC) ∘ ⟨ idC , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈˘⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (refl⟩∘⟨ (pullˡ (distribute₁ π₁ idC idC ○ refl⟩∘⟨ ⁂-cong₂ refl ([]-unique id-comm-sym id-comm-sym)) ○ assoc))) ⟩∘⟨refl) ⟩ + ([ (i₁ ∘ π₁) , (f' # ∘ π₁ +₁ idC) ∘ ((π₁ ⁂ idC) +₁ (π₁ ⁂ idC)) ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullʳ π₁∘⁂) identityˡ))) ⟩∘⟨refl) ⟩ + ([ (i₁ ∘ π₁) , ((f' # ∘ π₁ ∘ π₁ +₁ (π₁ ⁂ idC)) ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈˘⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (pullˡ (+₁∘+₁ ○ +₁-cong₂ assoc identityˡ))) ⟩∘⟨refl) ⟩ + ([ (i₁ ∘ π₁) , (((f' # ∘ π₁) +₁ idC) ∘ (π₁ +₁ π₁ ⁂ idC) ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩) ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC)) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ []∘+₁) ⟩ + ([ i₁ , (f' # ∘ π₁) +₁ idC ] ∘ h) # ≈˘⟨ #-resp-≈ (algebras _) (([]-cong₂ refl (+₁-cong₂ (#-Uniformity (algebras _) by-uni) refl)) ⟩∘⟨refl) ⟩ + ([ i₁ , ((idC +₁ ∇) ∘ h) # +₁ idC ] ∘ h) # ≈˘⟨ {! !} ⟩ -- proposition 41 + ((idC +₁ ∇) ∘ h)# ≈⟨ #-Uniformity (algebras _) by-uni ⟩ + (f' #) ∘ π₁ ∎) + where + h = (π₁ +₁ (π₁ +₁ π₁ ⁂ idC) ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) + step₁ : extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # ≈ ([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))# + step₁ = begin + extend [ f' # ∘ π₁ , η _ ∘ π₁ ] ∘ w # ≈⟨ extend-preserve [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] w ⟩ + ((extend [ f' # ∘ π₁ , η _ ∘ π₁ ] +₁ idC) ∘ w) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (∘[] ○ []-cong₂ (pullˡ +₁∘i₁) (pullˡ (+₁∘+₁ ○ +₁-cong₂ (pullˡ (extend∘F₁ monadK [ (f' #) ∘ π₁ , η (K.₀ Y) ∘ π₁ ] i₂ ○ kleisliK.extend-≈ inject₂)) identity²)))) ⟩ + ([ (i₁ ∘ extend [ f' # ∘ π₁ , η _ ∘ π₁ ]) ∘ K.₁ i₁ ∘ τ _ , ((extend (η (K.₀ Y) ∘ π₁) ∘ σ _ +₁ idC)) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (pullʳ (pullˡ (extend∘F₁ monadK [ f' # ∘ π₁ , η _ ∘ π₁ ] i₁ ○ kleisliK.extend-≈ inject₁))) ((+₁-cong₂ ((refl⟩∘⟨ monadK.F.homomorphism) ⟩∘⟨refl ○ (cancelˡ kleisliK.identityˡ) ⟩∘⟨refl) refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩ + ([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g')) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ identity² refl)) ⟩ + ([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC)) ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distribute₁ idC (η (K.₀ U)) idC)) ○ assoc)) ⟩ + ([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ (idC ⁂ η _ +₁ idC ⁂ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc²' (elimʳ (⟨⟩-unique id-comm id-comm)))) ⟩ + ([ i₁ ∘ extend (f' # ∘ π₁) ∘ τ _ ∘ (idC ⁂ η _) , (K.₁ π₁ ∘ σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ (refl⟩∘⟨ (τ-η _) ○ kleisliK.identityʳ)) ((+₁-cong₂ {! !} refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩ -- K.₁ π₁ law for σ + ([ i₁ ∘ f' # ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ ((#-Fixpoint (algebras _)) ⟩∘⟨refl ○ assoc ○ refl⟩∘⟨ (sym π₁∘⁂))) refl) ⟩∘⟨refl) ⟩ + ([ i₁ ∘ [ idC , f' # ] ∘ π₁ ∘ (f' ⁂ idC) , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc²' assoc)) ⟩ + ([ i₁ ∘ [ idC , f' # ] ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ ((f' ⁂ idC) +₁ (f' ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (distribute₁ f' idC idC))) ⟩ + ([ i₁ ∘ [ idC , f' # ] ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ (distributeˡ⁻¹ ∘ (f' ⁂ (idC +₁ idC))) ∘ (idC ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identityʳ (elimˡ ([]-unique id-comm-sym id-comm-sym))))) ⟩ + ([ i₁ ∘ [ idC , f' # ] ∘ π₁ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ refl⟩∘⟨ sym distribute₂') refl) ⟩∘⟨refl) ⟩ + ([ i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁) ∘ distributeʳ⁻¹ , (π₁ +₁ idC) ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ∘ (f' ⁂ g)) # ≈˘⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc²' refl)) ⟩ + ([ i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁) , (π₁ +₁ idC) ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ pullˡ distribute₄) ⟩ + ([ i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁) , (π₁ +₁ idC) ] ∘ ([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (pullˡ (∘[] ○ []-cong₂ []∘+₁ []∘+₁))) ⟩ + (([ [ ((i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁)) ∘ i₁) , (((π₁ +₁ idC)) ∘ i₁) ] , [ ((i₁ ∘ [ idC , f' # ] ∘ (π₁ +₁ π₁)) ∘ i₂) , (((π₁ +₁ idC)) ∘ i₂) ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (assoc ○ ([]-cong₂ ([]-cong₂ ((refl⟩∘⟨ []∘+₁) ⟩∘⟨refl ○ pullʳ inject₁) +₁∘i₁) ([]-cong₂ ((refl⟩∘⟨ []∘+₁) ⟩∘⟨refl ○ pullʳ inject₂) +₁∘i₂)) ⟩∘⟨refl) ⟩ + ([ [ (i₁ ∘ idC ∘ π₁) , i₁ ∘ π₁ ] , [ i₁ ∘ f' # ∘ π₁ , i₂ ∘ idC ] ] ∘ ((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ ([]-cong₂ (refl⟩∘⟨ identityˡ) refl ○ sym ∘[]) refl) ⟩∘⟨ assoc) ⟩ + ([ i₁ ∘ [ π₁ , π₁ ] , f' # ∘ π₁ +₁ idC ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ∘ (f' ⁂ g)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ ([]∘+₁ ○ []-cong₂ assoc refl)) ⟩ + ([ i₁ ∘ [ π₁ , π₁ ] ∘ distributeˡ⁻¹ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))# ≈⟨ #-resp-≈ (algebras _) (([]-cong₂ (refl⟩∘⟨ distribute₃) refl) ⟩∘⟨refl) ⟩ + ([ i₁ ∘ π₁ , (f' # ∘ π₁ +₁ idC) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ∘ (f' ⁂ g))# ∎ + by-uni : (idC +₁ π₁) ∘ (idC +₁ ∇) ∘ h ≈ f' ∘ π₁ + by-uni = begin + (idC +₁ π₁) ∘ (idC +₁ ∇) ∘ h ≈⟨ pullˡ +₁∘+₁ ○ pullˡ (+₁∘+₁ ○ +₁-cong₂ (elimˡ identity²) (pullʳ (pullˡ []∘+₁))) ⟩ + (π₁ +₁ π₁ ∘ [ (idC ∘ π₁) , (idC ∘ (π₁ ⁂ idC)) ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ≈⟨ (+₁-cong₂ refl (pullˡ ∘[] ○ ([]-cong₂ (refl⟩∘⟨ identityˡ) ((refl⟩∘⟨ identityˡ) ○ π₁∘⁂)) ⟩∘⟨refl)) ⟩∘⟨refl ⟩ + (π₁ +₁ [ π₁ ∘ π₁ , π₁ ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , g ∘ π₂ ⟩) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ≈⟨ (+₁-cong₂ refl (pullˡ ((sym ∘[]) ⟩∘⟨refl ○ pullʳ distribute₃))) ⟩∘⟨refl ⟩ + (π₁ +₁ (π₁ ∘ π₁) ∘ ⟨ idC , g ∘ π₂ ⟩) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ≈⟨ (+₁-cong₂ refl (cancelʳ project₁)) ⟩∘⟨refl ⟩ + (π₁ +₁ π₁) ∘ distributeʳ⁻¹ ∘ (f' ⁂ idC) ≈⟨ pullˡ distribute₂' ⟩ + π₁ ∘ (f' ⁂ idC) ≈⟨ π₁∘⁂ ⟩ + f' ∘ π₁ ∎ w-law₂ : g' # ∘ π₂ ≈ extend [ η _ ∘ π₂ , g' # ∘ π₂ ] ∘ w # w-law₂ = {! !} τσ : extend (τ _) ∘ σ _ ∘ (f' # ⁂ g' #) ≈ extend ([ σ _ ∘ ( f' # ⁂ idC ) , τ _ ∘ (idC ⁂ g' #) ]) ∘ w #