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.8 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-yb1-xb3b.google.com (mail-yb1-xb3b.google.com [IPv6:2607:f8b0:4864:20::b3b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 1be052eb for ; Fri, 21 Jun 2019 01:05:04 +0000 (UTC) Received: by mail-yb1-xb3b.google.com with SMTP id e193sf4245917ybf.20 for ; Thu, 20 Jun 2019 18:05:03 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1561079102; cv=pass; d=google.com; s=arc-20160816; b=pjpT7J67MEacDSlhXfQZkMCViF4nn4P7oagEBpXTng8KAtH+8wUrU8WvaYUzEnohLx +GgXxd+BKcFPat0uP6cEKD3OT87DJEoqhgf1PA47hss/5wF3j5ukzH67O9YQzv+Dlq66 WoTUj4w7gWEthIPZVO0itnt0Dpq2JrUc1Zk84eVI4S28+wchoU/53tJ2hHmJxKkR9Xa3 Hz48CkuySYu6++dbqkO5KKeTBAJQJZVFyfDBEj8ycl9a435rxzros94GEvTnvcSPsM3a hNrTdpZzr3YQIUSXY7c5JGhUxg6irEj3DVMtfj3jlWerH3GDjJDYfBuDCUS9dAJVepv1 AdzQ== 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:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=xY3uvsbU5L83J1YUzfFNWCiadShbnQO3Sjy/AeVGbxU=; b=il85rV+MzMy5N96h9pB+DbnKkpDvkmRgY/CMmCmHlLwyOURfZ7WnJK3UcOTHsef/zY 4Y2Yl/G5k+rlYSYG82p4mJ4/Cvm1eB7e625mS9K95lT3wdqa70QrucbqDd0PxeiwJ8J8 4jss5J5GWu6xoEuA/fln6xppJVkarPprpcPOj7RB2d3zFgrZmBEaBuvhM+TwWc0zknhO u9o5abqERK8jGb0OgofEIFG7QLbM9oGkHcN+u5/PWqYhNg2Bs2VzzbxkF9N0Ldi7OZSZ 0BYwGUmHYFfxsHcoG9aLvOvcKLNB+/CjAbJLYBRjoCIgqws06ht2xrXPquuZjY2BhDjg cVXg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=MpIK5x7V; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b35 as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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:to:cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=xY3uvsbU5L83J1YUzfFNWCiadShbnQO3Sjy/AeVGbxU=; b=E8ZFxPq7A/cOLD5+nCY5F/ccYWyemEX8cSeQOwWf7qO6+b2nUWRjQGXKX58z9mhKB8 RAFv2Kgofd4QkubqoKzjtyc2H/aMGpSBQI7INy7t7PctE/SVq+ncYbm8RqmvD0sxxpru /YYVwnb8C4LA9iyfWKvHGqXpOlZnoFiMh+J6xs6Wq56FcVayF6XnSphxcr0woh8viHLx u42SjF6aOTqm3g32+VO//Lq7+v/DRjp3PD0bk86IREeaeioXECFGmuEyZ6HBH6rKYsuu 1NmOnFNJXieT+rS7WQIpwRlyk/4t4d/l+Vzmk5kLjxXTq9hx/iAfhRv4te/OU8Nmf+XP Z8kQ== 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:to:cc:content-transfer-encoding :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=xY3uvsbU5L83J1YUzfFNWCiadShbnQO3Sjy/AeVGbxU=; b=EtVMTMJiQa3sDPVTe6bu5rI4IV/5l0dTwVOgtDLixsI/5NlkPJ/+EjL5uYTz9NDwEl wnRO2xaIh8c3mgt/JjByqDUi1gJ6b4leex5pgD+Au1rUDcnmnV/isIYTwseWZseNI/64 DbH2JdZ2po3Wvs37MgGBxnW5pBXVzllmK47qzgeMhxFcx9CoUQeL8JqFEl2FhABF54M0 pHEiBKjrlocaoaY/NpHOJPKTYxlcSC/Qocxdm7toLcV/RFSjhvnw24p/z5tHnuya/xrg E0cNEapu+jEg7myleJE35A9VJf+no76s2Vv7X8TdSwwYWIyDy81CXGdsl2w/TUTf2x3c k7wA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUsrcKmhl1JSAyrBdGpmqMNApoWSZOKoin09Xtsp13rvL1tnjyW fnSsfDClKipmjoSdmazAERc= X-Google-Smtp-Source: APXvYqxURC9sVXlkEj86IbSF/xKi+5Gnaj3BV8O9RMbHhRTYaRsZRVM3HgktD+43cNiryu8fiMm8Ug== X-Received: by 2002:a25:7901:: with SMTP id u1mr24316696ybc.209.1561079102751; Thu, 20 Jun 2019 18:05:02 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:14b:: with SMTP id 72ls1086734ywb.15.gmail; Thu, 20 Jun 2019 18:05:02 -0700 (PDT) X-Received: by 2002:a81:ee05:: with SMTP id l5mr4044706ywm.245.1561079102386; Thu, 20 Jun 2019 18:05:02 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1561079102; cv=none; d=google.com; s=arc-20160816; b=MtXzR0HpFjWlCs4Jq/VQgj8US/UxdAfMN9+iBR0AHYAHoT1D4r3151DBxeBn0bSJQG rcr3JojGVuhSbKDZ2pCXbv9UcziAgk7KxSZjm27R0kfxrNhgetYpXaxnoz14n50Mq1VW Znq1/Td5144+fEmSuY5Mh3cdiTsGhn+gZoExXsU8g4Tld7xD01LT5UoQvHHUN5Vpe6Dx n68OWMbfXyE1g292Ar2rsRbKHvoB0iSg/Wro4/QYCa5AgHaZdyd0NwBe31wzgNdiAfRL jgKbX8qkQI0sZ1urATrke6kFnmU/q2O2gIIQiqejuGSwa+EqvXtnRnLu8nO0VWUAMSCC ElOg== 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=9WgHNfANjSe3/6MSPIZAhybSBFODBaek6XxpHo3LCrc=; b=fla2AEvgPogvVL1h3gJp6sHXAPQSJ5R+FO6LC3Q++XR2jvcWGIxO6Wfe5APGknwR0Z KzpznDRXGXPc2R0UMql5TQzVaGUhjiUwlz4B36PGj2jLYuoX6upjSS7UXUHoZqef3UGB 6LQqEnwS5xLvq38hd/FTWcXEuI5E8+agaKb4eLUTLy0OY7kWi7UB8xP6lwDTvNfCK32+ eokA8aTd+uBMJ/ssD56LhURlsLhSg9+FbS6RyrReW9G88OEmpLpTuW6OHMkctyLwztci 0QdscNO+rTIoBYjTj8++X1Y2dIDi3aUxQJOZ+9FD178chwFTtQticHPWpIHMl/5IBMRk 5kdA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=MpIK5x7V; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b35 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb35.google.com (mail-yb1-xb35.google.com. [2607:f8b0:4864:20::b35]) by gmr-mx.google.com with ESMTPS id s12si51905ywg.0.2019.06.20.18.05.02 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 20 Jun 2019 18:05:02 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b35 as permitted sender) client-ip=2607:f8b0:4864:20::b35; Received: by mail-yb1-xb35.google.com with SMTP id i6so1976544ybq.6 for ; Thu, 20 Jun 2019 18:05:02 -0700 (PDT) X-Received: by 2002:a25:943:: with SMTP id u3mr67078529ybm.293.1561079101987; Thu, 20 Jun 2019 18:05:01 -0700 (PDT) Received: from mail-yw1-f42.google.com (mail-yw1-f42.google.com. [209.85.161.42]) by smtp.gmail.com with ESMTPSA id h2sm315763ywb.18.2019.06.20.18.05.01 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 20 Jun 2019 18:05:01 -0700 (PDT) Received: by mail-yw1-f42.google.com with SMTP id u134so2010428ywf.6 for ; Thu, 20 Jun 2019 18:05:01 -0700 (PDT) X-Received: by 2002:a81:1ed5:: with SMTP id e204mr18002198ywe.272.1561079101140; Thu, 20 Jun 2019 18:05:01 -0700 (PDT) MIME-Version: 1.0 References: <6682FD3B-6A4C-49B4-B54D-E78FB4E71046@gmail.com> In-Reply-To: <6682FD3B-6A4C-49B4-B54D-E78FB4E71046@gmail.com> From: Michael Shulman Date: Thu, 20 Jun 2019 18:04:48 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] my first 3 questions about HoTT To: Nathan Carter Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=MpIK5x7V; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b35 as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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: , I think the reason for the mixed messages re: #2 is that different type theories have different rules for judgmental equality. If the only rules for judgmental equality are "directed" ones like beta-reduction, then (assuming a normalization result) to check equality it generally suffices to reduce two terms to normal form and compare the normal forms. But if there are also other rules for judgmental equality, like eta-conversion, that are difficult to formulate in a "directed" way, then you generally need a fancier equality-checking algorithm. And some rules for judgmental equality, like equality reflection in ETT, prevent there from being any algorithm at all. The HoTT Book assumes eta-conversion, so simple reduction to normal forms is probably not sufficient. There are well-understood algorithms for equality-checking in MLTT with eta (generally built on ideas like https://ncatlab.org/nlab/show/bidirectional+typechecking); but Book HoTT also adds judgmental computation rules for point-constructors of HITs, and while it seems intuitive that those should be regarded as beta-reduction-like, I'm not aware that anyone has precisely formulated an equality-checking algorithm for Book HoTT. On Thu, Jun 20, 2019 at 4:11 PM Nathan Carter wro= te: > > > Thank you all (Thorsten, Ali, Michael, and some folks off-list, too) for = the helpful responses. I'll try to summarize here to be sure I've understo= od. Please feel free to correct anything I say incorrectly. > > 1. Regarding ETT > People mentioned the loss of important computational properties if one ad= opts ETT, and I can certainly see why that would be a big deal. While the = subtleties relating 0-truncation, UIP, K, and reflection rules are not 100%= clear to me, I at least have a high-level intuition, which is what I want = at this point. > > 2. Decidability of judgmental equality > I got seemingly (to me?) conflicting answers. One person off-list and on= e on-list said (I think) that applying all possible beta reductions and sym= bol definitions would be sufficient to decide judgmental equality; another = said that this is not the case (again, I think). But I was given a referen= ce to a paper, so I can find out more on my own. > > 3. Numbers as universe indices > The responses showed that my question wasn't clear. Saying something lik= e "from pi types you can do all the things" was sloppy. I was trying to ex= press that, once you've defined pi types, you've (a) learned the rules abou= t substitution, capture, etc., plus (b) encountered the principles by which= types are defined in general (which I have other questions about...but lat= er). And from those two things, you can do lots of stuff. > Several folks said that "the natural numbers" is an overstatement, since = successor and maximum are enough; responses suggested various things simple= r than N that have these. > But Michael helped express my unease more precisely: I'm not trying to d= o mathematics without the natural numbers; that would be silly and was part= of my question's sloppiness. Rather, I'm appreciating that DTT lets us bu= ild a foundation with fewer pieces than usual (cleaner than a dozen-or-so r= ules of ND with guards on variables appearing free in undischarged assumpti= ons and so on, plus mathematical axioms). To need a number system very ear= ly on seemed to lose some of this purity, especially since it seemed to be = in the metatheory. I do not (yet) fully understand Michael's answer about = Agda's type of universe levels, but I guess that it avoids paradoxes by bei= ng one step removed from a type of all universes, which sounds clever. > > These replies will help me make progress on my notes, so thank you very m= uch again. Once I've gotten to a good point for asking more questions, I w= ill do so. > > Nathan > > -- > 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/msgi= d/HomotopyTypeTheory/6682FD3B-6A4C-49B4-B54D-E78FB4E71046%40gmail.com. > For more options, visit https://groups.google.com/d/optout. --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAOvivQzbSbOCFrBK_X2-45eBovJ5e799wXrQPec9h1-sZUGH5Q%40ma= il.gmail.com. For more options, visit https://groups.google.com/d/optout.