= Least dense truth characterizes an open local operator
{title2=$J\text{ has least }u\iff j(p)=u\Rightarrow p$}
For $j=o(U)$, the <dense monomorphism classifier> consists of the truth values above $u$, so has least element $u$. Conversely, if it has least element $u$, density of a <monomorphism> is exactly containment of the pulled-back subterminal $U$. For a subobject $S\subseteq X$, the mono $S\to\overline S$ is dense, so $U\cap\overline S\subseteq S$ and $j(p)\le u\Rightarrow p$. Since $j(u)=\top$, applying $j$ to $u\wedge(u\Rightarrow p)\le p$ gives $u\Rightarrow p\le j(p)$. Hence equality holds.
Back to article page
