module Cat.Monoidal.Diagonals {o β} {C : Precategory o β} (Cα΅ : Monoidal-category C) where
Monoidal categories with diagonalsπ
A monoidal
category can be equipped with a system of diagonal
morphisms
Of course, such a system should be natural in
another sensible thing to require is that the diagonal
agree with the left (hence
also right) unitor.
We call the resulting structure a monoidal category with diagonals.
record Diagonals : Type (o β β) where field diagonals : Id => -β- Fβ Catβ¨ Id , Id β©Cat module Ξ΄ = _=>_ diagonals Ξ΄ : β {A} β Hom A (A β A) Ξ΄ = Ξ΄.Ξ· _ field diagonal-Ξ»β : Ξ΄ {Unit} β‘ Ξ»β {Unit}
The prototypical examples of monoidal categories with diagonals are cartesian monoidal categories.