Peter LeFanu Lumsdaine: The coherence problem for dependent type theory

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.