work on commutativity

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 ]
 ```

src/Monad/Instance/K/Commutative.lagda.md

@@ -149,6 +149,24 @@ private
       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 # ≈⟨ 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) ⟩ 
@@ -168,9 +186,16 @@ private
             ([ [ (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))# ≈⟨ {!   !} ⟩ 
+            ([ 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 #