From 348b119c651cc92319443778aefc2774beeeeb09 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Wed, 17 Jul 2024 12:58:07 +0200 Subject: [PATCH] (P)NNO: replace locally defined functors with corresponding coproduct functors, better module parameters, improve readability of proof --- .../Object/NaturalNumbers/Parametrized.agda | 7 +- .../Parametrized/Properties/F-Algebras.agda | 117 +++++++ .../NaturalNumbers/Properties/F-Algebras.agda | 288 +++++------------- .../Properties/Parametrized.agda | 122 ++++---- 4 files changed, 264 insertions(+), 270 deletions(-) create mode 100644 src/Categories/Object/NaturalNumbers/Parametrized/Properties/F-Algebras.agda diff --git a/src/Categories/Object/NaturalNumbers/Parametrized.agda b/src/Categories/Object/NaturalNumbers/Parametrized.agda index a93b42765..c212fe7be 100644 --- a/src/Categories/Object/NaturalNumbers/Parametrized.agda +++ b/src/Categories/Object/NaturalNumbers/Parametrized.agda @@ -2,15 +2,16 @@ open import Categories.Category.Core open import Categories.Object.Terminal using (Terminal) -open import Categories.Category.Cartesian.Bundle using (CartesianCategory) +open import Categories.Category.Cartesian using (Cartesian) open import Categories.Category.BinaryProducts using (BinaryProducts) -- Parametrized natural numbers object as described here https://ncatlab.org/nlab/show/natural+numbers+object#withparams -module Categories.Object.NaturalNumbers.Parametrized {o ℓ e} (CC : CartesianCategory o ℓ e) where +module Categories.Object.NaturalNumbers.Parametrized {o ℓ e} (𝒞 : Category o ℓ e) (𝒞-Cartesian : Cartesian 𝒞) where open import Level -open CartesianCategory CC renaming (U to 𝒞) +open Category 𝒞 +open Cartesian 𝒞-Cartesian open HomReasoning open Equiv diff --git a/src/Categories/Object/NaturalNumbers/Parametrized/Properties/F-Algebras.agda b/src/Categories/Object/NaturalNumbers/Parametrized/Properties/F-Algebras.agda new file mode 100644 index 000000000..08e0415d5 --- /dev/null +++ b/src/Categories/Object/NaturalNumbers/Parametrized/Properties/F-Algebras.agda @@ -0,0 +1,117 @@ +open import Level +open import Categories.Category.Core +open import Categories.Object.Terminal using (Terminal) +open import Categories.Category.Cocartesian using (BinaryCoproducts) +open import Categories.Category.Cartesian using (Cartesian) + +-- A parametrized NNO corresponds to existence of a (⊤ + (-)) algebra and initiality of the PNNO algebra +module Categories.Object.NaturalNumbers.Parametrized.Properties.F-Algebras {o ℓ e} (𝒞 : Category o ℓ e) (𝒞-Cartesian : Cartesian 𝒞) (𝒞-Coproducts : BinaryCoproducts 𝒞) where + +open import Function using (_$_) + +open import Categories.Category.Construction.F-Algebras using (F-Algebras) +open import Categories.Functor.Algebra using (F-Algebra; F-Algebra-Morphism) +open import Categories.Object.Initial using (Initial; IsInitial) +open import Categories.Category.BinaryProducts using (BinaryProducts) + +import Categories.Morphism.Reasoning as MR + +open Category 𝒞 +open BinaryCoproducts 𝒞-Coproducts +open Cartesian 𝒞-Cartesian +open HomReasoning +open Equiv +open MR 𝒞 +open BinaryProducts products +open Terminal terminal + +open import Categories.Object.NaturalNumbers.Parametrized 𝒞 𝒞-Cartesian +open import Categories.Object.NaturalNumbers.Properties.F-Algebras 𝒞 terminal 𝒞-Coproducts + +-- the algebra that corresponds to a PNNO (if it is initial) +PNNO-Algebra : ∀ A N → ⊤ ⇒ N → N ⇒ N → F-Algebra (A +-) +PNNO-Algebra A N z s = record + { A = A × N + ; α = [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] + } + +Initial⇒PNNO : (algebra : F-Algebra (⊤ +-)) + → (∀ A → IsInitial (F-Algebras (A +-)) + (PNNO-Algebra A (F-Algebra.A algebra) (F-Algebra.α algebra ∘ i₁) (F-Algebra.α algebra ∘ i₂))) + → ParametrizedNNO +Initial⇒PNNO algebra isInitial = record + { N = N + ; isParametrizedNNO = record + { z = z + ; s = s + ; universal = λ {A} {X} f g → F-Algebra-Morphism.f (isInitial.! A {A = alg′ f g}) + ; commute₁ = λ {A} {X} {f} {g} → begin + f ≈˘⟨ inject₁ ⟩ + [ f , g ] ∘ i₁ ≈˘⟨ refl⟩∘⟨ (+₁∘i₁ ○ identityʳ) ⟩ + [ f , g ] ∘ (id +₁ F-Algebra-Morphism.f (isInitial.! A)) ∘ i₁ ≈˘⟨ extendʳ (F-Algebra-Morphism.commutes (isInitial.! A {A = alg′ f g})) ⟩ + F-Algebra-Morphism.f (isInitial.! A) ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩ + (F-Algebra-Morphism.f (IsInitial.! (isInitial A))) ∘ ⟨ id , z ∘ ! ⟩ ∎ + ; commute₂ = λ {A} {X} {f} {g} → begin + g ∘ F-Algebra-Morphism.f (IsInitial.! (isInitial A)) ≈˘⟨ pullˡ inject₂ ⟩ + [ f , g ] ∘ i₂ ∘ F-Algebra-Morphism.f (IsInitial.! (isInitial A)) ≈˘⟨ refl⟩∘⟨ +₁∘i₂ ⟩ + [ f , g ] ∘ (id +₁ F-Algebra-Morphism.f (IsInitial.! (isInitial A))) ∘ i₂ ≈˘⟨ extendʳ (F-Algebra-Morphism.commutes (isInitial.! A {A = alg′ f g})) ⟩ + F-Algebra-Morphism.f (isInitial.! A) ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] ∘ i₂ ≈⟨ refl⟩∘⟨ inject₂ ⟩ + F-Algebra-Morphism.f (IsInitial.! (isInitial A)) ∘ (id ⁂ s) ∎ + ; unique = λ {A} {X} {f} {g} {u} eqᶻ eqˢ → ⟺ $ isInitial.!-unique A {A = alg′ f g} (record + { f = u + ; commutes = begin + u ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] ≈˘⟨ +-g-η ⟩ + [ ((u ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ]) ∘ i₁) + , ((u ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ]) ∘ i₂) ] ≈⟨ []-cong₂ (pullʳ inject₁) (pullʳ inject₂) ⟩ + [ u ∘ ⟨ id , z ∘ ! ⟩ , u ∘ (id ⁂ s) ] ≈˘⟨ []-cong₂ eqᶻ eqˢ ⟩ + [ f , g ∘ u ] ≈˘⟨ []∘+₁ ○ []-cong₂ identityʳ refl ⟩ + [ f , g ] ∘ (id +₁ u) ∎ + }) + } + } + where + open F-Algebra algebra using (α) renaming (A to N) + z = α ∘ i₁ + s = α ∘ i₂ + + module isInitial A = IsInitial (isInitial A) + + alg′ : ∀ {A X} → (f : A ⇒ X) → (g : X ⇒ X) → F-Algebra (A +-) + alg′ {A} {X} f g = record + { A = X + ; α = [ f , g ] + } + +PNNO⇒Initial₁ : ParametrizedNNO → Initial (F-Algebras (⊤ +-)) +PNNO⇒Initial₁ pnno = NNO⇒Initial (PNNO⇒NNO pnno) + +PNNO⇒Initial₂ : (pnno : ParametrizedNNO) + → (∀ A → IsInitial (F-Algebras (A +-)) + (PNNO-Algebra A (ParametrizedNNO.N pnno) (ParametrizedNNO.z pnno) (ParametrizedNNO.s pnno))) +PNNO⇒Initial₂ pnno A = record + { ! = λ {alg} → record + { f = universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂) + ; commutes = begin + universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂) ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] ≈⟨ ∘[] ⟩ + [ universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂) ∘ ⟨ id , z ∘ ! ⟩ + , universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂) ∘ (id ⁂ s) ] ≈˘⟨ []-cong₂ pnno.commute₁ pnno.commute₂ ⟩ + [ F-Algebra.α alg ∘ i₁ + , ((F-Algebra.α alg ∘ i₂) ∘ universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂)) ] ≈˘⟨ ∘[] ○ []-cong₂ (∘-resp-≈ʳ identityʳ) sym-assoc ⟩ + F-Algebra.α alg ∘ (id +₁ universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂)) ∎ + } + ; !-unique = λ {X} f → + let commute₁ = begin + F-Algebra.α X ∘ i₁ ≈˘⟨ refl⟩∘⟨ (+₁∘i₁ ○ identityʳ) ⟩ + F-Algebra.α X ∘ (id +₁ F-Algebra-Morphism.f f) ∘ i₁ ≈˘⟨ extendʳ (F-Algebra-Morphism.commutes f) ⟩ + F-Algebra-Morphism.f f ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩ + F-Algebra-Morphism.f f ∘ ⟨ id , z ∘ ! ⟩ ∎ + commute₂ = begin + (F-Algebra.α X ∘ i₂) ∘ F-Algebra-Morphism.f f ≈⟨ pullʳ $ ⟺ +₁∘i₂ ⟩ + F-Algebra.α X ∘ (id +₁ F-Algebra-Morphism.f f) ∘ i₂ ≈˘⟨ extendʳ (F-Algebra-Morphism.commutes f) ⟩ + F-Algebra-Morphism.f f ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] ∘ i₂ ≈⟨ refl⟩∘⟨ inject₂ ⟩ + F-Algebra-Morphism.f f ∘ (id ⁂ s) ∎ + in ⟺ $ pnno.unique commute₁ commute₂ + } + where + open ParametrizedNNO pnno using (s ; z ; universal) + module pnno = ParametrizedNNO pnno \ No newline at end of file diff --git a/src/Categories/Object/NaturalNumbers/Properties/F-Algebras.agda b/src/Categories/Object/NaturalNumbers/Properties/F-Algebras.agda index ca4896fd8..81f599ede 100644 --- a/src/Categories/Object/NaturalNumbers/Properties/F-Algebras.agda +++ b/src/Categories/Object/NaturalNumbers/Properties/F-Algebras.agda @@ -1,227 +1,97 @@ {-# OPTIONS --without-K --safe #-} -module Categories.Object.NaturalNumbers.Properties.F-Algebras where open import Level -open import Function using (_$_) - open import Categories.Category.Core -open import Categories.Category.Construction.F-Algebras using (F-Algebras) -open import Categories.Category.Cocartesian using (BinaryCoproducts) -open import Categories.Category.Cartesian.Bundle using (CartesianCategory) -open import Categories.Category.BinaryProducts using (BinaryProducts) -open import Categories.Functor using (Endofunctor; Functor) -open import Categories.Functor.Algebra using (F-Algebra; F-Algebra-Morphism) open import Categories.Object.Terminal using (Terminal) -open import Categories.Object.Initial using (Initial; IsInitial) - -import Categories.Morphism.Reasoning as MR -import Categories.Object.NaturalNumbers as NNOs -import Categories.Object.NaturalNumbers.Parametrized as PNNO +open import Categories.Category.Cocartesian using (BinaryCoproducts) -- A NNO is an inital algebra for the 'X ↦ ⊤ + X' endofunctor. -module _ {o ℓ e} (𝒞 : Category o ℓ e) (𝒞-Terminal : Terminal 𝒞) (𝒞-Coproducts : BinaryCoproducts 𝒞) where +module Categories.Object.NaturalNumbers.Properties.F-Algebras {o ℓ e} (𝒞 : Category o ℓ e) (𝒞-Terminal : Terminal 𝒞) (𝒞-Coproducts : BinaryCoproducts 𝒞) where - open Terminal 𝒞-Terminal - open BinaryCoproducts 𝒞-Coproducts - open Category 𝒞 - open HomReasoning - open Equiv - open MR 𝒞 - open NNOs 𝒞 𝒞-Terminal +open import Function using (_$_) - Maybe : Functor 𝒞 𝒞 - Maybe = record - { F₀ = λ X → ⊤ + X - ; F₁ = λ f → [ i₁ , i₂ ∘ f ] - ; identity = []-cong₂ refl identityʳ ○ +-η - ; homomorphism = +-unique (pullʳ inject₁ ○ inject₁) (pullʳ inject₂ ○ pullˡ inject₂ ○ assoc) - ; F-resp-≈ = λ eq → []-cong₂ refl (∘-resp-≈ʳ eq) - } +open import Categories.Category.Construction.F-Algebras using (F-Algebras) +open import Categories.Functor.Algebra using (F-Algebra; F-Algebra-Morphism) +open import Categories.Object.Initial using (Initial; IsInitial) - private - module Maybe = Functor Maybe +import Categories.Morphism.Reasoning as MR - Initial⇒NNO : Initial (F-Algebras Maybe) → NNO - Initial⇒NNO initial = record - { N = ⊥.A - ; isNNO = record - { z = ⊥.α ∘ i₁ - ; s = ⊥.α ∘ i₂ - ; universal = λ {A} q f → - F-Algebra-Morphism.f (initial.! {A = alg q f}) - ; z-commute = λ {A} {q} {f} → begin - q ≈⟨ ⟺ inject₁ ⟩ - [ q , f ] ∘ i₁ ≈⟨ pushʳ (⟺ inject₁) ⟩ - (([ q , f ] ∘ [ i₁ , i₂ ∘ F-Algebra-Morphism.f initial.! ]) ∘ i₁) ≈⟨ pushˡ (⟺ (F-Algebra-Morphism.commutes (initial.! {A = alg q f}))) ⟩ - F-Algebra-Morphism.f initial.! ∘ ⊥.α ∘ i₁ ∎ - ; s-commute = λ {A} {q} {f} → begin - (f ∘ F-Algebra-Morphism.f initial.!) ≈⟨ pushˡ (⟺ inject₂) ⟩ - [ q , f ] ∘ i₂ ∘ F-Algebra-Morphism.f initial.! ≈⟨ pushʳ (⟺ inject₂) ⟩ - ([ q , f ] ∘ [ i₁ , i₂ ∘ F-Algebra-Morphism.f initial.! ]) ∘ i₂ ≈⟨ pushˡ (⟺ (F-Algebra-Morphism.commutes (initial.! {A = alg q f}))) ⟩ - F-Algebra-Morphism.f initial.! ∘ ⊥.α ∘ i₂ ∎ - ; unique = λ {A} {f} {q} {u} eqᶻ eqˢ → ⟺ $ initial.!-unique record - { f = u - ; commutes = begin - u ∘ ⊥.α ≈⟨ ⟺ +-g-η ⟩ - [ (u ∘ ⊥.α) ∘ i₁ , (u ∘ ⊥.α) ∘ i₂ ] ≈⟨ []-cong₂ (assoc ○ ⟺ eqᶻ) (assoc ○ ⟺ eqˢ) ⟩ - [ f , q ∘ u ] ≈⟨ +-unique (pullʳ inject₁ ○ inject₁) (pullʳ inject₂ ○ pullˡ inject₂) ⟩ - [ f , q ] ∘ [ i₁ , i₂ ∘ u ] ∎ - } +open Terminal 𝒞-Terminal +open BinaryCoproducts 𝒞-Coproducts +open Category 𝒞 +open HomReasoning +open Equiv +open MR 𝒞 + +open import Categories.Object.NaturalNumbers 𝒞 𝒞-Terminal + +Initial⇒NNO : Initial (F-Algebras (⊤ +-)) → NNO +Initial⇒NNO initial = record + { N = ⊥.A + ; isNNO = record + { z = ⊥.α ∘ i₁ + ; s = ⊥.α ∘ i₂ + ; universal = λ {A} q f → + F-Algebra-Morphism.f (initial.! {A = alg q f}) + ; z-commute = λ {A} {q} {f} → begin + q ≈˘⟨ inject₁ ⟩ + [ q , f ] ∘ i₁ ≈˘⟨ refl⟩∘⟨ (+₁∘i₁ ○ identityʳ) ⟩ + [ q , f ] ∘ (id +₁ F-Algebra-Morphism.f initial.!) ∘ i₁ ≈˘⟨ extendʳ (F-Algebra-Morphism.commutes (initial.! {A = alg q f})) ⟩ + F-Algebra-Morphism.f initial.! ∘ ⊥.α ∘ i₁ ∎ + ; s-commute = λ {A} {q} {f} → begin + f ∘ F-Algebra-Morphism.f initial.! ≈˘⟨ pullˡ inject₂ ⟩ + [ q , f ] ∘ i₂ ∘ F-Algebra-Morphism.f initial.! ≈˘⟨ refl⟩∘⟨ +₁∘i₂ ⟩ + [ q , f ] ∘ (id +₁ F-Algebra-Morphism.f initial.!) ∘ i₂ ≈˘⟨ extendʳ $ F-Algebra-Morphism.commutes (initial.! {A = alg q f}) ⟩ + F-Algebra-Morphism.f initial.! ∘ ⊥.α ∘ i₂ ∎ + ; unique = λ {A} {f} {q} {u} eqᶻ eqˢ → ⟺ $ initial.!-unique $ record + { f = u + ; commutes = begin + u ∘ ⊥.α ≈˘⟨ +-g-η ⟩ + [ (u ∘ ⊥.α) ∘ i₁ , (u ∘ ⊥.α) ∘ i₂ ] ≈˘⟨ []-cong₂ (eqᶻ ○ sym-assoc) (eqˢ ○ sym-assoc) ⟩ + [ f , q ∘ u ] ≈˘⟨ []∘+₁ ○ []-cong₂ identityʳ refl ⟩ + [ f , q ] ∘ (id +₁ u) ∎ } } - where - module initial = Initial initial - module ⊥ = F-Algebra initial.⊥ - - alg : ∀ {A} → (q : ⊤ ⇒ A) → (f : A ⇒ A) → F-Algebra Maybe - alg {A} q f = record - { A = A - ; α = [ q , f ] - } - - NNO⇒Initial : NNO → Initial (F-Algebras Maybe) - NNO⇒Initial nno = record - { ⊥ = record - { A = N - ; α = [ z , s ] + } + where + module initial = Initial initial + module ⊥ = F-Algebra initial.⊥ + + alg : ∀ {A} → (q : ⊤ ⇒ A) → (f : A ⇒ A) → F-Algebra (⊤ +-) + alg {A} q f = record + { A = A + ; α = [ q , f ] } - ; ⊥-is-initial = record - { ! = λ {alg} → record - { f = universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂) - ; commutes = begin - universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂) ∘ [ z , s ] ≈⟨ ∘-distribˡ-[] ⟩ - [ universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂) ∘ z - , universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂) ∘ s ] ≈⟨ []-cong₂ (⟺ z-commute) (⟺ s-commute ○ assoc) ⟩ - [ F-Algebra.α alg ∘ i₁ , F-Algebra.α alg ∘ (i₂ ∘ universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂)) ] ≈˘⟨ ∘-distribˡ-[] ⟩ - F-Algebra.α alg ∘ [ i₁ , i₂ ∘ universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂) ] ∎ - } - ; !-unique = λ {A} f → - let z-commutes = begin - F-Algebra.α A ∘ i₁ ≈⟨ pushʳ (⟺ inject₁) ⟩ - (F-Algebra.α A ∘ [ i₁ , i₂ ∘ F-Algebra-Morphism.f f ]) ∘ i₁ ≈˘⟨ F-Algebra-Morphism.commutes f ⟩∘⟨refl ⟩ - (F-Algebra-Morphism.f f ∘ [ z , s ]) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩ - F-Algebra-Morphism.f f ∘ z ∎ - s-commutes = begin - (F-Algebra.α A ∘ i₂) ∘ F-Algebra-Morphism.f f ≈⟨ pullʳ (⟺ inject₂) ○ ⟺ assoc ⟩ - (F-Algebra.α A ∘ [ i₁ , i₂ ∘ F-Algebra-Morphism.f f ]) ∘ i₂ ≈˘⟨ F-Algebra-Morphism.commutes f ⟩∘⟨refl ⟩ - (F-Algebra-Morphism.f f ∘ [ z , s ]) ∘ i₂ ≈⟨ pullʳ inject₂ ⟩ - F-Algebra-Morphism.f f ∘ s ∎ - in ⟺ $ unique z-commutes s-commutes - } - } - where - open NNO nno - --- A parametrized NNO corresponds to existence of a Maybe algebra and initiality of the PNNO algebra -module _ {o ℓ e} (CC : CartesianCategory o ℓ e) (𝒞-Coproducts : BinaryCoproducts (CartesianCategory.U CC)) where - open CartesianCategory CC renaming (U to 𝒞) - open BinaryCoproducts 𝒞-Coproducts - open BinaryProducts products hiding (unique) - open HomReasoning - open Equiv - open MR 𝒞 - open PNNO CC - open NNOs 𝒞 terminal - open Terminal terminal - - coproductF : Obj → Endofunctor 𝒞 - coproductF A = record - { F₀ = λ X → A + X - ; F₁ = λ f → [ i₁ , (i₂ ∘ f) ] - ; identity = λ {A} → trans ([]-congˡ identityʳ) - (coproduct.unique identityˡ identityˡ) - ; homomorphism = λ {X} {Y} {Z} {f} {g} → coproduct.unique - (trans (pullʳ inject₁) (inject₁)) - (trans (pullʳ inject₂) (trans (pullˡ inject₂) assoc)) - ; F-resp-≈ = λ fg → []-congˡ (∘-resp-≈ʳ fg) - } - - private - module coproductF A = Functor (coproductF A) - -- the algebra that corresponds to a PNNO (if it is initial) - PNNO-Algebra : ∀ A N → ⊤ ⇒ N → N ⇒ N → F-Algebra (coproductF A) - PNNO-Algebra A N z s = record - { A = A × N - ; α = [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] +NNO⇒Initial : NNO → Initial (F-Algebras (⊤ +-)) +NNO⇒Initial nno = record + { ⊥ = record + { A = N + ; α = [ z , s ] } - - Initial⇒PNNO : (algebra : F-Algebra (Maybe 𝒞 terminal 𝒞-Coproducts)) - → (∀ A → IsInitial (F-Algebras (coproductF A)) - (PNNO-Algebra A (F-Algebra.A algebra) (F-Algebra.α algebra ∘ i₁) (F-Algebra.α algebra ∘ i₂))) - → ParametrizedNNO - Initial⇒PNNO algebra isInitial = record - { N = N - ; isParametrizedNNO = record - { z = z - ; s = s - ; universal = λ {A} {X} f g → F-Algebra-Morphism.f (isInitial.! A {A = alg′ f g}) - ; commute₁ = λ {A} {X} {f} {g} → begin - f ≈˘⟨ inject₁ ⟩ - [ f , g ] ∘ i₁ ≈⟨ pushʳ (⟺ inject₁) ⟩ - (([ f , g ] ∘ [ i₁ , i₂ ∘ F-Algebra-Morphism.f (isInitial.! A) ]) ∘ i₁) ≈⟨ pushˡ (⟺ (F-Algebra-Morphism.commutes (isInitial.! A {A = alg′ f g}))) ⟩ - (F-Algebra-Morphism.f (isInitial.! A) ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] ∘ i₁) ≈⟨ refl⟩∘⟨ inject₁ ⟩ - (F-Algebra-Morphism.f (IsInitial.! (isInitial A))) ∘ ⟨ id , z ∘ ! ⟩ ∎ - ; commute₂ = λ {A} {X} {f} {g} → begin - g ∘ F-Algebra-Morphism.f (IsInitial.! (isInitial A)) ≈⟨ pushˡ (⟺ inject₂) ⟩ - [ f , g ] ∘ i₂ ∘ F-Algebra-Morphism.f (IsInitial.! (isInitial A)) ≈⟨ pushʳ (⟺ inject₂) ⟩ - (([ f , g ] ∘ [ i₁ , i₂ ∘ F-Algebra-Morphism.f (IsInitial.! (isInitial A)) ]) ∘ i₂) ≈⟨ pushˡ (⟺ (F-Algebra-Morphism.commutes (isInitial.! A {A = alg′ f g}))) ⟩ - (F-Algebra-Morphism.f (isInitial.! A) ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] ∘ i₂) ≈⟨ (refl⟩∘⟨ inject₂) ⟩ - F-Algebra-Morphism.f (IsInitial.! (isInitial A)) ∘ (id ⁂ s) ∎ - ; unique = λ {A} {X} {f} {g} {u} eqᶻ eqˢ → ⟺ $ isInitial.!-unique A {A = alg′ f g} (record - { f = u - ; commutes = begin - u ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] ≈⟨ ⟺ +-g-η ⟩ - [ ((u ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ]) ∘ i₁) - , ((u ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ]) ∘ i₂) ] ≈⟨ []-cong₂ (pullʳ inject₁) (pullʳ inject₂) ⟩ - [ u ∘ ⟨ id , z ∘ ! ⟩ , u ∘ (id ⁂ s) ] ≈˘⟨ []-cong₂ eqᶻ eqˢ ⟩ - [ f , g ∘ u ] ≈⟨ +-unique (pullʳ inject₁ ○ inject₁) (pullʳ inject₂ ○ pullˡ inject₂) ⟩ - [ f , g ] ∘ [ i₁ , i₂ ∘ u ] ∎ - }) - } - } - where - open F-Algebra algebra using (α) renaming (A to N) - z = α ∘ i₁ - s = α ∘ i₂ - - module isInitial A = IsInitial (isInitial A) - - alg′ : ∀ {A X} → (f : A ⇒ X) → (g : X ⇒ X) → F-Algebra (coproductF A) - alg′ {A} {X} f g = record - { A = X - ; α = [ f , g ] - } - - PNNO⇒Initial₁ : ParametrizedNNO → Initial (F-Algebras (Maybe 𝒞 terminal 𝒞-Coproducts)) - PNNO⇒Initial₁ pnno = (NNO⇒Initial 𝒞 terminal 𝒞-Coproducts) (PNNO⇒NNO pnno) - - PNNO⇒Initial₂ : (pnno : ParametrizedNNO) - → (∀ A → IsInitial (F-Algebras (coproductF A)) - (PNNO-Algebra A (ParametrizedNNO.N pnno) (ParametrizedNNO.z pnno) (ParametrizedNNO.s pnno))) - PNNO⇒Initial₂ pnno A = record - { ! = λ {alg} → record - { f = universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂) + ; ⊥-is-initial = record + { ! = λ {alg} → record + { f = universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂) ; commutes = begin - universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂) ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ] ≈⟨ ∘-distribˡ-[] ⟩ - [ universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂) ∘ ⟨ id , z ∘ ! ⟩ - , universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂) ∘ (id ⁂ s) ] ≈⟨ []-cong₂ (⟺ commute₁) (⟺ commute₂) ⟩ - [ F-Algebra.α alg ∘ i₁ - , ((F-Algebra.α alg ∘ i₂) ∘ universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂)) ] ≈˘⟨ trans ∘-distribˡ-[] ([]-congˡ sym-assoc) ⟩ - F-Algebra.α alg ∘ [ i₁ , i₂ ∘ universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂) ] ∎ - } - ; !-unique = λ {X} f → - let commute₁ = begin - F-Algebra.α X ∘ i₁ ≈⟨ pushʳ (⟺ inject₁) ⟩ - ((F-Algebra.α X ∘ [ i₁ , i₂ ∘ F-Algebra-Morphism.f f ]) ∘ i₁) ≈˘⟨ F-Algebra-Morphism.commutes f ⟩∘⟨refl ⟩ - ((F-Algebra-Morphism.f f ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ]) ∘ i₁) ≈⟨ pullʳ inject₁ ⟩ - F-Algebra-Morphism.f f ∘ ⟨ id , z ∘ ! ⟩ ∎ - commute₂ = begin - (F-Algebra.α X ∘ i₂) ∘ F-Algebra-Morphism.f f ≈⟨ (pullʳ (⟺ inject₂) ○ ⟺ assoc) ⟩ - ((F-Algebra.α X ∘ [ i₁ , i₂ ∘ F-Algebra-Morphism.f f ]) ∘ i₂) ≈˘⟨ F-Algebra-Morphism.commutes f ⟩∘⟨refl ⟩ - ((F-Algebra-Morphism.f f ∘ [ ⟨ id , z ∘ ! ⟩ , id ⁂ s ]) ∘ i₂) ≈⟨ pullʳ inject₂ ⟩ - F-Algebra-Morphism.f f ∘ (id ⁂ s) ∎ - in ⟺ $ unique commute₁ commute₂ + universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂) ∘ [ z , s ] ≈⟨ ∘[] ⟩ + [ universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂) ∘ z + , universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂) ∘ s ] ≈˘⟨ []-cong₂ z-commute (sym-assoc ○ s-commute) ⟩ + [ F-Algebra.α alg ∘ i₁ , F-Algebra.α alg ∘ (i₂ ∘ universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂)) ] ≈˘⟨ ∘[] ○ []-cong₂ (∘-resp-≈ʳ identityʳ) refl ⟩ + F-Algebra.α alg ∘ (id +₁ universal (F-Algebra.α alg ∘ i₁) (F-Algebra.α alg ∘ i₂)) ∎ + } + ; !-unique = λ {A} f → + let z-commutes = begin + F-Algebra.α A ∘ i₁ ≈˘⟨ refl⟩∘⟨ (+₁∘i₁ ○ identityʳ) ⟩ + F-Algebra.α A ∘ (id +₁ F-Algebra-Morphism.f f) ∘ i₁ ≈˘⟨ extendʳ (F-Algebra-Morphism.commutes f) ⟩ + F-Algebra-Morphism.f f ∘ [ z , s ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩ + F-Algebra-Morphism.f f ∘ z ∎ + s-commutes = begin + (F-Algebra.α A ∘ i₂) ∘ F-Algebra-Morphism.f f ≈⟨ pullʳ $ ⟺ inject₂ ⟩ + F-Algebra.α A ∘ (id +₁ F-Algebra-Morphism.f f) ∘ i₂ ≈˘⟨ pushˡ (F-Algebra-Morphism.commutes f) ⟩ + (F-Algebra-Morphism.f f ∘ [ z , s ]) ∘ i₂ ≈⟨ pullʳ inject₂ ⟩ + F-Algebra-Morphism.f f ∘ s ∎ + in ⟺ $ unique z-commutes s-commutes } - where - open ParametrizedNNO pnno \ No newline at end of file + } + where + open NNO nno diff --git a/src/Categories/Object/NaturalNumbers/Properties/Parametrized.agda b/src/Categories/Object/NaturalNumbers/Properties/Parametrized.agda index 639ad1db3..d85401bed 100644 --- a/src/Categories/Object/NaturalNumbers/Properties/Parametrized.agda +++ b/src/Categories/Object/NaturalNumbers/Properties/Parametrized.agda @@ -1,34 +1,31 @@ {-# OPTIONS --without-K --safe #-} +open import Level open import Categories.Category.Core open import Categories.Object.Terminal using (Terminal) -open import Categories.Category.CartesianClosed.Bundle using (CartesianClosedCategory) open import Categories.Category.Cartesian using (Cartesian) open import Categories.Category.BinaryProducts using (BinaryProducts) open import Categories.Category.Cocartesian using (BinaryCoproducts) open import Categories.Category.CartesianClosed using (CartesianClosed) --- In CCCs NNOs and PNNOs coincide - -module Categories.Object.NaturalNumbers.Properties.Parametrized {o ℓ e} (CCC : CartesianClosedCategory o ℓ e) (𝒞-Coproducts : BinaryCoproducts (CartesianClosedCategory.U CCC)) where +-- In CCCs every NNO is a PNNO -open import Level +module Categories.Object.NaturalNumbers.Properties.Parametrized {o ℓ e} (𝒞 : Category o ℓ e) (𝒞-CartesianClosed : CartesianClosed 𝒞) (𝒞-Coproducts : BinaryCoproducts 𝒞) where -open CartesianClosedCategory CCC renaming (U to 𝒞) -open CartesianClosed cartesianClosed using (cartesian; λg; eval′; β′; λ-inj; λ-cong; η-exp′; λ-unique′; subst) +open Category 𝒞 +open CartesianClosed 𝒞-CartesianClosed using (cartesian; λg; eval′; β′; λ-inj; λ-cong; η-exp′; λ-unique′; subst) open Cartesian cartesian using (terminal; products) open BinaryProducts products renaming (unique′ to bp-unique′) +open Terminal terminal open import Categories.Object.NaturalNumbers 𝒞 terminal using (NNO) -open import Categories.Object.NaturalNumbers.Parametrized cartesianCategory using (ParametrizedNNO) +open import Categories.Object.NaturalNumbers.Parametrized 𝒞 cartesian using (ParametrizedNNO) open import Categories.Morphism 𝒞 open import Categories.Morphism.Reasoning 𝒞 open HomReasoning open Equiv -open Terminal terminal - NNO×CCC⇒PNNO : NNO → ParametrizedNNO NNO×CCC⇒PNNO nno = record { N = N @@ -42,54 +39,63 @@ NNO×CCC⇒PNNO nno = record } } where - open NNO nno renaming (unique to nno-unique) + open NNO nno renaming (unique to nno-unique) - commute₁' : ∀ {A X} {f : A ⇒ X} {g : X ⇒ X} → f ≈ ((eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap) ∘ ⟨ id , z ∘ ! ⟩ - commute₁' {A} {X} {f} {g} = begin - f ≈⟨ introʳ project₂ ⟩ - f ∘ π₂ ∘ ⟨ ! , id ⟩ ≈⟨ pullˡ (⟺ β′) ⟩ - (eval′ ∘ (λg (f ∘ π₂) ⁂ id)) ∘ ⟨ ! , id ⟩ ≈⟨ pullʳ ⁂∘⟨⟩ ⟩ - eval′ ∘ ⟨ λg (f ∘ π₂) ∘ ! , id ∘ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ (∘-resp-≈ˡ z-commute) ⟩ - eval′ ∘ ⟨ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ∘ z) ∘ ! , id ∘ id ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-congʳ assoc ○ ⟺ ⁂∘⟨⟩) ⟩ - eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id) ∘ ⟨ z ∘ ! , id ⟩ ≈⟨ sym-assoc ○ pushʳ (⟺ swap∘⟨⟩) ⟩ - ((eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap) ∘ ⟨ id , z ∘ ! ⟩ ∎ + commute₁' : ∀ {A X} {f : A ⇒ X} {g : X ⇒ X} → f ≈ ((eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap) ∘ ⟨ id , z ∘ ! ⟩ + commute₁' {A} {X} {f} {g} = begin + f ≈⟨ introʳ project₂ ⟩ + f ∘ π₂ ∘ ⟨ ! , id ⟩ ≈⟨ pullˡ (⟺ β′) ⟩ + (eval′ ∘ (λg (f ∘ π₂) ⁂ id)) ∘ ⟨ ! , id ⟩ ≈⟨ pullʳ ⁂∘⟨⟩ ⟩ + eval′ ∘ ⟨ λg (f ∘ π₂) ∘ ! , id ∘ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congʳ (∘-resp-≈ˡ z-commute) ⟩ + eval′ ∘ ⟨ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ∘ z) ∘ ! , id ∘ id ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-congʳ assoc ○ ⟺ ⁂∘⟨⟩) ⟩ + eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id) ∘ ⟨ z ∘ ! , id ⟩ ≈⟨ sym-assoc ○ pushʳ (⟺ swap∘⟨⟩) ⟩ + ((eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap) ∘ ⟨ id , z ∘ ! ⟩ ∎ - commute₂' : ∀ {A X} {f : A ⇒ X} {g : X ⇒ X} - → g ∘ ((eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap) ≈ ((eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap) ∘ (id ⁂ s) - commute₂' {A} {X} {f} {g} = begin - g ∘ (eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap ≈⟨ pullˡ (pullˡ (⟺ β′)) ⟩ - ((eval′ ∘ (λg (g ∘ eval′) ⁂ id)) ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap ≈⟨ (pullʳ ⁂∘⁂) ⟩∘⟨refl ⟩ - (eval′ ∘ (λg (g ∘ eval′) ∘ universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id ∘ id)) ∘ swap ≈⟨ (refl⟩∘⟨ (⁂-cong₂ s-commute refl)) ⟩∘⟨refl ⟩ - (eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ∘ s ⁂ id ∘ id)) ∘ swap ≈⟨ (refl⟩∘⟨ (⟺ ⁂∘⁂)) ⟩∘⟨refl ⟩ - (eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id) ∘ (s ⁂ id)) ∘ swap ≈⟨ pullʳ (pullʳ (⟺ swap∘⁂)) ⟩ - eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id) ∘ swap ∘ (id ⁂ s) ≈⟨ sym-assoc ○ sym-assoc ⟩ - ((eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap) ∘ (id ⁂ s) ∎ + commute₂' : ∀ {A X} {f : A ⇒ X} {g : X ⇒ X} + → g ∘ ((eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap) ≈ ((eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap) ∘ (id ⁂ s) + commute₂' {A} {X} {f} {g} = begin + g ∘ (eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap ≈⟨ pullˡ (pullˡ (⟺ β′)) ⟩ + ((eval′ ∘ (λg (g ∘ eval′) ⁂ id)) ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap ≈⟨ (pullʳ ⁂∘⁂) ⟩∘⟨refl ⟩ + (eval′ ∘ (λg (g ∘ eval′) ∘ universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id ∘ id)) ∘ swap ≈⟨ (refl⟩∘⟨ (⁂-cong₂ s-commute refl)) ⟩∘⟨refl ⟩ + (eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ∘ s ⁂ id ∘ id)) ∘ swap ≈⟨ (refl⟩∘⟨ (⟺ ⁂∘⁂)) ⟩∘⟨refl ⟩ + (eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id) ∘ (s ⁂ id)) ∘ swap ≈⟨ pullʳ (pullʳ (⟺ swap∘⁂)) ⟩ + eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id) ∘ swap ∘ (id ⁂ s) ≈⟨ sym-assoc ○ sym-assoc ⟩ + ((eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap) ∘ (id ⁂ s) ∎ - unique' : ∀ {A X} {f : A ⇒ X} {g : X ⇒ X} {u : A × N ⇒ X} - → f ≈ u ∘ ⟨ id , z ∘ ! ⟩ → g ∘ u ≈ u ∘ (id ⁂ s) → u ≈ (eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap - unique' {A} {X} {f} {g} {u} eqᶻ eqˢ = swap-epi _ _ (λ-inj (begin - λg (u ∘ swap) ≈⟨ nno-unique - (⟺ (λ-unique′ - (begin - eval′ ∘ (λg (u ∘ swap) ∘ z ⁂ id) ≈⟨ refl⟩∘⟨ ⟺ (⁂∘⁂ ○ ⁂-cong₂ refl identity²) ⟩ - eval′ ∘ (λg (u ∘ swap) ⁂ id) ∘ (z ⁂ id) ≈⟨ pullˡ β′ ⟩ - (u ∘ swap) ∘ (z ⁂ id) ≈⟨ pullʳ swap∘⁂ ⟩ - u ∘ (id ⁂ z) ∘ swap ≈⟨ pushʳ (bp-unique′ - ( pullˡ project₁ - ○ pullʳ project₁ - ○ ⟺ (pullˡ project₁)) - ( pullˡ project₂ - ○ pullʳ project₂ - ○ ⟺ (pullʳ !-unique₂) - ○ ⟺ (pullˡ project₂))) ⟩ - (u ∘ ⟨ id , z ∘ ! ⟩) ∘ π₂ ≈⟨ ⟺ (∘-resp-≈ˡ eqᶻ) ⟩ - f ∘ π₂ ∎))) - (begin - λg (g ∘ eval′) ∘ λg (u ∘ swap) ≈⟨ subst ⟩ - λg ((g ∘ eval′) ∘ (λg (u ∘ swap) ⁂ id)) ≈⟨ λ-cong (pullʳ β′ ○ pullˡ eqˢ) ⟩ - λg ((u ∘ (id ⁂ s)) ∘ swap) ≈⟨ λ-cong (pullʳ (⟺ swap∘⁂) ○ sym-assoc) ⟩ - λg ((u ∘ swap) ∘ (s ⁂ id)) ≈˘⟨ subst ⟩ - λg (u ∘ swap) ∘ s ∎) ⟩ - universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ≈˘⟨ η-exp′ ⟩ - λg (eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ≈˘⟨ λ-cong (cancelʳ swap∘swap) ⟩ - λg (((eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap) ∘ swap) ∎)) + unique' : ∀ {A X} {f : A ⇒ X} {g : X ⇒ X} {u : A × N ⇒ X} + → f ≈ u ∘ ⟨ id , z ∘ ! ⟩ → g ∘ u ≈ u ∘ (id ⁂ s) → u ≈ (eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap + unique' {A} {X} {f} {g} {u} eqᶻ eqˢ = swap-epi _ _ (λ-inj (begin + λg (u ∘ swap) ≈⟨ nno-unique (⟺ z-commutes) s-commutes ⟩ + universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ≈˘⟨ η-exp′ ⟩ + λg (eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ≈˘⟨ λ-cong (cancelʳ swap∘swap) ⟩ + λg (((eval′ ∘ (universal (λg (f ∘ π₂)) (λg (g ∘ eval′)) ⁂ id)) ∘ swap) ∘ swap) ∎)) + where + z-commutes : λg (u ∘ swap) ∘ z ≈ λg (f ∘ π₂) + z-commutes = λ-unique′ (begin + eval′ ∘ (λg (u ∘ swap) ∘ z ⁂ id) ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²) ⟩ + eval′ ∘ (λg (u ∘ swap) ⁂ id) ∘ (z ⁂ id) ≈⟨ extendʳ β′ ⟩ + u ∘ swap ∘ (z ⁂ id) ≈⟨ refl⟩∘⟨ swap∘⁂ ⟩ + u ∘ (id ⁂ z) ∘ swap ≈⟨ refl⟩∘⟨ (bp-unique′ π₁-commutes π₂-commutes) ⟩ + u ∘ ⟨ id , z ∘ ! ⟩ ∘ π₂ ≈⟨ pullˡ (⟺ eqᶻ) ⟩ + f ∘ π₂ ∎) + where + π₁-commutes : π₁ ∘ (id ⁂ z) ∘ swap ≈ π₁ ∘ ⟨ id , z ∘ ! ⟩ ∘ π₂ + π₁-commutes = begin + π₁ ∘ (id ⁂ z) ∘ swap ≈⟨ extendʳ project₁ ○ identityˡ ⟩ + π₁ ∘ swap ≈⟨ project₁ ⟩ + π₂ ≈˘⟨ cancelˡ project₁ ⟩ + π₁ ∘ ⟨ id , z ∘ ! ⟩ ∘ π₂ ∎ + π₂-commutes : π₂ ∘ (id ⁂ z) ∘ swap ≈ π₂ ∘ ⟨ id , z ∘ ! ⟩ ∘ π₂ + π₂-commutes = begin + π₂ ∘ (id ⁂ z) ∘ swap ≈⟨ extendʳ project₂ ⟩ + z ∘ π₂ ∘ swap ≈⟨ refl⟩∘⟨ project₂ ⟩ + z ∘ π₁ ≈⟨ refl⟩∘⟨ !-unique₂ ⟩ + z ∘ ! ∘ π₂ ≈˘⟨ extendʳ project₂ ⟩ + π₂ ∘ ⟨ id , z ∘ ! ⟩ ∘ π₂ ∎ + s-commutes : λg (g ∘ eval′) ∘ λg (u ∘ swap) ≈ λg (u ∘ swap) ∘ s + s-commutes = begin + λg (g ∘ eval′) ∘ λg (u ∘ swap) ≈⟨ subst ⟩ + λg ((g ∘ eval′) ∘ (λg (u ∘ swap) ⁂ id)) ≈⟨ λ-cong (pullʳ β′ ○ pullˡ eqˢ) ⟩ + λg ((u ∘ (id ⁂ s)) ∘ swap) ≈⟨ λ-cong (pullʳ (⟺ swap∘⁂) ○ sym-assoc) ⟩ + λg ((u ∘ swap) ∘ (s ⁂ id)) ≈˘⟨ subst ⟩ + λg (u ∘ swap) ∘ s ∎