Discussion of Homotopy Type Theory and Univalent Foundations
 help / Atom feed
From: Nathan Carter <nathancarter5@gmail.com>
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] my first 3 questions about HoTT
Date: Fri, 21 Jun 2019 01:11:04 +0200
Message-ID: <6682FD3B-6A4C-49B4-B54D-E78FB4E71046@gmail.com> (raw)
In-Reply-To: <CAOvivQzgvD8sqxbxn_2xOXQZ1XoSG4vnEe8LhcaQt_G2H8C6SQ@mail.gmail.com>

[-- 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 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.

[-- Attachment #2: Type: text/html, Size: 4439 bytes --]

  reply index

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

Reply instructions:

You may reply publically 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 \
    --in-reply-to=6682FD3B-6A4C-49B4-B54D-E78FB4E71046@gmail.com \
    --to=nathancarter5@gmail.com \
    --cc=homotopytypetheory@googlegroups.com \


* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Newsgroup available over NNTP:

AGPL code for this site: git clone https://public-inbox.org/ public-inbox