Homotopy theoretic models of identity types

TL;DR

This paper establishes a new link between homotopical algebra and type theory, demonstrating that a form of intensional type theory can be modeled within any Quillen model category, extending previous models.

Contribution

It introduces a homotopy-theoretic framework for modeling identity types in type theory using Quillen model categories, generalizing the Hofmann-Streicher groupoid model.

Findings

Intensional type theory is valid in any Quillen model category.

Generalization of the Hofmann-Streicher groupoid model.

Bridges homotopy theory and logical models.

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.