mathlib documentation

category_theory.limits.constructions.binary_products

Constructing binary product from pullbacks and terminal object. #

The product is the pullback over the terminal objects. In particular, if a category has pullbacks and a terminal object, then it has binary products.

We also provide the dual.

Any category with pullbacks and a terminal object has a limit cone for each walking pair.

Equations

A functor that preserves terminal objects and pullbacks preserves binary products.

Equations

Any category with pushouts and an initial object has a colimit cocone for each walking pair.

Equations

A functor that preserves initial objects and pushouts preserves binary coproducts.

Equations