10.1.1 Limits and colimits
Since sets are closed under products
, the universal property
of products in \autorefthm:prod-ump shows immediately that has finite products.
In fact, infinite products follow just as easily from the equivalence
And we saw in \autorefex:pullback that the pullback of and can be defined as ; this is a set if are and inherits the correct universal property.
Thus, is a complete
category
in the obvious sense.
Since sets are closed under and contain , has finite coproducts.
Similarly, since is a set whenever and each are, it yields a coproduct of the family in .
Finally, we showed in \autorefsec:pushouts that pushouts exist in -types, which includes in particular.
Thus, is also cocomplete.
Title | 10.1.1 Limits and colimits![]() |
---|---|
\metatable |