From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCHZRD56UYLBBG4WVLNQKGQES4IB7XQ@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-io0-x240.google.com (mail-io0-x240.google.com [IPv6:2607:f8b0:4001:c06::240]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 39563f5e for ; Wed, 8 Aug 2018 06:18:04 +0000 (UTC) Received: by mail-io0-x240.google.com with SMTP id p12-v6sf845690iog.8 for ; Tue, 07 Aug 2018 23:18:04 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1533709083; cv=pass; d=google.com; s=arc-20160816; b=Klilww0mjy9WeLUTUp0MhVFMx+YKXns0VqJPkbjdIlYOot7lOOKnbU8YvNWU85f0pj pNkMt2hQKvTjtPHTb38MFiGVAa8bNi3iwkgL18g5KkNl+Z3k75T8Dt5by/pAv3QQYtJo iGyPF4120RIpd61Fd4nMx3D8R+iHgasMsG5crvBw+p4V3NgGA+sdEsxHXjs87dJWSFa3 08NZRcU9G6qGfTxV/oRcrPWksmABDxrFZsIuUzWvyZWSHN3hVYjSCgfkt8qWOl/4il1H v7JggBLqgTiZpHFhenirTOtvsuhfWWK91IvmdLLALZO4HVNj8RXr/I5b8YpNiUTOcANM hHpw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:cc:to:subject:message-id:date:from :mime-version:arc-authentication-results:arc-message-signature :sender:dkim-signature:dkim-signature:arc-authentication-results; bh=JJUkOvxQtOzNjFK4xf15PMMzTfoKictC1o5W+Y81tNk=; b=tqAyPnq+N33nGtQqT7XJzJM+xZwAZ7zLke8nAymjXmT54OQogoyDWfB90bj7BM6UvR McDJaYK6YIJasy/58EozOj9t0xYAM0rdHotckIcsBCfLQz4Oib+QUAgIqw0Ftysv+yPY 0To/jUjEgkgPrUl0gp4VoeDqmlaPF1HHBis2Pl4u5kC5Px+XWNDqz4mS3EFPU0BLlton dVfWKEf2nHtqwkshir4MPCprzX5AzK/dtphNoxq0KGVHqFwS2MhJFh2+rR99MrUk4R1A 5HHdBKjzyWxKAgDBfKLwgHW5Pdx/PbsTsahZY/7U2k+wNdBlM4jc6Uf5zNTl2s4fO9Zs Z1BQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=NtUa03ZK; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4001:c06::22f as permitted sender) smtp.mailfrom=josephcmac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:from:date:message-id:subject:to:cc :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=JJUkOvxQtOzNjFK4xf15PMMzTfoKictC1o5W+Y81tNk=; b=SEuIOVV06H0gbpeb4u00IE7Gx2eSGI0yjbg3sQqPoJdeT8mWvhr6GV5UwH1sgaAhSv 4Egsz7zJcZEs27aiRaibhTgWGb2qd2BuBZyJSepGlvlhrVlPMsn5Ec2q8hHYvjhIKhEi P6kgrvIvYmWbDf+kCM9Kud9iDJYzRwgv4bILDfdQTpIBofYyBPjqgYxSai0Pe0tGIa95 yVSKAZPq1x9nA1F+yu8FSGV2mBs6VgMSVfrnnDpxSUZAsMM8edZ1+vnLMgPha1EjATq4 momOPIEd2Ve1ScYe/nicPTNbPbOHmOljDP0bXpJLfupISFNgs1s43Y1Oi5xk8VQqZQzM hTQg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to:cc:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=JJUkOvxQtOzNjFK4xf15PMMzTfoKictC1o5W+Y81tNk=; b=cqyI9RplXL7PI3W/VueW0TV43uSQyBOZ7xKeCO/E5M2RUpepBV8L4fct+lD5pVSA18 9MbtyhygMSQ8r9wPzaP1LZpbCTVd3oBSHCmp9kZZU6ck5NQKGHZKWNVEgV3riGB9TXWx IOA9q8KkEnsS8Ki6SYraPZJvhGPCh4d20eYRbyCzoKE+hgHbwlytpzoN6z3gO1TeO30n E5foWyeSYsKyG5bt2ut3LCxbka88G8qk4R1hMXOFysALhPnBbxy33CeJfdbF8JEOcEHl pvil83DQFUlQJwJGX8Aa8cLq7x5ZR6sH3RknhUnSyoCwqBq4Nlv5XrWRyyxvflaDrwzc 8JcQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:from:date:message-id:subject :to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:x-spam-checked-in-group:list-post :list-help:list-archive:list-unsubscribe; bh=JJUkOvxQtOzNjFK4xf15PMMzTfoKictC1o5W+Y81tNk=; b=TBenR6UKjJWvqn8f5vnVf658HR8AIY621MzBvHzx21G6ENFdA1pjTxCQ8urMci6kfZ Wow8cfi3woX8lfz2TzVJNqUOQPCSU+Wws8vfWPAUhoA2IckhpR2JAuoo6MM2GIGLe5eZ 4tFZqrh4nTN8CwowBg35dj4Lr7SsflFGDBRbR5dbTpCxojsG1RjSA8S2d4lT36ALVNlI edLghqA+BTe/DQfCyqlNdE0kXbwMxgZbL9kHMZ5VAaHHWPkPNT2/avvFU8rfAQ//3Fmb kjw04M9PT2baNRSi2/GaZpFLYCjCb+lJmHozxPl50FGEWUfAW97jTsOwFJUw1u3KzFxG ueAg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlFTnFNOv/T3sxj30lu+Katbm4NJ6s65M8jwRHLeMg+Ld69397cc NjUNu3q1MAvxF8icQbcFpWo= X-Google-Smtp-Source: AA+uWPzZS+64MKzvctUDgKaWV9IK9Q77xbgMBvjXBkgw2CICgeLagqNFKGEilBV8Z1Ycxguyjf0EIQ== X-Received: by 2002:a02:565d:: with SMTP id o90-v6mr15952jab.2.1533709083438; Tue, 07 Aug 2018 23:18:03 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a6b:ee13:: with SMTP id i19-v6ls665166ioh.19.gmail; Tue, 07 Aug 2018 23:18:03 -0700 (PDT) X-Received: by 2002:a6b:9fc1:: with SMTP id i184-v6mr591240ioe.75.1533709083103; Tue, 07 Aug 2018 23:18:03 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1533709083; cv=none; d=google.com; s=arc-20160816; b=tnhVmFR/yZ+bM2/zeN5iZZ1vl59MeDPNu3VjeRI+qvpNKwqR745DUT1CGSN804LQAh Dztw0LmuSX30aK0use+sCyfoM8pJF3q6HRpLf6C45uHzTl0odSv2BHpoPx8AwDnVPzkl jQpjp9HpMhRIzDc3+OtpSDkPw8E+VZyIrXbX8hb08KYvUiMWubKcKRJ5XF5pRpXz6ZfF 5/8pOMCP9DEWkUEoZ77q+1enir2wwE/taXzpL1oULJD7QkM3RYHeMKtDtqeUkW+0jSrm fJ1m+gq7jf+l6t1f931MCvGcIdhZNQ5VEshnI0aXZkN40fdPFxceKsS4XIlCa+tgD4dP JkCg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:mime-version:dkim-signature :arc-authentication-results; bh=6EhyJw3Vi6vvrIQYYRL+yo+VSY8DXtpnW41n/Ky45Yk=; b=K49jiVJ7TYAXb96Xbz7hzrrbcgBFjUmaSpkAK918zk7nklVyePfo5N3gp8mWv59KQ1 Yc2cY+E4yRsAAAyH7NmStQhPDnP+aFy6g7VgRorPUr2q7gDp9S2HfpzQUzAEaY8VF7JP yISkRuP1tYF7wC7vQct4QaAwCPhcfVV0Bse+ACOhS42yN38amShOLs8Z6XelAr5SdzY7 fHXAZyF+h7B3XD05Ih48NJah2lTN0I+gsWm3QG9nQfnFGVajbmomD0TmdwW3wmfcEmig HbMH/DO7fXF+c0o75EVUZVl7+EB8kr2eGEfdCUFbtLxfVd51dnHCOZKOc0EepJphhehJ 0Gsg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=NtUa03ZK; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4001:c06::22f as permitted sender) smtp.mailfrom=josephcmac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-io0-x22f.google.com (mail-io0-x22f.google.com. [2607:f8b0:4001:c06::22f]) by gmr-mx.google.com with ESMTPS id b190-v6si241350ite.1.2018.08.07.23.18.03 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 07 Aug 2018 23:18:03 -0700 (PDT) Received-SPF: pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4001:c06::22f as permitted sender) client-ip=2607:f8b0:4001:c06::22f; Received: by mail-io0-x22f.google.com with SMTP id l7-v6so941789ioj.1 for ; Tue, 07 Aug 2018 23:18:03 -0700 (PDT) X-Received: by 2002:a6b:9bd1:: with SMTP id d200-v6mr1293402ioe.147.1533709082753; Tue, 07 Aug 2018 23:18:02 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a02:6418:0:0:0:0:0 with HTTP; Tue, 7 Aug 2018 23:18:02 -0700 (PDT) From: =?UTF-8?Q?Jos=C3=A9_Manuel_Rodriguez_Caballero?= Date: Wed, 8 Aug 2018 02:18:02 -0400 Message-ID: Subject: [HoTT] [FOM] Why Voevodsky was concerned about the foundations of the natural numbers? To: fom@cs.nyu.edu Cc: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="00000000000010fd360572e67941" X-Original-Sender: josephcmac@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=NtUa03ZK; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4001:c06::22f as permitted sender) smtp.mailfrom=josephcmac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , --00000000000010fd360572e67941 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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=3D_7uONqXQvp8 Sincerely yours, Jos=C3=A9 M. --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. --00000000000010fd360572e67941 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear FOM = members,=C2=A0

