open import Cat.Functor.Naturality
open import Cat.Functor.Bifunctor
open import Cat.Monoidal.Base
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Functor.Reasoning
import Cat.Reasoning

open _=>_

module Cat.Monoidal.Braided {o ℓ}
  {C : Precategory o ℓ} (Cᵐ : Monoidal-category C)
  where

Braided and symmetric monoidal categories🔗

open Cat.Reasoning C
open Monoidal Cᵐ

A braided monoidal category is a monoidal category equipped with a braiding: a natural isomorphism $\beta :A\otimes B\cong B\otimes A$ satisfying some coherence conditions explained below.

record Braided-monoidal : Type (o ⊔ ℓ) where
  field
    braiding : -⊗- ≅ⁿ Flip -⊗-

  module β→ = _=>_ (braiding .Isoⁿ.to)
  module β← = _=>_ (braiding .Isoⁿ.from)

  β→ : ∀ {A B} → Hom (A ⊗ B) (B ⊗ A)
  β→ = braiding .Isoⁿ.to ._=>_.η _

  β← : ∀ {A B} → Hom (A ⊗ B) (B ⊗ A)
  β← = braiding .Isoⁿ.from ._=>_.η _

  β≅ : ∀ {A B} → A ⊗ B ≅ B ⊗ A
  β≅ = isoⁿ→iso braiding _

The name “braiding” is meant to suggest that flipping $A\otimes B$ twice in the same direction is not necessarily trivial, which we may represent using braid diagrams like this one:

The above diagram represents the morphism $\beta \circ \beta :A\otimes B\to A\otimes B\text{;}$ if the braiding is symmetric in the sense that this morphism is an identity (that is, if we can “untangle” the braid above by pulling the strands through each other), then we have a symmetric monoidal category, and it does not matter which direction we braid in.

Our definition of a braided monoidal category is not complete yet: we also require coherences saying that the braiding interacts nicely with the associator, in the sense that the following hexagon commutes:

  field
    braiding-α→ : ∀ {A B C}
      → (id ⊗₁ β→) ∘ α→ B A C ∘ (β→ ⊗₁ id) ≡ α→ B C A ∘ β→ ∘ α→ A B C

If the braiding is symmetric, then we’re done. However, in general we also need a second hexagon expressing the same condition with the “backwards” braiding (or, equivalently, with the braiding and the backwards associator), which might not be the same as the forward braiding.

  field
    unbraiding-α→ : ∀ {A B C}
      → (id ⊗₁ β←) ∘ α→ B A C ∘ (β← ⊗₁ id) ≡ α→ B C A ∘ β← ∘ α→ A B C

  β←-α← : ∀ {A B C}
    → (β← ⊗₁ id) ∘ α← B A C ∘ (id ⊗₁ β←) ≡ α← A B C ∘ β← ∘ α← B C A
  β←-α← = inverse-unique refl refl
    (◀.F-map-iso β≅ ∘Iso α≅ ∘Iso ▶.F-map-iso β≅)
    (α≅ ∘Iso β≅ ∘Iso α≅)
    (sym (assoc _ _ _) ·· braiding-α→ ·· assoc _ _ _)

A symmetric monoidal category simply bundles up a braided monoidal category with the property that its braiding is symmetric.

is-symmetric-braiding : -⊗- ≅ⁿ Flip -⊗- → Type (o ⊔ ℓ)
is-symmetric-braiding braiding = ∀ {A B} → β→ ∘ β→ {A} {B} ≡ id
  where
    β→ : ∀ {A B} → Hom (A ⊗ B) (B ⊗ A)
    β→ = braiding .Isoⁿ.to ._=>_.η _

record Symmetric-monoidal : Type (o ⊔ ℓ) where
  field
    Cᵇ : Braided-monoidal

  open Braided-monoidal Cᵇ hiding (β≅) public

  field
    has-is-symmetric : is-symmetric-braiding braiding

  β≅ : ∀ {A B} → A ⊗ B ≅ B ⊗ A
  β≅ = make-iso β→ β→ has-is-symmetric has-is-symmetric

In order to construct a symmetric monoidal category, as we discussed above, it is sufficient to give one of the hexagons: the other one follows by uniqueness of inverses.

