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*
$Ξ΄_{A}:AβAβA.$
Of course, such a system should be natural in
$A;$
another sensible thing to require is that the diagonal
$1β1β1$
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.