open import Cat.Instances.Functor
open import Cat.Instances.Product
open import Cat.Bi.Base
open import Cat.Prelude

import Cat.Functor.Bifunctor as Bifunctor
import Cat.Reasoning as Cr

module Cat.Monoidal.Base where

open _=>_

Monoidal categoriesπŸ”—

record Monoidal-category {o β„“} (C : Precategory o β„“) : Type (o βŠ” β„“) where
  no-eta-equality
  open Cr C

A monoidal category is a vertical categorification of the concept of monoid: We replace the identities in a monoid by isomorphisms. For this to make sense, a monoidal category must have an underlying precategory, rather than an underlying set; Similarly, the multiplication operation must be a multiplication functor, and we have to throw on some coherence data on top, to make sure everything works out.

We start with a category C\mathcal{C} together with a chosen functor, the tensor product, βŠ—:CΓ—Cβ†’C\otimes : \mathcal{C} \times \mathcal{C} \to \mathcal{C}, and a distinguished object I:CI : \mathcal{C}, the tensor unit. These take the place of the multiplication operation and identity element, respectively.

  field
    -βŠ—-  : Functor (C Γ—αΆœ C) C
    Unit : Ob

  private module -βŠ—- = Bifunctor -βŠ—-
  _βŠ—_ : Ob β†’ Ob β†’ Ob
  A βŠ— B = -βŠ—- .Functor.Fβ‚€ (A , B)

  _βŠ—β‚_ : βˆ€ {w x y z} β†’ Hom w x β†’ Hom y z β†’ Hom (w βŠ— y) (x βŠ— z)
  f βŠ—β‚ g = -βŠ—- .Functor.F₁ (f , g)

We replace the associativity and unit laws by associativity and unitor morphisms, which are natural isomorphisms (in components)

Ξ±X,Y,Z:XβŠ—(YβŠ—Z)β†’βˆΌ(XβŠ—Y)βŠ—ZρX:XβŠ—1β†’βˆΌXΞ»X:1βŠ—Xβ†’βˆΌX, \begin{align*} &\alpha_{X,Y,Z} : X \otimes (Y \otimes Z) \xrightarrow{\sim} (X \otimes Y) \otimes Z \\ &\rho_{X} : X \otimes 1 \xrightarrow{\sim} X \\ &\lambda_{X} : 1 \otimes X \xrightarrow{\sim} X\text{,} \end{align*}

The morphism α\alpha is called the associator, and ρ\rho (resp. λ\lambda) are the right unitor (resp. left unitor).

  field
    unitor-l : Cr._β‰…_ Cat[ C , C ] Id (-βŠ—-.Right Unit)
    unitor-r : Cr._β‰…_ Cat[ C , C ] Id (-βŠ—-.Left Unit)

    associator : Cr._β‰…_ Cat[ C Γ—αΆœ C Γ—αΆœ C , C ]
      (compose-assocΛ‘ {O = ⊀} {H = Ξ» _ _ β†’ C} -βŠ—-)
      (compose-assocΚ³ {O = ⊀} {H = Ξ» _ _ β†’ C} -βŠ—-)

  λ← : βˆ€ {X} β†’ Hom (Unit βŠ— X) X
  λ← = unitor-l .Cr._β‰…_.from .Ξ· _

  Ξ»β†’ : βˆ€ {X} β†’ Hom X (Unit βŠ— X)
  Ξ»β†’ = unitor-l .Cr._β‰…_.to .Ξ· _

  ρ← : βˆ€ {X} β†’ Hom (X βŠ— Unit) X
  ρ← = unitor-r .Cr._β‰…_.from .Ξ· _

  ρ→ : βˆ€ {X} β†’ Hom X (X βŠ— Unit)
  ρ→ = unitor-r .Cr._β‰…_.to .Ξ· _

  Ξ±β†’ : βˆ€ A B C β†’ Hom ((A βŠ— B) βŠ— C) (A βŠ— (B βŠ— C))
  Ξ±β†’ _ _ _ = associator .Cr._β‰…_.to .Ξ· _

  α← : βˆ€ A B C β†’ Hom (A βŠ— (B βŠ— C)) ((A βŠ— B) βŠ— C)
  α← _ _ _ = associator .Cr._β‰…_.from .Ξ· _

  -- whiskering on the right
  _β–Ά_ : βˆ€ A {B C} (g : Hom B C) β†’ Hom (A βŠ— B) (A βŠ— C)
  _β–Ά_ A f = id βŠ—β‚ f

  -- whiskering on the left
  _β—€_ : βˆ€ {A B} (g : Hom A B) C β†’ Hom (A βŠ— C) (B βŠ— C)
  _β—€_ f A = f βŠ—β‚ id

