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.5 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, MISSING_HEADERS,RCVD_IN_DNSWL_NONE autolearn=no autolearn_force=no version=3.4.2 Received: from mail-qt1-x83a.google.com (mail-qt1-x83a.google.com [IPv6:2607:f8b0:4864:20::83a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 744e379f for ; Thu, 20 Jun 2019 16:37:46 +0000 (UTC) Received: by mail-qt1-x83a.google.com with SMTP id z6sf4323980qtj.7 for ; Thu, 20 Jun 2019 09:37:46 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1561048665; cv=pass; d=google.com; s=arc-20160816; b=I8HlluIgh8ZvNH1Q7g+jhx2vMRla4DEp1Pf/COIxepMAj5nUBfCLzxicveUolGmrZ4 kc5QW5I5jyh9bDhl10bMfRpcjWgkzIqJ6rS3JFlDAxK8M/jc8mZ8QNkDuTovyjblv8fh c17o3E7SPz3001ADESZqjJzHvvfdlWDoDDHwEsqldyXC3qt6FOdnsXcT4lxRhgzh9LEo NFn7JmzQ2innfchV1wlBERHJBcX0bWVsiXjE6XDF5edYn8Y9MxUK0wN8J+biuUi5bFIa HXcP734wJsKkxzXtqbRYUECSl+xyFQVNTHpTKIZZFGOy2v47O+Khj2d+RyA28+0ziKAY Anuw== 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:subject:message-id:date:from:in-reply-to :references:mime-version:sender:dkim-signature:dkim-signature; bh=a/1tQ8TrI9gJcXhqiI/gVXRoujxuAueOyPpUAVHLcUo=; b=rn9PjgIhzHfiIrlIKl+6Br6SOkxDqthH69GE64H2cydkNkge049/7rZeW2Kha3lFIu 0QM/VhGwb2MubNcMkkQPM+kgJsdMZmKoLT7cwyS6AKSvhkbl2cPuOqUKfGp1wCoew5tz hUtoJGDQXZN8wieOwipXoyLNgaeUpSmAr3juiNCekgdY8jCGDFx1auSL7NNwoLBBCuUO Wo3zwOLydFsEHT8y52kN4vwupLp+LehFkBJbD1UapXNOyIY/88ULep3x18JyUNDoXOoI OC07//906YsjxfXtS4OwfU1LJI+Yi05xnTJXkLIhjB+trWMJpAlJub3rYambceKUvR0Q naEg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=hfMk13sL; spf=pass (google.com: domain of cory.m.knapp@gmail.com designates 2607:f8b0:4864:20::d2d as permitted sender) smtp.mailfrom=cory.m.knapp@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:references:in-reply-to:from:date:message-id :subject:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=a/1tQ8TrI9gJcXhqiI/gVXRoujxuAueOyPpUAVHLcUo=; b=fFJkkH3c7VVf+5mDh4Ybcomt+bD7WahVBT4I/75LBJOS6B6aeu8+3cCK46oaATeFJB KOWCfAsHGOKUaD5QtEt1fywsPM9a0MoLy8TpPOyunjqf5EwLtvWdC/qtsKNP5WFcFf9W SGKc+GdXfWWs5YqBNe6sGtPaeHWpSnu84fR2WnC0j7Bl9ur6NyO9jpJGUhS/EbLChfqj UuBY9QVjfjlxfl1L6injTwD/EJm1zIvb9pEzDVdupatw+0I8e7PuM77sqKFoCAFV50m2 UoDz0Z82xoTDBpwmAdFrkBc5dcIf6urIENGa7XHtUQmmSBs9TGkh0Sk9C0CcksxubPUg hTdA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:cc :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=a/1tQ8TrI9gJcXhqiI/gVXRoujxuAueOyPpUAVHLcUo=; b=l0NpAStKDNHo6Vlz2TAtxJhcxHjv/GHIfQsjOURbUGcSCGHAThtSwbSVGLsMg0BLUn SvRCOdB+mSHwfhBSozzvR5w32qQ3rvYUdem8+zbj6paT30wIfNMzbomTQUT7/Rzfop4B +DSka228wrzzURl3ble6PPQO8+NK0ix0Gy+7ohlhXRcvonxwmAIhFrhy8xriyFKlsD5O QKyVqRphZv+aMli2KcdnVy+R9QfRhRu0Ya6UUL8NkLnC212ZUsQlWdK+ANW8QsdSsB/x gkwPdhS8qzf/8zC+x8AGUXLnv4R85+zYqJiQfohObrRkeG+WHAwXb0BGEabh7rnunUfO 0dsw== 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:references:in-reply-to:from :date:message-id:subject: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=a/1tQ8TrI9gJcXhqiI/gVXRoujxuAueOyPpUAVHLcUo=; b=tBZMfThHwKTstURBaAD2oPCdZTD+3b35oMi6fYiBk4S648rN39qH2leQCIoYg42Kle /B21u+g8VNdovqWnUvEyOhbCEsG8iAVDUiQ5Yb6PiLdEPhLbMdxnLiKXAK6fMklg54fv rVftnKO+JXtVvYetbG/2nxsmz1a85tnuldLs+VHVPUgjqmc++z0gQQxT/dA3t/jqujPm hSg4rU+nsToma3nKH//+jd51j8LbjNlNZlsFmubUtsIj757q7EzPnt9mTc7BWasqhJ3c Ma2Jfm6VBCAPzleho9k9/4wc2zO5NljEuUF965kvBr3p2wgJwlyzSAInRtJvHMoJsc4U YyYA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUIACucdXrOt6ubLZMH3xBSFm6ivKR7c6jPQReEb70b71nEAFfX hIx/ZDe3OvDE24GXV+2118w= X-Google-Smtp-Source: APXvYqx/Eg1S9wQJYeoZKCgvy1u8HHUsWToawbvYIiLRmGkmrJU3Y3A9SxM0LYnf4NnhzNkJFfSN5A== X-Received: by 2002:a37:a244:: with SMTP id l65mr89212776qke.118.1561048665128; Thu, 20 Jun 2019 09:37:45 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:818:: with SMTP id u24ls1893097qth.5.gmail; Thu, 20 Jun 2019 09:37:44 -0700 (PDT) X-Received: by 2002:ac8:25b1:: with SMTP id e46mr93163483qte.36.1561048664791; Thu, 20 Jun 2019 09:37:44 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1561048664; cv=none; d=google.com; s=arc-20160816; b=wH0YykO43DrNdiW5qeYaTsHKBlQCra1hwlezLk7hJVs+O0BfONxi9KRIvNBgnof8AR fkW3sWK94pTIEQNqVRPoGKc9fh1YGpNJB9/hgXydApzhSq8BmgHRVk8NGfRL8rxOzlqd IrNriOqY+qCmHEd+GZBQ//pGfjIoRBf8PzRF2JvSN00jX/sbsc71imKZXHXKPjQf0Z8i fnYobf+UXn1AG7eBKXTHwMfVnRGbsLIzWKlLGSW3WG9nJLJmnuHFgzxud9FDCfu9hcmi Y520yWEFWy35XfpV6zVp7BI56GzAKFjohAMRjQ99SSywXYeZxzeTt4mbzy9ETFVT3Cq4 ZiQg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:subject:message-id:date:from:in-reply-to:references:mime-version :dkim-signature; bh=Zu9V/Qko6jk9rLo/dlba4gDpIwe0bNwRZtYU/oGEz9Q=; b=e6XiraB3OsltZJNW3TF2HDjEdR92r0tX4H2BJDy9CL/CaC+Uot/AJi/+PN8AXfDN6i tGvJGnBh8pMdSTBIPAP+aNQtQwZ32mIJQyI5D6C63wF97Fre1zbRFDIZepxJwpBvczu4 +EhGJB0QZ1ibn+ITw7Wbjhuaetw42NcQSM+gRx5lf62AH0qKgljLHRuB7Hw8wQfwq6P9 kG+7JKRD6RapbHDvKAHNDRp+qBPu5JovICvFv5FaxlDF+IJWnwlXwJ3pN8qcsIkLpLjb iMCMeAQWpDRdDYCuUWdDKhpDdT1TyVmzP6qYkhimNX25qG3rOdUUlRZshsd1DrD634L1 1vBg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=hfMk13sL; spf=pass (google.com: domain of cory.m.knapp@gmail.com designates 2607:f8b0:4864:20::d2d as permitted sender) smtp.mailfrom=cory.m.knapp@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-io1-xd2d.google.com (mail-io1-xd2d.google.com. [2607:f8b0:4864:20::d2d]) by gmr-mx.google.com with ESMTPS id u204si13802qka.6.2019.06.20.09.37.44 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 20 Jun 2019 09:37:44 -0700 (PDT) Received-SPF: pass (google.com: domain of cory.m.knapp@gmail.com designates 2607:f8b0:4864:20::d2d as permitted sender) client-ip=2607:f8b0:4864:20::d2d; Received: by mail-io1-xd2d.google.com with SMTP id k20so725368ios.10 for ; Thu, 20 Jun 2019 09:37:44 -0700 (PDT) X-Received: by 2002:a05:6638:149:: with SMTP id y9mr79861015jao.76.1561048664364; Thu, 20 Jun 2019 09:37:44 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Cory Knapp Date: Thu, 20 Jun 2019 17:37:33 +0100 Message-ID: Subject: Re: [HoTT] my first 3 questions about HoTT Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="0000000000001dda5b058bc3f746" X-Original-Sender: cory.m.knapp@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=hfMk13sL; spf=pass (google.com: domain of cory.m.knapp@gmail.com designates 2607:f8b0:4864:20::d2d as permitted sender) smtp.mailfrom=cory.m.knapp@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: , --0000000000001dda5b058bc3f746 Content-Type: text/plain; charset="UTF-8" Hi Nathan, I'm a bit rusty and don't want to say potentially misleading things on a public forum, so I'm messaging offlist. Hopefully someone else gives more thorough answers: 1. ETT provides little (if any) technical value over set theory, at the cost of more bureaucracy, so it's main draw is the philosophical underpinnings. Since it also seems to conflict with computational intuitions, it alienates not only the classical mathematician, but also the computer scientist--this leaves a small audience. 2. I believe you are correct 3. Without *any* type universes, you only get the types of System T---So you get a system that corresponds to higher-typed Heyting arithmetic. So we need at least one universe. The HoTT book doesn't *really* use the natural numbers, only successor and a (binary) least upper bound operator. I guess this corresponds roughly to Robinson's Arithmetic? Best, Cory On Thu, Jun 20, 2019 at 5:16 PM Nathan Carter wrote: > > 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. > -- 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/CADzYOhd-tHN0XO_c%2B-rW_JSU1%3DQ6CmGE3L8aSHCEW32oX%2BKttA%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout. --0000000000001dda5b058bc3f746 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Nathan,

I'm a bit rusty and don&= #39;t want to say potentially misleading things on a public forum, so I'= ;m messaging offlist. Hopefully someone else gives more thorough answers:

1. ETT provides little (if any) technical value ove= r set theory, at the cost of more bureaucracy, so it's main draw is the= philosophical underpinnings. Since it also seems to conflict with computat= ional intuitions, it alienates not only the classical mathematician, but al= so the computer scientist--this leaves a small audience.

=
2. I believe you are correct

3. Without= *any* type universes, you only get the types of System T---So you get a sy= stem that corresponds to higher-typed Heyting arithmetic. So we need at lea= st one universe. The HoTT book doesn't *really* use the natural numbers= , only successor and a (binary) least upper bound operator. I guess this co= rresponds roughly to Robinson's Arithmetic?

Be= st,
Cory

On Thu, Jun 20, 2019 at 5:16 PM Nathan Carter <<= a href=3D"mailto:nathancarter5@gmail.com">nathancarter5@gmail.com> w= rote:

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.= =C2=A0 It was suggested that I ask them on this list.=C2=A0 I will start wi= th a few small questions, and if anyone in the community here has time to a= nswer them, then I'll continue with others as needed.=C2=A0 Thank you i= n advance for any help you can give.

(Where I'= m coming from:=C2=A0 I'm a mathematician; my dissertation was on interm= ediate logics, but I haven't focused on logic much for the past 15 year= s, instead doing mathematical software and some applied mathematics.=C2=A0 = 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.= =C2=A0 When I can't explain something clearly, I flag it as a question.= =C2=A0 I'm bringing those questions here.)

Her= e are three to start.
  1. Very early in the HoTT book, it tal= ks about the difference between types and sets, and says that HoTT encourag= es us to see sets as spaces.=C2=A0 Yet in a set of lecture videos Robert Ha= rper 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 In= tuitionistic Type Theory in a different direction than HoTT does, formalizi= ng the idea that types are sets.=C2=A0 Why does the HoTT book not mention t= his possibility?=C2=A0 Why does ETT not seem to get as much press as HoTT?<= /li>
  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 are don= e more formally (twice, even).=C2=A0 The first of these two formalisms plac= es some restrictions on how one can introduce new judgmental equalities, wh= ich seem sufficient to guarantee its decidability, but at no point is an al= gorithm for deciding it given.=C2=A0 Is the algorithm simply to apply the o= nly 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:=C2=A0 Once you&#= 39;ve formalized pi types, you can define all of logic and (lots of) mathem= atics.=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 foundation= al level.=C2=A0 Am I right to be disappointed about that or am I missing so= mething?
Thanks in advance for any help you have time a= nd interest to provide!

Nathan Carter

--
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 ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-= aa1cce32bcb2%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
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.com/d/msgid/HomotopyTypeTheory/CADzYOhd-tHN0XO_c%2B-rW_JSU= 1%3DQ6CmGE3L8aSHCEW32oX%2BKttA%40mail.gmail.com.
For more options, visit http= s://groups.google.com/d/optout.
--0000000000001dda5b058bc3f746--