An interpretation of dependent type theory in a model category of locally cartesian closed categories

Abstract

Locally cartesian closed (lcc) categories are natural categorical models of extensional dependent type theory. This paper introduces the “gros” semantics in the category of lcc categories: Instead of constructing an interpretation in a given individual lcc category, we show that also the category of all lcc categories can be endowed with the structure of a model of dependent type theory. The original interpretation in an individual lcc category can then be recovered by slicing.

As in the original interpretation, we face the issue of coherence: Categorical structure is usually preserved by functors only up to isomorphism, whereas syntactic substitution commutes strictly with all type theoretic structure. Our solution involves a suitable presentation of the higher category of lcc categories as model category. To that end, we construct a model category of lcc sketches, from which we obtain by the formalism of algebraically (co)fibrant objects model categories of strict lcc categories and then algebraically cofibrant strict lcc categories. The latter is our model of dependent type theory.

1 Introduction

Locally cartesian closed (lcc) categories are natural categorical models of extensional dependent type theory [19]: Given an lcc category $\text{[math]}$ , one interprets

contexts $\text{[math]}$ as objects of $\text{[math]}$ ;
(simultaneous) substitutions from context $\text{[math]}$ to context $\text{[math]}$ as morphisms $\text{[math]}$ in $\text{[math]}$ ;
types $\text{[math]}$ as morphisms $\text{[math]}$ in $\text{[math]}$ with codomain $\text{[math]}$ ; and
terms $\text{[math]}$ as sections $\text{[math]}$ to the interpretations of types.

A context extension $\text{[math]}$ is interpreted as the domain of $\text{[math]}$ . Application of a substitution $\text{[math]}$ to a type $\text{[math]}$ is interpreted as pullback

and similarly for terms $\text{[math]}$ . By definition, the pullback functors $\text{[math]}$ in lcc categories $\text{[math]}$ have both left and right adjoints $\text{[math]}$ , and these are used for interpreting $\text{[math]}$ -types and $\text{[math]}$ -types. For example, the interpretation of a pair of types $\text{[math]}$ and $\text{[math]}$ is a composable pair of morphisms $\text{[math]}$ , and then the dependent product type $\text{[math]}$ is interpreted as $\text{[math]}$ , which is an object of $\text{[math]}$ , i.e. a morphism into $\text{[math]}$ .

However, there is a slight mismatch: Syntactic substitution is functorial and commutes strictly with type formers, whereas pullback is generally only pseudo-functorial and hence preserves universal objects only up to isomorphism. Here functoriality of substitution means that if one has a sequence $\text{[math]}$ of substitutions, then we have equalities $\text{[math]}$ and $\text{[math]}$ , i.e. substituting in succession yields the same result as substituting with the composition. For pullback functors, however, we are only guaranteed a natural isomorphism $\text{[math]}$ . Similarly, in type theory we have $\text{[math]}$ (where $\text{[math]}$ denotes the weakening of $\text{[math]}$ along $\text{[math]}$ ), whereas for pullback functors there merely exist isomorphisms $\text{[math]}$ .

In response to these problems, several notions of models with strict pullback operations were introduced, e.g. categories with families (cwfs) [11], and coherence techniques were developed to “strictify” weak models such as lcc categories to obtain models with well-behaved substitution [9, 13, 15]. Thus to interpret dependent type theory in some lcc category $\text{[math]}$ , one first constructs an equivalence $\text{[math]}$ such that $\text{[math]}$ can be endowed with the structure of a strict model of type theory (say, cwf structure), and then interprets type theory in $\text{[math]}$ .

In this paper we construct cwf structure on the category of all lcc categories instead of cwf structure on some specific lcc category. First note that the classical interpretation of type theory in an lcc category $\text{[math]}$ is essentially an interpretation in the slice categories of $\text{[math]}$ :

Objects $\text{[math]}$ can be identified with slice categories $\text{[math]}$ .
Morphisms $\text{[math]}$ can be identified with lcc functors $\text{[math]}$ which commute with the pullback functors $\text{[math]}$ and $\text{[math]}$ .
Morphisms $\text{[math]}$ with codomain $\text{[math]}$ can be identified with the objects of the slice categories $\text{[math]}$ .
Sections $\text{[math]}$ can be identified with morphisms $\text{[math]}$ with $\text{[math]}$ the terminal object in the slice category $\text{[math]}$ .

Removing all reference to the base category $\text{[math]}$ , we may now attempt to interpret

each context $\text{[math]}$ as a separate lcc category;
a substitution from $\text{[math]}$ to $\text{[math]}$ as an lcc functor $\text{[math]}$ ;
types $\text{[math]}$ as objects $\text{[math]}$ ; and
terms $\text{[math]}$ as morphisms $\text{[math]}$ from a terminal object $\text{[math]}$ to $\text{[math]}$ .

In the original interpretation, substitution in types and terms is defined by the pullback functor $\text{[math]}$ along a morphism $\text{[math]}$ . In our new interpretation, $\text{[math]}$ is already an lcc functor, which we simply apply to objects and morphisms of lcc categories.

The idea that different contexts should be understood as different categories is by no means novel, and indeed widespread among researchers of geometric logic; see e.g. [20, section 4.5]. Not surprisingly, some of the ideas in this paper have independently already been explored, in more explicit form, in [21] for geometric logic. To my knowledge, however, an interpretation of type theory along those lines, especially one with strict substitution, has never been spelled out explicitly, and the present paper is an attempt at filling this gap.

Like Seely's original interpretation, the naive interpretation in the category of lcc categories outlined above suffers from coherence issues: Lcc functors preserve lcc structure up to isomorphism, but not necessarily up to equality, and the latter would be required for a model of type theory.

Even worse, our interpretation of contexts as lcc categories does not admit well-behaved context extensions. Recall that for a context $\text{[math]}$ and a type $\text{[math]}$ in a cwf, a context extension consists of a context morphism $\text{[math]}$ and a term $\text{[math]}$ such that for every morphism $\text{[math]}$ and term $\text{[math]}$ there is a unique morphism $\text{[math]}$ over $\text{[math]}$ such that $\text{[math]}$ . In our case a context morphism is an lcc functor in the opposite direction. Thus a context extension of an lcc category $\text{[math]}$ by $\text{[math]}$ would consist of an lcc functor $\text{[math]}$ and a morphism $\text{[math]}$ in $\text{[math]}$ , and $\text{[math]}$ would have to be suitably initial. At first sight it might seem that the slice category $\text{[math]}$ is a good candidate: Pullback along the unique map $\text{[math]}$ defines an lcc functor $\text{[math]}$ . The terminal object of $\text{[math]}$ is the identity on $\text{[math]}$ , and applying $\text{[math]}$ to $\text{[math]}$ itself yields the first projection $\text{[math]}$ . Thus the diagonal $\text{[math]}$ is a term $\text{[math]}$ . The problem is that, while this data is indeed universal, it is only so in the bicategorical sense (see Lemma 29): Given an lcc functor $\text{[math]}$ and term $\text{[math]}$ , we obtain an lcc functor

however, $\text{[math]}$ commutes with $\text{[math]}$ and $\text{[math]}$ only up to natural isomorphism, the equation $\text{[math]}$ holds only up to this natural isomorphism, and $\text{[math]}$ is unique only up to unique isomorphism.

The issue with context extensions can be understood from the perspective of comprehension categories, an alternative notion of model of type theory, as follows. Our cwf is constructed on the opposite of $\text{[math]}$ , the category of lcc categories and lcc functors. The corresponding comprehension category should thus consist of a Grothendieck fibration $\text{[math]}$ and a functor $\text{[math]}$ to the arrow category of $\text{[math]}$ such that

commutes and $\text{[math]}$ is a pullback square for each cartesian morphism $\text{[math]}$ in $\text{[math]}$ . The data of a Grothendieck fibration $\text{[math]}$ as above is equivalent to a (covariant) functor $\text{[math]}$ via the Grothendieck construction, and here we simply take the forgetful functor. Thus the objects of $\text{[math]}$ are pairs $\text{[math]}$ such that $\text{[math]}$ is an lcc category and $\text{[math]}$ , and a morphism $\text{[math]}$ in $\text{[math]}$ is a pair $\text{[math]}$ of lcc functor $\text{[math]}$ and morphism $\text{[math]}$ in $\text{[math]}$ .

The functor $\text{[math]}$ should assign to objects $\text{[math]}$ of $\text{[math]}$ the projection of the corresponding context extension, hence we define $\text{[math]}$ as the pullback functor to the slice category. The cartesian morphisms of $\text{[math]}$ are those with invertible vertical components $\text{[math]}$ , so they are given up to isomorphism by pairs of the form $\text{[math]}$ . The images of such morphisms under $\text{[math]}$ are squares

(1)

in $\text{[math]}$ . For $\text{[math]}$ to be a comprehension category, they would have to be pushout squares, but in fact they are bipushout squares: They satisfy the universal property of pushouts up to unique isomorphism, but not up to equality. If $\text{[math]}$ does not preserve pullback squares up to strict equality, then the square (1) commutes only up to isomorphism, not equality. Thus $\text{[math]}$ is not even a functor but a bifunctor.

Usually when one considers coherence problems for type theory, the problem lies in the fibration $\text{[math]}$ , which is often not strict, and it suffices to change the total category $\text{[math]}$ while leaving the base unaltered. Our fibration $\text{[math]}$ is already strict, but it does not support substitution stable type constructors. Here the main problem is the base category, however: The required pullback diagrams exist only in the bicategorical sense. Thus the usual constructions [13, 15] are not applicable.

