Synthetic topos theory
[003Y] Proposition

Let \(T\) be a base type theory. We work in the type theory of spaces in \(T\). Let \(X\) be a topos. Then coétale points of \(X\) are closed under finite colimits that exist in \(X\).

Proof

This is because \(\mathcal {E}(0)\) is closed under finite limits.