Synthetic topos theory
[004P] Proposition

Let \(T\) be a base type theory. We work in the type theory of spaces in \(T\). Then the point \(\bot :\Omega \) is coétale.

Proof

By [003Y].