The goal must thus be to find a category that is (bi)equivalent to $\text{[math]}$ in which we can replace the bipushout squares (1) by 1-categorical pushouts. Our tool of choice to that end will be model category theory (see e.g. [12]). Model categories are presentations of higher categories as ordinary 1-categories with additional structure. Crucially, model categories allow the computation of higher (co)limits as ordinary 1-categorical (co)limits under suitable hypotheses. The underlying 1-category of the model category presenting a higher category is not unique, and some presentations are more suitable for our purposes than others. We explore three Quillen equivalent model categories, all of which encode the same higher category of lcc categories, and show that the third one indeed admits the structure of a model of dependent type theory.

Because of its central role in the paper, the reader is thus expected to be familiar with some notions of model category theory. We make extensive use of the notion of algebraically (co)fibrant object in a model category [18, 7], but the relevant results are explained where necessary and can be taken as black boxes for the purpose of this paper. Because of the condition on enrichment in Theorem 21, all model categories considered here are proved to be model $\text{[math]}$ -categories, that is, model categories enriched over the category of groupoids with their canonical model structure. See [3] for background on enriched model category theory, [4] for the canonical model category of groupoids, and [14] for the closely related model $\text{[math]}$ -categories. While it is more common to work with the more general simplicially enriched model categories, the fact that the higher category of lcc categories is 2-truncated affords us to work with simpler groupoid enrichments instead.

In Section 2 we construct the model category $\text{[math]}$ of lcc sketches, a left Bousfield localization of an instance of Isaev's model category structure on marked objects [2]. Lcc sketches are to lcc categories as finite limit sketches are to finite limit categories. Thus lcc sketches are categories with some diagrams marked as supposed to correspond to a universal object of lcc categories, but marked diagrams do not have to actually satisfy the universal property. The model category structure is set up such that every lcc sketch generates an lcc category via fibrant replacement, and lcc sketches are equivalent if and only if they generate equivalent lcc categories.

In Section 3 we define the model category $\text{[math]}$ of strict lcc categories. Strict lcc categories are the algebraically fibrant objects of $\text{[math]}$ , that is, they are objects of $\text{[math]}$ equipped with canonical lifts against trivial cofibrations witnessing their fibrancy in $\text{[math]}$ . Such canonical lifts correspond to canonical choices of universal objects in lcc categories, and the morphisms in $\text{[math]}$ preserve these canonical choices not only up to isomorphism but up to equality.

Section 4 finally establishes the model of type theory in the opposite of $\text{[math]}$ , the model category of algebraically cofibrant objects in $\text{[math]}$ . The objects of $\text{[math]}$ are strict lcc categories $\text{[math]}$ such that every (possibly non-strict) lcc functor $\text{[math]}$ has a canonical strict isomorph. This additional structure is crucial to reconcile the context extension operation, which is given by freely adjoining a morphism to a strict lcc category, with taking slice categories.

In Section 5 we show that the cwf structure on $\text{[math]}$ can be used to rectify Seely's original interpretation in a given lcc category $\text{[math]}$ . This is done by choosing an equivalent lcc category $\text{[math]}$ with $\text{[math]}$ , and then $\text{[math]}$ inherits cwf structure from the core of the slice cwf $\text{[math]}$ .

Acknowledgements. This paper benefited significantly from input by several members of the research community. I would like to thank the organizers of the TYPES workshop 2019 and the HoTT conference 2019 for giving me the opportunity to present preliminary versions of the material in this paper. Conversations with Emily Riehl, Karol Szumiło and David White made me aware that the constructions in this paper can be phrased in terms of model category theory. Daniel Gratzer pointed out to me the biuniversal property of slice categories. Valery Isaev explained to me some aspects of the model category structure on marked objects. I would like to thank my advisor Bas Spitters for his advice on this paper, which is part of my PhD research.

This work was supported by the Air Force Office and Scientific Research project “Homotopy Type Theory and Probabilistic Computation”, grant number 12595060.

2 Lcc sketches

This section is concerned with the model category $\text{[math]}$ of lcc sketches. $\text{[math]}$ is constructed as the left Bousfield localization of a model category of lcc-marked objects, an instance of Isaev's model category structure on marked objects.

Definition 1 ([2] Definition 2.1).

Let $\text{[math]}$ be a category and let $\text{[math]}$ be a diagram in $\text{[math]}$ . An ( $\text{[math]}$ -)marked object is given by an object $\text{[math]}$ in $\text{[math]}$ and a subfunctor $\text{[math]}$ of $\text{[math]}$ . A map of the form $\text{[math]}$ is marked if $\text{[math]}$ .

A morphism of $\text{[math]}$ -marked objects is a marking-preserving morphism of underlying objects in $\text{[math]}$ , i.e. a morphism $\text{[math]}$ such that the image of $\text{[math]}$ under postcomposition by $\text{[math]}$ is contained in $\text{[math]}$ . The category of $\text{[math]}$ -marked objects is denoted by $\text{[math]}$ .

The forgetful functor $\text{[math]}$ has a left and right adjoint: Its left adjoint $\text{[math]}$ is given by equipping an object $\text{[math]}$ of $\text{[math]}$ with the minimal marking $\text{[math]}$ , while the right adjoint $\text{[math]}$ equips objects with their maximal marking $\text{[math]}$ .

In our application, $\text{[math]}$ is the category of (sufficiently small) categories, and $\text{[math]}$ contains diagrams corresponding to the shapes (e.g. a squares for pullbacks) of lcc structure.

Definition 2.

The subcategory $\text{[math]}$ of lcc shapes is given as follows: Its objects are the three diagrams $\text{[math]}$ , $\text{[math]}$ and $\text{[math]}$ . $\text{[math]}$ is given by the category with a single object $\text{[math]}$ and no nontrivial morphisms; it corresponds to terminal objects. $\text{[math]}$ is the free-standing non-commutative square

and corresponds to pullback squares. $\text{[math]}$ is the free-standing non-commutative diagram

and corresponds to dependent products $\text{[math]}$ and their evaluation maps $\text{[math]}$ . The only nontrivial functor in $\text{[math]}$ is the inclusion of $\text{[math]}$ into $\text{[math]}$ as indicated by the variable names. It corresponds to the requirement that the domain of the evaluation map of dependent products must be a suitable pullback.

We obtain the category $\text{[math]}$ of lcc-marked categories.

Now suppose that $\text{[math]}$ is a model category. Let $\text{[math]}$ be the quotient functor to the homotopy category. A marking $\text{[math]}$ of some $\text{[math]}$ induces a canonical marking $\text{[math]}$ on $\text{[math]}$ by taking $\text{[math]}$ to be the image of $\text{[math]}$ under $\text{[math]}$ . Thus a morphism $\text{[math]}$ in $\text{[math]}$ is marked if and only if it has a preimage under $\text{[math]}$ which is marked.

Theorem 3 ([2] Theorem 3.3).

Let $\text{[math]}$ be a combinatorial model category and let $\text{[math]}$ be a diagram in $\text{[math]}$ such that every object in the image of $\text{[math]}$ is cofibrant. Then the following defines the structure of a combinatorial model category on $\text{[math]}$ :

A morphism $\text{[math]}$ in $\text{[math]}$ is a cofibration if and only if $\text{[math]}$ is a cofibration in $\text{[math]}$ .
A morphism $\text{[math]}$ in $\text{[math]}$ is a weak equivalence if and only if $\text{[math]}$ is an isomorphism in $\text{[math]}$ .

A marked object $\text{[math]}$ is fibrant if and only if $\text{[math]}$ is fibrant in $\text{[math]}$ and the markings of $\text{[math]}$ are stable under homotopy; that is, if $\text{[math]}$ are homotopic maps in $\text{[math]}$ and $\text{[math]}$ is marked, then $\text{[math]}$ is marked. The adjunctions $\text{[math]}$ and $\text{[math]}$ are Quillen adjunctions.

Remark 4.

The description of weak equivalences in Theorem 3 does not appear as stated in [2], but follows easily from results therein. Let $\text{[math]}$ be a fibrant replacement functor. By [2, lemma 2.5], a map $\text{[math]}$ is a weak equivalence in $\text{[math]}$ if and only if $\text{[math]}$ is a weak equivalence in $\text{[math]}$ and for every diagram (of solid arrows)

(2)

in which the outer square commutes up to homotopy and $\text{[math]}$ is marked, there exists a marked map $\text{[math]}$ as indicated such that $\text{[math]}$ . ( $\text{[math]}$ is not required to commute with $\text{[math]}$ and $\text{[math]}$ .)

Now assume that $\text{[math]}$ satisfies this condition and let us prove that $\text{[math]}$ is an isomorphism of induced marked objects in the homotopy category. $\text{[math]}$ is an isomorphism in $\text{[math]}$ , so it suffices to show that $\text{[math]}$ preserves markings. By definition, every marked morphism of $\text{[math]}$ is of the form $\text{[math]}$ for some marked $\text{[math]}$ . Because $\text{[math]}$ is cofibrant and $\text{[math]}$ is fibrant, the map $\text{[math]}$ has a preimage $\text{[math]}$ under $\text{[math]}$ . As $\text{[math]}$ is cofibrant, $\text{[math]}$ is fibrant and $\text{[math]}$ , there is a homotopy $\text{[math]}$ . By assumption, there exists a marked map $\text{[math]}$ such that $\text{[math]}$ , thus $\text{[math]}$ is marked.

To prove the other direction of the equivalence, assume that $\text{[math]}$ is an isomorphism of marked objects and let $\text{[math]}$ be as in diagram (2). $\text{[math]}$ is marked, hence has a preimage $\text{[math]}$ under $\text{[math]}$ which is marked. We have $\text{[math]}$ because postcomposition of both sides with the isomorphism $\text{[math]}$ gives equal results. $\text{[math]}$ is cofibrant and $\text{[math]}$ is fibrant, thus $\text{[math]}$ .

Lemma 5.

