Path Types in Algebraic Type Theory

TL;DR

This paper introduces a new categorical semantics for identity types in intensional Martin-Löf type theory using an interval, unifying extensional and intensional cases and connecting to cubical type theory.

Contribution

It provides a novel pullback-based specification of path types employing an interval, simplifying the modeling of identity types in type theory.

Findings

Single pullback specification of path types using an interval

Interval-based fibration structure on the universe

Modeling of intensional identity rules with finite limits

Abstract

A new approach to the semantics of identity types in intensional Martin-L\"of type theory is proposed, assuming only a category with finite limits and an interval. The specification of \emph{extensional} identity types in the original presentation of natural models paralleled that of the other type formers $\Sigma$ and $\Pi$, but the treatment of the \emph{intensional} case there was less uniform. It was later reformulated to an account based on polynomials; here a further improvement in the style of the other type formers is achieved by employing an interval, in order to give a single pullback specification of a model with \emph{path types}. The interval is also used to specify a (Hurewicz) fibration structure on the universe of the model. It is shown that the combination of these two conditions suffices to model the intensional identity rules, assuming only finite limits. The addition of an interval also relates the current treatment to that of cubical type theory.