Let \(T\) be a base type theory. We work in \(T\). Let \(X\) be a topos. We say a point \(a\) of \(X\) is essential if the morphism \(\_\mapsto a:\mathord {\textnormal {\textsf {1}}}\rightarrow X\) is essential.
Let \(T\) be a base type theory. We work in \(T\). Let \(X\) be a topos. We say a point \(a\) of \(X\) is essential if the morphism \(\_\mapsto a:\mathord {\textnormal {\textsf {1}}}\rightarrow X\) is essential.