2.1 Syntax

We stay close to the presentation of type theory given in the appendix in the homotopy type theory book (The Univalent Foundations Program, 2013, Appendix A.2). There is however one technical difference that we want to make. The semantics of Russell-style universes (where terms of the universe are types) is less elegant than the one of Tarski-style universes (if A is a term of a universe, then $\textsf{El}\ A$ is a type), and the former can be seen as a special case of the latter. This is a general observation in type theory which has little to do with the idea of having two levels; see also point (M2) in Subsection 2.4.

We consider the judgements $\Gamma \; \textrm{ctx}$ , $\Gamma \vdash a : A$ , and $\Gamma \vdash a \equiv a' : A$ . In addition, we consider the two judgements

\begin{equation*} \Gamma \vdash A \; \textrm{type}_j \qquad\qquad\qquad \Gamma \vdash A \; {\textrm{type}}^{\textsf{i}}_j\end{equation*}

Here, j is a natural number, the size of A. The first means that A is an outer type, the second that A is an inner type. Similar to the judgement $\Gamma \vdash a \equiv a' : A$ , we consider equality judgements for types.

For the outer level of the theory that we consider, we have the following basic types and type formers:

• $\Pi$ , the type former of dependent functions;

• $\Sigma$ , the type former of dependent pairs;

• $+$ , the coproduct type former;

• ${{\textbf{1}}}$ , the unit type;

• ${{\textbf{0}}}$ , the empty type;

• ${{\mathbb{N}}}$ , the type of natural numbers;

• $=$ , the equality type;

• a cumulative hierarchy ${{\mathcal{U}}}_0,\ {{\mathcal{U}}}_1, \ldots$ of universes;

• inductive and quotient types (not used in this paper).

The inner level of our 2LTT has the same basic types and type formers. We annotate them to avoid confusion: ^{Footnote 5}

• ${\Pi}^{\textsf{i}}$ , the type former of inner dependent functions;

• ${\Sigma}^{\textsf{i}}$ , the type former of inner dependent pairs;

• $\mathbin{{+}^{\textsf{i}}}$ , the inner coproduct type former;

• ${{{\textbf{1}}}}^{\textsf{i}}$ , the inner unit type;

• ${{{\textbf{0}}}}^{\textsf{i}}$ , the inner empty type;

• ${{{\mathbb{N}}}}^{\textsf{i}}$ , the inner type of natural numbers;

• ${=}^{\textsf{i}}$ , the inner equality (or path-equality) type (in the sense of $\textsf{HoTT}$ );

• a cumulative hierarchy ${{{\mathcal{U}}}}^{\textsf{i}}_0, {{{\mathcal{U}}}}^{\textsf{i}}_1, \ldots$ of inner universes;

• possibly inductive and higher inductive types.

The basic rules for $\Pi$ , $+$ , ${{\textbf{1}}}$ , ${{\textbf{0}}}$ , ${{\mathbb{N}}}$ , as well as ${\Pi}^{\textsf{i}}$ , ${+}^{\textsf{i}}$ , ${{{\textbf{1}}}}^{\textsf{i}}$ , ${{{\textbf{0}}}}^{\textsf{i}}$ , ${{{\mathbb{N}}}}^{\textsf{i}}$ are the standard ones and match those given in the HoTT book (The Univalent Foundations Program, 2013, Appendix A.2), modulo the difference between Russell and Tarski universes. For $\Sigma$ and ${\Sigma}^{\textsf{i}}$ , we assume in addition the judgemental $\eta$ -law $x \equiv (\pi_1(x),\pi_2(x))$ . ^{Footnote 6} Note that all inference rules in the cited appendix are stated in terms of universes, and in our situation, all occurrences of $A : {{\mathcal{U}}}_j$ are replaced by $A \; \textrm{type}_j$ and $A : {{{\mathcal{U}}}}^{\textsf{i}}_j$ by $A \; {\textrm{type}}^{\textsf{i}}_j$ ; this keeps the two levels separate. For example, for the formation of coproducts, we have the rules

To emphasise, these rules do not allow us to form a coproduct of an inner and an outer type! The outer equality type $=$ and inner equality (path-equality) type ${=}^{\textsf{i}}$ have the usual rules as well. Since equality is the central aspect of 2LTT, we state the rules for the outer equality type explicitly, although they are completely standard:

together with the usual computation rule:

\begin{equation*} J_P(d) [a, {{\textsf{refl}_{a}}}] \equiv d.\end{equation*}

The rules of the inner type are the same, with $\textrm{type}_j$ replaced by ${\textrm{type}}^{\textsf{i}}_j$ , $=$ by ${=}^{\textsf{i}}$ , and ${{\textsf{refl}_{a}}}$ by ${{{\textsf{refl}}^{\textsf{i}}_{a}}}$ . The $\textsf{El}$ operator is assumed to be an isomorphism between terms of ${{\mathcal{U}}}_j$ (or ${{{\mathcal{U}}}}^{\textsf{i}}_j)$ and (inner/outer) types at level i. For the outer equality type, we furthermore assume the principles of UIP and function extensionality:

Instead of UIP, we could add the slightly stronger principle called Axiom K (Streicher, 1993). This is a version of (2.1) (with its computation rule) for inducting on loops with a fixed base point. It does not make a difference in our treatment.

All inner universes ${{{\mathcal{U}}}}^{\textsf{i}}_j$ are assumed to be univalent in the sense of homotopy type theory.

Context extension also follows the rules of The Univalent Foundations Program (2013, Appendix A.2), but note that there is only one judgement of the form $\Gamma \vdash \textrm{ctx}$ and there are two hierarchies of types. Since context extension works for every type, we have:

This means that contexts are shared between the two levels.

Finally, we have a conversion operation $\textrm{c}$ which turns inner types into outer types: Whenever we have $\Gamma \vdash A \; {\textrm{type}}^{\textsf{i}}_j$ , we have a type $\textrm{c}(A)$ such that $\Gamma \vdash \textrm{c}(A) \; \textrm{type}_j$ and this operation preserves context extension, in the sense that $\Gamma . A$ and $\Gamma . \textrm{c}(A)$ are the same context. This operation is natural in $\Gamma$ , and the detailed specification is given in the next subsection. Preservation of context extension in particular means that the set of terms of A and $\textrm{c}(A)$ are isomorphic. For the ‘forwards-direction’, we again write $\textrm{c}$ , that is, for $\Gamma \vdash a:A$ , we have $\Gamma \vdash \textrm{c}(a) : \textrm{c}(A)$ .

2.2 Semantics

We define what it means to be a model of two-level type theory. For this, we use the language of categories with families (cwfs) (Dybjer, Reference Dybjer, Berardi and Coppo1995). We have a choice of how to handle universe hierarchies. In this work, we aim for concreteness and fix a cumulative hierarchy indexed by natural numbers, with no notion of top-level type.

Given a presheaf F over a category $\mathcal{E}$ , we denote by $\mathcal{E}/F$ its category of elements. Recall the following notion.

• a presheaf $\textsf{Ty}$ over $\mathcal{E}$ (types),

• a presheaf $\textsf{Tm}$ over $\mathcal{E}/\textsf{Ty}$ (terms),

• a terminal object $1 \in \mathcal{E}$ (global or empty context),

• for all $\Gamma \in \mathcal{E}$ and $A \in \textsf{Ty}(\Gamma)$ , a terminal object $(\Gamma.A, p_A, q_A)$ in the category of triples $(\Delta, \sigma, t)$ where $\Delta \in \mathcal{E}$ , $\sigma \mathbin{\colon} \Delta \rightarrow \Gamma$ , and $t \in \textsf{Tm}(\Delta, A [\sigma])$ (context extension).

In the above, $[\sigma]$ denotes the action of $\textsf{Ty}$ on the morphism $\sigma$ . The action of $\textsf{Tm}$ on morphisms is written similarly. These operations are referred to as substitutions of types and terms, respectively.

We treat Definition 2.2 as having algebraic character, immediately giving rise to a category of cwfs. This applies to all the definitions in this subsection. They are to be read as not just introducing a certain concept (algebraic in character), but also the corresponding notion of morphism for it, part of a category structure.

In the usual fashion, one has notions of cwfs with type formers and axioms such as $\Pi$ -types, identity types and function extensionality. In the following, we abbreviate a generic selection of such type formers and axioms by T and speak of cwfs having type formers T.

Given a cwf $\mathcal{E}$ , we also speak of a cwf structure on the category $\mathcal{E}$ . We abbreviate such a cwf structure just by its presheaf of types. By restriction, we obtain a category of cwf structures with type formers T on a fixed category $\mathcal{E}$ . Note that the action of its morphisms on terms is an isomorphism (this follows from preservation of extension).

Definition 2.4. A cwf hierarchy $\textsf{Ty}$ with type formers T on a category $\mathcal{E}$ is a sequential diagram

of cwf structures with type formers T on $\mathcal{E}$ .

We can regard a cwf hierarchy as a multi-sorted cwf indexed over the poset $\omega$ . This makes it a cumulative hierarchy. Note that the natural transformation $\textsf{Ty}_j \rightarrow \textsf{Ty}_{j+1}$ preserve the type formers T. We will omit the subscript index into the hierarchy when it is inferable or we are only interested at a fixed index.

We refer to such a model by just its cwf hierarchy $\textsf{Ty}$ . We call ${{\mathcal{U}}}_j$ the j-th universe. If unambiguous, we will omit the universe index j. Note that the above definition models a cumulative hierarchy of universes (closed under type formers), with no top-level notion of type.

We consider two important kinds of models of Martin-Löf type theory.

In applications, one can add more type formers to these notions as desired, for example higher inductive types to Definition 2.7 or quotient types to Definition 2.6. All our example models of set type theory are in fact models of extensional type theory, i.e. have equality reflection. For our developments here, the given type formers will suffice.

Ignoring type formers, a two-level model can be seen as a multi-sorted cwf indexed over the poset $\lbrace{0 \rightarrow 1}\rbrace \times \omega$ . With type formers, we have two separate multi-sorted cwfs (with inner and outer type formers, respectively) indexed over $\omega$ . The conversion morphism $\textrm{c}$ can be described as a morphism of multi-sorted cwfs that is the identity on the category of contexts. Consequently, context extension is automatically preserved: if we have $\Gamma \vdash A \; {\textrm{type}}^{\textsf{i}}_j$ , then $\Gamma.A$ and $\Gamma.\textrm{c}(A)$ are the same object of $\mathcal{E}$ . ^{Footnote 7} Note that we assume no interaction between inner and outer type formers under the conversion morphism.

Finally, we can make precise two-level type theory.

2.3 Preservation of type formers by conversion

For this subsection, we fix a model $\mathcal{E}$ of two-level type theory. We have assumed very little about the conversion morphism $\textrm{c} \mathbin{\colon} {\textsf{Ty}}^{\textsf{i}} \rightarrow \textsf{Ty}$ , but in this subsection, we see that it being a morphism of cwf hierarchies allows us to derive important properties.

Further, we can use that many types are characterised by universal properties (the syntactical equivalent of which are elimination rules). The consequences are summarised in the following statement.

Lemma 2.11. Let $\Gamma \in \mathcal{E}$ , $A \in {\textsf{Ty}}^{\textsf{i}}(\Gamma)$ and $B \in {\textsf{Ty}}^{\textsf{i}}(\Gamma.A)$ . We have the following morphisms natural in $\Gamma$ . All morphisms live in the slice over $\Gamma$ (and 7 lives in the slice over $\Gamma.A.A$ ):

(1)

(2)

(3)

(4)

(5)

(6)

(7)

(8)

Moreover, the three annotated morphisms are natural isomorphisms.

Before constructing the morphisms, let us make some remarks. Via the adjunction with $\Pi$ , the above morphisms give rise to internal functions at the outer level. This way, isomorphisms become judgemental internal isomorphisms, i.e. the functions in both directions compose judgementally to the identity.

It is also worth emphasising the asymmetry that the conversion function $\textrm{c}$ introduces: In general, the rules of the system mean that it is usually easier to eliminate from outer types into inner types than vice versa. While $\Pi$ , $\Sigma$ and ${{\textbf{1}}}$ at the outer level are ‘the same’ as at the inner level, in the sense made precise in the lemma above, the same is not automatically the case for the remaining types and type formers. For the case of equality types however, this assumption would destroy our motivation for two-level type theory altogether. Although invertibility of (4)–(6), discussed in Subsection 2.4 under (A1), does hold in some of the intended models, it is not valid with the point of view of the outer level as internalised meta-theory of the object theory given by the inner level, made precise by the presheaf model of two-level type theory in Subsection 2.5.3. From that point of view, some of the maps and the absence of their invertibility can be understood as follows:

• Coproducts $A+B$ : given a term of A or a term of B in the meta-theory, we get an element of $A \mathbin{{+}^{\textsf{i}}} B$ , but not vice versa. For example, the context might not allow us to normalise an element of a coproduct type to a coprojection.

• Empty type ${{\textbf{0}}}$ : from a contradiction in the meta-theory, one can get a contradiction in the object theory, but not vice versa.

• Natural numbers ${{\mathbb{N}}}$ : we think of an external natural number as a numeral. From a numeral, one can get an internal natural number, but from an element of the inner natural numbers type, we do not always get a numeral.

• Equality $x=y$ : two meta-theoretically (e.g. syntactically) equal expressions are provably equal via reflexivity, but provably equal expressions might not be equal meta-theoretically (syntactically).

The last morphism (8) says that inner types are (up to $\textrm{c}$ ) outer types, but we would not expect the reverse since not every meta-theoretic statement can be internalised.

Proof of 2.11. We start with the three isomorphisms. Recall that inner and outer ${{\textbf{1}}}/\Sigma$ -types come with $\eta$ -laws. Since $\textrm{c}$ preserves context extensions, it easily follows that $\textrm{c}$ preserves these type formers up to canonical isomorphism. In fact, this is true for cwf morphisms in general, without the requirement that the underlying functor is an identity. In detail, the isomorphism (1) is given by

\begin{align*}\Gamma.\textrm{c}({{{\textbf{1}}}}^{\textsf{i}})&=\Gamma.{{{\textbf{1}}}}^{\textsf{i}}\\&\simeq\Gamma\\&\simeq\Gamma.{{\textbf{1}}}\end{align*}

and the isomorphism (2) is given by

\begin{align*}\Gamma.\textrm{c}({\Sigma}^{\textsf{i}}_A B)&=\Gamma.{\Sigma}^{\textsf{i}}_A B\\&\simeq\Gamma.A.B\\&=\Gamma.c(A).c(B)\\&\simeq\Gamma.\Sigma_{\textrm{c}(A)} \textrm{c}(B).\end{align*}

