In the definition of an elementary topos, the "object of propositions" $\Omega$ is axiomatized by the universal property of a subobject classifier.
In homotopy type theory, we instead start with a universe of (small) types Type and define hProp to be the object of types that have at most one element (i.e., all elements are equal).
Are these necessarily isomorphic, and if so under what conditions? For instance are they always isomorphic in an $\infty$-topos where Type is a small object classifier? Are they always isomorphic in a 1-topos where Type is merely a universe in the sense of Streicher 2005?
I found a proof in Lurie's Higher Topos Theory that every $\infty$-topos has a sub-object classifier but it wasn't recognizable to me at least that what he was constructing was the same as hProp.
EDIT: To clarify, this is essentially a question about models, though it should be possible to restate it in terms of the internal language. My question is, if I interpret the definition of hProp in a model (say a 1-topos or an $\infty$-topos), if that model has a subobject classifier (which 1 and $\infty$-toposes do), then under what conditions is hProp isomorphic/equivalent to the subobject classifier. This would be useful to know when determining the consistency of adding axioms involving hProp since it is easy to calculate what the subobject classifier is in many concrete models.