{-# OPTIONS --without-K --safe #-}
open import Categories.Category
open import Categories.Category.Monoidal.Core using (Monoidal)
module Categories.Category.Monoidal.Braided {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) where
open import Level
open import Data.Product using (Σ; _,_)
open import Categories.Functor.Bifunctor
open import Categories.NaturalTransformation.NaturalIsomorphism
open Category C
open Commutation C
private
variable
X Y Z : Obj
record Braided : Set (levelOfTerm M) where
open Monoidal M public
field
braiding : NaturalIsomorphism ⊗ (flip-bifunctor ⊗)
module braiding = NaturalIsomorphism braiding
private
B : ∀ {X Y} → X ⊗₀ Y ⇒ Y ⊗₀ X
B {X} {Y} = braiding.⇒.η (X , Y)
field
hexagon₁ : [ (X ⊗₀ Y) ⊗₀ Z ⇒ Y ⊗₀ Z ⊗₀ X ]⟨
B ⊗₁ id ⇒⟨ (Y ⊗₀ X) ⊗₀ Z ⟩
associator.from ⇒⟨ Y ⊗₀ X ⊗₀ Z ⟩
id ⊗₁ B
≈ associator.from ⇒⟨ X ⊗₀ Y ⊗₀ Z ⟩
B ⇒⟨ (Y ⊗₀ Z) ⊗₀ X ⟩
associator.from
⟩
hexagon₂ : [ X ⊗₀ Y ⊗₀ Z ⇒ (Z ⊗₀ X) ⊗₀ Y ]⟨
id ⊗₁ B ⇒⟨ X ⊗₀ Z ⊗₀ Y ⟩
(associator.to ⇒⟨ (X ⊗₀ Z) ⊗₀ Y ⟩
B ⊗₁ id)
≈ associator.to ⇒⟨ (X ⊗₀ Y) ⊗₀ Z ⟩
(B ⇒⟨ Z ⊗₀ X ⊗₀ Y ⟩
associator.to)
⟩