 Hyperconnected-localic factorization

For a geometric morphism $f:\mathcal{E}\to \mathcal{F}$, the displayed internal frame represents $X\mapsto {\mathrm{Sub}}_{\mathcal{E}}(f^{\ast }X)$. The localic part is ${\mathrm{Sh}}_{\mathcal{F}}(L)\to \mathcal{F}$. Its basic open families pull back to the subobjects of $f^{\ast }X$ they represent; gluing these gives a full faithful, subobject-closed inverse image, hence the hyperconnected geometric morphism part. The represented subobject functor recovers the internal frame, proving uniqueness up to equivalence over $\mathcal{F}$.