The Biequivalence of Path Categories and Axiomatic Martin-Löf Type Theories

Dependent type theory, and most notably intensional type theory (ITT), has become a cornerstone of logic, with applications in proof assistants, programming languages, and the foundations of mathematics. Models of type theory form categories, and categorical formulations [15, 38, 29] provide a powerful tool to understand the behaviour of these systems. However, giving a satisfactory categorical formulation of dependent type theory is challenging. First of all, we want our requirements to be simple categorical properties instead of direct reproductions of the syntax; and secondly, categorical structure usually only satisfies stability conditions up to isomorphism instead of the strict equality imposed in the syntax. This means that it is significantly easier to produce weak models, which only satisfy stability up to equivalence. To deal with the second issue, strictification techniques [26, 5, 33, 12, 22, 31] have been developed to turn weakly stable structure into strictly stable structure. This paper focuses on the first issue: providing a categorical and homotopy theoretic presentation of the weak models of dependent type theory. We combine our results with existing techniques for the second issue to turn our weak models into (strict) models.

One difficulty in studying ITT is the fact that it has two notions of equality: propositional equality (=), which is an internal equality type, and definitional equality ($\equiv$), which is an external judgment. Distinguishing these notions provides ITT with its good computational properties: definitional equality is a decidable fragment of propositional equality and allows type checking to be algorithmically decidable. This fragment can be changed, such as by allowing the addition of rewrite rules [17]. The two extremes are: extensional type theory (ETT) [36], where every equality is definitional, and axiomatic type theory (ATT) [8, 44], where no equality is definitional.

For ETT the external and internal notions of equality match. This prevents it from being compatible with homotopy type theory: it proves uniqueness of identity proofs (UIP) which contradicts univalence [27, 47]. In addition, definitional equality is undecidable in ETT, which means that type checking is undecidable as well. By contrast, the semantics of ETT is easier to explore and allows for a simple categorical description of its type formers. Models can be formulated using locally Cartesian closed categories as seen by Seely [43]. However, Seely interprets substitutions using pullbacks, which are only specified up to isomorphism, leading to coherence problems. The precise statement is a biequivalence of 2-categories as shown by Clairambault and Dybjer [16] building on work of Curien, Hofmann and Garner [19, 26, 20], which has been extended by Maietti [35] and Van der Weide [48]:

In this paper we generalise this to ATT. The main reason to study axiomatic type theory is that – while it only has one notion of equality like ETT, and is therefore easier to study – it is minimal and therefore compatible with ITT and its extensions, and provides a larger class of models. In addition, there are conservativity results for ATT which means that we can use it to study ITT and ETT: for example, ETT is conservative over ATT extended with function extensionality and UIP [49, 13, 45]. Moreover, from a mathematical perspective, axiomatic type formers enjoy the advantage of being homotopy invariant, as explained in [3, 4]: any type that is homotopy equivalent to the one given by the formation rule of a type former satisfies the same rules.

We generalise the known correspondence by considering the notion of a path category introduced by Van den Berg and Moerdijk [9, 6]. Path categories have equivalences as a primitive notion, which allows the omission of explicit interpretations of the elimination and computation rules. This is a considerable simplification, since it is exactly these rules that become unwieldy in ATT, especially in a setting without $\mathrm{\Pi }$-types. We show a correspondence:

This extends the existing results since finitely complete categories can be seen as degenerate path categories where dependent homotopy exponentials simplify to dependent exponentials. We do this by proving an isomorphism of 2-categories between path categories and an existing notion of weak semantics: display map categories. Then we apply the results of Lumsdaine and Warren [33] and Bocquet [12] to strictify those path categories that satisfy the additional logical framework (21) condition, giving a biequivalence with models satisfying this condition. We also introduce a new and more fine-grained notion – that of a display map path category, which distinguishes types and telescopes – and prove similar correspondences:

This result is more modular without introducing significant additional complexity: display map path categories only have axiomatic =-types by default and can be extended with any combination of $\mathrm{𝟙}$, $\mathrm{\Sigma }$, and $\mathrm{\Pi }$ in a relatively simple way.

We will assume some familiarity with the syntax of Martin-Löf type theory; for an overview, see [37, 47]. Our main focus will be a minimal type theory with only propositional equality (the $=$-types) and no definitional equality (the $\equiv$-judgement). For the structural rules, the unit type ($\mathrm{𝟙}$), dependent product types ($\mathrm{\Sigma }$) and dependent function types ($\mathrm{\Pi }$), see Appendix A. Type formers in intensional Martin-Löf type theory are given by formation, introduction, elimination, and computation ($\beta$) rules. For the $=$-types, these are:

In extensional type theory, we also add a uniqueness ($\eta$) rule:

The $\eta$-rule implies that propositional equality and definitional equality coincide, making type checking undecidable. We are mainly interested in the other direction – a minimal type theory without definitional equality – so we modify intensional $=$-types in two ways: we weaken the $\beta$-rule (definitional equality) to a $\beta$-axiom (propositional equality), and fix the variable $x$ in place as a constant term $a$ in the eliminator:

These two modifications are orthogonal. The main focus of this paper is on the first one: weakening the $\beta$-rule to a $\beta$-axiom, that is, only requiring the $=$-type to be inhabited instead of requiring a judgemental equality. This weaker notion of $=$-type is called an axiomatic $=$-type, and is the version that appears in cubical type theory [18] as well as in axiomatic type theory (type theory without reductions) [8]. The other modification, fixing one of the two endpoints, is a technical variation known as based path induction or the Paulin-Mohring eliminator [41]. With $\mathrm{\Pi }$-types, based and unbased path induction are equivalent. However, without $\mathrm{\Pi }$-types, the based version is stronger and better behaved. For example, the transport ${\alpha }_{\ast }b:B[a^{\prime }/x]$ of a term $b:B[a/x]$ along an equality $\alpha :a{=}_A{a}^{\prime }$ can be defined as ${\mathrm{𝗂𝗇𝖽}}_b^{=}(\alpha )$ using based path induction, while it is not definable using unbased path induction.

Alternatively, to give the unbased version the same strength as the based version, we can extend it with a telescope $\mathrm{\Omega }$. This is called the parametrized or Frobenius version of path induction. For example, axiomatic parametrized unbased path induction is given by:

We have equivalences between axiomatic/intensional/extensional versions of path induction:

while the original unparametrized unbased version is weaker without $\mathrm{\Pi }$-types. We prove a semantic version of this in Proposition 14.

In general we use the following terminology: a type former is axiomatic if we only have a $\beta$-axiom, intensional if it has a $\beta$-rule, and extensional if it also has an $\eta$-rule. Note that the $\beta$-axiom generally implies the existence of an $\eta$-axiom [3, 4]. The type theory is axiomatic/intensional/extensional if every type former is. Note that having extensional =-types implies that every other type former is extensional.

There is a big zoo of semantic frameworks for the structural part of dependent type theory; see [1] for an overview of the equivalences. These range from frameworks that closely follow the syntax (such as categories with families, which have primitive notions for contexts, types, and terms) to frameworks that simplify the structure (such as display map categories, where a type $A$ in context $\mathrm{\Gamma }$ is identified with the display map or context projection $\mathrm{\Gamma }.A\to \mathrm{\Gamma }$, and a term $a$ of $A$ is identified with the induced context map $\mathrm{\Gamma }\to \mathrm{\Gamma }.A$). We will be working in the later setting for two reasons: it allows us to talk about both strict and weak models, and can easily be extended using ideas of homotopy theory as we will see in Section 4.

