Synthetic topos theory
[0040] Proposition

Let \(T\) be a base type theory. We work in the type theory of spaces in \(T\). Then every finitely presented point of \(\mathcal {E}\) is coétale.

Proof

By [003Y] and [003Z].