open import Cat.Diagram.Product.Solver
open import Cat.Instances.Functor
open import Cat.Diagram.Terminal
open import Cat.Monoidal.Base
open import Cat.Prelude

import Cat.Functor.Bifunctor as Bifunctor
import Cat.Diagram.Product
import Cat.Reasoning as Cr

module Cat.Monoidal.Instances.Cartesian where

Cartesian monoidal categoriesπŸ”—

Unlike with categories and bicategories, there is no handy example of monoidal category that is as canonical as how the collection of all nn-categories is an (n+1)(n+1)-category. However, we do have a certain canonical pool of examples to draw from: all the Cartesian monoidal categories, also known as finite-products categories.

  Cartesian-monoidal : (βˆ€ A B β†’ Product A B) β†’ Terminal C β†’ Monoidal-category C
  Cartesian-monoidal prods term = mon where
    open Cartesian prods
    open Terminal term
    mon : Monoidal-category C
    mon .-βŠ—- = Γ—-functor
    mon .Unit = top

There’s nothing much to say about this result: It’s pretty much just banging out the calculation. Our tensor product functor is the Cartesian product functor, and the tensor unit is the terminal object (the empty product). Associators and units are the evident maps, which are coherent by the properties of limits. Translating this intuitive explanation to a formal proof requires a lot of calculation, however:

    mon .unitor-l = to-natural-iso ni where
      ni : make-natural-iso _ _
      ni .eta x = ⟨ ! , id ⟩
      ni .inv x = Ο€β‚‚
      ni .eta∘inv x = Product.uniqueβ‚‚ (prods _ _)
        (pulll Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ sym (!-unique _)) (cancell Ο€β‚‚βˆ˜βŸ¨βŸ©) (!-uniqueβ‚‚ _ _) (idr _)
      ni .inv∘eta x = Ο€β‚‚βˆ˜βŸ¨βŸ©
      ni .natural x y f = Product.uniqueβ‚‚ (prods _ _)
        (pulll Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ pullr Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ idl _) (pulll Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ cancelr Ο€β‚‚βˆ˜βŸ¨βŸ©)
        (!-uniqueβ‚‚ _ _) (pulll Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ idl f)
    mon .unitor-r = to-natural-iso ni where
      ni : make-natural-iso _ _
      ni .eta x = ⟨ id , ! ⟩
      ni .inv x = π₁
      ni .eta∘inv x = Product.uniqueβ‚‚ (prods _ _)
        (pulll Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ idl _) (pulll Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ sym (!-unique _))
        (idr _) (sym (!-unique _))
      ni .inv∘eta x = Ο€β‚βˆ˜βŸ¨βŸ©
      ni .natural x y f = Product.uniqueβ‚‚ (prods _ _)
        (pulll Ο€β‚βˆ˜βŸ¨βŸ© Β·Β· pullr Ο€β‚βˆ˜βŸ¨βŸ© Β·Β· idr f)
        (pulll Ο€β‚‚βˆ˜βŸ¨βŸ© Β·Β· pullr Ο€β‚‚βˆ˜βŸ¨βŸ© Β·Β· idl !)
        (pulll Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ idl f)
        (!-uniqueβ‚‚ _ _)
    mon .associator = to-natural-iso ni where
      ni : make-natural-iso _ _
      ni .eta x = ⟨ π₁ ∘ π₁ , ⟨ Ο€β‚‚ ∘ π₁ , Ο€β‚‚ ⟩ ⟩
      ni .inv x = ⟨ ⟨ π₁ , π₁ ∘ Ο€β‚‚ ⟩ , Ο€β‚‚ ∘ Ο€β‚‚ ⟩
      ni .eta∘inv x =
        ⟨ π₁ ∘ π₁ , ⟨ Ο€β‚‚ ∘ π₁ , Ο€β‚‚ ⟩ ⟩ ∘ ⟨ ⟨ π₁ , π₁ ∘ Ο€β‚‚ ⟩ , Ο€β‚‚ ∘ Ο€β‚‚ ⟩ β‰‘βŸ¨ products! C prods βŸ©β‰‘
        id ∎
      ni .inv∘eta x =
        ⟨ ⟨ π₁ , π₁ ∘ Ο€β‚‚ ⟩ , Ο€β‚‚ ∘ Ο€β‚‚ ⟩ ∘ ⟨ π₁ ∘ π₁ , ⟨ Ο€β‚‚ ∘ π₁ , Ο€β‚‚ ⟩ ⟩ β‰‘βŸ¨ products! C prods βŸ©β‰‘
        id ∎
      ni .natural x y f =
        ⟨ f .fst ∘ π₁ , ⟨ f .snd .fst ∘ π₁ , f .snd .snd ∘ Ο€β‚‚ ⟩ ∘ Ο€β‚‚ ⟩ ∘ ⟨ π₁ ∘ π₁ , ⟨ Ο€β‚‚ ∘ π₁ , Ο€β‚‚ ⟩ ⟩     β‰‘βŸ¨ products! C prods βŸ©β‰‘
        ⟨ π₁ ∘ π₁ , ⟨ Ο€β‚‚ ∘ π₁ , Ο€β‚‚ ⟩ ⟩ ∘ ⟨ (⟨ f .fst ∘ π₁ , f .snd .fst ∘ Ο€β‚‚ ⟩ ∘ π₁) , (f .snd .snd ∘ Ο€β‚‚) ⟩ ∎
    mon .triangle = Product.unique (prods _ _) _
      (pulll Ο€β‚βˆ˜βŸ¨βŸ© Β·Β· pullr Ο€β‚βˆ˜βŸ¨βŸ© Β·Β· Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ introl refl)
      (pulll Ο€β‚‚βˆ˜βŸ¨βŸ© Β·Β· pullr Ο€β‚‚βˆ˜βŸ¨βŸ© Β·Β· idl _)
    mon .pentagon =
      ⟨ ⟨ ⟨ π₁ , π₁ ∘ Ο€β‚‚ ⟩ , Ο€β‚‚ ∘ Ο€β‚‚ ⟩ ∘ π₁ , id ∘ Ο€β‚‚ ⟩ ∘ ⟨ ⟨ π₁ , π₁ ∘ Ο€β‚‚ ⟩ , Ο€β‚‚ ∘ Ο€β‚‚ ⟩ ∘ ⟨ id ∘ π₁ , ⟨ ⟨ π₁ , π₁ ∘ Ο€β‚‚ ⟩ , Ο€β‚‚ ∘ Ο€β‚‚ ⟩ ∘ Ο€β‚‚ ⟩ β‰‘βŸ¨ products! C prods βŸ©β‰‘
      ⟨ ⟨ π₁ , π₁ ∘ Ο€β‚‚ ⟩ , Ο€β‚‚ ∘ Ο€β‚‚ ⟩ ∘ ⟨ ⟨ π₁ , π₁ ∘ Ο€β‚‚ ⟩ , Ο€β‚‚ ∘ Ο€β‚‚ ⟩ ∎