The objects of a display map category are called contexts. A type $A$ in context $\mathrm{\Gamma }$ consists of a context suggestively written $\mathrm{\Gamma }.A$ together with a display map $p_A:\mathrm{\Gamma }.A-⊳\mathrm{\Gamma }$. A term $a$ of $A$ is a section of $p_A:\mathrm{\Gamma }.A-⊳\mathrm{\Gamma }$, that is, a map $a:\mathrm{\Gamma }\to \mathrm{\Gamma }.A$ such that $p_{A}a=1_{\mathrm{\Gamma }}$. More generally, a term $a$ of $A$ for a context map $\sigma :\mathrm{\Delta }\to \mathrm{\Gamma }$ is a map $a:\mathrm{\Delta }\to \mathrm{\Gamma }.A$ such that $pa=\sigma$. Such a term of $A$ for $\sigma$ is equivalent to having a term of the pullback $A[\sigma ]$ of $A$ along $\sigma$:

We call $A[\sigma ]$ the re-indexing or substitution of $A$ along $\sigma$, and ${\sigma }^{\mathrm{▽}}$ the weakening of $\sigma$ for $A$. We extend both of these notions further. If $a$ is a term of type $A$, then, for any choice of $A[\sigma ]$, we write $a[\sigma ]$ for the unique term of type $A[\sigma ]$ such that $({\sigma }^{\mathrm{▽}})(a[\sigma ])=a\sigma$:

For a type $B$ in context $\mathrm{\Gamma }$ we write $B^{\mathrm{▽}}≔B[p_A]$ for the induced type in an extended context $\mathrm{\Gamma }.A$; and for a term $b$ of $B$ we write $b^{\mathrm{▽}}≔b[p_A]$ for the induced term of $B^{\mathrm{▽}}$. Finally, for any choice of $B^{\mathrm{▽}}$, we use the categorical notation $(a,b):\mathrm{\Gamma }\to \mathrm{\Gamma }.A.B^{\mathrm{▽}}$ for the term of the pullback induced by terms $a:\mathrm{\Gamma }\to \mathrm{\Gamma }.A$ and $b:\mathrm{\Gamma }\to \mathrm{\Gamma }.B$. We extend this to the dependent case by writing $(a,b):\mathrm{\Gamma }\to \mathrm{\Gamma }.A.B$ for the term $a^{\mathrm{▽}}b$ induced by terms $a:\mathrm{\Gamma }\to \mathrm{\Gamma }.A$ and $b:\mathrm{\Gamma }\to \mathrm{\Gamma }.B[a]$. For a type $A$ we have always the variable term or diagonal ${\delta }_a≔(1_{\mathrm{\Gamma }.A},1_{\mathrm{\Gamma }.A}):\mathrm{\Gamma }.A\to \mathrm{\Gamma }.A.A^{\mathrm{▽}}$.

Type formers follow the syntactic specification. For example, an =-type is given by:

We say that a display map category with $=$-types has weakly stable $=$-types if for every type $A$ in context $\mathrm{\Gamma }$ there exist an $=$-type ${\mathrm{𝖨𝖽}}_A$ and for every $\sigma :\mathrm{\Delta }\to \mathrm{\Gamma }$ we can equip ${\mathrm{𝖨𝖽}}_A[{\sigma }^{\mathrm{▽}\mathrm{▽}}]$ and

with the additional data required to form an $=$-type. To explain the intuition for this notion, we first need to explain the idea of an equivalence. A (homotopy) equivalence between types $A$ and $B$ fibered over a context $\mathrm{\Gamma }$ is a term $b:\mathrm{\Gamma }.A\to \mathrm{\Gamma }.B$ of $B$ for $p_A$ such that there exists a term $a:\mathrm{\Gamma }.B\to \mathrm{\Gamma }.A$ of $A$ for $p_B$ so that the two compositions are pointwise propositionally equal to the identity, that is, we have terms of ${\mathrm{𝖨𝖽}}_A[ab,1_{\mathrm{\Gamma }.A}]$ and ${\mathrm{𝖨𝖽}}_B[ba,1_{\mathrm{\Gamma }.B}]$. One can observe that between any two $=$-types ${\mathrm{𝖨𝖽}}_A,{\mathrm{𝖨𝖽}}_A^{\prime }$ for $A$ there exists an equivalence that respects the data of an =-type, and that any type that is equivalent to an $=$-type for $A$ can be given the additional data to form an $=$-type. Hence, weak stability is equivalent to the statement that =-types are preserved by re-indexing up to equivalence. This certainly holds in the syntax because the substitution of an =-type is still an =-type.

