open import Cat.Functor.Bifunctor
open import Cat.Instances.Product
open import Cat.Monoidal.Base
open import Cat.Prelude

import Cat.Reasoning

module Cat.Monoidal.Diagonals {o ℓ}
  {C : Precategory o ℓ} (Cᵐ : Monoidal-category C)
  where

Monoidal categories with diagonals🔗

open Cat.Reasoning C
open Monoidal Cᵐ

_ = λ≡ρ

A monoidal category can be equipped with a system of diagonal morphisms $δ_{A} : A \to A \otimes A .$ Of course, such a system should be natural in $A;$ 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 => Uncurry -⊗- F∘ Cat⟨ Id , Id ⟩Cat

  module δ = _=>_ diagonals
  open δ renaming (η to δ) using () public

  field
    diagonal-λ→ : δ _ ≡ λ→ Unit

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