Homotopy theoretic models of identity types
Logic
2009-11-13 v1 Algebraic Topology
Category Theory
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.
Cite
@article{arxiv.0709.0248,
title = {Homotopy theoretic models of identity types},
author = {Steve Awodey and Michael A. Warren},
journal= {arXiv preprint arXiv:0709.0248},
year = {2009}
}
Comments
11 pages