Let $\text{[math]}$ and $\text{[math]}$ be as in Theorem 3.

If $\text{[math]}$ is a left proper model category, then $\text{[math]}$ is a left proper model category.
If $\text{[math]}$ is a model $\text{[math]}$ -category, then $\text{[math]}$ admits the structure of a model $\text{[math]}$ -category such that $\text{[math]}$ and $\text{[math]}$ lift to Quillen $\text{[math]}$ -adjunctions.

Proof. 1. Let

be a pushout square in $\text{[math]}$ such that $\text{[math]}$ is a weak equivalence. $\text{[math]}$ is left proper, so $\text{[math]}$ is invertible as a map in $\text{[math]}$ .

A map $\text{[math]}$ is marked if and only if it factors via a marked map $\text{[math]}$ or via a marked map $\text{[math]}$ . In the first case,

which is marked because $\text{[math]}$ is a weak equivalence. Otherwise

which is also marked. We have shown that $\text{[math]}$ is an isomorphism of marked objects in $\text{[math]}$ , thus $\text{[math]}$ is a weak equivalence.

2. Let $\text{[math]}$ and $\text{[math]}$ be marked objects. We define the mapping groupoid $\text{[math]}$ as the full subgroupoid of $\text{[math]}$ of marking preserving maps.

$\text{[math]}$ is complete and cocomplete as a 1-category. Thus if we construct tensors $\text{[math]}$ and powers $\text{[math]}$ for all $\text{[math]}$ and $\text{[math]}$ it follows that $\text{[math]}$ is also complete and cocomplete as a $\text{[math]}$ -category. The underlying object of powers and copowers is constructed in $\text{[math]}$ , i.e. $\text{[math]}$ and $\text{[math]}$ . A map $\text{[math]}$ is marked if and only if the composite

is marked for every $\text{[math]}$ (which we identify with a map $\text{[math]}$ ). Similarly, a map $\text{[math]}$ is marked if and only if it factors as

for some object $\text{[math]}$ in $\text{[math]}$ and marked $\text{[math]}$ . It follows by [1, Theorem 4.85] from the preservation of tensors and powers by $\text{[math]}$ that the 1-categorical adjunctions $\text{[math]}$ and $\text{[math]}$ extend to $\text{[math]}$ -adjunctions.

It remains to show that the tensoring $\text{[math]}$ is a Quillen bifunctor. For this we need to prove that if $\text{[math]}$ is a cofibration of groupoids and $\text{[math]}$ is a cofibration of marked objects, then their pushout-product

is a cofibration, and that it is a weak equivalence if either $\text{[math]}$ or $\text{[math]}$ is furthermore a weak equivalence. The first part follows directly from the same property for the $\text{[math]}$ -enrichment of $\text{[math]}$ and the fact that $\text{[math]}$ preserves tensors and pushouts, and reflects cofibrations.

In the second part we have in both cases that $\text{[math]}$ is a weak equivalence in $\text{[math]}$ . Thus we only need to show that $\text{[math]}$ reflects a given marked morphism $\text{[math]}$ in $\text{[math]}$ . It follows from the construction of $\text{[math]}$ that for any such $\text{[math]}$ there exists $\text{[math]}$ such that $\text{[math]}$ for some marked map $\text{[math]}$ .

Assume first that $\text{[math]}$ is a trivial cofibration, i.e. an equivalence of groupoids that is injective on objects. Then there exists $\text{[math]}$ such that $\text{[math]}$ and $\text{[math]}$ are isomorphic objects of $\text{[math]}$ . $\text{[math]}$ is (left) homotopic to $\text{[math]}$ , which factors via the marked map $\text{[math]}$ . It follows that $\text{[math]}$ reflects marked morphisms.

Now assume that $\text{[math]}$ is a trivial cofibration. Then $\text{[math]}$ reflects marked maps, i.e. there exists a marked map $\text{[math]}$ such that $\text{[math]}$ . Thus the equivalence class of $\text{[math]}$ in $\text{[math]}$ is marked and mapped to $\text{[math]}$ under postcomposition by $\text{[math]}$ .

In the semantics of logic, one usually defines the notion of model of a logical theory in two steps: First a notion of structure is defined that interprets the theory's signature, i.e. the function and relation symbols that occur in its axioms. Then one defines what it means for such a structure to satisfy a formula over the signature, and a model is a structure of the theory's signature which satisfies the theory's axioms. For very well-behaved logics such as Lawvere theories, there is a method of freely turning structures into models of the theory, so that the category of models is a reflective subcategory of the category of structures.

By analogy, lcc-marked categories correspond to the structures of the signature of lcc categories. The model structure of $\text{[math]}$ ensures that markings respect the homotopy theory of $\text{[math]}$ , in that the choice of marking is only relevant up to isomorphism of diagrams. However, the model structure does not encode the universal property that marked diagrams are ultimately supposed to satisfy. To obtain the analogue of the category of models for a logical theory, we now define a reflective subcategory of $\text{[math]}$ . The technical tool to accomplish this is a left Bousfield localization at a set $\text{[math]}$ of morphisms in $\text{[math]}$ . $\text{[math]}$ corresponds to the set of axioms of a logical theory. We thus need to define $\text{[math]}$ in such a way that an lcc-marked category is lcc if and only if it has the right lifting property against the morphisms in $\text{[math]}$ such that lifts are determined uniquely up to unique isomorphism.

$\text{[math]}$ is a combinatorial and left proper model $\text{[math]}$ -category with mapping groupoids $\text{[math]}$ given by sets of functors and their natural isomorphisms. Thus $\text{[math]}$ has the structure of a combinatorial and left proper model $\text{[math]}$ -category by Lemma 5. It follows that the left Bousfield localization at any (small) set of maps exists by [12, Theorem 4.1.1].

Definition 6.

The model category $\text{[math]}$ of lcc sketches is the left Bousfield localization of the model category of $\text{[math]}$ -marked categories at the following morphisms.

The morphism $\text{[math]}$ given by the unique map from the empty category to the marked category with a single, $\text{[math]}$ -marked object. $\text{[math]}$ corresponds to the essentially unique existence of a terminal object.
The morphism $\text{[math]}$ given by the inclusion of the category with two objects

such that $\text{[math]}$ is $\text{[math]}$ -marked into

$\text{[math]}$ corresponds to the universal property of terminal objects.
The morphism $\text{[math]}$ given by the quotient map from the free-standing non-commutative and $\text{[math]}$ -marked square

to the commuting square

(which is still marked via $\text{[math]}$ ). $\text{[math]}$ corresponds to the commutativity of pullback squares.
The morphism $\text{[math]}$ given by the inclusion of the cospan

with no markings into the non-commutative square

which is marked via $\text{[math]}$ . $\text{[math]}$ corresponds to the essentially unique existence of pullback squares.
The morphism $\text{[math]}$ given by the inclusion of

in which the lower right square is non-commutative and marked via $\text{[math]}$ , into the diagram

in which the indicated triangles commute. $\text{[math]}$ corresponds to the universal property of pullback squares.
The morphism $\text{[math]}$ given by the quotient map of the non-commutative diagram

in which the square made of the $\text{[math]}$ and $\text{[math]}$ is marked via $\text{[math]}$ and the whole diagrams is marked via $\text{[math]}$ , to

in which the indicated triangle commutes. $\text{[math]}$ corresponds to the requirement that the evaluation map $\text{[math]}$ of the dependent product $\text{[math]}$ is a morphism in the slice category over $\text{[math]}$ .
The morphism $\text{[math]}$ given by the inclusion of a composable pair of morphisms

into the non-commutative diagram

which is marked via $\text{[math]}$ (and hence the outer square is marked via $\text{[math]}$ ). $\text{[math]}$ corresponds to the essentially unique existence of dependent products $\text{[math]}$ and their evaluation maps $\text{[math]}$ .
The morphism $\text{[math]}$ given by the inclusion of the diagram

in which the square given by the $\text{[math]}$ and $\text{[math]}$ is marked via $\text{[math]}$ , the subdiagram given by the $\text{[math]}$ and $\text{[math]}$ is marked via $\text{[math]}$ , the square given by $\text{[math]}$ and the $\text{[math]}$ is marked via $\text{[math]}$ , and $\text{[math]}$ , into the diagram

in which $\text{[math]}$ commutes with the $\text{[math]}$ and $\text{[math]}$ , and $\text{[math]}$ . $\text{[math]}$ corresponds to the universal property of the dependent product $\text{[math]}$ .

Proposition 7.

The model category $\text{[math]}$ is a model for the $\text{[math]}$ -category of lcc categories and lcc functors:

An object is fibrant if and only if its underlying category is lcc and
- a map $\text{[math]}$ is marked if and only if its image is a terminal object;
- a map $\text{[math]}$ is marked if and only if its image is a pullback square; and
- a map $\text{[math]}$ is marked if and only if its image is (isomorphic to) the diagram of the evaluation map of a dependent product.
The homotopy category of $\text{[math]}$ is equivalent to the category of lcc categories and isomorphism classes of lcc functors.
The homotopy function complexes of fibrant lcc sketches are given by the groupoids of lcc functors and their natural isomorphisms.

Proof. Homotopy function complexes of maps from cofibrant to fibrant objects in a model $\text{[math]}$ -category can be computed as nerves of the groupoid enrichment. Thus 2 and 3 follow from 1 and Lemma 5.

