Peter LeFanu Lumsdaine: Coherence constructions for models of type theory
Datum objave: 21. 11. 2016
Seminar za temelje matematike in teoretično računalništvo
Torek, 22. 11. 2016, od 12h do 14h, Plemljev seminar, Jadranska 19
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.