From 1a84efec2ba0769035144782e1e96a10e0d5a7b2 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sun, 4 Jan 2026 10:59:04 -0600 Subject: Update to latest agda-categories --- .../Cartesian/Instance/FinitelyCocompletes.agda | 51 +++++++++++++++++++--- Category/Instance/Properties/SymMonCat.agda | 1 - Category/Instance/SymMonCat.agda | 2 +- Category/Monoidal/Instance/DecoratedCospans.agda | 30 ++++++------- .../Instance/DecoratedCospans/Products.agda | 2 +- .../SymmetricMonoidal/FinitelyCocomplete.agda | 2 +- Functor/Monoidal/Strong/Properties.agda | 9 ---- 7 files changed, 64 insertions(+), 33 deletions(-) diff --git a/Category/Cartesian/Instance/FinitelyCocompletes.agda b/Category/Cartesian/Instance/FinitelyCocompletes.agda index 5425233..8c779d5 100644 --- a/Category/Cartesian/Instance/FinitelyCocompletes.agda +++ b/Category/Cartesian/Instance/FinitelyCocompletes.agda @@ -16,8 +16,8 @@ open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; ni open import Categories.NaturalTransformation.NaturalIsomorphism.Properties using (pointwise-iso) open import Categories.Object.Coproduct using (IsCoproduct; IsCoproduct⇒Coproduct; Coproduct) open import Categories.Object.Initial using (IsInitial) -open import Data.Product.Base using (_,_) renaming (_×_ to _×′_) - +open import Data.Product using (_,_; swap) renaming (_×_ to _×′_) +open import Function using () renaming (_∘_ to _∘′_) open import Category.Cocomplete.Finitely.Bundle using (FinitelyCocompleteCategory) open import Category.Instance.FinitelyCocompletes {o} {ℓ} {e} using (FinitelyCocompletes; FinitelyCocompletes-Cartesian; _×₁_) open import Functor.Exact using (IsRightExact; RightExactFunctor) @@ -44,13 +44,48 @@ module _ (𝒞 : FinitelyCocompleteCategory o ℓ e) where private module -+- = Functor -+- + flip-IsInitial + : {(A , B) : 𝒞×𝒞.Obj} + → IsInitial 𝒞×𝒞.U (A , B) + → IsInitial 𝒞×𝒞.U (B , A) + flip-IsInitial isInitial = let open IsInitial isInitial in record + { ! = swap ! + ; !-unique = swap ∘′ !-unique ∘′ swap + } + + flip-IsCoproduct + : {(A₁ , A₂) (B₁ , B₂) (C₁ , C₂) : 𝒞×𝒞.Obj} + {(i₁-₁ , i₁-₂) : (A₁ ⇒ C₁) ×′ (A₂ ⇒ C₂)} + {(i₂-₁ , i₂-₂) : (B₁ ⇒ C₁) ×′ (B₂ ⇒ C₂)} + → IsCoproduct 𝒞×𝒞.U (i₁-₁ , i₁-₂) (i₂-₁ , i₂-₂) + → IsCoproduct 𝒞×𝒞.U (i₁-₂ , i₁-₁) (i₂-₂ , i₂-₁) + flip-IsCoproduct isCoproduct = let module + = IsCoproduct isCoproduct in record + { [_,_] = λ x y → swap (+.[ swap x , swap y ]) + ; inject₁ = swap +.inject₁ + ; inject₂ = swap +.inject₂ + ; unique = λ x y → swap (+.unique (swap x) (swap y)) + } + + flip-IsCoequalizer + : {(A₁ , A₂) (B₁ , B₂) (C₁ , C₂) : 𝒞×𝒞.Obj} + {(f₁ , f₂) (g₁ , g₂) : (A₁ ⇒ B₁) ×′ (A₂ ⇒ B₂)} + {(h₁ , h₂) : (B₁ ⇒ C₁) ×′ (B₂ ⇒ C₂)} + → IsCoequalizer 𝒞×𝒞.U (f₁ , f₂) (g₁ , g₂) (h₁ , h₂) + → IsCoequalizer 𝒞×𝒞.U (f₂ , f₁) (g₂ , g₁) (h₂ , h₁) + flip-IsCoequalizer isCoeq = let open IsCoequalizer isCoeq in record + { equality = swap equality + ; coequalize = swap ∘′ coequalize ∘′ swap + ; universal = swap universal + ; unique = swap ∘′ unique ∘′ swap + } + +-resp-⊥ : {(A , B) : 𝒞×𝒞.Obj} → IsInitial 𝒞×𝒞.U (A , B) → IsInitial 𝒞.U (A + B) +-resp-⊥ {A , B} A,B-isInitial = record { ! = [ A-isInitial.! , B-isInitial.! ] - ; !-unique = λ { f → +-unique (sym (A-isInitial.!-unique (f ∘ i₁))) (sym (B-isInitial.!-unique (f ∘ i₂))) } + ; !-unique = λ f → +-unique (sym (A-isInitial.!-unique (f ∘ i₁))) (sym (B-isInitial.!-unique (f ∘ i₂))) } where open IsRightExact @@ -209,7 +244,14 @@ module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where module x+y = RightExactFunctor -+- ↔-+- : 𝒞 × 𝒞 ⇒ 𝒞 - ↔-+- = -+- ∘ Swap 𝒞 𝒞 + ↔-+- = record + { F = flip-bifunctor 𝒞.-+- + ; isRightExact = record + { F-resp-⊥ = λ x → +-resp-⊥ 𝒞 (flip-IsInitial 𝒞 x) + ; F-resp-+ = λ x → +-resp-+ 𝒞 (flip-IsCoproduct 𝒞 x) + ; F-resp-coeq = λ x → (+-resp-coeq 𝒞 (flip-IsCoequalizer 𝒞 x)) + } + } module y+x = RightExactFunctor ↔-+- [x+y]+z : (𝒞 × 𝒞) × 𝒞 ⇒ 𝒞 @@ -227,7 +269,6 @@ module _ {𝒞 : FinitelyCocompleteCategory o ℓ e} where module 𝒞×𝒞×𝒞 = FinitelyCocompleteCategory ((𝒞 × 𝒞) × 𝒞) open Morphism U using (_≅_; module ≅) module +-assoc {X} {Y} {Z} = _≅_ (≅.sym (+-assoc {X} {Y} {Z})) - open import Categories.Category.BinaryProducts using (BinaryProducts) open import Categories.Object.Duality 𝒞.U using (Coproduct⇒coProduct) op-binaryProducts : BinaryProducts op op-binaryProducts = record { product = Coproduct⇒coProduct coproduct } diff --git a/Category/Instance/Properties/SymMonCat.agda b/Category/Instance/Properties/SymMonCat.agda index fa15295..3b49b26 100644 --- a/Category/Instance/Properties/SymMonCat.agda +++ b/Category/Instance/Properties/SymMonCat.agda @@ -18,7 +18,6 @@ open import Categories.Category.Instance.One using (One) open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) open import Categories.Category.Cartesian SymMonCat using (Cartesian) open import Categories.Category.Cartesian.Bundle using (CartesianCategory) -open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) open import Categories.Category.BinaryProducts SymMonCat using (BinaryProducts) open import Categories.Functor.Monoidal.Construction.Product using () diff --git a/Category/Instance/SymMonCat.agda b/Category/Instance/SymMonCat.agda index e4b136c..814abeb 100644 --- a/Category/Instance/SymMonCat.agda +++ b/Category/Instance/SymMonCat.agda @@ -16,7 +16,7 @@ open import Relation.Binary.Core using (Rel) open import Categories.Category using (Category; _[_,_]; _[_∘_]) open import Categories.Category.Helper using (categoryHelper) open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory) -open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) +open import Categories.Functor.Monoidal.Symmetric.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) open SMF.Lax using (SymmetricMonoidalFunctor) open SMNI.Lax using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence) diff --git a/Category/Monoidal/Instance/DecoratedCospans.agda b/Category/Monoidal/Instance/DecoratedCospans.agda index 3df57ee..b0625ab 100644 --- a/Category/Monoidal/Instance/DecoratedCospans.agda +++ b/Category/Monoidal/Instance/DecoratedCospans.agda @@ -257,21 +257,21 @@ module LiftAssociator where open NaturalIsomorphism using (F⇐G) ≃₂≋≃₁ : (F⇐G (Hom[ 𝒟.U ][ 𝒟.unit ,-] ⓘˡ (F.F ⓘˡ assoc-≃))) ∘ᵥ ≃₂ ≋ ≃₁ ≃₂≋≃₁ {(X , Y) , Z} {(f , g) , h} = begin - F.₁ α⇐′ ∘ (F.⊗-homo.η (X , Y + Z) ∘ (f ⊗₁ _) ∘ ρ⇐) ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩ - F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h ∘ ρ⇐) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ sym-assoc ⟩∘⟨refl ⟩ - F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ ((F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ ρ⇐) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩ - F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ id ⊗₁ ρ⇐ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ ⟨ - F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ id ⊗₁ ρ⇐ ∘ λ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ unitorˡ-commute-to ⟨ - F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ λ⇐ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (switch-tofromˡ α coherence-inv₁) ⟩ - F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ α⇒ ∘ λ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩ - F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ f ⊗₁ (g ⊗₁ h) ∘ α⇒ ∘ λ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ ⟩⊗⟨refl ⟩∘⟨refl ⟩ - F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ f ⊗₁ (g ⊗₁ h) ∘ α⇒ ∘ ρ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨ - F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒ ∘ (f ⊗₁ g) ⊗₁ h ∘ ρ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym split₁ʳ) ⟩ - F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒ ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩ - F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ (id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒) ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐ ≈⟨ refl⟩∘⟨ sym-assoc ⟩ - F.₁ α⇐′ ∘ (F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒) ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐ ≈⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ α′) F.associativity) ⟨ - F.⊗-homo.η (X + Y , Z) ∘ F.⊗-homo.η (X , Y) ⊗₁ id ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ (sym split₁ˡ) ⟩ - F.⊗-homo.η (X + Y , Z) ∘ (F.⊗-homo.η (X , Y) ∘ (f ⊗₁ g) ∘ ρ⇐) ⊗₁ h ∘ ρ⇐ ∎ + F.₁ α⇐′ ∘ (F.⊗-homo.η (X , Y + Z) ∘ (f ⊗₁ _) ∘ ρ⇐) ∘ id ≈⟨ refl⟩∘⟨ identityʳ ⟩ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h ∘ ρ⇐) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ sym-assoc ⟩∘⟨refl ⟩ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ ((F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ ρ⇐) ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ id ⊗₁ ρ⇐ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ ⟨ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ id ⊗₁ ρ⇐ ∘ λ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ unitorˡ-commute-to ⟨ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ λ⇐ ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (switch-tofromˡ α coherence-inv₁) ⟩ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ f ⊗₁ (F.⊗-homo.η (Y , Z) ∘ g ⊗₁ h) ∘ α⇒ ∘ λ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ f ⊗₁ (g ⊗₁ h) ∘ α⇒ ∘ λ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ ⟩⊗⟨refl ⟩∘⟨refl ⟩ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ f ⊗₁ (g ⊗₁ h) ∘ α⇒ ∘ ρ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟨ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒ ∘ (f ⊗₁ g) ⊗₁ h ∘ ρ⇐ ⊗₁ id ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym split₁ʳ) ⟩ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒ ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym-assoc ⟩ + F.₁ α⇐′ ∘ F.⊗-homo.η (X , Y + Z) ∘ (id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒) ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐ ≈⟨ refl⟩∘⟨ sym-assoc ⟩ + F.₁ α⇐′ ∘ (F.⊗-homo.η (X , Y + Z) ∘ id ⊗₁ F.⊗-homo.η (Y , Z) ∘ α⇒) ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐ ≈⟨ extendʳ (switch-fromtoˡ ([ F.F ]-resp-≅ α′) F.associativity) ⟨ + F.⊗-homo.η (X + Y , Z) ∘ F.⊗-homo.η (X , Y) ⊗₁ id ∘ (f ⊗₁ g ∘ ρ⇐) ⊗₁ h ∘ ρ⇐ ≈⟨ refl⟩∘⟨ pullˡ (sym split₁ˡ) ⟩ + F.⊗-homo.η (X + Y , Z) ∘ (F.⊗-homo.η (X , Y) ∘ (f ⊗₁ g) ∘ ρ⇐) ⊗₁ h ∘ ρ⇐ ∎ where open Shorthands 𝒞.monoidal using () renaming (α⇐ to α⇐′) open Shorthands 𝒟.monoidal using (α⇒; λ⇐) diff --git a/Category/Monoidal/Instance/DecoratedCospans/Products.agda b/Category/Monoidal/Instance/DecoratedCospans/Products.agda index f8ef542..647f887 100644 --- a/Category/Monoidal/Instance/DecoratedCospans/Products.agda +++ b/Category/Monoidal/Instance/DecoratedCospans/Products.agda @@ -25,7 +25,7 @@ open import Categories.Category.BinaryProducts using (BinaryProducts) open import Categories.Category.Cartesian using (Cartesian) open import Categories.Category.Cartesian.Bundle using (CartesianCategory) open import Categories.Functor using (Functor; _∘F_) renaming (id to idF) -open import Categories.Functor.Monoidal.Properties using (∘-SymmetricMonoidal) +open import Categories.Functor.Monoidal.Symmetric.Properties using (∘-SymmetricMonoidal) open import Categories.Functor.Monoidal.Construction.Product using (⁂-SymmetricMonoidalFunctor) open import Categories.NaturalTransformation.Core using (NaturalTransformation; _∘ᵥ_; ntHelper) open import Category.Instance.Properties.SymMonCat {o} {ℓ} {e} using (SymMonCat-Cartesian) diff --git a/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda b/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda index 80b7b2f..77064ba 100644 --- a/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda +++ b/Functor/Instance/Underlying/SymmetricMonoidal/FinitelyCocomplete.agda @@ -12,7 +12,7 @@ open import Categories.Functor using (Functor; _∘F_) open import Categories.Functor.Properties using ([_]-resp-square; [_]-resp-∘) open import Categories.Functor.Monoidal using (IsMonoidalFunctor) open import Categories.Functor.Monoidal.Braided using (module Lax) -open import Categories.Functor.Monoidal.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) +open import Categories.Functor.Monoidal.Symmetric.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal) open import Categories.Functor.Monoidal.Symmetric using (module Lax) open import Categories.Category using (Category; _[_,_]; _[_≈_]; _[_∘_]) open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory; BraidedMonoidalCategory; MonoidalCategory) diff --git a/Functor/Monoidal/Strong/Properties.agda b/Functor/Monoidal/Strong/Properties.agda index 9eb7579..a8b8279 100644 --- a/Functor/Monoidal/Strong/Properties.agda +++ b/Functor/Monoidal/Strong/Properties.agda @@ -75,9 +75,6 @@ module Shorthands where open Shorthands open HomReasoning -associativityᵢ : Fα {X} {Y} {Z} ∘ᵢ φ ∘ᵢ φ ⊗ᵢ idᵢ ≈ᵢ φ ∘ᵢ idᵢ ⊗ᵢ φ ∘ᵢ α -associativityᵢ = ⌞ associativity ⌟ - associativity-inv : φ⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ (C.α⇐ {X} {Y} {Z}) ≈ α⇐ ∘ id ⊗₁ φ⇐ ∘ φ⇐ associativity-inv = begin φ⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ C.α⇐ ≈⟨ sym-assoc ⟩ @@ -85,18 +82,12 @@ associativity-inv = begin (α⇐ ∘ id ⊗₁ φ⇐) ∘ φ⇐ ≈⟨ assoc ⟩ α⇐ ∘ id ⊗₁ φ⇐ ∘ φ⇐ ∎ -unitaryˡᵢ : Fλ {X} ∘ᵢ φ ∘ᵢ ε ⊗ᵢ idᵢ ≈ᵢ λ- -unitaryˡᵢ = ⌞ unitaryˡ ⌟ - unitaryˡ-inv : ε⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ (C.λ⇐ {X}) ≈ λ⇐ unitaryˡ-inv = begin ε⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ C.λ⇐ ≈⟨ sym-assoc ⟩ (ε⇐ ⊗₁ id ∘ φ⇐) ∘ F₁ C.λ⇐ ≈⟨ to-≈ unitaryˡᵢ ⟩ λ⇐ ∎ -unitaryʳᵢ : Fρ {X} ∘ᵢ φ ∘ᵢ idᵢ ⊗ᵢ ε ≈ᵢ ρ -unitaryʳᵢ = ⌞ unitaryʳ ⌟ - unitaryʳ-inv : id ⊗₁ ε⇐ ∘ φ⇐ ∘ F₁ (C.ρ⇐ {X}) ≈ ρ⇐ unitaryʳ-inv = begin id ⊗₁ ε⇐ ∘ φ⇐ ∘ F₁ C.ρ⇐ ≈⟨ sym-assoc ⟩ -- cgit v1.2.3