The final data we need are coherences relating the left and right unitors (the triangle identity; despite the name, nothing to do with adjunctions), and one for reducing sequences of associators, the pentagon identity. As for where the name β€œpentagon” comes from, the path pentagon witnesses commutativity of the diagram

which we have drawn less like a regular pentagon and more like a children’s drawing of a house, so that it fits on the page horizontally.

  field
    triangle : βˆ€ {A B} β†’ (ρ← β—€ B) ∘ α← A Unit B ≑ A β–Ά λ←

    pentagon
      : βˆ€ {A B C D}
      β†’ (α← A B C β—€ D) ∘ α← A (B βŠ— C) D ∘ (A β–Ά α← B C D)
      ≑ α← (A βŠ— B) C D ∘ α← A B (C βŠ— D)

DeloopingsπŸ”—

Just as a monoid can be promoted to a 1-object category, with the underlying set of the monoid becoming the single Hom\mathbf{Hom}-set, we can deloop a monoidal category into a bicategory with a single object, where the sole Hom\mathbf{Hom}-category is given by the monoidal category.

Deloop
  : βˆ€ {o β„“} {C : Precategory o β„“} β†’ Monoidal-category C β†’ Prebicategory lzero o β„“
Deloop {C = C} mon = bi where
  open Prebicategory
  module M = Monoidal-category mon
  bi : Prebicategory _ _ _
  bi .Ob = ⊀
  bi .Hom _ _ = C
  bi .id = M.Unit
  bi .compose = M.-βŠ—-
  bi .unitor-l = M.unitor-l
  bi .unitor-r = M.unitor-r
  bi .associator = M.associator
  bi .triangle _ _ = M.triangle
  bi .pentagon _ _ _ _ = M.pentagon

This makes the idea that a monoidal category is β€œjust” the categorified version of a monoid precisely, and it’s generally called the delooping hypothesis: A monoidal nn-category is the same as an (n+1)(n+1)-category with a single object.

Endomorphism categoriesπŸ”—

In the same way that, if you have a category C\mathcal{C}, making a choice of object a:Ca : \mathcal{C} canonically gives you a monoid EndoC(a)\mathrm{Endo}_\mathcal{C}(a) of endomorphisms a→aa \to a, having a bicategory B\mathbf{B} and choosing an object a:Ba : \mathbf{B} canonically gives you a choice of monoidal category, EndoB(a)\mathrm{Endo}_\mathbf{B}(a).

Endomorphisms
  : βˆ€ {o β„“ β„“β€²} (B : Prebicategory o β„“ β„“β€²)
  β†’ (a : Prebicategory.Ob B)
  β†’ Monoidal-category (Prebicategory.Hom B a a)
Endomorphisms B a = mon where
  open Monoidal-category
  module B = Prebicategory B
  mon : Monoidal-category (B.Hom a a)
  mon .-βŠ—- = B.compose
  mon .Unit = B.id
  mon .unitor-l = B.unitor-l
  mon .unitor-r = B.unitor-r
  mon .associator = to-natural-iso $ ni where
    open make-natural-iso
    open Cr
    ni : make-natural-iso _ _
    ni .eta _ = B.Ξ±β†’ _ _ _
    ni .inv _ = B.α← _ _ _
    ni .eta∘inv _ = Cr.invl _ B.associator Ξ·β‚š _
    ni .inv∘eta _ = Cr.invr _ B.associator Ξ·β‚š _
    ni .natural x y f = sym $ Cr.to B.associator .is-natural _ _ _
  mon .triangle = B.triangle _ _
  mon .pentagon = B.pentagon _ _ _ _