9
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ What does "these" refer to in "are these isomorphic"? To me it looks like you're attempting to compare the object $\Omega$ in a topos with the type $\mathrm{hProp}$ in type theory, so I must be misreading the question. $\endgroup$ Commented Oct 6, 2022 at 15:37
  • $\begingroup$ Perhaps your question is: if a topos is construed as an $(\infty, 1)$-topos, does its subobject classifier coincide with the interpretation of $\mathrm{hProp}$ in the $(\infty, 1)$-topos? $\endgroup$ Commented Oct 6, 2022 at 15:39
  • $\begingroup$ Well the definition of hProp in type theory can be interpreted in an $(\infty, 1)$-topos and I believe in a 1-topos as well and my question is if that constructed object is isomorphic/equivalent to the subobject classifier. $\endgroup$
    – Max New
    Commented Oct 6, 2022 at 15:58
  • 1
    $\begingroup$ I would conjecture that $\mathrm{hProp}$ is equivalent to $\Omega$ whenever $\Omega$ happes to exist. $\endgroup$ Commented Oct 6, 2022 at 20:51
  • $\begingroup$ See section 3.5 of HoTT book, it's somewhat relevant. But I still don't understand what precisely you're asking. Is this a question about homotopy type theory or $(\infty, 1)$-toposes? A bit more technical clarity would help, as then we could arrive at a precise question. $\endgroup$ Commented Oct 7, 2022 at 7:46

3 Answers 3

4
$\begingroup$

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.

$\endgroup$
9
$\begingroup$

$\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.

$\endgroup$
3
  • $\begingroup$ So my one worry about this is that this is an internal definition of an embedding classifier, so do we know that this is equivalent to the external definition of a subobject classifier as classifying monomorphisms? (Forgive me if these are obviously equivalent in this case) $\endgroup$
    – Max New
    Commented Oct 7, 2022 at 13:04
  • $\begingroup$ If you postulate the definition of a subobject classifier as a schema, using rules of inference with a type metavariable $A$, then you can still show it to be equivalent to each $\mathsf{hProp}_i$ by instantiating the schema at $\mathsf{hProp}_i$. So the (weaker) external version is also good enough. $\endgroup$ Commented Oct 7, 2022 at 14:09
  • 1
    $\begingroup$ The remaining question is whether the equivalence between $A \to \Omega$ and the type of embeddings into $A$ actually captures the intended notion (a priori it might be too strong because it's internal). One would have to look at what the $(\infty,1)$-topos-theoretic notion of a subobject classifier is. $\endgroup$ Commented Oct 7, 2022 at 14:20
4
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.