Let \(T\) be a base type theory. We work in \(T\). Let \(X\) be a topos and let \(a\) be a coétale point of \(X\). Then we have a canonical equivalence