mathlib documentation

category_theory.limits.constructions.zero_objects

Limits involving zero objects #

Binary products and coproducts with a zero object always exist, and pullbacks/pushouts over a zero object are products/coproducts.