# Subobjects in Homotopy type theory

It is conjectured here that homotopy type theory is the internal language of an elementary $$(\infty,1)$$-topos. I have no idea what these are, but my naive understanding is the following:

Homotopy type theory is the internal language of an elementary topos, so in particular we should have a subobject classifier $$1\to\Omega$$, where we have in this case $$\Omega \equiv \text{Prop}$$, and for any type $$X$$ we should have an isomorphism of sets (in the meta language)

$$\phi:\text{hom}(X,\Omega) \cong \text{Sub}(X).$$

In particular (now in the language of HoTT), a map $$P:X\to \text{Prop}$$ should correspond uniquely to a subtype $$\Sigma_{x:X}P(x)$$.

However if we take $$2 = 1 + 1$$ $$A = \Sigma_{x:2}(x =_2 \text{inl}(*))$$ $$B = \Sigma_{x:2}(x =_2 \text{inr}(*))$$

then I expect $$A$$ and $$B$$ should be distinct types, however both are contractible so $$A\simeq B\simeq 1$$, and by univalence $$A = B = 1$$.

It seems to me that either my interpretation of HoTT as the internal language of a topos is incorrect, or the construction $$\Sigma_{x:A}P(x)$$ is not the subobject corresponding to $$P:A\to\text{Prop}$$.

Where am I going wrong?

What's wrong is your expectation that $$A$$ and $$B$$ should be distinct types. As you observe, in fact $$A=B=1$$ so they are not distinct. (-:
Perhaps what you expect is that $$A$$ and $$B$$ are distinct subtypes of $$2$$. And they are indeed, but as abstract types with their inclusion into $$2$$ forgotten they are the same. This distinction is nothing special to HoTT but arises already in 1-topos theory: the two monomorphisms $$1 \rightrightarrows 2$$ are distinct subobjects, in that they are not isomorphic in the slice category over $$2$$, but their domain objects are isomorphic if we forget about their inclusions into $$2$$.
In HoTT we have an additional way to represent subobjects: in addition to monomorphisms, we can talk about predicates $$P:A\to \rm Prop$$. The monomorphism corresponding to such a $$P$$ is the first projection $$(\sum_{x:A} P(x))\to A$$. Distinct predicates can therefore give rise to monomorphisms that are distinct as subobjects, i.e. not isomorphic in the slice category over $$A$$, and yet their domain objects $$\sum_{x:A}P(x)$$ and $$\sum_{x:A} Q(x)$$ may nevertheless be abstractly isomorphic (hence, by univalence, equal).