Article,

Homotopy theoretic models of identity types

, and .
(2007)cite http://arxiv.org/abs/0709.0248arxiv:0709.0248Comment: 11 pages.
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.

Tags

Users

  • @t.uemura

Comments and Reviews