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 ChosenFiniteProducts
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 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.