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 Ξ²β†’ = Binatural (braiding .Isoⁿ.to)
  module β← = Binatural (braiding .Isoⁿ.from)

  Ξ²β†’ : βˆ€ {A B} β†’ Hom (A βŠ— B) (B βŠ— A)
  Ξ²β†’ = Ξ²β†’.Ξ· _ _

  β← : βˆ€ {A B} β†’ Hom (A βŠ— B) (B βŠ— A)
  β← = β←.Ξ· _ _

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}
      β†’ (_ β–Ά Ξ²β†’) ∘ Ξ±β†’ (B , A , C) ∘ (Ξ²β†’ β—€ _) ≑ Ξ±β†’ (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}
      β†’ (_ β–Ά β←) ∘ Ξ±β†’ (B , A , C) ∘ (β← β—€ _) ≑ Ξ±β†’ (B , C , A) ∘ β← ∘ Ξ±β†’ (A , B , C)

  Ξ²β‰… : βˆ€ {A B} β†’ A βŠ— B β‰… B βŠ— A
  Ξ²β‰… = make-iso Ξ²β†’ β← (braiding .Isoⁿ.invl Ξ·β‚š _ Ξ·β‚š _) (braiding .Isoⁿ.invr Ξ·β‚š _ Ξ·β‚š _)

  open Ξ²β†’ renaming (natural-β–Ά to Ξ²β†’β–Ά ; natural-β—€ to Ξ²β†’β—€ ; natural-β—† to Ξ²β†’β—†) using () public
  open β← renaming (natural-β–Ά to β←◀ ; natural-β—€ to β←▢ ; natural-β—† to β←◆) using () public

  β←-α←
    : βˆ€ {A B C} β†’ (β← β—€ _) ∘ α← (B , A , C) ∘ (_ β–Ά β←) ≑ α← (A , B , C) ∘ β← ∘ α← (B , C , A)
  β←-α← = inverse-uniqueβ‚€
    (β—€.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)
  Ξ²β†’ = Binatural.Ξ· (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)
  Ξ²β†’ = Binatural.Ξ· (has-braiding .Isoⁿ.to) _ _
  β← : βˆ€ {A B} β†’ Hom (A βŠ— B) (B βŠ— A)
  β← = Binatural.Ξ· (has-braiding .Isoⁿ.from) _ _

  β→≑β← : Path (βˆ€ {A B} β†’ Hom (A βŠ— B) (B βŠ— A)) Ξ²β†’ β←
  β→≑β← = ext Ξ» {_} {_} β†’ inverse-uniqueβ‚€
    (make-iso Ξ²β†’ Ξ²β†’ symmetric symmetric)
    (make-iso Ξ²β†’ β← (has-braiding .Isoⁿ.invl Β·β‚š _ Β·β‚š _) (has-braiding .Isoⁿ.invr Β·β‚š _ Β·β‚š _))
    refl

  open Braided-monoidal hiding (Ξ²β†’)
  open Symmetric-monoidal hiding (Ξ²β†’)

  field
    has-braiding-Ξ±β†’ : βˆ€ {A B C}
      β†’ (_ β–Ά Ξ²β†’) ∘ Ξ±β†’ (B , A , C) ∘ (Ξ²β†’ β—€ _) ≑ Ξ±β†’ (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 (Ξ» Ξ² β†’ (_ β–Ά Ξ² {_} {_}) ∘ Ξ±β†’ (B , A , C) ∘ (Ξ² {_} {_} β—€ _) ≑ Ξ±β†’ _ ∘ Ξ² {_} {_} ∘ Ξ±β†’ _)
      β→≑β← 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}
    β†’ (_ β–Ά Ξ²β†’) ∘ Ξ±β†’ (C , A , B) ∘ (Ξ²β†’ β—€ _) ∘ α← (A , C , B) ∘ (_ β–Ά Ξ²β†’) ∘ Ξ±β†’ (A , B , C)
    ≑ Ξ±β†’ (C , B , A) ∘ (Ξ²β†’ β—€ _) ∘ α← (B , C , A) ∘ (_ β–Ά Ξ²β†’) ∘ Ξ±β†’ (B , A , C) ∘ (Ξ²β†’ β—€ _)
  yang-baxter =
    (_ β–Ά Ξ²β†’) ∘ Ξ±β†’ _ ∘ (Ξ²β†’ β—€ _) ∘ α← _ ∘ (_ β–Ά Ξ²β†’) ∘ Ξ±β†’ _   β‰‘βŸ¨ pushr (pushr refl) βŸ©β‰‘
    ((_ β–Ά Ξ²β†’) ∘ Ξ±β†’ _ ∘ (Ξ²β†’ β—€ _)) ∘ α← _ ∘ (_ β–Ά Ξ²β†’) ∘ Ξ±β†’ _ β‰‘βŸ¨ extendl (rswizzle (braiding-Ξ±β†’ βˆ™ assoc _ _ _) (Ξ±β‰… .invl)) βŸ©β‰‘
    Ξ±β†’ _ ∘ Ξ²β†’ ∘ (_ β–Ά Ξ²β†’) ∘ Ξ±β†’ _                           β‰‘βŸ¨ refl⟩∘⟨ extendl Ξ²β†’β–Ά βŸ©β‰‘
    Ξ±β†’ _ ∘ (Ξ²β†’ β—€ _) ∘ Ξ²β†’ ∘ Ξ±β†’ _                           β‰‘Λ˜βŸ¨ refl⟩∘⟨ refl⟩∘⟨ lswizzle braiding-Ξ±β†’ (Ξ±β‰… .invr) βŸ©β‰‘Λ˜
    Ξ±β†’ _ ∘ (Ξ²β†’ β—€ _) ∘ α← _ ∘ (_ β–Ά Ξ²β†’) ∘ Ξ±β†’ _ ∘ (Ξ²β†’ β—€ _)   ∎

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

  β←-Ξ²β†βŠ—id-α← : βˆ€ {A B C} β†’ β← ∘ (β← β—€ C) ∘ α← (A , B , C) ≑ Ξ±β†’ (C , B , A) ∘ (β← β—€ A) ∘ β←
  β←-Ξ²β†βŠ—id-α← =
    β← ∘ (β← β—€ _) ∘ α← _                 β‰‘βŸ¨ refl⟩∘⟨ sym (swizzle (sym (assoc _ _ _) βˆ™ sym unbraiding-Ξ±β†’ βˆ™ assoc _ _ _) (Ξ±β‰… .invl) (pullr (β–Ά.cancell (Ξ²β‰… .invl)) βˆ™ Ξ±β‰… .invr)) βŸ©β‰‘
    β← ∘ (α← _ ∘ (_ β–Ά Ξ²β†’)) ∘ Ξ±β†’ _ ∘ β←   β‰‘βŸ¨ pushr (pullr (pushr refl)) βŸ©β‰‘
    (β← ∘ α← _) ∘ ((_ β–Ά Ξ²β†’) ∘ Ξ±β†’ _) ∘ β← β‰‘βŸ¨ extendl (sym (swizzle β←-α← (pullr (β–Ά.cancell (Ξ²β‰… .invr)) βˆ™ Ξ±β‰… .invr) (Ξ±β‰… .invl))) βŸ©β‰‘
    Ξ±β†’ _ ∘ (β← β—€ _) ∘ β←                 ∎

  Ξ²β†’-idβŠ—Ξ²β†’-Ξ±β†’ : βˆ€ {A B C} β†’ Ξ²β†’ ∘ (_ β–Ά Ξ²β†’) ∘ Ξ±β†’ (A , B , C) ≑ α← _ ∘ Ξ²β†’ ∘ (Ξ²β†’ β—€ _)
  Ξ²β†’-idβŠ—Ξ²β†’-Ξ±β†’ =
    Ξ²β†’ ∘ (_ β–Ά Ξ²β†’) ∘ Ξ±β†’ _   β‰‘βŸ¨ pulll Ξ²β†’β–Ά βŸ©β‰‘
    ((Ξ²β†’ β—€ _) ∘ Ξ²β†’) ∘ Ξ±β†’ _
      β‰‘βŸ¨ swizzle (sym β←-Ξ²β†βŠ—id-α← βˆ™ assoc _ _ _)
        (pullr (cancell (Ξ²β‰… .invr)) βˆ™ β—€.annihilate (Ξ²β‰… .invr))
        (pullr (cancell (Ξ²β‰… .invl)) βˆ™ β—€.annihilate (Ξ²β‰… .invl))
      βŸ©β‰‘
    α← _ ∘ Ξ²β†’ ∘ (Ξ²β†’ β—€ _)   ∎

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 ∘ Ξ²β†’ ≑ ρ← A
  λ←-Ξ²β†’ = push-eqⁿ (unitor-r ni⁻¹) $
    (λ← _ ∘ Ξ²β†’) β—€ _                          β‰‘βŸ¨ insertl (Ξ²β‰… .invr) βŸ©β‰‘
    β← ∘ Ξ²β†’ ∘ ((λ← _ ∘ Ξ²β†’) β—€ _)              β‰‘βŸ¨ refl⟩∘⟨ refl⟩∘⟨ β—€.F-∘ _ _ βˆ™ (sym triangle-λ← ⟩∘⟨refl) βŸ©β‰‘
    β← ∘ Ξ²β†’ ∘ (λ← _ ∘ Ξ±β†’ _) ∘ (Ξ²β†’ β—€ _)       β‰‘βŸ¨ refl⟩∘⟨ extendl (pulll (sym (unitor-l .Isoⁿ.from .is-natural _ _ _))) βŸ©β‰‘
    β← ∘ (λ← _ ∘ (_ β–Ά Ξ²β†’)) ∘ Ξ±β†’ _ ∘ (Ξ²β†’ β—€ _) β‰‘βŸ¨ refl⟩∘⟨ pullr braiding-Ξ±β†’ βŸ©β‰‘
    β← ∘ λ← _ ∘ Ξ±β†’ _ ∘ Ξ²β†’ ∘ Ξ±β†’ _             β‰‘βŸ¨ refl⟩∘⟨ pulll triangle-λ← βŸ©β‰‘
    β← ∘ (λ← _ β—€ _) ∘ Ξ²β†’ ∘ Ξ±β†’ _              β‰‘βŸ¨ refl⟩∘⟨ extendl (sym Ξ²β†’β–Ά) βŸ©β‰‘
    β← ∘ Ξ²β†’ ∘ (_ β–Ά λ← _) ∘ Ξ±β†’ _              β‰‘βŸ¨ refl⟩∘⟨ refl⟩∘⟨ triangle-Ξ±β†’ βŸ©β‰‘
    β← ∘ Ξ²β†’ ∘ (ρ← _ β—€ _)                     β‰‘βŸ¨ cancell (Ξ²β‰… .invr) βŸ©β‰‘
    ρ← _ β—€ _                                 ∎

  λ←-β← : βˆ€ {A} β†’ λ← A ∘ β← ≑ ρ← A
  λ←-β← = push-eqⁿ (unitor-r ni⁻¹) $
    (λ← _ ∘ β←) β—€ _                          β‰‘βŸ¨ insertl (Ξ²β‰… .invl) βŸ©β‰‘
    Ξ²β†’ ∘ β← ∘ ((λ← _ ∘ β←) β—€ _)              β‰‘βŸ¨ refl⟩∘⟨ refl⟩∘⟨ β—€.F-∘ _ _ βˆ™ (sym triangle-λ← ⟩∘⟨refl) βŸ©β‰‘
    Ξ²β†’ ∘ β← ∘ (λ← _ ∘ Ξ±β†’ _) ∘ (β← β—€ _)       β‰‘βŸ¨ refl⟩∘⟨ extendl (pulll (sym (unitor-l .Isoⁿ.from .is-natural _ _ _))) βŸ©β‰‘
    Ξ²β†’ ∘ (λ← _ ∘ (_ β–Ά β←)) ∘ Ξ±β†’ _ ∘ (β← β—€ _) β‰‘βŸ¨ refl⟩∘⟨ pullr unbraiding-Ξ±β†’ βŸ©β‰‘
    Ξ²β†’ ∘ λ← _ ∘ Ξ±β†’ _ ∘ β← ∘ Ξ±β†’ _             β‰‘βŸ¨ refl⟩∘⟨ pulll triangle-λ← βŸ©β‰‘
    Ξ²β†’ ∘ (λ← _ β—€ _) ∘ β← ∘ Ξ±β†’ _              β‰‘βŸ¨ refl⟩∘⟨ extendl (sym β←▢) βŸ©β‰‘
    Ξ²β†’ ∘ β← ∘ (_ β–Ά λ← _) ∘ Ξ±β†’ _              β‰‘βŸ¨ refl⟩∘⟨ refl⟩∘⟨ triangle-Ξ±β†’ βŸ©β‰‘
    Ξ²β†’ ∘ β← ∘ (ρ← _ β—€ _)                     β‰‘βŸ¨ cancell (Ξ²β‰… .invl) βŸ©β‰‘
    ρ← _ β—€ _                                 ∎

  ρ←-β← : βˆ€ {A} β†’ ρ← A ∘ β← ≑ λ← A
  ρ←-β← = rswizzle (sym λ←-Ξ²β†’) (Ξ²β‰… .invl)

  ρ←-Ξ²β†’ : βˆ€ {A} β†’ ρ← A ∘ Ξ²β†’ ≑ λ← A
  ρ←-Ξ²β†’ = rswizzle (sym λ←-β←) (Ξ²β‰… .invr)