7
$\begingroup$

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

Improve this question
$\endgroup$
7
  • 4
    $\begingroup$ I don't quite understand why you wish to think of the sum of $BS_n$ as the categorified natural numbers. I am far more accustomed to seeing $BS_n$ as a categorified reciprocal whose decategorified shadow is $1/n!$, so that the sum of the $BS_n$ is a categorification of $e$, and the functor which takes a space $X$ to the space obtained as a sum of $E S_n \otimes_{S_n} X^n$ is a categorified exponential $\exp(X)$. $\endgroup$
    – Todd Trimble
    Commented Jun 9, 2011 at 18:15
  • $\begingroup$ Todd, then what is your categorified 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
    Commented Jun 9, 2011 at 22:13
  • 2
    $\begingroup$ Sergey, I didn't mean to seem aggressive here; I just wanted to understand your point of view. (I also acknowledge that there is more than one answer, depending on what one wants.) My first response is: $Fin$, the category of finite sets, which as a category with products that distribute over coproducts, decategorifies to the rig $\mathbb{N}$. But this suggests to me another way to interpret your meaning: just as $\mathbb{N}$ is the free commutative monoid on one generator, so the groupoid $\sum_n S_n$ is equivalent to the free symmetric monoidal category on one generator. No worries then.:-) $\endgroup$
    – Todd Trimble
    Commented Jun 9, 2011 at 23:02
  • 1
    $\begingroup$ What is the 'obvious' map $\sigma$? I guess it corresponds to a choice of inclusion $S_n \hookrightarrow S_{n+1}$ for each $n$. But I would wonder if there are any coherence conditions lying around. For example we know that $(0,s):1+\mathbb{N} \to \mathbb{N}$ is an isomorphism. I don't expect this be echoed in your $B$ above, but I feel there could be something lying around... (and I echo Todd's sentiment that categorification is an art, and so goes down various paths). $\endgroup$
    – David Roberts ♦
    Commented Jun 10, 2011 at 2:01
  • $\begingroup$ Todd and David, I agree, it should have been, a (not the) 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 a type, hopefully with additional structure corresponding to $+$, $∗$ and induction. Should it be sought in Awodey-style, not Voevodsky-style HTT? $\endgroup$
    – Sergey Melikhov
    Commented Jun 10, 2011 at 11:13

1 Answer 1

Reset to default
7
$\begingroup$

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.

Improve this answer
$\endgroup$
6
  • 1
    $\begingroup$ Thanks, Ulrik! With your comments, I seem to understand the proof of isasetifdeceq now, but I'd say that semantically, it's an incredible kind of reasoning! The law of excluded middle, or 'decidable equality', is stated as saying that either there is a path between x and x' or there's no path between them; now the latter assertion also has another meaning: the path fibration, sending to x' every path from x to x' is empty over all components except that of x. Then the topological observations you mentioned apply. Correct me if I'm wrong, but this is the first time I see a topological ... $\endgroup$
    – Sergey Melikhov
    Commented Jun 9, 2011 at 21:36
  • $\begingroup$ ... thinking have some application to logic, and not just providing an interpretation of what is already known in logic. It's a pity that there seems to be no more human-readable exposition of this argument. I'll need to think it all over to see what is going on here (in particular in my example with $B$ and $\sigma$). $\endgroup$
    – Sergey Melikhov
    Commented Jun 9, 2011 at 21:42
  • $\begingroup$ Regarding (2), I certainly started from your 'unpacking', and I now regret that I didn't mention it in the first place, so as to improve presentation. But your unpacking is incomplete, as it still contains quantifiers and connectives ("for any fibration", "given a point", "AND a section"), which in particular conceals that these quantifiers are to be understood constructively. I just tried to do a more complete unpacking. In any case, do you agree that there is something wrong with argument (2)? $\endgroup$
    – Sergey Melikhov
    Commented Jun 9, 2011 at 21:56
  • 3
    $\begingroup$ I agree it's an incredible kind of reasoning - that's part of the fun! And you're right that to give a full unpacking we have to interpret Type by a univalent universe, $U$, with corresponding fibration $\Sigma_{A:U} T(A)\to U$ (universe a la Tarski with decoding $T$). And then nat_rect is represented by a section of a certain fibration with base space $\text{Map}(\text{nat},U)$. But it's frankly easier to understand in the type-theoretic notation, remembering to understand constructs constructively/continuously. $\endgroup$
    – Ulrik Buchholtz
    Commented Jun 10, 2011 at 6:05
  • $\begingroup$ As for (2): The argument you refer to doesn't make much sense to me, since $\sigma$ is not interpreted as a fibration, so why does the question arise as to whether it has a section? That's why I suggested there might be some confusion going on – although I'm probably also confused :-) $\endgroup$
    – Ulrik Buchholtz
    Commented Jun 10, 2011 at 6:09

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .