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

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

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} -βŠ—-)

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