Since $\Pi$ -types in the inner and outer level come with the $\eta$ -law, their terms are uniquely characterised as terms of the codomain type. We have, naturally in $\sigma \mathbin{\colon} \Delta \rightarrow \Gamma$ :

\begin{align*}\mathcal{E}/\Gamma\left(\Delta, \Gamma.\textrm{c}({\Pi}^{\textsf{i}}_A B)\right)&=\mathcal{E}/\Gamma\left(\Delta, \Gamma.{\Pi}^{\textsf{i}}_A B\right)\\&\simeq\mathcal{E}/\Gamma.A\left(\Delta.A[\sigma], \Gamma.A.B\right)\\&=\mathcal{E}/\Gamma.\textrm{c}(A)\left(\Delta.\textrm{c}(A[\sigma]), \Gamma.\textrm{c}(A).\textrm{c}(B)\right)\\&=\mathcal{E}/\Gamma.\textrm{c}(A)\left(\Delta.\textrm{c}(A)[\sigma], \Gamma.\textrm{c}(A).\textrm{c}(B)\right)\\&\simeq\mathcal{E}/\Gamma\left(\Delta, \Gamma.\Pi_{\textrm{c}(A)} \textrm{c}(B)\right),\end{align*}

from which (3) follows by Yoneda. The morphism (4) is given by the usual properties of outer and inner coproduct. We have $\Gamma.A \rightarrow \Gamma.\textrm{c}(A \mathbin{{+}^{\textsf{i}}} B)$ and $\Gamma.B \rightarrow \Gamma.\textrm{c}(A \mathbin{{+}^{\textsf{i}}} B)$ due to the inner coproduct, and the outer coproduct lets us construct (4). The morphism (5) comes from the outer empty type ${{\textbf{0}}}$ ; no property of the inner empty type is used.

The usual morphism $\Gamma.\textrm{c}{({{{\textbf{1}}}}^{\textsf{i}} \, \mathbin{{+}^{\textsf{i}}} \, {{{\mathbb{N}}}}^{\textsf{i}})} \rightarrow \Gamma.\textrm{c}({{{\mathbb{N}}}}^{\textsf{i}})$ , by composition with (1) and (4), gives rise to a morphism $\Gamma.({{\textbf{1}}} + \textrm{c}({{{\mathbb{N}}}}^{\textsf{i}})) \rightarrow \Gamma.\textrm{c}({{{\mathbb{N}}}}^{\textsf{i}})$ . By the universal property of ${{\mathbb{N}}}$ , we get the morphism (6).

Outer equality implies inner equality in the sense of eq:equ-strict-fib by the J-eliminator of the outer equality and 2.10. Finally, (8) uses the isomorphisms $\textsf{El}_j$ and ${\textsf{El}}^{\textsf{i}}_j$ .

Our proof of the isomorphism (2) uses the judgemental $\eta$ -law for $\Sigma$ -types, a rule that is not assumed by all authors. If we only assume the induction principle with which the HoTT book (The Univalent Foundations Program, 2013, Chapter 1.6) characterises $\Sigma$ -types, without a judgemental $\eta$ -law, then $\Sigma$ becomes a positive type former, not generally preserved by $\textrm{c}$ .

In some of the models, we discuss in Subsection 2.5, the comparison maps (4)–(8) are indeed not isomorphisms.

2.4 Strengthenings and extensions

In Subsection 2.2, we have defined two-level type theory in a minimalistic fashion, eschewing properties that one might argue are reasonable to ask for. Indeed, other two-level type theories such as HTS are much more rigid.

We separate possible strengthenings into three groups. The first group has nothing to do with two-level type theory proper, concerning only the basic structure of models of Martin-Löf type theory as per Definition 2.5. In a model of two-level type theory, this applies to both inner and outer levels separately.

(M1) We can ask that the step maps $\textsf{Ty}_j \rightarrow \textsf{Ty}_{j+1}$ in the cwf hierarchy are mono. In a set-theoretic meta-theory, we could go further and demand the step maps are subpresheaf inclusions.

(M2) We can ask that the natural isomorphism $\textsf{El} \mathbin{\colon} \textsf{Tm}(\Gamma, {{\mathcal{U}}}_j) \simeq \textsf{Ty}_j(\Gamma)$ is an equality on the nose, i.e. that $\textsf{Tm}(\Gamma, {{\mathcal{U}}}_j) = \textsf{Ty}_j(\Gamma)$ and $\textsf{El} = {{\textsf{id}_{}}}$ . This has the effect of modelling Russell-style universes.

Implementing both of these points makes it possible to forgo the distinction between types and terms (with types just being terms of universes), treating the typing relation as going between terms. Together with univalence, this yields a type theory as in the homotopy type theory book (The Univalent Foundations Program, 2013, Appendix A.2) (but note that the $\eta$ -law for $\Sigma$ -types is not included there).

The second group concerns strictness properties of the conversion morphism $\textrm{c}$ relating the inner to the outer level in a model of two-level type theory as per Definition 2.9.

(T1) We can ask that the conversion morphism $\textrm{c} \mathbin{\colon} {\textsf{Ty}}^{\textsf{i}} \rightarrow \textsf{Ty}$ is mono on types, i.e. that $\textrm{c} \mathbin{\colon} {\textsf{Ty}}^{\textsf{i}}(\Gamma) \rightarrow \textsf{Ty}(\Gamma)$ is injective for $\Gamma \in \mathcal{E}$ . In a set-theoretic meta-theory, we could demand this is on the nose, i.e. that $\textrm{c}$ is a subpresheaf inclusion on types (and that the action on terms is not just an isomorphism, but an equality).

(T2) We can ask that the isomorphisms of 2.11 witnessing preservation of ${{\textbf{1}}}$ / $\Sigma$ / $\Pi$ -types under the conversion morphism $\textrm{c}$ are equalities on the nose. For $\Pi$ -types, this means the following: given $A \in {\textsf{Ty}}^{\textsf{i}}(\Gamma)$ and $B \in {\textsf{Ty}}^{\textsf{i}}(\Gamma.A)$ , we have $\textrm{c}({\Pi}^{\textsf{i}}_A B) = \Pi_{\textrm{c}(A)} \textrm{c}(B)$ ; given further $f \in {\textsf{Tm}}^{\textsf{i}}(\Gamma, {\Pi}^{\textsf{i}}(A, B))$ and $a \in {\textsf{Tm}}^{\textsf{i}}(\Gamma, A)$ , we have ${\textsf{app}}^{\textsf{i}}(f, a) = \textsf{app}(f, a)$ (preservation of abstraction is implied by this).

If we ask for any other type formers to be preserved by $\textrm{c}$ up to canonical isomorphism (such as in (A1) below), we can similarly ask that these isomorphisms are equalities on the nose.

(T3) We can ask that inner types are replete within outer types, i.e. that any outer type with extension isomorphic to that of an inner type is itself the image of an inner type under conversion. In detail, given $A \in \textsf{Ty}(\Gamma)$ and $B \in {\textsf{Ty}}^{\textsf{i}}(\Gamma)$ with $\Gamma.A \simeq \Gamma.B$ over $\Gamma$ , we have $A' \in {\textsf{Ty}}^{\textsf{i}}(\Gamma)$ with $A = \textrm{c}(A')$ , naturally in $\Gamma$ .

Implementing (T1) and (T2) essentially yields an (outer) type theory with a predicate of “being inner” on types that some type formers are closed under. With inner types named “fibrant”, this is the perspective taken in HTS.

The third group concerns more semantical extensions or axioms that will differ depending on what kinds of models one is interested in.

(A1) We can ask that conversion preserves certain “positive” type formers (minus identity types) up to canonical isomorphism, making for example the following canonical comparison maps over $\Gamma \in \mathcal{E}$ invertible:

We can weaken this by asking for an inverse only up to the outer identity type. Then, these properties become axioms internal to two-level type theory.

(A2) The following is a weakening of the assertion of (A1) for natural numbers that still allows for the construction of inner types of Reedy fibrant semisimplicial types (see 4.38 and afterwards). We can ask that countably infinite towers of (trivial) fibrations have (trivially) fibrant limits. The notion of fibration used here will be defined in Subsection 3.2 in terms of inner types. This is an internalisation (to the outer level) of the corresponding axiom considered for (co)fibration categories (Radulescu-Banu, Reference Radulescu-Banu2006, Definition 1.6.1) (see also Reference ShulmanShulman 2015b , Lemma 11.8).

(A3) Weakening (A2) further, we can ask that the outer natural number type is cofibrant. The notion of cofibrant type will be defined in Subsection 3.4, essentially meaning that exponentiation with it preserves inner types up to isomorphism. This axiom has been suggested by Shulman.

(A4) We can ask that the outer universes are “fibrant”, i.e. that there is $u \in {\textsf{Ty}}^{\textsf{i}}(\Gamma)$ such that $\Gamma.{{\mathcal{U}}} \simeq \Gamma.u$ over $\Gamma$ (or even ${{\mathcal{U}}} = \textrm{c}(u)$ ), naturally in $\Gamma \in \mathcal{E}$ . Again, we can weaken this to an isomorphism up to the outer identity type, making it an axiom internal to two-level type theory concerning universes.

(A5) We can ask that the outer level validates the equality reflection rule, i.e. forms a model of extensional type theory. This is the case in all the example models we are interested in.

We phrase this as an extension so that the base systems retains good meta-theoretical properties such as decidability of type checking. This is relevant for faithful implementation by current proof assistants (note though that some systems such as Andromeda (Bauer et al.) model equality reflection).

As a compromise, one may add features to the outer level that are partially extensional while retaining decidability of type checking. An example is the recent addition of universes of strict propositions (with judgemental uniqueness of elements) to Agda and Coq (Gilbert et al., Reference Gilbert, Cockx, Sozeau and Tabareau2019).

6. We may add more type formers to the inner or outer level as desired. For example, since the inner level is simply a version of homotopy type theory, it is natural to add inner higher inductive types. We can even add higher inductive-inductive types (see e.g. The Univalent Foundations Program 2013 and Kaposi and Kovács Reference Kaposi and Kovács2020 for a specification). Similarly, we can add quotient types or quotient inductive-inductive types (Altenkirch et al., Reference Altenkirch, Capriotti, Dijkstra, Kraus and Forsberg2018, Reference Altenkirch, Danielsson, Kraus, Esparza and Murawski2017; Altenkirch and Kaposi, Reference Altenkirch and Kaposi2016) to the outer level (note that the presence of uniqueness of identity proofs makes higher equalities moot).

Note that one may identify HTS as two-level type theory in our sense extended with the axioms (A1), (A4), (A5), (T1) and (T2), in their strongest form. In the following subsection, we will discuss which of the above strengthenings and extensions hold in each of several example models. This will provide justification for not including most of the above conditions as blanket assumptions. It will also serve as a guide to the reader on which assumption to include in their two-level type theory when they have a certain class of models in mind.

2.5 Example models

We discuss some key models of two-level type theory. All have in common that the underlying category is presheaves $\widehat{\mathcal{C}}$ over a category $\mathcal{C}$ and that the outer level is given by the standard presheaf model of extensional type theory (in particular, (A5) is validated) where types are (small) presheaves over the category of elements of their context. The only exception to this is in Proposition 2.16, where the outer level is different.

We briefly recall key details of this presheaf model in a set-theoretic meta-theory. Fix a sequence of Grothendieck universes $M_0 \in M_1 \in \ldots$ such that $\mathcal{C}$ lives in $M_0$ . Given $\Gamma \in \widehat{\mathcal{C}}$ , then $\textsf{Ty}_j(\Gamma)$ consists of presheaves over $\mathcal{C}/\Gamma$ valued in $M_j$ and $\textsf{Tm}_j(\Gamma, A)$ is the set of global sections of such a presheaf A. Then, $\textsf{Ty}_j$ is represented by ${{\mathcal{U}}}_j \in \widehat{\mathcal{C}}$ where ${{\mathcal{U}}}_j(X)$ is the set of presheaves over $\mathcal{C}/X$ valued in $M_j$ , which itself lives in $M_{j+1}$ . This defines the universe ${{\mathcal{U}}}_j \in \textsf{Ty}_{j+1}(1)$ . With types presented in this displayed form, the standard definition of type formers is substitution-stable and preserved under size change.

The above definition of types and universes is essentially that of Hofmann and Streicher (Reference Hofmann and Streicher1997). Other constructions are possible, for example following Voevodsky (Kapulkin and Lumsdaine, Reference Kapulkin and Lumsdaine2018, Subsection 2.1) or Shulman (Reference Shulman2015a) (the latter construction works equally in the non-univalent setting of classifying all maps, not fibrations), but necessitate further work to split type formers.

2.5.3 Presheaves over models of homotopy type theory

The material in the first half of this subsubsection follows Capriotti (2016, Chapter 3.2). The resulting models have guided the design choices of our two-level type theory.

We will first establish some preliminaries. A weak morphism $F \mathbin{\colon} \mathcal{C} \rightarrow \mathcal{D}$ of cwfs is a functor between underlying categories with natural transformations on types and terms that preserves the global context and extension only up to canonical isomorphism. Given interpretations of type formers T in $\mathcal{C}$ and $\mathcal{D}$ , it still makes sense to ask that F preserves the operations of T, transporting along these preservation isomorphisms when required. Indeed, by expressing the type formers T in a cwf $\mathcal{E}$ as operations internal to its presheaf category $\widehat{\mathcal{E}}$ , one may completely avoid the dependency of T on extension as an algebraic operation (Capriotti, Reference Capriotti2016; Uemura, Reference Uemura2019). Thus, we obtain a notion of weak morphism of cwfs with type formers T.

There is an evident notion of 2-morphism between weak cwf morphisms $F, G \mathbin{\colon} \mathcal{C} \rightarrow \mathcal{D}$ , a natural transformation $u \mathbin{\colon} F \rightarrow G$ such that $F A = (G A)[u_\Gamma]$ for $A \in \textsf{Ty}_\mathcal{C}(\Gamma)$ and $F t = (G t)[u_\Gamma]$ for additionally $t \in \textsf{Tm}_\mathcal{C}(\Gamma, A)$ . Note that this implies commutativity of

for $\Gamma \in \mathcal{C}$ and $A \in \textsf{Ty}_\mathcal{C}$ . This extends to a notion of 2-morphism for cwfs with type formers T by requiring that substitution along the components of u preserves the operations of T. With this, we obtain a (strict) 2-category of cwfs (with type formers T) and weak morphisms. It has the 1-category of cwfs (with type formers T) as a wide sub-2-category.

