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.