By [12, Theorem 4.1.1], the fibrant objects of the left Bousfield localization $\text{[math]}$ at the set $\text{[math]}$ of morphisms from Definition 6 are precisely the fibrant lcc-marked categories $\text{[math]}$ which are $\text{[math]}$ -local for all $\text{[math]}$ . The verification of the equivalence asserted in 1 can thus be split up into three parts corresponding to terminal objects, pullback squares and dependent products. As the three proofs are very similar, we give only the proof for pullbacks. For this we must show that if $\text{[math]}$ is a $\text{[math]}$ -marked category, then marked maps $\text{[math]}$ are stable under isomorphisms and $\text{[math]}$ is $\text{[math]}$ -local for $\text{[math]}$ if and only if the underlying category $\text{[math]}$ has all pullbacks and maps $\text{[math]}$ are marked if and only if their images are pullbacks.

Let $\text{[math]}$ be a model $\text{[math]}$ -category. The homotopy function complexes of maps from cofibrant to fibrant objects in $\text{[math]}$ can be computed as nerves of mapping groupoids. The nerve functor $\text{[math]}$ preserves and reflects trivial fibrations. Thus if $\text{[math]}$ is a morphism of cofibrant objects $\text{[math]}$ , then a fibrant object $\text{[math]}$ is $\text{[math]}$ -local if and only if

is a trivial fibration of groupoids, i.e. an equivalence that is surjective on objects.

Unfolding this we obtain the following characterization of $\text{[math]}$ -locality for a fibrant $\text{[math]}$ -marked category:

$\text{[math]}$ is $\text{[math]}$ -local if and only if all $\text{[math]}$ -marked squares commute.
$\text{[math]}$ is $\text{[math]}$ -local if and only if every cospan can be completed to a $\text{[math]}$ -marked square, and isomorphisms of cospans can be lifted uniquely to isomorphisms of $\text{[math]}$ -marked squares completing them.
$\text{[math]}$ is $\text{[math]}$ -local if and only if every commutative square completing the lower cospan of a $\text{[math]}$ -marked square factors via the $\text{[math]}$ -marked square, and every factorization is compatible with natural isomorphisms of diagrams. By compatibility with the identity isomorphism, the factorization is unique.

If these conditions are satisfied, then every cospan in $\text{[math]}$ can be completed to a pullback square which is $\text{[math]}$ -marked, and $\text{[math]}$ -marked squares are pullbacks. By fibrancy of $\text{[math]}$ , it follows that precisely the pullback squares are $\text{[math]}$ -marked.

Conversely, if we take as $\text{[math]}$ -marked squares the pullbacks in a category $\text{[math]}$ with all pullbacks, then $\text{[math]}$ -marked squares will be stable under isomorphism, and, by the characterization above, $\text{[math]}$ will be $\text{[math]}$ -local for all $\text{[math]}$ .

3 Strict lcc categories

A naive interpretation of type theory in the fibrant objects of $\text{[math]}$ as outlined in the introduction suffers from very similar issues as Seely's original version: Type theoretic structure is preserved up to equality by substitution, but lcc functors preserve the corresponding objects with universal properties only up to isomorphism.

In this section, we explore an alternative model categorical presentation of the higher category of lcc categories. Our goal is to rectify the deficiency that lcc functors do not preserve lcc structure up to equality. Indeed, lcc structure on fibrant lcc sketches is induced by a right lifting property, so there is no preferred choice of lcc structure on fibrant lcc sketches. We can thus not even state the required preservation up to equality. To be able to speak of distinguished choice of lcc structure, we employ the following technical device.

Definition 8 ([18]).

Let $\text{[math]}$ be a combinatorial model category and let $\text{[math]}$ be a set of trivial cofibrations such that objects with the right lifting property against $\text{[math]}$ are fibrant. An algebraically fibrant object of $\text{[math]}$ (with respect to $\text{[math]}$ ) consists of an object $\text{[math]}$ equipped with a choice of lifts against all morphisms $\text{[math]}$ . Thus $\text{[math]}$ comes with maps $\text{[math]}$ for all $\text{[math]}$ in $\text{[math]}$ and $\text{[math]}$ in $\text{[math]}$ such that

commutes. A morphism of algebraically fibrant objects $\text{[math]}$ is a morphism $\text{[math]}$ in $\text{[math]}$ that preserves the choices of lifts, in the sense that $\text{[math]}$ for all $\text{[math]}$ in $\text{[math]}$ and $\text{[math]}$ . The category of algebraically fibrant objects is denoted by $\text{[math]}$ , and the evident forgetful functor $\text{[math]}$ by $\text{[math]}$ .

Proposition 9.

Denote by $\text{[math]}$ the free-standing isomorphism with objects $\text{[math]}$ and $\text{[math]}$ and let $\text{[math]}$ . Let $\text{[math]}$ be the lcc-marked object given by $\text{[math]}$ with $\text{[math]}$ the only marking for $\text{[math]}$ and $\text{[math]}$ , $\text{[math]}$ the markings for $\text{[math]}$ , and denote by $\text{[math]}$ the obvious inclusion.

Then $\text{[math]}$ is a trivial cofibration in $\text{[math]}$ , and an object of $\text{[math]}$ is fibrant if and only if it has the right lifting property against $\text{[math]}$ for all $\text{[math]}$ .

Proof. The maps $\text{[math]}$ are injective on objects and hence cofibrations, and they reflect markings up to isomorphism, hence are also weak equivalences. A map $\text{[math]}$ corresponds to an isomorphism of maps $\text{[math]}$ with $\text{[math]}$ marked, and $\text{[math]}$ can be lifted to $\text{[math]}$ if and only if $\text{[math]}$ is also marked. Thus $\text{[math]}$ has the right lifting property against the $\text{[math]}$ if and only if its markings are stable under isomorphism, which is the case if and only if $\text{[math]}$ is fibrant.

Proposition 10.

An object of $\text{[math]}$ is fibrant if and only if it has the right lifting property against all of the following morphisms, all of which are trivial cofibrations in $\text{[math]}$ :

The maps $\text{[math]}$ of Proposition 9.
The morphisms of Definition 6.
The maps $\text{[math]}$ , where $\text{[math]}$ is one of $\text{[math]}$ or $\text{[math]}$ .

Proof. All three types of maps are injective on objects and hence cofibrations in $\text{[math]}$ and $\text{[math]}$ . By Proposition 9, the maps $\text{[math]}$ are trivial cofibrations of lcc-marked categories and hence also trivial cofibrations in $\text{[math]}$ .

By Proposition 7, the fibrant objects of $\text{[math]}$ are precisely the lcc categories. If $\text{[math]}$ is an lcc category and $\text{[math]}$ is a morphism of type 2 or 3, then

is an equivalence of groupoids and hence induces a bijection of isomorphism classes. It follows by the Yoneda lemma that $\text{[math]}$ is an isomorphism in $\text{[math]}$ , so $\text{[math]}$ is a weak equivalence in $\text{[math]}$ .

On the other hand, let $\text{[math]}$ be a fibrant lcc-marked category with the right lifting property against morphisms of type 2 and the morphisms of type 3. The right lifting property against $\text{[math]}$ and $\text{[math]}$ implies that $\text{[math]}$ -marked diagrams commute, that every cospan can be completed to a $\text{[math]}$ -marked square, and that every square over a cospan factors via every $\text{[math]}$ -marked square over the cospan. Uniqueness of factorizations follows from the right lifting property against the map of type 3 corresponding to pullbacks. Thus $\text{[math]}$ has pullbacks, and the argument for terminal objects and dependent products is similar.

Definition 11.

A strict lcc category is an algebraically fibrant object of $\text{[math]}$ with respect to the set $\text{[math]}$ consisting of the morphisms of types 1 -- 3 of Proposition 10. The category of strict lcc categories is denoted by $\text{[math]}$ .

Remark 12.

The objects in the image of the forgetful functor $\text{[math]}$ are the fibrant lcc sketches, i.e. lcc categories. To endow an lcc category with the structure of a strict lcc category, we need to choose canonical lifts $\text{[math]}$ against the morphisms $\text{[math]}$ . Because the lifts against all other morphisms are uniquely determined, only the choices for $\text{[math]}$ and $\text{[math]}$ are relevant for this. Thus a strict lcc category is an lcc category with assigned terminal object, pullback squares and dependent products (including the evaluation maps of dependent products). A strict lcc functor is then an lcc functor that preserves these canonical choices of universal objects not just up to isomorphism but up to equality.

The slice category $\text{[math]}$ over an object $\text{[math]}$ of an lcc category $\text{[math]}$ is lcc again. A morphism $\text{[math]}$ in $\text{[math]}$ induces by pullback an lcc functor $\text{[math]}$ , and there exist functors $\text{[math]}$ and adjunctions $\text{[math]}$ . These data depend on choices of pullback squares and dependent products, and hence they are preserved by lcc functors only up to isomorphism.

For strict lcc categories $\text{[math]}$ , however, these functors can be constructed using canonical lcc structure, i.e. using the lifts $\text{[math]}$ for various $\text{[math]}$ , and this choice is preserved by strict lcc functors.

Proposition 13.

Let $\text{[math]}$ be a strict lcc category, and let $\text{[math]}$ . Then there is a strict lcc category $\text{[math]}$ whose underlying category is the slice $\text{[math]}$ .

If $\text{[math]}$ is a morphism in $\text{[math]}$ , then there is a canonical choice of pullback functor $\text{[math]}$ which is lcc (but not necessarily strict) and canonical left and right adjoints

These data are natural in $\text{[math]}$ . Thus if $\text{[math]}$ is strict lcc, then the evident functor $\text{[math]}$ is strict lcc, and the following squares in $\text{[math]}$ respectively $\text{[math]}$ commute:

(Here application of $\text{[math]}$ and $\text{[math]}$ has been omitted; the left square is valued in $\text{[math]}$ , and the two right squares are valued in $\text{[math]}$ .) $\text{[math]}$ and $\text{[math]}$ commute with taking transposes along the involved adjunctions.

