Home > News > Peter LeFanu Lumsdaine: Coherence constructions for models of type theory

Peter LeFanu Lumsdaine: Coherence constructions for models of type theory

Date: 21. 11. 2016
Source: Mathematics and theoretical computing seminar
Torek, 22. 11. 2016, od 12h do 14h, Plemljev seminar, Jadranska 19

Peter LeFanu Lumsdaine

University of Stockholm, Švedska  

Abstract: Modelling type theory involves various subtleties known as “coherence issues”, arising from two directions: the syntactic side, and the semantic side.  I will discuss the latter: the semantic coherence issues.


Roughly, the difficulty on that side is making sure that all logical constructions commute strictly with substitution.  One one hand, there are various ad hoc solutions for specific models; on the other, there are several more general/abstract constructions (by Hofmann, Voevodsky, and Lumsdaine–Warren, among others).  I’ll discuss these various solutions, and their limitations, plus a few further obstacles that arise when internalising them in the HoTT/Univalent Foundations setting.