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