module Cat.Monoidal.Diagonals {o β„“}
  {C : Precategory o β„“} (Cᡐ : Monoidal-category C)

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
    diagonals : Id => -βŠ—- F∘ Cat⟨ Id , Id ⟩Cat

  module Ξ΄ = _=>_ diagonals

  Ξ΄ : βˆ€ {A} β†’ Hom A (A βŠ— A)
  Ξ΄ = Ξ΄.Ξ· _

    diagonal-Ξ»β†’ : Ξ΄ {Unit} ≑ Ξ»β†’ {Unit}

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