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

🚧 Case-statements and small progress on restriction category

Browse source
This commit is contained in:
Leon Vatthauer 2023-11-11 14:56:03 +01:00
parent a3973a0b38
commit 21c98bab4f
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 140 additions and 80 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

43
src/Monad/Instance/K/EquationalLifting.lagda.md
View file

@ -32,6 +32,7 @@ open kleisliK using (extend)
open monadK using (μ)
open FreeObject using (*-uniq)
open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈)
open strongK using (strengthen)
-- some helper definitions to make our life easier
private
@ -93,21 +94,28 @@ From this we can follow that the kleisli category of **K** is a *restriction cat
```agda
kleisli-restriction' : Restriction (Kleisli monadK)
kleisli-restriction' = record
{ _↓ = λ f → K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩
{ _↓ = _↓
; pidʳ = λ {A} {B} {f} → begin
(μ.η _ ∘ K.₁ f) ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ idC {A} , f ⟩ ≈⟨ {! !} ⟩
(μ.η _ ∘ K.₁ f) ∘ K.₁ π₁ ∘ τ _ ∘ (idC ⁂ f) ∘ ⟨ idC , idC ⟩ ≈⟨ {! !} ⟩
(μ.η B ∘ K.₁ f) ∘ K.₁ π₁ ∘ τ _ ∘ (idC ⁂ f) ∘ ⟨ idC , idC ⟩ ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
(μ.η B ∘ K.₁ f) ∘ η A ≈⟨ {! !} ⟩
(μ.η _ ∘ K.₁ f) ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ idC {A} , f ⟩ ≈⟨ pullʳ (sym-assoc ○ pullˡ ((sym K.homomorphism) ⟩∘⟨refl)) ⟩
μ.η _ ∘ (K.₁ (f ∘ π₁) ∘ τ _) ∘ ⟨ idC , f ⟩ ≈˘⟨ refl⟩∘⟨ ((K.F-resp-≈ π₁∘⁂) ⟩∘⟨refl) ⟩∘⟨refl ⟩
μ.η _ ∘ (K.₁ (π₁ ∘ (f ⁂ idC)) ∘ τ _) ∘ ⟨ idC , f ⟩ ≈˘⟨ refl⟩∘⟨ (pullˡ (pullˡ (sym K.homomorphism))) ⟩
μ.η _ ∘ K.₁ π₁ ∘ (K.₁ (f ⁂ idC) ∘ τ _) ∘ ⟨ idC , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (sym (strengthen.commute _) ○ refl⟩∘⟨ ⁂-cong₂ refl K.identity)) ⟩
μ.η _ ∘ K.₁ π₁ ∘ τ _ ∘ (f ⁂ idC) ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩
μ.η _ ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ f , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ Δ∘ ⟩
μ.η _ ∘ K.₁ π₁ ∘ (τ _ ∘ Δ) ∘ f ≈⟨ refl⟩∘⟨ refl⟩∘⟨ equationalLifting ⟩∘⟨refl ⟩
μ.η _ ∘ K.₁ π₁ ∘ (K.₁ ⟨ η _ , idC ⟩) ∘ f ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym K.homomorphism ○ K.F-resp-≈ ⁂∘Δ) ⟩
μ.η _ ∘ K.₁ π₁ ∘ K.₁ (η _ ⁂ idC) ∘ K.₁ Δ ∘ f ≈⟨ refl⟩∘⟨ (pullˡ (sym K.homomorphism)) ⟩
μ.η _ ∘ K.₁ (π₁ ∘ (η _ ⁂ idC)) ∘ K.₁ Δ ∘ f ≈⟨ refl⟩∘⟨ ((K.F-resp-≈ π₁∘⁂) ⟩∘⟨refl) ⟩
μ.η _ ∘ K.₁ (η _ ∘ π₁) ∘ K.₁ Δ ∘ f ≈˘⟨ refl⟩∘⟨ (pullˡ (sym K.homomorphism)) ⟩
μ.η _ ∘ K.₁ (η _) ∘ K.₁ π₁ ∘ K.₁ Δ ∘ f ≈⟨ cancelˡ monadK.identityˡ ⟩
K.₁ π₁ ∘ K.₁ Δ ∘ f ≈⟨ cancelˡ (sym K.homomorphism ○ K.F-resp-≈ project₁ ○ K.identity) ⟩
f ∎
; ↓-comm = λ {A} {B} {D} {f} {g} → begin
(μ.η _ ∘ K.₁ (K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩)) ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ idC , g ⟩ ≈⟨ pullˡ (pullʳ (sym K.homomorphism)) ⟩
(μ.η _ ∘ K.₁ ((K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩) ∘ π₁)) ∘ τ _ ∘ ⟨ idC , g ⟩ ≈⟨ {! !} ⟩
(K.₁ π₁ ∘ (μ.η _ ∘ K.₁ ((τ _ ∘ ⟨ idC , f ⟩) ∘ π₁))) ∘ τ _ ∘ ⟨ idC , g ⟩ ≈⟨ {! !} ⟩
(K.₁ π₁ ∘ (μ.η _ ∘ K.₁ (τ _) ∘ K.₁ ⟨ π₁ , f ∘ π₁ ⟩)) ∘ τ _ ∘ ⟨ idC , g ⟩ ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
(μ.η _ ∘ K.₁ (K.₁ π₁ ∘ τ _ ∘ ⟨ idC , g ⟩)) ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩ ∎
@ -115,4 +123,23 @@ kleisli-restriction' = record
; ↓-skew-comm = {! !}
; ↓-cong = λ eq → refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl eq
}
where
_↓ : ∀ {A B : Obj} → A ⇒ K.₀ B → A ⇒ K.₀ A
f ↓ = K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩
↓-comm' : ∀ {A B C : Obj} {f : A ⇒ K.₀ B} {g : A ⇒ K.₀ C} → extend (f ↓) ∘ g ↓ ≈ extend (g ↓) ∘ f ↓
↓-comm' {A} {B} {C} {f} {g} = begin
(μ.η _ ∘ K.₁ (K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩)) ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ idC , g ⟩ ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
(μ.η _ ∘ K.₁ (K.₁ π₁ ∘ τ _ ∘ ⟨ idC , g ⟩)) ∘ K.₁ π₁ ∘ τ _ ∘ ⟨ idC , f ⟩ ∎
where
f-helper : μ.η _ ∘ K.₁ (K.₁ π₁) ∘ K.₁ (τ _) ∘ K.₁ ⟨ idC , f ⟩ ≈ μ.η _ ∘ K.₁ π₁ ∘ τ _ ∘ Δ
f-helper = sym (begin
μ.η _ ∘ K.₁ π₁ ∘ τ _ ∘ Δ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ equationalLifting ⟩
μ.η A ∘ K.₁ π₁ ∘ K.₁ ⟨ η A , idC ⟩ ≈⟨ refl⟩∘⟨ sym K.homomorphism ⟩
μ.η A ∘ K.₁ (π₁ ∘ ⟨ η A , idC ⟩) ≈⟨ {! !} ⟩
μ.η A ∘ K.₁ (η A) ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
μ.η _ ∘ K.₁ (K.₁ π₁) ∘ K.₁ (τ _) ∘ K.₁ ⟨ idC , f ⟩ ∎)
```

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

