Monic endomorphism of a subobject classifier (source code)

= Monic endomorphism of a subobject classifier
{title2=$f^2=1_\Omega$}

In a category with <finite limits> and a <subobject classifier>, every monic endomorphism $f$ of $\Omega$ is an involution. The subobject $g:U\hookrightarrow\Omega$ classified by $f$ is subterminal, since $fg=\top!_U$ is monic. If $V\hookrightarrow U$ is classified by $g$, pullback uniqueness gives $f\top!_U=g$, hence $f^2g=g$. If $u$ classifies $U\hookrightarrow1$, the pullback of $g$ along $f$ is $\top!_U$, so $f^2(p)=u\wedge p$. Monicity implies $u=\top$, because $u\wedge u=u\wedge\top$, proving the displayed identity.