10.1.1 Limits and colimits

Since sets are closed under products, the universal property of products in \autorefthm:prod-ump shows immediately that $\mathcal{S}et$ has finite products. In fact, infinite products follow just as easily from the equivalence

\Bigl{(}X\to\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle% \prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}B(a)\Bigr{)}% \simeq\Bigl{(}\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}% }{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{% (a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle% \prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}(X\to B(a))\Bigr{% )}.

And we saw in \autorefex:pullback that the pullback of $f:A\to C$ and $g:B\to C$ can be defined as $\mathchoice{\sum_{(a:A)}\,}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)}% }{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:% A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{% (a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}\mathchoice{\sum_{(b:B)}\,}{\mathchoice{{% \textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{% \mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}% }}{\mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:% B)}}}f(a)=g(b)$ ; this is a set if $A, B, C$ are and inherits the correct universal property. Thus, $\mathcal{S}et$ is a complete category in the obvious sense.

Since sets are closed under $+$ and contain $\mathbf{0}$ , $\mathcal{S}et$ has finite coproducts. Similarly, since $\mathchoice{\sum_{a:A}\,}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)}}{% \sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)% }}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a% :A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}B(a)$ is a set whenever $A$ and each $B(a)$ are, it yields a coproduct of the family $B$ in $\mathcal{S}et$ . Finally, we showed in \autorefsec:pushouts that pushouts exist in $n$ -types, which includes $\mathcal{S}et$ in particular. Thus, $\mathcal{S}et$ is also cocomplete.

Title	10.1.1 Limits and colimits
\metatable