From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a9d:67c2:: with SMTP id c2mr11844860otn.227.1589208885915; Mon, 11 May 2020 07:54:45 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6830:1de1:: with SMTP id b1ls2067415otj.9.gmail; Mon, 11 May 2020 07:54:44 -0700 (PDT) X-Received: by 2002:a9d:7a8a:: with SMTP id l10mr12496437otn.302.1589208884703; Mon, 11 May 2020 07:54:44 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589208884; cv=none; d=google.com; s=arc-20160816; b=VPf5P7NaSmaChx6kAUXkgYYj1hHLHu7YbMyPEo5chedByE6C5PUybwcrfbjXAIiUY3 TiAsN1rk64qFEeb2NH5as3jDS4KnR5W/6r3tjGUbdDSI5zT7PRvMlmPsxIgrb6/0HQmH LUnB+6KqEnycGaFQZcwfTSCTTahvZNYwT/ZZmay0jOSKQFtv5/xyolPsQpOfVTScyf2Q EZ79iObzn45LHKXmsoLiB9+zMAPPLhdRnFqcEisSEz1dx08+ZYKkFmSzUzE3B6RzEFDT byVrEIK3qoR77ro8VxPlE/7fDG8CnvecYu9K5HbV0sO7/QuvWWa/SYPfKSvhlDvxz3lq qCDg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:ironport-sdr; bh=jpZc8wKzWM/IAQwHnKNENcyrfUep5R2gbEGYmBd9f5s=; b=Rpwch5dFTePeucZ9ylKWHO+KJ4FPzfzO3ZqHrVdprxUzXnnF82ijZRjmUS7RQ2CuW3 7hU9gc9ItJHX10VYvJgsKpx81V7od87mT/nJjq8rUzQkprXWdiyoJezxnJTwhqQ4q+oc V+Z9SDfV18PljXbegiVIL85EyZ369iDHm9aL36BJkxHgTLnwrVbQeNxQyhfOnBhpY6TN 1I25jmo4ezUmJr3rDgQJPq1jOKUYc2cLsoFRUWiOs5t8jl7V/AU1yPKHlpiRGKz/W82P 2GQuViraWAZ9CgEZ9/9xJHDhPam6zK83m2nJuuP1cllBRdJZqjshdA1pmAyHOqfCKHCq fabA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.108 as permitted sender) smtp.mailfrom=joyal...@uqam.ca Return-Path: Received: from mail5.uqam.ca (mail5.uqam.ca. [132.208.246.108]) by gmr-mx.google.com with ESMTP id x23si28669otq.4.2020.05.11.07.54.44 for ; Mon, 11 May 2020 07:54:44 -0700 (PDT) Received-SPF: pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.108 as permitted sender) client-ip=132.208.246.108; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.108 as permitted sender) smtp.mailfrom=joyal...@uqam.ca IronPort-SDR: Yi5G9uZWljpM25jWQoj1vxCFiO5vZHgqRlRaz+mSmFJd54NivedchM/x2zj9TRpATooV9owmHf GCClbJQKEp0scoDSUSNiY8/ItoH4FY4e/8I3Z4gib3kiH2+WMUBmwKNU3qH6ZOo4VqjefA6TAb G1XD0NiGHQAYYMCy/ptBFYMYx8Z0gq621J5lLeyTEiAgfzoTEg/IEy/qTEJsR2TH2JdPpCJ2es XuT+rDjXi9MFPNX6WAzp0EvlI7gzVyy/oFP/Vcc7XR+Sk9JXfAAkPXC7N5MCZdso0drD4iuLWK YLM= X-IronPort-AV: E=Sophos;i="5.73,380,1583211600"; d="scan'208";a="12051173" Received: from unknown (HELO Message.gst.uqam.ca) ([132.208.216.70]) by mail7.uqam.ca with ESMTP; 11 May 2020 10:54:26 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.153]) by Message.gst.uqam.ca ([169.254.1.218]) with mapi id 14.03.0439.000; Mon, 11 May 2020 10:54:25 -0400 From: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= To: Thomas Streicher CC: Ulrik Buchholtz , Homotopy Type Theory Subject: RE: [HoTT] Identity versus equality Thread-Topic: [HoTT] Identity versus equality Thread-Index: AQHWIrnt2rpL+UtjL0e4oihqoDCB+qibJxGOgACIG4CAAAS1AIAAPFAA//+/ZaSAAMfxgIAANUUAgAAO4LWAALJlgP//xKOFgABhQICAAHDSgIAAmhfJgAEWX4CAAC1BFIAAfoCA///K+0gALLNAgP//8k6KgAFGqwCAADAztQ== Date: Mon, 11 May 2020 14:54:25 +0000 Message-ID: <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> In-Reply-To: <20200511073332.GA30513@mathematik.tu-darmstadt.de> Accept-Language: en-US, en-CA Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [132.208.216.80] Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 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 ? G=F6del thought that ordinals and sets are real, like matter, but of a diff= erent kind.=20 He was the first to use the full power of mathematics for studying formal l= ogic. Most logicians believe that natural numbers are real.=20 They use natural numbers and induction for studying formal systems.=20 Best, Andr=E9 PS: It is not easy to stop participating to this interesting discussion! ________________________________________ From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] Sent: Monday, May 11, 2020 3:33 AM To: Joyal, Andr=E9 Cc: Ulrik Buchholtz; Homotopy Type Theory Subject: Re: [HoTT] Identity versus equality Dear Andr"e, the exo/endo distinction is different from external/internal. It is like L in set theory ZF which does not allow one to prove consisteny of ZF. (An aside: why do internal cats play such an important role in traditional topos theory and are evil in Hott?) Thomas