From 4d052891cd7df7ffb3cbb03c37f48b500a2b856b Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Sat, 11 Nov 2023 15:44:16 +0100
Subject: [PATCH] minor

---
 src/Monad/Instance/K/PreElgot.lagda.md | 33 +++++++++++++++-----------
 1 file changed, 19 insertions(+), 14 deletions(-)

diff --git a/src/Monad/Instance/K/PreElgot.lagda.md b/src/Monad/Instance/K/PreElgot.lagda.md
index 4b5c15c..2f61ec3 100644
--- a/src/Monad/Instance/K/PreElgot.lagda.md
+++ b/src/Monad/Instance/K/PreElgot.lagda.md
@@ -476,20 +476,6 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A),  (f : X
       w' = p-rec idC {! case ? inl ? inr ?  !} -- ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) 
       w : X × N ⇒ X
       w = universal idC (case f inl π₁ inr π₂) --([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩)
-
-      ww' : w' ∘ (idC ⁂ s) ≈ w
-      ww' = unique (sym IB) {!   !}
-        where
-          IB : (w' ∘ (idC ⁂ s)) ∘ ⟨ idC , z ∘ ! ⟩ ≈ idC
-          IB = begin 
-            (w' ∘ (idC ⁂ s)) ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ (p-rec-IS idC _) ⟩∘⟨refl ⟩ 
-            (([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _) ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ pullʳ (sym commute₁) ⟩ 
-            ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ ⟨ idC , ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ pullʳ (pullʳ ⁂∘⟨⟩) ⟩ 
-            [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC ∘ idC , (f ∘ π₁) ∘ ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ identity² (cancelʳ project₁) ⟩ 
-            [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈⟨ {!   !} ⟩ 
-            (case f inl π₁ inr π₂) ≈⟨ {!   !} ⟩ 
-            {!   !} ≈⟨ {!   !} ⟩ 
-            idC ∎
         
       -- TODO this depends on (8) and (9)
       stronger : ((extend [ i₂ # , f ]#⟩ ∘ τ (X , N) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ ⟨ π₁ , ⟨ w , π₂ ⟩ ⟩ ≈ f # ∘ w
@@ -498,6 +484,25 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A),  (f : X
         ((π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ idC ⁂ s , f ∘ w ⟩ )# ≈⟨ #-Uniformity (algebras _) by-uni₂ ⟩ 
         f # ∘ w ∎
         where
+          f#⟩-fact : [ i₂ # , f ]#⟩ ∘ (idC ⁂ s) ≈ case (f ∘ w) inl π₂ inr (i₂ #)
+          f#⟩-fact = begin 
+            [ i₂ # , f ]#⟩ ∘ (idC ⁂ s) ≈⟨ {!   !} ⟩
+            universal (case f inl (π₂) inr (i₂ #)) {!  case f inl ? inr ? !} ≈⟨ sym (unique (sym IB₁) (sym IS₁)) ⟩
+            (case (f ∘ w) inl π₂ inr (i₂ #)) ∎
+            where
+              IB₁ : (case f ∘ w inl π₂ inr (i₂ #)) ∘ ⟨ idC , z ∘ ! ⟩ ≈ case f inl (π₂) inr (i₂ #)
+              IB₁ = begin 
+                (case f ∘ w inl π₂ inr (i₂ #)) ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ case∘ʳ (f ∘ w) π₂ (i₂ #) ⟨ idC , z ∘ ! ⟩ ⟩ 
+                (case (f ∘ w) ∘ ⟨ idC , z ∘ ! ⟩ inl (π₂ ∘ (⟨ idC , z ∘ ! ⟩ ⁂ idC)) inr (i₂ # ∘ (⟨ idC , z ∘ ! ⟩ ⁂ idC))) ≈⟨ (case⟩ (cancelʳ (sym commute₁)) ⟨inl⟩ (π₂∘⁂ ○ identityˡ) ⟨inr⟩ {!   !}) ⟩ 
+                (case f inl (π₂) inr (i₂ #)) ∎
+              IS₁ : (case f ∘ w inl π₂ inr (i₂ #)) ∘ (idC ⁂ s) ≈ {!  (case f inl π₂ inr (i₂ #)) ∘ w !} ∘ (case f ∘ w inl π₂ inr (i₂ #))
+              IS₁ = begin 
+                (case f ∘ w inl π₂ inr (i₂ #)) ∘ (idC ⁂ s) ≈⟨ case∘ʳ (f ∘ w) π₂ (i₂ #) (idC ⁂ s) ⟩ 
+                (case ((f ∘ w) ∘ (idC ⁂ s)) inl (π₂ ∘ ((idC ⁂ s) ⁂ idC)) inr ((i₂ #) ∘ ((idC ⁂ s) ⁂ idC))) ≈⟨ (case⟩ (pullʳ (sym commute₂)) ⟨inl⟩ (π₂∘⁂ ○ identityˡ) ⟨inr⟩ {!   !}) ⟩ 
+                (case (f ∘ (case f inl π₁ inr π₂) ∘ w) inl (π₂) inr (i₂ #)) ≈⟨ {!   !} ⟩ 
+                {!   !} ≈⟨ {!   !} ⟩ 
+                {!   !} ≈⟨ {!   !} ⟩ 
+                {!   !} ∎
           by-uni₁ : (idC +₁ ⟨ π₁ , ⟨ w , π₂ ⟩ ⟩) ∘ (π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ idC ⁂ s , f ∘ w ⟩ ≈ ((extend [ i₂ # , f ]#⟩ ∘ τ (X , N) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ ⟨ π₁ , ⟨ w , π₂ ⟩ ⟩
           by-uni₁ = {!   !}
           by-uni₂ : (idC +₁ w) ∘ (π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ idC ⁂ s , f ∘ w ⟩ ≈ f ∘ w