Explicit limits and colimits #
This file collects some constructions of explicit limits and colimits in
which may be useful due to their definitional properties.
Main definitions #
Construct a morphism to the explicit pullback given morphisms to the factors which are compatible with the maps to the base. This is essentially the universal property of the pullback.
The homeomorphism from the explicit pullback to the abstract pullback.
To construct a morphism from the explicit finite coproduct, it suffices to specify a morphism from each of its factors. This is essentially the universal property of the coproduct.