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.
%0 Journal Article
%1 awodey2007homotopy
%A Awodey, Steve
%A Warren, Michael A.
%D 2007
%K HoTT homotopy model
%R 10.1017/S0305004108001783
%T Homotopy theoretic models of identity types
%U http://arxiv.org/abs/0709.0248
%X 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.
@article{awodey2007homotopy,
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.},
added-at = {2014-11-17T11:17:16.000+0100},
author = {Awodey, Steve and Warren, Michael A.},
biburl = {https://www.bibsonomy.org/bibtex/2bc4dc639fc3252754b01ac87c5c48b68/t.uemura},
description = {Homotopy theoretic models of identity types},
doi = {10.1017/S0305004108001783},
interhash = {b7973668e261ffcf4eab9442daae2441},
intrahash = {bc4dc639fc3252754b01ac87c5c48b68},
keywords = {HoTT homotopy model},
note = {cite \href{http://arxiv.org/abs/0709.0248}{arxiv:0709.0248}Comment: 11 pages},
timestamp = {2014-11-17T11:17:16.000+0100},
title = {Homotopy theoretic models of identity types},
url = {http://arxiv.org/abs/0709.0248},
year = 2007
}