Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
adding second reference
Anonymous
Changed “strong normalization” to “normalization” as the former is a category error — nobody has proposed any rewriting system for XTT, so strong normalization is neither here nor there. If a rewriting system is proposed, then SN or its failure would be a theorem about that rewriting system, not about XTT.
dumb question, but is it “X type theory” or just “X tee tee”?
Added a hyperlink to normal form (which is the appropriate pointer from the disambiguation page normalization), where this distinction should be (but is not currently) discussed.
I have fixed the arXiv link, from
https://arxiv.org/abs:1904.08562
to
https://arxiv.org/abs/1904.08562
here and in the author’s entries.
Now that I have done this, I see that somebody else was catching the same problem already elsewhere. So maybe there is yet more instances left to be fixed.
re #6
dumb question: is it “X type theory” or just “X tee tee”?
Just to say that i don’t find this a dumb question and that at least our nLab entry would deserve to be explicit about what “XTT” is meant to mean. In particular since the evident guess seems to be wrong: It’s not meant to be read as short for “extensional type theory”. Still, “extensional” seems to be the only plausible term that the “X” could be alluding to.
Hi all, I did indeed name XTT as a pun on “eXtensional Type Theory” — but it is meant to be read aloud only as XTT. It doesn’t actually stand for anything.
Best to add such explanation to the beginning of the entry!
1 to 13 of 13