leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

Work on kleene

Browse source
This commit is contained in:
Leon Vatthauer 2023-11-07 19:29:58 +01:00
parent 91ccbbf0c3
commit b6016084ac
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 234 additions and 88 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

320
src/Monad/Instance/K/PreElgot.lagda.md
View file

@ -34,9 +34,11 @@ module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK
open HomReasoning open HomReasoning
open Equiv open Equiv
open MR C open MR C
open kleisliK using (extend)
open monadK using (η; μ)
open strongK using (strengthen)
``` ```
First let's define bounded iteration via primitive recursion. 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 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 : Obj} → X ⇒ Y → Y × X × N ⇒ Y → X × N ⇒ Y
p-rec {X} {Y} f g = π₁ ∘ φ' f g 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 : 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-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 : 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-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 : 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 p-induction {X} {Y} f g w eq₁ eq₂ = begin
π₁ ∘ φ' f g ≈⟨ refl⟩∘⟨ (sym (unique zero₁ succ₁)) ⟩ π₁ ∘ φ' 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 ∘ π₁)) [_,_]#⟩ {X} {A} !! f = p-rec (!! ∘ !) ([ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁))
-- Notation -- Notation
open kleisliK using (extend)
open monadK using (η; μ)
open strongK using (strengthen)
_↓ : ∀ {X Y} (f : X ⇒ K.₀ Y) → X ⇒ K.₀ X _↓ : ∀ {X Y} (f : X ⇒ K.₀ Y) → X ⇒ K.₀ X
_↓ f = K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩ _↓ f = K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩
↓-cong : ∀ {X Y} {f g : X ⇒ K.₀ Y} → f ≈ g → f ↓ ≈ g ↓ ↓-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 ⟩ _ # ∘ ! ≈⟨ (#-resp-≈ (algebras _) (inject₂ ○ identityʳ)) ⟩∘⟨refl ⟩
i₂ # ∘ ! ∎ i₂ # ∘ ! ∎
kleene₁ : ∀ {X Y} (f : X ⇒ K.₀ Y + X) → ([ i₂ # , f ]#⟩) ⊑ (f # ∘ π₁) -- 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 -- kleene₁ {X} {Y} f = p-induction ((i₂ #) ∘ !) ([ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) (((f #) ∘ π₁) ⇂ [ i₂ # , f ]#⟩) IB IS
where -- where
IB : i₂ # ∘ ! ≈ (extend π₁ ∘ τ _ ∘ ⟨ ((f #) ∘ π₁) , [ i₂ # , f ]#⟩ ⟩) ∘ ⟨ idC , z ∘ ! ⟩ -- IB : i₂ # ∘ ! ≈ (extend π₁ ∘ τ _ ∘ ⟨ ((f #) ∘ π₁) , [ i₂ # , f ]#⟩ ⟩) ∘ ⟨ idC , z ∘ ! ⟩
IB = sym (begin -- IB = sym (begin
(extend π₁ ∘ τ _ ∘ ⟨ ((f #) ∘ π₁) , [ i₂ # , f ]#⟩ ⟩) ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ pullʳ (pullʳ ⟨⟩∘) ⟩ -- (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 #) ∘ π₁) ∘ ⟨ 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 π₁ ∘ τ _ ∘ ⟨ f # , i₂ # ∘ ! ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) ⟩
extend π₁ ∘ τ _ ∘ (idC ⁂ i₂ # ∘ !) ∘ ⟨ f # , idC ⟩ ≈⟨ refl⟩∘⟨ (pullˡ τ-strict) ⟩ -- extend π₁ ∘ τ _ ∘ (idC ⁂ i₂ # ∘ !) ∘ ⟨ f # , idC ⟩ ≈⟨ refl⟩∘⟨ (pullˡ τ-strict) ⟩
extend π₁ ∘ (i₂ # ∘ !) ∘ ⟨ f # , idC ⟩ ≈⟨ pullˡ (∘-right-strict π₁) ⟩ -- extend π₁ ∘ (i₂ # ∘ !) ∘ ⟨ f # , idC ⟩ ≈⟨ pullˡ (∘-right-strict π₁) ⟩
(i₂ # ∘ !) ∘ ⟨ f # , idC ⟩ ≈⟨ pullʳ (sym (!-unique (! ∘ ⟨ f # , idC ⟩))) ⟩ -- (i₂ # ∘ !) ∘ ⟨ f # , idC ⟩ ≈⟨ pullʳ (sym (!-unique (! ∘ ⟨ f # , idC ⟩))) ⟩
(i₂ #) ∘ ! ∎) -- (i₂ #) ∘ ! ∎)
IS : ([ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ ⟨ ((f #) ∘ π₁) ⇂ [ i₂ # , f ]#⟩ , idC ⟩ ≈ (((f #) ∘ π₁) ⇂ [ i₂ # , f ]#⟩) ∘ (idC ⁂ s) -- IS : ([ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ ⟨ ((f #) ∘ π₁) ⇂ [ i₂ # , f ]#⟩ , idC ⟩ ≈ (((f #) ∘ π₁) ⇂ [ i₂ # , f ]#⟩) ∘ (idC ⁂ s)
IS = begin -- IS = begin
([ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ ⟨ ((f #) ∘ π₁) ⇂ [ i₂ # , f ]#⟩ , idC ⟩ ≈⟨ pullʳ (pullʳ ⁂∘⟨⟩) ⟩ -- ([ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁)) ∘ ⟨ ((f #) ∘ π₁) ⇂ [ i₂ # , f ]#⟩ , idC ⟩ ≈⟨ pullʳ (pullʳ ⁂∘⟨⟩) ⟩
[ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC ∘ ((f #) ∘ π₁) ⇂ [ i₂ # , f ]#⟩ , (f ∘ π₁) ∘ idC ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ identityˡ identityʳ ⟩ -- [ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC ∘ ((f #) ∘ π₁) ⇂ [ i₂ # , f ]#⟩ , (f ∘ π₁) ∘ idC ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ identityˡ identityʳ ⟩
[ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ extend π₁ ∘ τ _ ∘ ⟨ (f #) ∘ π₁ , [ i₂ # , f ]#⟩ ⟩ , f ∘ π₁ ⟩ ≈⟨ {! !} ⟩ -- [ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ extend π₁ ∘ τ _ ∘ ⟨ (f #) ∘ π₁ , [ i₂ # , f ]#⟩ ⟩ , f ∘ π₁ ⟩ ≈⟨ {! !} ⟩
[ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ extend π₁ ∘ τ _ ∘ ((f #) ∘ π₁ ⁂ idC) ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ , f ∘ π₁ ⟩ ≈⟨ {! !} ⟩ -- [ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ extend π₁ ∘ τ _ ∘ ((f #) ∘ π₁ ⁂ idC) ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ , f ∘ π₁ ⟩ ≈⟨ {! !} ⟩
[ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ (extend π₁ ∘ τ _ ∘ ((f #) ∘ π₁ ⁂ idC) ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ⁂ idC) ∘ ⟨ idC , 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 ]#⟩ ⟩ ⁂ idC) , π₁ ∘ (extend π₁ ∘ τ _ ∘ ((f #) ∘ π₁ ⁂ idC) ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {! !} ⟩
[ π₂ , (extend π₁ ∘ τ _ ∘ ((f #) ∘ π₁ ⁂ idC) ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩) ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {! !} ⟩ -- [ π₂ , (extend π₁ ∘ τ _ ∘ ((f #) ∘ π₁ ⁂ idC) ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩) ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ π₁ ⟩ ≈⟨ {! !} ⟩
[ π₂ , extend π₁ ∘ τ _ ] ∘ (idC +₁ ((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)) ∘ (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₂ ∘ ⟨ π₁ , ([ π₂ , [ 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 , f ∘ π₁ ⟩ , ([ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹) ∘ ⟨ idC , f ∘ π₁ ⟩ ⟩ ≈⟨ {! !} ⟩
[ π₂ {A = X × N} , extend π₁ ∘ τ _ ] ∘ (idC +₁ ((f #) ∘ π₁ ⁂ idC)) ∘ i₂ ∘ ⟨ idC , ([ π₂ , [ 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 #) ∘ π₁ ⁂ idC) ∘ ⟨ idC , ([ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹) ∘ ⟨ idC , f ∘ π₁ ⟩ ⟩ ≈⟨ {! !} ⟩
[ π₂ {A = X × N} , extend π₁ ∘ τ _ ] ∘ i₂ ∘ ⟨ (f #) ∘ π₁ , ([ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹) ∘ ⟨ idC , f ∘ π₁ ⟩ ⟩ ≈⟨ pullˡ inject₂ ○ assoc ⟩ -- [ π₂ {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 ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹) ∘ ⟨ idC , f ∘ π₁ ⟩ ⟩ ≈⟨ {! !} ⟩
extend π₁ ∘ τ _ ∘ ⟨ (f #) ∘ π₁ , [ π₂ , π₁ ] ∘ ((([ i₂ # , f ]#⟩ ⁂ idC) +₁ ([ i₂ # , f ]#⟩ ⁂ idC)) ∘ 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 ]#⟩ ⁂ idC) ∘ ⟨ idC , f ∘ π₁ ⟩ ⟩ ≈⟨ {! !} ⟩
extend π₁ ∘ τ _ ∘ ⟨ (f #) ∘ π₁ , [ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ [ i₂ # , f ]#⟩ , f ∘ π₁ ⟩ ⟩ ≈⟨ {! !} ⟩ -- extend π₁ ∘ τ _ ∘ ⟨ (f #) ∘ π₁ , [ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ [ i₂ # , f ]#⟩ , f ∘ π₁ ⟩ ⟩ ≈⟨ {! !} ⟩
extend π₁ ∘ τ _ ∘ ⟨ (f #) ∘ idC ∘ π₁ , [ π₂ , π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC ∘ [ 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 ∘ π₁ , ([ π₂ , π₁ ] ∘ 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 #) ∘ π₁) ∘ (idC ⁂ s) , [ i₂ # , f ]#⟩ ∘ (idC ⁂ s) ⟩) ≈˘⟨ pullʳ (pullʳ ⟨⟩∘) ⟩
(extend π₁ ∘ τ _ ∘ ⟨ (f #) ∘ π₁ , [ i₂ # , f ]#⟩ ⟩) ∘ (idC ⁂ s) ≈⟨ refl ⟩ -- (extend π₁ ∘ τ _ ∘ ⟨ (f #) ∘ π₁ , [ i₂ # , f ]#⟩ ⟩) ∘ (idC ⁂ s) ≈⟨ refl ⟩
(((f #) ∘ π₁) ⇂ [ i₂ # , f ]#⟩) ∘ (idC ⁂ s) ∎ -- (((f #) ∘ π₁) ⇂ [ i₂ # , f ]#⟩) ∘ (idC ⁂ s) ∎
where -- where
helper : i₂ ∘ ⟨ π₁ , [ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹ ⟩ ≈ (idC +₁ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁) ∘ distributeˡ⁻¹ -- helper : i₂ ∘ ⟨ π₁ , [ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹ ⟩ ≈ (idC +₁ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁) ∘ distributeˡ⁻¹
helper = begin -- helper = begin
i₂ ∘ ⟨ π₁ , [ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹ ⟩ ≈⟨ {! !} ⟩ -- i₂ ∘ ⟨ π₁ , [ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹ ⟩ ≈⟨ {! !} ⟩
i₂ ∘ ⟨ π₁ ∘ distributeˡ ∘ distributeˡ⁻¹ , [ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹ ⟩ ≈⟨ {! !} ⟩ -- i₂ ∘ ⟨ π₁ ∘ distributeˡ ∘ distributeˡ⁻¹ , [ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ∘ distributeˡ⁻¹ ⟩ ≈⟨ {! !} ⟩
i₂ ∘ ⟨ π₁ ∘ distributeˡ , [ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ⟩ ∘ distributeˡ⁻¹ ≈⟨ refl⟩∘⟨ ((⟨⟩-cong₂ (∘[] ○ []-cong₂ (π₁∘⁂ ○ identityˡ) (π₁∘⁂ ○ identityˡ)) refl) ⟩∘⟨refl) ⟩ -- i₂ ∘ ⟨ π₁ ∘ distributeˡ , [ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ⟩ ∘ distributeˡ⁻¹ ≈⟨ refl⟩∘⟨ ((⟨⟩-cong₂ (∘[] ○ []-cong₂ (π₁∘⁂ ○ identityˡ) (π₁∘⁂ ○ identityˡ)) refl) ⟩∘⟨refl) ⟩
i₂ ∘ ⟨ [ π₁ , π₁ ] , [ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ⟩ ∘ distributeˡ⁻¹ ≈⟨ {! !} ⟩ -- i₂ ∘ ⟨ [ π₁ , π₁ ] , [ π₂ , [ i₂ # , f ]#⟩ ∘ π₁ ] ⟩ ∘ distributeˡ⁻¹ ≈⟨ {! !} ⟩
i₂ ∘ ⟨ [ π₁ , π₁ ] , [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩ ∘ distributeˡ⁻¹ ≈⟨ {! !} ⟩ -- pullˡ (sym ([]-unique sub₁ {! !})) ⟩ -- i₂ ∘ ⟨ [ π₁ , π₁ ] , [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩ ∘ distributeˡ⁻¹ ≈⟨ {! !} ⟩ -- pullˡ (sym ([]-unique sub₁ {! !})) ⟩
(distributeˡ⁻¹ ∘ (idC ⁂ i₂)) ∘ ⟨ [ π₁ , π₁ ] , [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩ ∘ distributeˡ⁻¹ ≈⟨ {! !} ⟩ -- (distributeˡ⁻¹ ∘ (idC ⁂ i₂)) ∘ ⟨ [ π₁ , π₁ ] , [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩ ∘ distributeˡ⁻¹ ≈⟨ {! !} ⟩
distributeˡ⁻¹ ∘ ⟨ [ π₁ , π₁ ] , i₂ ∘ [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩ ∘ distributeˡ⁻¹ ≈⟨ refl⟩∘⟨ (⟨⟩-unique subb subc ⟩∘⟨refl) ⟩ -- distributeˡ⁻¹ ∘ ⟨ [ π₁ , π₁ ] , i₂ ∘ [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩ ∘ distributeˡ⁻¹ ≈⟨ refl⟩∘⟨ (⟨⟩-unique subb subc ⟩∘⟨refl) ⟩
distributeˡ⁻¹ ∘ [ idC ⁂ i₁ , ⟨ idC , i₂ ∘ [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ∘ distributeˡ⁻¹ ≈⟨ {! !} ⟩ -- distributeˡ⁻¹ ∘ [ idC ⁂ i₁ , ⟨ idC , i₂ ∘ [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ∘ distributeˡ⁻¹ ≈⟨ {! !} ⟩
distributeˡ⁻¹ ∘ [ idC ⁂ i₁ , ⟨ idC ∘ 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ˡ⁻¹ ∘ [ (idC ⁂ i₁) ∘ idC , (idC ⁂ i₂) ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ∘ distributeˡ⁻¹ ≈˘⟨ pullʳ (pullˡ []∘+₁) ⟩
(distributeˡ⁻¹ ∘ distributeˡ) ∘ (idC +₁ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁) ∘ distributeˡ⁻¹ ≈⟨ {! !} ⟩ -- (distributeˡ⁻¹ ∘ distributeˡ) ∘ (idC +₁ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁) ∘ distributeˡ⁻¹ ≈⟨ {! !} ⟩
(idC +₁ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁) ∘ distributeˡ⁻¹ ∎ -- (idC +₁ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁) ∘ distributeˡ⁻¹ ∎
where -- where
subb : π₁ ∘ [ idC ⁂ i₁ , ⟨ idC , i₂ ∘ [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ≈ [ π₁ , π₁ ] -- subb : π₁ ∘ [ idC ⁂ i₁ , ⟨ idC , i₂ ∘ [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ≈ [ π₁ , π₁ ]
subb = ∘[] ○ []-cong₂ (π₁∘⁂ ○ identityˡ) (cancelˡ project₁) -- subb = ∘[] ○ []-cong₂ (π₁∘⁂ ○ identityˡ) (cancelˡ project₁)
subc : π₂ ∘ [ idC ⁂ i₁ , ⟨ idC , i₂ ∘ [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ≈ i₂ ∘ [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] -- subc : π₂ ∘ [ idC ⁂ i₁ , ⟨ idC , i₂ ∘ [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ≈ i₂ ∘ [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ]
subc = begin -- subc = begin
π₂ ∘ [ idC ⁂ i₁ , ⟨ idC , i₂ ∘ [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ≈⟨ ∘[] ⟩ -- π₂ ∘ [ idC ⁂ i₁ , ⟨ idC , i₂ ∘ [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ≈⟨ ∘[] ⟩
[ π₂ ∘ (idC ⁂ i₁) , π₂ ∘ ⟨ idC , i₂ ∘ [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ≈⟨ []-cong₂ π₂∘⁂ (pullˡ project₂) ⟩ -- [ π₂ ∘ (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₁ {A = K.₀ Y} {B = K.₀ Y} ∘ π₂ {A = X × N} {B = K.₀ Y} , (i₂ ∘ [ i₂ # , f ]#⟩) ∘ π₁ ] ≈⟨ []-cong₂ {! !} refl ⟩
[ {! _♯ !} , (i₂ ∘ [ i₂ # , f ]#⟩) ∘ π₁ ] ≈⟨ {! !} ⟩ -- [ {! _♯ !} , (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₂ {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₂ ∘ π₂ , i₂ ∘ π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ≈⟨ sym ∘[] ⟩
i₂ ∘ [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ∎ -- i₂ ∘ [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ∎
suba : ⟨ [ π₁ , π₁ ] , i₂ ∘ [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩ ∘ i₁ ≈ idC ⁂ i₁ -- suba : ⟨ [ π₁ , π₁ ] , i₂ ∘ [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩ ∘ i₁ ≈ idC ⁂ i₁
suba = begin -- suba = begin
⟨ [ π₁ , π₁ ] , i₂ ∘ [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩ ∘ i₁ ≈⟨ ⟨⟩∘ ⟩ -- ⟨ [ π₁ , π₁ ] , i₂ ∘ [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩ ∘ i₁ ≈⟨ ⟨⟩∘ ⟩
⟨ [ π₁ , π₁ ] ∘ i₁ , (i₂ ∘ [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ]) ∘ i₁ ⟩ ≈⟨ ⟨⟩-cong₂ inject₁ (pullʳ inject₁) ⟩ -- ⟨ [ π₁ , π₁ ] ∘ i₁ , (i₂ ∘ [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ]) ∘ i₁ ⟩ ≈⟨ ⟨⟩-cong₂ inject₁ (pullʳ inject₁) ⟩
⟨ π₁ , i₂ ∘ π₂ ⟩ ≈⟨ ⟨⟩-cong₂ {! !} {! !} ⟩ -- ⟨ π₁ , i₂ ∘ π₂ ⟩ ≈⟨ ⟨⟩-cong₂ {! !} {! !} ⟩
idC ⁂ i₁ ∎ -- idC ⁂ i₁ ∎
sub₁ : (i₂ ∘ ⟨ [ π₁ , π₁ ] , [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩) ∘ i₁ ≈ i₁ ∘ idC -- sub₁ : (i₂ ∘ ⟨ [ π₁ , π₁ ] , [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩) ∘ i₁ ≈ i₁ ∘ idC
sub₁ = begin -- sub₁ = begin
(i₂ ∘ ⟨ [ π₁ , π₁ ] , [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩) ∘ i₁ ≈⟨ pullʳ ⟨⟩∘ ⟩ -- (i₂ ∘ ⟨ [ π₁ , π₁ ] , [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ⟩) ∘ i₁ ≈⟨ pullʳ ⟨⟩∘ ⟩
i₂ ∘ ⟨ [ π₁ , π₁ ] ∘ i₁ , [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ∘ i₁ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ inject₁ inject₁ ⟩ -- i₂ ∘ ⟨ [ π₁ , π₁ ] ∘ i₁ , [ π₂ , π₂ ∘ ⟨ idC , [ i₂ # , f ]#⟩ ⟩ ∘ π₁ ] ∘ i₁ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ inject₁ inject₁ ⟩
i₂ ∘ ⟨ π₁ , π₂ ⟩ ≈⟨ elimʳ ⁂-η ⟩ -- i₂ ∘ ⟨ π₁ , π₂ ⟩ ≈⟨ elimʳ ⁂-η ⟩
i₂ {A = (X × N) × K.₀ Y} {B = (X × N) × K.₀ Y} ≈⟨ {! !} ⟩ -- i₂ {A = (X × N) × K.₀ Y} {B = (X × N) × K.₀ Y} ≈⟨ {! !} ⟩
i₁ {A = (X × N) × K.₀ Y} {B = (X × N) × K.₀ Y} ∘ idC ∎ -- 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 : 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₂) kleene₂ {X} {Y} f g leq = ⊑-trans (⊑-trans (⊑-cong₂ refl eq₁ ⊑-refl) leq₁) (⊑-trans (⊑-cong₂ refl eq₂ ⊑-refl) leq₂)
where where
h : X × N ⇒ (K.₀ N) + (X × N) 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₁ : 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 [ i₂ # , f ]#⟩ ∘ τ _ ∘ ⟨ idC , h # ∘ ⟨ idC , z ∘ ! ⟩ ⟩) ⊑ (extend (g ∘ π₁) ∘ τ _ ∘ ⟨ idC , h # ∘ ⟨ idC , z ∘ ! ⟩ ⟩)
leq₁ = ⊑∘ˡ (extend-⊑ leq) leq₁ = ⊑∘ˡ (extend-⊑ leq)
leq₂ : (g ⇂ (h # ∘ ⟨ idC , z ∘ ! ⟩)) ⊑ g 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 ∘ ! ⟩)) ≈⟨ ⇂-assoc ⟩
(g ⇂ (g ⇂ ((h #) ∘ ⟨ idC , z ∘ ! ⟩))) ∎ (g ⇂ (g ⇂ ((h #) ∘ ⟨ idC , z ∘ ! ⟩))) ∎
eq₂ : (extend (g ∘ π₁) ∘ τ _ ∘ ⟨ idC , h # ∘ ⟨ idC , z ∘ ! ⟩ ⟩) ≈ (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₂ = {! !}
``` ```