[HoTT] [FOM] Why Voevodsky was concerned about the foundations of the natural numbers?

["José Manuel Rodriguez Caballero" <josephcmac@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2033 bytes --]

Dear FOM members,

Here is an speculative hypothesis about Voevodsky's motivations concerning
the foundations of natural numbers. It would be interesting to know some
opinions about this possibility or new alternative hypothesis. I just try
to explain to myself the following strange quotation from Voevodsky: "CIC
[...] has this induction definition scheme which allows you to do things
parametrized by natural numbers. I think this is wrong, foundationally
speaking, in this sense that CIC is not cleanly defined, because it is an
initial model of a theory which itself requires natural numbers to be
specified" (Univalent Model Talk at CMU, Feb. 4, 2010).

I guess that Voevodsky was motivated to worry about the foundations of the
natural numbers by his intuition from elementary topos theory, where a
natural number object does not always exist. Indeed, he was motivated by
the formalisation of category theory in UniMath.

Cultures without numbers, or with only one or two precise numbers, include
the Munduruku and Piraha in Amazonia. Researchers have also studied some
adults in Nicaragua who were never taught number words. So, it seems that
natural numbers are a cultural phenomenon of some civilizations rather than
a knowledge given a priori. In Jean Benabou's language, the word "very" is
a sort of fossil from a time when the Western civilization didn't have
natural numbers.

Reference: Benabou J, Loiseau B. Orbits and monoids in a topos. Journal of
Pure and applied algebra. 1994 Feb 18;92(1):29-54.

Link to the paper: https://core.ac.uk/download/pdf/82030505.pdf

Link to a lecture about the paper: https://www.youtube.
com/watch?v=_7uONqXQvp8

Sincerely yours,

José M.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 4157 bytes --]