Proof. We take as canonical terminal object of $\text{[math]}$ the identity morphism $\text{[math]}$ on $\text{[math]}$ . Canonical pullbacks in $\text{[math]}$ are computed as canonical pullbacks of the underlying diagram in $\text{[math]}$ , and similarly for dependent products.

The canonical pullback and dependent product functors $\text{[math]}$ are defined using canonical pullbacks and dependent products, and dependent sum functors $\text{[math]}$ are computed by composition with $\text{[math]}$ . Units and counits of the adjunctions are given by the evaluation maps of canonical dependent products and the projections of canonical pullbacks.

Because these data are defined in terms of canonical lcc structure on $\text{[math]}$ , they are preserved by strict lcc functors.

The context morphisms in our categories with families (cwfs) [11] will usually be defined as functors of categories in the opposite directions. Cwfs are categories equipped with contravariant functors to $\text{[math]}$ , the category of families of sets. To avoid having to dualize twice, we thus introduce the following notion.

Definition 14.

A covariant cwf is a category $\text{[math]}$ equipped with a (covariant) functor $\text{[math]}$ .

The intuition for a context morphism $\text{[math]}$ in a cwf is an assignment of terms in $\text{[math]}$ to the variables occurring in $\text{[math]}$ . Dually, a morphism $\text{[math]}$ in a covariant cwf should thus be thought of as a mapping of the variables in $\text{[math]}$ to terms in context $\text{[math]}$ , or more conceptually as an interpretation of the mathematics internal to $\text{[math]}$ into the mathematics internal to $\text{[math]}$ .

Apart from our use of covariant cwfs, we adhere to standard terminology with the obvious dualization. For example, an empty context in a covariant cwf is an initial (instead of terminal) object in the underlying category.

To distinguish type and term formers in (covariant) cwfs from the corresponding categorical structure, the type theoretic notions are typeset in bold where confusion is possible. Thus $\text{[math]}$ denotes a dependent product type whereas $\text{[math]}$ denotes application of a dependent product functor $\text{[math]}$ to an object $\text{[math]}$ .

Definition 15.

The covariant cwf structure on $\text{[math]}$ is given by $\text{[math]}$ and $\text{[math]}$ , where $\text{[math]}$ denotes the canonical terminal object of $\text{[math]}$ .

Proposition 16.

The covariant cwf $\text{[math]}$ has an empty context and context extensions, and it supports finite product and extensional equality types.

Proof. It follows from Theorem 18 below that $\text{[math]}$ is cocomplete and that $\text{[math]}$ has a left adjoint $\text{[math]}$ . In particular, there exists an initial strict lcc category, i.e. an empty context in $\text{[math]}$ .

Let $\text{[math]}$ . The context extension $\text{[math]}$ is constructed as pushout

where $\text{[math]}$ denotes a minimally marked lcc sketch with two objects and $\text{[math]}$ is the minimally marked free-standing arrow. The vertical morphism on the left is induced by mapping $\text{[math]}$ to $\text{[math]}$ (the canonical terminal object of $\text{[math]}$ ) and $\text{[math]}$ to $\text{[math]}$ , and the top morphism is the evident inclusion. The variable $\text{[math]}$ is given by the image of $\text{[math]}$ in $\text{[math]}$ .

Unit types $\text{[math]}$ are given by the canonical terminal objects of strict lcc categories $\text{[math]}$ . Binary product types $\text{[math]}$ are given by canonical pullbacks $\text{[math]}$ over the canonical terminal object $\text{[math]}$ in $\text{[math]}$ . Finally, equality types $\text{[math]}$ are constructed as canonical pullbacks

in $\text{[math]}$ , i.e. as equalizers of $\text{[math]}$ and $\text{[math]}$ .

Because these type constructors (and evident term formers) are defined from canonical lcc structure, they are stable under substitution.

Remark 17.

Unfortunately, $\text{[math]}$ does not support dependent product or dependent sum types in a similarly obvious way. The introduction rule for dependent types is

To interpret it, we would like to apply the dependent product functor $\text{[math]}$ to $\text{[math]}$ .

We thus need a functor $\text{[math]}$ to obtain an object of the slice category, and the construction of such a functor appears to be not generally possible. Note that the most natural strategy for constructing this functor using the universal property of $\text{[math]}$ does not work: For this we would note that the pullback functor $\text{[math]}$ is lcc, and that the diagonal $\text{[math]}$ is a morphism $\text{[math]}$ in $\text{[math]}$ , and then try to obtain $\text{[math]}$ . The flaw in this argument is that $\text{[math]}$ , while lcc, is not strict, and the universal property of $\text{[math]}$ only applies to strict lcc functors. A solution to this problem is presented in Section 4.

We conclude the section with a justification for why we have not gone astray so far: The initial claim was that our interpretation of type theory would be valued in the category of lcc categories, but $\text{[math]}$ is neither 1-categorically nor bicategorically equivalent to the category $\text{[math]}$ of fibrant lcc sketches. Indeed, not every non-strict lcc functor of strict lcc categories is isomorphic to a strict lcc functor. Nevertheless, $\text{[math]}$ has model category structure that presents the same higher category of lcc categories by the following theorem:

Theorem 18 ([18] Proposition 2.4, [6] Theorem 19).

Let $\text{[math]}$ be a combinatorial model category, and let $\text{[math]}$ be a set of trivial cofibrations such that objects with the right lifting property against $\text{[math]}$ are fibrant. Then $\text{[math]}$ is monadic with left adjoint $\text{[math]}$ , and $\text{[math]}$ is a locally presentable category. The model structure of $\text{[math]}$ can be transferred along the adjunction $\text{[math]}$ to $\text{[math]}$ , endowing $\text{[math]}$ with the structure of a combinatorial model category. $\text{[math]}$ is a Quillen equivalence, and the unit $\text{[math]}$ is a trivial cofibration for all $\text{[math]}$ .

Theorem 18 appears in [18] with the additional assumption that all cofibrations in $\text{[math]}$ are monomorphisms. This assumption is lifted in [6], but there $\text{[math]}$ is a set of generating trivial cofibrations, which is a slightly stronger condition than the one stated in the theorem. However, the proof in [6] works without change in the more general setting.

That the model structure of $\text{[math]}$ is obtained by transfer from that of $\text{[math]}$ means that $\text{[math]}$ reflects fibrations and weak equivalences.

Lemma 19.

Let $\text{[math]}$ and $\text{[math]}$ be as in Theorem 18, and suppose furthermore that $\text{[math]}$ is a model $\text{[math]}$ -category. Then $\text{[math]}$ has the structure of a model $\text{[math]}$ -category, and the adjunction $\text{[math]}$ lifts to a Quillen $\text{[math]}$ -adjunction.

Proof. Let $\text{[math]}$ and $\text{[math]}$ be algebraically fibrant objects. We define the mapping groupoid $\text{[math]}$ to be the full subgroupoid of $\text{[math]}$ whose objects are the maps of algebraically fibrant objects $\text{[math]}$ .

Because $\text{[math]}$ is generated under colimits by the free-standing isomorphism $\text{[math]}$ , it will follow from the existence of powers $\text{[math]}$ that $\text{[math]}$ is complete as a $\text{[math]}$ -category. As we will later show that $\text{[math]}$ is a right adjoint, the powers in $\text{[math]}$ must be constructed such that they commute with $\text{[math]}$ , i.e. $\text{[math]}$ .

Let $\text{[math]}$ be in $\text{[math]}$ and let $\text{[math]}$ . The canonical lift $\text{[math]}$ is constructed as follows: $\text{[math]}$ corresponds to a map $\text{[math]}$ , i.e. an isomorpism of maps $\text{[math]}$ . Its source and target are morphisms $\text{[math]}$ , for which we obtain canonical lifts $\text{[math]}$ using the canonical lifts of $\text{[math]}$ . Because $\text{[math]}$ is fibrant and $\text{[math]}$ is a trivial cofibration, the map $\text{[math]}$ is a trivial fibration and in particular an equivalence. It follows that $\text{[math]}$ can be lifted uniquely to an isomorphism of $\text{[math]}$ with $\text{[math]}$ , and we take $\text{[math]}$ as this isomorphism's transpose.

From uniqueness of the lift defining $\text{[math]}$ , it follows that a map $\text{[math]}$ preserves canonical lifts if and only if the two maps

given by evaluation at the endpoints $\text{[math]}$ of the isomorphism $\text{[math]}$ preserve canonical lifts. Thus the canonical isomorphism

restricts to an isomorphism

It follows by [1, theorem 4.85] and the preservation of powers by $\text{[math]}$ that the 1-categorical adjunction $\text{[math]}$ is groupoid enriched. It is proved in [18] that $\text{[math]}$ , when considered as a functor of ordinary categories, is monadic using Beck's monadicity theorem. The only additional assumption for the enriched version of Beck's theorem [10, theorem II.2.1] we have to check is that the coequalizer of a $\text{[math]}$ -split pair of morphisms as constructed in [18] is a colimit also in the enriched sense. This follows immediately from the fact that $\text{[math]}$ is locally full and faithful. $\text{[math]}$ is $\text{[math]}$ -monadic and accessible, so $\text{[math]}$ is $\text{[math]}$ -cocomplete by [5, theorem 3.8].

It remains to show that $\text{[math]}$ is groupoid enriched also in the model categorical sense. For this it suffices to note that $\text{[math]}$ preserves (weighted) limits and that $\text{[math]}$ preserves and reflects fibrations and weak equivalences, so that the map

induced by a cofibration of groupoids $\text{[math]}$ and a fibration $\text{[math]}$ in $\text{[math]}$ is a fibration and a weak equivalence if either $\text{[math]}$ or $\text{[math]}$ is a weak equivalence.

Remark 20.

