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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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