{-# 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

-- braided monoidal category
-- it has a braiding natural isomorphism has two hexagon identities.
-- these two identities are directly expressed in the morphism level.
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)