(Co)limit construction theorems
(Co)limit construction theorems allow for the computation of (co)limits in terms of other limits. Namely #m/thm/cat
- All (co)limits are constructable from (co)products and (co)equalizers;
- All finite (co)limits are constructable from binary (co)products and binary (co)equalizers;
- All finite (co)limits are constructable from fibre (co)products and a (co)initial object.
Proof
#missing/proof See e.g. https://ncatlab.org/nlab/show/limit#ConstructionFromProductsAndEqualizers
#state/develop | #lang/en | #SemBr