Homotopy theoretic models of identity types
arXiv:0709.0248 · doi:10.1017/S0305004108001783
Abstract
This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing the Hofmann-Streicher groupoid model of Martin-Loef type theory.
11 pages