diff --git a/src/Monad/Instance/K/EquationalLifting.lagda.md b/src/Monad/Instance/K/EquationalLifting.lagda.md index 20d6bd2..23c4eb7 100644 --- a/src/Monad/Instance/K/EquationalLifting.lagda.md +++ b/src/Monad/Instance/K/EquationalLifting.lagda.md @@ -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 ⟩ ∎) ``` diff --git a/src/Monad/Instance/K/PreElgot.lagda.md b/src/Monad/Instance/K/PreElgot.lagda.md index f88f5f7..4b5c15c 100644 --- a/src/Monad/Instance/K/PreElgot.lagda.md +++ b/src/Monad/Instance/K/PreElgot.lagda.md @@ -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 ∎ ```