Path Types in Algebraic Type Theory
Steve Awodey, Joseph Hua
TL;DR
The paper addresses the semantics of intensional identity types in intensional Martin-Löf type theory using only finite limits and an interval $I$. It develops path types via a relative pathobject and a normal Hurewicz fibration on the universe, yielding a single pullback specification that validates the usual Id-elimination rules. This construction also ties the framework to cubical type theory by showing that classified type families become cubical Kan fibrations, and it provides concrete examples in presheaf categories, groupoids, and cartesian cubical sets, complemented by a Lean formalization. Overall, the approach offers a uniform, interval-based account of path types that aligns with cubical intuitions and supports formal certification in Lean.
Abstract
A new approach to the semantics of identity types in intensional Martin-Löf 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 $Σ$ and $Π$, 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.