From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:aa7:951b:: with SMTP id b27mr17000921pfp.2.1589215338701; Mon, 11 May 2020 09:42:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aa7:9a44:: with SMTP id x4ls47089pfj.9.gmail; Mon, 11 May 2020 09:42:16 -0700 (PDT) X-Received: by 2002:a63:2102:: with SMTP id h2mr15801341pgh.32.1589215336501; Mon, 11 May 2020 09:42:16 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589215336; cv=none; d=google.com; s=arc-20160816; b=ZIs1zi226pb8syDMIPE0hf6xdlsbMylAKeW13kwZxCnhuKhVf72aYSy+keLjQ7vKTM LxgkTdKh6hGIFIgOkTekhwRSyLEenfvRdkyWtmEleScRCSV/sIdKMfJ5EuIUGjNypRGG gV17667tCvAypVezjpwUr4Ta2enXKDnVwqzGvJrukQrqocxVkMSSlvbFRtLgNpTRuT4j cuR6gLKsSNJM0mTPEqVOXy5JTmfOpCfA+qEdIEn0JtE9O2gFr0mmtkkgNZwxkO95UeAZ EzhXoaw2RaJPJswUQe06/i4gtKg5Ov+gRJ7YeiBxe+01tYon1mMv6BVCdK+0JvCFpX19 a95A== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=AY7OJNSHj/YcUtOXz5Sd2iBj1a9BXw39C+CHCVUDlXU=; b=pM61nmm3aycuw0i5MqyAC/TWf/pxupqOTr5MJpQlBY4P0s6vUZozC3tokkaYhX1m4t TaRYPzinQC8COURAdzkqpFO9xomgDNv10cVBkCpW+Gt7bTmMzSqeNsnfGvfILB1MORD+ 2QHe/bMWeE3XvR9d7OMLYLJ9L+l6Xn6Dko1PrIR5ZFpmbeb4rpqCg0G5g3zI21ohO6uX j6BW91r68N+E0f6xs7t9o8nLc3JB7TSc6IzNIps6wXDABpEjsKlmq9JaPFMZTi8u08Jj 1znEL9sdBYt+kjVKR/Ypb9skR5xm8ec750W/Hm6C9k7Tc7NYik8pbF1aXyV+0/ODIea0 3T0g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=WLHzDFxY; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::336 as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Return-Path: Received: from mail-ot1-x336.google.com (mail-ot1-x336.google.com. [2607:f8b0:4864:20::336]) by gmr-mx.google.com with ESMTPS id a95si1338923pje.1.2020.05.11.09.42.16 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 11 May 2020 09:42:16 -0700 (PDT) Received-SPF: pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::336 as permitted sender) client-ip=2607:f8b0:4864:20::336; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=WLHzDFxY; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::336 as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: by mail-ot1-x336.google.com with SMTP id i27so8046963ota.7 for ; Mon, 11 May 2020 09:42:16 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=AY7OJNSHj/YcUtOXz5Sd2iBj1a9BXw39C+CHCVUDlXU=; b=WLHzDFxYFdJ8AQQeg/NCSZBNbMRTiTl87Ko3fsFVGtTuy1nv0fremWdsfJbQrY2GIj b3shW1AV5oyyBWWAzij4MnwoNyDVu8oS/Jc4jN03Zh5O+0Kuay3CoOoh+7ybgnoD/MDa ZVHzcBLqFA/WOsI2QnSe1/F0kDACDU8A9t/wQB3V38TDUjjZ8fWjbhvCkDnAwwhbAiYv lm3qp/5cGBo1hfWdcKEGytMGv1ZVOwFnOJeqn7uOjVJY3CJh8FbBiAopKxYuknYRY3h9 K/CvNvomnFuuE0Y+sh5+2gnFXoTPfUVPJqDcfvYpHbXXJTg/HeHPvaiGP52N1YUk29bI 3AfQ== X-Gm-Message-State: AGi0PuaH0wFnhJZu61B272E0GOsE76HzOgGDKC9eLZ+O7WDVX6YcKYC6 12vZKWyGxj+9BFSax5T0Y52OJ9znxygLc71zl8dif/0VfYpLLiIxGTOJl/USIaR4PL3Gi99uwbK SX8JwmyD7i9zdVdDVHBuT09hjV4aHLRP+6BzF4Anz8oWfA4kv7LvRAdlmyYWt0yXPwmoCmFR39C 7y8LV2vNhl X-Received: by 2002:a05:6830:1e39:: with SMTP id t25mr13187034otr.114.1589215334670; Mon, 11 May 2020 09:42:14 -0700 (PDT) Return-Path: Received: from mail-oi1-f171.google.com (mail-oi1-f171.google.com. [209.85.167.171]) by smtp.gmail.com with ESMTPSA id m63sm149816otm.21.2020.05.11.09.42.13 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 11 May 2020 09:42:13 -0700 (PDT) Received: by mail-oi1-f171.google.com with SMTP id t199so15683836oif.7 for ; Mon, 11 May 2020 09:42:13 -0700 (PDT) X-Received: by 2002:aca:f541:: with SMTP id t62mr19581618oih.148.1589215333427; Mon, 11 May 2020 09:42:13 -0700 (PDT) MIME-Version: 1.0 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> <0388695a1dfc717f9c5e458937dff760.squirrel@webmail.mathematik.tu-darmstadt.de> In-Reply-To: <0388695a1dfc717f9c5e458937dff760.squirrel@webmail.mathematik.tu-darmstadt.de> From: Michael Shulman Date: Mon, 11 May 2020 09:42:00 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Identity versus equality To: Thomas Streicher Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable FWIW there is no trouble at all with "internal categories" in HoTT; they just correspond to (pre)categories in the smallest universe. Some of them will naturally be univalent categories, while others will naturally be strict categories. If we want to "do category theory" with the latter we can Rezk-complete them to univalent ones, but sometimes this is unnecessary, e.g. if our goal is to talk about "internal presheaves" on them then these are just contravariant functors to the (univalent) category Set, and the universal property of Rezk-completion says that it doesn't matter whether or not we Rezk-complete the domain before talking about presheaves. In addition, we get the bonus that when talking about univalent categories internally we are externally talking about *stacks*, with the "weak equivalences" automatically inverted (but if for some reason we don't want to do that, we can stick with strict categories). On Mon, May 11, 2020 at 9:37 AM wrote: > > > Thank you for pointing out the case of the universe of constructible se= ts > > 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=C3=B6del 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 form= al > > 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 inconsequ= ent > but nobody is perfect :-) > > Thomas > > -- > 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 HomotopyT...@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/0388695a1dfc717f9c5e458937dff760.squirrel%40webmail.ma= thematik.tu-darmstadt.de.