When is hProp equivalent to the subobject classifier?

Question

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.

Answer 1

In Proposition 11.3 of All (∞,1)-toposes have strict univalent universes I proved that the interpretation of type theory in any $(\infty,1)$-topos — with the universes interpreted by object classifiers, so that univalence holds — satisfies propositional resizing. The proof proceeds by showing that the interpretations of $\rm hProp$ in any universe are all equivalent to the subobject classifier, hence are all equivalent to each other. So I believe this answers your question in that case.

This is not true in general for interpretation in a 1-topos, not even in $\rm Set$. For instance, if we interpret type theory in $\rm Set$ where the $j$th universe is interpreted by $V_\kappa$ where $\kappa$ is the $j$th inaccessible cardinal, then ${\rm hProp}_j$ is interpreted by the set of subsingletons in $V_\kappa$, of which there are generally quite a lot, so it is not equivalent to the subobject classifier. In $\rm Set$ you can probably cut and paste to create universes containing only two subsingletons, so that it becomes true; but that seems unlikely to work in an arbitrary 1-topos.

Answer 2

$\newcommand{\Type}{\mathsf{Type}}$ $\newcommand{\hProp}{\mathsf{hProp}}$ $\newcommand{\isEmbedding}{\mathsf{isEmbedding}}$

Recall from HoTT book Definition 4.6.1 that $f : A \to B$ is an embedding when for all $x, y : A$ the function $\mathsf{ap}_{f,x,y} : (x =_A y) \to (f(x) =_B f(y))$ is an equivalence. (This is the correct generalization of injectivity.) Because being an equivalence is a proposition, being an embedding is as well. Let $\isEmbedding(f)$ be the predicate stating that $f$ is an embedding: $$ \isEmbedding(f) = \textstyle \prod_{x, y : A} \mathsf{isEquiv}(\mathsf{ap}_{f,x,y}). $$

Let $!_B : B \to \mathsf{1}$ be the unique map to the unit type $\mathsf{1}$. Then $$ \textstyle \isEmbedding(!_B) \simeq \left(\prod_{x, y : B} \mathsf{isEquiv}(\mathsf{ap}_{!_B})\right) \simeq \left(\prod_{x, y : B} x =_B y\right) \simeq \mathsf{isProp}(B). $$

Say that $\Omega$ and $\top : \Omega$ form a subobject classifier when for every universe levels $i, j$ and type $A : \Type_j$ we have an equivalence $$(A \to \Omega) \simeq \textstyle \sum_{B : \Type_i} \sum_{f : B \to A} \isEmbedding(f).$$ By specializing to the unit type $\mathsf{1}$ we obtain $$ \textstyle \Omega \simeq (\mathsf{1} \to \Omega) \simeq \left(\sum_{B : \Type_i} \sum_{f : B \to \mathsf{1}} \isEmbedding(f)\right) \simeq \hProp_i. $$ Therefore $\Omega$ coincides with all the types $\hProp_i$, which are furthermore equivalent to each other. In other words, having a subobject classifier entail propositional resizing.

Answer 3

The precise answer is going to depend on exactly what formulation you are using of the two definitions, but there are a few things to be aware of in any case.

For any universe $U$ the projection map $\mathsf{hProp}_{\mathcal{U} \bullet} \to \mathsf{hProp}_\mathcal{U}$ from pointed hProps to hProps is always going to be a monomorphism - a monomorphism in the $\infty$-category sense if we define it in an $\infty$-topos, and a monomorphism in the $1$-category sense if we define it in a locally cartesian closed ($1$-)category. Hence there is a classifying map $\chi : \mathsf{hProp}_\mathcal{U} \to \Omega$. In many cases $\chi$ will be an equivalence, but not always:

1. In principle $\chi$ does not have to be surjective - there could be new hProps that don't belong to a given universe $\mathcal{U}$ but only appear later at higher universe levels. In particular, we could be working in a predicative metatheory where propositional resizing does not hold at any universe level. In that case we can define $\mathsf{hProp}_\mathcal{U}$ for each universe $\mathcal{U}$, but the subobject classifier does not exist at all. I'm not that familiar with Lurie's definitions, but I would imagine there's a requirement in the definition of universe that implies $\mathcal{U}$ contains $\Omega$ as an element, and so does contain every hProp.

2. For $\chi$ to be an embedding precisely says that proposition extensionality holds at $\mathcal{U}$: if two hProps are equivalent, then they are equal. For $\infty$-toposes (and internally in HoTT) this is a special case of univalence, and so true. It is not necessarily true in extensional type theory. E.g. in the category of sets, for sets $x \neq y \in V$, the singletons $\{x\}$ and $\{y\}$ are equivalent as hProps (they are both true), but they are not equal as sets, and so not equal as elements of the type $V$ of small sets.