diff --git a/agda/src/Monad/Instance/Maybe.lagda.md b/agda/src/Monad/Instance/Maybe.lagda.md new file mode 100644 index 0000000..b2d268a --- /dev/null +++ b/agda/src/Monad/Instance/Maybe.lagda.md @@ -0,0 +1,53 @@ + + +# The maybe monad + +```agda +module Monad.Instance.Maybe {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) where + open Category C + open MR C + open HomReasoning + open Equiv + open Distributive distributive + open Cocartesian cocartesian + open Cartesian cartesian using (terminal) + open Terminal terminal + + maybeFunctor : Endofunctor C + maybeFunctor = record + { F₀ = λ X → X + ⊤ + ; F₁ = λ f → f +₁ id + ; identity = +-unique id-comm-sym id-comm-sym + ; homomorphism = λ {X} {Y} {Z} {f} {g} → sym (+₁∘+₁ ○ +₁-cong₂ refl identity²) + ; F-resp-≈ = λ eq → +₁-cong₂ eq refl + } + + open Monad renaming (identityˡ to m-identityˡ; identityʳ to m-identityʳ; assoc to m-assoc; sym-assoc to m-sym-assoc) + + maybeMonad : Monad C + maybeMonad .F = maybeFunctor + maybeMonad .η = ntHelper (record { η = λ X → i₁ ; commute = λ f → sym inject₁ }) + maybeMonad .μ = ntHelper (record { η = λ X → [ id , i₂ ] ; commute = λ f → []∘+₁ ○ []-cong₂ id-comm-sym (sym inject₂) ○ sym ∘[]}) + maybeMonad .m-assoc = begin + [ id , i₂ ] ∘ ([ id , i₂ ] +₁ id) ≈⟨ []∘+₁ ⟩ + [ id ∘ [ id , i₂ ] , i₂ ∘ id ] ≈˘⟨ []-cong₂ id-comm (inject₂ ○ introʳ refl) ⟩ + [ [ id , i₂ ] ∘ id , [ id , i₂ ] ∘ i₂ ] ≈˘⟨ ∘[] ⟩ + [ id , i₂ ] ∘ [ id , i₂ ] ∎ + maybeMonad .m-sym-assoc = sym (m-assoc maybeMonad) + maybeMonad .m-identityˡ = []∘+₁ ○ +-unique refl id-comm-sym + maybeMonad .m-identityʳ = inject₁ +``` \ No newline at end of file diff --git a/agda/src/Monad/Instance/Maybe/Commutative.lagda.md b/agda/src/Monad/Instance/Maybe/Commutative.lagda.md new file mode 100644 index 0000000..7b3d6c6 --- /dev/null +++ b/agda/src/Monad/Instance/Maybe/Commutative.lagda.md @@ -0,0 +1,85 @@ + + +# The maybe monad + +```agda +module Monad.Instance.Maybe.Commutative {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) where + open Category C + open M C + open MR C + open MP C + open HomReasoning + open Equiv + open Distributive distributive + open import Categories.Category.Distributive.Properties distributive + open Cocartesian cocartesian + open Cartesian cartesian using (terminal; products) + open BinaryProducts products renaming (unique to ⟨⟩-unique) + open Terminal terminal + open CartesianMonoidal cartesian using (monoidal) + + open import Monad.Instance.Maybe distributive + open import Monad.Instance.Maybe.Strong distributive + + open Symmetric (symmetric C cartesian) using (braided) + + open Commutative + + 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ʳ) ∎) + + commutativeMaybe : Commutative braided maybeStrong + commutativeMaybe .commutes {X} {Y} = begin + [ id , i₂ ] ∘ ((swap +₁ id) ∘ ((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap +₁ id) ∘ (id +₁ !) ∘ distributeˡ⁻¹ ≈⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ identityˡ)) ⟩ + [ id , i₂ ] ∘ ((swap +₁ id) ∘ ((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap +₁ !) ∘ distributeˡ⁻¹ ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ identityˡ refl) ⟩ + [ (swap +₁ id) ∘ ((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap , i₂ ∘ ! ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ (refl⟩∘⟨ (pullʳ distributeˡ⁻¹∘swap)) (refl⟩∘⟨ !-unique (! ∘ distributeʳ⁻¹))) ⟩∘⟨refl ⟩ + [ (swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap) ∘ distributeʳ⁻¹ , i₂ ∘ ! ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹ ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ assoc²' assoc) ⟩ + [ (swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap) , i₂ ∘ ! ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ≈⟨ refl⟩∘⟨ distribute₄ ⟩ + [ (swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap) , i₂ ∘ ! ] ∘ [ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈⟨ pullˡ ∘[] ⟩ + [ [ (swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap) , i₂ ∘ ! ] ∘ (i₁ +₁ i₁) , [ (swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap) , i₂ ∘ ! ] ∘ (i₂ +₁ i₂) ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ []∘+₁ []∘+₁) ⟩∘⟨refl ⟩ + [ [ ((swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap)) ∘ i₁ , (i₂ ∘ !) ∘ i₁ ] , [ ((swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap)) ∘ i₂ , (i₂ ∘ !) ∘ i₂ ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ ([]-cong₂ (pullʳ (pullʳ inject₁)) (pullʳ (sym (!-unique (! ∘ i₁))))) ([]-cong₂ (pullʳ (pullʳ inject₂)) (pullʳ (sym (!-unique (! ∘ i₂)))))) ⟩∘⟨refl ⟩ + [ [ (swap +₁ id) ∘ (id +₁ !) ∘ i₁ ∘ swap , i₂ ∘ ! ] , [ (swap +₁ id) ∘ (id +₁ !) ∘ i₂ ∘ swap , i₂ ∘ ! ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ ([]-cong₂ (refl⟩∘⟨ (pullˡ (inject₁ ○ identityʳ))) refl) ([]-cong₂ (refl⟩∘⟨ (pullˡ inject₂)) refl)) ⟩∘⟨refl ⟩ + [ [ (swap +₁ id) ∘ i₁ ∘ swap , i₂ ∘ ! ] , [ (swap +₁ id) ∘ (i₂ ∘ !) ∘ swap , i₂ ∘ ! ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ ([]-cong₂ (pullˡ inject₁) refl) ([]-cong₂ (pullˡ (pullˡ (inject₂ ○ identityʳ))) refl)) ⟩∘⟨refl ⟩ + [ [ (i₁ ∘ swap) ∘ swap , i₂ ∘ ! ] , [ (i₂ ∘ !) ∘ swap , i₂ ∘ ! ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ ([]-cong₂ (pullʳ swap∘swap) refl) ([]-cong₂ (pullʳ (sym (!-unique (! ∘ swap)))) refl)) ⟩∘⟨refl ⟩ + [ id +₁ ! , [ i₂ ∘ ! , i₂ ∘ ! ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈⟨ pullˡ []∘+₁ ⟩ + [ (id +₁ !) ∘ distributeˡ⁻¹ , [ i₂ ∘ ! , i₂ ∘ ! ] ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ refl ((sym ∘[]) ⟩∘⟨refl)) ⟩∘⟨refl ⟩ + [ (id +₁ !) ∘ distributeˡ⁻¹ , (i₂ ∘ [ ! , ! ]) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ refl (pullʳ (sym (!-unique ([ ! , ! ] ∘ distributeˡ⁻¹))))) ⟩∘⟨refl ⟩ + [ (id +₁ !) ∘ distributeˡ⁻¹ , i₂ ∘ ! ] ∘ distributeʳ⁻¹ ≈˘⟨ ([]-cong₂ (cancelʳ swap∘swap) (pullʳ (sym (!-unique (! ∘ swap))))) ⟩∘⟨refl ⟩ + [ (((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap) ∘ swap , (i₂ ∘ !) ∘ swap ] ∘ distributeʳ⁻¹ ≈˘⟨ pullˡ []∘+₁ ⟩ + [ ((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap , i₂ ∘ ! ] ∘ (swap +₁ swap) ∘ distributeʳ⁻¹ ≈˘⟨ pullʳ distributeˡ⁻¹∘swap ⟩ + ([ ((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap , i₂ ∘ ! ] ∘ distributeˡ⁻¹) ∘ swap ≈˘⟨ pullˡ (pullˡ ([]∘+₁ ○ []-cong₂ identityˡ (refl⟩∘⟨ identityˡ))) ⟩ + [ id , i₂ ] ∘ (((((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap) +₁ id ∘ !) ∘ distributeˡ⁻¹) ∘ swap ≈˘⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²) ○ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ refl))) ⟩ + [ id , i₂ ] ∘ ((id +₁ !) ∘ distributeˡ⁻¹ +₁ id) ∘ (swap +₁ id) ∘ ((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap ∎ + + +``` \ No newline at end of file diff --git a/agda/src/Monad/Instance/Maybe/EquationalLifting.lagda.md b/agda/src/Monad/Instance/Maybe/EquationalLifting.lagda.md new file mode 100644 index 0000000..5333e8d --- /dev/null +++ b/agda/src/Monad/Instance/Maybe/EquationalLifting.lagda.md @@ -0,0 +1,61 @@ + + +# The maybe monad + +```agda +module Monad.Instance.Maybe.EquationalLifting {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) where + open Category C + open M C + open MR C + open MP C + open HomReasoning + open Equiv + open Distributive distributive + open import Categories.Category.Distributive.Properties distributive + open Cocartesian cocartesian + open Cartesian cartesian using (terminal; products) + open BinaryProducts products renaming (unique to ⟨⟩-unique) + open Terminal terminal + open CartesianMonoidal cartesian using (monoidal) + + equationalLifting : ∀ {X} → ((id +₁ !) ∘ distributeˡ⁻¹) ∘ Δ {X + ⊤} ≈ ⟨ i₁ , id ⟩ +₁ id + equationalLifting = sym (+-unique inj₁ inj₂) + where + inj₁ : (((id +₁ !) ∘ distributeˡ⁻¹) ∘ Δ) ∘ i₁ ≈ i₁ ∘ ⟨ i₁ , id ⟩ + inj₁ = begin + (((id +₁ !) ∘ distributeˡ⁻¹) ∘ Δ) ∘ i₁ ≈⟨ pullʳ Δ∘ ⟩ + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ i₁ , i₁ ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) ⟩ + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₁) ∘ ⟨ i₁ , id ⟩ ≈⟨ pullʳ (pullˡ distributeˡ⁻¹-i₁) ⟩ + (id +₁ !) ∘ i₁ ∘ ⟨ i₁ , id ⟩ ≈⟨ pullˡ (inject₁ ○ identityʳ) ⟩ + i₁ ∘ ⟨ i₁ , id ⟩ ∎ + inj₂ : (((id +₁ !) ∘ distributeˡ⁻¹) ∘ Δ) ∘ i₂ ≈ i₂ ∘ id + inj₂ = begin + (((id +₁ !) ∘ distributeˡ⁻¹) ∘ Δ) ∘ i₂ ≈⟨ pullʳ Δ∘ ⟩ + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ i₂ , i₂ ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) ⟩ + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₂) ∘ ⟨ i₂ , id ⟩ ≈⟨ pullʳ (pullˡ distributeˡ⁻¹-i₂) ⟩ + (id +₁ !) ∘ i₂ ∘ ⟨ i₂ , id ⟩ ≈⟨ pullˡ inject₂ ⟩ + (i₂ ∘ !) ∘ ⟨ i₂ , id ⟩ ≈⟨ pullʳ (sym (!-unique (! ∘ ⟨ i₂ , id ⟩))) ⟩ + i₂ ∘ ! ≈⟨ refl⟩∘⟨ (!-unique id) ⟩ + i₂ ∘ id ∎ +``` \ No newline at end of file diff --git a/agda/src/Monad/Instance/Maybe/Strong.lagda.md b/agda/src/Monad/Instance/Maybe/Strong.lagda.md new file mode 100644 index 0000000..2f812ab --- /dev/null +++ b/agda/src/Monad/Instance/Maybe/Strong.lagda.md @@ -0,0 +1,102 @@ + + +# The maybe monad + +```agda +module Monad.Instance.Maybe.Strong {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) where + open Category C + open M C + open MR C + open MP C + open HomReasoning + open Equiv + open Distributive distributive + open import Categories.Category.Distributive.Properties distributive + open Cocartesian cocartesian + open Cartesian cartesian using (terminal; products) + open BinaryProducts products renaming (unique to ⟨⟩-unique) + open Terminal terminal + open CartesianMonoidal cartesian using (monoidal) + open import Monad.Instance.Maybe distributive + + open StrongMonad using (M; strength) + open Strength renaming (identityˡ to s-identityˡ) + + maybeStrong : StrongMonad monoidal + maybeStrong .M = maybeMonad + maybeStrong .strength .strengthen = ntHelper (record { η = λ X → (id +₁ !) ∘ distributeˡ⁻¹ ; commute = λ {X} {Y} (f , g) → begin + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (f ⁂ (g +₁ id)) ≈⟨ pullʳ (sym (distributeˡ⁻¹-natural f g id)) ⟩ + (id +₁ !) ∘ (f ⁂ g +₁ f ⁂ id) ∘ distributeˡ⁻¹ ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ (sym (!-unique (! ∘ (f ⁂ id))))) ⟩ + (f ⁂ g +₁ !) ∘ distributeˡ⁻¹ ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ identityˡ) ⟩ + (f ⁂ g +₁ id) ∘ (id +₁ !) ∘ distributeˡ⁻¹ ∎ }) + maybeStrong .strength .s-identityˡ = begin + (π₂ +₁ id) ∘ (id +₁ !) ∘ distributeˡ⁻¹ ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ (identityˡ ○ !-unique π₂)) ⟩ + (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ≈⟨ distributeˡ⁻¹-π₂ ⟩ + π₂ ∎ + maybeStrong .strength .η-comm = begin + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₁) ≈⟨ pullʳ distributeˡ⁻¹-i₁ ⟩ + (id +₁ !) ∘ i₁ ≈⟨ inject₁ ○ identityʳ ⟩ + i₁ ∎ + maybeStrong .strength .μ-η-comm = begin + [ id , i₂ ] ∘ (((id +₁ !) ∘ distributeˡ⁻¹) +₁ id) ∘ (id +₁ !) ∘ distributeˡ⁻¹ ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ identityˡ identityʳ) ○ pullˡ ([]∘+₁ ○ []-cong₂ identityʳ refl) ⟩ + [ (id +₁ !) ∘ distributeˡ⁻¹ , i₂ ∘ ! ] ∘ distributeˡ⁻¹ ≈⟨ Iso⇒Epi (IsIso.iso isIsoˡ) ([ (id +₁ !) ∘ distributeˡ⁻¹ , i₂ ∘ ! ] ∘ distributeˡ⁻¹) (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ [ id , i₂ ])) (begin + ([ (id +₁ !) ∘ distributeˡ⁻¹ , i₂ ∘ ! ] ∘ distributeˡ⁻¹) ∘ distributeˡ ≈⟨ cancelʳ (IsIso.isoˡ isIsoˡ) ⟩ + [ (id +₁ !) ∘ distributeˡ⁻¹ , i₂ ∘ ! ] ≈˘⟨ []-cong₂ refl inject₂ ⟩ + [ (id +₁ !) ∘ distributeˡ⁻¹ , (id +₁ !) ∘ i₂ ] ≈˘⟨ []-cong₂ refl (pullʳ distributeˡ⁻¹-i₂) ⟩ + [ (id +₁ !) ∘ distributeˡ⁻¹ , ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₂) ] ≈˘⟨ []-cong₂ (cancelʳ (⁂∘⁂ ○ ⁂-cong₂ identity² inject₁ ○ ⟨⟩-unique id-comm id-comm)) (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² inject₂)) ⟩ + [ (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ [ id , i₂ ])) ∘ (id ⁂ i₁) , (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ [ id , i₂ ])) ∘ (id ⁂ i₂) ] ≈˘⟨ ∘[] ⟩ + (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ [ id , i₂ ])) ∘ distributeˡ ∎) ⟩ + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ [ id , i₂ ]) ∎ + maybeStrong .strength .strength-assoc = Iso⇒Epi (IsIso.iso isIsoˡ) _ _ (begin + ((⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ id) ∘ (id +₁ !) ∘ distributeˡ⁻¹) ∘ distributeˡ ≈⟨ pullʳ (cancelʳ (IsIso.isoˡ isIsoˡ)) ⟩ + (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ id) ∘ (id +₁ !) ≈⟨ +₁∘+₁ ○ +₁-cong₂ identityʳ identityˡ ⟩ + ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ! ≈⟨ []-cong₂ (sym lhs) (sym rhs) ⟩ + [ (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (id ⁂ i₁) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (id ⁂ i₁) ⟩) , (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (id ⁂ i₂) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (id ⁂ i₂) ⟩) ] ≈˘⟨ []-cong₂ (pullʳ (pullʳ ⟨⟩∘)) (pullʳ (pullʳ ⟨⟩∘)) ⟩ + [ (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (id ⁂ i₁) , (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (id ⁂ i₂) ] ≈˘⟨ ∘[] ⟩ + (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ ∎) + where + lhs : ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (id ⁂ i₁) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (id ⁂ i₁) ⟩ ≈ i₁ ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ + lhs = begin + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (id ⁂ i₁) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (id ⁂ i₁) ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (pullʳ (project₁ ○ identityˡ)) (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ (project₁ ○ identityˡ)) project₂) ⟩ + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , i₁ ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩ + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₂ ∘ π₁ , i₁ ∘ π₂ ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl))) ⟩ + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₁) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (pullˡ (pullʳ distributeˡ⁻¹-i₁))) ⟩ + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ((id +₁ !) ∘ i₁) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl ((inject₁ ○ identityʳ) ⟩∘⟨refl)) ⟩ + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , i₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩ + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₁) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ pullˡ (pullʳ distributeˡ⁻¹-i₁) ⟩ + ((id +₁ !) ∘ i₁) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ (inject₁ ○ identityʳ) ⟩∘⟨refl ⟩ + i₁ ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎ + rhs : (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (id ⁂ i₂) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (id ⁂ i₂) ⟩) ≈ i₂ ∘ ! + rhs = begin + (((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (id ⁂ i₂) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (id ⁂ i₂) ⟩) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ (pullʳ (project₁ ○ identityˡ)) (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ (project₁ ○ identityˡ)) project₂) ⟩ + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ (id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , i₂ ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩ + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₂ ∘ π₁ , i₂ ∘ π₂ ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl))) ⟩ + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₂) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (pullˡ (pullʳ distributeˡ⁻¹-i₂))) ⟩ + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ((id +₁ !) ∘ i₂) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (inject₂ ⟩∘⟨refl)) ⟩ + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , (i₂ ∘ !) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (pullʳ (sym (!-unique (! ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩))))) ⟩ + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , i₂ ∘ ! ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ refl) ⟩ + ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₂) ∘ ⟨ π₁ ∘ π₁ , ! ⟩ ≈⟨ pullˡ (pullʳ distributeˡ⁻¹-i₂) ⟩ + ((id +₁ !) ∘ i₂) ∘ ⟨ π₁ ∘ π₁ , ! ⟩ ≈⟨ inject₂ ⟩∘⟨refl ⟩ + (i₂ ∘ !) ∘ ⟨ π₁ ∘ π₁ , ! ⟩ ≈⟨ pullʳ (sym (!-unique (! ∘ ⟨ π₁ ∘ π₁ , ! ⟩))) ⟩ + i₂ ∘ ! ∎ +``` \ No newline at end of file