= Boolean cover by a generic quasi-closed subtopos
{c}
{title2=$\operatorname{sh}_{q(\top)}(\mathcal E/\Omega)\to\mathcal E$}
In $\mathcal E/\Omega$, the generic truth mono $\top:1\hookrightarrow\Omega$ defines a quasi-closed Boolean subtopos. Its composite to $\mathcal E$ is surjective. If a predicate $p(x)$ pulled back from $\mathcal E$ becomes dense, then $((p(x)\Rightarrow u)\Rightarrow u)=1$ for the generic truth $u$. Substitution $u=p(x)$ yields $p(x)=1$, proving reflection of invertible monos and hence faithfulness.
Back to article page
