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?
 A: 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).
