10.1.1 Limits and colimits

Since sets are closed underPlanetmathPlanetmath productsMathworldPlanetmathPlanetmathPlanetmath, the universal propertyMathworldPlanetmath of products in \autorefthm:prod-ump shows immediately that 𝒮et has finite products. In fact, infinite products follow just as easily from the equivalence


And we saw in \autorefex:pullbackPlanetmathPlanetmath that the pullback of f:AC and g:BC can be defined as (a:A)(b:B)f(a)=g(b); this is a set if A,B,C are and inherits the correct universal property. Thus, 𝒮et is a completePlanetmathPlanetmathPlanetmathPlanetmath categoryMathworldPlanetmath in the obvious sense.

Since sets are closed under + and contain 𝟎, 𝒮et has finite coproductsMathworldPlanetmath. Similarly, since (a:A)B(a) is a set whenever A and each B(a) are, it yields a coproduct of the family B in 𝒮et. Finally, we showed in \autorefsec:pushouts that pushouts exist in n-types, which includes 𝒮et in particular. Thus, 𝒮et is also cocomplete.

Title 10.1.1 Limits and colimitsMathworldPlanetmath