Path categories and propositional identity types

TL;DR

This paper links a weakened form of identity types in type theory to path categories from homotopy theory, establishing a new framework that bridges logic and topology.

Contribution

It shows that the syntactic category of a type theory with weak identity types forms a path category, connecting homotopy theory concepts with logical type theories.

Findings

Syntactic categories with weak identity types form path categories.

Establishes a connection between homotopy theory and type theory.

Strengthens previous results by Avigad, Lumsdaine, and Kapulkin.

Abstract

Connections between homotopy theory and type theory have recently attracted a lot of attention, with Voevodsky's univalent foundations and the interpretation of Martin-Lof's identity types in Quillen model categories as some of the highlights. In this paper we establish a connection between a natural weakening of Martin-Lof's rules for the identity types which has been considered by Cohen, Coquand, Huber and Mortberg in their work on a constructive interpretation of the univalence axiom on the one hand, and the notion of a path category, a slight variation on the classic notion of a category of fibrant objects due to Brown. This involves showing that the syntactic category associated to a type theory with weak identity types carries the structure of a path category, strengthening earlier results by Avigad, Lumsdaine and Kapulkin. In this way we not only relate a well-known concept in homotopy theory with a natural concept in logic, but also provide a framework for further developments.