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-ed1-x538.google.com (mail-ed1-x538.google.com [IPv6:2a00:1450:4864:20::538]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 64bd7cf5 for ; Thu, 20 Jun 2019 23:11:07 +0000 (UTC) Received: by mail-ed1-x538.google.com with SMTP id i44sf6372979eda.3 for ; Thu, 20 Jun 2019 16:11:07 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1561072267; cv=pass; d=google.com; s=arc-20160816; b=dIRvsM4Ss1HvlsdjPkfJJJIa6D+Fq/W6HLvS9dtzxnzIWoiQO01o767q0SQELClUwU XctuCGYdsRmtlZ8k5s+KAJba8C2oTUkVB8/SxteJ9qAaXOoGR2lrS+4IG349x6xjuwaA k1Y3DQ5Hey2dECkvg1gW2y/QFDJ4BWCJJNkeimEvvnmJMKAHSViwo+Tg4WdE641x4YfN +hV6UH9oCQmvnkUFnVbU0+EFN56dRfRtlFP6IwjoVZHeRM1uMY5Q2EgKNhzUpF9e34DQ /w1GxBpJpxlNaP1ZVADgsjE7bVyncSalMe8cIOGYoqOt45SwfpUCUjB5AEj5IN6aS/gB WVoA== 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:message-id:in-reply-to:to:references:date :subject:mime-version:from:sender:dkim-signature:dkim-signature; bh=s/wC5/ZDF+g+sATuBdN7YroNDuCqH6wswOd6zLZliV4=; b=teW05d6ZTm9ZWE5VxlqyC3Gh3+A7VHMHdeNRqXTmvzEIQd25tLnB2rGHl6jj/kQFxj DktyfvauBbmOYEB3PzR+Rdawhs6JUq7UoAygZLRd03dwfxdpW8moxldpZyDq4haKgba0 jHo2qkBzaXfueBc/feU89oAXeRpFfhPp15S8y/R+3g5PtGS5JfPDJ4bjzAYRcMYTxGqW ocpHRXze0642sMbjiadVHVfMtPC6ovHegt20ODVa1EULR1AAhK0L7C/wVC20IfliSmH3 GvlSJJfpKWwHCvuErUWW7CsTlltcaRou3af1SdTpGMEaHywOW68wK+odylIuj7PgsvG0 4ceA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=SKaWKaVv; spf=pass (google.com: domain of nathancarter5@gmail.com designates 2a00:1450:4864:20::429 as permitted sender) smtp.mailfrom=nathancarter5@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:from:mime-version:subject:date:references:to:in-reply-to :message-id:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=s/wC5/ZDF+g+sATuBdN7YroNDuCqH6wswOd6zLZliV4=; b=YsQ36yd5e0dBduT2uK9DDp73DvmPGyaqKoa2GquAIQ6J6rOJM5WLtQaCtwE5W58mT0 9kc613IAMU0G5ICw3Hlb4tkU+eCUI/Xx+81B4dK511HMujQShEd7uDdzR0gIfT2I1wjH EDV41sWwsYs60oA91h0RIdgi+zTBHFbF5WHSgJl0e8Q5jA5LY7bxf+xwRn/G7oYvIRCk QfgRhtoqPakOf4tE7/aG/I9I4TKH7s7gx2/2sLsErfdP7/kHqQhoAsUfhFQ6ssKOzpcG 1nzxKL808wVzmN1jai+1KLv8PSEkgrJk2t394eAzL51QbTao6TIwJUkID9uDh7FrHYcO 2DlA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:mime-version:subject:date:references:to:in-reply-to:message-id :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=s/wC5/ZDF+g+sATuBdN7YroNDuCqH6wswOd6zLZliV4=; b=qGG5aIxTSD7JGwXu1vvpgqLa7b2sq0agu7UWcmQXfkb4df50hsnp00pabRzNeh+soN IDtqt1qFv6tgGrKX/2On911HjDxMwqQaO/NgABkHia79XJQe9M/Ddnda36H3Tmz/cPTn BdjdkL14WjxH9+HITWiIfnUZfeqE4SLMM/ZomIs43DgqnGNIAKX5CsiBB4AM9DbqwBq0 Y5v3ke8CUrocfzS/19WiUKUMnRcFWN/lWMrsdxm7KjAlqvycSldrSjYLnlZog26KhERl gzehptrNJzZaqGFbaKfgXqWg+XB705N193/YhXi7bf1HzUBxH1Gf8W9ndkaDT28KulRa kn1g== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:mime-version:subject:date:references :to:in-reply-to:message-id: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=s/wC5/ZDF+g+sATuBdN7YroNDuCqH6wswOd6zLZliV4=; b=S+U4up4nS2We8kETSankgkJ7sLhqCIKLC4Nxw2XarHYmRomCCdkElcyhWwmnOlQsGi na6ye/Hh+gSFDFq22NFEbOrYp5SXz0rLuJaikdPaLPBzjPZkQZnZX65a5mA/5Fy3Nxyq Zl/XxjAzAVaG/zy+O+0BMvIAPzk8/Ym8ADgjHRd8BOgOymePz5k3feZiz3/jJKRx03Ec qZ7twLN1kT9eXJPX2KLQJJTDXrI6T0AZlpSS+Uz9W4OEsSzlKcVSH0qw/24Yb2ZIEop7 YAZb8Y+N2/TygZVZndvLDR/YbJFj9hZ5PRn89YjTAhp+mTX3MgjsVdPE89tKclsNM5ju Gvpw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVf6vdggRWWIPK9ie1upEE8jwoktpT4M16M9eoh+7NOt4k312Od KphSP1fR0ypb4cHUtKOvuiY= X-Google-Smtp-Source: APXvYqyYdmiNoqiyKhTsCzZ5fNp/Z2TPOEHck6DcmjEUfDWZFCdwjU2AMrDxflNbJp7MJh88nWrqHQ== X-Received: by 2002:a17:906:e2c2:: with SMTP id gr2mr13985871ejb.284.1561072267278; Thu, 20 Jun 2019 16:11:07 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:e114:: with SMTP id gj20ls1746861ejb.0.gmail; Thu, 20 Jun 2019 16:11:06 -0700 (PDT) X-Received: by 2002:a17:906:1ed4:: with SMTP id m20mr46055510ejj.154.1561072266877; Thu, 20 Jun 2019 16:11:06 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1561072266; cv=none; d=google.com; s=arc-20160816; b=BwBUY4h4RCkqnTwlv9F+SVy6v+QVeG26RD1KCz6yC8Xhmj1lsyBev+z3i/VYvdYA1M PlIsNIzDuhfBKDIkgbU9oWOj79D2hQW9CKfsMIqCR8l078JuvaUMtP4QjWWAJMb7QPOJ vjzgrEDeNkDR2Jn6mYQ28gpC243uBJwLWQQfUZp42RqTqeftYGYKmCknTQ/iYHbtXUBm k1j7VrP5K/fbvjwgLIyVJgNvvTr2EOdeEph7AhsbsfglKV7wKCjE0yYM6H+gAUPAWuXB Tnixh6ePNOEpoWiu/MxU8woiY2Vw32PJaW3n1SoPvzQvysMv3FxHpPnNBhZheEo9ZbAW RzzA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=message-id:in-reply-to:to:references:date:subject:mime-version:from :dkim-signature; bh=xMW+eZgl8wZcrYskobaxwGNVPs1GNNEoZTjUFXiMt8s=; b=vlNQCJVVCY7M3YHV8If6RMPrKwMe9G8s//m8i8FFwiwKaKydbO1P/uSYGpZf4Xcf39 0NAcgdSN4vbHmhDKx3QqAqKUBXUGaOrsHT29ePTk2JKWI9d0P+Y4DHl+KQ5bLu5oSbvN 0Wh2Fi7oidM64K/N2sigcNEwZLUij4nlp1xmvDa/VnrME3dsxYmSDf4c0A+Zrlc274La QX2FCeIIABGL/atl9j98QSITyvgr1VEp6/j+Mtz+Bv75At/jFtjALzXoSGapz45wC/nJ yjNFJaDte3SwFiIx7ZJebNZozMZVWfpw1atfHioHcar9h1smBK3/Aw2OZULNtrS9rRdb O6Jg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=SKaWKaVv; spf=pass (google.com: domain of nathancarter5@gmail.com designates 2a00:1450:4864:20::429 as permitted sender) smtp.mailfrom=nathancarter5@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wr1-x429.google.com (mail-wr1-x429.google.com. [2a00:1450:4864:20::429]) by gmr-mx.google.com with ESMTPS id z20si108498edc.1.2019.06.20.16.11.06 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 20 Jun 2019 16:11:06 -0700 (PDT) Received-SPF: pass (google.com: domain of nathancarter5@gmail.com designates 2a00:1450:4864:20::429 as permitted sender) client-ip=2a00:1450:4864:20::429; Received: by mail-wr1-x429.google.com with SMTP id d18so4666802wrs.5 for ; Thu, 20 Jun 2019 16:11:06 -0700 (PDT) X-Received: by 2002:a5d:5446:: with SMTP id w6mr83210378wrv.164.1561072266195; Thu, 20 Jun 2019 16:11:06 -0700 (PDT) Received: from [192.168.1.194] (cer78-1-88-174-56-78.fbx.proxad.net. [88.174.56.78]) by smtp.gmail.com with ESMTPSA id l17sm1113180wrq.37.2019.06.20.16.11.04 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 20 Jun 2019 16:11:05 -0700 (PDT) From: Nathan Carter Content-Type: multipart/alternative; boundary="Apple-Mail=_CB000786-CB47-4260-829E-6AFF01C80ED5" Mime-Version: 1.0 (Mac OS X Mail 12.4 \(3445.104.11\)) Subject: Re: [HoTT] my first 3 questions about HoTT Date: Fri, 21 Jun 2019 01:11:04 +0200 References: To: Homotopy Type Theory In-Reply-To: Message-Id: <6682FD3B-6A4C-49B4-B54D-E78FB4E71046@gmail.com> X-Mailer: Apple Mail (2.3445.104.11) X-Original-Sender: nathancarter5@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=SKaWKaVv; spf=pass (google.com: domain of nathancarter5@gmail.com designates 2a00:1450:4864:20::429 as permitted sender) smtp.mailfrom=nathancarter5@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: , --Apple-Mail=_CB000786-CB47-4260-829E-6AFF01C80ED5 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="UTF-8" Thank you all (Thorsten, Ali, Michael, and some folks off-list, too) for th= e helpful responses. I'll try to summarize here to be sure I've understood= . Please feel free to correct anything I say incorrectly. 1. Regarding ETT People mentioned the loss of important computational properties if one ado= pts ETT, and I can certainly see why that would be a big deal. While the s= ubtleties 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 a= t this point. 2. Decidability of judgmental equality I got seemingly (to me?) conflicting answers. One person off-list and one= on-list said (I think) that applying all possible beta reductions and symb= ol definitions would be sufficient to decide judgmental equality; another s= aid that this is not the case (again, I think). But I was given a referenc= e 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 like= "from pi types you can do all the things" was sloppy. I was trying to exp= ress that, once you've defined pi types, you've (a) learned the rules about= substitution, capture, etc., plus (b) encountered the principles by which = types are defined in general (which I have other questions about...but late= r). And from those two things, you can do lots of stuff. Several folks said that "the natural numbers" is an overstatement, since s= uccessor and maximum are enough; responses suggested various things simpler= than N that have these. But Michael helped express my unease more precisely: I'm not trying to do= 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 bui= ld a foundation with fewer pieces than usual (cleaner than a dozen-or-so ru= les of ND with guards on variables appearing free in undischarged assumptio= ns and so on, plus mathematical axioms). To need a number system very earl= y on seemed to lose some of this purity, especially since it seemed to be i= n the metatheory. I do not (yet) fully understand Michael's answer about A= gda's type of universe levels, but I guess that it avoids paradoxes by bein= g 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 muc= h again. Once I've gotten to a good point for asking more questions, I wil= l do so. Nathan --=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/6682FD3B-6A4C-49B4-B54D-E78FB4E71046%40gmail.com. For more options, visit https://groups.google.com/d/optout. --Apple-Mail=_CB000786-CB47-4260-829E-6AFF01C80ED5 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset="UTF-8"
Thank you all (Thorsten, Ali, Michael, and some fol= ks off-list, too) for the helpful responses.  I'll try to summarize he= re to be sure I've understood.  Please feel free to correct anything I= say incorrectly.

1. Regarding ETT
People mentioned the loss of important compu= tational properties if one adopts ETT, and I can certainly see why that wou= ld 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-leve= l 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 one on-list said (I think) that applying all possible beta reduct= ions and symbol definitions would be sufficient to decide judgmental equali= ty; another said that this is not the case (again, I think).  But I wa= s given a reference to a paper, so I can find out more o= n my own.

3. Numb= ers as universe indices
The responses showed that my question = wasn't clear.  Saying something like "from pi types you can do all the things" was sloppy.  I was trying to expr= ess that, once you've defined pi types, you've (a) learned the rules about = substitution, capture, etc., plus (b) encountered the principles by which t= ypes are defined in general (which I have other questions about...but later= ).  And from those two things, you can do = lots of stuff.
Several folks said that "the natural numbers" i= s an overstatement, since successor and maximum are enough; responses sugge= sted various things simpler than N that have these.
But Michae= l helped express my unease more precisely:  I'm not trying to do mathe= matics without the natural numbers; that would be silly and was part of my = question's sloppiness.  Rather, I'm appreciating that DTT lets us buil= d a foundation with fewer pieces than usual (cleaner than a dozen-or-so rul= es of ND with guards on variables appearing free in undischarged assumption= s and so on, plus mathematical axioms).  To need a number system very = early on seemed to lose some of this purity, especially&= nbsp;since it seemed to be in the metatheory.  I do not (yet) full= y understand Michael's answer about Agda's type of universe levels, but I g= uess that it avoids paradoxes by being one step removed from a type of all = universes, which sounds clever.

<= div class=3D"">These replies will help me make progress on my notes, so tha= nk you very much again.  Once I've gotten to a good point for asking m= ore questions, I will do so.

Nathan

<= /html>

--
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/msg= id/HomotopyTypeTheory/6682FD3B-6A4C-49B4-B54D-E78FB4E71046%40gmail.com.=
For more options, visit http= s://groups.google.com/d/optout.
--Apple-Mail=_CB000786-CB47-4260-829E-6AFF01C80ED5--