From 91ccbbf0c34253d9d5313170b32d4f139dfb6ba5 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Tue, 7 Nov 2023 13:53:13 +0100 Subject: [PATCH] Work on kleene --- src/Monad/Instance/K/PreElgot.lagda.md | 151 ++++++++++++++++++++++++- 1 file changed, 149 insertions(+), 2 deletions(-) diff --git a/src/Monad/Instance/K/PreElgot.lagda.md b/src/Monad/Instance/K/PreElgot.lagda.md index d87bccc..c2461cc 100644 --- a/src/Monad/Instance/K/PreElgot.lagda.md +++ b/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₂ = {! !} + ```