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 ${\delta }_A:A\to A\otimes A\text{.}$ Of course, such a system should be natural in $A\text{;}$ another sensible thing to require is that the diagonal $1\to 1\otimes 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 ⟩

  module δ = _=>_ diagonals

  δ : ∀ {A} → Hom A (A ⊗ A)
  δ = δ.η _

  field
    diagonal-λ→ : δ {Unit} ≡ λ→ {Unit}

The prototypical examples of monoidal categories with diagonals are cartesian monoidal categories.