[Math] categorifying induction in homotopy type theory

Question

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

Answer 1

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.