In trying to understand homotopy type theory, I stumbled upon the following silly question, which is likely to be trivial for the experts.

Let $B=\sqcup_{n\in\Bbb N} BS_n$, which I'd like to think of as the categorified version of the natural numbers $\Bbb N$. There is an obvious map $\sigma:B\to B$ that covers the successor map $s:\Bbb N\to\Bbb N$, $s(n)=n+1$.

On the other hand, in Martin-Löf's type theory, there is the inductive type of natural numbers, written as

```
Inductive nat : Type := O : nat | S : nat -> nat.
```

in the syntax of Coq. The induction rule reads

```
nat_rect: forall P: nat -> Type,
x: PO -> ((forall n: nat, Pn -> P(Sn)) -> (forall n: nat, Pn)).
```

Question: Can

`nat`

and`S`

be interpreted as $B$ and $\sigma$? Presumably not, but why so?

In fact, such interpretation is impossible, according to Voevodsky: (1) because `nat`

has contractible components (see `Theorem isasetnat`

here); (2) because `nat_rect`

would cause the fibration $\sigma$ to have a section.

Both arguments elude me, however. (1) just needs better knowledge of Coq and more patience with this new way of writing down proofs than I've developed so far (so I don't follow the proof of his `Theorem isasetifdeceq`

). In (2), I fail to see how `nat_rect`

manages to mention a section of $\sigma$, or even that $\sigma$ must be a fibration. Indeed, let me parse the second line of the induction rule.

```
P: nat -> Type
```

I'm reading this as $p\in Map(B, U)$, where $U$ is a universe.

```
forall n: nat, Pn
```

This is the space of sections of $p^*\xi$, where $\xi$ is the universal fibration over $U$.

```
S: nat -> nat
```

This says $\sigma\in Map(B, B)$.

```
Pn -> P(Sn)
```

And this is $Map(\xi^{-1}(p(x)),\xi^{-1}(p(\sigma(x)))$.

```
forall n: nat, Pn -> P(Sn)
```

Here the previous space of maps needs to be understood as the homotopy fiber of a fibration over $B$. This fibration is $G_\sigma^*(p\times p)^*Map(\xi,\xi)$, where $G_\sigma: B\to B\times B$ is the graph of $\sigma$, $p\times p: B\times B\to B\times B$, and $Map(\xi,\xi)$ is the fibration over $U\times U$ whose fiber over $(X,Y)$ is $Map(\xi^{-1}(X),\xi^{-1}(Y))$. (I understand that fibrations like $Map(\xi,\xi)$ and $\xi\times\xi$ are implicitly postulated by saying that $U$ is closed under products, dependent products, etc.; and these postulates correspond to Martin-Löf's universe formation rules.)

So we end up with the space of sections $Sect(G_\sigma^*(p\times p)^*Map(\xi,\xi))$.

```
(forall n: nat, Pn -> P(Sn)) -> (forall n: nat, Pn)
```

This is $Map(Sect(p^*\xi), Sect(G_\sigma^*(p\times p)^*Map(\xi,\xi)))$. Let me call it $M(p)$.

```
x: PO -> [(forall n: nat, Pn -> P(Sn)) -> (forall n: nat, Pn)]
```

and this is just $Map(\xi^{-1}(p(0)),M(p))$.

It seems to be a bit harder to parse the entire `nat_rect`

; but I don't see how on earth this could help one to find a section of $\sigma$.

yourcategorified natural numbers? I'm simply following the well-trodden path a standard reference for which is Baez-Dolan. In more detail, some people tend to think of '$3$' as the 'equivalence class' of three apples, three pears, etc. Whereas $BS_n$ can be identified with the nerve of the category of $n$-element sets and their isomorphisms, and the universal $n$-fold covering $ES_n\to BS_n$ is the tautological covering over this nerve: the fiber over an object is the $n$-element set represented by this object. $\endgroup$ – Sergey Melikhov Jun 9 '11 at 22:13a(notthe) categorification (there are no articles in my native language, so I don't always get them right without a conscious effort). Also the category $Fin$ may be a better categorification of $\Bbb N$ than the nerve B of isomorphisms of $Fin$, so maybe I should've put 'categorification' in quotes. But in homotopy type theory, a 'categorification' (or '∞-categorification') of $\Bbb N$ should be atype, hopefully with additional structure corresponding to $+$, $∗$ and induction. Should it be sought in Awodey-style, not Voevodsky-style HTT? $\endgroup$ – Sergey Melikhov Jun 10 '11 at 11:132more comments