Let \(T\) be a base type theory. We work in the type theory of spaces in \(T\). Let \(X\) be a topos. We say a point \(a:X\) is coétale if the type family \((x:X)\mapsto a\Rightarrow x\) is valued in \(\mathcal {E}(0)\).
Let \(T\) be a base type theory. We work in the type theory of spaces in \(T\). Let \(X\) be a topos. We say a point \(a:X\) is coétale if the type family \((x:X)\mapsto a\Rightarrow x\) is valued in \(\mathcal {E}(0)\).