[14] defines model category structure on $\text{[math]}$ , the category of strict algebras and their strict morphisms for a 2-monad $\text{[math]}$ on a model $\text{[math]}$ -category. If we choose for $\text{[math]}$ the monad on $\text{[math]}$ assigning to every category the free lcc category generated by it, then $\text{[math]}$ is $\text{[math]}$ -equivalent to $\text{[math]}$ , so it is natural ask whether their model category structures agree.

The model category structure on $\text{[math]}$ is defined by transfer from $\text{[math]}$ , i.e. such that the forgetful functor $\text{[math]}$ reflects fibrations and weak equivalences. The same is true for $\text{[math]}$ , and this functor is valued in the fibrant objects of $\text{[math]}$ . The restriction of the functor $\text{[math]}$ to fibrant objects reflects weak equivalences and trivial fibrations because equivalences of categories preserve and reflect universal objects that exist in domain and codomain. Thus $\text{[math]}$ and $\text{[math]}$ have the same sets of weak equivalences and trivial fibrations, hence their model category structures coincide.

4 Algebraically cofibrant strict lcc categories

As noted in Remark 17, to interpret dependent sum and dependent product types in $\text{[math]}$ , we would need to relate context extensions $\text{[math]}$ to slice categories $\text{[math]}$ . In this section we discuss how this problem can be circumvented by considering yet another Quillen equivalent model category: The category of algebraically cofibrant strict lcc categories.

The slice category $\text{[math]}$ of an lcc category $\text{[math]}$ is bifreely generated by (any choice of) the pullback functor $\text{[math]}$ and the diagonal $\text{[math]}$ , viewed as a morphism $\text{[math]}$ in $\text{[math]}$ : Given a pair of lcc functor $\text{[math]}$ and morphism $\text{[math]}$ in $\text{[math]}$ , there is an lcc functor $\text{[math]}$ that commutes with $\text{[math]}$ and $\text{[math]}$ up to a natural isomorphism under which $\text{[math]}$ corresponds to $\text{[math]}$ , and every other lcc functor with this property is uniquely isomorphic to $\text{[math]}$ .

Phrased in terms of model category theory, this biuniversal property amounts to asserting that the square

is a homotopy pushout square in $\text{[math]}$ . Here $\text{[math]}$ denotes the discrete category with two objects and no markings, from which $\text{[math]}$ is obtained by adjoining a single morphism $\text{[math]}$ . The left vertical map $\text{[math]}$ maps $\text{[math]}$ to some terminal object and $\text{[math]}$ to $\text{[math]}$ , and the right vertical map maps $\text{[math]}$ to the diagonal $\text{[math]}$ in $\text{[math]}$ .

Recall from Proposition 16 that a context extension $\text{[math]}$ in $\text{[math]}$ is defined by the 1-categorical pushout square

(3)

Because $\text{[math]}$ is a Quillen equivalence, we should thus expect to find weak equivalences relating $\text{[math]}$ to $\text{[math]}$ if the pushout (3) is also a homotopy pushout.

By [16, Proposition A.2.4.4], this is the case if $\text{[math]}$ , $\text{[math]}$ and $\text{[math]}$ are cofibrant, and the map $\text{[math]}$ is a cofibration. The cofibrations of $\text{[math]}$ are the maps which are injective on objects. It follows that $\text{[math]}$ and $\text{[math]}$ are cofibrant lcc sketches, and that the inclusion of the former into the latter is a cofibration. $\text{[math]}$ is a left Quillen functor and hence preserves cofibrations. Thus the pushout (3) is a homotopy pushout if $\text{[math]}$ is cofibrant.

Note that components of the counit $\text{[math]}$ are cofibrant replacements: Every lcc sketch is cofibrant in $\text{[math]}$ , every strict lcc category is fibrant in $\text{[math]}$ , and $\text{[math]}$ is a Quillen equivalence. It follows that a strict lcc category $\text{[math]}$ is cofibrant if and only if the counit $\text{[math]}$ is a retraction, say with section $\text{[math]}$ .

And indeed, this section can be used to strictify the pullback functor. We have $\text{[math]}$ , which induces a strict lcc functor $\text{[math]}$ . Now let

which is naturally isomorphic to $\text{[math]}$ . Adjusting the domain and codomain of the diagonal $\text{[math]}$ suitably to match $\text{[math]}$ , we thus obtain the desired comparison functor $\text{[math]}$ .

At first we might thus attempt to restrict the category of contexts to the cofibrant strict lcc categories $\text{[math]}$ , for which sections $\text{[math]}$ exist. Indeed, cofibrant objects are stable under pushouts along cofibrations, so the context extension $\text{[math]}$ will be cofibrant again if $\text{[math]}$ is cofibrant. The dependent product type $\text{[math]}$ would be defined by application of

to $\text{[math]}$ . Unfortunately, the definition of the comparison functor $\text{[math]}$ required a choice of section $\text{[math]}$ , and this choice will not generally be compatible with strict lcc functors $\text{[math]}$ . The dependent products defined as above will thus not be stable under substitution.

To solve this issue, we make the section $\text{[math]}$ part of the structure. Similarly to how strict lcc categories have associated structure corresponding to their fibrancy in lcc, we make the section $\text{[math]}$ witnessing the cofibrancy of strict lcc categories part of the data, and require morphisms to preserve it. We thus consider algebraically cofibrant objects, which, dually to algebraically fibrant objects, are defined as coalgebras for a cofibrant replacement comonad. As in the case of algebraically fibrant objects, we are justified in doing so because we obtain an equivalent model category:

Theorem 21 ([7] Lemmas 1.2 and 1.3, Theorems 1.4 and 2.5).

Let $\text{[math]}$ be a combinatorial and model $\text{[math]}$ -category. Then there are arbitrarily large cardinals $\text{[math]}$ such that

$\text{[math]}$ is locally $\text{[math]}$ -presentable;
$\text{[math]}$ is cofibrantly generated with a set of generating cofibrations for which domains and codomains are $\text{[math]}$ -presentable objects;
an object $\text{[math]}$ is $\text{[math]}$ -presentable if and only if the functor $\text{[math]}$ , given by the groupoid enrichment of $\text{[math]}$ , preserves $\text{[math]}$ -filtered colimits.

Let $\text{[math]}$ be any such cardinal. Then there is a cofibrant replacement $\text{[math]}$ -comonad $\text{[math]}$ that preserves $\text{[math]}$ -filtered colimits. Let $\text{[math]}$ be any such comonad and denote its category of coalgebras by $\text{[math]}$ .

Then the forgetful functor $\text{[math]}$ has a left adjoint $\text{[math]}$ . $\text{[math]}$ is a complete and cocomplete $\text{[math]}$ -category, and $\text{[math]}$ is a $\text{[math]}$ -adjunction. The model category structure of $\text{[math]}$ can be transferred along $\text{[math]}$ , making $\text{[math]}$ a model $\text{[math]}$ -category. $\text{[math]}$ is a Quillen equivalence.

For $\text{[math]}$ , the first infinite cardinal $\text{[math]}$ satisfies the three conditions of Theorem 21, and $\text{[math]}$ is a suitable cofibrant replacement comonad.

Definition 22.

The covariant cwf structure on $\text{[math]}$ is defined as the composite

in terms of the covariant cwf structure on $\text{[math]}$ .

We denote by $\text{[math]}$ the unit and by $\text{[math]}$ the counit of the adjunction $\text{[math]}$ .

Lemma 23.

Let $\text{[math]}$ be an $\text{[math]}$ -coalgebra. Then there is a canonical natural isomorphism $\text{[math]}$ of lcc functors which is compatible with morphisms of $\text{[math]}$ -coalgebras.

Proof. It suffices to construct a natural isomorphism

of lcc endofunctors on $\text{[math]}$ for every strict lcc category $\text{[math]}$ , because then

for every coalgebra $\text{[math]}$ .

$\text{[math]}$ is a trivial cofibration, so the map

(4)

is a trivial fibration of groupoids. By one of the triangle identities of units and counits, we have $\text{[math]}$ . Thus both $\text{[math]}$ and $\text{[math]}$ are sent to $\text{[math]}$ under the surjective equivalence (4), and so we can lift the identity natural isomorphism on $\text{[math]}$ to an isomorphism $\text{[math]}$ as above. Since the lift is unique, it is preserved under strict lcc functors in $\text{[math]}$ .

Proposition 24.

The covariant cwf $\text{[math]}$ has an empty context and context extensions, and the forgetful functor $\text{[math]}$ preserves both.

Proof. The model category $\text{[math]}$ has an initial object, i.e. an empty context. Its underlying strict lcc category $\text{[math]}$ is the initial strict lcc category, and the structure map $\text{[math]}$ is the unique strict lcc functor with this signature.

Now let $\text{[math]}$ be an $\text{[math]}$ -coalgebra and $\text{[math]}$ be a type. We must construct coalgebra structure $\text{[math]}$ on the context extension in $\text{[math]}$ such that

commutes, and show that the strict lcc functor $\text{[math]}$ induced by a coalgebra morphism $\text{[math]}$ and a term $\text{[math]}$ is a coalgebra morphism.

Let $\text{[math]}$ be the variable term of the context extension of $\text{[math]}$ by $\text{[math]}$ . Then $\text{[math]}$ is a morphism

in $\text{[math]}$ . $\text{[math]}$ is a terminal object and hence uniquely isomorphic to the canonical terminal object $\text{[math]}$ of $\text{[math]}$ , and $\text{[math]}$ is isomorphic to $\text{[math]}$ via a component of $\text{[math]}$ , where $\text{[math]}$ is the natural isomorphism constructed in Lemma 23. We thus obtain a term $\text{[math]}$ and can define

by the universal property of $\text{[math]}$ . $\text{[math]}$ is compatible with $\text{[math]}$ and $\text{[math]}$ by construction.

