The local universes model: an overlooked coherence construction for dependent type theories

Peter LeFanu Lumsdaine, Michael A. Warren

We present a new coherence theorem for comprehension categories, providing strict models of dependent type theory with all standard constructors, including dependent products, depe…