Work on kleene fixpoint

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

@@ -1,26 +1,37 @@
 <!--
 ```agda
 open import Level
+open import Data.Product using (_,_)
 open import Category.Instance.AmbientCategory
 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.Category.Restriction
+import Monad.Instance.K as MIK
 ```
 -->
 
 
 
 ```agda
-module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) where
+module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
   open Ambient ambient
-  open import Monad.Instance.K ambient
+  open import Monad.Instance.K.Strong ambient MK
-  open import Monad.Instance.K.Strong ambient
+  open import Monad.Instance.K.Commutative ambient MK
-  open import Monad.Instance.K.Commutative ambient
+  open import Monad.Instance.K.EquationalLifting ambient MK
-  open import Monad.Instance.K.EquationalLifting ambient
+  open import Category.Construction.UniformIterationAlgebras ambient
+  open import Algebra.UniformIterationAlgebra ambient
+  open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
 
+  open MIK ambient
+  open MonadK MK
   open Terminal terminal using (⊤; !)
   open Initial using () renaming (! to ¡)
+
+  open HomReasoning
+  open Equiv
+  open MR C
 ```
 
 
@@ -33,7 +44,71 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A),  (f : X
   -- 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 ∘ π₁))
+  [_,_]#⟩ {X} {A} !! f = p-rec (!! ∘ !) ([ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁))
-  -- TODO might be wrong, check it by testing kleene fixpoint
+  -- TODO might be wrong, check it by testing kleene fixpoint ʳ 
+
+  -- Notation
+  open kleisliK using (extend)
+  open monadK using (η; μ)
+  open strongK using (strengthen)
+  _↓ : ∀ {X Y} (f : X ⇒ K.₀ Y) → X ⇒ K.₀ X
+  _↓ f = K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩
+
+  _⇂_ : ∀ {X Y Z} (f : X ⇒ K.₀ Y) (g : X ⇒ K.₀ Z) → X ⇒ K.₀ Y
+  _⇂_ {X} {Y} {Z} f g = extend π₁ ∘ τ (K.₀ Y , Z) ∘ ⟨ f , g ⟩
+
+  restrict-η : ∀ {X Y} (f : X ⇒ K.₀ Y) → f ↓ ≈ η.η _ ⇂ f
+  restrict-η {X} {Y} f = begin 
+    K.₁ π₁ ∘ τ (X , Y) ∘ ⟨ idC , f ⟩ ≈˘⟨ cancelˡ monadK.identityˡ ⟩∘⟨refl ⟩∘⟨refl ○ assoc ⟩ 
+    ((μ.η _ ∘ K.₁ (η.η _) ∘ K.₁ π₁) ∘ τ (X , Y)) ∘ ⟨ idC , f ⟩ ≈⟨ ((refl⟩∘⟨ (sym K.homomorphism)) ⟩∘⟨refl) ⟩∘⟨refl ⟩ 
+    ((μ.η _ ∘ K.₁ (η.η _ ∘ π₁)) ∘ τ (X , Y)) ∘ ⟨ idC , f ⟩ ≈⟨ ((refl⟩∘⟨ (K.F-resp-≈ (sym π₁∘⁂))) ⟩∘⟨refl) ⟩∘⟨refl ⟩ 
+    ((μ.η _ ∘ K.₁ (π₁ ∘ (η.η _ ⁂ idC))) ∘ τ (X , Y)) ∘ ⟨ idC , f ⟩ ≈˘⟨ pullˡ (pullˡ (pullʳ (sym K.homomorphism))) ⟩ 
+    (μ.η _ ∘ K.₁ π₁) ∘ (K.₁ (η.η _ ⁂ idC) ∘ τ (X , Y)) ∘ ⟨ idC , f ⟩ ≈⟨ refl ⟩ 
+    extend π₁ ∘ (K.₁ (η.η _ ⁂ idC) ∘ τ (X , Y)) ∘ ⟨ idC , f ⟩ ≈˘⟨ refl⟩∘⟨ pullˡ (strengthen.commute _) ⟩ 
+    extend π₁ ∘ τ (K.₀ X , Y) ∘ (η.η _ ⁂ K.₁ idC) ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂-cong₂ refl K.identity) ⟩∘⟨refl ⟩ 
+    extend π₁ ∘ τ (K.₀ X , Y) ∘ (η.η _ ⁂ idC) ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩ 
+    extend π₁ ∘ τ (K.₀ X , Y) ∘ ⟨ η.η _ , f ⟩ ∎
+  
+  restrict-law : ∀ {X Y Z} (f : X ⇒ K.₀ Y) (g : X ⇒ K.₀ Z) → f ⇂ g ≈ extend f ∘ g ↓
+  restrict-law {X} {Y} {Z} f g = begin 
+    extend π₁ ∘ τ (K.₀ Y , Z) ∘ ⟨ f , g ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩ 
+    extend π₁ ∘ τ (K.₀ Y , Z) ∘ (f ⁂ idC) ∘ ⟨ idC , g ⟩ ≈⟨ refl⟩∘⟨ (pullˡ (τ-comm-id f)) ⟩ 
+    extend π₁ ∘ (K.₁ (f ⁂ idC) ∘ τ (X , Z)) ∘ ⟨ idC , g ⟩ ≈⟨ (refl⟩∘⟨ assoc) ○ pullˡ (pullʳ (sym K.homomorphism)) ⟩ 
+    (μ.η _ ∘ K.₁ (π₁ ∘ (f ⁂ idC))) ∘ τ (X , Z) ∘ ⟨ idC , g ⟩ ≈⟨ (refl⟩∘⟨ ((K.F-resp-≈ π₁∘⁂) ○ K.homomorphism)) ⟩∘⟨refl ⟩ 
+    (μ.η Y ∘ (K.₁ f ∘ K.₁ π₁)) ∘ τ (X , Z) ∘ ⟨ idC , g ⟩ ≈⟨ sym-assoc ⟩∘⟨refl ○ assoc ⟩ 
+    extend f ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ idC , g ⟩ ∎
+
+  dom-η : ∀ {X Y} (f : X ⇒ K.₀ Y) → (η.η _ ∘ f) ↓ ≈ η.η _
+  dom-η {X} {Y} f = begin 
+    K.₁ π₁ ∘ τ _ ∘ ⟨ idC , η.η _ ∘ f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl) ⟩ 
+    K.₁ π₁ ∘ τ _ ∘ (idC ⁂ η.η _) ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ (pullˡ (τ-η _)) ⟩ 
+    K.₁ π₁ ∘ η.η _ ∘ ⟨ idC , f ⟩ ≈⟨ pullˡ (K₁η π₁) ⟩ 
+    (η.η _ ∘ π₁) ∘ ⟨ idC , f ⟩ ≈⟨ cancelʳ project₁ ⟩ 
+    η.η _ ∎
+
+  _⊑_ : ∀ {X Y} (f g : X ⇒ K.₀ Y) → Set e
+  f ⊑ g = f ≈ g ⇂ f
+
+  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 ⟩ ⟩ ≈⟨ {!   !} ⟩
+    ((η.η X) ⇂ (f ↓)) ∎
+
+  -- some helper definitions to make our life easier
+  private
+    _♯ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f
+    _♯ˡ = λ {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 = {!   !}
   
 ```

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

@@ -265,4 +265,14 @@ The following diagram demonstrates this:
     { M = monadK
     ; strength = KStrength
     }
+
+  τ-comm-id : ∀ {X Y Z} (f : X ⇒ Y) → τ (Y , Z) ∘ (f ⁂ idC) ≈ K.₁ (f ⁂ idC) ∘ τ (X , Z)
+  τ-comm-id {X} {Y} {Z} f = begin 
+    τ (Y , Z) ∘ (f ⁂ idC) ≈⟨ refl⟩∘⟨ (⁂-cong₂ refl (sym K.identity)) ⟩ 
+    τ (Y , Z) ∘ (f ⁂ K.₁ idC) ≈⟨ strengthen.commute (f , idC) ⟩ 
+    K.₁ (f ⁂ idC) ∘ τ (X , Z) ∎
+    where
+      open Strength KStrength using (strengthen)
+
+  module strongK = StrongMonad KStrong
 ```