Two-Level Type Theory

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

• Nicolai Kraus (University of Nottingham)
• Tuesday 07 November 2017, 14:15-15:15
• MR5, Centre for Mathematical Sciences.

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.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Category Theory Seminar
• DPMMS Lists
• DPMMS Pure Maths Seminar
• DPMMS info aggregator
• DPMMS lists
• Hanchen DaDaDash
• Interested Talks
• MR5, Centre for Mathematical Sciences
• School of Physical Sciences
• bld31
• ndb35's list
• yk373's list

Note that ex-directory lists are not shown.