As explained in [1], there exists a 2-category $\mathrm{𝖣𝗂𝗌𝗉𝖢𝖺𝗍}$ of display map categories, functors preserving display maps and pullbacks of display maps, and natural transformations. We can specialize this to 0-cells that are rooted and 1-cells that preserve the terminal object. Another specialization is to 0-cells with additional weakly stable type formers and 1-cells that weakly preserve them; see Appendix B. In Section 5, we show that the 2-category of path categories is isomorphic to the 2-category ${\mathrm{𝖣𝗂𝗌𝗉𝖢𝖺𝗍}}_{{=}_{\mathrm{𝖺𝗑𝗂}},{\mathrm{𝟙}}_{\mathrm{𝖾𝗑𝗍}},{\mathrm{\Sigma }}_{\mathrm{𝖾𝗑𝗍}}}^{\mathrm{𝗋𝗈𝗈𝗍}}$ of rooted display map categories with weakly stable axiomatic $=$-types, extensional $\mathrm{𝟙}$-types, and extensional $\mathrm{\Sigma }$-types.

We start with the following notion from abstract homotopy theory:

We have a forgetful functor from rooted display map categories to clans (only remembering the fibrations, that is, the compositions of display maps), and conversely every clan gives a rooted display map category in a cofree way: the entire class of fibrations can be taken as the display maps. To emphasize the topological view, we start writing the pullback of $\mathrm{\Omega }-⊳⊳\mathrm{\Gamma }$ and $\sigma :\mathrm{\Delta }\to \mathrm{\Gamma }$ as $\mathrm{\Delta }{\times }_{\mathrm{\Gamma }}\mathrm{\Omega }$ instead of $\mathrm{\Delta }.\mathrm{\Omega }[\sigma ]$. We extend clans with equivalences:

This is a strengthening of Brown’s notion of a category of fibrant objects [14] in two ways: (a) we have 2-out-of-6 instead of the weaker 2-out-of-3 (if for $A\to B\to C$ two of the three maps are equivalences, then so is the third), which is equivalent to saturation [42], and (b) every trivial fibration has a section, which is equivalent to every object being cofibrant.

A trivial example of a path category is a category with finite limits where every morphism is a fibration, and only isomorphisms are equivalences. More interesting examples arise by taking the fibrant-cofibrant objects of a model category where every object is cofibrant. In addition, the effective topos can be seen as the homotopy category of a path category [7].

Four main results for path categories are: factorization, slicing, lifting, and saturation, which we will show here; for proofs, see [9]. First, notice that finite products exist and that the projections are pullbacks of fibrations and therefore fibrations. In addition, we see that the source and target maps $s,t:PA\to A$ are always trivial fibrations: equivalences by 2-out-of-3 on $sr=1$ and $tr=1$, and fibrations as compositions of fibrations because $s={\pi }_0(s,t)$ and $t={\pi }_1(s,t)$. Now we can state:

Using generalized elements, we think of the mapping path space $Lf≔B{}_f{}^{}\times _s^{}PA$ as the space of pairs $(b,\alpha )$ with $b$ in $B$ and $\alpha$ a path in $A$ with source $fb$:

Then $w_f≔(1_B,rf)$ maps $b$ in $B$ to the pair consisting of $b$ and the trivial path on $fb$, and $p_f≔t{\pi }_1$ maps $(b,\alpha )$ to the target of $\alpha$.

