Two-level type theory and applications
(2023)
Journal Article
We define and develop two-level type theory (2LTT), a version of Martin-Löf type theory which combines two different type theories. We refer to them as the ‘inner’ and the ‘outer’ type theory. In our case of interest, the inner theory is homotopy typ... Read More about Two-level type theory and applications.