work on proof

src/Algebra/Elgot.lagda.md

@@ -1,5 +1,6 @@
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Categories.Functor renaming (id to idF)
 open import Categories.Functor.Algebra
@@ -133,10 +134,9 @@ Here we give a different Characterization and show that it is equal.
         by-uni = begin 
           ([ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) ∘ (i₁ +₁ idC) ≈⟨ ((∘[] ○ []-cong₂ inject₁ refl) ⟩∘⟨refl) ⟩ 
           [ h +₁ i₁ ∘ i₁ , [ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ∘ (i₁ +₁ idC) ≈⟨ ([]∘+₁ ○ []-cong₂ +₁∘i₁ identityʳ) ⟩ 
-          -- TODO all these steps work
+          [ i₁ ∘ h , [ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ []-cong₂ (pullˡ (+₁∘i₁ ○ identityʳ)) (([]-cong₂ (+₁∘+₁ ○ +₁-cong₂ identityˡ +₁∘i₁) (pullˡ +₁∘i₂ ○ pullʳ (+₁∘i₂ ○ identityʳ))) ⟩∘⟨refl) ⟩ 
-          [ i₁ ∘ h , [ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ≈⟨ {!   !} ⟩ 
+          [ (idC +₁ (i₁ +₁ idC)) ∘ i₁ ∘ h , [ (idC +₁ (i₁ +₁ idC)) ∘ (h +₁ i₁) , (idC +₁ (i₁ +₁ idC)) ∘ i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ []-cong₂ refl (pullˡ ∘[]) ⟩
-          [ (idC +₁ (i₁ +₁ idC)) ∘ i₁ ∘ h , [ (idC +₁ (i₁ +₁ idC)) ∘ (h +₁ i₁) , (idC +₁ (i₁ +₁ idC)) ∘ i₂ ∘ i₂ ] ∘ f ] ≈⟨ {!   !} ⟩
+          [ (idC +₁ (i₁ +₁ idC)) ∘ i₁ ∘ h , (idC +₁ (i₁ +₁ idC)) ∘ [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ ∘[] ⟩
-          [ (idC +₁ (i₁ +₁ idC)) ∘ i₁ ∘ h , (idC +₁ (i₁ +₁ idC)) ∘ [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ≈⟨ {!   !} ⟩
           (idC +₁ (i₁ +₁ idC)) ∘ [ i₁ ∘ h , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ∎
 
     -- TODO Proposition 41
@@ -147,22 +147,24 @@ Here we give a different Characterization and show that it is equal.
       [ (idC +₁ i₁) ∘ g , f ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl (elimˡ ([]-unique id-comm-sym id-comm-sym)))) ⟩∘⟨refl) ⟩ 
       [ (idC +₁ i₁) ∘ g , (idC +₁ idC) ∘ f ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₁ identityˡ)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₂ identityˡ)))) ⟩∘⟨refl) ⟩
       [ ([ idC , idC ] +₁ idC) ∘ ((i₁ +₁ i₁) ∘ g) , ([ idC , idC ] +₁ idC) ∘ ((i₂ +₁ idC) ∘ f) ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ∘[]) ⟩∘⟨refl) ⟩
-      (([ idC , idC ] +₁ idC) ∘ [ ((i₁ +₁ i₁) ∘ g) , ((i₂ +₁ idC) ∘ f) ]) # ∘ i₂ ≈⟨ {!   !} ⟩ -- lemma 40
+      (([ idC , idC ] +₁ idC) ∘ [ ((i₁ +₁ i₁) ∘ g) , ((i₂ +₁ idC) ∘ f) ]) # ∘ i₂ ≈⟨ ((#-Stutter [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ idC) ∘ f ] idC) ⟩∘⟨refl) ⟩ 
+      ([ i₁ ∘ idC , [ idC +₁ i₁ , i₂ ∘ i₂ ] ∘ [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ idC) ∘ f ] ] # ∘ i₂) ∘ i₂ ≈⟨ (assoc ○ ((#-resp-≈ ([]-cong₂ identityʳ refl)) ⟩∘⟨refl)) ⟩
       [ i₁ , ([ idC +₁ i₁ , i₂ ∘ i₂ ] ∘ [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ idC) ∘ f ]) ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl (∘[] ○ []-cong₂ (pullˡ []∘+₁) (pullˡ []∘+₁)))) ⟩∘⟨refl) ⟩ 
       [ i₁ , [ [ (idC +₁ i₁) ∘ i₁ , (i₂ ∘ i₂) ∘ i₁ ] ∘ g , [ (idC +₁ i₁) ∘ i₂ , (i₂ ∘ i₂) ∘ idC ] ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (([]-cong₂ (+₁∘i₁ ○ identityʳ) assoc) ⟩∘⟨refl) (([]-cong₂ +₁∘i₂ identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩ 
       [ i₁ , [ [ i₁ , i₂ ∘ i₂ ∘ i₁ ] ∘ g , [ i₂ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ] # ∘ i₂ ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (pullˡ ([]∘+₁ ○ []-cong₂ identityʳ refl)) (∘[] ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩
       [ i₁ , [ [ i₁ , i₂ ] ∘ (idC +₁ i₂ ∘ i₁) ∘ g , (i₂ ∘ [ i₁ , i₂ ]) ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (elimˡ +-η) ((elimʳ +-η) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩ 
-      [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ {!   !} ⟩
+      [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] # ∘ i₂ ∘ i₂ {A = X} {B = X} ≈⟨ sym (#-Uniformity (sym by-uni₂)) ⟩
-      -- [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ pullˡ (sym (#-Uniformity (sym by-uni₂))) ⟩ 
-      -- {!   !} ≈⟨ {!   !} ⟩
-      -- [ {!   !} , [ [ i₁ , (idC +₁ i₂ ∘ i₁ ∘ i₂) ∘ g ] , i₂ ∘ i₂ ∘ h ] ] # ∘ i₂ ∘ i₂ ≈˘⟨ (#-Uniformity by-uni₃ ⟩∘⟨refl) ○ assoc ⟩ 
-      [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ ≈⟨ {!   !} ⟩ 
       {!   !} ≈⟨ {!   !} ⟩ 
-      {!   !} ≈⟨ {!   !} ⟩ 
+      (([ {!   !} , {!   !} ] ∘ f) #) ≈⟨ #-Uniformity (sym by-uni₃) ⟩ 
-      [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , [ i₂ ∘ i₁ ∘ i₁ , i₂ ∘ (i₂ +₁ idC) ] ∘ f ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ (∘[] ○ []-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl))) (pullˡ ∘[]))) ⟩∘⟨refl) ⟩ 
+      [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ (∘[] ○ []-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl))) refl)) ⟩∘⟨refl) ⟩ 
       [ (idC +₁ i₁) ∘ [ i₁ , (idC +₁ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ ≈⟨ (sym #-Folding) ⟩∘⟨refl ⟩ 
-      ([ i₁ , (idC +₁ i₂) ∘ g ] # +₁ h)# ∘ i₂ ≈⟨ {!   !} ⟩ 
+      ([ i₁ , (idC +₁ i₂) ∘ g ] # +₁ h)# ∘ i₂ ≈⟨ ((#-resp-≈ (+₁-cong₂ by-fix refl)) ⟩∘⟨refl) ⟩ 
-      {!   !} ≈⟨ {!   !} ⟩ 
+      ([ idC , g # ] +₁ h ) # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl ((sym ∘[] ○ elimʳ +-η) ⟩∘⟨refl))) ⟩∘⟨refl) ⟩ 
+      [ i₁ ∘ [ idC , g # ] , [ i₂ ∘ i₁ , i₂ ∘ i₂ ] ∘ h ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl (pullˡ ([]∘+₁ ○ []-cong₂ inject₂ identityʳ)))) ⟩∘⟨refl) ⟩ 
+      [ i₁ ∘ [ idC , g # ] , [ [ idC , g # ] +₁ i₁ , i₂ ∘ i₂ ] ∘ (i₂ +₁ idC) ∘ h ] # ∘ i₂ ≈⟨ sym (#-Stutter ((i₂ +₁ idC) ∘ h) [ idC , g # ]) ⟩ 
+      (([ [ idC , g # ] , [ idC , g # ] ] +₁ idC) ∘ (i₂ +₁ idC) ∘ h) # ≈⟨ #-resp-≈ (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₂ identity²)) ⟩ 
+      ((([ idC , g # ] +₁ idC)) ∘ h) # ≈⟨ #-resp-≈ (pullˡ (∘[] ○ []-cong₂ (pullˡ +₁∘i₁) +₁∘+₁)) ⟩ 
+      ([ (i₁ ∘ [ idC , g # ]) ∘ i₁ , [ idC , g # ] ∘ i₂ +₁ idC ∘ idC ] ∘ f) # ≈⟨ #-resp-≈ (([]-cong₂ (cancelʳ inject₁) (+₁-cong₂ inject₂ identity²)) ⟩∘⟨refl) ⟩ 
       ([ i₁ , g # +₁ idC ] ∘ f) # ∎
       where
         g = (idC +₁ [ idC , idC ]) ∘ f
@@ -174,22 +176,27 @@ Here we give a different Characterization and show that it is equal.
           [ (idC +₁ idC) ∘ g , (idC +₁ [ idC , idC ]) ∘ f ] ≈⟨ []-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) refl ⟩ 
           [ g , g ] ≈⟨ sym (∘[] ○ []-cong₂ identityʳ identityʳ) ⟩ 
           g ∘ [ idC , idC ] ∎
-        by-uni₂ : [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ∘ i₂ ≈ (idC +₁ i₂) ∘ {!   !}
+        by-uni₂ : [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ∘ i₂ ∘ i₂ ≈ (idC +₁ i₂ ∘ i₂) ∘ {!   !}
         by-uni₂ = begin 
-          [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ∘ i₂ ≈⟨ inject₂ ⟩ 
+          [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ∘ i₂ ∘ i₂ ≈⟨ (pullˡ inject₂) ○ inject₂ ⟩ 
-          [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ≈⟨ {!   !} ⟩ 
+          i₂ ∘ f ≈⟨ {!   !} ⟩ 
-          {!   !} ≈⟨ {!   !} ⟩ 
-          {!   !} ≈⟨ {!   !} ⟩ 
-          (idC +₁ i₂) ∘ [ ((idC +₁ i₁) ∘ g) , {! h  !} ] ∎
-        by-uni₃ : (idC +₁ i₂) ∘ [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ≈ {!   !} ∘ i₂
-        by-uni₃ = begin 
-          (idC +₁ i₂) ∘ [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ≈⟨ ∘[] ⟩ 
-          [ (idC +₁ i₂) ∘ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , (idC +₁ i₂) ∘ i₂ ∘ h ] ≈⟨ []-cong₂ ∘[] (pullˡ +₁∘i₂) ⟩ 
-          [ [ (idC +₁ i₂) ∘ i₁ , (idC +₁ i₂) ∘ (idC +₁ i₁ ∘ i₂) ∘ g ] , (i₂ ∘ i₂) ∘ h ] ≈⟨ []-cong₂ ([]-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl))) assoc ⟩ 
-          [ [ i₁ , (idC +₁ i₂ ∘ i₁ ∘ i₂) ∘ g ] , i₂ ∘ i₂ ∘ h ] ≈⟨ {!   !} ⟩ 
-          {!   !} ≈⟨ {!   !} ⟩ 
           {!   !} ≈⟨ {!   !} ⟩ 
           {!   !} ∎
+        by-uni₃ : [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ i₂ ≈ (idC +₁ i₂) ∘ {!   !}
+        by-uni₃ = begin 
+          [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ i₂ ≈⟨ inject₂ ⟩ 
+          i₂ ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ f ≈⟨ pullˡ ∘[] ⟩ 
+          [ i₂ ∘ i₁ ∘ i₁ , i₂ ∘ (i₂ +₁ idC) ] ∘ f ≈⟨ {!   !} ⟩ 
+          {!   !} ≈⟨ {!   !} ⟩ 
+          {!   !} ≈⟨ {!   !} ⟩ 
+          (idC +₁ i₂) ∘ [ i₁ , {! i₂  !} ] ∘ f ∎
+        by-fix : [ i₁ , (idC +₁ i₂) ∘ g ] # ≈ [ idC , g # ]
+        by-fix = sym (begin 
+          [ idC , g # ] ≈⟨ []-cong₂ refl #-Fixpoint ⟩ 
+          [ idC , [ idC , g # ] ∘ g ] ≈⟨ []-cong₂ refl (([]-cong₂ refl (#-Uniformity (sym inject₂))) ⟩∘⟨refl) ⟩ 
+          [ idC , [ idC , [ i₁ , (idC +₁ i₂) ∘ g ] # ∘ i₂ ] ∘ g ] ≈˘⟨ ∘[] ○ []-cong₂ inject₁ (pullˡ ([]∘+₁ ○ []-cong₂ identity² refl)) ⟩ 
+          [ idC , [ i₁ , (idC +₁ i₂) ∘ g ] # ] ∘ [ i₁ , (idC +₁ i₂) ∘ g ] ≈˘⟨ #-Fixpoint ⟩ 
+          ([ i₁ , (idC +₁ i₂) ∘ g ] #) ∎)
 
     -- every elgot-algebra comes with a divergence constant
     !ₑ : ⊥ ⇒ A

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

@@ -210,13 +210,36 @@ KCommutative = record { commutes = commutes' }
                   (idC +₁ (idC ⁂ h #)) ∘ ((ψ ∘ (idC ⁂ h #)) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) ∎
             comm₈ : ∀ {U} (g : U ⇒ K.₀ X + U) → ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ (g # ⁂ idC) ≈ ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#
             comm₈ {U} g = begin
+              ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈⟨ στ ⟩
+              extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ {!   !} ⟩ -- lemma 42
+              extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ sym τσ ⟩
+              ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ∎
+              where
+                τσ : ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ≈ extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #)
+                τσ = begin 
+                  (((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#) ≈⟨ {!   !} ⟩ 
+                  {!   !} ≈⟨ {!   !} ⟩ 
+                  {!   !} ≈⟨ {!   !} ⟩ 
+                  {!   !} ≈⟨ {!   !} ⟩ 
+                  extend ψ ∘ extend (τ _) ∘ σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ∎
+                στ : ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈ extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #)
+                στ = begin
                   ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈⟨ sym (#-Uniformity (algebras (X × Y)) (sym by-uni)) ⟩ 
                   ((ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ (ψ-left-iter g) refl) ⟩∘⟨refl) ⟩
-              (((((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # +₁ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ {!   !} ⟩
+                  (((((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # +₁ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #  ≈˘⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)) ⟩
-              {!   !} ≈⟨ {!   !} ⟩
+                  (((extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) +₁ idC) ∘ (η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ≈˘⟨ extend-preserve (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ((η (U × K.₀ Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ⟩
-              {!   !} ≈⟨ {!   !} ⟩
+                  extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ ((η _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ refl⟩∘⟨ (#-resp-≈ (algebras _) ((+₁-cong₂ (sym (τ-η _)) refl) ⟩∘⟨refl)) ⟩
-              {!   !} ≈⟨ {!   !} ⟩
+                  extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ ((τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈˘⟨ refl⟩∘⟨ (τ-comm ((η (K.₀ Y) +₁ idC) ∘ h) ○ #-resp-≈ (algebras _) comm) ⟩
-              ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ∎
+                  extend (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h)#) ≈˘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ kleisliK.identityʳ identity²)))) ⟩∘⟨refl ⟩
+                  extend ((((extend ψ +₁ idC) ∘ (η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ (kleisliK.extend-≈ (extend-preserve ψ ((η (K.₀ X × K.₀ Y) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)))) ⟩∘⟨refl ⟩
+                  extend (extend ψ ∘ (((η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ pullˡ kleisliK.sym-assoc ⟩
+                  extend ψ ∘ extend (((η _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distribute₁' idC (η (K.₀ X)) idC)))) ○ #-resp-≈ (algebras _) (pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ σ-η (elimʳ (⟨⟩-unique id-comm id-comm)))) ○ assoc))) ⟩∘⟨refl) ⟩
+                  extend ψ ∘ extend (((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ ((η (K.₀ X) +₁ idC) ⁂ idC) ∘ (g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ (kleisliK.extend-≈ (#-resp-≈ (algebras _) (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))))) ⟩∘⟨refl ⟩
+                  extend ψ ∘ extend (((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ ((η (K.₀ X) +₁ idC) ∘ g ⁂ idC)) #) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ ((kleisliK.extend-≈ (σ-comm ((η (K.₀ X) +₁ idC) ∘ g))) ⟩∘⟨refl) ⟩
+                  extend ψ ∘ extend (σ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ idC)) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈˘⟨ refl⟩∘⟨ (pullˡ (extend∘F₁ monadK (σ _) (((η _ +₁ idC) ∘ g) # ⁂ idC))) ⟩
+                  extend ψ ∘ extend (σ _) ∘ K.₁ (((η _ +₁ idC) ∘ g) # ⁂ idC) ∘ τ _ ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (strengthen.commute (((η (K.₀ X) +₁ idC) ∘ g) # , idC))) ⟩
+                  extend ψ ∘ extend (σ _) ∘ (τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ K.₁ idC)) ∘ (idC ⁂ ((η _ +₁ idC) ∘ h) #) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityʳ (elimˡ monadK.F.identity))) ⟩
+                  extend ψ ∘ extend (σ _) ∘ τ _ ∘ (((η _ +₁ idC) ∘ g) # ⁂ ((η _ +₁ idC) ∘ h) #) ∎
                   where
                     by-uni : ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ ((g #) ⁂ idC) ≈ (idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)
                     by-uni = begin 
@@ -225,4 +248,10 @@ KCommutative = record { commutes = commutes' }
                       (ψ +₁ idC) ∘ ((((g #) ⁂ idC) +₁ ((g #) ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (sym identityˡ) id-comm-sym ○ sym +₁∘+₁)) ⟩ 
                       (((idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ assoc² ⟩ 
                       (idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ∎
+                    comm : (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC) ∘ h) ≈ (τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)
+                    comm = sym (begin 
+                      (τ _ ∘ (idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²) ⟩ 
+                      (τ _ +₁ idC) ∘ ((idC ⁂ η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ (pullˡ ((+₁-cong₂ refl (sym (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ○ distribute₁ idC (η (K.₀ Y)) idC)) ⟩ 
+                      (τ _ +₁ idC) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC))) ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩ 
+                      (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (η _ +₁ idC) ∘ h) ∎)
 ```

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

@@ -0,0 +1,51 @@
+<!--
+```agda 
+open import Level
+open import Category.Instance.AmbientCategory
+open import Categories.Category
+open import Categories.Category.Instance.Setoids
+open import Categories.Monad
+open import Categories.Category.Monoidal.Instance.Setoids
+open import Categories.Category.Cocartesian
+open import Categories.Object.Terminal
+open import Function.Equality as SΠ renaming (id to ⟶-id)
+import Categories.Morphism.Reasoning as MR
+open import Relation.Binary
+open import Agda.Builtin.Unit using (tt)
+
+```
+-->
+
+```agda
+module Monad.Instance.K.Instance.Maybe {o ℓ e} (ambient : Ambient o ℓ e) where
+open Ambient ambient using ()
+```
+
+# The Maybe Monad as instance of K
+Assuming the axiom of choice, the maybe monad is an instance of K in the category of setoids.
+
+```agda
+module _ {c ℓ' : Level} where
+  open Cocartesian (Setoids-Cocartesian {c} {c ⊔ ℓ'})
+  open Terminal (terminal {c} {c ⊔ ℓ'})
+  open MR (Setoids c (c ⊔ ℓ'))
+  open Category (Setoids c (c ⊔ ℓ'))
+  open Equiv
+  
+  maybe : Monad (Setoids c (c ⊔ ℓ'))
+  maybe = record
+    { F = record
+      { F₀ = λ X → X + ⊤ 
+      ; F₁ = λ {A} {B} f → f +₁ ⟶-id
+      ; identity = {!   !}
+      ; homomorphism = {!   !}
+      ; F-resp-≈ = λ {A} {B} {f} {g} f≈g → +₁-cong₂ f≈g ?
+      }
+    ; η = {!   !}
+    ; μ = {!   !}
+    ; assoc = {!   !}
+    ; sym-assoc = {!   !}
+    ; identityˡ = {!   !}
+    ; identityʳ = {!   !}
+    }
+```