diff --git a/src/Monad/Instance/K/PreElgot.lagda.md b/src/Monad/Instance/K/PreElgot.lagda.md index c2461cc..f88f5f7 100644 --- a/src/Monad/Instance/K/PreElgot.lagda.md +++ b/src/Monad/Instance/K/PreElgot.lagda.md @@ -34,9 +34,11 @@ module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK open HomReasoning open Equiv open MR C + open kleisliK using (extend) + open monadK using (η; μ) + open strongK using (strengthen) ``` - 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 @@ -47,15 +49,55 @@ 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₁ 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₁ + π₁∘π₂∘φ' : ∀ {X Y : Obj} (f : X ⇒ Y) (g : Y × X × N ⇒ Y) → π₁ ∘ π₂ ∘ φ' f g ≈ π₁ + π₁∘π₂∘φ' f g = begin + π₁ ∘ π₂ ∘ φ' f g ≈⟨ unique (sym zero₁) (sym succ₁) ⟩ + universal idC idC ≈⟨ sym (unique (sym project₁) (sym π₁∘⁂)) ⟩ + π₁ ∎ + where + zero₁ : (π₁ ∘ π₂ ∘ φ' f g) ∘ ⟨ idC , z ∘ ! ⟩ ≈ idC + zero₁ = begin + (π₁ ∘ π₂ ∘ φ' f g) ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ pullʳ (pullʳ (sym commute₁)) ⟩ + π₁ ∘ π₂ ∘ ⟨ f , ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ refl⟩∘⟨ project₂ ⟩ + π₁ ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ project₁ ⟩ + idC ∎ + succ₁ : (π₁ ∘ π₂ ∘ φ' f g) ∘ (idC ⁂ s) ≈ idC ∘ π₁ ∘ π₂ ∘ φ' f g + succ₁ = begin + (π₁ ∘ π₂ ∘ φ' f g) ∘ (idC ⁂ s) ≈⟨ pullʳ (pullʳ (sym commute₂)) ⟩ + π₁ ∘ π₂ ∘ ⟨ g , ⟨ π₁ ∘ π₂ , s ∘ π₂ ∘ π₂ ⟩ ⟩ ∘ φ' f g ≈⟨ refl⟩∘⟨ pullˡ project₂ ⟩ + π₁ ∘ ⟨ π₁ ∘ π₂ , s ∘ π₂ ∘ π₂ ⟩ ∘ φ' f g ≈⟨ pullˡ project₁ ⟩ + (π₁ ∘ π₂) ∘ φ' f g ≈⟨ (sym identityˡ) ○ refl⟩∘⟨ assoc ⟩ + idC ∘ π₁ ∘ π₂ ∘ φ' f g ∎ + + π₂∘π₂∘φ' : ∀ {X Y : Obj} (f : X ⇒ Y) (g : Y × X × N ⇒ Y) → π₂ ∘ π₂ ∘ φ' f g ≈ π₂ + π₂∘π₂∘φ' f g = begin + π₂ ∘ π₂ ∘ φ' f g ≈⟨ unique (sym zero₁) (sym succ₁) ⟩ + universal (z ∘ !) s ≈⟨ sym (unique (sym project₂) (sym π₂∘⁂)) ⟩ + π₂ ∎ + where + zero₁ : (π₂ ∘ π₂ ∘ φ' f g) ∘ ⟨ idC , z ∘ ! ⟩ ≈ z ∘ ! + zero₁ = begin + (π₂ ∘ π₂ ∘ φ' f g) ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ pullʳ (pullʳ (sym commute₁)) ⟩ + π₂ ∘ π₂ ∘ ⟨ f , ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ refl⟩∘⟨ project₂ ⟩ + π₂ ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ project₂ ⟩ + z ∘ ! ∎ + succ₁ : (π₂ ∘ π₂ ∘ φ' f g) ∘ (idC ⁂ s) ≈ s ∘ π₂ ∘ π₂ ∘ φ' f g + succ₁ = begin + (π₂ ∘ π₂ ∘ φ' f g) ∘ (idC ⁂ s) ≈⟨ pullʳ (pullʳ (sym commute₂)) ⟩ + π₂ ∘ π₂ ∘ ⟨ g , ⟨ π₁ ∘ π₂ , s ∘ π₂ ∘ π₂ ⟩ ⟩ ∘ φ' f g ≈⟨ refl⟩∘⟨ pullˡ project₂ ⟩ + π₂ ∘ ⟨ π₁ ∘ π₂ , s ∘ π₂ ∘ π₂ ⟩ ∘ φ' f g ≈⟨ pullˡ project₂ ⟩ + (s ∘ π₂ ∘ π₂) ∘ φ' f g ≈⟨ assoc²' ⟩ + s ∘ π₂ ∘ π₂ ∘ φ' f g ∎ + + φ'-charac : ∀ {X Y : Obj} (f : X ⇒ Y) (g : Y × X × N ⇒ Y) → φ' f g ≈ ⟨ p-rec f g , ⟨ π₁ , π₂ ⟩ ⟩ + φ'-charac f g = sym (⟨⟩-unique refl (sym (⟨⟩-unique (π₁∘π₂∘φ' f g) (π₂∘π₂∘φ' f g)))) + 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₁)) ⟩ @@ -83,9 +125,6 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A), (f : X [_,_]#⟩ {X} {A} !! f = p-rec (!! ∘ !) ([ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) -- 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 ⟩ ↓-cong : ∀ {X Y} {f g : X ⇒ K.₀ Y} → f ≈ g → f ↓ ≈ g ↓ @@ -238,91 +277,107 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A), (f : X _ # ∘ ! ≈⟨ (#-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 IS - 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₂ #) ∘ ! ∎) - 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) → ([ i₂ # , f ]#⟩) ⊑ (f # ∘ π₁) + -- 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 + -- (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₂ #) ∘ ! ∎) + -- 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 ∎ + + -- TODO also needed further up + extend-preserves : ∀ {X Y Z : Obj} (f : X ⇒ K.₀ Y) (h : Z ⇒ K.₀ X + Z) → extend f ∘ h # ≈ ((extend f +₁ idC) ∘ h)# + extend-preserves {X} {Y} {Z} f h = begin + extend f ∘ h # ≈⟨ pullʳ (Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η.η _ ∘ f))) ⟩ + μ.η _ ∘ ((K.₁ f +₁ idC) ∘ h) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC) ⟩ + ((μ.η _ +₁ idC) ∘ (K.₁ f +₁ idC) ∘ h) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ + (((extend f +₁ idC) ∘ h)#) ∎ kleene₂ : ∀ {X Y} (f : X ⇒ K.₀ Y + X) (g : X ⇒ K.₀ Y) → ([ i₂ # , f ]#⟩) ⊑ (g ∘ π₁) → (f #) ⊑ g 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 = {! !} + h = (η.η _ ∘ π₂ +₁ idC) ∘ distributeʳ⁻¹ ∘ (f ⁂ s) + -- TODO how to follow this from the strengthened goal? eq₁ : f # ≈ extend [ i₂ # , f ]#⟩ ∘ τ _ ∘ ⟨ idC , h # ∘ ⟨ idC , z ∘ ! ⟩ ⟩ - eq₁ = {! !} + eq₁ = sym (begin + extend [ i₂ # , f ]#⟩ ∘ τ _ ∘ ⟨ idC , h # ∘ ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩-cong₂ (sym identity²) refl ○ sym ⁂∘⟨⟩) ⟩ + extend [ i₂ # , f ]#⟩ ∘ τ (X , N) ∘ (idC ⁂ (h #)) ∘ ⟨ idC , ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ refl⟩∘⟨ pullˡ (τ-comm h) ⟩ + extend [ i₂ # , f ]#⟩ ∘ ((τ (X , N) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ ⟨ idC , ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ pullˡ (extend-preserves [ i₂ # , f ]#⟩ ((τ (X , N) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))) ⟩ + ((extend [ i₂ # , f ]#⟩ +₁ idC) ∘ (τ (X , N) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ ⟨ idC , ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ (#-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²))) ⟩∘⟨refl ⟩ + ((extend [ i₂ # , f ]#⟩ ∘ τ (X , N) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ ⟨ idC , ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + (f #) ∎) leq₁ : (extend [ i₂ # , f ]#⟩ ∘ τ _ ∘ ⟨ idC , h # ∘ ⟨ idC , z ∘ ! ⟩ ⟩) ⊑ (extend (g ∘ π₁) ∘ τ _ ∘ ⟨ idC , h # ∘ ⟨ idC , z ∘ ! ⟩ ⟩) leq₁ = ⊑∘ˡ (extend-⊑ leq) leq₂ : (g ⇂ (h # ∘ ⟨ idC , z ∘ ! ⟩)) ⊑ g @@ -331,7 +386,98 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A), (f : X ((g ⇂ g) ⇂ ((h #) ∘ ⟨ idC , z ∘ ! ⟩)) ≈⟨ ⇂-assoc ⟩ (g ⇂ (g ⇂ ((h #) ∘ ⟨ idC , z ∘ ! ⟩))) ∎ eq₂ : (extend (g ∘ π₁) ∘ τ _ ∘ ⟨ idC , h # ∘ ⟨ idC , z ∘ ! ⟩ ⟩) ≈ (g ⇂ (h # ∘ ⟨ idC , z ∘ ! ⟩)) - eq₂ = {! !} + eq₂ = sym (begin + extend π₁ ∘ τ (K.₀ Y , N) ∘ ⟨ g , (h #) ∘ ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ((⟨⟩-cong₂ (sym identityʳ) (sym identityˡ)) ○ sym ⁂∘⟨⟩) ⟩ + extend π₁ ∘ τ (K.₀ Y , N) ∘ (g ⁂ idC) ∘ ⟨ idC , (h #) ∘ ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ refl⟩∘⟨ pullˡ (τ-comm-id g) ⟩ + extend π₁ ∘ (K.₁ (g ⁂ idC) ∘ τ (X , N)) ∘ ⟨ idC , (h #) ∘ ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ pullˡ (pullˡ (extend∘F₁ monadK π₁ (g ⁂ idC))) ⟩ + (extend (π₁ ∘ (g ⁂ idC)) ∘ τ _) ∘ ⟨ idC , (h #) ∘ ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ assoc ○ (kleisliK.extend-≈ π₁∘⁂) ⟩∘⟨refl ⟩ + extend (g ∘ π₁) ∘ τ (X , N) ∘ ⟨ idC , (h #) ∘ ⟨ idC , z ∘ ! ⟩ ⟩ ∎) + -- to show eq₁ we strengthen the goal: + w-fact : w ∘ (idC ⁂ s) ≈ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ∘ w + w-fact = begin + w ∘ (idC ⁂ s) ≈⟨ p-rec-IS _ _ ⟩ + ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ ≈⟨ pullʳ (pullʳ ⟨⟩∘) ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ π₁) ∘ φ' _ _ , ((f ∘ π₁) ∘ π₂) ∘ φ' _ _ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (assoc ○ identityˡ) (assoc ○ pullʳ (π₁∘π₂∘φ' _ _)) ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ w , f ∘ π₁ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym (p-induction ⟨ idC , f ⟩ {! !} ⟨ w , f ∘ π₁ ⟩ (sym (⟨⟩∘ ○ ⟨⟩-cong₂ (p-rec-IB idC _) (cancelʳ project₁))) (sym {! !})) ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ p-rec ⟨ idC , f ⟩ {! !} ≈⟨ refl⟩∘⟨ refl⟩∘⟨ p-induction ⟨ idC , f ⟩ {! !} ⟨ w , f ∘ w ⟩ (sym (⟨⟩∘ ○ ⟨⟩-cong₂ (p-rec-IB idC _) (cancelʳ (p-rec-IB idC _)))) (sym {! !}) ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ w , f ∘ w ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ refl) ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ∘ w ∎ + where + -- TODO this just wont work... maybe w-fact' is wrong, maybe im just missing the link in between + -- maybe step: ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ⁂ f ∘ π₁) + ind-base : w ∘ (idC ⁂ s) ∘ ⟨ idC , z ∘ ! ⟩ ≈ ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ∘ w) ∘ ⟨ idC , z ∘ ! ⟩ + ind-base = begin + w ∘ (idC ⁂ s) ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ pullˡ (p-rec-IS _ _) ⟩ + (([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _) ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ pullʳ (sym commute₁) ⟩ + ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ ⟨ idC , ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ pullʳ (pullʳ ⁂∘⟨⟩) ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC ∘ idC , (f ∘ π₁) ∘ ⟨ idC , z ∘ ! ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ identity² (cancelʳ project₁) ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ∘ idC ≈˘⟨ pullʳ (pullʳ (pullʳ (p-rec-IB _ _))) ⟩ + ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ∘ w) ∘ ⟨ idC , z ∘ ! ⟩ ∎ + ind-step : w ∘ (idC ⁂ s) ∘ (idC ⁂ s) ≈ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ∘ w ∘ (idC ⁂ s) + ind-step = begin + w ∘ (idC ⁂ s) ∘ (idC ⁂ s) ≈⟨ pullˡ (p-rec-IS _ _) ⟩ + (([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _) ∘ (idC ⁂ s) ≈⟨ pullʳ (sym commute₂) ⟩ + ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ ⟨ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁) , ⟨ π₁ ∘ π₂ , s ∘ π₂ ∘ π₂ ⟩ ⟩ ∘ φ' _ _ ≈⟨ pullʳ (pullʳ (pullˡ ⁂∘⟨⟩)) ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁) , (f ∘ π₁) ∘ ⟨ π₁ ∘ π₂ , s ∘ π₂ ∘ π₂ ⟩ ⟩ ∘ φ' _ _ ≈⟨ {! !} ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , ((f ∘ π₁) ∘ ⟨ π₁ ∘ π₂ , s ∘ π₂ ∘ π₂ ⟩) ∘ φ' _ _ ⟩ ≈⟨ {! !} ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , (f ∘ π₁ ∘ π₂) ∘ φ' _ _ ⟩ ≈⟨ {! !} ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , f ∘ π₁ ⟩ ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , f ∘ [ π₁ ∘ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ φ' _ _ , f ∘ π₁ ⟩ ⟩ ≈⟨ {! !} ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , f ∘ [ π₁ , π₂ ] ∘ ((π₁ ⁂ idC) +₁ (π₁ ⁂ idC)) ∘ distributeˡ⁻¹ ∘ ⟨ φ' _ _ , f ∘ π₁ ⟩ ⟩ ≈⟨ {! !} ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , f ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (π₁ ⁂ idC) ∘ ⟨ φ' _ _ , f ∘ π₁ ⟩ ⟩ ≈⟨ {! !} ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , f ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ w , f ∘ π₁ ⟩ ⟩ ≈˘⟨ {! !} ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , f ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ π₁) ∘ φ' _ _ , ((f ∘ π₁) ∘ π₂) ∘ φ' _ _ ⟩ ⟩ ≈˘⟨ {! !} ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , (f ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ ⟩ ≈˘⟨ {! !} ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁) , f ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁) ⟩ ∘ φ' _ _ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ ⟨⟩∘ ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ∘ ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ p-rec-IS _ _ ⟩ + [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ∘ w ∘ (idC ⁂ s) ∎ + help : π₁ ≈ [ π₁ ∘ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ φ' _ _ , f ∘ π₁ ⟩ + help = begin + π₁ ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + [ w ∘ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {! !} ⟩ + π₁ ∘ [ φ' _ _ ∘ π₁ , ⟨ π₂ , {! !} ∘ (φ' _ _ ⁂ idC) ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {! !} ⟩ + π₁ ∘ [ φ' _ _ ∘ π₁ , ⟨ π₂ ∘ (φ' _ _ ⁂ idC) , {! !} ∘ (φ' _ _ ⁂ idC) ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {! !} ⟩ + π₁ ∘ [ π₁ ∘ (φ' _ _ ⁂ idC) , ⟨ π₂ , {! !} ⟩ ∘ (φ' _ _ ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {! !} ⟩ + π₁ ∘ [ π₁ , ⟨ π₂ , {! !} ⟩ ] ∘ ((φ' _ _ ⁂ idC) +₁ (φ' _ _ ⁂ idC)) ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {! !} ⟩ + π₁ ∘ [ π₁ , ⟨ π₂ , {! !} ⟩ ] ∘ distributeˡ⁻¹ ∘ (φ' _ _ ⁂ idC) ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {! !} ⟩ + π₁ ∘ [ π₁ , ⟨ π₂ , {! !} ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ φ' _ _ , f ∘ π₁ ⟩ ≈⟨ {! !} ⟩ + [ π₁ ∘ π₁ , π₁ ∘ ⟨ π₂ , {! !} ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ φ' _ _ , f ∘ π₁ ⟩ ≈⟨ {! !} ⟩ + [ π₁ ∘ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ φ' _ _ , f ∘ π₁ ⟩ ∎ + helper : (idC ⁂ f ∘ π₁) ∘ φ' _ _ ≈ ⟨ w , f ∘ π₁ ⟩ + helper = begin {! !} ≈⟨ {! !} ⟩ {! !} ∎ + IS₁ : ⟨ w , f ∘ π₁ ⟩ ∘ (idC ⁂ s) ≈ ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ⁂ f ∘ π₁) ∘ ⟨ ⟨ w , f ∘ π₁ ⟩ , idC ⟩ + IS₁ = begin + ⟨ w , f ∘ π₁ ⟩ ∘ (idC ⁂ s) ≈⟨ ⟨⟩∘ ⟩ + ⟨ w ∘ (idC ⁂ s) , (f ∘ π₁) ∘ (idC ⁂ s) ⟩ ≈⟨ ⟨⟩-cong₂ (p-rec-IS idC _) (pullʳ π₁∘⁂) ⟩ + ⟨ ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , f ∘ idC ∘ π₁ ⟩ ≈⟨ ⟨⟩-cong₂ (pullʳ (pullʳ ⟨⟩∘)) (refl⟩∘⟨ identityˡ) ⟩ + ⟨ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ (idC ∘ π₁) ∘ φ' _ _ , ((f ∘ π₁) ∘ π₂) ∘ φ' _ _ ⟩ , f ∘ π₁ ⟩ ≈⟨ ⟨⟩-cong₂ (refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (assoc ○ identityˡ) (assoc ○ pullʳ (π₁∘π₂∘φ' _ _))) refl ⟩ + ⟨ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ w , f ∘ π₁ ⟩ , f ∘ π₁ ⟩ ≈˘⟨ ⁂∘⟨⟩ ○ ⟨⟩-cong₂ assoc identityʳ ⟩ + ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ⁂ f ∘ π₁) ∘ ⟨ ⟨ w , f ∘ π₁ ⟩ , idC ⟩ ∎ + IS₂ : ⟨ w , f ∘ w ⟩ ∘ (idC ⁂ s) ≈ ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ⁂ f ∘ π₁) ∘ ⟨ ⟨ w , f ∘ w ⟩ , idC ⟩ + IS₂ = begin + ⟨ w , f ∘ w ⟩ ∘ (idC ⁂ s) ≈⟨ ⟨⟩∘ ⟩ + ⟨ w ∘ (idC ⁂ s) , (f ∘ w) ∘ (idC ⁂ s) ⟩ ≈⟨ ⟨⟩-cong₂ (p-rec-IS _ _) (pullʳ (p-rec-IS _ _)) ⟩ + ⟨ ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ , f ∘ ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ φ' _ _ ⟩ ≈⟨ ⟨⟩-cong₂ (pullʳ (pullʳ helper)) (refl⟩∘⟨ pullʳ (pullʳ helper)) ⟩ + ⟨ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ w , f ∘ π₁ ⟩ , f ∘ [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ w , f ∘ π₁ ⟩ ⟩ ≈⟨ {! !} ⟩ + ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ⁂ f) ∘ ⟨ ⟨ w , f ∘ π₁ ⟩ , [ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ w , f ∘ π₁ ⟩ ⟩ ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ⁂ f) ∘ ⟨ ⟨ w , f ∘ w ⟩ , π₁ ⟩ ≈⟨ {! !} ⟩ + ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ⁂ f ∘ π₁) ∘ ⟨ ⟨ w , f ∘ w ⟩ , idC ⟩ ∎ + + -- TODO this depends on (8) and (9) + stronger : ((extend [ i₂ # , f ]#⟩ ∘ τ (X , N) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ ⟨ π₁ , ⟨ w , π₂ ⟩ ⟩ ≈ f # ∘ w + stronger = begin + ((extend [ i₂ # , f ]#⟩ ∘ τ (X , N) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ ⟨ π₁ , ⟨ w , π₂ ⟩ ⟩ ≈⟨ sym (#-Uniformity (algebras _) by-uni₁) ⟩ + ((π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ idC ⁂ s , f ∘ w ⟩ )# ≈⟨ #-Uniformity (algebras _) by-uni₂ ⟩ + f # ∘ w ∎ + where + by-uni₁ : (idC +₁ ⟨ π₁ , ⟨ w , π₂ ⟩ ⟩) ∘ (π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ idC ⁂ s , f ∘ w ⟩ ≈ ((extend [ i₂ # , f ]#⟩ ∘ τ (X , N) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ ⟨ π₁ , ⟨ w , π₂ ⟩ ⟩ + by-uni₁ = {! !} + by-uni₂ : (idC +₁ w) ∘ (π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ idC ⁂ s , f ∘ w ⟩ ≈ f ∘ w + by-uni₂ = {! !} - ```