Importantly, the initial object $\mathcal{C}$ of the 1-category of cwfs (with type formers T) becomes biinitial in the 2-category of cwfs (with type formers T) and weak morphisms. That is, given an object $\mathcal{D}$ with a weak morphism $H \mathbin{\colon} \mathcal{C} \rightarrow \mathcal{D}$ , there is an isomorphism $H \cong F$ between weak morphisms where $F \mathbin{\colon} \mathcal{C} \rightarrow \mathcal{D}$ is the unique morphism. This may be derived from making the strict pseudolimit of H (seen as a diagram indexed by the walking arrow) into a cwf $\mathcal{E}$ (with type formers T):

• objects are triples (X, X’, f) where $X \in \mathcal{C}$ , $X' \in \mathcal{D}$ , and $f \mathbin{\colon} H(X) \simeq X'$ ,

• types over such an object are pairs (A, A’) with $A \in \textsf{Ty}_\mathcal{C}(X)$ and $A' \in \textsf{Ty}_\mathcal{D}(X')$ such that H(A) and A’ correspond over f,

• terms of such a type are pairs (t, t’) with $t \in \textsf{Tm}_\mathcal{C}(X, A)$ and $t' \in \textsf{Tm}_\mathcal{D}(X', A')$ such that H(t) and t’ correspond over f.

Note that A’ and t’ in the above description are redundant. We have projection morphisms $p_\mathcal{C} \mathbin{\colon} \mathcal{E} \rightarrow \mathcal{C}$ and $p_\mathcal{D} \mathbin{\colon} \mathcal{E} \rightarrow \mathcal{D}$ . By initiality of $\mathcal{C}$ , we have $G \mathbin{\colon} \mathcal{C} \rightarrow \mathcal{E}$ such that $p_\mathcal{C} \circ G = {{\textsf{id}_{\mathcal{C}}}}$ and $p_\mathcal{D} \circ G = F$ . The isomorphism $H \cong F$ is read off from it.

Everything we have said above extends analogously to cwf hierarchies (with type formers T), models of Martin-Löf type theory (with type formers T), models of homotopy type theory and models of two-level type theory.

Recall from Hofmann (1997) that for any category $\mathcal{C}$ , the category $\widehat{\mathcal{C}}$ of presheaves over $\mathcal{C}$ forms a model of extensional type theory. Here, the types and terms are defined as follows. Given a presheaf P, which we think of as a context, we define $\textsf{Ty}(P)$ to consists of (small) presheaves over the category $\mathcal{C} / P$ of elements of P (specifically, for $\textsf{Ty}_j(P)$ , we require these presheaves to be valued in the Grothendieck universe $M_j$ ). Given such a type $A \in \textsf{Ty}^i(P)$ over P, the set $\textsf{Tm}(A)$ of terms is the set of global sections of the corresponding presheaf over $\mathcal{C} / P$ .

In the special case where $\mathcal{C}$ is itself a cwf, we can define an additional, inner cwf structure ${\textsf{Ty}}^{\textsf{i}}$ on presheaves $\widehat{\mathcal{C}}$ with a morphism $\textrm{c} \mathbin{\colon} {\textsf{Ty}}^{\textsf{i}} \rightarrow \textsf{Ty}$ to the presheaf cwf structure $\textsf{Ty}$ . This works as follows. We can single out a special context (in other words, a type in the empty context), namely $\textsf{Ty}_\mathcal{C}$ itself. This context can play the role of a universe in the presheaf cwf $\widehat{\mathcal{C}}$ . In fact, we have a type $\textsf{Tm}_\mathcal{C} \in \textsf{Ty}(\textsf{Ty}_\mathcal{C})$ , acting as the universal family of this universe. The cwf structure induced by this universe forms the inner cwf structure ${\textsf{Ty}}^{\textsf{i}}$ of $\widehat{\mathcal{C}}$ . In detail, we define ${\textsf{Ty}}^{\textsf{i}} = y(\textsf{Ty}_\mathcal{C})$ , i.e. ${\textsf{Ty}}^{\textsf{i}}(P) = \widehat{\mathcal{C}}(P, \textsf{Ty}_\mathcal{C})$ , and let $\textrm{c}$ send $A \in {\textsf{Ty}}^{\textsf{i}}(P)$ to the restriction of $\textsf{Tm}_\mathcal{C}$ along the functor $\mathcal{C}/P \rightarrow \mathcal{C}/\textsf{Ty}_\mathcal{C}$ induced by A, i.e. to $c(A) \in \widehat{\mathcal{C}/P}$ sending $(\Gamma, x)$ to $\textsf{Tm}_\mathcal{C}(\Gamma, A(x))$ . We are then forced to define ${\textsf{Tm}}^{\textsf{i}}(P, A)$ as the set of global sections of $\textrm{c}(A)$ .

The Yoneda embedding $y_\mathcal{C} \mathbin{\colon} \mathcal{C} \rightarrow \widehat{\mathcal{C}}$ becomes a weak morphism of cwfs

(9) \begin{equation} y_\mathcal{C} \mathbin{\colon} \mathcal{C} \rightarrow (\widehat{\mathcal{C}}, {\textsf{Ty}}^{\textsf{i}}),\end{equation}

whose actions on types and terms are bijective by construction of ${\textsf{Ty}}^{\textsf{i}}$ .

Let $\mathcal{C}$ now support a selection of type formers T. We can lift the rules in T to corresponding operations and laws on the “universe” $\textsf{Ty}_\mathcal{C}$ in $(\widehat{\mathcal{C}}, \textsf{Ty})$ and thereby to interpretations of the type formers T in the inner cwf $(\widehat{\mathcal{C}}, {\textsf{Ty}}^{\textsf{i}})$ . Furthermore, the weak morphism (9) preserves these, i.e. $y_\mathcal{C}$ becomes a weak morphism of cwfs with type formers T. This process and its properties are explained in Hofmann (Reference Hofmann1997) for a specific set of type formers, and in Capriotti (Reference Capriotti2016) for a generic notion of type former.

We illustrate the above process for the formation operation for dependent products. We desire the following judgement in the presheaf cwf:

(10) \begin{equation} A : \textsf{Ty}_\mathcal{C}, B : \textsf{Tm}_\mathcal{C}(A) \rightarrow \textsf{Ty}_\mathcal{C} \vdash \Pi(A, B) : \textsf{Ty}_\mathcal{C}.\end{equation}

Naturally in $\Gamma \in \mathcal{C}$ , we are given:

1. (1) $A \in \textsf{Ty}_\mathcal{C}(\Gamma)$ ,

2. (2) naturally in $(\Delta, \sigma \mathbin{\colon} \Delta \rightarrow \Gamma) \in \mathcal{C} / \Gamma$ , a map $B_\sigma \mathbin{\colon} \textsf{Tm}_\mathcal{C}(\Delta, A[\sigma]) \rightarrow \textsf{Ty}_\mathcal{C}(\Delta)$ ,

and have to produce an element $\Pi(A, B) \in \textsf{Ty}_\mathcal{C}(\Gamma)$ . By the universal property of context extension in $\mathcal{C}$ , data in (2) are uniquely induced by just the element $B_{p_A} \in \textsf{Ty}(\Gamma.A)$ . Thus, our obligation precisely corresponds to the formation rule for $\Pi$ in $\mathcal{C}$ . Furthermore, after lifting to the cwf $(\widehat{\mathcal{C}}, {\textsf{Ty}}^{\textsf{i}})$ , we can check that the weak morphism (9) preserves the formation rule.

The above example makes it reasonable to expect that every type former can be lifted, rule by rule, from $\mathcal{C}$ , producing judgements that replicate each rule internally in the theory of $\widehat{\mathcal{C}}$ when expressed using the “universe” $\textsf{Ty}_C$ , and that hence one can interpret each rule in the inner presheaf cwf.

The above construction is functorial in the cwf structure $\textsf{Ty}_\mathcal{C}$ (with type formers T) on $\mathcal{C}$ and 2-functorial in $\mathcal{C}$ as an object of the 2-category of cwfs (with type formers T) and weak morphisms. From this, we obtain the following.

Proposition 2.13 Let $\mathcal{C}$ be a model of Martin-Löf type theory with type formers T. Assume that $(\textsf{Tm}_\mathcal{C})_j$ is valued in the Grothendieck universe $M_j$ for every i. Then, $\widehat{\mathcal{C}}$ forms a two-level model of Martin-Löf type theory with inner type formers T and outer types formers from extensional type theory. The Yoneda embedding extends to a weak morphism $y \mathbin{\colon} \mathcal{C} \rightarrow (\widehat{\mathcal{C}}, {\textsf{Ty}}^{\textsf{i}})$ of models of Martin-Löf type theory that acts bijectively on types and terms.

Furthermore, this operation is 2-functorial in $\mathcal{C}$ as an object of the 2-category of models of Martin-Löf type theory with type formers T and weak morphisms. The action on a weak morphism $F \mathbin{\colon} \mathcal{C} \rightarrow \mathcal{D}$ is as follows. The left Kan extension $F_ {\text{!}} \mathbin{\colon} \widehat{\mathcal{C}} \rightarrow \widehat{\mathcal{D}}$ extends to a weak morphism of two-level models as above. The natural isomorphism $F_{\text{!}} \circ y_\mathcal{C} \simeq y_\mathcal{D} \circ F$ of functors lifts to the 2-category of models of Martin-Löf type theory with type formers T and weak morphisms.

Proof. Applying the above discussion to the sequence of cwf structures $(\textsf{Ty}_\mathcal{C})_j$ with type formers T on $\mathcal{C}$ , we obtain a corresponding sequence of cwf structures

with type formers T on $\widehat{\mathcal{C}}$ . Yoneda preserves terminal objects, so sends the global section ${{\mathcal{U}}}_j$ of $(\textsf{Ty}_\mathcal{C})_{j+1}$ to a global section ${{{\mathcal{U}}}}^{\textsf{i}}_j$ of ${\textsf{Ty}}^{\textsf{i}}_{j+1}$ . Naturally in $\Gamma \in \mathcal{C}$ , we have

\begin{align*}{\textsf{Tm}}^{\textsf{i}}(y(\Gamma), {{{\mathcal{U}}}}^{\textsf{i}}_j)={\textsf{Tm}}^{\textsf{i}}(y(\Gamma), y({{\mathcal{U}}}_j))\simeq\textsf{Tm}_\mathcal{C}(\Gamma, {{\mathcal{U}}}_j)\simeq(\textsf{Ty}_\mathcal{C})_j(\Gamma)\simeq{\textsf{Ty}}^{\textsf{i}}_j(y(\Gamma)),\end{align*}

using that the action of (9) on types and terms is bijective. By cocontinuous extension, we thus have ${\textsf{Tm}}^{\textsf{i}}(X, {{{\mathcal{U}}}}^{\textsf{i}}_j) \simeq {\textsf{Ty}}^{\textsf{i}}_j(X)$ naturally in $X \in \widehat{\mathcal{C}}$ . By the smallness assumption, the map ${\textsf{Ty}}^{\textsf{i}}_j \rightarrow \textsf{Ty}$ restricts to ${\textsf{Ty}}^{\textsf{i}}_j \rightarrow \textsf{Ty}_j$ .

Seeing univalence as just another type former, the universes ${{{\mathcal{U}}}}^{\textsf{i}}_j$ in the above model are univalent if the original universes ${{\mathcal{U}}}_j$ in $\mathcal{C}$ are.

Corollary 2.14. Let $\mathcal{C}$ be a model of homotopy type theory. Assume that $(\textsf{Tm}_\mathcal{C})_j$ is valued in the Grothendieck universe $M_j$ for every i. Then, $\widehat{\mathcal{C}}$ forms a model of two-level type theory. The Yoneda embedding extends to a weak morphism $y \mathbin{\colon} \mathcal{C} \rightarrow (\widehat{\mathcal{C}}, {\textsf{Ty}}^{\textsf{i}})$ of models of homotopy type theory that acts bijectively on types and terms. Furthermore, this operation is 2-functorial in $\mathcal{C}$ as in Proposition 2.13.

We call this the presheaf model $\widehat{\mathcal{C}}$ of two-level type theory over the given model $\mathcal{C}$ of homotopy type theory. It will be key for proving conservativity of two-level type theory over homotopy type theory in Subsection 2.6.

Let us discuss strictness properties of conversion satisfies by the presheaf model. Depending on the specifics of the implementation of the outer types, $\textrm{c}$ may or may not have a chance to be mono. With our choice of presheaves over categories of elements, (T1) holds as long as the action of the presheaf $\textsf{Tm}_\mathcal{C}$ on objects is injective. Note that this can always be achieved by passing through the Grothendieck construction. None of the other strictness properties (T2) and (T3) are satisfied.

Remark 2.15. Concerning (T2), some effort is expended in Capriotti (2016, Chapter 3.2) to achieve strict preservation of ${{\textbf{1}}}/\Sigma/\Pi$ -types under what we here call conversion from the inner to outer level. This is achieved by defining the inner types more cleverly as certain free expressions involving the types of $\mathcal{C}$ and formal ${{\textbf{1}}}/\Sigma/\Pi$ -type forming operations. Unfortunately, this only works for “top-level” ${{\textbf{1}}}/\Sigma/\Pi$ -types and breaks whenever the kind of type in question has a classifier that is itself a type (of higher size). Thus, this technique is not applicable here.

The presheaf model does not preserve (up to isomorphism) “positive” type formers as in (A1). Note that the interpretation of empty types, coproducts, and natural numbers in the outer level is levelwise. Were (A1) to hold, then in an arbitrary context $\Gamma$ in $\mathcal{C}$ , there would be no terms of empty type, every term of coproduct type would be a constructor application, and every natural number term would be a canonical numeral. Even the weaker versions (A2) and (A3) do not hold in general. Note that (A2) holds if $\mathcal{C}$ supports dependent sums of “arity” $\omega$ (also known as record types with countably infinitely many fields). Axiom (A4) is also generally not satisfied.

As for the other example models, the outer level models extensional type theory, i.e. (A5) holds. Extension (A6) holds as far as permitted by the given model $\mathcal{C}$ of homotopy type theory.

We end this subsection by giving a modified version of the presheaf model where (T1) and (T2) hold. This is achieved by modifying the interpretation of the outer level. The technique is inspired by Shulman’s modification (Shulman, Reference Shulman2019, Appendix A) of the local universe splitting technique in the presence of universes (recall though that we do not make use of the local universe splitting technique).

