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](https://mathoverflow.net/questions/4841) 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](https://raw.github.com/vladimirias/Foundations/master/Main_Library/Generalities/uu0.v)); (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$. 



categorifying induction in homotopy type theory
The first reason you give is sufficient to answer your question: any interpretation of `nat` (and any other type with decidable equality) must have contractible components. Let me try to unpack the proof:


The proof of `isasetifdeceq` goes as follows: Fixing $x:X$, we must show that $\text{Paths}(x,x)$ is contractible. We know that $\Sigma\_{x':X}\text{Paths}(x,x')$ is contractible, so we just need the natural map $f:\text{Paths}(x,x)\to\Sigma\_{x':X}\text{Paths}(x,x')$ to be a weak equivalence. This follows from the hypothesis using the theorem `onefiber`, which establishes that for a fibration which is empty over all but one path-component of the base, the total space is equivalent to a fiber over the remaining component.


Regarding (2). I think there's some confusion here: Let me try to unpack `nat_rect` in a more direct way: For any fibration $\Sigma\_{\text{nat}} P\to\text{nat}$ over `nat`, given a point in $P\_0$ and a section of $\Pi\_{n:\text{nat}}\text{Map}(P\_n,P\_{n+1})\to\text{nat}$, you get a section of $P$. That is the interpretation of primitive recursion/induction.


