Re: [HoTT] my first 3 questions about HoTT

[Michael Shulman <shulman@sandiego.edu>]

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 <nathancarter5@gmail.com> wrote:
>
>
> 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, 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.
>
> 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/msgid/HomotopyTypeTheory/6682FD3B-6A4C-49B4-B54D-E78FB4E71046%40gmail.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/CAOvivQzbSbOCFrBK_X2-45eBovJ5e799wXrQPec9h1-sZUGH5Q%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.