Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Big cleanup: factor out common shorthand notation #306

Merged
merged 1 commit into from
Aug 25, 2021
Merged

Big cleanup: factor out common shorthand notation #306

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
54 changes: 25 additions & 29 deletions src/Categories/Bicategory/Extras.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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ᵢ
Expand Down Expand Up @@ -170,7 +166,7 @@ _⟩⊚⟨refl = ⊚-resp-≈ˡ
α ∘ᵥ λ⇒ ∎

▷-∘ᵥ-λ⇐ : (id₁ ▷ α) ∘ᵥ λ⇐ ≈ λ⇐ ∘ᵥ α
▷-∘ᵥ-λ⇐ = conjugate-to (≅.sym unitorˡ) (≅.sym unitorˡ) λ⇒-∘ᵥ-▷
▷-∘ᵥ-λ⇐ = conjugate-to (unitorˡ ⁻¹) (unitorˡ ⁻¹) λ⇒-∘ᵥ-▷

ρ⇒-∘ᵥ-◁ : ρ⇒ ∘ᵥ (α ◁ id₁) ≈ α ∘ᵥ ρ⇒
ρ⇒-∘ᵥ-◁ {α = α} = begin
Expand All @@ -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
Expand All @@ -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

Expand Down
34 changes: 32 additions & 2 deletions src/Categories/Category/Construction/Core.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 _≃_
Expand Down Expand Up @@ -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
)
121 changes: 67 additions & 54 deletions src/Categories/Category/Monoidal/Braided/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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)
Loading