Proposition 2.16. Denote by $({\textsf{Ty}}^{\textsf{i}}, \textsf{Ty}, \textrm{c})$ the presheaf model of two-level type theory on $\widehat{\mathcal{C}}$ as established by Corollary 2.14. There is a factorisation

in the category of cwf hierarchies such that $({\textsf{Ty}}^{\textsf{i}}, \textsf{Ty}', \textrm{c}')$ forms a model of two-level type theory satisfying (T1) and (T2).

Furthermore, this operation is 2-functorial in $\mathcal{C}$ in the same sense as Corollary 2.14.

Proof. The following is to be understood as happening for every size index i, which we omit. By a small set, we mean an element of the Grothendieck universe $M_j$ .

Let ${{\mathcal{U}}} \in \widehat{\mathcal{C}}$ denote the representing object of $\textsf{Ty}$ , with universal element $\textsf{El} \in \textsf{Ty}({{\mathcal{U}}})$ . Define $\textsf{Ty}'$ as the presheaf represented by $\textsf{Ty}_\mathcal{C} + {{\mathcal{U}}}$ . We have a map $[\textrm{c}, {{\textsf{id}_{{{\mathcal{U}}}}}}] \mathbin{\colon} \textsf{Ty}_\mathcal{C} + {{\mathcal{U}}} \rightarrow {{\mathcal{U}}}$ . Applying Yoneda, this induces the map $r \mathbin{\colon} \textsf{Ty}' \rightarrow \textsf{Ty}$ . The cwf structure of $\textsf{Ty}'$ is inherited from $\textsf{Ty}$ via r. Applying Yoneda to the coprojections $\textsf{inl} \mathbin{\colon} \textsf{Ty}_\mathcal{C} \rightarrow \textsf{Ty}_\mathcal{C} + {{\mathcal{U}}}$ and $\textsf{inr} \mathbin{\colon} {{\mathcal{U}}} \rightarrow \textsf{Ty}_\mathcal{C} + {{\mathcal{U}}}$ , we obtain respective cwf structure morphisms $\textrm{c}' \mathbin{\colon} {\textsf{Ty}}^{\textsf{i}} \rightarrow \textsf{Ty}'$ and $s \mathbin{\colon} \textsf{Ty} \rightarrow \textsf{Ty}'$ . These fit into a commuting diagram as follows:

Unfolding the definition, we find that, given $X \in \widehat{\mathcal{C}}$ , an element of $\textsf{Ty}'(X)$ consists of a partition $X = X_0 \sqcup X_1$ of X into subpresheaves $X_0$ and $X_1$ together with $A_0 \in {\textsf{Ty}}^{\textsf{i}}(X_0)$ , i.e. $A_0 \mathbin{\colon} X_0 \rightarrow \textsf{Ty}_\mathcal{C}$ , and $A_1 \in \textsf{Ty}(X_1)$ , i.e. a small presheaf $A_1$ over $\mathcal{C}/X_1$ .

The interpretation of type formers in $\textsf{Ty}'$ other than ${{\textbf{1}}}/\Sigma/\Pi$ -types is as for $\textsf{Ty}$ and is defined such that it is preserved by r. For the type forming operations, we first transport the given types in $\textsf{Ty}'$ to $\textsf{Ty}$ via r, use the corresponding type forming operation there, and apply s to the result. Since $r \circ s = {{\textsf{id}_{}}}$ , this makes r preserve the type forming operation, meaning the remainder of the operations dealing with terms can be copied from $\textsf{Ty}$ to $\textsf{Ty}'$ .

It remains to interpret ${{\textbf{1}}}/\Sigma/\Pi$ -types in $\textsf{Ty}'$ . Since the terms of these type formers are characterised by universal properties, it will suffice to define their type forming operations such that r preserves ${{\textbf{1}}}/\Sigma/\Pi$ -types up to isomorphism. The remainder of their operations dealing with terms is then uniquely induced. In order to ensure that $\textrm{c}'$ preserves ${{\textbf{1}}}/\Sigma/\Pi$ -types, we only have to check that $\textrm{c}'$ preserves the type forming operations and that the isomorphisms used in the penultimate sentence are the ones of Lemma 2.11 whenever the input types come from

The case of ${{\textbf{1}}}$ -types is trivial: given $X \in \widehat{\mathcal{C}}$ , we imply take ${{\textbf{1}}}' = \textsf{inl}({{{\textbf{1}}}}^{\textsf{i}}) \in \textsf{Ty}'(X)$ using ${{{\textbf{1}}}}^{\textsf{i}} \in {\textsf{Ty}}^{\textsf{i}}$ . Since it has no inputs, there is nothing to show. The type forming operations for $\Sigma$ -types and $\Pi$ -types are of the same form. To save space, we only show the case of $\Pi$ -types.

Recall how the $\Pi$ -type forming operation of ${\textsf{Ty}}^{\textsf{i}}$ was inherited from the one of $\textsf{Ty}_\mathcal{C}$ via the operation (10). The cwf structure of $\textsf{Ty}'$ is induced by $\textsf{El} [\textrm{c}, {{\textsf{id}_{{{\mathcal{U}}}}}}] \in \textsf{Ty}(\textsf{Ty}_\mathcal{C} + {{\mathcal{U}}})$ rather than $\textsf{Tm}_\mathcal{C} \in \textsf{Ty}(\textsf{Ty}_\mathcal{C})$ as for (10). Here, we have to interpret the analogous operation

