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 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 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 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.

We start by proving the Yang-Baxter equation, which says, pictorially, that the following two ways of going from to are the same:

That is, morally, 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.

Source

These proofs are adapted from braiding-coherenceβunit in the agda-categories library: see there for an explanation and diagram.

  Ξ»β-Ξ²β : β {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β©ββ¨ 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)