Abstract

I give an introduction to two-level type theory, a system that can combine two Martin-Lof style type theories. We can take one of them to be homotopy type theory (HoTT), and the other to be a version of MLTT with unique identity proofs. This yields an extension of HoTT where a “type of strict equalities” is available, and from the point of view of HoTT, this strict equality can be compared to judgmental/definitional equality; essentially, we get a variant of HoTT where it is possible to reason internally about judgmental equality. This system can be understood as a variant of Voevodsky’s homotopy type system (HTS). Both HTS and two-level type theory address the issue that certain higher-categorical structures cannot be suitably encoded in standard HoTT (cf. semisimplicial types). Two-level type theory has been suggested by Altenkirch-Capriotti-K (arXiv:1604.03799 / CSL ’16), developed further by Annenkov-Capriotti-K (arXiv:1705.03307), and a conservativity result has been shown by Capriotti (arXiv:1702.04912 / PhD thesis).