Explicit limits and colimits #
This file collects some constructions of explicit limits and colimits in CompHaus
,
which may be useful due to their definitional properties.
So far, we have the following:
- Explicit pullbacks, defined in the "usual" way as a subset of the product.
- Explicit finite coproducts, defined as a disjoint union.
The projection from the pullback to the first component.
Instances For
The projection from the pullback to the second component.
Instances For
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.
Instances For
The homeomorphism from the explicit pullback to the abstract pullback.
Instances For
The inclusion of one of the factors into the explicit finite coproduct.
Instances For
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.
Instances For
The coproduct cocone associated to the explicit finite coproduct.
Instances For
The explicit finite coproduct cocone is a colimit cocone.
Instances For
The isomorphism from the explicit finite coproducts to the abstract coproduct.
Instances For
The homeomorphism from the explicit finite coproducts to the abstract coproduct.