Work on kleene

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

@@ -47,6 +47,9 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A),  (f : X
   p-rec : ∀ {X Y : Obj} → X ⇒ Y → Y × X × N ⇒ Y → X × N ⇒ Y
   p-rec {X} {Y} f g = π₁ ∘ φ' f g
 
+  φ'-charac : ∀ {X Y : Obj} (f : X ⇒ Y) (g : Y × X × N ⇒ Y) → φ' f g ≈ ⟨ p-rec f g , ⟨ π₁ , π₂ ⟩ ⟩
+  φ'-charac = {!   !}
+
   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₁
 
@@ -85,9 +88,13 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A),  (f : X
   open strongK using (strengthen)
   _↓ : ∀ {X Y} (f : X ⇒ K.₀ Y) → X ⇒ K.₀ X
   _↓ f = K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩
+  ↓-cong : ∀ {X Y} {f g : X ⇒ K.₀ Y} → f ≈ g → f ↓ ≈ g ↓
+  ↓-cong eq = refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl eq
 
   _⇂_ : ∀ {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 ⟩
+  ⇂-cong₂ : ∀ {X Y Z} {f h : X ⇒ K.₀ Y} {g i : X ⇒ K.₀ Z} → f ≈ h → g ≈ i → f ⇂ g ≈ h ⇂ i
+  ⇂-cong₂ eq₁ eq₂ = refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ eq₁ eq₂
 
   restrict-η : ∀ {X Y} (f : X ⇒ K.₀ Y) → f ↓ ≈ η.η _ ⇂ f
   restrict-η {X} {Y} f = begin 
@@ -110,6 +117,35 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A),  (f : X
     (μ.η Y ∘ (K.₁ f ∘ K.₁ π₁)) ∘ τ (X , Z) ∘ ⟨ idC , g ⟩ ≈⟨ sym-assoc ⟩∘⟨refl ○ assoc ⟩ 
     extend f ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ idC , g ⟩ ∎
 
+  ⇂-assoc : ∀ {X Y Z A} {f : X ⇒ K.₀ Y} {g : X ⇒ K.₀ Z} {h : X ⇒ K.₀ A} → (f ⇂ g) ⇂ h ≈ f ⇂ (g ⇂ h)
+  ⇂-assoc {X} {Y} {Z} {A} {f} {g} {h} = begin 
+    (f ⇂ g) ⇂ h ≈⟨ ⇂-cong₂ (restrict-law f g) refl ⟩
+    ((extend f ∘ g ↓) ⇂ h) ≈⟨ restrict-law (extend f ∘ (g ↓)) h ⟩ 
+    extend (extend f ∘ g ↓) ∘ h ↓ ≈⟨ pushˡ kleisliK.assoc ⟩ 
+    extend f ∘ extend (g ↓) ∘ h ↓ ≈˘⟨ refl⟩∘⟨ {!   !} ⟩ -- TODO RST₃
+    extend f ∘ (extend g ∘ h ↓) ↓ ≈˘⟨ refl⟩∘⟨ ↓-cong (restrict-law g h) ⟩ 
+    extend f ∘ (g ⇂ h) ↓ ≈˘⟨ restrict-law f (g ⇂ h) ⟩ 
+    f ⇂ (g ⇂ h) ∎
+
+  ⇂∘ : ∀ {A X Y Z} {f : X ⇒ K.₀ Y} {g : X ⇒ K.₀ Z} {h : A ⇒ X} → (f ⇂ g) ∘ h ≈ (f ∘ h) ⇂ (g ∘ h)
+  ⇂∘ {A} {X} {Y} {Z} {f} {g} {h} = pullʳ (pullʳ ⟨⟩∘)
+
+  extend-⇂ : ∀ {X Y Z} {f : X ⇒ K.₀ Y} {g : X ⇒ K.₀ Z} → extend (f ⇂ g) ≈ (extend f) ⇂ (extend g)
+  extend-⇂ {X} {Y} {Z} {f} {g} = begin 
+    extend (f ⇂ g) ≈⟨ kleisliK.extend-≈ (restrict-law f g) ⟩ 
+    extend (extend f ∘ (g ↓)) ≈⟨ kleisliK.assoc ⟩ 
+    extend f ∘ extend (g ↓) ≈⟨ {!   !} ⟩ 
+    {!   !} ≈⟨ {!   !} ⟩
+    {!   !} ≈⟨ {!   !} ⟩
+    {!   !} ≈˘⟨ {! kleisliK.sym-assoc  !} ⟩ 
+    extend (extend f) ∘ ((extend g) ↓) ≈˘⟨ restrict-law (extend f) (extend g) ⟩ 
+    (extend f ⇂ extend g) ∎
+    -- extend (extend π₁ ∘ τ (K.₀ Y , Z) ∘ ⟨ f , g ⟩) ≈⟨ kleisliK.assoc ⟩ 
+    -- extend π₁ ∘ extend (τ (K.₀ Y , Z) ∘ ⟨ f , g ⟩) ≈⟨ {!   !} ⟩ 
+    -- {!   !} ≈⟨ {!   !} ⟩ 
+    -- {!   !} ≈⟨ {!   !} ⟩ 
+    -- extend π₁ ∘ τ (K.₀ Y , Z) ∘ ⟨ extend f , extend g ⟩ ∎
+
   dom-η : ∀ {X Y} (f : X ⇒ K.₀ Y) → (η.η _ ∘ f) ↓ ≈ η.η _
   dom-η {X} {Y} f = begin 
     K.₁ π₁ ∘ τ _ ∘ ⟨ idC , η.η _ ∘ f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl) ⟩ 
@@ -121,6 +157,37 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A),  (f : X
   _⊑_ : ∀ {X Y} (f g : X ⇒ K.₀ Y) → Set e
   f ⊑ g = f ≈ g ⇂ f
 
+  ⊑∘ˡ : ∀ {A X Y} {f g : X ⇒ K.₀ Y} {h : A ⇒ X} → f ⊑ g → (f ∘ h) ⊑ (g ∘ h)
+  ⊑∘ˡ {A} {X} {Y} {f} {g} {h} leq = begin 
+    f ∘ h ≈⟨ leq ⟩∘⟨refl ⟩ 
+    (g ⇂ f) ∘ h ≈⟨ ⇂∘ ⟩ 
+    ((g ∘ h) ⇂ (f ∘ h)) ∎
+
+  extend-⊑ : ∀ {X Y} {f g : X ⇒ K.₀ Y} → f ⊑ g → extend f ⊑ extend g
+  extend-⊑ {X} {Y} {f} {g} fg = begin 
+    extend f ≈⟨ kleisliK.extend-≈ fg ⟩ 
+    extend (g ⇂ f) ≈⟨ extend-⇂ ⟩ 
+    (extend g ⇂ extend f) ∎
+
+  ⊑-cong₂ : ∀ {X Y} {f g h i : X ⇒ K.₀ Y} → f ≈ h → g ≈ i → f ⊑ g → h ⊑ i
+  ⊑-cong₂ eq₁ eq₂ leq = (sym eq₁) ○ leq ○ ⇂-cong₂ eq₂ eq₁
+
+  ⊑-refl : ∀ {X Y} {f : X ⇒ K.₀ Y} → f ⊑ f
+  ⊑-refl {X} {Y} {f} = sym (begin 
+    extend π₁ ∘ τ _ ∘ ⟨ f , f ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym Δ∘ ⟩ 
+    extend π₁ ∘ τ _ ∘ Δ ∘ f ≈⟨ refl⟩∘⟨ (pullˡ equationalLifting) ⟩ 
+    extend π₁ ∘ K.₁ ⟨ η.η _ , idC ⟩ ∘ f ≈⟨ pullˡ (extend∘F₁ monadK π₁ ⟨ η.η Y , idC ⟩) ⟩ 
+    extend (π₁ ∘ ⟨ η.η _ , idC ⟩) ∘ f ≈⟨ (kleisliK.extend-≈ project₁) ⟩∘⟨refl ⟩
+    extend (η.η _) ∘ f ≈⟨ elimˡ kleisliK.identityˡ ⟩
+    f ∎)
+
+  ⊑-trans : ∀ {X Y} {f g h : X ⇒ K.₀ Y} → f ⊑ g → g ⊑ h → f ⊑ h
+  ⊑-trans {X} {Y} {f} {g} {h} leq₁ leq₂ = begin 
+    f ≈⟨ leq₁ ⟩ 
+    (g ⇂ f) ≈⟨ ⇂-cong₂ leq₂ refl ⟩ 
+    ((h ⇂ g) ⇂ f) ≈⟨ ⇂-assoc ○ ⇂-cong₂ refl (sym leq₁) ⟩ 
+    (h ⇂ f) ∎
+
   dom-⊑ : ∀ {X Y} (f : X ⇒ K.₀ Y) → (f ↓) ⊑ (η.η _)
   dom-⊑ {X} {Y} f = begin 
     (f ↓) ≈⟨ refl ⟩
@@ -172,7 +239,7 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A),  (f : X
     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 {!   !}
+  kleene₁ {X} {Y} f = p-induction ((i₂ #) ∘ !) ([ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) (((f #) ∘ π₁) ⇂ [ i₂ # , f ]#⟩) IB IS
     where
       IB : i₂ # ∘ ! ≈ (extend π₁ ∘ τ _ ∘ ⟨ ((f #) ∘ π₁) , [ i₂ # , f ]#⟩ ⟩) ∘ ⟨ idC , z ∘ ! ⟩
       IB = sym (begin 
@@ -183,8 +250,88 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A),  (f : X
         extend π₁ ∘ (i₂ # ∘ !) ∘ ⟨ f # , idC ⟩ ≈⟨ pullˡ (∘-right-strict π₁) ⟩ 
         (i₂ # ∘ !) ∘ ⟨ f # , idC ⟩ ≈⟨ pullʳ (sym (!-unique (! ∘ ⟨ f # , idC ⟩))) ⟩ 
         (i₂ #) ∘ ! ∎)
+      IS : ([ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ ⟨ ((f #) ∘ π₁) ⇂ [ i₂ # , f ]#⟩ , idC ⟩ ≈ (((f #) ∘ π₁) ⇂ [ i₂ # , f ]#⟩) ∘ (idC ⁂ s)
+      IS = begin 
+        ([ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ ⟨ ((f #) ∘ π₁) ⇂ [ i₂ # , f ]#⟩ , idC ⟩ ≈⟨ pullʳ (pullʳ ⁂∘⟨⟩) ⟩ 
+        [ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC ∘ ((f #) ∘ π₁) ⇂ [ i₂ # , f ]#⟩ , (f ∘ π₁) ∘ idC ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ identityˡ identityʳ ⟩ 
+        [ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ extend π₁ ∘ τ _ ∘ ⟨ (f #) ∘ π₁ , [ i₂ # , f ]#⟩ ⟩ , f ∘ π₁ ⟩ ≈⟨ {!   !} ⟩ 
+        [ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ extend π₁ ∘ τ _ ∘ ((f #) ∘ π₁ ⁂ idC) ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ , f ∘ π₁ ⟩ ≈⟨ {!   !} ⟩ 
+        [ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (extend π₁ ∘ τ _ ∘ ((f #) ∘ π₁ ⁂ idC) ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ⁂ idC) ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {!   !} ⟩ 
+        [ π₂ ∘ (extend π₁ ∘ τ _ ∘ ((f #) ∘ π₁ ⁂ idC) ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ⁂ idC) , π₁ ∘ (extend π₁ ∘ τ _ ∘ ((f #) ∘ π₁ ⁂ idC) ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {!   !} ⟩ 
+        [ π₂ , (extend π₁ ∘ τ _ ∘ ((f #) ∘ π₁ ⁂ idC) ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩) ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {!   !} ⟩ 
+        [ π₂ , extend π₁ ∘ τ _ ] ∘ (idC +₁ ((f #) ∘ π₁ ⁂ idC) ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {!   !} ⟩ 
+        [ π₂ {A = X × N} , extend π₁ ∘ τ _ ] ∘ (idC +₁ ((f #) ∘ π₁ ⁂ idC)) ∘ (idC +₁ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (sym-assoc ○ (sym helper) ⟩∘⟨refl ○ assoc) ⟩ 
+        [ π₂ {A = X × N} , extend π₁ ∘ τ _ ] ∘ (idC +₁ ((f #) ∘ π₁ ⁂ idC)) ∘ i₂ ∘ ⟨ π₁ , ([ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹) ⟩ ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {!   !} ⟩ 
+        [ π₂ {A = X × N} , extend π₁ ∘ τ _ ] ∘ (idC +₁ ((f #) ∘ π₁ ⁂ idC)) ∘ i₂ ∘ ⟨ π₁ ∘ ⟨ idC , f ∘ π₁ ⟩ , ([ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹) ∘ ⟨ idC , f ∘ π₁ ⟩ ⟩ ≈⟨ {!   !} ⟩ 
+        [ π₂ {A = X × N} , extend π₁ ∘ τ _ ] ∘ (idC +₁ ((f #) ∘ π₁ ⁂ idC)) ∘ i₂ ∘ ⟨ idC , ([ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹) ∘ ⟨ idC , f ∘ π₁ ⟩ ⟩ ≈⟨ {!   !} ⟩ 
+        [ π₂ {A = X × N} , extend π₁ ∘ τ _ ] ∘ i₂ ∘ ((f #) ∘ π₁ ⁂ idC) ∘ ⟨ idC , ([ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹) ∘ ⟨ idC , f ∘ π₁ ⟩ ⟩ ≈⟨ {!   !} ⟩ 
+        [ π₂ {A = X × N} , extend π₁ ∘ τ _ ] ∘ i₂ ∘ ⟨ (f #) ∘ π₁ , ([ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹) ∘ ⟨ idC , f ∘ π₁ ⟩ ⟩ ≈⟨ pullˡ inject₂ ○ assoc ⟩ 
+        extend π₁ ∘ τ _ ∘ ⟨ (f #) ∘ π₁ , ([ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹) ∘ ⟨ idC , f ∘ π₁ ⟩ ⟩ ≈⟨ {!   !} ⟩ 
+        extend π₁ ∘ τ _ ∘ ⟨ (f #) ∘ π₁ , [ π₂ , π₁ ] ∘ ((([ i₂ # , f ]#⟩ ⁂ idC) +₁ ([ i₂ # , f ]#⟩ ⁂ idC)) ∘ distributeˡ⁻¹) ∘ ⟨ idC , f ∘ π₁ ⟩ ⟩ ≈⟨ {!   !} ⟩ 
+        extend π₁ ∘ τ _ ∘ ⟨ (f #) ∘ π₁ , [ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ ([ i₂ # , f ]#⟩ ⁂ idC) ∘ ⟨ idC , f ∘ π₁ ⟩ ⟩ ≈⟨ {!   !} ⟩ 
+        extend π₁ ∘ τ _ ∘ ⟨ (f #) ∘ π₁ , [ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ [ i₂ # , f ]#⟩ , f ∘ π₁ ⟩ ⟩ ≈⟨ {!   !} ⟩ 
+        extend π₁ ∘ τ _ ∘ ⟨ (f #) ∘ idC ∘ π₁ , [ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC ∘ [ i₂ # , f ]#⟩ , f ∘ π₁ ∘ ⟨ π₁ , π₂ ⟩ ⟩ ⟩ ≈˘⟨ {!   !} ⟩ 
+        extend π₁ ∘ τ _ ∘ ⟨ (f #) ∘ idC ∘ π₁ , ([ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (pullʳ π₁∘⁂) (p-rec-IS ((i₂ #) ∘ !) ([ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁))) ⟩ 
+        (extend π₁ ∘ τ _ ∘ ⟨ ((f #) ∘ π₁) ∘ (idC ⁂ s) , [ i₂ # , f ]#⟩ ∘ (idC ⁂ s) ⟩) ≈˘⟨ pullʳ (pullʳ ⟨⟩∘) ⟩ 
+        (extend π₁ ∘ τ _ ∘ ⟨ (f #) ∘ π₁ , [ i₂ # , f ]#⟩ ⟩) ∘ (idC ⁂ s) ≈⟨ refl ⟩ 
+        (((f #) ∘ π₁) ⇂ [ i₂ # , f ]#⟩) ∘ (idC ⁂ s) ∎
+        where
+          helper : i₂ ∘ ⟨ π₁ , [ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹ ⟩ ≈ (idC +₁ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁) ∘ distributeˡ⁻¹
+          helper = begin 
+            i₂ ∘ ⟨ π₁ , [ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹ ⟩ ≈⟨ {!   !} ⟩ 
+            i₂ ∘ ⟨ π₁ ∘ distributeˡ ∘ distributeˡ⁻¹ , [ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹ ⟩ ≈⟨ {!   !} ⟩ 
+            i₂ ∘ ⟨ π₁ ∘ distributeˡ , [ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ⟩ ∘ distributeˡ⁻¹ ≈⟨ refl⟩∘⟨ ((⟨⟩-cong₂ (∘[] ○ []-cong₂ (π₁∘⁂ ○ identityˡ) (π₁∘⁂ ○ identityˡ)) refl) ⟩∘⟨refl) ⟩ 
+            i₂ ∘ ⟨ [ π₁ , π₁ ] , [ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ⟩ ∘ distributeˡ⁻¹ ≈⟨ {!   !} ⟩ 
+            i₂ ∘ ⟨ [ π₁ , π₁ ] , [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩ ∘ distributeˡ⁻¹ ≈⟨ {!   !} ⟩ -- pullˡ (sym ([]-unique sub₁ {!   !})) ⟩ 
+            (distributeˡ⁻¹ ∘ (idC ⁂ i₂)) ∘ ⟨ [ π₁ , π₁ ] , [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩ ∘ distributeˡ⁻¹ ≈⟨ {!   !} ⟩
+            distributeˡ⁻¹ ∘ ⟨ [ π₁ , π₁ ] , i₂ ∘ [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩ ∘ distributeˡ⁻¹ ≈⟨ refl⟩∘⟨ (⟨⟩-unique subb subc ⟩∘⟨refl) ⟩
+            distributeˡ⁻¹ ∘ [ idC ⁂ i₁ , ⟨ idC , i₂ ∘ [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ∘ distributeˡ⁻¹ ≈⟨ {!   !} ⟩
+            distributeˡ⁻¹ ∘ [ idC ⁂ i₁ , ⟨ idC ∘ idC , i₂ ∘ [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ∘ distributeˡ⁻¹ ≈⟨ {!   !} ⟩
+            distributeˡ⁻¹ ∘ [ (idC ⁂ i₁) ∘ idC , (idC ⁂ i₂) ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ∘ distributeˡ⁻¹ ≈˘⟨ pullʳ (pullˡ []∘+₁) ⟩
+            (distributeˡ⁻¹ ∘ distributeˡ) ∘ (idC +₁ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁) ∘ distributeˡ⁻¹ ≈⟨ {!   !} ⟩
+            (idC +₁ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁) ∘ distributeˡ⁻¹ ∎
+            where
+              subb : π₁ ∘ [ idC ⁂ i₁ , ⟨ idC , i₂ ∘ [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ≈ [ π₁ , π₁ ]
+              subb = ∘[] ○ []-cong₂ (π₁∘⁂ ○ identityˡ) (cancelˡ project₁)
+              subc : π₂ ∘ [ idC ⁂ i₁ , ⟨ idC , i₂ ∘ [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ≈ i₂ ∘ [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ]
+              subc = begin 
+                π₂ ∘ [ idC ⁂ i₁ , ⟨ idC , i₂ ∘ [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ≈⟨ ∘[] ⟩ 
+                [ π₂ ∘ (idC ⁂ i₁) , π₂ ∘ ⟨ idC , i₂ ∘ [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ≈⟨ []-cong₂ π₂∘⁂ (pullˡ project₂) ⟩ 
+                [ i₁ {A = K.₀ Y} {B = K.₀ Y} ∘ π₂ {A = X × N} {B = K.₀ Y} , (i₂ ∘ [ i₂ # , f ]#⟩) ∘ π₁ ] ≈⟨ []-cong₂ {!   !} refl ⟩
+                [ {!  _♯ !} , (i₂ ∘ [ i₂ # , f ]#⟩) ∘ π₁ ] ≈⟨ {!   !} ⟩ 
+                [ i₂ {A = K.₀ Y} {B = K.₀ Y} ∘ π₂ {A = X × N} {B = K.₀ Y} , i₂ ∘ [ i₂ # , f ]#⟩ ∘ π₁ ] ≈⟨ sym ([]-cong₂ refl (refl⟩∘⟨ (pullˡ project₂))) ⟩ 
+                [ i₂ ∘ π₂ , i₂ ∘ π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ≈⟨ sym ∘[] ⟩ 
+                i₂ ∘ [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ∎
+              suba : ⟨ [ π₁ , π₁ ] , i₂ ∘ [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩ ∘ i₁ ≈ idC ⁂ i₁
+              suba = begin 
+                ⟨ [ π₁ , π₁ ] , i₂ ∘ [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩ ∘ i₁ ≈⟨ ⟨⟩∘ ⟩ 
+                ⟨ [ π₁ , π₁ ] ∘ i₁ , (i₂ ∘ [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ]) ∘ i₁ ⟩ ≈⟨ ⟨⟩-cong₂ inject₁ (pullʳ inject₁) ⟩ 
+                ⟨ π₁ , i₂ ∘ π₂ ⟩ ≈⟨ ⟨⟩-cong₂ {!   !} {!   !} ⟩ 
+                idC ⁂ i₁ ∎
+              sub₁ : (i₂ ∘ ⟨ [ π₁ , π₁ ] , [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩) ∘ i₁ ≈ i₁ ∘ idC
+              sub₁ = begin 
+                (i₂ ∘ ⟨ [ π₁ , π₁ ] , [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩) ∘ i₁ ≈⟨ pullʳ ⟨⟩∘ ⟩ 
+                i₂ ∘ ⟨ [ π₁ , π₁ ] ∘ i₁ , [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ∘ i₁ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ inject₁ inject₁ ⟩ 
+                i₂ ∘ ⟨ π₁ , π₂ ⟩ ≈⟨ elimʳ ⁂-η ⟩ 
+                i₂ {A = (X × N) × K.₀ Y} {B = (X × N) × K.₀ Y} ≈⟨ {!   !} ⟩ 
+                i₁ {A = (X × N) × K.₀ Y} {B = (X × N) × K.₀ Y} ∘ idC ∎
 
   kleene₂ : ∀ {X Y} (f : X ⇒ K.₀ Y + X) (g : X ⇒ K.₀ Y) → ([ i₂ # , f ]#⟩) ⊑ (g ∘ π₁) → (f #) ⊑ g
-  kleene₂ = {!   !}
+  kleene₂ {X} {Y} f g leq = ⊑-trans (⊑-trans (⊑-cong₂ refl eq₁ ⊑-refl) leq₁) (⊑-trans (⊑-cong₂ refl eq₂ ⊑-refl) leq₂)
+    where
+      h : X × N ⇒ (K.₀ N) + (X × N)
+      h = {!   !}
+      eq₁ : f # ≈ extend [ i₂ # , f ]#⟩ ∘ τ _ ∘ ⟨ idC , h # ∘ ⟨ idC , z ∘ ! ⟩ ⟩
+      eq₁ = {!   !}
+      leq₁ : (extend [ i₂ # , f ]#⟩ ∘ τ _ ∘ ⟨ idC , h # ∘ ⟨ idC , z ∘ ! ⟩ ⟩) ⊑ (extend (g ∘ π₁) ∘ τ _ ∘ ⟨ idC , h # ∘ ⟨ idC , z ∘ ! ⟩ ⟩)
+      leq₁ = ⊑∘ˡ (extend-⊑ leq)
+      leq₂ : (g ⇂ (h # ∘ ⟨ idC , z ∘ ! ⟩)) ⊑ g
+      leq₂ = begin 
+        (g ⇂ ((h #) ∘ ⟨ idC , z ∘ ! ⟩)) ≈⟨ ⇂-cong₂ ⊑-refl refl ⟩ 
+        ((g ⇂ g) ⇂ ((h #) ∘ ⟨ idC , z ∘ ! ⟩)) ≈⟨ ⇂-assoc ⟩ 
+        (g ⇂ (g ⇂ ((h #) ∘ ⟨ idC , z ∘ ! ⟩))) ∎
+      eq₂ : (extend (g ∘ π₁) ∘ τ _ ∘ ⟨ idC , h # ∘ ⟨ idC , z ∘ ! ⟩ ⟩) ≈ (g ⇂ (h # ∘ ⟨ idC , z ∘ ! ⟩))
+      eq₂ = {!   !}
+
   
 ```