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.
@[reducible, inline]
The chosen terminal object in Cat
.
Equations
Instances For
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
- C.prodCone D = CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.Prod.fst ↑C ↑D) (CategoryTheory.Prod.snd ↑C ↑D)
Instances For
The product cone in Cat
is indeed a product.
Equations
- X.isLimitProdCone Y = CategoryTheory.Limits.BinaryFan.isLimitMk (fun (S : CategoryTheory.Limits.BinaryFan X Y) => CategoryTheory.Functor.prod' S.fst S.snd) ⋯ ⋯ ⋯
Instances For
Equations
- One or more equations did not get rendered due to their size.