@ -33,7 +33,9 @@ module Monad.Instance.K.PreElgot {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK
open HomReasoning
open Equiv
open M C
open MR C
open import Categories.Morphism.Properties C
open kleisliK using (extend)
open monadK using (η; μ)
open strongK using (strengthen)
@ -202,6 +204,20 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A), (f : X
(g ⇂ f) ∘ h ≈⟨ ⇂∘ ⟩
((g ∘ h) ⇂ (f ∘ h)) ∎
⊑-monoʳ : ∀ {A X Y} {f g : X ⇒ K.₀ Y} {h : A ⇒ K.₀ X} → f ⊑ g → (extend f ∘ h) ⊑ (extend g ∘ h)
⊑-monoʳ {A} {X} {Y} {f} {g} {h} leq = sym (begin
((extend g ∘ h) ⇂ (extend f ∘ h)) ≈⟨ restrict-law (extend g ∘ h) (extend f ∘ h) ⟩
extend (extend g ∘ h) ∘ (extend f ∘ h)↓ ≈˘⟨ pullˡ kleisliK.sym-assoc ⟩
extend g ∘ extend h ∘ (extend f ∘ h) ↓ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ↓-cong (sym (pullˡ (kleisliK.sym-assoc ○ kleisliK.extend-≈ leq'))) ⟩
extend g ∘ extend h ∘ (extend g ∘ extend (f ↓) ∘ h) ↓ ≈⟨ refl⟩∘⟨ {! !} ⟩ -- RST₄ + kleisliK.sym-assoc inside
extend g ∘ extend ((extend g ∘ (f ↓)) ↓) ∘ h ≈⟨ {! !} ⟩ -- RST₃
extend g ∘ extend (g ↓) ∘ extend (f ↓) ∘ h ≈⟨ {! !} ⟩ -- RST₁
extend g ∘ extend (f ↓) ∘ h ≈⟨ pullˡ (kleisliK.sym-assoc ○ kleisliK.extend-≈ leq') ⟩
extend f ∘ h ∎)
where
leq' : extend g ∘ f ↓ ≈ f
leq' = sym (restrict-law g f) ○ sym leq
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 ⟩
@ -392,81 +408,88 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A), (f : X
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 ∎
case'_inl_inr_ : ∀ {X Y Z U} → X ⇒ Y + Z → Y ⇒ U → Z ⇒ U → X ⇒ U
case' f inl g inr h = [ g , h ] ∘ f
case_inl_inr_ : ∀ {X Y Z U} → X ⇒ Y + Z → X × Y ⇒ U → X × Z ⇒ U → X ⇒ U
case f inl g inr h = [ g , h ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩
casecase' : ∀ {X Y Z U} (f : X ⇒ Y + Z) (g : Y ⇒ U) (h : Z ⇒ U) → case f inl (g ∘ π₂) inr (h ∘ π₂) ≈ case' f inl g inr h
casecase' f g h = begin
[ g ∘ π₂ , h ∘ π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈⟨ sym (pullˡ []∘+₁) ⟩
[ g , h ] ∘ (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ pullˡ distribute₂ ⟩
[ g , h ] ∘ π₂ ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ project₂ ⟩
[ g , h ] ∘ f ∎
case-id : ∀ {X Y Z} (f : X ⇒ Y + Z) → case f inl (i₁ ∘ π₂) inr (i₂ ∘ π₂) ≈ f
case-id f = begin
(case f inl i₁ ∘ π₂ inr (i₂ ∘ π₂)) ≈⟨ casecase' f i₁ i₂ ⟩
(case' f inl i₁ inr i₂) ≈⟨ elimˡ +-η ⟩
f ∎
case_inl$l->_$l&inr$r->_$r : ∀ {X Y Z U} → X ⇒ Y + Z → X × Y ⇒ U → X × Z ⇒ U → X ⇒ U
case f inl$l-> g $l&inr$r-> h $r = [ g , h ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩
case∘ˡ : ∀ {X Y Z U V} (f : X ⇒ Y + Z) (g : X × Y ⇒ U) (h : X × Z ⇒ U) (l : U ⇒ V) → l ∘ (case f inl g inr h) ≈ case f inl (l ∘ g) inr (l ∘ h)
case∘ˡ f g h l = pullˡ ∘[]
case∘ʳ : ∀ {X Y Z U V} (f : X ⇒ Y + Z) (g : X × Y ⇒ U) (h : X × Z ⇒ U) (r : V ⇒ X) → (case f inl g inr h) ∘ r ≈ case f ∘ r inl (g ∘ (r ⁂ idC)) inr (h ∘ (r ⁂ idC))
case∘ʳ f g h r = begin
(case f inl g inr h) ∘ r ≈⟨ pullʳ (pullʳ ⟨⟩∘) ⟩
[ g , h ] ∘ distributeˡ⁻¹ ∘ ⟨ idC ∘ r , f ∘ r ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ id-comm identityˡ) ⟩
[ g , h ] ∘ distributeˡ⁻¹ ∘ (r ⁂ idC) ∘ ⟨ idC , f ∘ r ⟩ ≈⟨ refl⟩∘⟨ (pullˡ (refl⟩∘⟨ (⁂-cong₂ refl (sym ([]-unique id-comm-sym id-comm-sym))) ○ sym (distribute₁ r idC idC))) ⟩
[ g , h ] ∘ (((r ⁂ idC) +₁ (r ⁂ idC)) ∘ distributeˡ⁻¹) ∘ ⟨ idC , f ∘ r ⟩ ≈⟨ pullˡ (pullˡ []∘+₁) ○ assoc ⟩
(case f ∘ r inl (g ∘ (r ⁂ idC)) inr (h ∘ (r ⁂ idC))) ∎
case⟩_⟨inl⟩_⟨inr⟩_ : ∀ {X Y Z U} {f f' : X ⇒ Y + Z} {g g' : X × Y ⇒ U} {h h' : X × Z ⇒ U} → f ≈ f' → g ≈ g' → h ≈ h' → case f inl g inr h ≈ case f' inl g' inr h'
case⟩ f≈f' ⟨inl⟩ g≈g' ⟨inr⟩ h≈h' = []-cong₂ g≈g' h≈h' ⟩∘⟨ refl ⟩∘⟨ ⟨⟩-cong₂ refl f≈f'
case-nested : ∀ {X Y Z U} (f : X ⇒ Y + Z) (g : X × Y ⇒ U) (g' : X × Y ⇒ U) (h : X × Z ⇒ U) → case f inl g inr ((case f inl g' inr h) ∘ π₁) ≈ case f inl g inr h
case-nested f g g' h = begin
[ g , (case f inl g' inr h) ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈⟨ refl ⟩
[ g , ([ g' , h ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩) ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈˘⟨ ([]-cong₂ (elimʳ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ (cancelˡ project₁) (cancelˡ identity²) ○ ⁂-η)) (sym (pullʳ (pullʳ (sym π₁∘⁂))))) ⟩∘⟨refl ⟩
[ g ∘ (π₁ ⁂ idC) ∘ (⟨ idC , f ⟩ ⁂ idC) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ∘ (⟨ idC , f ⟩ ⁂ idC) ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ assoc assoc²') ⟩
[ g ∘ (π₁ ⁂ idC) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ] ∘ ((⟨ idC , f ⟩ ⁂ idC) +₁ (⟨ idC , f ⟩ ⁂ idC)) ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ pullˡ (distribute₁ ⟨ idC , f ⟩ idC idC ○ refl⟩∘⟨ ⁂-cong₂ refl ([]-unique id-comm-sym id-comm-sym)) ⟩
[ g ∘ (π₁ ⁂ idC) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ] ∘ (distributeˡ⁻¹ ∘ (⟨ idC , f ⟩ ⁂ idC)) ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ (pullʳ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ)) ⟩
[ g ∘ (π₁ ⁂ idC) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ ⟨ idC , f ⟩ , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl project₂ ⟩
[ g ∘ (π₁ ⁂ idC) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ ⟨ idC , f ⟩ , π₂ ∘ ⟨ idC , f ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩∘ ○ refl⟩∘⟨ (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ refl)) ⟩
[ g ∘ (π₁ ⁂ idC) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , π₂ ⟩ ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ pullˡ helper ⟩
[ g ∘ (π₁ ⁂ idC) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ] ∘ ((⟨ (idC ⁂ i₁) , π₂ ⟩ +₁ ⟨ (idC ⁂ i₂) , π₂ ⟩) ∘ distributeˡ⁻¹) ∘ ⟨ idC , f ⟩ ≈⟨ refl⟩∘⟨ assoc ○ pullˡ ([]∘+₁ ○ []-cong₂ assoc assoc²') ⟩
[ g ∘ (π₁ ⁂ idC) ∘ ⟨ (idC ⁂ i₁) , π₂ ⟩ , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ∘ ⟨ (idC ⁂ i₂) , π₂ ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈⟨ ([]-cong₂ (refl⟩∘⟨ ⁂∘⟨⟩) (refl⟩∘⟨ refl⟩∘⟨ project₁)) ⟩∘⟨refl ⟩
[ g ∘ ⟨ π₁ ∘ (idC ⁂ i₁) , idC ∘ π₂ ⟩ , [ g' , h ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂) ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈⟨ ([]-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ π₁∘⁂ refl)) (refl⟩∘⟨ dstr-law₂)) ⟩∘⟨refl ⟩
[ g ∘ ⟨ idC ∘ π₁ , idC ∘ π₂ ⟩ , [ g' , h ] ∘ i₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ≈⟨ []-cong₂ (elimʳ (⟨⟩-cong₂ identityˡ identityˡ ○ ⁂-η)) inject₂ ⟩∘⟨refl ⟩
[ g , h ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩ ∎
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 _ _) ⟩
helper : distributeˡ⁻¹ ∘ ⟨ idC , π₂ ⟩ ≈ (⟨ (idC ⁂ i₁) , π₂ ⟩ +₁ ⟨ (idC ⁂ i₂) , π₂ ⟩) ∘ distributeˡ⁻¹
helper = Iso⇒Epi (IsIso.iso isIsoˡ) (distributeˡ⁻¹ ∘ ⟨ idC , π₂ ⟩) ((⟨ idC ⁂ i₁ , π₂ ⟩ +₁ ⟨ idC ⁂ i₂ , π₂ ⟩) ∘ distributeˡ⁻¹) (begin
(distributeˡ⁻¹ ∘ ⟨ idC , π₂ ⟩) ∘ distributeˡ ≈⟨ ∘[] ⟩
[ ((distributeˡ⁻¹ ∘ ⟨ idC , π₂ ⟩) ∘ (idC ⁂ i₁)) , ((distributeˡ⁻¹ ∘ ⟨ idC , π₂ ⟩) ∘ (idC ⁂ i₂)) ] ≈⟨ []-cong₂ (pullʳ ⟨⟩∘) (pullʳ ⟨⟩∘) ⟩
[ (distributeˡ⁻¹ ∘ ⟨ idC ∘ (idC ⁂ i₁) , π₂ ∘ (idC ⁂ i₁) ⟩) , (distributeˡ⁻¹ ∘ ⟨ idC ∘ (idC ⁂ i₂) , π₂ ∘ (idC ⁂ i₂) ⟩) ] ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ π₂∘⁂)) (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ π₂∘⁂)) ⟩
[ distributeˡ⁻¹ ∘ ⟨ (idC ⁂ i₁) , i₁ ∘ π₂ ⟩ , distributeˡ⁻¹ ∘ ⟨ (idC ⁂ i₂) , i₂ ∘ π₂ ⟩ ] ≈˘⟨ []-cong₂ (refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl)) (refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl)) ⟩
[ distributeˡ⁻¹ ∘ (idC ⁂ i₁) ∘ ⟨ (idC ⁂ i₁) , π₂ ⟩ , distributeˡ⁻¹ ∘ (idC ⁂ i₂) ∘ ⟨ (idC ⁂ i₂) , π₂ ⟩ ] ≈⟨ []-cong₂ (pullˡ dstr-law₁) (pullˡ dstr-law₂) ⟩
[ i₁ ∘ ⟨ (idC ⁂ i₁) , π₂ ⟩ , i₂ ∘ ⟨ (idC ⁂ i₂) , π₂ ⟩ ] ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoˡ) ⟩
((⟨ (idC ⁂ i₁) , π₂ ⟩ +₁ ⟨ (idC ⁂ i₂) , π₂ ⟩) ∘ distributeˡ⁻¹) ∘ distributeˡ ∎)
-- to show eq₁ we strengthen the goal:
w' : X × N ⇒ X
w' = p-rec idC {! case ? inl ? inr ? !} -- ([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ f ∘ π₁))
w : X × N ⇒ X
w = universal idC (case f inl π₁ inr π₂) --([ π₁ , π₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ⟩)
ww' : w' ∘ (idC ⁂ s) ≈ w
ww' = unique (sym IB) {! !}
where
IB : (w' ∘ (idC ⁂ s)) ∘ ⟨ idC , z ∘ ! ⟩ ≈ idC
IB = begin
(w' ∘ (idC ⁂ s)) ∘ ⟨ idC , z ∘ ! ⟩ ≈⟨ (p-rec-IS idC _) ⟩∘⟨refl ⟩
(([ π₁ , π₂ ] ∘ 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 , f ⟩ ≈⟨ {! !} ⟩
(case f inl π₁ inr π₂) ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
[ π₁ , π₂ ] ∘ 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 ⟩ ∎
idC ∎
-- TODO this depends on (8) and (9)
stronger : ((extend [ i₂ # , f ]#⟩ ∘ τ (X , N) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ ⟨ π₁ , ⟨ w , π₂ ⟩ ⟩ ≈ f # ∘ w
@ -478,6 +501,16 @@ Given a pointed object A (i.e. there exists a morphism !! : ⊤ ⇒ A), (f : X
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₂ = {! !}
by-uni₂ = begin
(idC +₁ w) ∘ (π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ idC ⁂ s , f ∘ w ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩
(idC +₁ w) ∘ (π₂ +₁ π₁) ∘ distributeˡ⁻¹ ∘ ((idC ⁂ s) ⁂ idC) ∘ ⟨ idC , f ∘ w ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ (sym (distribute₁ (idC ⁂ s) idC idC ○ refl⟩∘⟨ ⁂-cong₂ refl ([]-unique id-comm-sym id-comm-sym))) ○ assoc) ⟩
(idC +₁ w) ∘ (π₂ +₁ π₁) ∘ ((idC ⁂ s) ⁂ idC +₁ (idC ⁂ s) ⁂ idC) ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ w ⟩ ≈⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (π₂∘⁂ ○ identityˡ) π₁∘⁂)) ⟩
(idC +₁ w) ∘ (π₂ +₁ (idC ⁂ s) ∘ π₁) ∘ distributeˡ⁻¹ ∘ ⟨ idC , f ∘ w ⟩ ≈⟨ refl ⟩
(idC +₁ w) ∘ (case f ∘ w inl (i₁ ∘ π₂) inr (i₂ ∘ (idC ⁂ s) ∘ π₁)) ≈⟨ case∘ˡ (f ∘ w) (i₁ ∘ π₂) (i₂ ∘ (idC ⁂ s) ∘ π₁) (idC +₁ w) ○ (case⟩ refl ⟨inl⟩ (pullˡ (+₁∘i₁ ○ identityʳ)) ⟨inr⟩ (pullˡ +₁∘i₂ ○ assoc)) ⟩
case (f ∘ w) inl (i₁ ∘ π₂) inr (i₂ ∘ w ∘ (idC ⁂ s) ∘ π₁) ≈⟨ (case⟩ refl ⟨inl⟩ refl ⟨inr⟩ (refl⟩∘⟨ (pullˡ (sym commute₂) ○ assoc))) ⟩
case (f ∘ w) inl (i₁ ∘ π₂) inr (i₂ ∘ (case f inl π₁ inr π₂) ∘ w ∘ π₁) ≈⟨ (case⟩ refl ⟨inl⟩ refl ⟨inr⟩ (refl⟩∘⟨ (pullˡ (case∘ʳ f π₁ π₂ w)))) ⟩
(case (f ∘ w) inl (i₁ ∘ π₂) inr (i₂ ∘ (case f ∘ w inl (π₁ ∘ (w ⁂ idC)) inr (π₂ ∘ (w ⁂ idC))) ∘ π₁)) ≈⟨ (case⟩ refl ⟨inl⟩ refl ⟨inr⟩ (pullˡ (case∘ˡ (f ∘ w) (π₁ ∘ (w ⁂ idC)) (π₂ ∘ (w ⁂ idC)) i₂))) ⟩
(case (f ∘ w) inl (i₁ ∘ π₂) inr ((case f ∘ w inl (i₂ ∘ π₁ ∘ (w ⁂ idC)) inr (i₂ ∘ π₂ ∘ (w ⁂ idC))) ∘ π₁)) ≈⟨ case-nested (f ∘ w) (i₁ ∘ π₂) (i₂ ∘ π₁ ∘ (w ⁂ idC)) (i₂ ∘ π₂ ∘ (w ⁂ idC)) ⟩
(case f ∘ w inl i₁ ∘ π₂ inr (i₂ ∘ π₂ ∘ (w ⁂ idC))) ≈⟨ (case⟩ refl ⟨inl⟩ refl ⟨inr⟩ (refl⟩∘⟨ (π₂∘⁂ ○ identityˡ))) ○ case-id (f ∘ w) ⟩
f ∘ w ∎
```