We anticipated that path categories would provide a natural semantics for axiomatic $=$-types. In this section, we establish the rigorous correspondence by rephrasing a path category as a display map category with weakly-stable axiomatic $=$-types and three other properties: a root, (pseudo-stable) extensional $\mathrm{𝟙}$-types, and (pseudo-stable) extensional $\mathrm{\Sigma }$-types. In Section 6, we introduce a version of path categories that does not necessarily model extensional $\mathrm{𝟙}$-types and $\mathrm{\Sigma }$-types, and hence provides semantics for a minimal axiomatic type theory with only axiomatic $=$-types. We will also see how we can extend this with other axiomatic type formers. Let us start from these last properties:

To define a more fine-grained semantics that does not necessarily model extensional $\mathrm{𝟙}$-types and extensional $\mathrm{\Sigma }$-types, we will add some additional structure to path categories: we exchange the clan for a display map category to distinguish display maps and fibrations.

We call a display map path category rooted if the underlying display map category is. Every rooted display map path category is in particular a path category, and every path category gives a cofree rooted display map path category by considering every fibrations to be a display map. Now a natural question is: are path display maps $P_{\mathrm{\Gamma }}A-⊳A{\times }_{\mathrm{\Gamma }}A$ already enough to define path fibrations $P_{\mathrm{\Gamma }}\mathrm{\Delta }-⊳⊳\mathrm{\Delta }{\times }_{\mathrm{\Gamma }}\mathrm{\Delta }$? This is the case in the syntax: with $=$-types (and transport) we can define =-telescopes. For a telescope $\overrightarrow{x}:\overrightarrow{A}$ of $\mathrm{\Gamma }$ we define the =-telescope $\overrightarrow{\chi }:{\overrightarrow{\chi }}_{\ast }\overrightarrow{x}{=}_{\overrightarrow{A}}{\overrightarrow{x}}^{\prime }$ of $\mathrm{\Gamma },\overrightarrow{x}:\overrightarrow{A},{\overrightarrow{x}}^{\prime }:\overrightarrow{A}$ where:

The same is true in general. However, we do need to assume a notion of transport:

In this last section, we use our isomorphisms to prove a coherence result: a biequivalence between a certain class of path categories and the class of (strict) models of a specific theory. First, we recall the LF condition that Lumsdaine and Warren [33] use to strictify:

This condition is very close to the existence of $\mathrm{\Pi }$-types for (display map) path categories but distinct in two important ways: we do not ask for ${\mathrm{\Pi }}_{A}B\to \mathrm{\Gamma }$ to be a display map (so ${\mathrm{\Pi }}_{A}B$ is not a type), and we ask for an isomorphism instead of a full map or equivalence. As a consequence, it captures a situation that is better viewed as a logical framework [25] or a 2-level type theory [35, 2] where the ambient theory has strong $\mathrm{\Pi }$-types regardless of the internal theory that we consider.

This follows by combining Theorem 16 with the work of Lumsdaine and Warren [33], and Bocquet [12]. As they work in different frameworks, we provide the details in the full version [39, Appendix D].

We have established a biequivalence between path categories and models of axiomatic $=$-types extended with extensional $\mathrm{𝟙}-$ and $\mathrm{\Sigma }$-types. This result provides a clean categorical formulation of the semantics of axiomatic =-types, allowing us to construct strict models directly from weak homotopy-theoretic structures. Furthermore, we introduced the novel notion of a display map path category. This more fine-grained structure distinguishes between types and telescopes, and offers a semantics for minimal axiomatic type theories that do not include extensional type formers. As we saw, this leaves room to add other axiomatic type formers, such as axiomatic $\mathrm{𝟙}$-, $\mathrm{\Sigma }$-, and $\mathrm{\Pi }$-types, providing a modular semantics for axiomatic type theory. Our framework lays the groundwork for future investigations into the semantics of higher inductive types and computational interpretations of univalence.