Merge pull request #306 from sstucki/refactor-shorthand

Big cleanup: factor out common shorthand notation

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,44 +26,50 @@ 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})
 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
 

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
+    )

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)