10.1.1 Limits and colimits

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

$$(X\to \prod _{a:A}B(a))\simeq \left(\prod _{a:A}(X\to B(a))\right).$$

And we saw in ex:pullback that the pullback of $f:A\to C$ and $g:B\to C$ can be defined as ${\sum }_{(a:A)}{\sum }_{(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 complete category in the obvious sense.

Since sets are closed under $+$ and contain $\mathrm{𝟎}$, $𝒮et$ has finite coproducts.Similarly, since ${\sum }_{(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 sec:pushouts that pushouts exist in $n$-types, which includes $𝒮et$ in particular.Thus, $𝒮et$ is also cocomplete.