From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.7 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,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.2 Received: from mail-oi1-x23a.google.com (mail-oi1-x23a.google.com [IPv6:2607:f8b0:4864:20::23a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 1adbbfd7 for ; Thu, 20 Jun 2019 16:16:39 +0000 (UTC) Received: by mail-oi1-x23a.google.com with SMTP id u200sf1504373oia.23 for ; Thu, 20 Jun 2019 09:16:39 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=9JCA+ewF0rUFeBxK8Wywk4qrXOtTzG579RTu1uTYIDQ=; b=b8WQFDW+ZLrzL77ekcM0G2bK2KhsiRtPw9bXwiJw9JLDNrd6QjaMbCE2QJpaLA6DQr cw4i6ozqDvFskhtFqDxZx6VUVQPCs/Vp0ecS3kuY09EI/tV05Oz7++tnv4guCV5x45rs +HK3WpUMhf0CzxKbNbj9hHRl3emRk6MQYekWeOwSZ1sGVcTfTiDnSrHqcqdQVUwJ+n/p /+WsZ8TceNbjz5C/Fl7puEe3seFgRgAf2AEZn5PRQbkZCe5lve+VChYI770UwuetQ3Re TGInQBGa5JrUoTUcVW/UV3a1jcGm7wMJ9Q1/zHksjgNJ7qqGSu0g2tLxIIBwCXTWgtht 4PpQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=9JCA+ewF0rUFeBxK8Wywk4qrXOtTzG579RTu1uTYIDQ=; b=MW/yqIitAcTY4yLTjd2K5c1x5r6jFczcy5Uyp38geohvaZR3COkUd0/0a+bVhRPcsF 3/+wKrO57fAz1yrC1QeB1OcAoKdyKAJP0s/urd53ydwkeZUv9aRwsfTTCrnzjrgx8MeP 2aZPex3giNCcteM6Kk0jknjqpwrjSZdwGLK3ixIwNxXdQj6AtTqNmb1F61/fMnq7AuG8 lrcuq8JF3p5StLtY0PRiI5MTsOvtd+aYORRgXY2xdQ43Hh8ZO35F57W5IzIZchpEBQCl NxjXtgntU9dL5F1PSGHncvCyV5FklzcTai6TWFmha23wOBXMwbx/hFV3fs86qgJE2H/e fawQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=9JCA+ewF0rUFeBxK8Wywk4qrXOtTzG579RTu1uTYIDQ=; b=dF8S882ewLmQhPLwyQ0AWRDp1EpSpGAtsq+zDPHOPW65yjx+4fu7RevbPAHB4B8SQm 8oLqLVOdTu+f9QAFC1p0wNQ68oYiDrdX50/KLR4fDvdUxUpCJWNvXvbAo8ju56S143ww WhlDwUuQhmw5EElT3JpKF8/gar+bwErElELUhHpp1oHhcoCZUOpWacC1vQ5HI9NUJOWy aXw/NCB2DQzB92CBIV7lADW2gHTK1CxmKZO02D9H4F9JkVckvJC43nh/iA5oQufn7r6o TFAuNPxr49nnF9BV2/jXX3aZE9RVJxCdua0P0xHR7/CwPPxutFs49CK6OoWJpt02SSMw 9PMQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUGX704wBlVCk7ioNQoTEweW+2rZfL9f8NaS0VhIVHkENSDidxG JJBK1w8Q/vGtop3jjHPkuhg= X-Google-Smtp-Source: APXvYqz7hRGPOeiKazY5NuLk3sRi+4sfAcqd0462E7qoQk9zh8y04Fbp0qESrMe24EWhzv/aanHsAw== X-Received: by 2002:a9d:6394:: with SMTP id w20mr14837174otk.151.1561047397322; Thu, 20 Jun 2019 09:16:37 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:3fc3:: with SMTP id m186ls979035oia.15.gmail; Thu, 20 Jun 2019 09:16:36 -0700 (PDT) X-Received: by 2002:aca:3809:: with SMTP id f9mr6325239oia.119.1561047396562; Thu, 20 Jun 2019 09:16:36 -0700 (PDT) Date: Thu, 20 Jun 2019 09:16:35 -0700 (PDT) From: Nathan Carter To: Homotopy Type Theory Message-Id: Subject: [HoTT] my first 3 questions about HoTT MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2264_1191050770.1561047395850" X-Original-Sender: nathancarter5@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: , ------=_Part_2264_1191050770.1561047395850 Content-Type: multipart/alternative; boundary="----=_Part_2265_237964951.1561047395850" ------=_Part_2265_237964951.1561047395850 Content-Type: text/plain; charset="UTF-8" Hello, HoTT community. I've learned a bit about HoTT in bits of spare time over the past few years, and have come up with some questions I can't answer on my own. It was suggested that I ask them on this list. I will start with a few small questions, and if anyone in the community here has time to answer them, then I'll continue with others as needed. Thank you in advance for any help you can give. (Where I'm coming from: I'm a mathematician; my dissertation was on intermediate logics, but I haven't focused on logic much for the past 15 years, instead doing mathematical software and some applied mathematics. I have a passion for clear exposition, so as I learn about HoTT, I process it by writing detailed notes to myself, explaining it as clearly as I can. When I can't explain something clearly, I flag it as a question. I'm bringing those questions here.) Here are three to start. 1. Very early in the HoTT book, it talks about the difference between types and sets, and says that HoTT encourages us to see sets as spaces. Yet in a set of lecture videos Robert Harper did that I watched on YouTube (which also seem to have disappeared, so I cannot link to them here), he said that Extensional Type Theory takes Intuitionistic Type Theory in a different direction than HoTT does, formalizing the idea that types are sets. Why does the HoTT book not mention this possibility? Why does ETT not seem to get as much press as HoTT? 2. When that same text introduces judgmental equality, it claims that it is a decidable relation. It does not seem to prove this, and so I suspected that perhaps the evidence was in Appendix A, where things are done more formally (twice, even). The first of these two formalisms places some restrictions on how one can introduce new judgmental equalities, which seem sufficient to guarantee its decidability, but at no point is an algorithm for deciding it given. Is the algorithm simply to apply the only applicable rule over and over to reduce each side, and then compare for exact syntactic equality? 3. One of my favorite things about HoTT as a foundation for mathematics actually comes just from DTT: Once you've formalized pi types, you can define all of logic and (lots of) mathematics. But then the hierarchy of type universes seem to require that we understand the natural numbers, which is way more complicated than just pi types, and thus highly disappointing to have to bring in at a foundational level. Am I right to be disappointed about that or am I missing something? Thanks in advance for any help you have time and interest to provide! Nathan Carter -- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_2265_237964951.1561047395850 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

Hello, HoTT community.

<= /div>
I've learned a bit about HoTT in bits of spare time over the = past few years, and have come up with some questions I can't answer on = my own.=C2=A0 It was suggested that I ask them on this list.=C2=A0 I will s= tart with a few small questions, and if anyone in the community here has ti= me to answer them, then I'll continue with others as needed.=C2=A0 Than= k you in advance for any help you can give.

(Where= I'm coming from:=C2=A0 I'm a mathematician; my dissertation was on= intermediate logics, but I haven't focused on logic much for the past = 15 years, instead doing mathematical software and some applied mathematics.= =C2=A0 I have a passion for clear exposition, so as I learn about HoTT, I p= rocess it by writing detailed notes to myself, explaining it as clearly as = I can.=C2=A0 When I can't explain something clearly, I flag it as a que= stion.=C2=A0 I'm bringing those questions here.)

Here are three to start.
  1. Very early in the HoTT book, = it talks about the difference between types and sets, and says that HoTT en= courages us to see sets as spaces.=C2=A0 Yet in a set of lecture videos Rob= ert Harper did that I watched on YouTube (which also seem to have disappear= ed, so I cannot link to them here), he said that Extensional Type Theory ta= kes Intuitionistic Type Theory in a different direction than HoTT does, for= malizing the idea that types are sets.=C2=A0 Why does the HoTT book not men= tion this possibility?=C2=A0 Why does ETT not seem to get as much press as = HoTT?
  2. When that same text introduces judgmental equality, it claims= that it is a decidable relation.=C2=A0 It does not seem to prove this, and= so I suspected that perhaps the evidence was in Appendix A, where things a= re done more formally (twice, even).=C2=A0 The first of these two formalism= s places some restrictions on how one can introduce new judgmental equaliti= es, which seem sufficient to guarantee its decidability, but at no point is= an algorithm for deciding it given.=C2=A0 Is the algorithm simply to apply= the only applicable rule over and over to reduce each side, and then compa= re for exact syntactic equality?
  3. One of my favorite things about Ho= TT as a foundation for mathematics actually comes just from DTT:=C2=A0 Once= you've formalized pi types, you can define all of logic and (lots of) = mathematics.=C2=A0 But then the hierarchy of type universes seem to require= that we understand the natural numbers, which is way more complicated than= just pi types, and thus highly disappointing to have to bring in at a foun= dational level.=C2=A0 Am I right to be disappointed about that or am I miss= ing something?
Thanks in advance for any help you have = time and interest to provide!

Nathan Carter
<= div>

--
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.
To view this discussion on the web visit https://groups.google.co= m/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googleg= roups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_2265_237964951.1561047395850-- ------=_Part_2264_1191050770.1561047395850--