record make-symmetric-monoidal : Type (o ⊔ ℓ) where
  field
    has-braiding : -⊗- ≅ⁿ Flip -⊗-
    symmetric : is-symmetric-braiding has-braiding

  β→ : ∀ {A B} → Hom (A ⊗ B) (B ⊗ A)
  β→ = has-braiding .Isoⁿ.to ._=>_.η _
  β← : ∀ {A B} → Hom (A ⊗ B) (B ⊗ A)
  β← = has-braiding .Isoⁿ.from ._=>_.η _

  β→≡β← : Path (∀ {A B} → Hom (A ⊗ B) (B ⊗ A)) β→ β←
  β→≡β← = ext λ {_} {_} → inverse-unique refl refl
    (make-iso β→ β→ symmetric symmetric)
    (isoⁿ→iso has-braiding _)
    refl

  open Braided-monoidal hiding (β→)
  open Symmetric-monoidal hiding (β→)

  field
    has-braiding-α→ : ∀ {A B C}
      → (id ⊗₁ β→) ∘ α→ B A C ∘ (β→ ⊗₁ id) ≡ α→ B C A ∘ β→ ∘ α→ A B C

  to-symmetric-monoidal : Symmetric-monoidal
  to-symmetric-monoidal .Cᵇ .braiding = has-braiding
  to-symmetric-monoidal .Cᵇ .braiding-α→ = has-braiding-α→
  to-symmetric-monoidal .Cᵇ .unbraiding-α→ {A} {B} {C} =
    subst (λ β → (id ⊗₁ β {_} {_}) ∘ α→ B A C ∘ (β {_} {_} ⊗₁ id) ≡ α→ _ _ _ ∘ β {_} {_} ∘ α→ _ _ _)
      β→≡β← has-braiding-α→
  to-symmetric-monoidal .has-is-symmetric = symmetric

open make-symmetric-monoidal using (to-symmetric-monoidal) public

Properties🔗

module Braided (Cᵇ : Braided-monoidal) where
  open Braided-monoidal Cᵇ public

Just like with monoidal categories, the two hexagons relating the braiding with the associator automatically give us a whole lot of extra coherence, but it still takes a bit of work.

$\equiv$

That is, morally, $(\mathrm{id}\otimes \beta )\circ (\beta \otimes \mathrm{id})\circ (\mathrm{id}\otimes \beta )\equiv (\beta \otimes \mathrm{id})\circ (\mathrm{id}\otimes \beta )\circ (\beta \otimes \mathrm{id})\text{,}$ except we have to insert associators everywhere in order for this equation to make sense.

  yang-baxter : ∀ {A B C}
    → (id ⊗₁ β→) ∘ α→ C A B ∘ (β→ ⊗₁ id) ∘ α← A C B ∘ (id ⊗₁ β→) ∘ α→ A B C
    ≡ α→ C B A ∘ (β→ ⊗₁ id) ∘ α← B C A ∘ (id ⊗₁ β→) ∘ α→ B A C ∘ (β→ ⊗₁ id)
  yang-baxter =
    (id ⊗₁ β→) ∘ α→ _ _ _ ∘ (β→ ⊗₁ id) ∘ α← _ _ _ ∘ (id ⊗₁ β→) ∘ α→ _ _ _   ≡⟨ pushr (pushr refl) ⟩≡
    ((id ⊗₁ β→) ∘ α→ _ _ _ ∘ (β→ ⊗₁ id)) ∘ α← _ _ _ ∘ (id ⊗₁ β→) ∘ α→ _ _ _ ≡⟨ extendl (rswizzle (braiding-α→ ∙ assoc _ _ _) (α≅ .invl)) ⟩≡
    α→ _ _ _ ∘ β→ ∘ (id ⊗₁ β→) ∘ α→ _ _ _                                   ≡⟨ refl⟩∘⟨ extendl (β→.is-natural _ _ _) ⟩≡
    α→ _ _ _ ∘ (β→ ⊗₁ id) ∘ β→ ∘ α→ _ _ _                                   ≡˘⟨ refl⟩∘⟨ refl⟩∘⟨ lswizzle braiding-α→ (α≅ .invr) ⟩≡˘
    α→ _ _ _ ∘ (β→ ⊗₁ id) ∘ α← _ _ _ ∘ (id ⊗₁ β→) ∘ α→ _ _ _ ∘ (β→ ⊗₁ id)   ∎

We also derive more equations relating the braiding with the associator.

  β←-β←⊗id-α← : ∀ {A B C} → β← ∘ (β← ⊗₁ id) ∘ α← A B C ≡ α→ C B A ∘ (β← ⊗₁ id) ∘ β←
  β←-β←⊗id-α← =
    β← ∘ (β← ⊗₁ id) ∘ α← _ _ _                     ≡⟨ refl⟩∘⟨ sym (swizzle (sym (assoc _ _ _) ∙ sym unbraiding-α→ ∙ assoc _ _ _) (α≅ .invl) (pullr (▶.cancell (β≅ .invl)) ∙ α≅ .invr)) ⟩≡
    β← ∘ (α← _ _ _ ∘ (id ⊗₁ β→)) ∘ α→ _ _ _ ∘ β←   ≡⟨ pushr (pullr (pushr refl)) ⟩≡
    (β← ∘ α← _ _ _) ∘ ((id ⊗₁ β→) ∘ α→ _ _ _) ∘ β← ≡⟨ extendl (sym (swizzle β←-α← (pullr (▶.cancell (β≅ .invr)) ∙ α≅ .invr) (α≅ .invl))) ⟩≡
    α→ _ _ _ ∘ (β← ⊗₁ id) ∘ β←                     ∎

  β→-id⊗β→-α→ : ∀ {A B C} → β→ ∘ (id ⊗₁ β→) ∘ α→ A B C ≡ α← _ _ _ ∘ β→ ∘ (β→ ⊗₁ id)
  β→-id⊗β→-α→ =
    β→ ∘ (id ⊗₁ β→) ∘ α→ _ _ _   ≡⟨ pulll (β→.is-natural _ _ _) ⟩≡
    ((β→ ⊗₁ id) ∘ β→) ∘ α→ _ _ _ ≡⟨ swizzle (sym β←-β←⊗id-α← ∙ assoc _ _ _)
      (pullr (cancell (β≅ .invr)) ∙ ◀.annihilate (β≅ .invr))
      (pullr (cancell (β≅ .invl)) ∙ ◀.annihilate (β≅ .invl)) ⟩≡
    α← _ _ _ ∘ β→ ∘ (β→ ⊗₁ id)   ∎

