open import Categories.Category.Core
open import Categories.Category.Distributive
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP
module Misc.Cases {o ℓ e} {𝒞 : Category o ℓ e} (distributive : Distributive 𝒞) where
open import Category.Distributive.Helper distributive
open Category 𝒞
open HomReasoning
open Equiv
open M 𝒞
open MR 𝒞
open MP 𝒞
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ˡ⁻¹ ∘ ⟨ id , f ⟩
caseʳ_inl_inr : ∀ {X Y Z U} → X ⇒ Y + Z → Y × X ⇒ U → Z × X ⇒ U → X ⇒ U
caseʳ f inl g inr h = [ g , h ] ∘ distributeʳ⁻¹ ∘ ⟨ f , id ⟩
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ˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ sym (pullˡ []∘+₁) ⟩
[ g , h ] ∘ (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ refl⟩∘⟨ pullˡ distributeˡ⁻¹-π₂ ⟩
[ g , h ] ∘ π₂ ∘ ⟨ id , 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∘ˡ : ∀ {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 ⁂ id)) inr (h ∘ (r ⁂ id))
case∘ʳ f g h r = begin
(case f inl g inr h) ∘ r ≈⟨ pullʳ (pullʳ ⟨⟩∘) ⟩
[ g , h ] ∘ distributeˡ⁻¹ ∘ ⟨ id ∘ r , f ∘ r ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ id-comm identityˡ) ⟩
[ g , h ] ∘ distributeˡ⁻¹ ∘ (r ⁂ id) ∘ ⟨ id , f ∘ r ⟩ ≈⟨ refl⟩∘⟨ (pullˡ (refl⟩∘⟨ (⁂-cong₂ refl (sym ([]-unique id-comm-sym id-comm-sym))) ○ sym (distributeˡ⁻¹-natural r id id))) ⟩
[ g , h ] ∘ (((r ⁂ id) +₁ (r ⁂ id)) ∘ distributeˡ⁻¹) ∘ ⟨ id , f ∘ r ⟩ ≈⟨ pullˡ (pullˡ []∘+₁) ○ assoc ⟩
(case f ∘ r inl (g ∘ (r ⁂ id)) inr (h ∘ (r ⁂ id))) ∎
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'
private
nested-helper : ∀ {X Y Z} → distributeˡ⁻¹ ∘ ⟨ id {X × (Y + Z)} , π₂ ⟩ ≈ (⟨ (id ⁂ i₁) , π₂ ⟩ +₁ ⟨ (id ⁂ i₂) , π₂ ⟩) ∘ distributeˡ⁻¹
nested-helper = Iso⇒Epi (IsIso.iso isIsoˡ) (distributeˡ⁻¹ ∘ ⟨ id , π₂ ⟩) ((⟨ id ⁂ i₁ , π₂ ⟩ +₁ ⟨ id ⁂ i₂ , π₂ ⟩) ∘ distributeˡ⁻¹) (begin
(distributeˡ⁻¹ ∘ ⟨ id , π₂ ⟩) ∘ distributeˡ ≈⟨ ∘[] ⟩
[ ((distributeˡ⁻¹ ∘ ⟨ id , π₂ ⟩) ∘ (id ⁂ i₁)) , ((distributeˡ⁻¹ ∘ ⟨ id , π₂ ⟩) ∘ (id ⁂ i₂)) ] ≈⟨ []-cong₂ (pullʳ ⟨⟩∘) (pullʳ ⟨⟩∘) ⟩
[ (distributeˡ⁻¹ ∘ ⟨ id ∘ (id ⁂ i₁) , π₂ ∘ (id ⁂ i₁) ⟩) , (distributeˡ⁻¹ ∘ ⟨ id ∘ (id ⁂ i₂) , π₂ ∘ (id ⁂ i₂) ⟩) ] ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ π₂∘⁂)) (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ π₂∘⁂)) ⟩
[ distributeˡ⁻¹ ∘ ⟨ (id ⁂ i₁) , i₁ ∘ π₂ ⟩ , distributeˡ⁻¹ ∘ ⟨ (id ⁂ i₂) , i₂ ∘ π₂ ⟩ ] ≈˘⟨ []-cong₂ (refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl)) (refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl)) ⟩
[ distributeˡ⁻¹ ∘ (id ⁂ i₁) ∘ ⟨ (id ⁂ i₁) , π₂ ⟩ , distributeˡ⁻¹ ∘ (id ⁂ i₂) ∘ ⟨ (id ⁂ i₂) , π₂ ⟩ ] ≈⟨ []-cong₂ (pullˡ distributeˡ⁻¹-i₁) (pullˡ distributeˡ⁻¹-i₂) ⟩
[ i₁ ∘ ⟨ (id ⁂ i₁) , π₂ ⟩ , i₂ ∘ ⟨ (id ⁂ i₂) , π₂ ⟩ ] ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoˡ) ⟩
((⟨ (id ⁂ i₁) , π₂ ⟩ +₁ ⟨ (id ⁂ i₂) , π₂ ⟩) ∘ distributeˡ⁻¹) ∘ distributeˡ ∎)
case-nestedˡ : ∀ {X Y Z U} (f : X ⇒ Y + Z) (g : X × Y ⇒ U) (h h' : X × Z ⇒ U) → case f inl ((case f inl g inr h') ∘ π₁) inr h ≈ case f inl g inr h
case-nestedˡ f g h h' = begin
[ ([ g , h' ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩) ∘ π₁ , h ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ (pullʳ (pullʳ project₁) ○ sym assoc²βε) (cancelʳ (⁂∘⁂ ○ ⁂-cong₂ project₁ identity² ○ ⟨⟩-unique id-comm id-comm))) ⟩
[ [ g , h' ] ∘ distributeˡ⁻¹ ∘ π₁ , h ∘ (π₁ ⁂ id) ] ∘ (⟨ id , f ⟩ ⁂ id +₁ ⟨ id , f ⟩ ⁂ id) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ refl⟩∘⟨ (extendʳ (distributeˡ⁻¹-natural _ _ _ ○ ∘-resp-≈ʳ (⁂-cong₂ refl ([]-unique id-comm-sym id-comm-sym)))) ⟩
[ [ g , h' ] ∘ distributeˡ⁻¹ ∘ π₁ , h ∘ (π₁ ⁂ id) ] ∘ distributeˡ⁻¹ ∘ (⟨ id , f ⟩ ⁂ id) ∘ ⟨ id , f ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩
[ [ g , h' ] ∘ distributeˡ⁻¹ ∘ π₁ , h ∘ (π₁ ⁂ id) ] ∘ distributeˡ⁻¹ ∘ ⟨ ⟨ id , f ⟩ , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ project₂) ⟩
[ [ g , h' ] ∘ distributeˡ⁻¹ ∘ π₁ , h ∘ (π₁ ⁂ id) ] ∘ distributeˡ⁻¹ ∘ ⟨ id , π₂ ⟩ ∘ ⟨ id , f ⟩ ≈⟨ refl⟩∘⟨ (extendʳ nested-helper) ⟩
[ [ g , h' ] ∘ distributeˡ⁻¹ ∘ π₁ , h ∘ (π₁ ⁂ id) ] ∘ (⟨ (id ⁂ i₁) , π₂ ⟩ +₁ ⟨ (id ⁂ i₂) , π₂ ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ assoc²βε assoc) ⟩
[ [ g , h' ] ∘ distributeˡ⁻¹ ∘ π₁ ∘ ⟨ (id ⁂ i₁) , π₂ ⟩ , h ∘ (π₁ ⁂ id) ∘ ⟨ (id ⁂ i₂) , π₂ ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ ([]-cong₂ (∘-resp-≈ʳ (∘-resp-≈ʳ project₁)) (∘-resp-≈ʳ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ refl identityˡ))) ⟩∘⟨refl ⟩
[ [ g , h' ] ∘ distributeˡ⁻¹ ∘ (id ⁂ i₁) , h ∘ ⟨ π₁ ∘ (id ⁂ i₂) , π₂ ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ ([]-cong₂ (∘-resp-≈ʳ distributeˡ⁻¹-i₁) (∘-resp-≈ʳ (⟨⟩-cong₂ (project₁ ○ identityˡ) refl))) ⟩∘⟨refl ⟩
[ [ g , h' ] ∘ i₁ , h ∘ ⟨ π₁ , π₂ ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ ([]-cong₂ inject₁ (elimʳ (⟨⟩-unique identityʳ identityʳ))) ⟩∘⟨refl ⟩
[ g , h ] ∘ distributeˡ⁻¹ ∘ ⟨ id , 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ˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ refl ⟩
[ g , ([ g' , h ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩) ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈˘⟨ ([]-cong₂ (elimʳ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ (cancelˡ project₁) (cancelˡ identity²) ○ ⁂-η)) (sym (pullʳ (pullʳ (sym π₁∘⁂))))) ⟩∘⟨refl ⟩
[ g ∘ (π₁ ⁂ id) ∘ (⟨ id , f ⟩ ⁂ id) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ∘ (⟨ id , f ⟩ ⁂ id) ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ assoc assoc²βε) ⟩
[ g ∘ (π₁ ⁂ id) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ] ∘ ((⟨ id , f ⟩ ⁂ id) +₁ (⟨ id , f ⟩ ⁂ id)) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ refl⟩∘⟨ pullˡ (distributeˡ⁻¹-natural ⟨ id , f ⟩ id id ○ refl⟩∘⟨ ⁂-cong₂ refl ([]-unique id-comm-sym id-comm-sym)) ⟩
[ g ∘ (π₁ ⁂ id) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ] ∘ (distributeˡ⁻¹ ∘ (⟨ id , f ⟩ ⁂ id)) ∘ ⟨ id , f ⟩ ≈⟨ refl⟩∘⟨ (pullʳ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ)) ⟩
[ g ∘ (π₁ ⁂ id) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ ⟨ id , f ⟩ , f ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl project₂ ⟩
[ g ∘ (π₁ ⁂ id) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ ⟨ id , f ⟩ , π₂ ∘ ⟨ id , f ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩∘ ○ refl⟩∘⟨ (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ refl)) ⟩
[ g ∘ (π₁ ⁂ id) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , π₂ ⟩ ∘ ⟨ id , f ⟩ ≈⟨ refl⟩∘⟨ pullˡ nested-helper ⟩
[ g ∘ (π₁ ⁂ id) , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ] ∘ ((⟨ (id ⁂ i₁) , π₂ ⟩ +₁ ⟨ (id ⁂ i₂) , π₂ ⟩) ∘ distributeˡ⁻¹) ∘ ⟨ id , f ⟩ ≈⟨ refl⟩∘⟨ assoc ○ pullˡ ([]∘+₁ ○ []-cong₂ assoc assoc²βε) ⟩
[ g ∘ (π₁ ⁂ id) ∘ ⟨ (id ⁂ i₁) , π₂ ⟩ , [ g' , h ] ∘ distributeˡ⁻¹ ∘ π₁ ∘ ⟨ (id ⁂ i₂) , π₂ ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ ([]-cong₂ (refl⟩∘⟨ ⁂∘⟨⟩) (refl⟩∘⟨ refl⟩∘⟨ project₁)) ⟩∘⟨refl ⟩
[ g ∘ ⟨ π₁ ∘ (id ⁂ i₁) , id ∘ π₂ ⟩ , [ g' , h ] ∘ distributeˡ⁻¹ ∘ (id ⁂ i₂) ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ ([]-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ π₁∘⁂ refl)) (refl⟩∘⟨ distributeˡ⁻¹-i₂)) ⟩∘⟨refl ⟩
[ g ∘ ⟨ id ∘ π₁ , id ∘ π₂ ⟩ , [ g' , h ] ∘ i₂ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ []-cong₂ (elimʳ (⟨⟩-cong₂ identityˡ identityˡ ○ ⁂-η)) inject₂ ⟩∘⟨refl ⟩
[ g , h ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ∎
case-nestedʳ' : ∀ {X Y Z : Obj} (f : X × Y ⇒ Z + X) (g : (X × Y) × Z ⇒ Z + X × X × Y) (g' : (X × Y) × Z ⇒ X) (h : (X × Y) × X ⇒ X) (i : X × Y ⇒ Y) → case f inl g inr (i₂ {Z} {X × X × Y} ∘ ⟨ π₁ ∘ π₁ , ⟨ (case f inl g' inr h) ∘ π₁ {X × Y} {X} , i ∘ π₁ ⟩ ⟩) ≈ case f inl g inr (i₂ ∘ ⟨ π₁ ∘ π₁ , ⟨ h , i ∘ π₁ ⟩ ⟩)
case-nestedʳ' f g g' h i = begin
[ g , i₂ ∘ ⟨ π₁ ∘ π₁ , ⟨ ([ g' , h ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩) ∘ π₁ , i ∘ π₁ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
[ g , i₂ ∘ ⟨ π₁ , ⟨ ([ g' , h ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩) , i ⟩ ⟩ ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
[ g , i₂ ∘ ⟨ π₁ , ⟨ case f inl g' inr h , i ⟩ ⟩ ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
[ g , i₂ ∘ (case f inl {! !} inr (⟨ π₁ ∘ π₁ , ⟨ h , i ∘ π₁ ⟩ ⟩)) ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
[ g , (case f inl i₂ ∘ {! !} inr (i₂ ∘ ⟨ π₁ ∘ π₁ , ⟨ h , i ∘ π₁ ⟩ ⟩)) ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
[ g , i₂ ∘ ⟨ π₁ ∘ π₁ , ⟨ h , i ∘ π₁ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ∎
where
helper : ⟨ π₁ , ⟨ case f inl g' inr h , i ⟩ ⟩ ≈ case f inl ⟨ g' , π₁ ⟩ inr (⟨ π₁ ∘ π₁ , ⟨ h , i ∘ π₁ ⟩ ⟩)
helper = ⟨⟩-unique left right
where
left : π₁ ∘ case f inl ⟨ g' , π₁ ⟩ inr (⟨ π₁ ∘ π₁ , ⟨ h , i ∘ π₁ ⟩ ⟩) ≈ π₁
left = begin
π₁ ∘ [ ⟨ g' , π₁ ⟩ , ⟨ π₁ ∘ π₁ , ⟨ h , i ∘ π₁ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
[ g' , π₁ ∘ π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
π₁ ∎
right : π₂ ∘ case f inl ⟨ g' , π₁ ⟩ inr (⟨ π₁ ∘ π₁ , ⟨ h , i ∘ π₁ ⟩ ⟩) ≈ ⟨ case f inl g' inr h , i ⟩
right = begin
π₂ ∘ [ ⟨ g' , π₁ ⟩ , ⟨ π₁ ∘ π₁ , ⟨ h , i ∘ π₁ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
[ π₁ , ⟨ h , i ∘ π₁ ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
⟨ case f inl g' inr h , i ⟩ ∎
double-case : ∀ {X Y Z U V W} (f : X ⇒ Y + Z) (g : X × Y ⇒ U) (h : X × Z ⇒ V) (u : X × U ⇒ W) (v : X × V ⇒ W) → case (case f inl (i₁ ∘ g) inr (i₂ ∘ h)) inl u inr v ≈ case f inl u ∘ ⟨ π₁ , g ⟩ inr (v ∘ ⟨ π₁ , h ⟩)
double-case f g h u v = begin
[ u , v ] ∘ distributeˡ⁻¹ ∘ ⟨ id , [ i₁ ∘ g , i₂ ∘ h ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ⟩ ≈⟨ refl⟩∘⟨ (∘-resp-≈ʳ helper ○ cancelˡ (IsIso.isoˡ isIsoˡ)) ⟩
[ u , v ] ∘ (⟨ π₁ , g ⟩ +₁ ⟨ π₁ , h ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ refl refl) ⟩
[ u ∘ ⟨ π₁ , g ⟩ , v ∘ ⟨ π₁ , h ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ∎
where
helper : ⟨ id , [ i₁ ∘ g , i₂ ∘ h ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ⟩ ≈ distributeˡ ∘ (⟨ π₁ , g ⟩ +₁ ⟨ π₁ , h ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩
helper = begin
⟨ id , [ i₁ ∘ g , i₂ ∘ h ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ⟩ ≈⟨ ⟨⟩-unique pr₁ pr₂ ⟩
[ ⟨ π₁ , i₁ ∘ g ⟩ , ⟨ π₁ , i₂ ∘ h ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl)) ⟩
[ id ⁂ i₁ , id ⁂ i₂ ] ∘ (⟨ π₁ , g ⟩ +₁ ⟨ π₁ , h ⟩) ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ∎
where
pr₁ : π₁ ∘ [ ⟨ π₁ , i₁ ∘ g ⟩ , ⟨ π₁ , i₂ ∘ h ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈ id
pr₁ = begin
π₁ ∘ [ ⟨ π₁ , i₁ ∘ g ⟩ , ⟨ π₁ , i₂ ∘ h ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ pullˡ (∘[] ○ []-cong₂ project₁ project₁) ⟩
[ π₁ , π₁ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈⟨ pullˡ distributeˡ⁻¹-π₁ ⟩
π₁ ∘ ⟨ id , f ⟩ ≈⟨ project₁ ⟩
id ∎
pr₂ : π₂ ∘ [ ⟨ π₁ , i₁ ∘ g ⟩ , ⟨ π₁ , i₂ ∘ h ⟩ ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩ ≈ [ i₁ ∘ g , i₂ ∘ h ] ∘ distributeˡ⁻¹ ∘ ⟨ id , f ⟩
pr₂ = pullˡ (∘[] ○ []-cong₂ project₂ project₂)