Now let $\text{[math]}$ be a coalgebra morphism and let $\text{[math]}$ . We need to show that

commutes. This follows from the universal property of $\text{[math]}$ : The two maps $\text{[math]}$ agree after precomposing $\text{[math]}$ because by assumption $\text{[math]}$ is a coalgebra morphism, and they both map $\text{[math]}$ to the term $\text{[math]}$ obtained from $\text{[math]}$ similarly to $\text{[math]}$ from $\text{[math]}$ because the isomorphism $\text{[math]}$ constructed in Lemma 23 is compatible with coalgebra morphisms.

For $\text{[math]}$ a $\text{[math]}$ -category and $\text{[math]}$ , we denote by $\text{[math]}$ the higher coslice $\text{[math]}$ -category of objects under $\text{[math]}$ . Its objects are morphisms out of $\text{[math]}$ , its morphisms are triangles

in $\text{[math]}$ which commute up to specified isomorphism $\text{[math]}$ , and its 2-cells $\text{[math]}$ are 2-cells $\text{[math]}$ in $\text{[math]}$ such that $\text{[math]}$ .

Definition 25.

Let $\text{[math]}$ be an lcc category and $\text{[math]}$ . A weak context extension of $\text{[math]}$ by $\text{[math]}$ consists of an lcc functor $\text{[math]}$ and a morphism $\text{[math]}$ with $\text{[math]}$ a terminal object in $\text{[math]}$ such that the following biuniversal property holds:

For every lcc category $\text{[math]}$ , lcc functor $\text{[math]}$ and morphism $\text{[math]}$ in $\text{[math]}$ with $\text{[math]}$ terminal, the full subgroupoid of $\text{[math]}$ given by pairs of lcc functor $\text{[math]}$ and natural isomorphism $\text{[math]}$ such that the square

in $\text{[math]}$ commutes is contractible (i.e. equivalent to the terminal groupoid).

Remark 26.

Note that the definition entails that mapping groupoids of lcc functors $\text{[math]}$ under $\text{[math]}$ with $\text{[math]}$ a weak context extension are equivalent to discrete groupoids. Lcc functors $\text{[math]}$ under $\text{[math]}$ are (necessarily uniquely) isomorphic under $\text{[math]}$ if and only if they correspond to the same morphism $\text{[math]}$ in $\text{[math]}$ .

Lemma 27.

Let $\text{[math]}$ be an $\text{[math]}$ -coalgebra and let $\text{[math]}$ be a strict lcc category. Then the full and faithful inclusion of groupoids

(5)

admits a canonical retraction $\text{[math]}$ . There is a natural isomorphism $\text{[math]}$ , exhibiting the retract (5) as an equivalence of groupoids. The retraction $\text{[math]}$ and natural isomorphism $\text{[math]}$ is $\text{[math]}$ -natural in $\text{[math]}$ and $\text{[math]}$ .

Proof. Let $\text{[math]}$ . The transpose of $\text{[math]}$ is a strict lcc functor $\text{[math]}$ such that $\text{[math]}$ . We set $\text{[math]}$ and $\text{[math]}$ for $\text{[math]}$ as in Lemma 23. If $\text{[math]}$ already arises from a strict lcc functor $\text{[math]}$ , then $\text{[math]}$ and hence $\text{[math]}$ . The action of the retraction $\text{[math]}$ on natural isomorphisms $\text{[math]}$ is defined analogously from the $\text{[math]}$ -enrichment of $\text{[math]}$ .

Lemma 28.

Let $\text{[math]}$ be an $\text{[math]}$ -coalgebra. Then $\text{[math]}$ and $\text{[math]}$ form a weak context extension of $\text{[math]}$ by $\text{[math]}$ .

Proof. Let $\text{[math]}$ be an lcc functor and $\text{[math]}$ be a morphism with terminal domain in $\text{[math]}$ . Let $\text{[math]}$ be a strict lcc category such that $\text{[math]}$ . Then by Lemma 27 there is an isomorphism $\text{[math]}$ for some strict lcc functor $\text{[math]}$ . Set $\text{[math]}$ , where $\text{[math]}$ is the unique morphism in $\text{[math]}$ such that

commutes. (Both vertical arrows are isomorphisms.) Now with $\text{[math]}$ we have $\text{[math]}$ .

Let $\text{[math]}$ and $\text{[math]}$ be any other lcc functor over $\text{[math]}$ such that

commutes. We need to show that $\text{[math]}$ and $\text{[math]}$ are uniquely isomorphic under $\text{[math]}$ . Lemma 27 reduces this to the unique existence of an extension of the isomorphism $\text{[math]}$ defined as composite

to an isomorphism $\text{[math]}$ under $\text{[math]}$ . This follows from the construction of $\text{[math]}$ as pushout

and its universal property on 2-cells.

Lemma 29.

Let $\text{[math]}$ be an object of an lcc category $\text{[math]}$ , and let $\text{[math]}$ be any choice of pullback functor. Denote by $\text{[math]}$ the diagonal morphism in $\text{[math]}$ . Then $\text{[math]}$ and $\text{[math]}$ form a weak context extension of $\text{[math]}$ by $\text{[math]}$ .

Proof. Let $\text{[math]}$ be an lcc category, $\text{[math]}$ be an lcc functor and $\text{[math]}$ be a morphism in $\text{[math]}$ with $\text{[math]}$ terminal. We define the induced lcc functor $\text{[math]}$ as composition

where $\text{[math]}$ is given by a choice of pullback functor.

Let $\text{[math]}$ . We denote the composite $\text{[math]}$ by $\text{[math]}$ . Then the two squares

are both pullbacks over the same cospan. Here $\text{[math]}$ denotes the first projection of the product defining the pullback functor $\text{[math]}$ , and $\text{[math]}$ is the projection's domain. (These should not be confused with canonical products in strict lcc categories; $\text{[math]}$ and $\text{[math]}$ are only lcc categories.) $\text{[math]}$ preserves pullbacks, so $\text{[math]}$ is a product of $\text{[math]}$ with $\text{[math]}$ . We obtain natural isomorphisms $\text{[math]}$ relating the two pullbacks for all $\text{[math]}$ .

The diagram

commutes, and in particular the left square commutes. It follows that $\text{[math]}$ is compatible with $\text{[math]}$ and $\text{[math]}$ .

$\text{[math]}$ and $\text{[math]}$ are unique up to unique isomorphism because for every morphism $\text{[math]}$ in $\text{[math]}$ , i.e. object of $\text{[math]}$ , the square

is a pullback square in $\text{[math]}$ .

Lemma 30.

Let $\text{[math]}$ be an $\text{[math]}$ -coalgebra and let $\text{[math]}$ be a type. Then $\text{[math]}$ and $\text{[math]}$ are equivalent objects of the coslice category $\text{[math]}$ . The equivalence $\text{[math]}$ can be constructed naturally in $\text{[math]}$ and $\text{[math]}$ , in the sense that coalgebra morphisms in $\text{[math]}$ preserving $\text{[math]}$ induce natural transformations of diagrams

(6)

Proof. It follows immediately from Lemmas 28 and 29 that $\text{[math]}$ and $\text{[math]}$ are equivalent under $\text{[math]}$ . However, a priori the corresponding diagrams (6) can only be assumed to vary pseudonaturally in $\text{[math]}$ and $\text{[math]}$ , meaning that for example the square

(7)

induced by a coalgebra morphism $\text{[math]}$ would only commute up to isomorphism.

The issue is that Definition 25 only requires that certain mapping groupoids are contractible to a point, but the choice of point is not uniquely determined. To obtain a square (7) that commutes up to equality, we have to explicitly construct a map $\text{[math]}$ (i.e. point of the contractible mapping groupoid) and show that this choice is strictly natural.

The map $\text{[math]}$ over $\text{[math]}$ is determined up to unique isomorphism by compatibility with the (canonical) pullback functor $\text{[math]}$ and the diagonal $\text{[math]}$ . Recall from the proof of Lemma 28 that $\text{[math]}$ and $\text{[math]}$ is a valid choice. $\text{[math]}$ is stable under strict lcc functors, hence by Lemmas 13 and 27, $\text{[math]}$ and $\text{[math]}$ are natural in $\text{[math]}$ -coalgebra morphisms.

As in the proof of Lemma 29, the map in the other direction can be constructed as composite

where $\text{[math]}$ is the canonical pullback along the variable $\text{[math]}$ , and the components of the natural isomorphism $\text{[math]}$ are the unique isomorphisms relating pullback squares

All data involved in the construction are natural in $\text{[math]}$ by Proposition 13, hence so are $\text{[math]}$ and $\text{[math]}$ .

By Remark 26, the natural isomorphisms $\text{[math]}$ and $\text{[math]}$ over $\text{[math]}$ are uniquely determined given their domain and codomain. Their naturality in $\text{[math]}$ and $\text{[math]}$ thus follows from that of $\text{[math]}$ and $\text{[math]}$ .

Lemma 31.

Let $\text{[math]}$ be an $\text{[math]}$ -coalgebra, let $\text{[math]}$ be types in context $\text{[math]}$ and let $\text{[math]}$ be a term. Let $\text{[math]}$ be the morphism in $\text{[math]}$ that corresponds to $\text{[math]}$ under the isomorphism

induced by the equivalence of Lemma 30 and the adjunction $\text{[math]}$ . Then the square

in $\text{[math]}$ commutes up to a unique natural isomorphism that is compatible with $\text{[math]}$ -coalgebra morphisms in $\text{[math]}$ .

Proof. $\text{[math]}$ maps the diagonal of $\text{[math]}$ to the diagonal of $\text{[math]}$ up to the canonical isomorphism $\text{[math]}$ , hence Lemma 28 applies.

