diff --git a/src/Categories/Bicategory/Extras.agda b/src/Categories/Bicategory/Extras.agda index 6b78d261e..86765d5a8 100644 --- a/src/Categories/Bicategory/Extras.agda +++ b/src/Categories/Bicategory/Extras.agda @@ -6,6 +6,7 @@ module Categories.Bicategory.Extras {o ℓ e t} (Bicat : Bicategory o ℓ e t) w open import Data.Product using (_,_) +import Categories.Category.Construction.Core as Core open import Categories.Category.Construction.Functors using (Functors; module curry) open import Categories.Functor using (Functor) open import Categories.Functor.Bifunctor using (flip-bifunctor) @@ -16,9 +17,7 @@ open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIs import Categories.Morphism as Mor import Categories.Morphism.Reasoning as MR -import Categories.Morphism.IsoEquiv as IsoEquiv -open import Categories.NaturalTransformation.NaturalIsomorphism.Properties - using (push-eq) +open import Categories.NaturalTransformation.NaturalIsomorphism.Properties using (push-eq) open Bicategory Bicat public private @@ -27,11 +26,10 @@ private f g h i : A ⇒₁ B α β γ δ : f ⇒₂ g -infixr 7 _∘ᵢ_ -infixr 9 _▷ᵢ_ -infixl 9 _◁ᵢ_ -infixr 6 _⟩⊚⟨_ refl⟩⊚⟨_ -infixl 7 _⟩⊚⟨refl +infixr 10 _▷ᵢ_ +infixl 10 _◁ᵢ_ +infixr 6 _⟩⊚⟨_ refl⟩⊚⟨_ +infixl 7 _⟩⊚⟨refl module ⊚ {A B C} = Functor (⊚ {A} {B} {C}) module ⊚-assoc {A B C D} = NaturalIsomorphism (⊚-assoc {A} {B} {C} {D}) @@ -39,32 +37,39 @@ module unitˡ {A B} = NaturalIsomorphism (unitˡ {A} {B}) module unitʳ {A B} = NaturalIsomorphism (unitʳ {A} {B}) module id {A} = Functor (id {A}) -unitorˡ : {A B : Obj} {f : A ⇒₁ B} → Mor._≅_ (hom A B) (id₁ ∘ₕ f) f +private + module MR′ {A} {B} where + open Core.Shorthands (hom A B) public + open MR (hom A B) public hiding (push-eq) + open MR′ + +unitorˡ : {A B : Obj} {f : A ⇒₁ B} → id₁ ∘ₕ f ≅ f unitorˡ {_} {_} {f} = record { from = unitˡ.⇒.η (_ , f) ; to = unitˡ.⇐.η (_ , f) ; iso = unitˡ.iso (_ , f) } -module unitorˡ {A B f} = Mor._≅_ (unitorˡ {A} {B} {f}) +module unitorˡ {A B f} = _≅_ (unitorˡ {A} {B} {f}) -unitorʳ : {A B : Obj} {f : A ⇒₁ B} → Mor._≅_ (hom A B) (f ∘ₕ id₁) f +unitorʳ : {A B : Obj} {f : A ⇒₁ B} → f ∘ₕ id₁ ≅ f unitorʳ {_} {_} {f} = record { from = unitʳ.⇒.η (f , _) ; to = unitʳ.⇐.η (f , _) ; iso = unitʳ.iso (f , _) } -module unitorʳ {A B f} = Mor._≅_ (unitorʳ {A} {B} {f}) +module unitorʳ {A B f} = _≅_ (unitorʳ {A} {B} {f}) -associator : {A B C D : Obj} {f : D ⇒₁ B} {g : C ⇒₁ D} {h : A ⇒₁ C} → Mor._≅_ (hom A B) ((f ∘ₕ g) ∘ₕ h) (f ∘ₕ g ∘ₕ h) +associator : {A B C D : Obj} {f : D ⇒₁ B} {g : C ⇒₁ D} {h : A ⇒₁ C} → + (f ∘ₕ g) ∘ₕ h ≅ f ∘ₕ g ∘ₕ h associator {_} {_} {_} {_} {f} {g} {h} = record { from = ⊚-assoc.⇒.η ((f , g) , h) ; to = ⊚-assoc.⇐.η ((f , g) , h) ; iso = ⊚-assoc.iso ((f , g) , h) } -module associator {A B C D} {f : C ⇒₁ B} {g : D ⇒₁ C} {h} = Mor._≅_ (associator {A = A} {B = B} {f = f} {g = g} {h = h}) +module associator {A B C D} {f : C ⇒₁ B} {g : D ⇒₁ C} {h} = _≅_ (associator {A = A} {B = B} {f = f} {g = g} {h = h}) module Shorthands where λ⇒ = unitorˡ.from @@ -114,14 +119,6 @@ id₂◁ = ⊚.identity open hom.HomReasoning open hom.Equiv -private - module MR′ {A} {B} where - open MR (hom A B) public hiding (push-eq) - open Mor (hom A B) using (_≅_; module ≅) public - open IsoEquiv (hom A B) using (⌞_⌟; _≃_) public - open MR′ -idᵢ = λ {A B f} → ≅.refl {A} {B} {f} -_∘ᵢ_ = λ {A B f g h} α β → ≅.trans {A} {B} {f} {g} {h} β α _⊚ᵢ_ : f ≅ h → g ≅ i → f ⊚₀ g ≅ h ⊚₀ i α ⊚ᵢ β = record @@ -131,7 +128,6 @@ _⊚ᵢ_ : f ≅ h → g ≅ i → f ⊚₀ g ≅ h ⊚₀ i { isoˡ = [ ⊚ ]-merge (isoˡ α) (isoˡ β) ○ ⊚.identity ; isoʳ = [ ⊚ ]-merge (isoʳ α) (isoʳ β) ○ ⊚.identity } } - where open _≅_ _◁ᵢ_ : {g h : B ⇒₁ C} (α : g ≅ h) (f : A ⇒₁ B) → g ∘ₕ f ≅ h ∘ₕ f α ◁ᵢ _ = α ⊚ᵢ idᵢ @@ -170,7 +166,7 @@ _⟩⊚⟨refl = ⊚-resp-≈ˡ α ∘ᵥ λ⇒ ∎ ▷-∘ᵥ-λ⇐ : (id₁ ▷ α) ∘ᵥ λ⇐ ≈ λ⇐ ∘ᵥ α -▷-∘ᵥ-λ⇐ = conjugate-to (≅.sym unitorˡ) (≅.sym unitorˡ) λ⇒-∘ᵥ-▷ +▷-∘ᵥ-λ⇐ = conjugate-to (unitorˡ ⁻¹) (unitorˡ ⁻¹) λ⇒-∘ᵥ-▷ ρ⇒-∘ᵥ-◁ : ρ⇒ ∘ᵥ (α ◁ id₁) ≈ α ∘ᵥ ρ⇒ ρ⇒-∘ᵥ-◁ {α = α} = begin @@ -179,7 +175,7 @@ _⟩⊚⟨refl = ⊚-resp-≈ˡ α ∘ᵥ ρ⇒ ∎ ◁-∘ᵥ-ρ⇐ : (α ◁ id₁) ∘ᵥ ρ⇐ ≈ ρ⇐ ∘ᵥ α -◁-∘ᵥ-ρ⇐ = conjugate-to (≅.sym unitorʳ) (≅.sym unitorʳ) ρ⇒-∘ᵥ-◁ +◁-∘ᵥ-ρ⇐ = conjugate-to (unitorʳ ⁻¹) (unitorʳ ⁻¹) ρ⇒-∘ᵥ-◁ α⇐-◁-∘ₕ : α⇐ ∘ᵥ (γ ◁ (g ∘ₕ f)) ≈ ((γ ◁ g) ◁ f) ∘ᵥ α⇐ α⇐-◁-∘ₕ {γ = γ} {g = g} {f = f} = begin @@ -206,20 +202,20 @@ _⟩⊚⟨refl = ⊚-resp-≈ˡ ◁-▷-exchg = [ ⊚ ]-commute triangle-iso : {f : A ⇒₁ B} {g : B ⇒₁ C} → - (g ▷ᵢ unitorˡ ∘ᵢ associator) ≃ (unitorʳ ◁ᵢ f) + (g ▷ᵢ unitorˡ ∘ᵢ associator) ≈ᵢ (unitorʳ ◁ᵢ f) triangle-iso = ⌞ triangle ⌟ triangle-inv : {f : A ⇒₁ B} {g : B ⇒₁ C} → α⇐ ∘ᵥ g ▷ λ⇐ ≈ ρ⇐ ◁ f -triangle-inv = _≃_.to-≈ triangle-iso +triangle-inv = to-≈ triangle-iso pentagon-iso : ∀ {E} {f : A ⇒₁ B} {g : B ⇒₁ C} {h : C ⇒₁ D} {i : D ⇒₁ E} → - (i ▷ᵢ associator ∘ᵢ associator ∘ᵢ associator ◁ᵢ f) ≃ + (i ▷ᵢ associator ∘ᵢ associator ∘ᵢ associator ◁ᵢ f) ≈ᵢ (associator {f = i} {h} {g ∘ₕ f} ∘ᵢ associator) pentagon-iso = ⌞ pentagon ⌟ pentagon-inv : ∀ {E} {f : A ⇒₁ B} {g : B ⇒₁ C} {h : C ⇒₁ D} {i : D ⇒₁ E} → (α⇐ ◁ f ∘ᵥ α⇐) ∘ᵥ i ▷ α⇐ ≈ α⇐ ∘ᵥ α⇐ {f = i} {h} {g ∘ₕ f} -pentagon-inv = _≃_.to-≈ pentagon-iso +pentagon-inv = to-≈ pentagon-iso module UnitorCoherence where diff --git a/src/Categories/Category/Construction/Core.agda b/src/Categories/Category/Construction/Core.agda index e7cdf188e..4dc229fa7 100644 --- a/src/Categories/Category/Construction/Core.agda +++ b/src/Categories/Category/Construction/Core.agda @@ -11,8 +11,8 @@ open import Level using (_⊔_) open import Function using (flip) open import Categories.Category.Groupoid using (Groupoid; IsGroupoid) -open import Categories.Morphism 𝒞 -open import Categories.Morphism.IsoEquiv 𝒞 +open import Categories.Morphism 𝒞 as Morphism +open import Categories.Morphism.IsoEquiv 𝒞 as IsoEquiv open Category 𝒞 open _≃_ @@ -42,3 +42,33 @@ Core-isGroupoid = record CoreGroupoid : Groupoid o (ℓ ⊔ e) e CoreGroupoid = record { category = Core; isGroupoid = Core-isGroupoid } + +module CoreGroupoid = Groupoid CoreGroupoid + +-- Useful shorthands for reasoning about isomorphisms and morphisms of +-- 𝒞 in the same module. + +module Shorthands where + module Commutationᵢ where + open Commutation Core public using () renaming ([_⇒_]⟨_≈_⟩ to [_≅_]⟨_≈_⟩) + + infixl 2 connectᵢ + connectᵢ : ∀ {A C : Obj} (B : Obj) → A ≅ B → B ≅ C → A ≅ C + connectᵢ B f g = ≅.trans f g + + syntax connectᵢ B f g = f ≅⟨ B ⟩ g + + open _≅_ public + open _≃_ public + open Morphism public using (module _≅_) + open IsoEquiv public using (⌞_⌟) renaming (module _≃_ to _≈ᵢ_) + open CoreGroupoid public using (_⁻¹) renaming + ( _⇒_ to _≅_ + ; _≈_ to _≈ᵢ_ + ; id to idᵢ + ; _∘_ to _∘ᵢ_ + ; iso to ⁻¹-iso + ; module Equiv to Equivᵢ + ; module HomReasoning to HomReasoningᵢ + ; module iso to ⁻¹-iso + ) diff --git a/src/Categories/Category/Monoidal/Braided/Properties.agda b/src/Categories/Category/Monoidal/Braided/Properties.agda index a61306f45..a63e7fe31 100644 --- a/src/Categories/Category/Monoidal/Braided/Properties.agda +++ b/src/Categories/Category/Monoidal/Braided/Properties.agda @@ -9,29 +9,43 @@ module Categories.Category.Monoidal.Braided.Properties open import Data.Product using (_,_) +import Categories.Category.Construction.Core C as Core open import Categories.Category.Monoidal.Properties M open import Categories.Category.Monoidal.Reasoning M -open import Categories.Category.Monoidal.Utilities M +import Categories.Category.Monoidal.Utilities M as MonoidalUtilities open import Categories.Functor using (Functor) -open import Categories.Morphism C using (module ≅) -open import Categories.Morphism.IsoEquiv C using (_≃_; ⌞_⌟) open import Categories.Morphism.Reasoning C hiding (push-eq) open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper) open import Categories.NaturalTransformation.NaturalIsomorphism.Properties using (push-eq) open Category C -open Braided BM open Commutation C +open Braided BM +open MonoidalUtilities using (_⊗ᵢ_; unitorʳ-naturalIsomorphism) +open MonoidalUtilities.Shorthands +open Core.Shorthands +open Commutationᵢ private variable X Y Z : Obj - -- A shorthand for the braiding - B : ∀ {X Y} → X ⊗₀ Y ⇒ Y ⊗₀ X - B {X} {Y} = braiding.⇒.η (X , Y) +-- Shorthands for the braiding + +module Shorthands where + + σ⇒ : ∀ {X Y} → X ⊗₀ Y ⇒ Y ⊗₀ X + σ⇒ {X} {Y} = braiding.⇒.η (X , Y) + σ⇐ : ∀ {X Y} → Y ⊗₀ X ⇒ X ⊗₀ Y + σ⇐ {X} {Y} = braiding.⇐.η (X , Y) + + σ = braiding.FX≅GX + +open Shorthands + +private -- It's easier to prove the following lemma, which is the desired -- coherence theorem moduolo application of the |-⊗ unit| functor. @@ -54,92 +68,91 @@ private -- -- -- ┌─────> X(11) ─────────> (11)X ──────┐ - -- ┌┘ α │ B │ α └┐ + -- ┌┘ α │ σ │ α └┐ -- ┌┘ │id⊗λ │λ⊗id └┐ -- ┌┘ V V V -- (X1)1 ═══════> X1 ════════════> 1X <══════ 1(1X) - -- ╚╗ ρ⊗id Λ <───┐ B λ Λ + -- ╚╗ ρ⊗id Λ <───┐ σ λ Λ -- ╚╗ │λ⊗id └────────┐ ╔╝ -- ╚╗ │ λ └┐ ╔╝ -- ╚═════> (1X)1 ═════════> 1(X1) ═════╝ - -- B⊗id α id⊗B + -- σ⊗id α id⊗σ braiding-coherence⊗unit : [ (X ⊗₀ unit) ⊗₀ unit ⇒ X ⊗₀ unit ]⟨ - B ⊗₁ id ⇒⟨ (unit ⊗₀ X) ⊗₀ unit ⟩ - unitorˡ.from ⊗₁ id - ≈ unitorʳ.from ⊗₁ id - ⟩ - braiding-coherence⊗unit = cancel-fromˡ braiding.FX≅GX ( - begin - B ∘ unitorˡ.from ⊗₁ id ∘ B ⊗₁ id ≈⟨ pullˡ (⟺ (glue◽◃ unitorˡ-commute-from coherence₁)) ⟩ - (unitorˡ.from ∘ id ⊗₁ B ∘ associator.from) ∘ B ⊗₁ id ≈⟨ assoc²' ⟩ - unitorˡ.from ∘ id ⊗₁ B ∘ associator.from ∘ B ⊗₁ id ≈⟨ refl⟩∘⟨ hexagon₁ ⟩ - unitorˡ.from ∘ associator.from ∘ B ∘ associator.from ≈⟨ pullˡ coherence₁ ⟩ - unitorˡ.from ⊗₁ id ∘ B ∘ associator.from ≈˘⟨ pushˡ (braiding.⇒.commute _) ⟩ - (B ∘ id ⊗₁ unitorˡ.from) ∘ associator.from ≈⟨ pullʳ triangle ⟩ - B ∘ unitorʳ.from ⊗₁ id - ∎) + σ⇒ ⊗₁ id ⇒⟨ (unit ⊗₀ X) ⊗₀ unit ⟩ + λ⇒ ⊗₁ id + ≈ ρ⇒ ⊗₁ id + ⟩ + braiding-coherence⊗unit = cancel-fromˡ braiding.FX≅GX (begin + σ⇒ ∘ λ⇒ ⊗₁ id ∘ σ⇒ ⊗₁ id ≈⟨ pullˡ (⟺ (glue◽◃ unitorˡ-commute-from coherence₁)) ⟩ + (λ⇒ ∘ id ⊗₁ σ⇒ ∘ α⇒) ∘ σ⇒ ⊗₁ id ≈⟨ assoc²' ⟩ + λ⇒ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id ≈⟨ refl⟩∘⟨ hexagon₁ ⟩ + λ⇒ ∘ α⇒ ∘ σ⇒ ∘ α⇒ ≈⟨ pullˡ coherence₁ ⟩ + λ⇒ ⊗₁ id ∘ σ⇒ ∘ α⇒ ≈˘⟨ pushˡ (braiding.⇒.commute _) ⟩ + (σ⇒ ∘ id ⊗₁ λ⇒) ∘ α⇒ ≈⟨ pullʳ triangle ⟩ + σ⇒ ∘ ρ⇒ ⊗₁ id ∎) -- The desired theorem follows from |braiding-coherence⊗unit| by -- translating it along the right unitor (which is a natural iso). braiding-coherence : [ X ⊗₀ unit ⇒ X ]⟨ - B ⇒⟨ unit ⊗₀ X ⟩ - unitorˡ.from - ≈ unitorʳ.from + σ⇒ ⇒⟨ unit ⊗₀ X ⟩ + λ⇒ + ≈ ρ⇒ ⟩ braiding-coherence = push-eq unitorʳ-naturalIsomorphism (begin - (unitorˡ.from ∘ B) ⊗₁ id ≈⟨ homomorphism ⟩ - (unitorˡ.from ⊗₁ id) ∘ (B ⊗₁ id) ≈⟨ braiding-coherence⊗unit ⟩ - unitorʳ.from ⊗₁ id ∎) + (λ⇒ ∘ σ⇒) ⊗₁ id ≈⟨ homomorphism ⟩ + (λ⇒ ⊗₁ id) ∘ (σ⇒ ⊗₁ id) ≈⟨ braiding-coherence⊗unit ⟩ + ρ⇒ ⊗₁ id ∎) where open Functor (-⊗ unit) - --- Shorthands for working with isomorphisms. - -open ≅ using () renaming (refl to idᵢ; sym to _⁻¹) -infixr 9 _∘ᵢ_ -private - _∘ᵢ_ = λ {A B C} f g → ≅.trans {A} {B} {C} g f - Bᵢ = braiding.FX≅GX - B⁻¹ = λ {X} {Y} → braiding.⇐.η (X , Y) - -- Variants of the hexagon identities defined on isos. -hexagon₁-iso : idᵢ ⊗ᵢ Bᵢ ∘ᵢ associator ∘ᵢ Bᵢ {X , Y} ⊗ᵢ idᵢ {Z} ≃ - associator ∘ᵢ Bᵢ {X , Y ⊗₀ Z} ∘ᵢ associator +hexagon₁-iso : idᵢ ⊗ᵢ σ ∘ᵢ associator ∘ᵢ σ {X , Y} ⊗ᵢ idᵢ {Z} ≈ᵢ + associator ∘ᵢ σ {X , Y ⊗₀ Z} ∘ᵢ associator hexagon₁-iso = ⌞ hexagon₁ ⌟ -hexagon₂-iso : (Bᵢ ⊗ᵢ idᵢ ∘ᵢ associator ⁻¹) ∘ᵢ idᵢ {X} ⊗ᵢ Bᵢ {Y , Z} ≃ - (associator ⁻¹ ∘ᵢ Bᵢ {X ⊗₀ Y , Z}) ∘ᵢ associator ⁻¹ +hexagon₁-inv : (σ⇐ {X} {Y} ⊗₁ id {Z} ∘ α⇐) ∘ id ⊗₁ σ⇐ ≈ + (α⇐ ∘ σ⇐ {X} {Y ⊗₀ Z}) ∘ α⇐ +hexagon₁-inv = to-≈ hexagon₁-iso + +hexagon₂-iso : (σ ⊗ᵢ idᵢ ∘ᵢ associator ⁻¹) ∘ᵢ idᵢ {X} ⊗ᵢ σ {Y , Z} ≈ᵢ + (associator ⁻¹ ∘ᵢ σ {X ⊗₀ Y , Z}) ∘ᵢ associator ⁻¹ hexagon₂-iso = ⌞ hexagon₂ ⌟ --- A variants of the above coherence law defined on isos. +hexagon₂-inv : id {X} ⊗₁ σ⇐ {Y} {Z} ∘ α⇒ ∘ σ⇐ ⊗₁ id ≈ + α⇒ ∘ σ⇐ {X ⊗₀ Y} {Z} ∘ α⇒ +hexagon₂-inv = to-≈ hexagon₂-iso + +-- Variants of the above coherence law. -braiding-coherence-iso : unitorˡ ∘ᵢ Bᵢ ≃ unitorʳ {X} +braiding-coherence-iso : unitorˡ ∘ᵢ σ ≈ᵢ unitorʳ {X} braiding-coherence-iso = ⌞ braiding-coherence ⌟ +braiding-coherence-inv : σ⇐ ∘ λ⇐ ≈ ρ⇐ {X} +braiding-coherence-inv = to-≈ braiding-coherence-iso + -- The inverse of the braiding is also a braiding on M. inv-Braided : Braided M inv-Braided = record { braiding = niHelper (record - { η = λ _ → B⁻¹ - ; η⁻¹ = λ _ → B + { η = λ _ → σ⇐ + ; η⁻¹ = λ _ → σ⇒ ; commute = λ{ (f , g) → braiding.⇐.commute (g , f) } ; iso = λ{ (X , Y) → record { isoˡ = braiding.iso.isoʳ (Y , X) ; isoʳ = braiding.iso.isoˡ (Y , X) } } }) - ; hexagon₁ = _≃_.to-≈ hexagon₂-iso - ; hexagon₂ = _≃_.to-≈ hexagon₁-iso + ; hexagon₁ = hexagon₂-inv + ; hexagon₂ = hexagon₁-inv } -- A variant of the above coherence law for the inverse of the braiding. inv-braiding-coherence : [ unit ⊗₀ X ⇒ X ]⟨ - B⁻¹ ⇒⟨ X ⊗₀ unit ⟩ - unitorʳ.from - ≈ unitorˡ.from + σ⇐ ⇒⟨ X ⊗₀ unit ⟩ + ρ⇒ + ≈ λ⇒ ⟩ -inv-braiding-coherence = ⟺ (switch-fromtoʳ Bᵢ braiding-coherence) +inv-braiding-coherence = ⟺ (switch-fromtoʳ σ braiding-coherence) diff --git a/src/Categories/Category/Monoidal/Core.agda b/src/Categories/Category/Monoidal/Core.agda index 1f97b3f10..772283b67 100644 --- a/src/Categories/Category/Monoidal/Core.agda +++ b/src/Categories/Category/Monoidal/Core.agda @@ -16,21 +16,13 @@ open import Categories.Category module Categories.Category.Monoidal.Core {o ℓ e} (C : Category o ℓ e) where -open import Level -open import Function using (_$_) -open import Data.Product using (_×_; _,_; curry′) +open import Level using (_⊔_) +open import Data.Product using (_,_; curry′) -open import Categories.Category.Product -open import Categories.Functor renaming (id to idF) +open import Categories.Functor using (Functor) open import Categories.Functor.Bifunctor using (Bifunctor; appˡ; appʳ) -open import Categories.Functor.Properties using ([_]-resp-≅) -open import Categories.NaturalTransformation renaming (id to idN) -open import Categories.NaturalTransformation.NaturalIsomorphism - hiding (unitorˡ; unitorʳ; associator; _≃_) -open import Categories.Morphism C using (_≅_; module ≅) -open import Categories.Morphism.IsoEquiv C using (_≃_; ⌞_⌟) -open import Categories.Morphism.Isomorphism C using (_∘ᵢ_; lift-triangle′; lift-pentagon′) -open import Categories.Morphism.Reasoning C +open import Categories.Morphism C using (_≅_) +open import Categories.Morphism.Reasoning C using (conjugate-from) private module C = Category C diff --git a/src/Categories/Category/Monoidal/Interchange/Braided.agda b/src/Categories/Category/Monoidal/Interchange/Braided.agda index 2b77f7c5b..f5d225f5d 100644 --- a/src/Categories/Category/Monoidal/Interchange/Braided.agda +++ b/src/Categories/Category/Monoidal/Interchange/Braided.agda @@ -12,8 +12,9 @@ module Categories.Category.Monoidal.Interchange.Braided open import Level using (_⊔_) open import Data.Product using (_,_) +import Categories.Category.Construction.Core C as Core import Categories.Category.Monoidal.Construction.Product as MonoidalProduct -open import Categories.Category.Monoidal.Braided.Properties +open import Categories.Category.Monoidal.Braided.Properties as BraidedProps using (braiding-coherence; inv-Braided; inv-braiding-coherence) open import Categories.Category.Monoidal.Interchange using (HasInterchange) open import Categories.Category.Monoidal.Properties using (module Kelly's) @@ -23,8 +24,6 @@ open import Categories.Category.Product using (_⁂_; assocˡ) open import Categories.Functor using (_∘F_) open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper) -open import Categories.Morphism C using (_≅_; module ≅) -open import Categories.Morphism.IsoEquiv C using (module _≃_) open import Categories.Morphism.Reasoning C open Category C @@ -35,28 +34,14 @@ private W W₁ W₂ X X₁ X₂ Y Y₁ Y₂ Z Z₁ Z₂ : Obj f g h i : X ⇒ Y --- Shorthands for composing and inverting isomorphisms. - -open ≅ using () renaming (refl to idᵢ; sym to _⁻¹) -private - infixr 9 _∘ᵢ_ - _∘ᵢ_ = λ {X Y Z} f g → ≅.trans {X} {Y} {Z} g f - -- Braided monoidal categories have an interchange map. open MonoidalReasoning M open MonoidalUtilities M open Braided B renaming (associator to α) -open Shorthands - --- Shorthands for braiding. - -private - σ : X ⊗₀ Y ≅ Y ⊗₀ X - σ = braiding.FX≅GX - module σ {X Y} = _≅_ (σ {X} {Y}) - σ⇒ = σ.from - σ⇐ = σ.to +open Core.Shorthands -- for idᵢ, _∘ᵢ_, ... +open Shorthands -- for λ⇒, ρ⇒, α⇒, ... +open BraidedProps.Shorthands B -- for σ⇒, ... -- The "four middle interchange" for braided tensor products. @@ -156,13 +141,12 @@ private id ⊗₁ α⇒ ∘ α⇒ ⊗₁ id ≈⟨ refl⟩∘⟨ (begin α⇒ ⊗₁ id ≈⟨ switch-fromtoˡ α (switch-fromtoˡ (idᵢ ⊗ᵢ α) pentagon) ⟩ α⇐ ∘ id ⊗₁ α⇐ ∘ α⇒ ∘ α⇒ ≈˘⟨ refl⟩∘⟨ refl⟩⊗⟨ cancelˡ α.isoʳ ⟩∘⟨refl ⟩ - α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇐ ∘ α⇐) ∘ α⇒ ∘ α⇒ ≈˘⟨ refl⟩∘⟨ refl⟩⊗⟨ pullʳ inv-pentagon ⟩∘⟨refl ⟩ + α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇐ ∘ α⇐) ∘ α⇒ ∘ α⇒ ≈˘⟨ refl⟩∘⟨ refl⟩⊗⟨ pullʳ pentagon-inv ⟩∘⟨refl ⟩ α⇐ ∘ id ⊗₁ (α-mid ∘ id ⊗₁ α⇐) ∘ α⇒ ∘ α⇒ ≈⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩ α⇐ ∘ id ⊗₁ α-mid ∘ id ⊗₁ (id ⊗₁ α⇐) ∘ α⇒ ∘ α⇒ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ assoc-commute-from ⟩ α⇐ ∘ id ⊗₁ α-mid ∘ α⇒ ∘ (id ⊗₁ id) ⊗₁ α⇐ ∘ α⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩∘⟨refl ⟩ α⇐ ∘ id ⊗₁ α-mid ∘ α⇒ ∘ id ⊗₁ α⇐ ∘ α⇒ ∎) ⟩ id ⊗₁ α⇒ ∘ α⇐ ∘ id ⊗₁ α-mid ∘ α⇒ ∘ id ⊗₁ α⇐ ∘ α⇒ ∎ - where inv-pentagon = λ {W X Y Z} → _≃_.to-≈ (pentagon-iso {W} {X} {Y} {Z}) swapInner-assoc : [ ((X₁ ⊗₀ X₂) ⊗₀ (Y₁ ⊗₀ Y₂)) ⊗₀ (Z₁ ⊗₀ Z₂) ⇒ (X₁ ⊗₀ (Y₁ ⊗₀ Z₁)) ⊗₀ (X₂ ⊗₀ (Y₂ ⊗₀ Z₂)) ]⟨ @@ -232,7 +216,7 @@ swapInner-assoc = begin α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ (id ⊗₁ σ⇒) ⊗₁ id ∘ (α⇐ ∘ (id ⊗₁ α⇐ ∘ α⇒)) ∘ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ (sym-assoc ○ - (conjugate-to α (α ⊗ᵢ idᵢ) (sym-assoc ○ inv-pentagon))) ⟩∘⟨refl ⟩ + (conjugate-to α (α ⊗ᵢ idᵢ) (sym-assoc ○ pentagon-inv))) ⟩∘⟨refl ⟩ α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ (id ⊗₁ σ⇒) ⊗₁ id ∘ (α⇒ ⊗₁ id ∘ α⇐) ∘ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐ ≈˘⟨ refl⟩∘⟨ split₁ Equiv.refl ⟩∘⟨ @@ -245,7 +229,7 @@ swapInner-assoc = begin ≈˘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩ α⇒ ∘ ((α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ∘ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id) ⊗₁ id ∘ α⇐ ∘ α⇐ - ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (sym-assoc ○ inv-pentagon) ⟩ + ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (sym-assoc ○ pentagon-inv) ⟩ α⇒ ∘ ((α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ∘ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id) ⊗₁ id ∘ α⇐ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇐ ≈⟨ refl⟩∘⟨ pullˡ (⟺ split₁ˡ ○ (assoc ⟩⊗⟨refl)) ⟩ @@ -262,8 +246,8 @@ swapInner-assoc = begin α⇒ ∘ (σ⇒ ⊗₁ id) ⊗₁ id ∘ α⇐ ⊗₁ id ∘ α⇐ ≈⟨ pullʳ (refl⟩∘⟨ extendʳ assoc-commute-from) ⟩ (α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ id ⊗₁ α⇐) ∘ α⇒ ∘ σ⇒ ⊗₁ (id ⊗₁ id) ∘ α⇒ ∘ α⇐ ⊗₁ id ∘ α⇐ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ ⟺ split₂ˡ) ⟩∘⟨ refl⟩∘⟨ (refl⟩⊗⟨ ⊗.identity ⟩∘⟨ - conjugate-from (idᵢ ⊗ᵢ (α ⁻¹)) (α ⁻¹) inv-pentagon) ⟩ - (α⇐ ∘ α⇐ ∘ id ⊗₁ (σ⇒ ∘ α⇐)) ∘ α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒ ≈˘⟨ extendʳ (sym-assoc ○ inv-pentagon) ⟩∘⟨refl ⟩ + conjugate-from (idᵢ ⊗ᵢ (α ⁻¹)) (α ⁻¹) pentagon-inv) ⟩ + (α⇐ ∘ α⇐ ∘ id ⊗₁ (σ⇒ ∘ α⇐)) ∘ α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒ ≈˘⟨ extendʳ (sym-assoc ○ pentagon-inv) ⟩∘⟨refl ⟩ (α⇐ ⊗₁ id ∘ (α⇐ ∘ id ⊗₁ α⇐) ∘ id ⊗₁ (σ⇒ ∘ α⇐)) ∘ α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ α⇒ ≈˘⟨ (refl⟩∘⟨ pushʳ split₂ˡ) ⟩∘⟨refl ⟩ (α⇐ ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (α⇐ ∘ σ⇒ ∘ α⇐)) ∘ @@ -290,7 +274,7 @@ swapInner-assoc = begin ((((α⇐ ∘ id ⊗₁ σ⇒) ∘ α⇒) ⊗₁ id ∘ (σ⇒ ⊗₁ id) ⊗₁ id) ∘ α⇐) ∘ α⇐ ∘ id ⊗₁ id ⊗₁ σ⇒ ∘ id ⊗₁ α⇒ ≈˘⟨ ((sym-assoc ○ sym-assoc) ⟩⊗⟨refl ○ split₁ˡ) ⟩∘⟨refl ⟩∘⟨ refl⟩∘⟨ split₂ˡ ⟩ (((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ⊗₁ id) ∘ α⇐) ∘ - α⇐ ∘ id ⊗₁ (id ⊗₁ σ⇒ ∘ α⇒) ≈˘⟨ extend² (sym-assoc ○ inv-pentagon) ⟩ + α⇐ ∘ id ⊗₁ (id ⊗₁ σ⇒ ∘ α⇒) ≈˘⟨ extend² (sym-assoc ○ pentagon-inv) ⟩ (((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ⊗₁ id) ∘ α⇐ ⊗₁ id) ∘ (α⇐ ∘ id ⊗₁ α⇐) ∘ id ⊗₁ (id ⊗₁ σ⇒ ∘ α⇒) ≈˘⟨ split₁ˡ ⟩∘⟨ pushʳ split₂ˡ ⟩ ((α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐) ⊗₁ id ∘ @@ -319,7 +303,6 @@ swapInner-assoc = begin i⇒ ∘ (id ⊗₁ id) ⊗₁ j⇒ ∘ α⇒ ≈⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨ ⟺ swapInner-coherent ⟩∘⟨refl ⟩ i⇒ ∘ id ⊗₁ i⇒ ∘ α⇒ ∎ - where inv-pentagon = λ {W X Y Z} → _≃_.to-≈ (pentagon-iso {W} {X} {Y} {Z}) private mid-1-elim-coh : [ X ⊗₀ (unit ⊗₀ Y) ⇒ X ⊗₀ Y ]⟨ λ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐ ≈ id ⊗₁ λ⇒ ⟩ @@ -333,12 +316,9 @@ private Kelly₁′ : [ unit ⊗₀ (X ⊗₀ Y) ⇒ X ⊗₀ Y ]⟨ λ⇒ ⊗₁ id ∘ α⇐ ≈ λ⇒ ⟩ Kelly₁′ = ⟺ (switch-fromtoʳ α (Kelly's.coherence₁ M)) - Kelly₂′ : [ X ⊗₀ (Y ⊗₀ unit) ⇒ X ⊗₀ Y ]⟨ ρ⇒ ∘ α⇐ ≈ id ⊗₁ ρ⇒ ⟩ + Kelly₂′ : [ X ⊗₀ (Y ⊗₀ unit) ⇒ X ⊗₀ Y ]⟨ ρ⇒ ∘ α⇐ ≈ id ⊗₁ ρ⇒ ⟩ Kelly₂′ = ⟺ (switch-fromtoʳ α (Kelly's.coherence₂ M)) - Kelly₃′ : [ unit ⇒ unit ⊗₀ unit ]⟨ λ⇐ ≈ ρ⇐ ⟩ - Kelly₃′ = _≃_.to-≈ (Kelly's.coherence-iso₃ M) - σ⁻¹-coherence : [ unit ⊗₀ X ⇒ X ]⟨ ρ⇒ ∘ σ⇒ ≈ λ⇒ ⟩ σ⁻¹-coherence = inv-braiding-coherence (inv-Braided B) @@ -349,7 +329,7 @@ swapInner-unitˡ : [ unit ⊗₀ (X ⊗₀ Y) ⇒ (X ⊗₀ Y) ]⟨ ≈ λ⇒ ⟩ swapInner-unitˡ = begin - λ⇒ ⊗₁ λ⇒ ∘ i⇒ ∘ λ⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ swapInner-coherent ⟩∘⟨ (Kelly₃′ ⟩⊗⟨refl) ⟩ + λ⇒ ⊗₁ λ⇒ ∘ i⇒ ∘ λ⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ swapInner-coherent ⟩∘⟨ (Kelly's.coherence-inv₃ M ⟩⊗⟨refl) ⟩ λ⇒ ⊗₁ λ⇒ ∘ j⇒ ∘ ρ⇐ ⊗₁ id ≈⟨ pullˡ (pushˡ serialize₁₂) ⟩ (λ⇒ ⊗₁ id ∘ id ⊗₁ λ⇒ ∘ α⇒ ∘ swapʳ ⊗₁ id ∘ α⇐) ∘ ρ⇐ ⊗₁ id ≈⟨ (refl⟩∘⟨ (begin @@ -421,12 +401,11 @@ swapInner-braiding = begin α⇐ ∘ id ⊗₁ (id ⊗₁ σ⇒) ∘ id ⊗₁ swapˡ ∘ α⇒ ≈⟨ [23][14]ʳ ⟩∘⟨ [13][42]ˡ ⟩ ((α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇒ ⊗₁ id ∘ α⇐) ∘ (α⇐ ∘ id ⊗₁ α⇒) ∘ id ⊗₁ σ⇒ ∘ α⇒ ≈˘⟨ extendʳ (pushʳ (pushʳ assoc)) ⟩ (α⇒ ∘ σ⇒ ⊗₁ id) ∘ (α⇒ ⊗₁ id ∘ (α⇐ ∘ α⇐) ∘ id ⊗₁ α⇒) ∘ id ⊗₁ σ⇒ ∘ α⇒ ≈˘⟨ refl⟩∘⟨ switch-tofromˡ (α ⊗ᵢ idᵢ) - (switch-tofromʳ (idᵢ ⊗ᵢ α) inv-pentagon) ⟩∘⟨refl ⟩ + (switch-tofromʳ (idᵢ ⊗ᵢ α) pentagon-inv) ⟩∘⟨refl ⟩ (α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒ ≈⟨ pullʳ (sym-assoc ○ pullˡ hexagon₂) ⟩ α⇒ ∘ ((α⇐ ∘ σ⇒) ∘ α⇐) ∘ α⇒ ≈⟨ (refl⟩∘⟨ cancelʳ α.isoˡ) ⟩ α⇒ ∘ (α⇐ ∘ σ⇒) ≈⟨ cancelˡ α.isoʳ ⟩ σ⇒ ∎ - where inv-pentagon = _≃_.to-≈ pentagon-iso -- Braided monoidal categories have an interchange. diff --git a/src/Categories/Category/Monoidal/Interchange/Symmetric.agda b/src/Categories/Category/Monoidal/Interchange/Symmetric.agda index 06adcdf44..134da1111 100644 --- a/src/Categories/Category/Monoidal/Interchange/Symmetric.agda +++ b/src/Categories/Category/Monoidal/Interchange/Symmetric.agda @@ -11,46 +11,39 @@ module Categories.Category.Monoidal.Interchange.Symmetric open import Data.Product using (_,_) +import Categories.Category.Construction.Core C as Core +import Categories.Category.Monoidal.Braided.Properties as BraidedProps open import Categories.Category.Monoidal.Interchange using (HasInterchange) import Categories.Category.Monoidal.Interchange.Braided as BraidedInterchange using (module swapInner; swapInner-braiding) -import Categories.Category.Monoidal.Reasoning as MonoidalReasoning -import Categories.Category.Monoidal.Utilities as MonoidalUtilities - using (module Shorthands; _⊗ᵢ_) +import Categories.Category.Monoidal.Reasoning M as MonoidalReasoning +import Categories.Category.Monoidal.Utilities M as MonoidalUtilities open import Categories.Category.Product using (_⁂_; assocˡ) open import Categories.Functor using (_∘F_) open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper) -open import Categories.Morphism C using (_≅_; module ≅) open import Categories.Morphism.IsoEquiv C using (to-unique) open import Categories.Morphism.Reasoning C using (elim-center; pushˡ; pullʳ; cancelInner; switch-fromtoˡ) open Category C using (Obj; _⇒_; _∘_; id; sym-assoc; ∘-resp-≈ʳ; module Equiv) open Commutation C -open MonoidalReasoning M -open MonoidalUtilities M -open Symmetric S renaming (associator to α) -open Shorthands -open BraidedInterchange braided +open MonoidalReasoning +open MonoidalUtilities using (_⊗ᵢ_) +open Symmetric S renaming (associator to α; braided to B) +open BraidedInterchange B +open Core.Shorthands -- for idᵢ, _∘ᵢ_, ... +open MonoidalUtilities.Shorthands -- for λ⇒, ρ⇒, α⇒, ... +open BraidedProps.Shorthands B -- for σ⇒, ... private variable W W₁ W₂ X X₁ X₂ Y Y₁ Y₂ Z Z₁ Z₂ : Obj f g h i : X ⇒ Y --- Shorthands for composing and inverting isomorphisms. - -open ≅ using () renaming (refl to idᵢ; sym to _⁻¹) -private - infixr 9 _∘ᵢ_ - _∘ᵢ_ = λ {X Y Z} f g → ≅.trans {X} {Y} {Z} g f - private i⇒ = swapInner.from i⇐ = swapInner.to - σ⇒ = λ {X Y} → braiding.⇒.η (X , Y) - σ⇐ = λ {X Y} → braiding.⇐.η (X , Y) swapInner-commutative : [ (X₁ ⊗₀ X₂) ⊗₀ (Y₁ ⊗₀ Y₂) ⇒ (X₁ ⊗₀ X₂) ⊗₀ (Y₁ ⊗₀ Y₂) ]⟨ @@ -82,7 +75,7 @@ swapInner-selfInverse : [ (X₁ ⊗₀ X₂) ⊗₀ (Y₁ ⊗₀ Y₂) ⇒ ≈ i⇐ ⟩ swapInner-selfInverse = - to-unique (_≅_.iso swapInner-iso) swapInner.iso Equiv.refl + to-unique (iso swapInner-iso) swapInner.iso Equiv.refl swapInner-braiding′ : [ (W ⊗₀ X) ⊗₀ (Y ⊗₀ Z) ⇒ (Y ⊗₀ W) ⊗₀ (Z ⊗₀ X) ]⟨ i⇒ ⇒⟨ (W ⊗₀ Y) ⊗₀ (X ⊗₀ Z) ⟩ diff --git a/src/Categories/Category/Monoidal/Properties.agda b/src/Categories/Category/Monoidal/Properties.agda index da51660e3..18798a4d0 100644 --- a/src/Categories/Category/Monoidal/Properties.agda +++ b/src/Categories/Category/Monoidal/Properties.agda @@ -13,15 +13,13 @@ open Category C open M.Monoidal MC open import Categories.Category.Monoidal.Utilities MC import Categories.Category.Monoidal.Reasoning as MonR -open import Categories.Category.Construction.Core C +open import Categories.Category.Construction.Core C as Core using (Core) open import Categories.Category.Product using (Product) open import Categories.Functor using (Functor) open import Categories.Functor.Bifunctor open import Categories.Functor.Properties -open import Categories.Category.Groupoid using (IsGroupoid) -open import Categories.Morphism C -open import Categories.Morphism.IsoEquiv C using (_≃_; ⌞_⌟) open import Categories.Morphism.Isomorphism C + using (elim-triangleˡ′; triangle-prism; cut-squareʳ) import Categories.Morphism.Reasoning as MR open import Categories.NaturalTransformation.NaturalIsomorphism.Properties using (push-eq) @@ -30,6 +28,7 @@ private module C = Category C variable A B : Obj +open Core.Shorthands ⊗-iso : Bifunctor Core Core Core ⊗-iso = record @@ -40,7 +39,6 @@ private ; F-resp-≈ = λ where (⌞ eq₁ ⌟ , ⌞ eq₂ ⌟) → ⌞ F-resp-≈ (eq₁ , eq₂) ⌟ } where open Functor ⊗ - open _≃_ _⊗ᵢ- : Obj → Functor Core Core X ⊗ᵢ- = appˡ ⊗-iso X @@ -55,193 +53,217 @@ X ⊗ᵢ- = appˡ ⊗-iso X module Kelly's where open Functor - open Commutation Core + open Shorthands + open Commutation C + open Commutationᵢ private - assoc′ = IsGroupoid.assoc Core-isGroupoid variable - f f′ g h h′ i i′ j k : A ≅ B + f f′ g h h′ i i′ j k : A ≅ B module _ {X Y : Obj} where - open IsGroupoid.HomReasoning Core-isGroupoid + open HomReasoningᵢ -- TS: following three isos commute ua : unit ⊗₀ (unit ⊗₀ X) ⊗₀ Y ≅ unit ⊗₀ unit ⊗₀ X ⊗₀ Y - ua = ≅.refl ⊗ᵢ associator + ua = idᵢ ⊗ᵢ associator u[λY] : unit ⊗₀ (unit ⊗₀ X) ⊗₀ Y ≅ unit ⊗₀ X ⊗₀ Y - u[λY] = ≅.refl ⊗ᵢ unitorˡ ⊗ᵢ ≅.refl + u[λY] = idᵢ ⊗ᵢ unitorˡ ⊗ᵢ idᵢ uλ : unit ⊗₀ unit ⊗₀ X ⊗₀ Y ≅ unit ⊗₀ X ⊗₀ Y - uλ = ≅.refl ⊗ᵢ unitorˡ + uλ = idᵢ ⊗ᵢ unitorˡ -- setups - perimeter : [ ((unit ⊗₀ unit) ⊗₀ X) ⊗₀ Y ⇒ unit ⊗₀ X ⊗₀ Y ]⟨ - (unitorʳ ⊗ᵢ ≅.refl) ⊗ᵢ ≅.refl ⇒⟨ (unit ⊗₀ X) ⊗₀ Y ⟩ + perimeter : [ ((unit ⊗₀ unit) ⊗₀ X) ⊗₀ Y ≅ unit ⊗₀ X ⊗₀ Y ]⟨ + (unitorʳ ⊗ᵢ idᵢ) ⊗ᵢ idᵢ ≅⟨ (unit ⊗₀ X) ⊗₀ Y ⟩ associator - ≈ associator ⇒⟨ (unit ⊗₀ unit) ⊗₀ X ⊗₀ Y ⟩ - associator ⇒⟨ unit ⊗₀ unit ⊗₀ X ⊗₀ Y ⟩ + ≈ associator ≅⟨ (unit ⊗₀ unit) ⊗₀ X ⊗₀ Y ⟩ + associator ≅⟨ unit ⊗₀ unit ⊗₀ X ⊗₀ Y ⟩ uλ ⟩ perimeter = ⟺ (glue◃◽′ triangle-iso - (⟺ (lift-square′ (Equiv.trans assoc-commute-from - (∘-resp-≈ˡ (F-resp-≈ ⊗ (Equiv.refl , identity ⊗))))))) + (⟺ ⌞ Equiv.trans assoc-commute-from + (∘-resp-≈ˡ (F-resp-≈ ⊗ (Equiv.refl , identity ⊗))) ⌟)) where open MR Core [uλ]Y : (unit ⊗₀ (unit ⊗₀ X)) ⊗₀ Y ≅ (unit ⊗₀ X) ⊗₀ Y - [uλ]Y = (≅.refl ⊗ᵢ unitorˡ) ⊗ᵢ ≅.refl + [uλ]Y = (idᵢ ⊗ᵢ unitorˡ) ⊗ᵢ idᵢ aY : ((unit ⊗₀ unit) ⊗₀ X) ⊗₀ Y ≅ (unit ⊗₀ unit ⊗₀ X) ⊗₀ Y - aY = associator ⊗ᵢ ≅.refl + aY = associator ⊗ᵢ idᵢ [ρX]Y : ((unit ⊗₀ unit) ⊗₀ X) ⊗₀ Y ≅ (unit ⊗₀ X) ⊗₀ Y - [ρX]Y = (unitorʳ ⊗ᵢ ≅.refl) ⊗ᵢ ≅.refl + [ρX]Y = (unitorʳ ⊗ᵢ idᵢ) ⊗ᵢ idᵢ - tri : [uλ]Y ∘ᵢ aY ≃ [ρX]Y - tri = lift-triangle′ ([ appʳ ⊗ Y ]-resp-∘ triangle) + tri : [uλ]Y ∘ᵢ aY ≈ᵢ [ρX]Y + tri = ⌞ [ appʳ ⊗ Y ]-resp-∘ triangle ⌟ - sq : associator ∘ᵢ [uλ]Y ≃ u[λY] ∘ᵢ associator - sq = lift-square′ assoc-commute-from + sq : associator ∘ᵢ [uλ]Y ≈ᵢ u[λY] ∘ᵢ associator + sq = ⌞ assoc-commute-from ⌟ -- proofs - perimeter′ : [ ((unit ⊗₀ unit) ⊗₀ X) ⊗₀ Y ⇒ unit ⊗₀ X ⊗₀ Y ]⟨ - (unitorʳ ⊗ᵢ ≅.refl) ⊗ᵢ ≅.refl ⇒⟨ (unit ⊗₀ X) ⊗₀ Y ⟩ + perimeter′ : [ ((unit ⊗₀ unit) ⊗₀ X) ⊗₀ Y ≅ unit ⊗₀ X ⊗₀ Y ]⟨ + (unitorʳ ⊗ᵢ idᵢ) ⊗ᵢ idᵢ ≅⟨ (unit ⊗₀ X) ⊗₀ Y ⟩ associator - ≈ aY ⇒⟨ (unit ⊗₀ (unit ⊗₀ X)) ⊗₀ Y ⟩ - associator ⇒⟨ unit ⊗₀ (unit ⊗₀ X) ⊗₀ Y ⟩ - ua ⇒⟨ unit ⊗₀ unit ⊗₀ X ⊗₀ Y ⟩ + ≈ aY ≅⟨ (unit ⊗₀ (unit ⊗₀ X)) ⊗₀ Y ⟩ + associator ≅⟨ unit ⊗₀ (unit ⊗₀ X) ⊗₀ Y ⟩ + ua ≅⟨ unit ⊗₀ unit ⊗₀ X ⊗₀ Y ⟩ uλ ⟩ perimeter′ = begin - associator ∘ᵢ (unitorʳ ⊗ᵢ ≅.refl) ⊗ᵢ ≅.refl ≈⟨ perimeter ⟩ - uλ ∘ᵢ associator ∘ᵢ associator ≈˘⟨ refl⟩∘⟨ pentagon-iso ⟩ - uλ ∘ᵢ ua ∘ᵢ associator ∘ᵢ aY ∎ + associator ∘ᵢ (unitorʳ ⊗ᵢ idᵢ) ⊗ᵢ idᵢ ≈⟨ perimeter ⟩ + uλ ∘ᵢ associator ∘ᵢ associator ≈˘⟨ refl⟩∘⟨ pentagon-iso ⟩ + uλ ∘ᵢ ua ∘ᵢ associator ∘ᵢ aY ∎ - top-face : uλ ∘ᵢ ua ≃ u[λY] + top-face : uλ ∘ᵢ ua ≈ᵢ u[λY] top-face = elim-triangleˡ′ (⟺ perimeter′) (glue◽◃ (⟺ sq) tri) where open MR Core - coherence-iso₁ : [ (unit ⊗₀ X) ⊗₀ Y ⇒ X ⊗₀ Y ]⟨ - associator ⇒⟨ unit ⊗₀ X ⊗₀ Y ⟩ - unitorˡ - ≈ unitorˡ ⊗ᵢ ≅.refl - ⟩ + coherence-iso₁ : [ (unit ⊗₀ X) ⊗₀ Y ≅ X ⊗₀ Y ]⟨ + associator ≅⟨ unit ⊗₀ X ⊗₀ Y ⟩ + unitorˡ + ≈ unitorˡ ⊗ᵢ idᵢ + ⟩ coherence-iso₁ = triangle-prism top-face square₁ square₂ square₃ - where square₁ : [ unit ⊗₀ X ⊗₀ Y ⇒ unit ⊗₀ X ⊗₀ Y ]⟨ - ≅.sym unitorˡ ∘ᵢ unitorˡ - ≈ ≅.refl ⊗ᵢ unitorˡ ∘ᵢ ≅.sym unitorˡ + where square₁ : [ unit ⊗₀ X ⊗₀ Y ≅ unit ⊗₀ X ⊗₀ Y ]⟨ + unitorˡ ⁻¹ ∘ᵢ unitorˡ + ≈ idᵢ ⊗ᵢ unitorˡ ∘ᵢ unitorˡ ⁻¹ ⟩ - square₁ = lift-square′ unitorˡ-commute-to + square₁ = ⌞ unitorˡ-commute-to ⌟ - square₂ : [ (unit ⊗₀ X) ⊗₀ Y ⇒ unit ⊗₀ unit ⊗₀ X ⊗₀ Y ]⟨ - ≅.sym unitorˡ ∘ᵢ associator - ≈ ≅.refl ⊗ᵢ associator ∘ᵢ ≅.sym unitorˡ + square₂ : [ (unit ⊗₀ X) ⊗₀ Y ≅ unit ⊗₀ unit ⊗₀ X ⊗₀ Y ]⟨ + unitorˡ ⁻¹ ∘ᵢ associator + ≈ idᵢ ⊗ᵢ associator ∘ᵢ unitorˡ ⁻¹ ⟩ - square₂ = lift-square′ unitorˡ-commute-to + square₂ = ⌞ unitorˡ-commute-to ⌟ - square₃ : [ (unit ⊗₀ X) ⊗₀ Y ⇒ unit ⊗₀ X ⊗₀ Y ]⟨ - ≅.sym unitorˡ ∘ᵢ unitorˡ ⊗ᵢ ≅.refl - ≈ ≅.refl ⊗ᵢ unitorˡ ⊗ᵢ ≅.refl ∘ᵢ ≅.sym unitorˡ + square₃ : [ (unit ⊗₀ X) ⊗₀ Y ≅ unit ⊗₀ X ⊗₀ Y ]⟨ + unitorˡ ⁻¹ ∘ᵢ unitorˡ ⊗ᵢ idᵢ + ≈ idᵢ ⊗ᵢ unitorˡ ⊗ᵢ idᵢ ∘ᵢ unitorˡ ⁻¹ ⟩ - square₃ = lift-square′ unitorˡ-commute-to + square₃ = ⌞ unitorˡ-commute-to ⌟ - coherence₁ : unitorˡ.from ∘ associator.from ≈ unitorˡ.from {X} ⊗₁ C.id {Y} - coherence₁ = project-triangle coherence-iso₁ + coherence₁ : [ (unit ⊗₀ X) ⊗₀ Y ⇒ X ⊗₀ Y ]⟨ + α⇒ ⇒⟨ unit ⊗₀ X ⊗₀ Y ⟩ + λ⇒ + ≈ λ⇒ ⊗₁ id + ⟩ + coherence₁ = from-≈ coherence-iso₁ + + coherence-inv₁ : [ X ⊗₀ Y ⇒ (unit ⊗₀ X) ⊗₀ Y ]⟨ + λ⇐ ⇒⟨ unit ⊗₀ X ⊗₀ Y ⟩ + α⇐ + ≈ λ⇐ ⊗₁ id + ⟩ + coherence-inv₁ = to-≈ coherence-iso₁ -- another coherence property -- TS : the following three commute ρu : ((X ⊗₀ Y) ⊗₀ unit) ⊗₀ unit ≅ (X ⊗₀ Y) ⊗₀ unit - ρu = unitorʳ ⊗ᵢ ≅.refl + ρu = unitorʳ ⊗ᵢ idᵢ au : ((X ⊗₀ Y) ⊗₀ unit) ⊗₀ unit ≅ (X ⊗₀ Y ⊗₀ unit) ⊗₀ unit - au = associator ⊗ᵢ ≅.refl + au = associator ⊗ᵢ idᵢ [Xρ]u : (X ⊗₀ Y ⊗₀ unit) ⊗₀ unit ≅ (X ⊗₀ Y) ⊗₀ unit - [Xρ]u = (≅.refl ⊗ᵢ unitorʳ) ⊗ᵢ ≅.refl + [Xρ]u = (idᵢ ⊗ᵢ unitorʳ) ⊗ᵢ idᵢ - perimeter″ : [ ((X ⊗₀ Y) ⊗₀ unit) ⊗₀ unit ⇒ X ⊗₀ Y ⊗₀ unit ]⟨ - associator ⇒⟨ (X ⊗₀ Y) ⊗₀ unit ⊗₀ unit ⟩ - associator ⇒⟨ X ⊗₀ Y ⊗₀ unit ⊗₀ unit ⟩ - ≅.refl ⊗ᵢ ≅.refl ⊗ᵢ unitorˡ - ≈ ρu ⇒⟨ (X ⊗₀ Y) ⊗₀ unit ⟩ + perimeter″ : [ ((X ⊗₀ Y) ⊗₀ unit) ⊗₀ unit ≅ X ⊗₀ Y ⊗₀ unit ]⟨ + associator ≅⟨ (X ⊗₀ Y) ⊗₀ unit ⊗₀ unit ⟩ + associator ≅⟨ X ⊗₀ Y ⊗₀ unit ⊗₀ unit ⟩ + idᵢ ⊗ᵢ idᵢ ⊗ᵢ unitorˡ + ≈ ρu ≅⟨ (X ⊗₀ Y) ⊗₀ unit ⟩ associator ⟩ - perimeter″ = glue▹◽ triangle-iso (⟺ (lift-square′ - (Equiv.trans (∘-resp-≈ʳ (F-resp-≈ ⊗ (Equiv.sym (identity ⊗) , Equiv.refl))) - assoc-commute-from))) + perimeter″ = glue▹◽ triangle-iso (⟺ ⌞ + Equiv.trans (∘-resp-≈ʳ (F-resp-≈ ⊗ (Equiv.sym (identity ⊗) , Equiv.refl))) + assoc-commute-from ⌟) where open MR Core - perimeter‴ : [ ((X ⊗₀ Y) ⊗₀ unit) ⊗₀ unit ⇒ X ⊗₀ Y ⊗₀ unit ]⟨ - associator ⊗ᵢ ≅.refl ⇒⟨ (X ⊗₀ (Y ⊗₀ unit)) ⊗₀ unit ⟩ - (associator ⇒⟨ X ⊗₀ (Y ⊗₀ unit) ⊗₀ unit ⟩ - ≅.refl ⊗ᵢ associator ⇒⟨ X ⊗₀ Y ⊗₀ unit ⊗₀ unit ⟩ - ≅.refl ⊗ᵢ ≅.refl ⊗ᵢ unitorˡ) - ≈ ρu ⇒⟨ (X ⊗₀ Y) ⊗₀ unit ⟩ + perimeter‴ : [ ((X ⊗₀ Y) ⊗₀ unit) ⊗₀ unit ≅ X ⊗₀ Y ⊗₀ unit ]⟨ + associator ⊗ᵢ idᵢ ≅⟨ (X ⊗₀ (Y ⊗₀ unit)) ⊗₀ unit ⟩ + (associator ≅⟨ X ⊗₀ (Y ⊗₀ unit) ⊗₀ unit ⟩ + idᵢ ⊗ᵢ associator ≅⟨ X ⊗₀ Y ⊗₀ unit ⊗₀ unit ⟩ + idᵢ ⊗ᵢ idᵢ ⊗ᵢ unitorˡ) + ≈ ρu ≅⟨ (X ⊗₀ Y) ⊗₀ unit ⟩ associator ⟩ perimeter‴ = let α = associator in let λλ = unitorˡ in begin - (≅.refl ⊗ᵢ ≅.refl ⊗ᵢ λλ ∘ᵢ ≅.refl ⊗ᵢ α ∘ᵢ α) ∘ᵢ α ⊗ᵢ ≅.refl ≈⟨ assoc′ ⟩ - ≅.refl ⊗ᵢ ≅.refl ⊗ᵢ λλ ∘ᵢ (≅.refl ⊗ᵢ α ∘ᵢ α) ∘ᵢ α ⊗ᵢ ≅.refl ≈⟨ refl⟩∘⟨ assoc′ ⟩ - ≅.refl ⊗ᵢ ≅.refl ⊗ᵢ λλ ∘ᵢ ≅.refl ⊗ᵢ α ∘ᵢ α ∘ᵢ α ⊗ᵢ ≅.refl ≈⟨ refl⟩∘⟨ pentagon-iso ⟩ - ≅.refl ⊗ᵢ ≅.refl ⊗ᵢ λλ ∘ᵢ α ∘ᵢ α ≈⟨ perimeter″ ⟩ - α ∘ᵢ ρu ∎ - - top-face′ : [Xρ]u ∘ᵢ au ≃ ρu - top-face′ = cut-squareʳ perimeter‴ (⟺ (glue◃◽′ tri′ (⟺ (lift-square′ assoc-commute-from)))) + (idᵢ ⊗ᵢ idᵢ ⊗ᵢ λλ ∘ᵢ idᵢ ⊗ᵢ α ∘ᵢ α) ∘ᵢ α ⊗ᵢ idᵢ ≈⟨ ⌞ assoc ⌟ ⟩ + idᵢ ⊗ᵢ idᵢ ⊗ᵢ λλ ∘ᵢ (idᵢ ⊗ᵢ α ∘ᵢ α) ∘ᵢ α ⊗ᵢ idᵢ ≈⟨ refl⟩∘⟨ ⌞ assoc ⌟ ⟩ + idᵢ ⊗ᵢ idᵢ ⊗ᵢ λλ ∘ᵢ idᵢ ⊗ᵢ α ∘ᵢ α ∘ᵢ α ⊗ᵢ idᵢ ≈⟨ refl⟩∘⟨ pentagon-iso ⟩ + idᵢ ⊗ᵢ idᵢ ⊗ᵢ λλ ∘ᵢ α ∘ᵢ α ≈⟨ perimeter″ ⟩ + α ∘ᵢ ρu ∎ + + top-face′ : [Xρ]u ∘ᵢ au ≈ᵢ ρu + top-face′ = cut-squareʳ perimeter‴ (⟺ (glue◃◽′ tri′ (⟺ ⌞ assoc-commute-from ⌟))) where open MR Core - tri′ : [ X ⊗₀ (Y ⊗₀ unit) ⊗₀ unit ⇒ X ⊗₀ Y ⊗₀ unit ]⟨ - (≅.refl ⊗ᵢ ≅.refl ⊗ᵢ unitorˡ ∘ᵢ ≅.refl ⊗ᵢ associator) - ≈ ≅.refl ⊗ᵢ unitorʳ ⊗ᵢ ≅.refl - ⟩ - tri′ = lift-triangle′ ([ X ⊗- ]-resp-∘ triangle) - - coherence-iso₂ : [ (X ⊗₀ Y) ⊗₀ unit ⇒ X ⊗₀ Y ]⟨ - ≅.refl ⊗ᵢ unitorʳ ∘ᵢ associator + tri′ : [ X ⊗₀ (Y ⊗₀ unit) ⊗₀ unit ≅ X ⊗₀ Y ⊗₀ unit ]⟨ + (idᵢ ⊗ᵢ idᵢ ⊗ᵢ unitorˡ ∘ᵢ idᵢ ⊗ᵢ associator) + ≈ idᵢ ⊗ᵢ unitorʳ ⊗ᵢ idᵢ + ⟩ + tri′ = ⌞ [ X ⊗- ]-resp-∘ triangle ⌟ + + coherence-iso₂ : [ (X ⊗₀ Y) ⊗₀ unit ≅ X ⊗₀ Y ]⟨ + idᵢ ⊗ᵢ unitorʳ ∘ᵢ associator ≈ unitorʳ ⟩ - coherence-iso₂ = triangle-prism top-face′ square₁ square₂ (lift-square′ unitorʳ-commute-to) - where square₁ : [ X ⊗₀ Y ⊗₀ unit ⇒ (X ⊗₀ Y) ⊗₀ unit ]⟨ - ≅.sym unitorʳ ∘ᵢ ≅.refl ⊗ᵢ unitorʳ - ≈ (≅.refl ⊗ᵢ unitorʳ) ⊗ᵢ ≅.refl ∘ᵢ ≅.sym unitorʳ + coherence-iso₂ = triangle-prism top-face′ square₁ square₂ ⌞ unitorʳ-commute-to ⌟ + where square₁ : [ X ⊗₀ Y ⊗₀ unit ≅ (X ⊗₀ Y) ⊗₀ unit ]⟨ + unitorʳ ⁻¹ ∘ᵢ idᵢ ⊗ᵢ unitorʳ + ≈ (idᵢ ⊗ᵢ unitorʳ) ⊗ᵢ idᵢ ∘ᵢ unitorʳ ⁻¹ ⟩ - square₁ = lift-square′ unitorʳ-commute-to + square₁ = ⌞ unitorʳ-commute-to ⌟ - square₂ : [ (X ⊗₀ Y) ⊗₀ unit ⇒ (X ⊗₀ Y ⊗₀ unit) ⊗₀ unit ]⟨ - ≅.sym unitorʳ ∘ᵢ associator - ≈ associator ⊗ᵢ ≅.refl ∘ᵢ ≅.sym unitorʳ + square₂ : [ (X ⊗₀ Y) ⊗₀ unit ≅ (X ⊗₀ Y ⊗₀ unit) ⊗₀ unit ]⟨ + unitorʳ ⁻¹ ∘ᵢ associator + ≈ associator ⊗ᵢ idᵢ ∘ᵢ unitorʳ ⁻¹ ⟩ - square₂ = lift-square′ unitorʳ-commute-to + square₂ = ⌞ unitorʳ-commute-to ⌟ - coherence₂ : C.id {X} ⊗₁ unitorʳ.from {Y} ∘ associator.from ≈ unitorʳ.from - coherence₂ = project-triangle coherence-iso₂ + coherence₂ : [ (X ⊗₀ Y) ⊗₀ unit ⇒ X ⊗₀ Y ]⟨ + α⇒ ⇒⟨ X ⊗₀ (Y ⊗₀ unit) ⟩ + id ⊗₁ ρ⇒ + ≈ ρ⇒ + ⟩ + coherence₂ = from-≈ coherence-iso₂ + + coherence-inv₂ : [ X ⊗₀ Y ⇒ (X ⊗₀ Y) ⊗₀ unit ]⟨ + id ⊗₁ ρ⇐ ⇒⟨ X ⊗₀ (Y ⊗₀ unit) ⟩ + α⇐ + ≈ ρ⇐ + ⟩ + coherence-inv₂ = to-≈ coherence-iso₂ -- A third coherence condition (Lemma 2.3) - coherence₃ : unitorˡ.from {unit} ≈ unitorʳ.from + coherence₃ : [ unit ⊗₀ unit ⇒ unit ]⟨ λ⇒ ≈ ρ⇒ ⟩ coherence₃ = push-eq unitorˡ-naturalIsomorphism (begin - C.id ⊗₁ unitorˡ.from - ≈˘⟨ cancelʳ associator.isoʳ ⟩ - (C.id ⊗₁ unitorˡ.from ∘ associator.from) ∘ associator.to - ≈⟨ triangle ⟩∘⟨refl ⟩ - unitorʳ.from ⊗₁ C.id ∘ associator.to - ≈⟨ unitor-coherenceʳ ⟩∘⟨refl ⟩ - unitorʳ.from ∘ associator.to - ≈˘⟨ coherence₂ ⟩∘⟨refl ⟩ - (C.id ⊗₁ unitorʳ.from ∘ associator.from) ∘ associator.to - ≈⟨ cancelʳ associator.isoʳ ⟩ - C.id ⊗₁ unitorʳ.from - ∎) + C.id ⊗₁ λ⇒ ≈˘⟨ cancelʳ associator.isoʳ ⟩ + (C.id ⊗₁ λ⇒ ∘ α⇒) ∘ α⇐ ≈⟨ triangle ⟩∘⟨refl ⟩ + ρ⇒ ⊗₁ C.id ∘ α⇐ ≈⟨ unitor-coherenceʳ ⟩∘⟨refl ⟩ + ρ⇒ ∘ α⇐ ≈˘⟨ coherence₂ ⟩∘⟨refl ⟩ + (C.id ⊗₁ ρ⇒ ∘ α⇒) ∘ α⇐ ≈⟨ cancelʳ associator.isoʳ ⟩ + C.id ⊗₁ ρ⇒ ∎) where open MR C hiding (push-eq) open C.HomReasoning - coherence-iso₃ : [ unit ⊗₀ unit ⇒ unit ]⟨ unitorˡ ≈ unitorʳ ⟩ + coherence-iso₃ : [ unit ⊗₀ unit ≅ unit ]⟨ unitorˡ ≈ unitorʳ ⟩ coherence-iso₃ = ⌞ coherence₃ ⌟ -open Kelly's using (coherence₁; coherence-iso₁; coherence₂; coherence-iso₂) public + coherence-inv₃ : [ unit ⇒ unit ⊗₀ unit ]⟨ λ⇐ ≈ ρ⇐ ⟩ + coherence-inv₃ = to-≈ coherence-iso₃ + +open Kelly's public using + ( coherence₁; coherence-iso₁; coherence-inv₁ + ; coherence₂; coherence-iso₂; coherence-inv₂ + ; coherence₃; coherence-iso₃; coherence-inv₃ + ) diff --git a/src/Categories/Category/Monoidal/Utilities.agda b/src/Categories/Category/Monoidal/Utilities.agda index e3d226513..0487d1136 100644 --- a/src/Categories/Category/Monoidal/Utilities.agda +++ b/src/Categories/Category/Monoidal/Utilities.agda @@ -10,6 +10,7 @@ open import Function using (_$_) open import Data.Product using (_×_; _,_; curry′) open import Categories.Category.Product +import Categories.Category.Construction.Core as Core open import Categories.Functor renaming (id to idF) open import Categories.Functor.Bifunctor using (Bifunctor; appˡ; appʳ) open import Categories.Functor.Properties using ([_]-resp-≅) @@ -17,18 +18,17 @@ open import Categories.NaturalTransformation renaming (id to idN) open import Categories.NaturalTransformation.NaturalIsomorphism hiding (unitorˡ; unitorʳ; associator; _≃_) -infixr 10 _⊗ᵢ_ - -open import Categories.Morphism C using (_≅_; module ≅) -open import Categories.Morphism.IsoEquiv C using (_≃_; ⌞_⌟) -open import Categories.Morphism.Isomorphism C using (_∘ᵢ_; lift-triangle′; lift-pentagon′) +--open import Categories.Morphism C using (_≅_) +--open import Categories.Morphism.IsoEquiv C using (_≃_; ⌞_⌟) +open import Categories.Morphism.Isomorphism C using (lift-triangle′; lift-pentagon′) open import Categories.Morphism.Reasoning C private module C = Category C -open C hiding (id; identityˡ; identityʳ; assoc) +open C hiding (identityˡ; identityʳ; assoc) open Commutation C +open Core.Shorthands C private variable @@ -113,6 +113,8 @@ module unitorˡ-natural = NaturalIsomorphism unitorˡ-naturalIsomorphism module unitorʳ-natural = NaturalIsomorphism unitorʳ-naturalIsomorphism module associator-natural = NaturalIsomorphism associator-naturalIsomorphism +infixr 10 _⊗ᵢ_ + _⊗ᵢ_ : X ≅ Y → Z ≅ W → X ⊗₀ Z ≅ Y ⊗₀ W f ⊗ᵢ g = [ ⊗ ]-resp-≅ record { from = from f , from g @@ -122,15 +124,20 @@ f ⊗ᵢ g = [ ⊗ ]-resp-≅ record ; isoʳ = isoʳ f , isoʳ g } } - where open _≅_ -triangle-iso : ≅.refl ⊗ᵢ unitorˡ ∘ᵢ associator ≃ unitorʳ {X} ⊗ᵢ ≅.refl {Y} -triangle-iso = lift-triangle′ triangle +triangle-iso : idᵢ ⊗ᵢ unitorˡ ∘ᵢ associator ≈ᵢ unitorʳ {X} ⊗ᵢ idᵢ {Y} +triangle-iso = ⌞ triangle ⌟ + +triangle-inv : α⇐ ∘ id ⊗₁ λ⇐ ≈ ρ⇐ {X} ⊗₁ id {Y} +triangle-inv = to-≈ triangle-iso pentagon-iso : - ≅.refl ⊗ᵢ associator ∘ᵢ associator ∘ᵢ associator {X} {Y} {Z} ⊗ᵢ ≅.refl {W} - ≃ associator ∘ᵢ associator -pentagon-iso = lift-pentagon′ pentagon + idᵢ ⊗ᵢ associator ∘ᵢ associator ∘ᵢ associator {X} {Y} {Z} ⊗ᵢ idᵢ {W} + ≈ᵢ associator ∘ᵢ associator +pentagon-iso = ⌞ pentagon ⌟ + +pentagon-inv : (α⇐ {X} {Y} {Z} ⊗₁ id {W} ∘ α⇐) ∘ id ⊗₁ α⇐ ≈ α⇐ ∘ α⇐ +pentagon-inv = to-≈ pentagon-iso -refl⊗refl≃refl : ≅.refl {A} ⊗ᵢ ≅.refl {B} ≃ ≅.refl +refl⊗refl≃refl : idᵢ {A} ⊗ᵢ idᵢ {B} ≈ᵢ idᵢ refl⊗refl≃refl = ⌞ ⊗.identity ⌟ diff --git a/src/Categories/Enriched/Category/Underlying.agda b/src/Categories/Enriched/Category/Underlying.agda index ea57a46c0..f1d37b9fa 100644 --- a/src/Categories/Enriched/Category/Underlying.agda +++ b/src/Categories/Enriched/Category/Underlying.agda @@ -15,12 +15,10 @@ open import Categories.Category.Monoidal.Properties M using (module Kelly's) open import Categories.Category.Monoidal.Reasoning M open import Categories.Category.Monoidal.Utilities M using (module Shorthands) open import Categories.Morphism.Reasoning V -import Categories.Morphism.IsoEquiv V as IsoEquiv open Setoid-Category V renaming (Obj to ObjV; id to idV) open Monoidal M open Shorthands -open IsoEquiv._≃_ -- A V-category C does not have morphisms of its own, but the -- collection of V-morphisms from the monoidal unit into the @@ -40,7 +38,7 @@ Underlying C = categoryHelper (record ⊚ ∘ ((⊚ ∘ h ⊗₁ g) ∘ λ⇐) ⊗₁ f ∘ λ⇐ ≈⟨ refl⟩∘⟨ pushˡ split₁ʳ ⟩ ⊚ ∘ (⊚ ∘ h ⊗₁ g) ⊗₁ f ∘ (λ⇐ ⊗₁ idV) ∘ λ⇐ ≈⟨ pullˡ ⊚-assoc-var ⟩ (⊚ ∘ h ⊗₁ (⊚ ∘ g ⊗₁ f) ∘ α⇒) ∘ (λ⇐ ⊗₁ idV) ∘ λ⇐ ≈˘⟨ pushˡ (pushʳ (pushʳ - (switch-tofromˡ associator (to-≈ Kelly's.coherence-iso₁)))) ⟩ + (switch-tofromˡ associator Kelly's.coherence-inv₁))) ⟩ (⊚ ∘ h ⊗₁ (⊚ ∘ g ⊗₁ f) ∘ λ⇐) ∘ λ⇐ ≈⟨ pullʳ (pullʳ unitorˡ-commute-to) ⟩ ⊚ ∘ h ⊗₁ (⊚ ∘ g ⊗₁ f) ∘ idV ⊗₁ λ⇐ ∘ λ⇐ ≈˘⟨ refl⟩∘⟨ pushˡ split₂ʳ ⟩ ⊚ ∘ h ⊗₁ ((⊚ ∘ g ⊗₁ f) ∘ λ⇐) ∘ λ⇐ ≈⟨ refl⟩∘⟨ refl⟩⊗⟨ assoc ⟩∘⟨refl ⟩ diff --git a/src/Categories/Enriched/NaturalTransformation.agda b/src/Categories/Enriched/NaturalTransformation.agda index 933f5edc0..a83e51666 100644 --- a/src/Categories/Enriched/NaturalTransformation.agda +++ b/src/Categories/Enriched/NaturalTransformation.agda @@ -17,7 +17,6 @@ open import Categories.Enriched.Functor M using (Functor; UnderlyingFunctor; _ renaming (id to idF) open import Categories.Morphism.Reasoning V using (pushˡ; pullˡ; cancelʳ; pullʳ; pushʳ; switch-tofromˡ; extendˡ; extendʳ) -import Categories.Morphism.IsoEquiv V as IsoEquiv open import Categories.NaturalTransformation using (ntHelper) renaming (NaturalTransformation to Setoid-NT) @@ -64,7 +63,6 @@ module _ {c d : Level} {C : Category c} {D : Category d} where open NaturalTransformation open D hiding (id) - open IsoEquiv._≃_ id : ∀ {F : Functor C D} → NaturalTransformation F F id {F} = record @@ -108,7 +106,7 @@ module _ {c d : Level} {C : Category c} {D : Category d} where ⊚ ∘ ((⊚ ∘ H.₁ ⊗₁ α [ X ]) ⊗₁ β [ X ] ∘ ρ⇐ ⊗₁ idV) ∘ ρ⇐ ≈⟨ pullˡ (pullˡ ⊚-assoc-var) ⟩ ((⊚ ∘ H.₁ ⊗₁ (⊚ ∘ α [ X ] ⊗₁ β [ X ]) ∘ α⇒) ∘ ρ⇐ ⊗₁ idV) ∘ ρ⇐ - ≈˘⟨ pushʳ (pushʳ (switch-tofromˡ associator (to-≈ triangle-iso))) ⟩∘⟨refl ⟩ + ≈˘⟨ pushʳ (pushʳ (switch-tofromˡ associator triangle-inv)) ⟩∘⟨refl ⟩ (⊚ ∘ H.₁ ⊗₁ (⊚ ∘ α [ X ] ⊗₁ β [ X ]) ∘ idV ⊗₁ λ⇐) ∘ ρ⇐ ≈˘⟨ pushʳ (split₂ʳ ⟩∘⟨refl) ⟩ ⊚ ∘ H.₁ ⊗₁ ((⊚ ∘ α [ X ] ⊗₁ β [ X ]) ∘ λ⇐) ∘ ρ⇐ @@ -133,7 +131,7 @@ module _ {c d : Level} {C : Category c} {D : Category d} where ⊚ ∘ ((⊚ ∘ f ⊗₁ g) ⊗₁ h ∘ λ⇐ ⊗₁ idV) ∘ i ≈⟨ pullˡ (pullˡ ⊚-assoc-var) ⟩ ((⊚ ∘ f ⊗₁ (⊚ ∘ g ⊗₁ h) ∘ α⇒) ∘ λ⇐ ⊗₁ idV) ∘ i - ≈˘⟨ pushʳ (pushʳ (switch-tofromˡ associator (to-≈ Kelly's.coherence-iso₁))) ⟩∘⟨refl ⟩ + ≈˘⟨ pushʳ (pushʳ (switch-tofromˡ associator Kelly's.coherence-inv₁)) ⟩∘⟨refl ⟩ (⊚ ∘ f ⊗₁ (⊚ ∘ g ⊗₁ h) ∘ λ⇐) ∘ i ≈⟨ pullʳ (pullʳ unitorˡ-commute-to) ⟩ ⊚ ∘ f ⊗₁ (⊚ ∘ g ⊗₁ h) ∘ idV ⊗₁ i ∘ λ⇐ @@ -161,7 +159,7 @@ module _ {c d : Level} {C : Category c} {D : Category d} where ⊚ ∘ (α [ Y ] ⊗₁ F.₁ ∘ λ⇐) ∘ f ≈⟨ extendʳ (commute α) ⟩ ⊚ ∘ (G.₁ ⊗₁ α [ X ] ∘ ρ⇐) ∘ f ≈⟨ refl⟩∘⟨ extendˡ unitorʳ-commute-to ⟩ ⊚ ∘ (G.₁ ⊗₁ α [ X ] ∘ f ⊗₁ idV) ∘ ρ⇐ ≈˘⟨ refl⟩∘⟨ split₁ʳ ⟩∘⟨refl ⟩ - ⊚ ∘ (G.₁ ∘ f) ⊗₁ α [ X ] ∘ ρ⇐ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ to-≈ Kelly's.coherence-iso₃ ⟩ + ⊚ ∘ (G.₁ ∘ f) ⊗₁ α [ X ] ∘ ρ⇐ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ Kelly's.coherence-inv₃ ⟩ ⊚ ∘ (G.₁ ∘ f) ⊗₁ α [ X ] ∘ λ⇐ ∎ }) where diff --git a/src/Categories/Functor/Properties.agda b/src/Categories/Functor/Properties.agda index 0f9d01f2d..07df576f6 100644 --- a/src/Categories/Functor/Properties.agda +++ b/src/Categories/Functor/Properties.agda @@ -11,13 +11,15 @@ open import Relation.Binary using (_Preserves_⟶_) open import Relation.Nullary open import Categories.Category +open import Categories.Category.Construction.Core using (module Shorthands) open import Categories.Functor import Categories.Morphism as Morphism import Categories.Morphism.Reasoning as Reas open import Categories.Morphism.IsoEquiv as IsoEquiv -open import Categories.Morphism.Isomorphism open import Categories.Morphism.Notation +open Shorthands using (_∘ᵢ_) + private variable o ℓ e o′ ℓ′ e′ : Level diff --git a/src/Categories/Morphism/Isomorphism.agda b/src/Categories/Morphism/Isomorphism.agda index 65f3a88c4..3535852b8 100644 --- a/src/Categories/Morphism/Isomorphism.agda +++ b/src/Categories/Morphism/Isomorphism.agda @@ -23,10 +23,9 @@ import Categories.Morphism.Properties as MorphismProps import Categories.Morphism.IsoEquiv as IsoEquiv import Categories.Category.Construction.Path as Path -open Core 𝒞 using (Core; Core-isGroupoid; CoreGroupoid) +open Core 𝒞 using (Core; Core-isGroupoid; CoreGroupoid; module Shorthands) open Morphism 𝒞 open MorphismProps 𝒞 -open IsoEquiv 𝒞 using (_≃_; ⌞_⌟; ≃-sym) open Path 𝒞 import Categories.Morphism.Reasoning as MR @@ -36,16 +35,15 @@ open Definitions 𝒞 private module MCore where - open IsGroupoid Core-isGroupoid public open GroupoidProps CoreGroupoid public - open MorphismProps Core public - open Morphism Core public - open Path Core public + open MorphismProps Core public + open Morphism Core public + open Path Core public variable A B C D E F : Obj -open MCore using () renaming (_∘_ to _∘ᵢ_) public +open Shorthands hiding (_≅_) CommutativeIso = IsGroupoid.CommutativeSquare Core-isGroupoid @@ -90,23 +88,23 @@ module _ where ; iso = λ {_ _ f⁺} → record { isoˡ = isoˡ′ f⁺ ; isoʳ = isoʳ′ f⁺ } } where - open MCore.HomReasoning + open HomReasoningᵢ - isoˡ′ : (f⁺ : A [ _≅_ ]⁺ B) → ∘ᵢ-tc (reverse f⁺) ∘ᵢ ∘ᵢ-tc f⁺ ≃ ≅.refl + isoˡ′ : (f⁺ : A [ _≅_ ]⁺ B) → ∘ᵢ-tc (reverse f⁺) ∘ᵢ ∘ᵢ-tc f⁺ ≈ᵢ ≅.refl isoˡ′ f⁺ = begin ∘ᵢ-tc (reverse f⁺) ∘ᵢ ∘ᵢ-tc f⁺ ≡⟨ ≡.cong (_∘ᵢ ∘ᵢ-tc f⁺) (reverse⇒≅-sym f⁺) ⟩ ≅.sym (∘ᵢ-tc f⁺) ∘ᵢ ∘ᵢ-tc f⁺ - ≈⟨ MCore.iso.isoˡ ⟩ + ≈⟨ ⁻¹-iso.isoˡ ⟩ ≅.refl ∎ - isoʳ′ : (f⁺ : A [ _≅_ ]⁺ B) → ∘ᵢ-tc f⁺ ∘ᵢ ∘ᵢ-tc (reverse f⁺) ≃ ≅.refl + isoʳ′ : (f⁺ : A [ _≅_ ]⁺ B) → ∘ᵢ-tc f⁺ ∘ᵢ ∘ᵢ-tc (reverse f⁺) ≈ᵢ ≅.refl isoʳ′ f⁺ = begin ∘ᵢ-tc f⁺ ∘ᵢ ∘ᵢ-tc (reverse f⁺) ≡⟨ ≡.cong (∘ᵢ-tc f⁺ ∘ᵢ_) (reverse⇒≅-sym f⁺) ⟩ ∘ᵢ-tc f⁺ ∘ᵢ ≅.sym (∘ᵢ-tc f⁺) - ≈⟨ MCore.iso.isoʳ ⟩ + ≈⟨ ⁻¹-iso.isoʳ ⟩ ≅.refl ∎ @@ -117,7 +115,7 @@ module _ where ≅*⇒⇒*-cong : ≅⁺⇒⇒⁺ {A} {B} Preserves _≃⁺_ ⟶ _≈⁺_ ≅*⇒⇒*-cong {_} {_} {f⁺} {g⁺} f⁺≃⁺g⁺ = begin ∘-tc (≅⁺⇒⇒⁺ f⁺) ≡˘⟨ from-∘ᵢ-tc f⁺ ⟩ - from (∘ᵢ-tc f⁺) ≈⟨ _≃_.from-≈ f⁺≃⁺g⁺ ⟩ + from (∘ᵢ-tc f⁺) ≈⟨ from-≈ f⁺≃⁺g⁺ ⟩ from (∘ᵢ-tc g⁺) ≡⟨ from-∘ᵢ-tc g⁺ ⟩ ∘-tc (≅⁺⇒⇒⁺ g⁺) ∎ where open HomReasoning @@ -129,7 +127,7 @@ module _ where ∘ᵢ-tc g⁺ ∘ᵢ (∘ᵢ-tc f⁺ ∘ᵢ ∘ᵢ-tc (reverse f⁺)) ≈⟨ pullˡ eq ⟩ ∘ᵢ-tc h⁺ ∘ᵢ ∘ᵢ-tc (reverse f⁺) ∎ where - open MCore.HomReasoning + open HomReasoningᵢ open MR Core module I {A B} (f⁺ : A [ _≅_ ]⁺ B) = Morphism.Iso (IsGroupoid.iso TransitiveClosure-groupoid {f = f⁺}) @@ -180,64 +178,63 @@ module _ where -- projecting isomorphism commutations to morphism commutations - project-triangle : {g : A ≅ B} {f : C ≅ A} {h : C ≅ B} → g ∘ᵢ f ≃ h → from g ∘ from f ≈ from h - project-triangle = _≃_.from-≈ + project-triangle : {g : A ≅ B} {f : C ≅ A} {h : C ≅ B} → g ∘ᵢ f ≈ᵢ h → from g ∘ from f ≈ from h + project-triangle = from-≈ - project-square : {g : A ≅ B} {f : C ≅ A} {i : D ≅ B} {h : C ≅ D} → g ∘ᵢ f ≃ i ∘ᵢ h → from g ∘ from f ≈ from i ∘ from h - project-square = _≃_.from-≈ + project-square : {g : A ≅ B} {f : C ≅ A} {i : D ≅ B} {h : C ≅ D} → g ∘ᵢ f ≈ᵢ i ∘ᵢ h → from g ∘ from f ≈ from i ∘ from h + project-square = from-≈ -- direct lifting from morphism commutations to isomorphism commutations - lift-triangle′ : {f : A ≅ B} {g : C ≅ A} {h : C ≅ B} → from f ∘ from g ≈ from h → f ∘ᵢ g ≃ h + lift-triangle′ : {f : A ≅ B} {g : C ≅ A} {h : C ≅ B} → from f ∘ from g ≈ from h → f ∘ᵢ g ≈ᵢ h lift-triangle′ = ⌞_⌟ - lift-square′ : {f : A ≅ B} {g : C ≅ A} {h : D ≅ B} {i : C ≅ D} → from f ∘ from g ≈ from h ∘ from i → f ∘ᵢ g ≃ h ∘ᵢ i + lift-square′ : {f : A ≅ B} {g : C ≅ A} {h : D ≅ B} {i : C ≅ D} → from f ∘ from g ≈ from h ∘ from i → f ∘ᵢ g ≈ᵢ h ∘ᵢ i lift-square′ = ⌞_⌟ lift-pentagon′ : {f : A ≅ B} {g : C ≅ A} {h : D ≅ C} {i : E ≅ B} {j : D ≅ E} → - from f ∘ from g ∘ from h ≈ from i ∘ from j → f ∘ᵢ g ∘ᵢ h ≃ i ∘ᵢ j + from f ∘ from g ∘ from h ≈ from i ∘ from j → f ∘ᵢ g ∘ᵢ h ≈ᵢ i ∘ᵢ j lift-pentagon′ = ⌞_⌟ open MR Core - open MCore using (_⁻¹) - open MCore.HomReasoning + open HomReasoningᵢ open MR.GroupoidR _ Core-isGroupoid squares×≃⇒≃ : {f f′ : A ≅ B} {g : A ≅ C} {h : B ≅ D} {i i′ : C ≅ D} → - CommutativeIso f g h i → CommutativeIso f′ g h i′ → i ≃ i′ → f ≃ f′ + CommutativeIso f g h i → CommutativeIso f′ g h i′ → i ≈ᵢ i′ → f ≈ᵢ f′ squares×≃⇒≃ sq₁ sq₂ eq = MCore.isos×≈⇒≈ eq helper₁ (MCore.≅.sym helper₂) sq₁ sq₂ where - helper₁ = record { iso = MCore.iso } - helper₂ = record { iso = MCore.iso } + helper₁ = record { iso = ⁻¹-iso } + helper₂ = record { iso = ⁻¹-iso } -- imagine a triangle prism, if all the sides and the top face commute, the bottom face commute. triangle-prism : {i′ : A ≅ B} {f′ : C ≅ A} {h′ : C ≅ B} {i : D ≅ E} {j : D ≅ A} {k : E ≅ B} {f : F ≅ D} {g : F ≅ C} {h : F ≅ E} → - i′ ∘ᵢ f′ ≃ h′ → + i′ ∘ᵢ f′ ≈ᵢ h′ → CommutativeIso i j k i′ → CommutativeIso f g j f′ → CommutativeIso h g k h′ → - i ∘ᵢ f ≃ h + i ∘ᵢ f ≈ᵢ h triangle-prism {i′ = i′} {f′} {_} {i} {_} {k} {f} {g} {_} eq sq₁ sq₂ sq₃ = squares×≃⇒≃ glued sq₃ eq where glued : CommutativeIso (i ∘ᵢ f) g k (i′ ∘ᵢ f′) - glued = ≃-sym (glue (≃-sym sq₁) (≃-sym sq₂)) + glued = ⟺ (glue (⟺ sq₁) (⟺ sq₂)) elim-triangleˡ : {f : A ≅ B} {g : C ≅ A} {h : D ≅ C} {i : D ≅ B} {j : D ≅ A} → - f ∘ᵢ g ∘ᵢ h ≃ i → f ∘ᵢ j ≃ i → g ∘ᵢ h ≃ j + f ∘ᵢ g ∘ᵢ h ≈ᵢ i → f ∘ᵢ j ≈ᵢ i → g ∘ᵢ h ≈ᵢ j elim-triangleˡ perim tri = MCore.mono _ _ (perim ○ ⟺ tri) elim-triangleˡ′ : {f : A ≅ B} {g : C ≅ A} {h : D ≅ C} {i : D ≅ B} {j : C ≅ B} → - f ∘ᵢ g ∘ᵢ h ≃ i → j ∘ᵢ h ≃ i → f ∘ᵢ g ≃ j + f ∘ᵢ g ∘ᵢ h ≈ᵢ i → j ∘ᵢ h ≈ᵢ i → f ∘ᵢ g ≈ᵢ j elim-triangleˡ′ {f = f} {g} {h} {i} {j} perim tri = MCore.epi _ _ ( begin - (f ∘ᵢ g) ∘ᵢ h ≈⟨ MCore.assoc ⟩ + (f ∘ᵢ g) ∘ᵢ h ≈⟨ ⌞ assoc ⌟ ⟩ f ∘ᵢ g ∘ᵢ h ≈⟨ perim ⟩ i ≈˘⟨ tri ⟩ j ∘ᵢ h ∎ ) cut-squareʳ : {g : A ≅ B} {f : A ≅ C} {h : B ≅ D} {i : C ≅ D} {j : B ≅ C} → - CommutativeIso g f h i → i ∘ᵢ j ≃ h → j ∘ᵢ g ≃ f + CommutativeIso g f h i → i ∘ᵢ j ≈ᵢ h → j ∘ᵢ g ≈ᵢ f cut-squareʳ {g = g} {f = f} {h = h} {i = i} {j = j} sq tri = begin j ∘ᵢ g ≈⟨ switch-fromtoˡ′ {f = i} {h = j} {k = h} tri ⟩∘⟨refl ⟩ - (i ⁻¹ ∘ᵢ h) ∘ᵢ g ≈⟨ MCore.assoc ⟩ - i ⁻¹ ∘ᵢ h ∘ᵢ g ≈˘⟨ switch-fromtoˡ′ {f = i} {h = f} {k = h ∘ᵢ g} (≃-sym sq) ⟩ + (i ⁻¹ ∘ᵢ h) ∘ᵢ g ≈⟨ ⌞ assoc ⌟ ⟩ + i ⁻¹ ∘ᵢ h ∘ᵢ g ≈˘⟨ switch-fromtoˡ′ {f = i} {h = f} {k = h ∘ᵢ g} (⟺ sq) ⟩ f ∎ diff --git a/src/Categories/Pseudofunctor/Hom.agda b/src/Categories/Pseudofunctor/Hom.agda index 3fd329010..8cdbae2a9 100644 --- a/src/Categories/Pseudofunctor/Hom.agda +++ b/src/Categories/Pseudofunctor/Hom.agda @@ -11,6 +11,7 @@ open import Data.Product using (_,_) import Categories.Bicategory.Extras as BicategoryExtras open import Categories.Bicategory.Opposite using (op) open import Categories.Bicategory.Instance.Cats using (Cats) +import Categories.Category.Construction.Core as Core open import Categories.Functor.Bifunctor.Properties open import Categories.Pseudofunctor using (Pseudofunctor) import Categories.Morphism.Reasoning as MorphismReasoning @@ -24,9 +25,8 @@ open Shorthands open hom.HomReasoning private module MR {A} {B} where - open Morphism (hom A B) public using (_≅_; module ≅) + open Core.Shorthands (hom A B) public open MorphismReasoning (hom A B) public - open _≅_ public open MR @@ -93,7 +93,7 @@ Hom[ A ,-] = record ρ⇒ ◁ g ∘ᵥ α⇐ ∘ᵥ f ▷ λ⇐ ∘ᵥ id₂ ≈⟨ pushʳ (refl⟩∘⟨ hom.identityʳ) ⟩ (ρ⇒ ◁ g ∘ᵥ α⇐) ∘ᵥ f ▷ λ⇐ - ≈˘⟨ switch-tofromʳ (≅.sym associator) triangle ⟩∘⟨refl ⟩ + ≈˘⟨ switch-tofromʳ (associator ⁻¹) triangle ⟩∘⟨refl ⟩ f ▷ λ⇒ ∘ᵥ f ▷ λ⇐ ≈⟨ isoʳ (f ▷ᵢ unitorˡ) ⟩ id₂ @@ -104,7 +104,7 @@ Hom[ A ,-] = record α⇒ ◁ e ∘ᵥ α⇐ ∘ᵥ id₂ ∘ᵥ α⇐ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ hom.identityˡ ⟩ α⇒ ◁ e ∘ᵥ α⇐ ∘ᵥ α⇐ - ≈˘⟨ switch-fromtoˡ (≅.sym (associator ◁ᵢ e)) + ≈˘⟨ switch-fromtoˡ ((associator ◁ᵢ e) ⁻¹) (hom.sym-assoc ○ pentagon-inv) ⟩ α⇐ ∘ᵥ h ▷ α⇐ ≈˘⟨ pushʳ hom.identityʳ ○ hom.identityʳ ⟩