🚧 added proof by induction, started work on kleenes fixpoint theorem

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

@@ -7,6 +7,7 @@ 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
 ```
@@ -26,8 +27,9 @@ module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK
 
   open MIK ambient
   open MonadK MK
-  open Terminal terminal using (⊤; !)
+  open Terminal terminal using (⊤; !; !-unique)
   open Initial using () renaming (! to ¡)
+  open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈)
 
   open HomReasoning
   open Equiv
@@ -39,9 +41,40 @@ 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 = π₁ ∘ universal {X = Y × X × N} ⟨ f , ⟨ idC , z ∘ ! ⟩ ⟩ ⟨ g , ⟨ π₁ ∘ π₂ , π₂ ∘ π₂ ⟩ ⟩
-  -- TODO induction, see proposition 2.3 https://ncatlab.org/nlab/show/natural+numbers+object
+  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) ∎
 
   [_,_]#⟩ : ∀ {X A : Obj} → (⊤ ⇒ A) → X ⇒ A + X → X × N ⇒ A
   [_,_]#⟩ {X} {A} !! f = p-rec (!! ∘ !) ([ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁))
@@ -120,8 +153,36 @@ 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₁ = {!   !}
+  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₂ = {!   !}