work on proofs

src/Algebra/Elgot.lagda.md

@@ -112,12 +112,54 @@ Here we give a different Characterization and show that it is equal.
       ⟩
       ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂  ∎
 
+    #-Stutter : ∀ {X Y} (f : X ⇒ (Y + Y) + X) (h : Y ⇒ A) → (([ h , h ] +₁ idC) ∘ f)# ≈ [ i₁ ∘ h , [ h +₁ i₁ , i₂ ∘ i₂ ] ∘ f ] # ∘ i₂
+    #-Stutter {X} {Y} f h = begin 
+      (([ h , h ] +₁ idC) ∘ f)# ≈⟨ #-resp-≈ ((+₁-cong₂ (sym help) refl) ⟩∘⟨refl) ⟩ 
+      (((h +₁ i₁) # +₁ idC) ∘ f) # ≈⟨ #-Compositionality ⟩
+      ([ (idC +₁ i₁) ∘ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) # ∘ i₂ ≈⟨ ((#-resp-≈ (([]-cong₂ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl) refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩
+      ([ (h +₁ i₁ ∘ i₁) , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) # ∘ i₂ ≈˘⟨ (refl⟩∘⟨ (+₁∘i₂ ○ identityʳ)) ⟩
+      ([ (h +₁ i₁ ∘ i₁) , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) # ∘ (i₁ +₁ idC) ∘ i₂ ≈⟨ pullˡ (sym (#-Uniformity (sym by-uni))) ⟩
+      [ i₁ ∘ h , [ h +₁ i₁ , i₂ ∘ i₂ ] ∘ f ] # ∘ i₂ ∎
+      where
+        help : (h +₁ i₁) # ≈ [ h , h ]
+        help = begin 
+          ((h +₁ i₁) #) ≈⟨ #-Fixpoint ⟩ 
+          [ idC , (h +₁ i₁) # ] ∘ (h +₁ i₁) ≈⟨ []∘+₁ ○ []-cong₂ identityˡ refl ⟩ 
+          [ h , (h +₁ i₁) # ∘ i₁ ] ≈⟨ []-cong₂ refl (#-Fixpoint ⟩∘⟨refl) ⟩ 
+          [ h , ([ idC , (h +₁ i₁) # ] ∘ (h +₁ i₁)) ∘ i₁ ] ≈⟨ []-cong₂ refl (pullʳ +₁∘i₁) ⟩ 
+          [ h , [ idC , (h +₁ i₁) # ] ∘ i₁ ∘ h ] ≈⟨ []-cong₂ refl (cancelˡ inject₁) ⟩ 
+          [ h , h ] ∎
+        by-uni : ([ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) ∘ (i₁ +₁ idC) ≈ (idC +₁ (i₁ +₁ idC)) ∘ [ i₁ ∘ h , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ]
+        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 ] ≈⟨ {!   !} ⟩ 
+          [ (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 , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ] ∎
+
     -- TODO Proposition 41
     #-Diamond : ∀ {X} (f : X ⇒ A + (X + X)) → ((idC +₁ [ idC , idC ]) ∘ f)# ≈ ([ i₁ , ((idC +₁ [ idC , idC ]) ∘ f) # +₁ idC ] ∘ f) #
     #-Diamond {X} f = begin 
-      g # ≈⟨ {!   !} ⟩ 
+      g # ≈⟨ introʳ inject₂ ⟩ 
+      g # ∘ [ idC , idC ] ∘ i₂ ≈⟨ pullˡ (sym (#-Uniformity by-uni₁)) ⟩ 
+      [ (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
+      [ 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₂ ≈⟨ 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₂ ≈⟨ {!   !} ⟩ 
       {!   !} ≈⟨ {!   !} ⟩ 
       {!   !} ≈⟨ {!   !} ⟩ 
+      [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , [ i₂ ∘ i₁ ∘ i₁ , i₂ ∘ (i₂ +₁ idC) ] ∘ f ] # ∘ i₂ ≈˘⟨ ((#-resp-≈ ([]-cong₂ (∘[] ○ []-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl))) (pullˡ ∘[]))) ⟩∘⟨refl) ⟩ 
       [ (idC +₁ i₁) ∘ [ i₁ , (idC +₁ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ ≈⟨ (sym #-Folding) ⟩∘⟨refl ⟩ 
       ([ i₁ , (idC +₁ i₂) ∘ g ] # +₁ h)# ∘ i₂ ≈⟨ {!   !} ⟩ 
       {!   !} ≈⟨ {!   !} ⟩ 
@@ -125,6 +167,29 @@ Here we give a different Characterization and show that it is equal.
       where
         g = (idC +₁ [ idC , idC ]) ∘ f
         h = [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ f
+        by-uni₁ : (idC +₁ [ idC , idC ]) ∘ [ (idC +₁ i₁) ∘ g , f ] ≈ g ∘ [ idC , idC ]
+        by-uni₁ = begin 
+          (idC +₁ [ idC , idC ]) ∘ [ (idC +₁ i₁) ∘ g , f ] ≈⟨ ∘[] ⟩ 
+          [ (idC +₁ [ idC , idC ]) ∘ (idC +₁ i₁) ∘ g , (idC +₁ [ idC , idC ]) ∘ f ] ≈⟨ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² inject₁)) refl ⟩ 
+          [ (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₂ = begin 
+          [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ∘ i₂ ≈⟨ inject₂ ⟩ 
+          [ (idC +₁ i₂ ∘ i₁) ∘ g , 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 ] ≈⟨ {!   !} ⟩ 
+          {!   !} ≈⟨ {!   !} ⟩ 
+          {!   !} ≈⟨ {!   !} ⟩ 
+          {!   !} ∎
 
     -- every elgot-algebra comes with a divergence constant
     !ₑ : ⊥ ⇒ A

src/index.lagda.md

@@ -71,9 +71,10 @@ open import Monad.Instance.K.Commutative
 open import Monad.Instance.K.EquationalLifting
 ```
 
-and lastly we formalize the notion of *pre-Elgot monad* and show that **K** is the initial pre-Elgot monad.
+and lastly we formalize the notion of *pre-Elgot monad* and show that **K** is the initial (strong) pre-Elgot monad.
 
 ```agda
 open import Monad.PreElgot
 open import Monad.Instance.K.PreElgot
+open import Monad.Instance.K.StrongPreElgot
 ```