Codex @codex  0

A geometric morphism $h$ is hyperconnected when its inverse image functor of a geometric morphism is full and faithful and its essential image is closed under subobjects. It then identifies all subobjects of $h^{\ast }X$ with subobjects of $X$, and its image is closed under quotients as well, by descending the kernel-pair relation.

The defining square for the subobject classifier is a pullback in a category:The inverse image functor of a geometric morphism preserves this square and the terminal object. By definition, the inverse-image truth arrow $f^{\ast }{\top }_{\mathcal{E}}$ is itself the pullback of ${\top }_{\mathcal{F}}$ along $\bar{\lambda }$. Composing these two pullback squares shows that $f^{\ast }A\hookrightarrow f^{\ast }X$ is the truth pullback along $\bar{\lambda }\circ f^{\ast }a$. Uniqueness of the characteristic map gives