src/Category/Instance/AmbientCategory.lagda.md

@@ -200,14 +200,4 @@ 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

@@ -7,7 +7,6 @@ open import Categories.Object.Terminal
 open import Categories.Functor.Algebra
 open import Categories.Object.Initial
 open import Categories.Object.NaturalNumbers.Properties.F-Algebras
-open import Categories.FreeObjects.Free
 -- open import Categories.Category.Restriction
 import Monad.Instance.K as MIK
 ```
@@ -27,9 +26,8 @@ module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK
 
   open MIK ambient
   open MonadK MK
-  open Terminal terminal using (⊤; !; !-unique)
+  open Terminal terminal using (⊤; !)
   open Initial using () renaming (! to ¡)
-  open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈)
 
   open HomReasoning
   open Equiv
@@ -41,43 +39,13 @@ First let's define bounded iteration via primitive recursion.
 Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A),  (f : X ⇒ A + X)#⟩ : X × ℕ ⇒ A
 
 ```agda
-  φ' : ∀ {X Y : Obj} → X ⇒ Y → Y × X × N ⇒ Y → X × N ⇒ Y × X × N
-  φ' {X} {Y} f g = universal {X = Y × X × N} ⟨ f , ⟨ idC , z ∘ ! ⟩ ⟩ ⟨ g , ⟨ π₁ ∘ π₂ , s ∘ π₂ ∘ π₂ ⟩ ⟩
-
   p-rec : ∀ {X Y : Obj} → X ⇒ Y → Y × X × N ⇒ Y → X × N ⇒ Y
-  p-rec {X} {Y} f g = π₁ ∘ φ' f g
-
-  p-rec-IB : ∀ {X Y : Obj} (f : X ⇒ Y) (g : Y × X × N ⇒ Y) → p-rec f g ∘ ⟨ idC , z ∘ ! ⟩ ≈ f
-  p-rec-IB {X} {Y} f g = (pullʳ (sym commute₁)) ○ project₁
-
-  p-rec-IS : ∀ {X Y : Obj} (f : X ⇒ Y) (g : Y × X × N ⇒ Y) → p-rec f g ∘ ( idC ⁂ s ) ≈ g ∘ φ' f g
-  p-rec-IS {X} {Y} f g = (pullʳ (sym commute₂)) ○ pullˡ project₁
-
-  p-induction : ∀ {X Y : Obj} (f : X ⇒ Y) (g : Y × X × N ⇒ Y) (w : X × N ⇒ Y) → f ≈ w ∘ ⟨ idC , z ∘ ! ⟩ → g ∘ ⟨ w , idC ⟩ ≈ w ∘ (idC ⁂ s) → p-rec f g ≈ w
-  p-induction {X} {Y} f g w eq₁ eq₂ = begin 
-    π₁ ∘ φ' f g ≈⟨ refl⟩∘⟨ (sym (unique zero₁ succ₁)) ⟩
-    π₁ ∘ w' ≈⟨ project₁ ⟩
-    w ∎
-    where
-      w' : X × N ⇒ Y × X × N
-      w' = ⟨ w , idC ⟩
-      zero₁ : ⟨ f , ⟨ idC , z ∘ ! ⟩ ⟩ ≈ w' ∘ ⟨ idC , z ∘ ! ⟩
-      zero₁ = sym (begin 
-        w' ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ ⟨⟩∘ ⟩ 
-        ⟨ w ∘ ⟨ idC , z ∘ ! ⟩ , idC ∘ ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ (sym eq₁) identityˡ ⟩ 
-        ⟨ f , ⟨ idC , z ∘ ! ⟩ ⟩ ∎)
-      succ₁ : ⟨ g , ⟨ π₁ ∘ π₂ , s ∘ π₂ ∘ π₂ ⟩ ⟩ ∘ ⟨ w , idC ⟩ ≈ ⟨ w , idC ⟩ ∘ (idC ⁂ s)
-      succ₁ = begin 
-        ⟨ g , ⟨ π₁ ∘ π₂ , s ∘ π₂ ∘ π₂ ⟩ ⟩ ∘ ⟨ w , idC ⟩ ≈⟨ ⟨⟩∘ ⟩ 
-        ⟨ g ∘ ⟨ w , idC ⟩ , ⟨ π₁ ∘ π₂ , s ∘ π₂ ∘ π₂ ⟩ ∘ ⟨ w , idC ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ refl ⟨⟩∘ ⟩ 
-        ⟨ g ∘ ⟨ w , idC ⟩ , ⟨ (π₁ ∘ π₂) ∘ ⟨ w , idC ⟩ , (s ∘ π₂ ∘ π₂) ∘ ⟨ w , idC ⟩ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ eq₂ (⟨⟩-cong₂ (cancelʳ project₂) (pullʳ (cancelʳ project₂))) ⟩ 
-        ⟨ w ∘ (idC ⁂ s) , ⟨ π₁ , s ∘ π₂ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ refl (⟨⟩-cong₂ (sym identityˡ) refl ○ sym ⁂∘⟨⟩) ⟩ 
-        ⟨ w ∘ (idC ⁂ s) , (idC ⁂ s) ∘ ⟨ π₁ , π₂ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ refl (elimʳ ⁂-η) ⟩ 
-        ⟨ w ∘ (idC ⁂ s) , (idC ⁂ s) ⟩ ≈⟨ ⟨⟩-cong₂ refl (sym identityˡ) ○ sym ⟨⟩∘ ⟩ 
-        ⟨ w , idC ⟩ ∘ (idC ⁂ s) ∎
+  p-rec {X} {Y} f g = π₁ ∘ universal {X = Y × X × N} ⟨ f , ⟨ idC , z ∘ ! ⟩ ⟩ ⟨ g , ⟨ π₁ ∘ π₂ , π₂ ∘ π₂ ⟩ ⟩
+  -- TODO induction, see proposition 2.3 https://ncatlab.org/nlab/show/natural+numbers+object
 
   [_,_]#⟩ : ∀ {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)
