Peter LeFanu Lumsdaine: The coherence problem for dependent type theory
Time: Wed 2014-12-03 10.00 - 11.45
Location: Room 16, building 5, Kräftriket, Department of mathematics, Stockholm university
Coherence constructions are a vexing technical hurdle which most models of dependent type theory, especially homotopical ones, have to tackle in some way.
I will explain what the basic problem of coherence is, and survey the main known approaches to overcoming it, including the constructions of Hofmann,Voevodsky/Hofmann–Streicher, Lumsdaine–Warren, and Curien–Garner–Hofmann.