From: Nathan Carter <firstname.lastname@example.org>
To: Homotopy Type Theory <email@example.com>
Subject: Re: [HoTT] my first 3 questions about HoTT
Date: Fri, 21 Jun 2019 01:11:04 +0200 [thread overview]
Message-ID: <6682FD3B-6A4C-49B4-B54D-E78FB4E71046@gmail.com> (raw)
[-- Attachment #1: Type: text/plain, Size: 3015 bytes --]
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 understood. Please feel free to correct anything I say incorrectly.
1. Regarding ETT
People mentioned the loss of important computational properties if one adopts 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 one on-list said (I think) that applying all possible beta reductions and symbol definitions would be sufficient to decide judgmental equality; another said that this is not the case (again, I think). But I was given a reference to a paper <https://link.springer.com/chapter/10.1007/978-3-540-70594-9_4>, 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 express 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 later). 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 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 build a foundation with fewer pieces than usual (cleaner than a dozen-or-so rules of ND with guards on variables appearing free in undischarged assumptions and so on, plus mathematical axioms). To need a number system very early 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 being 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 much again. Once I've gotten to a good point for asking more questions, I will do so.
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 HomotopyTypeTheoryfirstname.lastname@example.org.
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.
[-- Attachment #2: Type: text/html, Size: 4439 bytes --]
next prev parent reply other threads:[~2019-06-20 23:11 UTC|newest]
Thread overview: 7+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-06-20 16:16 Nathan Carter
2019-06-20 16:37 ` Cory Knapp
2019-06-20 16:39 ` Thorsten Altenkirch
2019-06-20 16:56 ` Michael Shulman
2019-06-20 23:11 ` Nathan Carter [this message]
2019-06-21 1:04 ` Michael Shulman
2019-06-20 16:48 ` Ali Caglayan
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).