Finished small proof

src/Category/Instance/AmbientCategory.lagda.md

@@ -200,4 +200,14 @@ module Category.Instance.AmbientCategory where
       μ.η _ ∘ F.₁ (η.η _) ∘ F.₁ f ≈⟨ cancelˡ m-identityˡ ⟩ 
       F.₁ f ∎
       where open Monad M using (F; η; μ) renaming (identityˡ to m-identityˡ)
+
+    extend∘F₁ : ∀ (M : Monad C) {X Y Z} (f : Y ⇒ Monad.F.₀ M Z) (g : X ⇒ Y) → RMonad.extend (Monad⇒Kleisli C M) f ∘ Monad.F.₁ M g ≈ RMonad.extend (Monad⇒Kleisli C M) (f ∘ g)
+    extend∘F₁ M f g = begin 
+      extend f ∘ F.₁ g ≈⟨ (refl⟩∘⟨ sym (F₁⇒extend M g)) ⟩ 
+      extend f ∘ extend (unit ∘ g) ≈⟨ k-sym-assoc ⟩ 
+      extend (extend f ∘ unit ∘ g) ≈⟨ extend-≈ (pullˡ k-identityʳ) ⟩ 
+      extend (f ∘ g) ∎
+      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ʳ)
 ```

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

@@ -45,7 +45,6 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A),  (f : X
 
   [_,_]#⟩ : ∀ {X A : Obj} → (⊤ ⇒ A) → X ⇒ A + X → X × N ⇒ A
   [_,_]#⟩ {X} {A} !! f = p-rec (!! ∘ !) ([ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁))
-  -- TODO might be wrong, check it by testing kleene fixpoint ʳ 
 
   -- Notation
   open kleisliK using (extend)
@@ -91,15 +90,28 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A),  (f : X
 
   dom-⊑ : ∀ {X Y} (f : X ⇒ K.₀ Y) → (f ↓) ⊑ (η.η _)
   dom-⊑ {X} {Y} f = begin 
-  -- TODO try with RST laws
     (f ↓) ≈⟨ refl ⟩
-    K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩ ≈⟨ {!   !} ⟩
-    {!   !} ≈⟨ {!   !} ⟩
-    {!   !} ≈⟨ {!   !} ⟩
-    extend π₁ ∘ τ _ ∘ ⟨ η.η X , τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈⟨ {!   !} ⟩ -- multiple steps
-    extend π₁ ∘ K.₁ (idC ⁂ π₁) ∘ τ _ ∘ ⟨ η.η X , τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈⟨ {!   !} ⟩
-    extend π₁ ∘ τ _ ∘ (idC ⁂ K.₁ π₁) ∘ ⟨ η.η X , τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈⟨ {!   !} ⟩
-    extend π₁ ∘ τ _ ∘ ⟨ η.η X , K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈⟨ {!   !} ⟩
+    K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩ ≈⟨ (sym (F₁⇒extend monadK π₁)) ⟩∘⟨refl ⟩
+    extend (η.η X ∘ π₁) ∘ τ _ ∘ ⟨ idC , f ⟩  ≈˘⟨ (kleisliK.extend-≈ (pullˡ project₁)) ⟩∘⟨refl ⟩ 
+    extend (π₁ ∘ ⟨ η.η X , idC ⟩ ∘ π₁) ∘ τ _ ∘ ⟨ idC , f ⟩ ≈˘⟨ (kleisliK.extend-≈ (pullʳ π₁∘⁂)) ⟩∘⟨refl ⟩ 
+    extend ((π₁ ∘ π₁) ∘ (⟨ η.η X , idC ⟩ ⁂ idC)) ∘ τ _ ∘ ⟨ idC , f ⟩ ≈˘⟨ pullˡ (extend∘F₁ monadK (π₁ ∘ π₁) (⟨ η.η X , idC ⟩ ⁂ idC)) ⟩ 
+    extend (π₁ ∘ π₁) ∘ K.₁ ((⟨ η.η X , idC ⟩ ⁂ idC)) ∘ τ _ ∘ ⟨ idC , f ⟩ ≈˘⟨ pullʳ (pullˡ (τ-comm-id ⟨ η.η X , idC ⟩) ○ assoc) ⟩ 
+    (extend (π₁ ∘ π₁) ∘ τ _) ∘ (⟨ η.η X , idC ⟩ ⁂ idC) ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩ 
+    (extend (π₁ ∘ π₁) ∘ τ _) ∘ ⟨ ⟨ η.η X , idC ⟩ , f ⟩ ≈˘⟨ ((kleisliK.extend-≈ project₁) ⟩∘⟨refl) ⟩∘⟨refl ⟩ 
+    (extend (π₁ ∘ assocˡ) ∘ τ _) ∘ ⟨ ⟨ η.η X , idC ⟩ , f ⟩ ≈˘⟨ (kleisliK.extend-≈ (pullˡ kleisliK.identityʳ)) ⟩∘⟨refl ⟩∘⟨refl ⟩ 
+    (extend (extend π₁ ∘ η.η _ ∘ assocˡ) ∘ τ _) ∘ ⟨ ⟨ η.η X , idC ⟩ , f ⟩ ≈˘⟨ pullˡ (pullˡ kleisliK.sym-assoc) ⟩ 
+    extend π₁ ∘ (extend (η.η _ ∘ assocˡ) ∘ τ _) ∘ ⟨ ⟨ η.η X , idC ⟩ , f ⟩ ≈⟨ refl⟩∘⟨ ((F₁⇒extend monadK assocˡ ⟩∘⟨refl) ⟩∘⟨refl) ⟩ 
+    extend π₁ ∘ (K.₁ assocˡ ∘ τ _) ∘ ⟨ ⟨ η.η X , idC ⟩ , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (⟨⟩-cong₂ (elimʳ project₁) refl) refl ⟩ 
+    extend π₁ ∘ (K.₁ assocˡ ∘ τ _) ∘ ⟨ ⟨ η.η X ∘ π₁ ∘ ⟨ idC , f ⟩ , idC ⟩ , f ⟩ ≈˘⟨ refl⟩∘⟨ (sym-assoc ○ pullˡ (assoc ○ sym strongK.strength-assoc)) ⟩ 
+    extend π₁ ∘ τ _ ∘ (idC ⁂ τ _) ∘ assocˡ ∘ ⟨ ⟨ η.η X ∘ π₁ ∘ ⟨ idC , f ⟩ , idC ⟩ , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ assocʳ∘⟨⟩ ⟩ 
+    extend π₁ ∘ τ _ ∘ (idC ⁂ τ _) ∘ (assocˡ ∘ assocʳ) ∘ ⟨ η.η X ∘ π₁ ∘ ⟨ idC , f ⟩ , ⟨ idC , f ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ elimˡ assocˡ∘assocʳ ⟩ 
+    extend π₁ ∘ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ η.η X ∘ π₁ ∘ ⟨ idC , f ⟩ , ⟨ idC , f ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ (⟨⟩-cong₂ identityˡ refl)) ⟩ 
+    extend π₁ ∘ τ _ ∘ ⟨ η.η X ∘ π₁ ∘ ⟨ idC , f ⟩ , τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (elimʳ project₁) refl ⟩
+    extend π₁ ∘ τ _ ∘ ⟨ η.η X , τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈⟨ (sym (kleisliK.extend-≈ (π₁∘⁂ ○ identityˡ))) ⟩∘⟨refl ⟩ -- multiple steps
+    extend (π₁ ∘ (idC ⁂ π₁)) ∘ τ _ ∘ ⟨ η.η X , τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈˘⟨ pullˡ (extend∘F₁ monadK π₁ (idC ⁂ π₁)) ⟩
+    extend π₁ ∘ K.₁ (idC ⁂ π₁) ∘ τ _ ∘ ⟨ η.η X , τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈⟨ refl⟩∘⟨ (pullˡ (sym (strengthen.commute (idC , π₁))) ○ assoc) ⟩
+    extend π₁ ∘ τ _ ∘ (idC ⁂ K.₁ π₁) ∘ ⟨ η.η X , τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩
+    extend π₁ ∘ τ _ ∘ ⟨ η.η X , K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩ ⟩ ≈⟨ refl ⟩
     ((η.η X) ⇂ (f ↓)) ∎
 
   -- some helper definitions to make our life easier
@@ -108,7 +120,10 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A),  (f : X
     _♯ˡ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ˡ {Y = X} (stable X) {X = A} (algebras Y) f
     _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f
 
-  kleene : ∀ {X Y} (f : X ⇒ K.₀ Y + X) (g : X ⇒ K.₀ Y) → ([ i₂ # , f ]#⟩) ⊑ (f # ∘ π₁) → ([ i₂ # , f ]#⟩) ⊑ (g ∘ π₁) → (f #) ⊑ g
-  kleene = {!   !}
+  kleene₁ : ∀ {X Y} (f : X ⇒ K.₀ Y + X) → ([ i₂ # , f ]#⟩) ⊑ (f # ∘ π₁)
+  kleene₁ = {!   !}
+
+  kleene₂ : ∀ {X Y} (f : X ⇒ K.₀ Y + X) (g : X ⇒ K.₀ Y) → ([ i₂ # , f ]#⟩) ⊑ (g ∘ π₁) → (f #) ⊑ g
+  kleene₂ = {!   !}
   
 ```