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
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|