Theorem 32.

The cwf $\text{[math]}$ is a model of dependent type theory with finite product, extensional equality, dependent product and dependent sum types.

Proof. $\text{[math]}$ has an empty context and context extensions by Proposition 24. Finite product and equality types are interpreted as in $\text{[math]}$ (see Proposition 16).

Let $\text{[math]}$ and $\text{[math]}$ . Denote by $\text{[math]}$ the functor that is part of the equivalence established in Lemma 30. Then $\text{[math]}$ respectively $\text{[math]}$ are defined by application of the functors

to $\text{[math]}$ .

$\text{[math]}$ being an equivalence and the adjunction $\text{[math]}$ establish an isomorphism

by which we define lambda abstraction $\text{[math]}$ for some term $\text{[math]}$ and the inverse to $\text{[math]}$ (i.e. application of $\text{[math]}$ to the variable $\text{[math]}$ for some term $\text{[math]}$ ).

Now let $\text{[math]}$ and $\text{[math]}$ . The pair term $\text{[math]}$ of type $\text{[math]}$ is defined by the diagram

Here the isomorphism $\text{[math]}$ is a component of the natural isomorphism $\text{[math]}$ constructed in Lemma 31, instantiated for $\text{[math]}$ . Given just $\text{[math]}$ we recover $\text{[math]}$ by composition with $\text{[math]}$ , and then $\text{[math]}$ as composition

These constructions establish an isomorphism of terms $\text{[math]}$ and $\text{[math]}$ with terms $\text{[math]}$ , so the $\text{[math]}$ and $\text{[math]}$ laws hold.

The functors $\text{[math]}$ and the involved adjunctions are preserved by $\text{[math]}$ -coalgebra morphisms (Proposition 13, Lemmas 30 and 31 ), so our type theoretic structure is stable under substitution.

5 Cwf structure on individual lcc categories

In this section we show that the covariant cwf structure on $\text{[math]}$ that we established in Theorem 32 can be used as a coherence method to rectify Seely's interpretation in a given lcc category $\text{[math]}$ .

Lemma 33.

Let $\text{[math]}$ be an $\text{[math]}$ -coalgebra. Then the following categories are equivalent:

$\text{[math]}$ ;
the category of isomorphism classes of morphisms in the restriction of the higher coslice category $\text{[math]}$ to slice categories $\text{[math]}$ ;
the category of isomorphism classes of morphisms in the restriction of the higher coslice category $\text{[math]}$ to context extensions $\text{[math]}$ ;
the full subcategory of the 1-categorical coslice category $\text{[math]}$ given by the context extensions $\text{[math]}$ .

Proof. As noted in Remark 26, the higher categories in 2 and 3 are already locally equivalent to discrete groupoids and hence biequivalent to their categories of isomorphism classes.

The functor from 1 to 2 is given by assigning to a morphism $\text{[math]}$ in $\text{[math]}$ the isomorphism class of the pullback functor $\text{[math]}$ . The isomorphism class of an lcc functor $\text{[math]}$ over $\text{[math]}$ is uniquely determined by the morphism

which in turn corresponds to a morphism $\text{[math]}$ , and then $\text{[math]}$ .

The categories 2 and 3 are equivalent because they are both categories of weak context extensions (Lemmas 28 and 29). Finally, the inclusion of 4 into 3 is an equivalence by the Lemma 27. Note that every strict lcc functor $\text{[math]}$ commuting (up to equality) with the projections $\text{[math]}$ and $\text{[math]}$ is compatible with the coalgebra structures of $\text{[math]}$ and $\text{[math]}$ .

Definition 34.

Let $\text{[math]}$ be a covariant cwf and let $\text{[math]}$ be a context of $\text{[math]}$ . Then the coslice covariant cwf $\text{[math]}$ has as underlying category the (1-categorical) coslice category under $\text{[math]}$ , and its types and terms are given by the composite functor $\text{[math]}$ .

Lemma 35.

Let $\text{[math]}$ be a covariant cwf and let $\text{[math]}$ be a context of $\text{[math]}$ . Then the coslice covariant cwf $\text{[math]}$ has an initial context. If $\text{[math]}$ has context extensions, then $\text{[math]}$ has context extensions, and they are preserved by $\text{[math]}$ . If $\text{[math]}$ supports any of finite product, extensional equality, dependent product or dependent sum types, then so does $\text{[math]}$ , and they are preserved by $\text{[math]}$

Definition 36.

Let $\text{[math]}$ be a covariant cwf with an empty context and context extensions. The core of $\text{[math]}$ is a covariant cwf on the least full subcategory $\text{[math]}$ that contains the empty context and is closed under context extensions, with types and terms given by $\text{[math]}$ .

Lemma 37.

Let $\text{[math]}$ be a covariant cwf with an empty context and context extension. If $\text{[math]}$ supports any of finite product types, extensional equality types, dependent product or dependent sums, then so does $\text{[math]}$ , and they are preserved by the inclusion $\text{[math]}$ .

If $\text{[math]}$ supports unit and dependent sum types, then $\text{[math]}$ is democratic, i.e. every context is isomorphic to a context obtained from the empty context by a single context extension [8].

Theorem 38.

Let $\text{[math]}$ be an $\text{[math]}$ -coalgebra. Then the underlying category of $\text{[math]}$ is equivalent to $\text{[math]}$ . In particular, every lcc category is equivalent to a cwf that has an empty context and context extensions, and that supports finite product, extensional equality, dependent sum and dependent product types.

Proof. $\text{[math]}$ is a covariant cwf supporting all relevant type constructors by Lemmas 35 and 37. It is democratic and hence equivalent to category 4 of lemma 33.

Given an arbitrary lcc category $\text{[math]}$ , we set $\text{[math]}$ and define coalgebra structure by $\text{[math]}$ . Then $\text{[math]}$ is equivalent to both $\text{[math]}$ and a cwf supporting the relevant type constructors.

6 Conclusion

We have shown that the category of lcc categories is a model of extensional dependent type theory. Previously only individual lcc categories were considered as targets of interpretations. As in these previous interpretations, we have had to deal with the issue of coherence: Lcc functors (and pullback functors in particular) preserve lcc structure only up to isomorphism, whereas substitution in type theory commutes with type and term formers up to equality.

Our novel solution to the coherence problem relies on working globally, on all lcc categories at once. In contrast to some individual lcc categories, the higher category of all lcc categories is locally presentable. This allows the use of model category theory to construct a presentation of this higher category in terms of a 1-category that admits an interpretation of type theory.

While we have only studied an interpretation of a type theory with dependent sum and dependent product, extensional equality and finite product types, it is straightforward to adapt the techniques of this paper to type theories with other type constructors. For example, a dependent type theory with a type of natural numbers can be interpreted in the category of lcc categories with objects of natural numbers. Alternatively, we can add finite coproduct, quotient and list types but omit dependent products, and obtain an interpretation in the category of arithmetic universes [17, 21].

I would expect there to be a general theorem by which one can obtain a type theory and its interpretation in the category of algebras for every (higher) monad $\text{[math]}$ on $\text{[math]}$ (with the algebras of $\text{[math]}$ perhaps subject to being finitely complete and stable under slicing). Such a theorem, however, is beyond the scope of the present paper.

Bibliography

Basic concepts of enriched category theory. London Mathematical Society Lecture Note Series, 64, 1982.
Model category of marked objects. 2016.
Enriched model categories and presheaf categories. New York J. of Mathematics, 26:37–91, 2020.
D. W. Anderson. Fibrations and geometric realizations. Bulletin of the American Mathematical Society, 84(5):765–788, 1978.
Robert Blackwell, Gregory Maxwell Kelly and A. John Power. Two-dimensional monad theory. Journal of pure and applied algebra, 59(1):1–41, 1989.
John Bourke. Equipping weak equivalences with algebraic structure. Mathematische Zeitschrift, 2019.
Michael Ching and Emily Riehl. Coalgebraic models for combinatorial model categories. Homology, Homotopy and Applications, 16(2):171–184, 2014.
Pierre Clairambault and Peter Dybjer. The biequivalence of locally cartesian closed categories and Martin-Löf type theories. International Conference on Typed Lambda Calculi and Applications, pages 91–106, 2011.
Pierre-Louis Curien. Substitution up to Isomorphism. Diagrammes, 23:43–66, 1990.
Eduardo J. Dubuc. Kan extensions in enriched category theory. 1970.
Peter Dybjer. Internal type theory. International Workshop on Types for Proofs and Programs, pages 120–134, 1995.
Philip S. Hirschhorn. Model categories and their localizations. 2003.
Martin Hofmann. On the interpretation of type theory in locally cartesian closed categories. International Workshop on Computer Science Logic, pages 427–441, 1994.
Stephen Lack. Homotopy-theoretic aspects of 2-monads. Journal of Homotopy and Related Structures, 2(2):229–260, 2007.
Peter LeFanu Lumsdaine and Michael A Warren. The local universes model: an overlooked coherence construction for dependent type theories. ACM Transactions on Computational Logic (TOCL), 16(3):1–31, 2015.
Jacob Lurie. Higher topos theory. 2009.
Maria Emilia Maietti. Joyal's arithmetic universe as list-arithmetic pretopos. Theory \& Applications of Categories, 24:39–83, 2010.
Thomas Nikolaus. Algebraic models for higher categories. Indagationes Mathematicae, 21(1-2):52–75, 2011.
Robert A. G. Seely. Locally cartesian closed categories and type theory. Mathematical proceedings of the Cambridge philosophical society, 95(1):33–48, 1984.
Steven Vickers. Locales and toposes as spaces. Handbook of spatial logics, pages 429–496, 2007.
Steven Vickers. Sketches for arithmetic universes. Journal of Logic and Analysis, 2016.