open import Categories.Category.Core
open import Categories.Category.Distributive using (Distributive)
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.Cocartesian using (Cocartesian)
open import Categories.Category.BinaryProducts using (BinaryProducts)
open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
open import Categories.Category.Cartesian.Monoidal
open import Categories.Category.Cartesian.SymmetricMonoidal using () renaming (symmetric to symm)
open import Categories.Category.Monoidal using (Monoidal)
open import Categories.Category.Monoidal.Symmetric using (Symmetric)
open import Categories.Category.Monoidal.Braided using (Braided)

import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP


-- Some helpers to make working with distributive categories easier

module Category.Distributive.Helper {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) where
  open Category C
  -- open cartesian and cocartesian publically, because usually both are needed when working with a distributive category.
  open Distributive distributive public
  open import Categories.Category.Distributive.Properties distributive public
  open Cocartesian cocartesian renaming (+-unique to []-unique) public
  open Cartesian cartesian public
  open BinaryProducts products renaming (η to ⁂-η; g-η to ⁂-g-η; unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′) public
  open CartesianMonoidal cartesian using (⊤×A≅A; A×⊤≅A) public
  open Dual.op-binaryProducts using () renaming (unique′ to []-unique′) public

  -- the codiagonal
  ∇ : ∀ {X} → X + X ⇒ X
  ∇ = [ id , id ]

  -- other bundles that can be derived
  module Bundles where
    cartesianCategory : CartesianCategory o ℓ e
    cartesianCategory = record { U = C ; cartesian = cartesian }

    monoidal : Monoidal C
    monoidal = CartesianMonoidal.monoidal cartesian

    symmetric : Symmetric monoidal
    symmetric = symm C cartesian

    braided : Braided monoidal
    braided = Symmetric.braided symmetric

  
  -- some lemmas
  open M C
  open MR C
  open MP C
  open HomReasoning
  open Equiv

  distributeˡ⁻¹-natural-id : ∀ {X Y U V} {f : X ⇒ Y} → ((f ⁂ id {U}) +₁ (f ⁂ id {V})) ∘ distributeˡ⁻¹ ≈ distributeˡ⁻¹ ∘ (f ⁂ id)
  distributeˡ⁻¹-natural-id {X} {Y} {U} {V} {f} = distributeˡ⁻¹-natural f id id ○ ∘-resp-≈ʳ (⁂-cong₂ refl ([]-unique id-comm-sym id-comm-sym))

  distribute₄ : ∀ {A B C D} → (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ {A + B} {C} {D} ≈ [ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹
  distribute₄ = Iso⇒Epi (IsIso.iso isIsoʳ) ((distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) (begin 
    (((distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ∘ distributeʳ)                                                                                                ≈⟨ ∘[] ⟩ 
    [ (((distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ∘ (i₁ ⁂ id)) , (((distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ∘ (i₂ ⁂ id)) ]                         ≈⟨ []-cong₂ (pullʳ ((refl⟩∘⟨ (⁂-cong₂ refl (sym ([]-unique id-comm-sym id-comm-sym)))) ○ sym (distributeˡ⁻¹-natural i₁ id id))) (pullʳ (((refl⟩∘⟨ (⁂-cong₂ refl (sym ([]-unique id-comm-sym id-comm-sym)))) ○ sym (distributeˡ⁻¹-natural i₂ id id)))) ⟩ 
    [ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ ((i₁ ⁂ id) +₁ (i₁ ⁂ id)) ∘ distributeˡ⁻¹ , (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ ((i₂ ⁂ id) +₁ (i₂ ⁂ id)) ∘ distributeˡ⁻¹ ] ≈⟨ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ distributeʳ⁻¹-i₁ distributeʳ⁻¹-i₁)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ distributeʳ⁻¹-i₂ distributeʳ⁻¹-i₂)) ⟩
    [ (i₁ +₁ i₁) ∘ distributeˡ⁻¹ , (i₂ +₁ i₂) ∘ distributeˡ⁻¹ ]                                                                                                       ≈˘⟨ []∘+₁ ⟩ 
    ([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹))                                                                                                      ≈˘⟨ pullʳ (cancelʳ (IsIso.isoˡ isIsoʳ)) ⟩ 
    (([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ distributeʳ)                                                                      ∎)

  distributeˡ⁻¹-assoc : ∀ {A B C D : Obj} → distributeˡ⁻¹ ∘ (id ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc ≈ (_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ∘ distributeˡ⁻¹ {A × B} {C} {D}
  distributeˡ⁻¹-assoc {A} {B} {U} {D} = Iso⇒Epi (IsIso.iso isIsoˡ) (distributeˡ⁻¹ ∘ (id ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ((_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ∘ distributeˡ⁻¹) (begin 
    (distributeˡ⁻¹ ∘ (id ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ∘ [ id ⁂ i₁ , id ⁂ i₂ ]                                                                                                                          ≈⟨ ∘[] ⟩ 
    [ (distributeˡ⁻¹ ∘ (id ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ∘ (id ⁂ i₁) , (distributeˡ⁻¹ ∘ (id ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ∘ (id ⁂ i₂) ]                                                           ≈⟨ []-cong₂ (pullʳ (pullʳ ⟨⟩∘)) (pullʳ (pullʳ ⟨⟩∘)) ⟩ 
    [ distributeˡ⁻¹ ∘ (id ⁂ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (id ⁂ i₁) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (id ⁂ i₁) ⟩ , distributeˡ⁻¹ ∘ (id ⁂ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (id ⁂ i₂) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (id ⁂ i₂) ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ ⁂∘⟨⟩) (refl⟩∘⟨ ⁂∘⟨⟩) ⟩ 
    [ distributeˡ⁻¹ ∘ ⟨ id ∘ (π₁ ∘ π₁) ∘ (id ⁂ i₁) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (id ⁂ i₁) ⟩ , distributeˡ⁻¹ ∘ ⟨ id ∘ (π₁ ∘ π₁) ∘ (id ⁂ i₂) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (id ⁂ i₂) ⟩ ]     ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ refl)) (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ refl)) ⟩ 
    [ distributeˡ⁻¹ ∘ ⟨ (π₁ ∘ π₁) ∘ (id ⁂ i₁) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (id ⁂ i₁) ⟩ , distributeˡ⁻¹ ∘ ⟨ (π₁ ∘ π₁) ∘ (id ⁂ i₂) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (id ⁂ i₂) ⟩ ]                 ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) (refl⟩∘⟨ ⟨⟩∘))) (refl⟩∘⟨ ⟨⟩-cong₂ (pullʳ π₁∘⁂) (refl⟩∘⟨ ⟨⟩∘)) ⟩ 
    [ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ id ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ (π₂ ∘ π₁) ∘ (id ⁂ i₁) , π₂ ∘ (id ⁂ i₁) ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ id ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ (π₂ ∘ π₁) ∘ (id ⁂ i₂) , π₂ ∘ (id ⁂ i₂) ⟩ ⟩ ]     ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)))) (refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)))) ⟩ 
    [ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ id ∘ π₁ , i₁ ∘ π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ id ∘ π₁ , i₂ ∘ π₂ ⟩ ⟩ ]                                                   ≈⟨ []-cong₂ (refl⟩∘⟨ ⟨⟩-cong₂ refl (refl⟩∘⟨ ⟨⟩-cong₂ ((refl⟩∘⟨ identityˡ) ○ sym identityˡ) refl)) (refl⟩∘⟨ ⟨⟩-cong₂ refl (refl⟩∘⟨ ⟨⟩-cong₂ ((refl⟩∘⟨ identityˡ) ○ sym identityˡ) refl)) ⟩ 
    [ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ id ∘ π₂ ∘ π₁ , i₁ ∘ π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ id ∘ π₂ ∘ π₁ , i₂ ∘ π₂ ⟩ ⟩ ]                                                   ≈˘⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ ⁂∘⟨⟩))) (refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ ⁂∘⟨⟩))) ⟩  
    [ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ (id ⁂ i₁) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ (id ⁂ i₂) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ]                                               ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (pullˡ distributeˡ⁻¹-i₁))) (refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (pullˡ distributeˡ⁻¹-i₂))) ⟩ 
    [ distributeˡ⁻¹ ∘ ⟨ id ∘ π₁ ∘ π₁ , i₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ id ∘ π₁ ∘ π₁ , i₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ]                                                                                   ≈˘⟨ []-cong₂ (refl⟩∘⟨ ⁂∘⟨⟩) (refl⟩∘⟨ ⁂∘⟨⟩) ⟩ 
    [ distributeˡ⁻¹ ∘ (id ⁂ i₁) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ (id ⁂ i₂) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ]                                                                               ≈⟨ []-cong₂ (pullˡ distributeˡ⁻¹-i₁) (pullˡ distributeˡ⁻¹-i₂) ⟩ 
    (_≅_.to ×-assoc +₁ _≅_.to ×-assoc)                                                                                                                                                                          ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoˡ) ⟩ 
    ((_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ∘ distributeˡ⁻¹) ∘ distributeˡ                                                                                                                                          ∎)

  [⟨⟩]≈⟨[]⟩ : ∀ {A B C D} (f : A ⇒ B) (g : A ⇒ C) (h : D ⇒ B) (i : D ⇒ C) → [ ⟨ f , g ⟩ , ⟨ h , i ⟩ ] ≈ ⟨ [ f , h ] , [ g , i ] ⟩
  [⟨⟩]≈⟨[]⟩ f g h i = []-unique (⟨⟩∘ ○ ⟨⟩-cong₂ inject₁ inject₁) (⟨⟩∘ ○ ⟨⟩-cong₂ inject₂ inject₂)  

  distr : ∀ {X Y Z W} → (X + Y) × (Z + W) ⇒ (X × Z + (X × W + Y × Z)) + Y × W
  distr = [ i₁ ∘ (id +₁ i₁) ∘ distributeˡ⁻¹ ,  (i₂ ∘ i₂ +₁ id) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹

  distr-i₁+i₁ : ∀ {X Y Z W} →  distr {X}{Y}{Z}{W} ∘ (i₁ ⁂ i₁) ≈ i₁ ∘ i₁
  distr-i₁+i₁ =
    begin
      distr ∘ (i₁ ⁂ i₁)                                                                                  ≈˘⟨  ∘-resp-≈ʳ (⁂∘⁂ ○ ⁂-cong₂ identityʳ identityˡ) ⟩
      distr ∘ (i₁ ⁂ id) ∘ (id ⁂ i₁)                                                                      ≈⟨ pullˡ (pullʳ distributeʳ⁻¹-i₁) ⟩
      ([ i₁ ∘ (id +₁ i₁) ∘ distributeˡ⁻¹ , (i₂ ∘ i₂ +₁ id) ∘ distributeˡ⁻¹ ] ∘ i₁) ∘ (id ⁂ i₁)           ≈⟨ pushˡ inject₁ ⟩ 
      i₁ ∘ ((id +₁ i₁) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₁)                                                      ≈⟨ refl⟩∘⟨ pullʳ distributeˡ⁻¹-i₁ ⟩ 
      i₁ ∘ (id +₁ i₁) ∘ i₁                                                                               ≈⟨ refl⟩∘⟨ inject₁ ○ ∘-resp-≈ refl identityʳ ⟩
      i₁ ∘ i₁
    ∎

  distr-i₂+i₂ : ∀ {X Y Z W} →  distr {X}{Y}{Z}{W} ∘ (i₂ ⁂ i₂) ≈ i₂
  distr-i₂+i₂ =
    begin
      distr ∘ (i₂ ⁂ i₂)                                                                                  ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityʳ identityˡ) ⟩
      distr ∘ (i₂ ⁂ id) ∘ (id ⁂ i₂)                                                                      ≈⟨ pullˡ (pullʳ distributeʳ⁻¹-i₂) ⟩
      ([ i₁ ∘ (id +₁ i₁) ∘ distributeˡ⁻¹ , (i₂ ∘ i₂ +₁ id) ∘ distributeˡ⁻¹ ] ∘ i₂) ∘ (id ⁂ i₂)           ≈⟨ pushˡ inject₂ ⟩
      (i₂ ∘ i₂ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ i₂)                                                        ≈⟨ refl⟩∘⟨ distributeˡ⁻¹-i₂ ⟩
      (i₂ ∘ i₂ +₁ id) ∘ i₂                                                                               ≈⟨ +₁∘i₂ ○ identityʳ ⟩
      i₂
    ∎

  distr-i₁+i₂ : ∀ {X Y Z W} → distr {X}{Y}{Z}{W} ∘ (i₁ ⁂ i₂) ≈ (i₁ ∘ i₂) ∘ i₁
  distr-i₁+i₂ =
    begin
      distr ∘ (i₁ ⁂ i₂)                                                                                    ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityʳ identityˡ) ⟩
      distr ∘ (i₁ ⁂ id) ∘ (id ⁂ i₂)                                                                       ≈⟨ pullˡ (pullʳ distributeʳ⁻¹-i₁) ⟩
      ([ i₁ ∘ (id +₁ i₁) ∘ distributeˡ⁻¹ , (i₂ ∘ i₂ +₁ id) ∘ distributeˡ⁻¹ ] ∘ i₁) ∘ (id ⁂ i₂)             ≈⟨ pushˡ inject₁ ⟩
      i₁ ∘ ((id +₁ i₁) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₂)                                                        ≈⟨ refl⟩∘⟨ pullʳ distributeˡ⁻¹-i₂ ⟩
      i₁ ∘ (id +₁ i₁) ∘ i₂                                                                                  ≈⟨ ∘-resp-≈ʳ +₁∘i₂ ○ sym-assoc ⟩
      (i₁ ∘ i₂) ∘ i₁    ∎

  distr-i₂+i₁ : ∀ {X Y Z W} → distr {X}{Y}{Z}{W} ∘ (i₂ ⁂ i₁) ≈ (i₁ ∘ i₂) ∘ i₂
  distr-i₂+i₁ =
    begin
      distr ∘ (i₂ ⁂ i₁)                                                                                   ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identityʳ identityˡ) ⟩
      distr ∘ (i₂ ⁂ id) ∘ (id ⁂ i₁)                                                                      ≈⟨ pullˡ (pullʳ distributeʳ⁻¹-i₂) ⟩
      ([ i₁ ∘ (id +₁ i₁) ∘ distributeˡ⁻¹ , (i₂ ∘ i₂ +₁ id) ∘ distributeˡ⁻¹ ] ∘ i₂) ∘ (id ⁂ i₁)            ≈⟨ pushˡ inject₂ ⟩
      (i₂ ∘ i₂ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ i₁)                                                         ≈⟨ refl⟩∘⟨ distributeˡ⁻¹-i₁ ⟩
      (i₂ ∘ i₂ +₁ id) ∘ i₁                                                                                 ≈⟨ +₁∘i₁ ○ sym-assoc ⟩
      (i₁ ∘ i₂) ∘ i₂    ∎
      
  distr-helper : ∀ {X Y Z W} →  distr {X}{Y}{Z}{W} ∘ ⟨ [ i₁ ∘ π₁ , π₁ +₁ π₁ ] , [ i₁ ∘ π₂ , [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ] ⟩ ≈ i₁
  distr-helper = []-unique′ (assoc ○ eq₁) ([]-unique′ (assoc ○ assoc ○ eq₂) (assoc ○ assoc ○ eq₃)) 
    where
    
      eq₁ = begin
        distr ∘ ⟨ [ i₁ ∘ π₁ , π₁ +₁ π₁ ] , [ i₁ ∘ π₂ , [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ] ⟩ ∘ i₁
          ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ inject₁ inject₁) ⟩
        distr ∘ ⟨ i₁ ∘ π₁ , i₁ ∘ π₂ ⟩ 
          ≈˘⟨ refl⟩∘⟨ ⁂∘⟨⟩ ⟩
        distr ∘ (i₁ ⁂ i₁) ∘ ⟨ π₁ , π₂ ⟩
          ≈⟨ pullˡ distr-i₁+i₁ ⟩
        (i₁ ∘ i₁) ∘ ⟨ π₁ , π₂ ⟩
          ≈⟨ ∘-resp-≈ʳ ⁂-η ○ identityʳ ⟩
        i₁ ∘ i₁ ∎
        
      eq₂ = begin
        distr ∘ ⟨ [ i₁ ∘ π₁ , π₁ +₁ π₁ ] , [ i₁ ∘ π₂ , [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ] ⟩ ∘ i₂ ∘ i₁
          ≈⟨ refl⟩∘⟨ pullˡ (⟨⟩∘ ○ ⟨⟩-cong₂ inject₂ inject₂) ⟩
        distr ∘  ⟨ π₁ +₁ π₁ , [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ⟩ ∘ i₁
          ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ inject₁ inject₁) ⟩
        distr ∘  ⟨ i₁ ∘ π₁ , i₂ ∘ π₂ ⟩ 
          ≈˘⟨ refl⟩∘⟨ ⁂∘⟨⟩ ⟩
        distr ∘ (i₁ ⁂ i₂) ∘ ⟨ π₁ , π₂ ⟩
          ≈⟨ pullˡ distr-i₁+i₂ ⟩
        ((i₁ ∘ i₂) ∘ i₁) ∘ ⟨ π₁ , π₂ ⟩
          ≈⟨ ∘-resp-≈ʳ ⁂-η ○ identityʳ ⟩
        (i₁ ∘ i₂) ∘ i₁  ∎

      eq₃ = begin
        distr ∘ ⟨ [ i₁ ∘ π₁ , π₁ +₁ π₁ ] , [ i₁ ∘ π₂ , [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ] ⟩ ∘ i₂ ∘ i₂
          ≈⟨ refl⟩∘⟨ pullˡ (⟨⟩∘ ○ ⟨⟩-cong₂ inject₂ inject₂) ⟩
        distr ∘  ⟨ π₁ +₁ π₁ , [ i₂ ∘ π₂ , i₁ ∘ π₂ ] ⟩ ∘ i₂  
          ≈⟨ refl⟩∘⟨ (⟨⟩∘ ○ ⟨⟩-cong₂ inject₂ inject₂) ⟩
        distr ∘  ⟨ i₂ ∘ π₁ , i₁ ∘ π₂ ⟩  
          ≈˘⟨ refl⟩∘⟨ ⁂∘⟨⟩ ⟩
        distr ∘ (i₂ ⁂ i₁) ∘ ⟨ π₁ , π₂ ⟩  
          ≈⟨ pullˡ distr-i₂+i₁ ⟩
        ((i₁ ∘ i₂) ∘ i₂) ∘ ⟨ π₁ , π₂ ⟩  
          ≈⟨ ∘-resp-≈ʳ ⁂-η ○ identityʳ ⟩
        (i₁ ∘ i₂) ∘ i₂  ∎