We can also show that the unitors are related to each other via the braiding, which requires a surprising amount of work.

  λ←-β→ : ∀ {A} → λ← {A} ∘ β→ ≡ ρ←
  λ←-β→ = push-eqⁿ (unitor-r ni⁻¹) $
    (λ← ∘ β→) ⊗₁ id                                ≡⟨ insertl (β≅ .invr) ⟩≡
    β← ∘ β→ ∘ ((λ← ∘ β→) ⊗₁ id)                    ≡⟨ refl⟩∘⟨ refl⟩∘⟨ ◀.F-∘ _ _ ∙ (sym triangle-λ← ⟩∘⟨refl) ⟩≡
    β← ∘ β→ ∘ (λ← ∘ α→ _ _ _) ∘ (β→ ⊗₁ id)         ≡⟨ refl⟩∘⟨ extendl (pulll (sym (unitor-l .Isoⁿ.from .is-natural _ _ _))) ⟩≡
    β← ∘ (λ← ∘ (id ⊗₁ β→)) ∘ α→ _ _ _ ∘ (β→ ⊗₁ id) ≡⟨ refl⟩∘⟨ pullr braiding-α→ ⟩≡
    β← ∘ λ← ∘ α→ _ _ _ ∘ β→ ∘ α→ _ _ _             ≡⟨ refl⟩∘⟨ pulll triangle-λ← ⟩≡
    β← ∘ (λ← ⊗₁ id) ∘ β→ ∘ α→ _ _ _                ≡⟨ refl⟩∘⟨ extendl (sym (β→.is-natural _ _ _)) ⟩≡
    β← ∘ β→ ∘ (id ⊗₁ λ←) ∘ α→ _ _ _                ≡⟨ refl⟩∘⟨ refl⟩∘⟨ triangle-α→ ⟩≡
    β← ∘ β→ ∘ (ρ← ⊗₁ id)                           ≡⟨ cancell (β≅ .invr) ⟩≡
    ρ← ⊗₁ id                                       ∎

  λ←-β← : ∀ {A} → λ← {A} ∘ β← ≡ ρ←
  λ←-β← = push-eqⁿ (unitor-r ni⁻¹) $
    (λ← ∘ β←) ⊗₁ id                                ≡⟨ insertl (β≅ .invl) ⟩≡
    β→ ∘ β← ∘ ((λ← ∘ β←) ⊗₁ id)                    ≡⟨ refl⟩∘⟨ refl⟩∘⟨ ◀.F-∘ _ _ ∙ (sym triangle-λ← ⟩∘⟨refl) ⟩≡
    β→ ∘ β← ∘ (λ← ∘ α→ _ _ _) ∘ (β← ⊗₁ id)         ≡⟨ refl⟩∘⟨ extendl (pulll (sym (unitor-l .Isoⁿ.from .is-natural _ _ _))) ⟩≡
    β→ ∘ (λ← ∘ (id ⊗₁ β←)) ∘ α→ _ _ _ ∘ (β← ⊗₁ id) ≡⟨ refl⟩∘⟨ pullr unbraiding-α→ ⟩≡
    β→ ∘ λ← ∘ α→ _ _ _ ∘ β← ∘ α→ _ _ _             ≡⟨ refl⟩∘⟨ pulll triangle-λ← ⟩≡
    β→ ∘ (λ← ⊗₁ id) ∘ β← ∘ α→ _ _ _                ≡⟨ refl⟩∘⟨ extendl (sym (β←.is-natural _ _ _)) ⟩≡
    β→ ∘ β← ∘ (id ⊗₁ λ←) ∘ α→ _ _ _                ≡⟨ refl⟩∘⟨ refl⟩∘⟨ triangle-α→ ⟩≡
    β→ ∘ β← ∘ (ρ← ⊗₁ id)                           ≡⟨ cancell (β≅ .invl) ⟩≡
    ρ← ⊗₁ id                                       ∎

  ρ←-β← : ∀ {A} → ρ← {A} ∘ β← ≡ λ←
  ρ←-β← = rswizzle (sym λ←-β→) (β≅ .invl)

  ρ←-β→ : ∀ {A} → ρ← {A} ∘ β→ ≡ λ←
  ρ←-β→ = rswizzle (sym λ←-β←) (β≅ .invr)