Here is = an speculative hypothesis about Voevodsky's motivations concerning the foundat= ions of natural numbers. It would be interesting to know some opinions abou= t this possibility or new alternative hypothesis. I just try to explain to = myself the following strange quotation from Voevodsky:=C2=A0"CIC [...] has this indu= ction definition scheme which allows you to do things parametrized by natur= al numbers. I think this is wrong, foundationally speaking, in this sense t= hat 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).

<= span style=3D"font-size:12.8px;text-decoration-style:initial;text-decoratio= n-color:initial;float:none;display:inline">I guess that Voevodsky was motiv= ated to worry about the foundations of the natural numbers by his intuition= from elementary topos theory, where a natural number object does not alway= s exist. Indeed, he was motivated by the formalisation of category theory i= n UniMath.

Cultures without nu= mbers, or with only one or two precise numbers, include the Munduruku and P= iraha in Amazonia. Researchers have also studied some adults in Nicaragua w= ho were never taught number words. So, it seems that natural numbers are a = cultural phenomenon of some civilizations rather than a=C2=A0knowledge give= n 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 na= tural numbers.

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

Link to a lecture about the paper:=C2=A0= https://www.youtube.com/watch?v=3D_7uONqXQvp8

=
Sincerely yours,

Jos=C3=A9 M.

=

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
--00000000000010fd360572e67941--