Documentation

Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Chosen finite products in Cat #

This file proves that the cartesian product of a pair of categories agrees with the product in Cat, and provides the associated CartesianMonoidalCategory instance.

The chosen terminal object in Cat is terminal.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    The type of functors out of the chosen terminal category is equivalent to the type of objects in the target category. TODO: upgrade to an equivalence of categories.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      The chosen product of categories C × D yields a product cone in Cat.

      Equations
      Instances For

        The product cone in Cat is indeed a product.

        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          theorem CategoryTheory.Monoidal.associator_hom (X Y Z : Cat) :
          (MonoidalCategoryStruct.associator X Y Z).hom = ((Prod.fst (X × Y) Z).comp (Prod.fst X Y)).prod' (((Prod.fst (X × Y) Z).comp (Prod.snd X Y)).prod' (Prod.snd (X × Y) Z))
          theorem CategoryTheory.Monoidal.associator_inv (X Y Z : Cat) :
          (MonoidalCategoryStruct.associator X Y Z).inv = ((Prod.fst (↑X) (Y × Z)).prod' ((Prod.snd (↑X) (Y × Z)).comp (Prod.fst Y Z))).prod' ((Prod.snd (↑X) (Y × Z)).comp (Prod.snd Y Z))