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.Functor.Reasoning as Fr
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 together with a chosen functor, the tensor product, and a distinguished object 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)

infixr 25 _β_


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

The morphism is called the associator, and (resp. 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} β X β Unit β X
Ξ»β = isoβΏβiso unitor-l _

Ξ»β : β {X} β Hom (Unit β X) X
Ξ»β = unitor-l .Cr._β_.from .Ξ· _

Ξ»β : β {X} β Hom X (Unit β X)
Ξ»β = unitor-l .Cr._β_.to .Ξ· _

Οβ : β {X} β X β X β Unit
Οβ = isoβΏβiso unitor-r _

Οβ : β {X} β Hom (X β Unit) X
Οβ = unitor-r .Cr._β_.from .Ξ· _

Οβ : β {X} β Hom X (X β Unit)
Οβ = unitor-r .Cr._β_.to .Ξ· _

Ξ±β : β {A B C} β (A β B) β C β A β (B β C)
Ξ±β = isoβΏβiso associator _

Ξ±β : β 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 .Ξ· _

module β = Fr -β-
module βΆ {A} = Fr (-β-.Right A)
module β {A} = Fr (-β-.Left A)

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

  triangle-Ξ±β : β {A B} β (A βΆ Ξ»β) β Ξ±β _ _ _ β‘ Οβ β B
triangle-Ξ±β = rswizzle (sym triangle) (Ξ±β .invr)

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
pentagon-Ξ±β = inverse-unique refl refl
(βΆ.F-map-iso (Ξ±β Isoβ»ΒΉ) βIso Ξ±β Isoβ»ΒΉ βIso β.F-map-iso (Ξ±β Isoβ»ΒΉ))
(Ξ±β Isoβ»ΒΉ βIso Ξ±β Isoβ»ΒΉ)
(sym (assoc _ _ _) β pentagon)


## Deloopingsπ

Just as a monoid can be promoted to a 1-object category, with the underlying set of the monoid becoming the single we can deloop a monoidal category into a bicategory with a single object, where the sole 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 is the same as an with a single object.

## Endomorphism categoriesπ

In the same way that, if you have a category making a choice of object canonically gives you a monoid of endomorphisms having a bicategory and choosing an object canonically gives you a choice of monoidal category,

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


## Propertiesπ

module Monoidal {o β} {C : Precategory o β} (M : Monoidal-category C) where
open Cr C
open Monoidal-category M public


While the triangle and pentagon identities turn out to be sufficient to derive all the desired coherence in a monoidal category, this is not exactly trivial. We prove a few basic identities that follow from the axioms.

Source

The proofs in this section are from Kelly (1964), but the visualisation as a triangular prism takes inspiration from the previous formalisation in agda-categories.

First, we will show that the two ways of going (using the unitor on or on are coherent. We do this by pasting isomorphisms together to form a triangular prism with given sides and lid, as in the following diagram:

We obtain the commutativity of the bottom triangle, which yields the desired equation since is an equivalence.

  triangle-Ξ»β : β {A B} β Ξ»β β Ξ±β Unit A B β‘ Ξ»β ββ id
triangle-Ξ»β {A} {B} = push-eqβΏ (unitor-l niβ»ΒΉ) $βΆ.F-β _ _ β ap to (Iso-prism base sq1 sq2 sq3) where base : β.F-map-iso (Ξ±β Isoβ»ΒΉ) βIso β.F-map-iso (β.F-map-iso (Οβ Isoβ»ΒΉ)) β‘ β.F-map-iso (βΆ.F-map-iso (Ξ»β Isoβ»ΒΉ)) base = β -path (β.collapse triangle) sq1 : β.F-map-iso (Ξ±β Isoβ»ΒΉ) βIso Ξ±β βIso Ξ±β β‘ Ξ±β βIso βΆ.F-map-iso Ξ±β sq1 = β -path (rswizzle (sym pentagon-Ξ±β β assoc _ _ _) (β.annihilate (Ξ±β .invl))) sq2 : β.F-map-iso (β.F-map-iso (Οβ Isoβ»ΒΉ)) βIso Ξ±β β‘ (Ξ±β βIso Ξ±β ) βIso βΆ.F-map-iso (Ξ»β Isoβ»ΒΉ) sq2 = β -path$
Ξ±β _ _ _ β ((Οβ ββ id) ββ id)    β‘β¨ associator .IsoβΏ.to .is-natural _ _ _ β©β‘
(Οβ ββ β id ββ id β) β Ξ±β _ _ _  β‘β¨ ap! β.F-id β©β‘
(Οβ ββ id) β Ξ±β _ _ _            β‘Λβ¨ pulll triangle-Ξ±β β©β‘Λ
(id ββ Ξ»β) β Ξ±β _ _ _ β Ξ±β _ _ _ β

sq3 : β.F-map-iso (βΆ.F-map-iso (Ξ»β Isoβ»ΒΉ)) βIso Ξ±β
β‘ Ξ±β βIso βΆ.F-map-iso (β.F-map-iso (Ξ»β Isoβ»ΒΉ))
sq3 = β-path (associator .IsoβΏ.to .is-natural _ _ _)


As a consequence, we get that the two unitors agree:

  Ξ»β‘Ο : Ξ»β {Unit} β‘ Οβ {Unit}
Ξ»β‘Ο = push-eqβΏ (unitor-r niβ»ΒΉ) \$
(Ξ»β ββ id)            β‘Λβ¨ triangle-Ξ»β β©β‘Λ
Ξ»β β Ξ±β _ _ _         β‘β¨ (insertl (Ξ»β .invl) Β·Β· reflβ©ββ¨ sym (unitor-l .IsoβΏ.from .is-natural _ _ _) Β·Β· cancell (Ξ»β .invl)) β©ββ¨refl β©β‘
(id ββ Ξ»β) β Ξ±β _ _ _ β‘β¨ triangle-Ξ±β β©β‘
(Οβ ββ id)            β


## References

• Kelly, G. M. 1964. βOn MacLaneβs Conditions for Coherence of Natural Associativities, Commutativities, Etc.β Journal of Algebra 1 (4): 397β402. https://doi.org/https://doi.org/10.1016/0021-8693(64)90018-3.