Categories with chosen finite products #
We introduce a class, ChosenFiniteProducts
, which bundles explicit choices
for a terminal object and binary products in a category C
.
This is primarily useful for categories which have finite products with good
definitional properties, such as the category of types.
Given a category with such an instance, we also provide the associated
symmetric monoidal structure so that one can write X ā Y
for the explicit
binary product and š_ C
for the explicit terminal object.
Projects #
- Construct an instance of chosen finite products in the category of affine scheme, using the tensor product.
- Construct chosen finite products in other categories appearing "in nature".
An instance of ChosenFiniteProducts C
bundles an explicit choice of a binary
product of two objects of C
, and a terminal object in C
.
Users should use the monoidal notation: X ā Y
for the product and š_ C
for
the terminal object.
- product : (X Y : C) ā CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)
A choice of a limit binary fan for any two objects of the category.
- terminal : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C)
A choice of a terminal object.
Instances
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The unique map to the terminal object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- CategoryTheory.ChosenFiniteProducts.instUniqueHomTensorUnit X = { default := CategoryTheory.ChosenFiniteProducts.toUnit X, uniq := āÆ }
This lemma follows from the preexisting Unique
instance, but
it is often convenient to use it directly as apply toUnit_unique
forcing
lean to do the necessary elaboration.
Construct a morphism to the product given its two components.
Equations
- CategoryTheory.ChosenFiniteProducts.lift f g = (CategoryTheory.ChosenFiniteProducts.product X Y).isLimit.lift (CategoryTheory.Limits.BinaryFan.mk f g)
Instances For
The first projection from the product.
Equations
Instances For
The second projection from the product.
Equations
Instances For
Equations
- āÆ = āÆ
Equations
- āÆ = āÆ
Construct an instance of ChosenFiniteProducts C
given an instance of HasFiniteProducts C
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- āÆ = āÆ