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
  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 .inv∘eta x = Ο€β‚‚βˆ˜βŸ¨βŸ©
    ni .natural x y f = Product.uniqueβ‚‚ (prods _ _)
      (pulll Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ pullr Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ idl _) (pulll Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ cancelr Ο€β‚‚βˆ˜βŸ¨βŸ©)
      (!-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 _ _)
      (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β‚‚ _ _)
  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 _ _)
    (pulll Ο€β‚βˆ˜βŸ¨βŸ© Β·Β· pullr Ο€β‚βˆ˜βŸ¨βŸ© Β·Β· Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ introl refl)
    (pulll Ο€β‚‚βˆ˜βŸ¨βŸ© Β·Β· pullr Ο€β‚‚βˆ˜βŸ¨βŸ© Β·Β· idl _)
  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
    mk .symmetric = ⟨⟩∘ _ βˆ™ apβ‚‚ ⟨_,_⟩ Ο€β‚‚βˆ˜βŸ¨βŸ© Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ ⟨⟩-Ξ·
    mk .has-braiding-Ξ±β†’ = products! C prods

We also have a system of diagonal morphisms:

  Cartesian-diagonal : Diagonals Cartesian-monoidal
  Cartesian-diagonal .diagonals ._=>_.Ξ· A = Ξ΄
  Cartesian-diagonal .diagonals ._=>_.is-natural = Ξ΄-natural
  Cartesian-diagonal .diagonal-Ξ»β†’ = ap ⟨_, id ⟩ (sym (!-unique _))