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 -categories is an -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 β©β‘ β¨ β¨ Οβ , Οβ β Οβ β© , Οβ β Οβ β© β β¨ β¨ Οβ , Οβ β Οβ β© , Οβ β Οβ β© β