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.
I don’t think I even know what a “decidable language” is. Do you mean decidability of type inhabitation?
added pointer to:
Adding XTT as an example of an extensional cubical type theory, and adding a paper where XTT was defined as a reference:
Anonymous
adding reference
Anonymous
I would kind of like to split this page into “extensional type theory”, referring only to the historically accurate definitionally extensional type theory, and another page called something like “set-level type theory” that includes also the so-called “propositionally extensional” type theories like MLTT+UIP, Agda-with-K, OTT, and XTT. I think the expansion of the meaning of “extensional type theory” to the latter class was a mistake and we should try to fix it. We probably can’t immediately fix all the pages that use that terminology, but we can make a note at “extensional type theory” that you might have meant “set-level type theory” and fix them as we find them.
Thoughts?
I strongly agree.
An anonymous contributor created set-level type theory. Since no one seems to be objecting, we can move anything relevant from this page over there and refocus it on the definitionally-extensional sort.
1 to 11 of 11