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⟩∘⟨ 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)