University of Cambridge > > Category Theory Seminar > Two-Level Type Theory

Two-Level Type Theory

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Tamara von Glehn.

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).

This talk is part of the Category Theory Seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2019, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity