Path Types in Algebraic Type Theory

We propose a new approach to the semantics of identity types in intensional Martin-Löf type theory. The setting is quite general, assuming only a category with finite limits and an exponentiable interval $1\rightrightarrows I$. It therefore applies to many different cases such as clans [1], model categories [2], path categories [3], categories with families [4], and natural models [5]. This approach is being used in the HoTTLean project [6], where it has already been formalized in Lean.

The specification of extensional identity types in natural models paralleled that of the other type formers $\mathrm{\Sigma }$ and $\mathrm{\Pi }$, but the treatment of the intensional case was less uniform. The latter was updated in [7] to a cleaner account suggested by R. Garner using polynomials. Here that approach is improved further by employing an interval to give a specification entirely analogous to that of the other type formers. We require namely a pullback diagram of the following form for path types, where $\dot{𝖳}\to 𝖳$ is the natural model.

(1)

The interval is also used to specify a (Hurewicz) fibration structure on $\dot{𝖳}\to 𝖳$. The combination of these two conditions already suffices to validate the usual rules for intensional identity types. The presence of an interval moreover relates the new approach to that of cubical type theory [8]. Indeed, the category of types is thereby enriched in cubical sets, and the type families classified by $\dot{𝖳}\to 𝖳$ are then necessarily cubical Kan fibrations in the sense of [9].

Many familiar models of type theory are subsumed as examples, including locally cartesian closed categories (the 0-truncated case), the usual groupoid model (the 1-truncated case), and certain monoidal model categories, such as simplicial and cubical sets (the untruncated case).