From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a1c:2d0e:: with SMTP id t14mr33152853wmt.153.1589215067635; Mon, 11 May 2020 09:37:47 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6000:8d:: with SMTP id m13ls7297608wrx.4.gmail; Mon, 11 May 2020 09:37:46 -0700 (PDT) X-Received: by 2002:a05:6000:8:: with SMTP id h8mr21030483wrx.372.1589215065914; Mon, 11 May 2020 09:37:45 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589215065; cv=none; d=google.com; s=arc-20160816; b=hb479lqQP2PDCW/GGRi27y8zWhs9E+eKNB7txGBcFa/v89twDbI/GG11K1sYVuY8JV T+X6Y0/k5w2LWTE+6dyE4AfW5IhKVm8NAkaCpprA81ptazVWdkHnsjcuAQ9NxpZWfWPx Ae7GnPIKhdRNLTwZl9smWmmbQVN4jiBDZdi78JhJtZYE1aDATxPvHRgocPDrrLhqvoR5 pBoJVMEfcBSMtoVwQ8oyEKaH9g5pPmMkeWx10nBm6c8Zu7faB+26wcJwVVbWNG24Q1Jx jD4+pCJXM4D6kXweiOaLCirtPR/rcxraFYFqBPX4gTxA6nRNIMG3r+IgMwcYkOvsLsxd ddgw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=importance:content-transfer-encoding:mime-version:user-agent:cc:to :from:subject:date:references:in-reply-to:message-id; bh=LhTu3YDfP6VtqwFy8yYFqniTf3D9GAOq/Th4HUE5uqE=; b=ZQSCLv5hIPEdPDgC32vc8YxbH9mroUnkSdQeGnBYmgn/RsBZqA/pb24T4UBThmKg9o oR3DvT3vRMGWLnRW6m5eM8/02qlyCoyCzaqUTc+kniCc0X/hoWxoqMQB5UMwXrcRf3zE HX/x/a77XvBT/yAz8sxD29mCwVIWukoRH4Hw0+V6U//wFgbT2D2tR2BK26LYDY22g8JV sMMd3CTWy7dOItY7iQwaXg6rsPQz+ASYpGe75qu1AeQhJLq/eJjwmJprvVQpeQiobN4h cHHmH+QPZzLnBpeN6GlCAV6MpeswdewZj/GcHyjkL8n+EitOIstqvlL5eRcBjsNdUD5x rHug== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.233 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Return-Path: Received: from mail-relay232.hrz.tu-darmstadt.de (mail-relay233.hrz.tu-darmstadt.de. [130.83.156.233]) by gmr-mx.google.com with ESMTPS id u16si1079254wmd.2.2020.05.11.09.37.45 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 May 2020 09:37:45 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.233 as permitted sender) client-ip=130.83.156.233; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.233 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client CN "mail.mathematik.tu-darmstadt.de", Issuer "DFN-Verein Global Issuing CA" (verified OK)) by mail-relay232.hrz.tu-darmstadt.de (Postfix) with ESMTPS id 49LRS844d3z43p9; Mon, 11 May 2020 18:37:44 +0200 (CEST) Received: from webmail.mathematik.tu-darmstadt.de (fb04277.mathematik.tu-darmstadt.de [130.83.2.17]) by fb04281.mathematik.tu-darmstadt.de (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id 04BGcSIT013194; Mon, 11 May 2020 18:38:28 +0200 Received: from 79.233.167.171 (SquirrelMail authenticated user streicher) by webmail.mathematik.tu-darmstadt.de with HTTP; Mon, 11 May 2020 18:37:42 +0200 Message-ID: <0388695a1dfc717f9c5e458937dff760.squirrel@webmail.mathematik.tu-darmstadt.de> In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F5861@Pli.gst.uqam.ca> References: <8C57894C7413F04A98DDF5629FEC90B1652F53A3@Pli.gst.uqam.ca> <20200508064039.GC21473@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca> <20200509082829.GA8417@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F55C8@Pli.gst.uqam.ca> <20200509184313.GB28841@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F563A@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B1652F5753@Pli.gst.uqam.ca>,<20200511073332.GA30513@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F5861@Pli.gst.uqam.ca> Date: Mon, 11 May 2020 18:37:42 +0200 Subject: RE: [HoTT] Identity versus equality From: stre...@mathematik.tu-darmstadt.de To: =?iso-8859-1?Q?=22Joyal=2C_Andr=E9=22?= Cc: "Thomas Streicher" , "Ulrik Buchholtz" , "Homotopy Type Theory" User-Agent: SquirrelMail/1.4.21 MIME-Version: 1.0 Content-Type: text/plain;charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Priority: 3 (Normal) Importance: Normal > Thank you for pointing out the case of the universe of constructible sets > L. > It is internal to ZF because it is was constructed from ordinals in ZF. > Could it be also external to ZF ? Anything internal can be externalized but not the other way round. The point I tried to make was that in the usual models of 2-level type theory the homotopical part is not internal to the ambient nonhomotopical part. > Gödel thought that ordinals and sets are real, like matter, but of a > different kind. > He was the first to use the full power of mathematics for studying formal > logic. > Most logicians believe that natural numbers are real. > They use natural numbers and induction for studying formal systems. Indeed, Goedel was the first one who took serious the difference between syntax and semantics. This was crucial for his findings. That he nevertheless was a dyed in the wool Platonist was a bit inconsequent but nobody is perfect :-) Thomas