open import Cat.Instances.Sets.Complete
open import Cat.Diagram.Product.Solver
open import Cat.Monoidal.Diagonals
open import Cat.Instances.Functor
open import Cat.Diagram.Terminal
open import Cat.Monoidal.Braided
open import Cat.Diagram.Product
open import Cat.Monoidal.Base
open import Cat.Prelude

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 is an However, we do have a certain canonical pool of examples to draw from: all the Cartesian monoidal categories, also known as finite-products categories.

module _
{o β} {C : Precategory o β}
(prods : β A B β Product C A B) (term : Terminal C)
where

  open Monoidal-category hiding (_ββ_)
open Braided-monoidal
open Symmetric-monoidal
open Diagonals hiding (Ξ΄)
open make-natural-iso
open Cr C
open Binary-products C prods
open Terminal term

  Cartesian-monoidal : Monoidal-category C
Cartesian-monoidal .-β- = Γ-functor
Cartesian-monoidal .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:

  Cartesian-monoidal .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 .natural x y f = Product.uniqueβ (prods _ _)
(!-uniqueβ _ _) (pulll Οβββ¨β© β idl f)
Cartesian-monoidal .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 _ _)
(idr _) (sym (!-unique _))
ni .natural x y f = Product.uniqueβ (prods _ _)
(!-uniqueβ _ _)
Cartesian-monoidal .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 β Οβ) β© β
Cartesian-monoidal .triangle = Product.unique (prods _ _)
Cartesian-monoidal .pentagon =
β¨ β¨ β¨ Οβ , Οβ β Οβ β© , Οβ β Οβ β© β Οβ , id β Οβ β© β β¨ β¨ Οβ , Οβ β Οβ β© , Οβ β Οβ β© β β¨ id β Οβ , β¨ β¨ Οβ , Οβ β Οβ β© , Οβ β Οβ β© β Οβ β© β‘β¨ products! C prods β©β‘
β¨ β¨ Οβ , Οβ β Οβ β© , Οβ β Οβ β© β β¨ β¨ Οβ , Οβ β Οβ β© , Οβ β Οβ β© β


Cartesian monoidal categories also inherit a lot of additional structure from the categorical product. In particular, they are symmetric monoidal categories.

  Cartesian-symmetric : Symmetric-monoidal Cartesian-monoidal
Cartesian-symmetric = to-symmetric-monoidal mk where
open make-symmetric-monoidal
mk : make-symmetric-monoidal Cartesian-monoidal
mk .has-braiding = isoβisoβΏ
(Ξ» _ β invertibleβiso swap swap-is-iso) swap-natural

  Cartesian-diagonal : Diagonals Cartesian-monoidal

Setsβ : β {β} β Monoidal-category (Sets β)