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 integersnatural 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$? If Presumably not, but why so?

In fact, according to Voevodsky, 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 p\in Map(B, U)$, where $U$ is a universe.

forall n: nat, Pn 

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

S: nat -> nat 

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

Pn -> P(Sn) 

And this is $Map(\xi^{-1}(P(n)),\xi^{-1}(P(S(n)))$.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_S^*(P\times P)^*Map(\xi,\xi)$G_\sigma^*(p\times p)^*Map(\xi,\xi)$, where $G_S: G_\sigma: B\to B\times B$ is the graph of $S$, \sigma$, $P\times Pp\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_S^*(P\times P)^*Map(\xi,\xi))$Sect(G_\sigma^*(p\times p)^*Map(\xi,\xi))$.

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

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

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

and this is just $Map(P(0),M(P))$.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$.

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 integers, 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$? If not, why so?

In fact, according to Voevodsky, such interpretation is impossible: (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 $S\in Map(B, B)$.

Pn -> P(Sn) 

And this is $Map(\xi^{-1}(P(n)),\xi^{-1}(P(S(n)))$.

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_S^*(P\times P)^*Map(\xi,\xi)$, where $G_S: B\to B\times B$ is the graph of $S$, $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_S^*(P\times P)^*Map(\xi,\xi))$.

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

This is $Map(Sect(\eta), Sect(G_S^*(P\times P)^*Map(\xi,\xi)))$. Let me call it $M(P)$.

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

and this is just $Map(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$.