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.
Notice that we already have an entry Homotopy Type System, which is the same kind of idea.
Ah ok. The second reference’s abstract says
The idea of two-level type theory is heavily inspired by Voevodsky’s Homotopy Type System (HTS). Two-level type theory can be thought of as a version of HTS without equality reflection. We show that the lack of equality reflection does not hinder the development of the ideas that HTS was designed for.
Does this merit a distinct entry then?
Sorry, I forgot about that page.
I would lean towards folding Homotopy Type System into two-level type theory. Unfortunately, “2LTT” seems to be being used both as a general term for type theories with both exact and path equality types, and also a name for the specific ACK system. The general term includes not just ACK and HTS but also the “computational cubical type theory” of Harper-Angiuli et. al. Nearly everything we currently have at Homotopy Type System applies more generally to all two-level type theories, and right now it seems that ACK and CCTT are receiving more active work than HTS. (In particular, HTS has the disadvantage of undecidable type-checking, which ACK restores by leaving out equality reflection in favor of UIP – for CCTT I’m not sure, that may not be a relevant question for the sort of type theory that it is.)
I added a link to Homotopy Type System. I’ll leave it to experts to arrange what they take to be the proper relation between these pages.
I also added some discussion of the issue of fibrant vs non-fibrant nat.
1 to 7 of 7