\[A : \textsf{Ty}_\mathcal{C} + {{\mathcal{U}}}, B : \textsf{El}([\textrm{c}, {{\textsf{id}_{{{\mathcal{U}}}}}}](A)) \rightarrow (\textsf{Ty}_\mathcal{C} + {{\mathcal{U}}}) \vdash \Pi'(A, B) : \textsf{Ty}_\mathcal{C} + {{\mathcal{U}}}\]

together with

\[\textsf{El}([\textrm{c}, {{\textsf{id}_{{{\mathcal{U}}}}}}](\Pi'(A, B))) \simeq \textsf{El}(\Pi([\textrm{c}, {{\textsf{id}_{{{\mathcal{U}}}}}}](A), [\textrm{c}, {{\textsf{id}_{{{\mathcal{U}}}}}}] \circ B))\]

in the same context.

To define the action at level $\Gamma \in \mathcal{C}$ , we take

(11) \begin{align}\notag A &\in \textsf{Ty}_\mathcal{C}(\Gamma) + {{\mathcal{U}}}(\Gamma),\\B &\in \widehat{\mathcal{C}/\Gamma}(\textsf{El}([\textrm{c}, {{\textsf{id}_{{{\mathcal{U}}}(\Gamma)}}}](A)), \textsf{Ty}_\mathcal{C} + {{\mathcal{U}}})\end{align}

(omitting restriction in the target of B) and must define $\Pi'(A, B) \in \textsf{Ty}_\mathcal{C}(\Gamma) + {{\mathcal{U}}}(\Gamma)$ with an isomorphism

(12) \begin{equation} \textsf{El}([\textrm{c}, {{\textsf{id}_{{{\mathcal{U}}}}}}](\Pi'(A, B))) \simeq \textsf{El}(\Pi([\textrm{c}, {{\textsf{id}_{{{\mathcal{U}}}}}}](A), [\textrm{c}, {{\textsf{id}_{{{\mathcal{U}}}}}}] \circ B))\end{equation}

of presheaves over $\mathcal{C}/\Gamma$ . We perform a case distinction on A.

1. (i) Suppose $A = \textsf{inr}(A_1)$ with $A_1 \in {{\mathcal{U}}}(\Gamma)$ . Then, we take

   \[\Pi'(A, B)(\Gamma) = \textsf{inr}(\Pi(A_1, [\textrm{c}, {{\textsf{id}_{{{\mathcal{U}}}}}}] \circ B)),\]
   using the type forming operation of $\textsf{Ty}$ , and let (12) be the identity.

2. (ii) Suppose $A = \textsf{inl}(A_0)$ with $A_0 \in \textsf{Ty}_\mathcal{C}(\Gamma)$ . Then, $\textsf{El}([\textrm{c}, {{\textsf{id}_{{{\mathcal{U}}}(\Gamma)}}}](A) = \textsf{El}(\textrm{c}(A))$ is the presheaf over $\mathcal{C}/\Gamma$ sending $\sigma \mathbin{\colon} \Delta \rightarrow \Gamma$ to $\textsf{Tm}(\Delta, A[\sigma])$ . Since $\mathcal{C}$ has extension, this presheaf is representable (represented by $\Gamma.A$ ). In particular, mapping out of it as in (11) preserves coproducts. We can thus make a further case distinction on B.

   1. (a) If $B = \textsf{inr} \circ B_1$ with $B_1 \in \widehat{\mathcal{C}/\Gamma}(\textsf{El}(\textrm{c}(A)), {{\mathcal{U}}})$ , we take

      \[\Pi'(A, B)(\Gamma) = \textsf{inr}(\Pi(\textrm{c}(A_0), B_1)),\]
      again using the type forming operation of $\textsf{Ty}$ , and let (12) be the identity.

   2. (b) If $B = \textsf{inl} \circ B_0$ with $B_0 \in \widehat{\mathcal{C}/\Gamma}(\textsf{El}(\textrm{c}(A)), \textsf{Ty}_\mathcal{C})$ , we take

      \[\Pi'(A, B)(\Gamma) = \textsf{inl}({\Pi}^{\textsf{i}}(A_0, B_0)),\]
      using the type forming operation of ${\textsf{Ty}}^{\textsf{i}}$ , and let (12) be the isomorphism given by Lemma 2.11.

One checks that this definition is natural in $\Gamma$ . Recalling that $\textrm{c}'$ is given by the action of Yoneda on $\textsf{inl} \mathbin{\colon} \textsf{Ty}_\mathcal{C} \rightarrow \textsf{Ty}_\mathcal{C} + {{\mathcal{U}}}$ , we find that $\textrm{c}'$ preserves $\Pi$ -type formation by construction (case (ii.b)) with the required coherence isomorphism.

This finishes the verification that $\textsf{Ty}'$ forms a cwf hierarchy with the type formers of the outer level of a model of two-level type theory. Note that uniqueness of identity proofs and function extensionality are inherited from $\textsf{Ty}$ (this is immediate for the former; for the latter, use that the outer identity type respects the isomorphism relating $\Pi'$ and $\Pi$ ).

To obtain the universes in $\textsf{Ty}'$ , we must encode the representing object $(\textsf{Ty}_\mathcal{C})_j + ({{\mathcal{U}}})_j$ as $\textsf{El}(r({{\mathcal{U}}}_j'))$ (under the isomorphism $\widehat{\mathcal{C}} \simeq \widehat{\mathcal{C}/1}$ ) for some ${{\mathcal{U}}}_j' \in \textsf{Ty}'(1)$ . We have $V_j \in \textsf{Ty}_{j+1}(1)$ such that $(\textsf{Ty}_\mathcal{C})_j + ({{\mathcal{U}}})_j$ is $\textsf{El}(V_j)$ (under the isomorphism $\widehat{\mathcal{C}} \simeq \widehat{\mathcal{C}/1}$ ). So we simply take ${{\mathcal{U}}}_j' = s(V_j)$ .

2-Functoriality in $\mathcal{C}$ is a straightforward calculation.

Note that the cwf hierarchy morphism s in the above proof preserves almost all type formers: the only one not preserved is the unit type. Note also that the technique of Proposition 2.16 is constructive only for finitary type formers: were we to add product types of infinite arity or dependent sums of “arity $\omega$ ( $\omega^{\textrm{op}}$ -Reedy limits) to homotopy type theory, then to make $\textrm{c}'$ preserve these using the above approach, we would have to perform an infinite number of case distinctions before deciding on the result of the corresponding type forming operation in $\textsf{Ty}'$ on given inputs, which requires classical logic.

In Subsection 2.6, we will use this modified presheaf model to strengthen conservativity of two-level type theory over homotopy type theory to additionally include conservativity of (T1) and (T2).

None of the other properties (A1) and (T3) to (A6) are generally impacted by the model construction of proposition 2.16.

2.6 Conservativity

Two-level type theory is an extension of homotopy type theory, which forms its inner level. As such, it makes sense to ask if two-level type theory is conservative over homotopy type theory.

Here, we take the perspective regarding homotopy type theory and two-level type theory simply as the initial models in their respective categories of models, which are the primary notion. Syntax is treated as notation, that is, merely as a device for working within such models. Expressions of our syntax denoting types and terms are just stand-ins denoting certain derivations. We do not analyse them as raw syntactic objects independently from the associated derivation, although such considerations are of course important for the implementation of proof assistants.

What does conservativity mean under this perspective? We have a forgetful functor ${(-)}^{\textsf{i}}$ from the category of models of two-level type theory to the category of models of homotopy type theory. Letting $0_\textsf{HoTT}$ and $0_\textsf{2LTT}$ denote their respective initial objects, we have a unique morphism $0_\textsf{HoTT} \rightarrow {0_\textsf{2LTT}}^{\textsf{i}}$ . This expresses that any derivation in homotopy type theory can also be performed in two-level type theory. For conservativity, we wish to know reversely that any construction of a type or term, or equality of such, in ${0_\textsf{2LTT}}^{\textsf{i}}$ , with given context (and type, in the case of constructions for terms) coming from $0_\textsf{HoTT}$ , can be lifted to $0_\textsf{HoTT}$ .

We will employ the following definition of conservativity for a cwf morphism $F \mathbin{\colon} \mathcal{C} \rightarrow D$ , which is, in some sense, the weakest possible. It essentially states that F reflects inhabitation of terms. This formalises the idea that we can use the language of $\mathcal{D}$ to prove statements in $\mathcal{C}$ .

Note that is definition is unrelated to the underlying functor F being conservative, i.e. reflecting isomorphisms. Stronger definitions are of course possible, for example requiring that F acts (split) surjectively or bijectively on terms and types, perhaps up to internal notions of equality in $\mathcal{D}$ .

Proof. We apply the construction of Corollary 2.14 to $0_\textsf{HoTT}$ and ${0_\textsf{2LTT}}^{\textsf{i}}$ , obtaining a diagram

commuting up to isomorphism in the 2-category of models of homotopy type theory and weak morphisms. Conservativity of the vertical map now follows immediately from the fact that the Yoneda embedding acts bijectively on terms.

Using proposition 2.16, we may strengthen the above statement to two-level type theory with injective conversion morphisms that strictly preserve $1/\Sigma/\Pi$ -types.

We conjecture a stronger conservativity result: if equality reflection (A5) holds in the outer level, then the actions of the cwf morphism ${\text{!}} \mathbin{\colon} 0_\textsf{HoTT} \rightarrow {(0_\textsf{2LTT})}^{\textsf{i}}$ on types and terms are bijective (and hence the underlying functor is fully faithful). We believe this result can be obtained using the technique of categorical glueing. A concrete argument has been given by Kovács (Reference Kovács2022, Corollary 5.5), seen there as “soundness and stability of staging.

2.7 On the possibility of a fibrant replacement

In homotopical models of two-level type theory, outer types in context $\Gamma$ correspond to arbitrary maps into $\Gamma$ , whereas inner types correspond to fibrations with base $\Gamma$ . From this viewpoint, it is natural to ask whether we could extend our theory with a fibrant replacement operation, allowing us to replace any outer type by its “closest inner approximation. A syntactic presentation of rules for such a fibrant replacement type former might look as follows:

Phrased internally, given an outer type A, we get an inner type RA together with a function $r : A \rightarrow c(RA)$ with the universal property that, for any inner type X, to define a function $RA \rightarrow X$ is to give a function $A \rightarrow c(X)$ . Note the similarity of the above rules to those of the propositional truncation modality; the only difference is, of course, that R makes types fibrant rather than propositional.

A type former along these lines is considered in Boulier and Tabareau (Reference Boulier and Tabareau2017), where the authors construct a model structure on a universe of outer types using fibrant replacement.

Unfortunately, the fibrant replacement operation cannot actually be internalised in the above form while still retaining interesting homotopical models. This is shown by the following theorem.

Proof. For an inner type A with $u, v : A$ , the internalisation of (7) gives us a canonical map

\begin{equation*} i : \left(\textrm{c}(u) =_{\textrm{c}(A)} \textrm{c}(v)\right) \rightarrow \textrm{c}(u \mathrel{{=}^{\textsf{i}}_{[}}A] v).\end{equation*}

We claim the following:

(13)

By inner path induction, we can assume $p \equiv {{{\textsf{refl}}^{\textsf{i}}_{u}}}$ . Using intro-R it remains to show that, for $h : \textrm{c}(u) = \textrm{c}(u)$ , we have

(14) \begin{equation} \textrm{c}(\textrm{c}^{-1}(i(h)) \mathrel{{=}^{\textsf{i}}_{{{{\textsf{refl}}^{\textsf{i}}_{}}}}} u).\end{equation}

Because of UIP, we can replace h by ${{\textsf{refl}_{\textrm{c}(u)}}}$ , and by observing that i maps the trivial outer equality to the trivial inner equality we get (14).

Our goal is to show that A satisfies UIP. Assume now $u : A$ and $p : u \mathrel{{=}^{\textsf{i}}_{u}}$ . It suffices to show $p \mathrel{{=}^{\textsf{i}}_{{{{\textsf{refl}}^{\textsf{i}}_{}}}}}{u}$ . This follows from (13), choosing h to be ${{\textsf{refl}_{\textrm{c}(u)}}}$ .

While homotopical models do have fibrant replacement operations coming from weak factorisation systems, they are usually not stable under base change. This prevents internalisation of this operation in the form of the above rules. That is, we may replace an inner type by an outer type, but this operation is not natural in the context. If one still wishes to expose this operation, one option is to make two-level type theory into a modal type theory extended with a notion of crisp types as in Licata et al. (Reference Licata, Orton, Pitts, Spitters and Kirchner2018). Then, one can state the above replacement operation crisply.

2.8 Notational conventions

The rest of the paper does not concern the meta-properties of 2LTT. Instead, we develop some theory internally to 2LTT. As described above, we use the syntax suggested in Subsection 2.1. For notational convenience, we omit applications of $\textsf{El}$ and pretend that we work with Russell-style universes. As it is fairly standard, we also omit universe indices in the style of typical ambiguity. Similarly, we will keep the conversion operation $\textrm{c}$ between inner and outer types implicit.

Note that we did not assume a built-in universe of propositions in either level (but cf. (A5)). Instead, we define

(15)

(16)

Most of the time, we work with the outer level, which is why we treat that level as the default; note how the inner type formers are annotated with the symbol ${}^{\textsf{i}}$ , while the outer do not carry annotations. This also means that, when we say that a diagram commutes, it commutes up to the outer equality type.

For outer types A and B, we can form the type of isomorphisms, written $A \simeq B$ . Note that, because of UIP, asking for maps in both directions such that both compositions are pointwise equal to the identity is well-behaved. For inner types A and B, the inner type $A \mathrel{{\simeq}^{\textsf{i}}} B$ is the usual type of equivalences.

3.1 Preliminaries

Although somewhat trivial, the importance of finite types for our development justifies that we introduce them explicitly. Recall that, in usual type-theoretic terminology, $\textsf{Fin}_n$ is the finite type with n elements. In our development, we will use this notation exclusively to refer to finite types in the outer level. One explicit definition is as the type of natural numbers smaller than n, where the order on natural numbers is defined as usual.

We will say that a type X is finite if it is isomorphic to $\textsf{Fin}_n$ , for some n, i.e. if we have $\Sigma \left(n: {{\mathbb{N}}}\right).\, X \cong \textsf{Fin}_n$ . The type $\textsf{Fin}_n$ is not to be confused with its inner counterpart ${\textsf{Fin}}^{\textsf{i}}_n$ , which exists for $n : {{{\mathbb{N}}}}^{\textsf{i}}$ . Of course, we have a canonical function $\textsf{Fin}_n \rightarrow {\textsf{Fin}}^{\textsf{i}}_n$ , where the application of the function ${{\mathbb{N}}} \rightarrow {{{\mathbb{N}}}}^{\textsf{i}}$ is kept implicit. In a two-level theory satisfying (A1), this would be an isomorphism, but in general, we do not even assume a function in the other direction.

In the following, will make heavy use of category-theoretic notions. Categories are defined in the usual way, within the outer level of the theory.

Given objects x and y of a category $\mathcal{C}$ , we also write $f \mathbin{\colon} x \rightarrow y$ for a morphism from x to y, that is, an element of the type $\mathcal{C}(x, y)$ . It will always be clear from the context if x and y are types or objects of a category, so that there is no confusion with the function type former. (In the case of a category of types, the two notions agree.)

Readers familiar with the chapter on category theory in the HoTT book (The Univalent Foundations Program, 2013) (and Ahrens et al. Reference Ahrens, Kapulkin and Shulman2015) will note that our definition is exactly the same as that of precategories there. Of course, since our outer theory validates UIP, and therefore every type is a set, we do not need to explicitly add a truncation condition on homsets.

A canonical example of a category is the category of types, whose objects are the types in a given universe ${{\mathcal{U}}}$ , and whose morphisms are functions. By a slight abuse of notation, we will simply write ${{\mathcal{U}}}$ to denote this category. Analogously, if $\mathcal{C}$ is a category, we allow ourselves to denote the type of objects by $\mathcal{C}$ itself.

The usual theory of categories can be reproduced in the context of our categories (as long as we stay constructive). We write $[\mathcal{C}, \mathcal{D}]$ for the functor category of categories $\mathcal{C}$ and $\mathcal{D}$ , with the type of natural transformations from a functor F to a functor G also written $\textbf{Nat}(\mathcal{C}, \mathcal{D})$ . Functors and natural transformations form the objects and morphisms of a (larger) category of categories. We have the usual concepts such as limits and adjunctions and can prove all their usual properties, for example that limits (if they exist) are unique up to isomorphism.

When translating category-theoretical statements originally formulated in the metalanguage of set theory, one is posed with the question of what precise type-theoretic meaning to give to the term “small”.

As most incarnations of type theory, including our outer level, provide the user with an infinite tower of universes, it feels unnecessarily restrictive to constrain a general term like “small” to a predetermined choice of a universe level.

For this reason, we will not make such a choice, and simply continue the tradition of writing “small” for a type that resides in a universe which is one step below a “default” unspecified universe level. This makes it clear that the absolute level that certain constructions happen to end in is not particularly important, rather what we have to pay attention to are the differences in relative size.

Note that the universe ${{{\mathcal{U}}}}^{\textsf{i}}$ of inner types also forms a category, although it is not as well behaved as ${{\mathcal{U}}}$ . For example, it does not have pullbacks (but see part (i) of Lemma 3.10).

3.2 Fibrant types

Note that fibrancy (and similarly trivial fibrancy) is a proof-relevant notion, in that being fibrant is not a proposition (in the sense of having at most one element). A fibrant type A carries with it a choice of an inner type A’ and an isomorphism $f : A \cong A'$ relating its coercion to a type to the original type A (and a trivially fibrant type furthermore carries an element witnessing inner contractibility of A’). This should be kept in mind in our use of language when we use being fibrant as an adjective. For example, when we say that A is fibrant exactly if B is fibrant, what we mean is functions back and forth between the types witnessing fibrancy of A and B.

Generally speaking, our use of informal language in the outer level follows the mantra of “propositions as types”. Thus, similar conventions as established in the previous paragraph apply to notions such as fibrations and cofibrations defined below (and their Reedy variants considered later).

We write ${{\mathcal{U}}}_{\textsf{fib}}$ for the type of fibrant types in ${{\mathcal{U}}}$ . Note that it is itself not generally fibrant (although it is in some of the intended models such as simplicial sets). We let ${{\mathcal{U}}}_{\textsf{fib}}$ inherit the category structure of ${{\mathcal{U}}}$ . Note that the functor ${{\mathcal{U}}}_{\textsf{fib}} \rightarrow {{\mathcal{U}}}$ is the replacement of the coercion functor ${{{\mathcal{U}}}}^{\textsf{i}} \rightarrow {{\mathcal{U}}}$ by an isofibration. In particular, fibrant types are closed under isomorphism. We allow ourselves to implicitly coerce from ${{\mathcal{U}}}_{\textsf{fib}}$ to ${{\mathcal{U}}}$ .

We do the case of dependent products in detail. Note that we can internalise the inner dependent product as an operation ${\Pi}^{\textsf{i}} : (\Sigma \left(A : {{{\mathcal{U}}}}^{\textsf{i}}\right).\, (A \rightarrow {{{\mathcal{U}}}}^{\textsf{i}})) \rightarrow {{{\mathcal{U}}}}^{\textsf{i}}$ and that given $A : {{{\mathcal{U}}}}^{\textsf{i}}$ and $B : A \rightarrow {{{\mathcal{U}}}}^{\textsf{i}}$ , we have a comparison isomorphism ${\Pi}^{\textsf{i}}(A, B) \cong \Pi_{a:A}\mkern1mu B(a)$ . This shows that the (outer) dependent product of $A : {{{\mathcal{U}}}}^{\textsf{i}}$ and $B : A \rightarrow {{{\mathcal{U}}}}^{\textsf{i}}$ is fibrant. Isomorphic families have isomorphic dependent product, generalising the statement to $B : A \rightarrow {{\mathcal{U}}}_{\textsf{fib}}$ . Finally, reindexing a family along an isomorphism gives isomorphic dependent product, generalising the statement to $A : {{\mathcal{U}}}_{\textsf{fib}}$ .

Note that the notion of f being an equivalence in the above definition formally depends on the witnesses of fibrancy of A and B. Different witnesses yield non-isomorphic types of f being an equivalence. However, they will still be logically equivalent (in the sense of maps back and forth) and are in fact propositionally fibrant (meaning that their underlying inner type is a proposition in the sense of homotopy type theory). As per our convention, we can thus say that the notion of equivalence is invariant under isomorphism.

Properties of equivalences are directly lifted from the inner level. For example, equivalences satisfy 2-out-of-6.

3.3 Fibrations

Recall that the fibre $p^{-1}(x)$ of a function $p : Y \rightarrow X$ over $x : X$ is given by the type $\Sigma \left(y:Y\right).\, p(e) = b$ . This is not to be confused with the notion of homotopy fibre, which is only available for inner types (using the inner identity type). More generally, we say that a type A is the fibre of p over x if A arises as a pullback of p along $1 \rightarrow X$ , in which case it is isomorphic to $p^{-1}(x)$ .

In the running text and diagrams, a fibration $Y \rightarrow X$ is denoted $Y \twoheadrightarrow X$ .

Since isomorphic maps have isomorphic fibres and the notion of (trivial) fibrancy is invariant under isomorphism, the notion of (trivial) fibration is invariant under isomorphism as well. From this, the following lemma is an immediate consequence of the definitions.

and if X is fibrant with underlying inner type $X' : {{{\mathcal{U}}}}^{\textsf{i}}$ :

1. (iv) p is isomorphic to the map ${\Sigma}^{\textsf{i}}_{X'} Y' \rightarrow X'$ corresponding to the inner dependent projection ${\Sigma}^{\textsf{i}}_{X'} Y' \mathbin{{\rightarrow}^{\textsf{i}}} X'$ for some $Y' : X' \rightarrow {{{\mathcal{U}}}}^{\textsf{i}}$ .

We have analogous equivalences for trivial fibrations with ${{{\mathcal{U}}}}^{\textsf{i}}$ replaced by the type of inner contractible types and ${{\mathcal{U}}}_{\textsf{fib}}$ replaced by the type of trivially fibrant types.

Fibrations and trivial fibrations enjoy a number of closure properties. We start with the following easy collection.

For part (ii), the nullary and binary case reduce to parts (i) and (ii) of Lemma 3.5, respectively. The general case follows by induction.

Part (iii) is a consequence of (i) and (ii).

Proof. By Lemma 3.9, we can assume that the given trivial fibration is of the form $\Sigma \left(b : B\right).\, X(b) \rightarrow B$ for a type B and a family $X : B \rightarrow {{{\mathcal{U}}}}^{\textsf{i}}$ of contractible fibrant types over B. We obtain a section $\Pi_{b : B}\mkern1mu X(b)$ by extracting the centre of contraction from the contractibility proof of X(b).

3.4 Cofibrations

Cofibrations and cofibrant types are further technical concepts which help us to study the actual objects of interest, i.e. fibrant types. We will see their usefulness later in this article, but let us in addition try to give some motivation here. If B is a fibrant type, then so are $B \times B$ and $B \times B \times B$ . More generally, if we work in HoTT and fix any natural number n in the meta-theory, we can consider the n-fold product of B. In our setting, this corresponds to the function type $\textsf{Fin}_n \rightarrow B$ . It is important to note that, while $(\textsf{Fin}_2 \rightarrow B)$ is isomorphic to $B \times B$ , this and analogous isomorphisms do in general not hold if we use the inner version ${\textsf{Fin}}^{\textsf{i}}_2$ instead; we will only get the weaker notion of an inner equivalence. While $\textsf{Fin}_n \rightarrow B$ is fibrant, this is not directly given by the rules of 2LTT and instead requires a proof (see Lemma 3.25). This, we hope, makes it plausible that it is useful to have a notion of cofibrant types, which we want to be those that exponentiation with preserves fibrancy, and it is not too far-fetched that we also want an analogous notion for functions. In fact, one might expect that any setting which allows to reason about HoTT externally in such a way benefits from a notion of cofibration. For example, it is worth comparing the characterisation in Remark 3.14(i) with the extension types by Riehl and Shulman (Reference Riehl and Shulman2017).

To define and reason about cofibrations (as well as Reedy cofibrations later on), we make use of the theory of Leibniz constructions established in Riehl and Verity (Reference Riehl and Verity2014). Given a bifunctor $F : \mathcal{C} \times \mathcal{D} \rightarrow \mathcal{E}$ , the Leibniz action $\widehat{F}(f, g)$ of F on maps $f \mathbin{\colon} A \rightarrow B$ in $\mathcal{C}$ and $g \mathbin{\colon} C \rightarrow D$ in $\mathcal{D}$ is the induced map from the pushout corner in the square

i.e. the map

assuming that this pushout exists. If $\mathcal{E}$ has all pushouts, this gives rise to a bifunctor $\widehat{F} : \mathcal{C}^\rightarrow \times \mathcal{D}^\rightarrow \rightarrow \mathcal{E}^\rightarrow$ , the Leibniz construction of F.

In a category $\mathcal{C}$ with finite products, the Leibniz action of the product functor $(-) \times (-) : \mathcal{C} \times \mathcal{C} \rightarrow \mathcal{C}$ in a category $\mathcal{C}$ is called the pushout product. For $\mathcal{C}$ Cartesian closed, the Leibniz action of the exponential functor $\exp^{\textrm{op}} : \mathcal{C} \times \mathcal{C}^{\textrm{op}} \rightarrow \mathcal{C}^{\textrm{op}}$ is called the pullback exponential. Note the dualised functor signature we have given $\exp$ here (as opposed to $\exp : \mathcal{C}^{\textrm{op}} \times \mathcal{C} \rightarrow \mathcal{C}$ ). This causes the pushout (in $\mathcal{C}^{\textrm{op}}$ ) of the Leibniz construction to become a pullback in $\mathcal{C}$ , explaining the naming.

The category ${{\mathcal{U}}}$ of types is Cartesian closed and has pullbacks; thus, we have the pullback exponential bifunctor $\widehat{\exp} : ({{\mathcal{U}}}^{\textrm{op}})^\rightarrow \times {{\mathcal{U}}}^\rightarrow \rightarrow {{\mathcal{U}}}^\rightarrow$ , sending functions $f : A \rightarrow B$ and $p : Y \rightarrow X$ to the function

A type B is (trivially) cofibrant if the function $0 \rightarrow B$ is a (trivial) cofibration.

We thank Mike Shulman for pointing out that we were missing the condition on trivial fibrations for cofibration in an earlier version of this definition.

In the simplicial set model, our notion of (trivial) cofibration (interpreted in the empty context) coincides with the (trivial) cofibrations of the Kan model structure. This can be seen as follows. The Kan model structure is Cartesian closed; hence, a (trivial) cofibration of the model structure is a (trivial) cofibration in our sense. Reversely, let $f \mathbin{\colon} A \rightarrow B$ be a cofibration in our sense. In particular, Leibniz exponential with f preserves trivial fibrations. Then, f lifts against trivial fibrations by Lemma 3.11, i.e. is a cofibration of the model structure. A similar argument applies to trivial cofibrations, and our reasoning is not specific to simplicial sets but applies to any cartesian closed model structure.

One can ask for a local version of this correspondence. Given a simplicial set $\Gamma$ , the above argument in the slice over $\Gamma$ shows that the (trivial) cofibrations of the model structure over $\Gamma$ include all of our (trivial) cofibrations in context $\Gamma$ . However, the reverse inclusions fails as the slices of the Kan model structure are not Cartesian closed. For example, taking $\Gamma = \Delta^1$ , the map $\lbrace{0}\rbrace \rightarrow \Delta^1$ (sitting over $\Delta^1$ via the identity) is an example of a trivial cofibration of the model structure that is not even a cofibration in context $\Gamma$ in our sense. For if it were, pullback exponentials over $\Delta^1$ with $\lbrace{0}\rbrace \rightarrow \Delta^1$ would preserve fibrations, which, by the adjunction between product and exponential, would imply that pushout product over $\Delta^1$ with $\lbrace{0}\rbrace \rightarrow \Delta^1$ preserves trivial cofibrations. However, the pushout product over $\Delta^1$ of $\lbrace{0}\rbrace \rightarrow \Delta^1$ and $\lbrace{1}\rbrace \rightarrow \Delta^1$ is simply their union $\partial \Delta^1 \rightarrow \Delta^1$ , which is not a trivial cofibration.

Within fibrant types, trivial cofibrations can be characterised as cofibrations that are equivalences.

If f is a trivial cofibration, then, for all fibrant types X, the restriction map $(B \rightarrow X) \rightarrow (A \rightarrow X)$ is an equivalence. A Yoneda-like argument implies that f is an equivalence in this case. In detail, the characterisation (ii) of Remark 3.14 implies that the type of dotted diagonal fillers is trivially fibrant in each of the following two diagrams:

As indicated, we call g the unique morphism $B \rightarrow A$ that makes the left triangle commute. In the right triangle, observe that $f \circ g$ and $\textsf{id}$ both make the triangle commute, and the desired result follows by uniqueness.

Conversely, let $p : Y \rightarrow X$ be a fibration. Then, the corresponding pullback-exponential fibration

\[(B \rightarrow Y) \rightarrow (B \rightarrow X) \times_{(A \rightarrow X)} (A \rightarrow Y)\]

is an equivalence by preservation of equivalences under exponentiation with a fixed base and 2-out-of-3, hence a trivial fibration by Lemma 3.12. Thus, f is a trivial cofibration.

The following key lemma helps us characterise cofibrations.

Before giving its proof, let us recall the following characterisation of dependent functions in terms of non-dependent functions into a type of pairs where the first component is fixed.

Lemma 3.19. For a function $f : A \rightarrow B$ and a family $X : B \rightarrow {{\mathcal{U}}}$ , the following diagram is a pullback:

Proof of Lemma 3.18. Let $p : Y \rightarrow X$ be a fibration. It is isomorphic to $\Sigma_X Y' \rightarrow X$ for some family $Y' : X \rightarrow {{\mathcal{U}}}_{\textsf{fib}}$ of fibrant types. Given $v : B \rightarrow X$ , we have the following diagram:

The right bottom square is a pullback by construction. The composite bottom square and the composite left square are pullbacks by Lemma 3.19. By pullback pasting, the top left square is a pullback.

Note that a map over a type Z is a (trivial) fibration exactly if all its pullbacks along maps $1 \rightarrow Z$ are (trivial) fibrations. It follows that $\widehat{\exp}(f, p)$ is a (trivial) fibration exactly if $\Pi_B (Y' \circ v) \rightarrow \Pi_A (Y' \circ v \circ f)$ is a (trivial) fibration for all v. This shows the desired equivalences: going forward, we put $X = B$ and $v = {{\textsf{id}_{B}}}$ ; going backward, we use the given condition for the family $Y' \circ v$ for all v.

By setting $A = 0$ in Lemma 3.18, we obtain the following important special case.

In the following, we make use of standard properties of the Leibniz calculus (most of which are established at a general level in Riehl and Verity Reference Riehl and Verity2014). They allow us to infer closure properties of (trivial) cofibrations from corresponding closure properties of (trivial) fibrations established in Lemma 3.10.

Recall that ${{\mathcal{U}}}$ does not possess pushouts in general. Part (i) does not establish the existence of pushouts, but merely asserts that any pushout of a (trivial) cofibration is also one.

Proof of Lemma 3.21. For part (i), recall from Riehl and Verity (Reference Riehl and Verity2014) that the functorial action of the pullback exponential in its first argument sends morphisms of arrows that are pushouts to morphisms of arrows that are pullbacks. Thus, the claim follows from part (i) of Lemma 3.10.

In detail, consider a pushout

Assuming that f is a cofibration, we wish to show that g is a cofibration (the case of trivial cofibrations is analogous). Let $Y \twoheadrightarrow X$ be a (trivial) fibration. From the universal property of the pushout and pullback pasting, we get that the square

is a pullback. Since $f : A \rightarrow B$ is a cofibration, the right vertical map is a (trivial) fibration, hence so is the left vertical map by part (i) of Lemma 3.10. This makes g a cofibration. An alternative argument uses Lemma 3.18 and the dependent version of the universal property of pushouts.

For part (ii), recall from Riehl and Verity (Reference Riehl and Verity2014) that the pullback exponential of a map p with a finite composition is a finite composition of pullbacks of pullback exponentials of p with the individual factors. Thus, the claim follows from parts (i) and (ii) of Lemma 3.10.

For an alternative proof, we can make use of the characterisation of (trivial) cofibrations given by Lemma 3.18. Let us only deal with the case of a binary composition

of cofibrations. Given a family $X : C \rightarrow {{\mathcal{U}}}_{\textsf{fib}}$ of (trivially) fibrant types, we have to show that $\Pi_{C}\mkern1mu X \rightarrow \Pi_{A}\mkern1mu (X \circ g \circ f)$ is a (trivial) fibration. This writes as the composite

whose factors are (trivial) fibrations by assumption. The statements then follows from closure of fibrations under composition, i.e. part (ii) of Lemma 3.10.

For part (iii), recall that the exponential bifunctor sends colimits in its exponent to limits. By Riehl and Verity (Reference Riehl and Verity2014), this property transfers to the pullback exponential bifunctor. In particular, for a fixed function p, the operation $\widehat{\exp}(-, p)$ sends coproducts (in ${{\mathcal{U}}}^\rightarrow$ ) to products. The claim then reduces to part (iii) of Lemma 3.10. Alternatively, it is a consequence of (i) and (ii) in the same fashion as for Lemma 3.10.

Alternatively, we could instantiate part (iii) of Lemma 3.21 to the cofibrations ${{\textsf{id}_{A}}}$ (using the nullary case of part (ii) of Lemma 3.21) and $0 \rightarrow B$ .

Note that the map $0 \rightarrow 1$ is the unit for the pushout product. Thus, the pullback exponential with $0 \rightarrow 1$ is equivalent to the identity functor. Thus, 1 is the simplest example a cofibrant type. This can be seen as the nullary version of the following statement.

Proof. Recall that binary product and exponential form a two-variable adjunction. As explained in Riehl and Verity (Reference Riehl and Verity2014), this lifts to Leibniz constructions. In particular, given a function p, we have isomorphisms

\[ \widehat{\exp}(f \widehat{\times} g, p)\cong \widehat{\exp}(g, \widehat{\exp}(f, p))\cong \widehat{\exp}(f, \widehat{\exp}(g, p)).\]

With this, the claim reduces to the definition of (trivial) cofibrations.

We are now able to characterise a large class of cofibrant types.

Part (ii) is an instance of part (iii) of Lemma 3.21.

Part (iii) is a corollary of (ii) and cofibrancy of 1.

For part (iv), we work with the characterisation of cofibrancy given by Corollary 3.20. Let $X : (\Sigma_A B) \rightarrow {{\mathcal{U}}}_{\textsf{fib}}$ be a (trivially) fibrant family. We have to show that $\Pi_{\Sigma A B}\mkern1mu X$ is (trivially) fibrant. This type is strictly isomorphic to $\Pi_{a:A}\mkern1mu \Pi_{b:B(a)}\mkern1mu X(a,b)$ and (trivially) fibrant by two applications of Corollary 3.20.

For part (v), the nullary case is given by cofibrancy of 1. With this, the general situation reduces to the case of binary products. This is the non-dependent instance of (iv). Alternatively, it is the instance of Lemma 3.23 for maps $0 \rightarrow A$ and $0 \rightarrow B$ (whose pushout product is $0 \rightarrow A \times B$ ).

We note that part (iv) of Lemma 3.25 has a relative generalisation: given cofibrant A and a family $f_a : C_a \rightarrow D_a$ of cofibrations indexed over $a : A$ , the functorial action $\Sigma_A C \rightarrow \Sigma_A D$ of $\Sigma_A$ on f is a cofibration. This is proved using Lemma 3.19 instead of Lemma 3.18. In principle, one could generalise further to a ‘Leibniz dependent sum’ of a cofibration $A \rightarrow B$ with a family of cofibrations indexed over B, but we have no need for that here.

4.1 Motivation

The connection between dependency structures of types and type families and what is known as Reedy fibrancy (Reedy, Reference Reedy1974) is well-known in the type theory community, although people have used different names for this concept; for example, Makkai’s FOLDS (Makkai, Reference Makkai1995) builds on the same insights. Let us explain the idea with the help of a very concrete example. The category $\Delta_{} $ + $ ^{< 3}$ is the category with three objects [0], [1], [2] (‘vertices’, ‘edges’, ‘triangles’), and morphisms generated by $s, t \mathbin{\colon} [0] \rightarrow [1]$ (‘source’, ‘target’) and $u, v, w \mathbin{\colon} [1] \rightarrow [2]$ , subject to the following three equations:

The type of functors

+

is defined in the usual way and is isomorphic to the type of 9-tuples $(X_0,X_1,X_2,f_s,f_t,f_u,f_v,f_w,e_0,e_1,e_2)$ where:

\begin{align*} & X_0 : {{\mathcal{U}}} &\qquad & f_s \mathbin{\colon} X_1 \rightarrow X_0 &\qquad & e_0 : f_s \circ f_u = f_s \circ f_v \\ & X_1 : {{\mathcal{U}}} && f_t \mathbin{\colon} X_1 \rightarrow X_0 && e_1 : f_t \circ f_u = f_s \circ f_w \\ & X_2 : {{\mathcal{U}}} && f_u \mathbin{\colon} X_2 \rightarrow X_1 && e_2 : f_t \circ f_v = f_t \circ f_w\\ &&& f_v \mathbin{\colon} X_2 \rightarrow X_1 \\ &&& f_w \mathbin{\colon} X_2 \rightarrow X_1\end{align*}

While this type of 9-tuples is unfortunately not fibrant, we can identify a class of diagrams – the Reedy fibrant ones (Definition 4.6) – whose type will turn out to be fibrant, and such that every functor is equivalent a Reedy fibrant one for a suitably weak notion of equivalence.

We will illustrate the idea using + . We will regard this category as a presentation of a dependency structure of types and type families. That is, instead of asking for source and target map from the type of edges to the type of vertices, we let the type of edges be indexed twice over the type of vertices, and similarly for triangles over edges. This leads to a type of triples $(A_0,A_1,A_2)$ with the following components:

\begin{align*} & A_0 : {{\mathcal{U}}} \\ & A_1 : A_0 \rightarrow A_0 \rightarrow {{\mathcal{U}}} \\ & A_2 : \Pi(a,b,c : A_0). A_1\, a \, b \rightarrow A_1 \, b \, c \rightarrow A_1 \, a \, c \rightarrow {{\mathcal{U}}}\end{align*}

The type of triples $(A_0, A_1, A_2)$ encodes the so-called Reedy fibrant functors from + to ${{\mathcal{U}}}$ and can be formulated in homotopy type theory without the notion of strict equality; or in other words, it can be formulated in our inner theory without using equality from the outer theory.

Every triple $(A_0, A_1, A_2)$ determines a functor, but, unfortunately, it is not the case that the latter type of triples is isomorphic (as a type) to the former type of tuples that used strict equality. Instead, we will show later that for every functor there exists a Reedy fibrant one that is equivalent to it in a weaker sense (Corollary 4.27) – its Reedy fibrant replacement.

Before this, we introduce the basic required categorical infrastructure within the language of 2LTT. This is a first demonstration of results which can be expressed in full in 2LTT although they would require meta-theoretic reasoning in more traditional approaches. We define the notion of Reedy fibration and show that Reedy fibrant diagrams $\mathcal{C} \rightarrow {{\mathcal{U}}}$ have limits in ${{\mathcal{U}}}$ for a finite inverse category $\mathcal{C}$ . This is an internalised version of Shulman’s results which can be found in Reference ShulmanShulman (2015b ). In the second half of this section, we describe how to construct Reedy fibrant replacements, discuss classifiers for Reedy fibrations (a special case of which would be the type of semisimplicial types restricted to level n), and finally, we develop the theory of exponentials of diagrams.

4.2 Inverse categories

In the following, when considering categories of diagrams, we will mostly focus on diagrams over inverse categories. In contrast with the setup leading, for instance, to the Reedy model structure on simplicial presheaves over a Reedy category, in our setting it is necessary to impose the further restriction on the index category to be ‘one way’. We can either express this in terms of direct categories and contravariant functors, or inverse categories and covariant functors. We have arbitrarily picked the second representation. For readers familiar with Reedy categories, inverse categories are simply the special case of those obtained by requiring that there be no non-trivial positive arrows. For the sake of illustrating how to encode the details of the definition in two-level type theory, however, we choose to give an explicit definition.

Consider the category $\omega$ . Its objects are the natural numbers ${{\mathbb{N}}}$ and its morphisms are given by

with ${\leq} : {{\mathbb{N}}} \rightarrow {{\mathbb{N}}} \rightarrow \textsf{Prop}$ defined in the usual way. This category is in fact a poset. In general, Reedy categories can be defined in terms of arbitrary ordinals, but $\omega$ is enough for our purposes. This lets us evade the question of how to encode more general ordinals in the theory.

Given category $\mathcal{C}$ and a functor $F \mathbin{\colon} \mathcal{C} \rightarrow {{\mathcal{U}}}$ , the category of elements F, denoted $F / \mathcal{C}$ in analogy with the notation for coslices, is defined as usual via the Grothendieck construction. In particular, objects are pairs (a, x) where $a : \vert \mathcal{C} \vert$ and $x : F(a)$ and morphisms from (a, x) to (b, y) are maps $f : a \rightarrow b$ such that $Ff(x) = y$ . We have a forgetful functor $F/\mathcal{C} \rightarrow \mathcal{C}$ that is discrete Grothendieck opfibration. This is a cosieve exactly if F is valued in propositions.

Let $\mathcal{C}$ now be an inverse category. Then, the forgetful functor $F/\mathcal{C} \rightarrow \mathcal{C}$ induces a rank functor also on $F/\mathcal{C}$ . This makes $F/\mathcal{C}$ into an inverse category.

Given a category $\mathcal{C}$ , recall that the coslice over an object $x : \mathcal{C}$ has as objects pairs (y, f) of $y : \mathcal{C}$ and a map $f \mathbin{\colon} x \rightarrow y$ . Morphisms between (y, f) and (y’, f’) are given maps $h \mathbin{\colon} y \rightarrow y'$ with $h \circ f = f'$ in $\mathcal{C}$ . The evident forgetful functor is a discrete Grothendieck opfibration.

The formulation of Reedy fibrancy for diagrams over inverse categories makes use of the notion of matching object. The following definition can be used (see Definition 4.4) to give a formulation of matching objects in terms of limits.

By definition, we have a fully faithful forgetful functor . Composing it with the forgetful functor to $\mathcal{C}$ , we obtain , sending an object (y, f, p) to y.

Definition 4.2 may seem slightly unnatural from a category theory point of view. There is, however, a different perspective that can perhaps help to shed some light on the above definition, motivated by thinking of inverse categories as generalisations of +.

For a given inverse $\mathcal{C}$ with an object $x : \mathcal{C}$ , we have the representable diagram $\mathcal{C}[x]$ defined by (with evident functorial action). Note that the coslice is the category of elements of $\mathcal{C}[x]$ . Now, the representable diagram $\mathcal{C}[x]$ has a maximal non-trivial subfunctor consisting of all the elements of $\mathcal{C}[x]$ except the identity arrow ${{\textsf{id}_{x}}} \mathbin{\colon} x \rightarrow x$ . We detail its construction below.

Recall that subfunctors of representable functors correspond to cosieves, i.e. families of propositions:

such that, for maps $f \mathbin{\colon} x \rightarrow y$ and $g \mathbin{\colon} y \rightarrow z$ , we have

(17) \begin{equation} \varphi_y(f) \rightarrow \varphi_z(g \circ f).\end{equation}

The functor $\Phi \mathbin{\colon} \mathcal{C} \rightarrow {{\mathcal{U}}}$ corresponding to such a cosieve $\varphi$ is then given by

on objects, and rule (17) ensures that the functor can act on morphisms by function composition, thereby giving a subfunctor of $\mathcal{C}[x]$ .

Now, if $\delta$ is defined by

the condition on $\mathcal{C}$ being inverse guarantees that $\delta$ is a well-defined cosieve. The corresponding subfunctor of $\mathcal{C}[x]$ is denoted by $\partial C[x]$ and referred to as the abstract boundary of x. In the following, we will denote by $i^x \mathbin{\colon} \partial \mathcal{C}[x] \rightarrow \mathcal{C}[x]$ the obvious inclusion map.

The following result is an immediate consequence of the definitions.

4.3 Reedy fibrations

Part (i) of Lemma 3.10 makes it possible to construct fibrant limits of certain “well-behaved” functors from inverse categories. We follow Reference ShulmanShulman (2015b ), but our setup allows a slightly more general development. We will give a short analysis after the proof of Theorem 4.8.

In the following, we always assume that $\mathcal{C}$ is an inverse category.

Using the universal property of the limit defining the matching object, we obtain a map $X_z \rightarrow M_z^X$ . Abstracting over X, this gives a natural transformation $(-)_z \rightarrow M_z$ between functors from $[\mathcal{C}, {{\mathcal{U}}}]$ to ${{\mathcal{U}}}$ .

Alternatively, we can formulate matching objects in terms of abstract boundaries:

Definition 4.6 (Reedy (trivial) fibration; see Reference ShulmanShulman 2015b , Definition 11.3). Let $X, Y \mathbin{\colon} \mathcal{C} \rightarrow {{\mathcal{U}}}$ be two diagrams. Further, let $p \mathbin{\colon} Y \rightarrow X$ be a natural transformation. We say that p is a Reedy (trivial) fibration if, for all $z : \mathcal{C}$ , the canonical map

\begin{equation*} Y_z \rightarrow M_z^Y \times_{M_z^X} X_z, \end{equation*}

induced by the universal property of the pullback, is a (trivial) fibration.

A diagram X is said to be Reedy (trivially) fibrant if the canonical map $X \rightarrow 1$ is a Reedy (trivial) fibration, where here 1 denotes the diagram that is constantly the unit type.

In terms of the natural transformation $(-)_z \rightarrow M_z$ , we can express that p is a Reedy fibration by saying that the pullback application of $(-)_z \rightarrow M_z$ to p is a fibration for all $z : \mathcal{C}$ . Here, we have applied the Leibniz calculus to the bifunctor $[[\mathcal{C}, {{\mathcal{U}}}], {{\mathcal{U}}}] \times [\mathcal{C}, {{\mathcal{U}}}] \rightarrow {{\mathcal{U}}}$ .

We can use abstract boundaries to improve on this. The pullback hom $\widehat{\textbf{Nat}}$ in the category of diagrams on $\mathcal{C}$ is the Leibniz construction of the natural transformation bifunctor $\textbf{Nat}$ . Concretely, given natural transformations $f \mathbin{\colon} A \rightarrow B$ and $p \mathbin{\colon} Y \rightarrow X$ between diagram on $\mathcal{C}$ , their pullback hom is the induced map

With this, we can give an alternative characterisation of Definition 4.6 that is occasionally useful.

Using Definition 4.6, we can make precise the claim that we can construct fibrant limits of certain well-behaved diagrams.

Otherwise, we have $\vert \mathcal{C} \vert \cong \textsf{Fin}_{n+1}$ . Let us consider the rank functor

\[\varphi \mathbin{\colon} \mathcal{C}^{\textrm{op}} \rightarrow \omega.\]

Choose an object $z : \mathcal{C}$ such that $\varphi(z)$ is maximal; this is possible (constructively) due to the finiteness of $\vert \mathcal{C} \vert$ . Let us call $\mathcal{C}'$ the category that we get if we remove z from $\mathcal{C}$ ; that is, we set . Clearly, $\mathcal{C}'$ is still inverse, and we have $\vert \mathcal{C}' \vert \cong \textsf{Fin}_n$ .

Denote by 1 the terminal diagram on $\mathcal{C}$ , and by 1’ the left Kan extension of the terminal diagram on $\mathcal{C}'$ to $\mathcal{C}$ . So 1’ has value 1 on all objects except z, where it has value 0. Similarly, let X’ be the restriction of X on $\mathcal{C}'$ .

The following square of diagrams on $\mathcal{C}$

is a pushout, as one can easily check levelwise, using the fact that equality on objects in $\mathcal{C}$ is decidable, since $|\mathcal{C}|$ is finite.

By applying the bifunctor $\textbf{Nat}$ with X on the right, we get that the square

is a pullback. The right vertical map is a fibration by Reedy fibrancy of $X;$ hence, the left vertical map is a fibration by part (i) of Lemma 3.10. Now $\mathop{\textsf{lim}} X'$ is fibrant by induction hypothesis; hence, $\mathop{\textsf{lim}} X$ is fibrant.

In Shulman’s work (Reference ShulmanShulman, 2015b ), the notion of an outer type does not exist, and every type that occurs is inner. This means that every diagram is valued in inner types, and consequently, matching objects do not necessarily exist, so the definition of a Reedy fibration has to include the condition that all the matching objects involved are available.

If we wanted to precisely reproduce Shulman’s definition of a Reedy fibration, we would have to modify Definition 4.6: first, that all occurring diagrams are valued in fibrant types, and second, that all occurring matching objects, obtained by coercing to outer types then taking a limit, happen to be fibrant.

In our setting, it is more natural to work with outer types from the beginning. We recover Shulman’s notion in the special case where the outer types that occur are coercions of inner types. Although diagrams of fibrant types ( $\mathcal{C} \rightarrow {{{\mathcal{U}}}}^{\textsf{i}}$ ) are what we are ultimately interested in, we can at no cost enlarge the class of diagrams that we talk about to those that are built out of outer types, possibly not even isomorphic to inner ones. The ability to make this choice is an important feature of two-level type theory as a meta-theoretic reasoning framework, and it can help to obtain some slightly more general results compared to a traditional approach.

Similarly to the notation $\mathcal{C}^{<n}$ (see Definition 4.1), we will denote by $X|n$ the restriction of a diagram $X \mathbin{\colon} \mathcal{C} \rightarrow {{\mathcal{U}}}$ to $\mathcal{C}^{<n}$ .

The following lemma generalises Lemma 3.10 to Reedy fibrations.

For part (i), we first give an abstract argument. Recall from Riehl and Verity (Reference Riehl and Verity2014) that the functorial action of the pullback hom in its second argument preserves morphisms between arrows that are pullbacks. It follows that $\widehat{\textbf{Nat}}(i^z, p^* f)$ is a pullback of $\widehat{\textbf{Nat}}(i^z, f)$ for any $z : \mathcal{C}$ . This reduces the claim to part (i) to Lemma 3.10.

For the benefit of the reader, we also include a more direct proof, which is obtained by unfolding the abstract argument. Suppose we have a pullback square:

where p is a Reedy fibration. We want to show that q is a Reedy fibration. Now fix an object $n : \vert \mathcal{C} \vert$ , and consider the cube:

The front and back faces are pullbacks by construction, and the right face is a pullback because it is the limit of a pullback square. By a pullback pasting argument, the square determined by the front left and the back right vertical arrow is a pullback. By a second pullback pasting argument, the left face is a pullback.

Now consider the diagram:

We have proved that the lower square is a pullback, and the outermost square is a pullback because limits in categories of diagrams are pointwise. It follows that the upper square is a pullback for all $n : \mathcal{C}$ , which shows that the map $Y \rightarrow A$ is a Reedy fibration.

For part (ii), recall from Riehl and Verity (Reference Riehl and Verity2014) that the pullback hom with a fixed map $i^z \mathbin{\colon} \partial\mathcal{C}[Z] \rightarrow \mathcal{C}[Z]$ of a finite composition is a finite composition of pullbacks of pullback homs of $i^z$ with the individual factors. Thus, the claim reduces to parts parts (i) and (ii) of Lemma 3.10.

Reedy fibrations admit “change of base” along discrete Grothendieck fibrations.

Alternatively, one checks for $z : \mathcal{C}$ that left Kan extension $H_{\text{!}}$ along H sends the map $i^z \mathbin{\colon} \partial\mathcal{C}[z] \rightarrow \mathcal{C}[z]$ in $[\mathcal{C}, {{\mathcal{U}}}]$ to the map $i^{Hz} \mathbin{\colon} \partial\mathcal{C}[Hz] \rightarrow \mathcal{C}[hZ]$ (this always holds for the codomain, independently of requiring that H is a discrete Grothendieck fibration). Indeed, this follows from the following special case. The map $i^z$ is itself the left Kan extension of the maximal non-trivial subobject of the terminal object in diagrams over

, and similarly for the abstract boundary $i^{Hz}$ and $\mathcal{D}$ . The claim then follows from commutativity of the diagram

of categories.

4.4 Reedy fibrant factorisations

The goal of the current section is to show that any functor X from an admissible inverse category $\mathcal{C}$ to ${{\mathcal{U}}}_{\textsf{fib}}$ has a Reedy fibrant replacement; that is, we can construct a Reedy fibrant diagram which is equivalent to X in a suitable sense. More generally, given any map of pointwise fibrant diagrams, we can always factor it into a (pointwise) equivalence followed by a fibration.

We emphasise that we are talking about diagrams that are valued in fibrant types. An obvious reason why this is necessary is that the only notion of equivalence for general diagrams that we could use would be (strict) isomorphism, which clearly would be too strong. But even if we came up with a weak notion of equivalence of general diagrams, we could not expect it to be possible to start with any diagram $\mathcal{C} \rightarrow {{\mathcal{U}}}$ and derive a Reedy fibrant one from it which is in some sense equivalent. Already in the special case that $\mathcal{C}$ is the discrete category with exactly one object, this would correspond to finding a fibrant replacement of an outer type. By Theorem 2.20, such a fibrant replacement cannot be defined internally.

Our construction is an internalisation of the known analogous construction in traditional mathematics (see e.g. Reference ShulmanShulman 2015b , Lemma 11.10 or Riehl and Verity Reference Riehl and Verity2014).

The following characterisations of anodyne maps are straightforward to establish.

Lemma 4.13. Assume we are given a commutative triangle

where the map i is fibrewise anodyne, i.e. for all $x : X$ , the induced map $p^{-1}(x) \rightarrow q^{-1}(x)$ between the fibres is anodyne. Then, i is anodyne.

Since anodyne maps are defined by a left lifting property, they exhibit familiar closure properties, of which we recall the following:

When focusing on fibrant types, we can say more about anodyne maps.

Trivial cofibrations are in particular anodyne maps, as the following lemma shows.

The following lemma provides an important example of anodyne map which is not necessarily a trivial cofibration.

Now consider the projection $q : N \rightarrow A$ on the first component. If we use q to regard i as a map over A, then it is clear that the fibres of i have the form of Lemma 4.17 up to isomorphism, hence they are anodyne. It then follows from Lemma 4.13 that i itself is anodyne, as required.

We will refer to the type N constructed in the proof of Corollary 4.18 as the mapping cocylinder of f.

Let $\mathcal{C}$ be an inverse category with a functor $F \mathbin{\colon} \mathcal{C} \rightarrow {{\mathcal{U}}}$ . Since the category of elements $F / \mathcal{C} \rightarrow \mathcal{C}$ is a discrete Grothendieck opfibration, the induced functor is an isomorphism for any $(a, x) : F / \mathcal{C}$ , and similarly for the (non-reduced) coslices. It follows that admissibility of $\mathcal{C}$ implies admissibility of $F / \mathcal{C}$ .

Therefore, if $\mathcal{C}$ is admissible, the matching object $M^X_z$ of X is fibrant for all $z : \mathcal{C}$ . Since furthermore the map $X_z \rightarrow M^X_z$ is a fibration by the assumption that X is Reedy fibrant, we get that $X_z$ is fibrant as well.

The main example of an admissible inverse category is +, the opposite of the simplex category restricted to strictly monotone maps. We can define it concretely as follows:

That + is admissible follows from Theorem 4.8 and the fact that all the reduced coslices of + are finite.

The notion of anodyne can be extended to diagrams in a pointwise fashion.

Similarly, we have a notion of equivalence of diagrams, defined pointwise.

Let $y : \mathop{\textsf{lim}} Y$ be an arbitrary element of the limit. We can think of y as a natural transformation $y \mathbin{\colon} 1 \rightarrow Y$ . Consider the following pullback of diagrams:

By part (i) of Lemma 4.9, X[y] is a Reedy fibrant diagram, hence its limit is fibrant by the assumption on $\mathcal{C}$ . Since limits commute with pullbacks, we get a pullback diagram:

showing that the fibre of $\mathop{\textsf{lim}} p$ over y is fibrant.

Lemma 4.26. Let $f \mathbin{\colon} X \rightarrow Z$ be a natural transformation of pointwise fibrant diagrams over an admissible inverse category $\mathcal{C}$ . Then, f can be factored as:

where i is anodyne, and p is a Reedy fibration.

Proof. We will construct, by induction on the natural number n, a diagram $Y^{(n)}$ over $\mathcal{C}^{<n}$ , and a factorisation of f:

where $i^{(n)}$ is anodyne and $p^{(n)}$ is a Reedy fibration.

For $n=0$ there is nothing to construct, so assume the existence of $Y^{(n)}$ , and fix any object $x : \mathcal{C}$ of rank $n+1$ . The forgetful functor factors through $\mathcal{C}^{<n}$ ; hence, we can consider the composition $Y^{(n)} \circ j_x$ and take its limit L. Note that L is not necessarily fibrant, but the map $L \rightarrow M_x^Z$ induced by $p^{(n)}$ is a fibration by Lemma 4.25 and the admissibility of $\mathcal{C}$ . By part (i) of Lemma 3.10, we get a fibration $L \times_{M_x^Z} Z_x \rightarrow Z_x$ , hence $L \times_{M_x^Z} Z_x$ is a fibrant type.

Now f, together with $i^{(n)}$ , determine a map $X_x \rightarrow L \times_{M_x^Z} Z_x$ . Define $Y^{(n+1)}_x$ to be the mapping cocylinder of this map. For any object y of rank n or less, define $Y^{(n+1)}_y$ as $Y^{(n)}_y$ , and for any morphism $f \mathbin{\colon} x \rightarrow y$ in $\mathcal{C}$ , the corresponding function $Y^{(n+1)}_x \rightarrow Y^{(n+1)}_y$ is given by the projection from the mapping cocylinder, followed by a map of the universal cone of the limit L. The action of $Y^{(n)}$ on morphisms between objects of ranks n or less is defined to be the same as that of $Y^{(n)}$ .

It is easy to see that those definitions make $Y^{(n+1)}$ into a diagram that extends $Y^{(n)}$ to objects of rank $n+1$ . We can also extend $i^{(n)}$ by defining $i^{(n+1)}_x$ to be the embedding of $X_x$ into the mapping cocylinder $Y^{(n+1)}_x$ , which is anodyne by Corollary 4.18.

Similarly, we define $p^{(n+1)}_x$ to be the composition of the projection from the mapping cocylinder with the map $L \times_{M_x^Z} Z_x \rightarrow Z_x$ defined above. The fact that $p^{(n+1)}$ is a Reedy fibration follows immediately from the construction, since L is exactly the matching object of $Y^{(n+1)}$ at x.

To conclude the proof, we glue together all the $Y^{(n)}$ , $i^{(n)}$ and $p^{(n)}$ into a single diagram Y and natural transformations i, p. Clearly, p is a Reedy fibration, and i is an equivalence.

Proof. First suppose that $i \mathbin{\colon} A \rightarrow B$ is anodyne, and let $p \mathbin{\colon} Y \rightarrow X$ be any fibration. Consider a commutative square

For all natural numbers n, we will construct a lift w for the square of the restrictions of all the diagrams involved to $\mathcal{C}^{<n}$ . The base of the induction is trivial, so suppose we have constructed such a lift for n, and let $x \in C$ be an object of degree $n + 1$ . Consider the square:

where the bottom map is obtained from the inductively constructed lift w, together with the bottom natural transformation v of the original square.

The right map is a fibration by the assumption that p is a Reedy fibration, which lets us construct a diagonal lift $w_x$ for the square. This gives an extension of the lift w to all objects x of degree n, and naturality of w follows immediately from the commutativity of the bottom right triangle. Note that we have not used the assumption that A and B are pointwise fibrant for this direction.

Conversely, suppose that $i \mathbin{\colon} A \rightarrow B$ has the stated lifting property. Since A and B are pointwise fibrant, we can factor i as $A \xrightarrow{j} N \xrightarrow{p} B$ , where j is anodyne and p is a Reedy fibration, thanks to Lemma 4.26. At this point, a standard retract argument shows that i must be anodyne. More explicitly, first consider the square

and use the lifting property of i to get a natural transformation $r \mathbin{\colon} B \rightarrow M$ . It then follows that i is a retract of j, so in particular $i_x$ is a retract of $j_x$ for all objects $x : \mathcal{C}$ . The conclusion now follows from Lemma 4.14.

4.5 Classifiers for Reedy fibrations

Let $\mathcal{C}$ be an admissible category. The goal of this section is to construct a type that classifies, in the appropriate sense, Reedy fibrant diagrams over $\mathcal{C}$ . In certain cases, this type will itself be fibrant, giving a construction of a classifier for diagrams which is completely internal to the inner level.

The construction of this classifier makes use of a stricter notion of fibration than the one we have used so far.

Any strict fibration A over X determines a map $Y \rightarrow X$ , where . We will sometimes abuse language and refer to a map $p : Y \rightarrow X$ itself as a strict fibration, with the convention that strict fibrations are always assumed to be equipped with a corresponding choice of a family A, which we will refer to as a strict fibration structure on p. Fibrations can then be characterised as those maps $Y \rightarrow X$ that are isomorphic over X to some strict fibration. In particular, strict fibrations are fibrations.

Correspondingly, we get a notion of strict Reedy fibration, simply by replacing fibrations with strict fibrations in Definition 4.6.

Definition 4.31. Let $\mathcal{C}$ be an inverse category. A strict Reedy fibration is a natural transformation $p \mathbin{\colon} Y \rightarrow X$ , where X and Y are diagrams on $\mathcal{C}$ , together with, for all $z : \mathcal{C}$ , a choice of a strict fibration structure $\overline Y_z$ for the canonical map

(18) \begin{equation} Y_z \rightarrow M_z^Y \times_{M_z^X} X_z.\end{equation}

A strictly Reedy fibrant diagram is a strict Reedy fibration $X \rightarrow 1$ .

It is crucial to observe that the notion of strict fibration is not invariant under isomorphism, since it uses strict equality of types. Consequently, (18) has to be intended with a specific choice of pullbacks and limits in the target type. For concreteness, given a functor $F \mathbin{\colon} \mathcal{A} \rightarrow {{\mathcal{U}}}$ , we will always choose the limit of F to be the type given by $\textbf{Nat}(1, F)$ .

Nevertheless, given a type X, the type of strict fibrations over X is isomorphic to the type of functions $X \rightarrow {{{\mathcal{U}}}}^{\textsf{i}}$ , so it is a representable functor of X, hence in particular if $X \cong Y$ , then also the types of strict fibrations over X and Y are isomorphic.

Again, since strict fibrations are in particular fibrations, it follows that strict Reedy fibrations are Reedy fibrations. Recall that both notions are equipped with structure, namely a choice of a family of inner types for all objects of the base category. For our usage of Reedy fibration, this choice usually does not matter; however, for strict Reedy fibrations, it is important.

Definition 4.32. Given strict Reedy fibrations $X \rightarrow A$ and $Y \rightarrow B$ , a morphism between them is a pullback square

such that for all $z : \mathcal{C}$ , the induced triangle

(19)

commutes.

With this definition of morphisms, the collection of strict Reedy fibrations on an inverse category $\mathcal{C}$ forms a category, which we will denote by $\mathcal{R}_{\mathcal{C}}$ .

then it is clear we can uniquely construct a map $X \rightarrow Y$ that fits into a pullback square

To show that this is a morphism of strict Reedy fibrations, observe that in the induced diagram

the outermost triangle and the right triangle commute, and hence the left triangle commutes as well.

Now, let $f \mathbin{\colon} A \rightarrow B$ be a natural transformation, and $Y \rightarrow B$ a strict Reedy fibration. We want to show that there exists a unique strict Reedy fibration $X \rightarrow A$ equipped with a morphism $Y \rightarrow B$ . For all natural numbers n, we construct a strict Reedy fibration $X^{(n)} \rightarrow A|n$ on $\mathcal{C}^{<n}$ , together with a morphism to $Y|n \rightarrow B|n$ , with the property that $X^{(n+1)} | n = X^{(n)}$ .

The base case is trivial as usual; hence, we can assume that we have constructed $X^{(n)}$ . If $z : \mathcal{C}$ has rank n, let $\overline X_z^{(n+1)}$ be the composition

\[ M_z^{X^{(n)}} \times_{M_z^A} A_z \rightarrow M_z^Y \times_{M_z^B} B_z \rightarrow {{{\mathcal{U}}}}^{\textsf{i}}, \]

and define . It is easy to verify that this defines an extension $X^{(n+1)}$ of $X^{(n)}$ to objects of degree n. The map $X^{(n+1)} \rightarrow A$ is a strict Reedy fibration, and the choice of $\overline X_z^{(n+1)}$ induces a morphism of strict Reedy fibrations $X^{(n+1)} \rightarrow Y$ , essentially by construction.

As for uniqueness, note that the choice of $\overline X_z^{(n+1)}$ is forced by the requirement that the triangle (19) commute; hence, the fibration $X^{(n+1)} \rightarrow A$ and the morphism to $Y|n \rightarrow B|n$ are uniquely determined by the corresponding data for n. It follows that the whole fibration $X \rightarrow A$ and morphism to $Y \rightarrow B$ , obtained by gluing all the $X^{(n)}$ , are uniquely determined.

The discrete Grothendieck fibration $\mathcal{R}_{\mathcal{C}} \rightarrow [\mathcal{C}, {{\mathcal{U}}}]$ determines a presheaf $\textsf{Reedy}$ on $[\mathcal{C}, {{\mathcal{U}}}]$ . For the next lemma, recall that, for a category $\mathcal{A}$ with pullbacks, a diagram $X \mathbin{\colon} I \rightarrow \mathcal{A}$ is said to have a van Kampen colimit if the colimit of X exists, and the reindexing functor induces an equivalence of categories

\[ \mathcal{A} / \mathop{\textsf{colim}} X \xrightarrow{\cong} \mathop{\textsf{lim}}_i \mathcal{A} / X_i.\]