@@ -123,28 +91,15 @@ 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 ⟩ ≈⟨ (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 ⟩
+    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 ⟩ ⟩ ≈⟨ {!   !} ⟩
     ((η.η X) ⇂ (f ↓)) ∎
 
   -- some helper definitions to make our life easier
@@ -153,38 +108,7 @@ 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
 
-  τ-strict : ∀ {X Y Z} → τ (X , Y) ∘ (idC ⁂ (i₂ #) ∘ ! {A = Z}) ≈ i₂ # ∘ !
-  τ-strict {X} {Y} {Z} = begin 
-    τ (X , Y) ∘ (idC ⁂ (i₂ #) ∘ ! {A = Z}) ≈⟨ refl⟩∘⟨ ((⁂-cong₂ (sym identity²) refl) ○ sym ⁂∘⁂) ⟩ 
-    τ (X , Y) ∘ (idC ⁂ i₂ #) ∘ (idC ⁂ ! {A = Z}) ≈⟨ pullˡ (τ-comm i₂) ⟩ 
-    ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂)) # ∘ (idC ⁂ !) ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ dstr-law₂) ⟩∘⟨refl ⟩ 
-    ((τ _ +₁ idC) ∘ i₂) # ∘ (idC ⁂ !) ≈⟨ (#-resp-≈ (algebras _) (+₁∘i₂ ○ identityʳ)) ⟩∘⟨refl ⟩ 
-    i₂ # ∘ (idC ⁂ !) ≈⟨ sym (#-Uniformity (algebras _) +₁∘i₂) ⟩
-    (i₂ #) ≈⟨ #-Uniformity (algebras _) +₁∘i₂ ⟩
-    (i₂ #) ∘ ! ∎
-
-  ∘-right-strict : ∀ {X Y Z} (f : X ⇒ K.₀ Y) → extend f ∘ (i₂ #) ∘ ! {A = Z} ≈ (i₂ #) ∘ !
-  ∘-right-strict {X} {Y} f = begin 
-    extend f ∘ i₂ # ∘ ! ≈⟨ pullˡ (pullʳ (Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) _))) ⟩ 
-    (μ.η _ ∘ (_ #)) ∘ ! ≈⟨ (refl⟩∘⟨ #-resp-≈ (algebras _) (inject₂ ○ identityʳ)) ⟩∘⟨refl ⟩ 
-    (μ.η _ ∘ i₂ #) ∘ ! ≈⟨ (Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC)) ⟩∘⟨refl ⟩ 
-    _ # ∘ ! ≈⟨ (#-resp-≈ (algebras _) (inject₂ ○ identityʳ)) ⟩∘⟨refl ⟩ 
-    i₂ # ∘ ! ∎ 
-
-  kleene₁ : ∀ {X Y} (f : X ⇒ K.₀ Y + X) → ([ i₂ # , f ]#⟩) ⊑ (f # ∘ π₁)
-  kleene₁ {X} {Y} f = p-induction ((i₂ #) ∘ !) ([ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) (((f #) ∘ π₁) ⇂ [ i₂ # , f ]#⟩) IB {!   !}
-    where
-      IB : i₂ # ∘ ! ≈ (extend π₁ ∘ τ _ ∘ ⟨ ((f #) ∘ π₁) , [ i₂ # , f ]#⟩ ⟩) ∘ ⟨ idC , z ∘ ! ⟩
-      IB = sym (begin 
-        (extend π₁ ∘ τ _ ∘ ⟨ ((f #) ∘ π₁) , [ i₂ # , f ]#⟩ ⟩) ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ pullʳ (pullʳ ⟨⟩∘) ⟩ 
-        extend π₁ ∘ τ _ ∘ ⟨ ((f #) ∘ π₁) ∘ ⟨ idC , z ∘ ! ⟩ , [ i₂ # , f ]#⟩ ∘ ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (cancelʳ project₁) (p-rec-IB ((i₂ #) ∘ !) ([ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁))) ⟩ 
-        extend π₁ ∘ τ _ ∘ ⟨ f # , i₂ # ∘ ! ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) ⟩ 
-        extend π₁ ∘ τ _ ∘ (idC ⁂ i₂ # ∘ !) ∘ ⟨ f # , idC ⟩ ≈⟨ refl⟩∘⟨ (pullˡ τ-strict) ⟩
-        extend π₁ ∘ (i₂ # ∘ !) ∘ ⟨ f # , idC ⟩ ≈⟨ pullˡ (∘-right-strict π₁) ⟩ 
-        (i₂ # ∘ !) ∘ ⟨ f # , idC ⟩ ≈⟨ pullʳ (sym (!-unique (! ∘ ⟨ f # , idC ⟩))) ⟩ 
-        (i₂ #) ∘ ! ∎)
-
-  kleene₂ : ∀ {X Y} (f : X ⇒ K.₀ Y + X) (g : X ⇒ K.₀ Y) → ([ i₂ # , f ]#⟩) ⊑ (g ∘ π₁) → (f #) ⊑ g
-  kleene₂ = {!   !}
+  kleene : ∀ {X Y} (f : X ⇒ K.₀ Y + X) (g : X ⇒ K.₀ Y) → ([ i₂ # , f ]#⟩) ⊑ (f # ∘ π₁) → ([ i₂ # , f ]#⟩) ⊑ (g ∘ π₁) → (f #) ⊑ g
+  kleene = {!   !}
   
 ```