2
$\begingroup$

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?

$\endgroup$
0

1 Answer 1

5
$\begingroup$

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).

$\endgroup$
1
  • 1
    $\begingroup$ Thanks, this clears things up! It seems my flawed intuition came from a naive understanding of the category of sets. $\endgroup$
    – Couchy
    Apr 3, 2019 at 1:10

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .