# Locally presentable initial-algebra semantics for (multimodal) dependent type theories

André Hirschowitz, Tom Hirschowitz, Ambroise Lafont

► To cite this version:

André Hirschowitz, Tom Hirschowitz, Ambroise Lafont. Locally presentable initial-algebra semantics for (multimodal) dependent type theories. 2025. hal-05535887

HAL Id: hal-05535887

https://hal.science/hal-05535887v1

Preprint submitted on 4 Mar 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
Locally presentable initial-algebra semantics for
(multimodal) dependent type theories

André Hirschowitz¹[0000-0003-2523-1481], Tom Hirschowitz²[0000-0002-7220-4067],
and Ambroise Lafont³[0000-0002-9299-641X]

¹Univ. Côte d'Azur,
CNRS, LJAD,
Nice, France

²Univ. Savoie Mont
Blanc, CNRS, LAMA,
73000 Chambéry, France

³École Polytechnique
Palaiseau, France

**Abstract.** We propose a new approach to initial-algebra semantics for dependent type theories in locally presentable categories. Concretely, we list a handful of fundamental constructions (most of them well known) of locally presentable categories, right adjoint functors between them, and natural transformations between those. We then show how to compose these fundamental contructions in order to recover categories of models for dependent type theories, including Gratzer et al.'s multimodal type theory, as well as Uemura's second-order generalised algebraic theories.

# 1 Introduction

## 1.1 Motivation

Cartmell [8] introduced *generalised algebraic theories* (GATs) as a device for presenting dependent type theories and their categories of models, in the spirit of *initial-algebra semantics* [17,16]: each GAT generates a category of “models”, and the presented type theory is implicitly defined as “the” initial object therein.

Furthermore, Cartmell showed that such categories of models are locally presentable [15,2,28], and conversely that any locally presentable category is presented by some GAT.

After Cartmell, one of the main reasons for continuing the research was that GATs are rather low-level, thus making it tedious to present even mildly complex type theories. Notably, dependent type theories always come with some notion of capture-avoiding substitution, which GATs make no attempt at automating. E.g., specifying a type constructor like dependent product requires many components: the type and term constructors (in any context), the eliminator with associated reduction rules or equations, as well as equations stating that these operations are compatible with substitution.

Recently, a few approaches have managed to improve the situation, in two complementary ways.

- First, they build substitution into operation arities [34,19,10,13]. E.g., the dependent product type constructor may be defined as a mere operation of arity $(ty \to ty) \to ty$ - its behaviour w.r.t. substitution follows.
- Moreover, some of them handle what Coraglia and Di Liberti call *extensional type constructors* [10, Section 3.7]. These are defined in a very compact way by requiring a well-chosen pair of (generally non-parallel) morphisms to be completed into a pullback square, as, e.g., in Fig. 2(left) below. Features that may be specified in this way include extensional identity types, dependent products, and dependent sums.

Built-in substitution and extensional type constructors significantly simplify the task of specifying a type theory.

## 1.2 Contribution

In this paper, we present a new approach to initial-algebra semantics for dependent type theories, which features built-in substitution and extensional type constructors.

A surprising feature is that our approach mostly relies on standard results from locally presentable category theory.

More specifically, we show that the categories of models of a few “typical” dependent type theories may be reconstructed from first principles using only a handful of standard 2-categorical constructions, under which locally presentable categories are (mostly) known to be closed in **CAT**, the 2-category of locally small categories.

We demonstrate the expressiveness of our approach by (1) exhibiting a reconstruction of Gratzer et al.'s [18] multimodal type theory and (2) interpreting SOGATs in our framework. Multimodal type theory is a typical example that SOGATs cannot handle, so (1) shows that our framework is more expressive.

## 1.3 Related work

Let us compare our approach with already mentioned high-level ones [34, 19, 10, 13]. A first difference is that they do *biinitial-algebra semantics*, not initial-algebra semantics. Indeed, in all of these approaches, the models of any signature form a 2-category. Accordingly, the specified dependent type theory is a biinitial object. This is a refinement of initial objects, in which the *category* of morphisms from the biinitial object to any object is *equivalent* to 1, as opposed to isomorphic.

Kaposi and Xie [22] recently provided a translation of Uemura's [34] SOGATs into GATs, hence indirectly equipped SOGATs with proper initial-algebra semantics. Our §4 may be viewed as an alternative route to the same goal, which avoids resorting to GATs.

A further difference between our approach and other high-level ones is that, in all of them, each signature gives rise to a *theory*, i.e., a somed kind of structured category modelling the syntactic constructions inherent in dependent type theory, which is then used to construct the category of models. These are *categories with representable maps* in Uemura [34], locally cartesian closed categories in Gratzer and Sterling [19], and lex 2-categories in Di Liberti et al. [10,13]. This is
in fact also true in Cartmell’s work, theories being his *contextual categories* [8].
Our approach avoids the need for a notion of theory altogether.

In less closely related work, let us mention the recent work by Bourke and
Garner [7] and the references therein, which also contains general constructions
of locally presentable categories. To our knowledge, such approaches have not
been applied to specifying dependent type theories. Notably, they do not feature
built-in substitution or extensional type constructors.

Finally, we drew some initial inspiration from Altenkirch et al. [1].

**1.4 Overview**

Before diving into technical details, let us present the big picture. We first sketch
our approach to constructing categories of models for dependent type theories,
and then briefly touch upon the issue of local presentability.

**Constructing categories of models for dependent type theories** A core notion for models of dependent type theories is Awodey’s category of natural models [3,34]. A natural model consists of a “base” category $\mathbb{C}$, two discrete fibrations $\pi^{ty}: ty \to \mathbb{C}$ and $\pi^{tm}: tm \to \mathbb{C}$ over it, a functor $proj: tm \to ty$ over $\mathbb{C}$ as on the right, together with a right adjoint $var \vdash proj$ (not necessarily over $\mathbb{C}$).

<figure><img src="image_2.png" /></figure>

*Remark 1.* We can additionally require the existence of a terminal object in $\mathbb{C}$, thought of as the empty context. We deal with it in Example 2.

Let us sketch our construction of the category of natural models. We will
later show that all the constructions ensure local presentability.

(a) We first construct the category $\mathbf{DFib}_v^2$ whose objects consist of a small category $\mathbb{C}$, together with discrete fibrations $\pi^{ty}: ty \to \mathbb{C}$ and $\pi^{tm}: tm \to \mathbb{C}$ on it, and a functor $proj: tm \to ty$ over $\mathbb{C}$, as above right.

(b) This category admits a forgetful functor $dom^2: \mathbf{DFib}_v^2 \to \mathbf{Cat}^2$, the category of morphisms in $\mathbf{Cat}$, mapping any object $(\mathbb{C}, ty, tm, proj)$ to $proj$.

(c) We then construct the category $\mathbf{Cat}^{\text{adj}}$, whose objects are adjunctions between small categories.

(d) This category also admits a forgetful functor to $\mathbf{Cat}^2$, which maps any ad-
junction to the left adjoint.

(e) Finally, we define **NatMod** as the pullback below left. An object thus consists

<figure><img src="image_3.png" /></figure>

<figure><img src="image_4.png" /><figcaption>**Fig. 1.** Example constructions of categories of models
of an object $(\mathbb{C}, ty, tm, proj) \in \mathbf{DFib}_v^2$, together with a right adjoint to $proj$, as
desired.</figcaption></figure>
Now that we have constructed the category of natural models of dependent type theory, let us sketch how to refine it to account for dependent products. A particularly efficient way of saying that a natural model $(\mathbb{C}, ty, tm, proj, var)$ (with $proj \lhd var$) has dependent products is using extensional type constructors [10, Section 3.7]. This amounts to (1) computing an “arity” object $\mathfrak{P}(proj)$ of $\mathbf{DFib}_{\mathbb{C}}^2$, and then (2) requiring the existence of a morphism $(\lambda, \Pi) : \mathfrak{P}(proj) \to proj$ making the square below left a pullback [34, §3.3]. The endofunctor $\mathfrak{P}$ is

<figure><img src="image_5.png" /><figcaption>**Fig. 2.** Extensional type constructor for dependent product defined as the composite above right, where</figcaption></figure>

- $ext$, thought of as context extension, is the composite $ty \xrightarrow{var} tm \xrightarrow{\pi^{tm}} \mathbb{C}$,

- $ext^*$ denotes pullback along it, and

- $\pi_i^{ty}$ denotes post-composition with $\pi^{ty} : ty \to \mathbb{C}$.

In order to add such structure to the objects of **NatMod**, we proceed as follows.

(a) We construct a category $\mathbf{DFib}_{\mathbb{V}}^{2+2}$, whose objects consist of a small category $\mathbb{C}$, together with a pair of morphisms of discrete fibrations over $\mathbb{C}$.

(b) We define the functor **NatMod** $\to \mathbf{DFib}_{\mathbb{V}}^{2+2}$ sending any natural model $(\mathbb{C}, ty, tm, proj, var)$ to the pair of solid morphisms in Fig. 2(left) above.

(c) We define the category $\mathbf{DFib}_{\mathbb{V}}^{\square_{\mathrm{lim}}}$, whose objects consist of a small category $\mathbb{C}$, together with a pullback square in $\mathbf{DFib}_{\mathbb{C}}$. We have a forgetful functor $\mathbf{DFib}_{\mathbb{V}}^{\square_{\mathrm{lim}}} \to \mathbf{DFib}_{\mathbb{V}}^{2+2}$.

(d) Finally, we define $\mathbf{NatMod}_{\Pi}$ as the pullback of the last two functors, as in Fig. 1(right). An object is a natural model, together with morphisms $\lambda$ and $\Pi$ making the above square commutative into a pullback, i.e., a model of dependent type theory with dependent products.

**Local presentability** Let us now briefly sketch the tools needed to ensure that the categories of models, constructed as above, are locally presentable.

For this, we rely on a list of mostly known constructions of categories (resp. functors), under which local presentability (resp. right adjointness) are preserved.

The first, obvious construction that we used is the pullback. For this, we exploit the well-known result that the sub-2-category **RLPCAT** $\hookrightarrow \mathbf{CAT}$ spanned by locally presentable categories, right adjoints between them, and all natural transformations, is closed under pullbacks, provided one of the legs is an *isofibration* (see Definition 1 below). In order to apply this to both pullbacks we took above (in **CAT**), we show that (1) the bottom morphism lives in **RLPCAT**, and (2) the right-hand morphism lives in **IRLPCAT**, the sub-2-category of **RLPCAT** spanned by isofibrations.
The first thing to check is of course that all involved categories in Fig. 1 are locally presentable. Roughly, the ingredients for this are the category **DFib** of discrete fibrations, and exponentiation by a small category.

(a) For showing that **DFib** is locally presentable, we observe that it may be defined by orthogonality from **Cat**². It thus suffices to prove that locally presentable categories are closed under taking orthogonality classes and exponentiation by small categories. Both facts are indeed known.

(b) We actually need a 2-categorical generalisation of the exponentiation result for the case of **Cat**<sup>adj</sup> (Fig. 1, left).

(c) Furthermore, we observe that the category **DFib**<sub>v</sub><sup>2</sup> and its variants **DFib**<sub>v</sub><sup>C</sup> for some small category C, may be reconstructed by further pullbacks from **DFib** and categories of the form **Cat**<sup>C</sup> for small C.

(d) Finally, **DFib**<sub>v</sub><sup>lim</sup> is in fact equivalent to **DFib**<sub>v</sub><sup>2T</sup>, where 2<sup>T</sup> denotes the free-standing cospan.

At this point, we know that all categories occurring in Fig. 1 are locally presentable. Now, how about the functors?

For right-hand functors, the result about exponentiation by small (2-)categories extends to exponentiation by (2-)functors *F* between such (2-)categories. Any functor obtained in this way lives in **RLPCAT**, and is an isofibration when *F* is injective on objects. This covers all cases, except **DFib**<sub>v</sub><sup>lim</sup> → **DFib**<sub>v</sub><sup>2+2</sup>. But this one factors as **DFib**<sub>v</sub><sup>lim</sup> → **DFib**<sub>v</sub><sup>2</sup> → **DFib**<sub>v</sub><sup>2+2</sup>. The second factor lives in **IRLPCAT** by the results on pullback and exponentiation, and we prove separately that the first factor does so too.

Let us now turn to bottom functors in Fig. 1. Their construction may be broken down a little by the above-mentioned result on pullbacks: we exhibit an isomorphism **DFib**<sub>v</sub><sup>2+2</sup> ≅ **DFib**<sub>v</sub><sup>2</sup>×**Cat****DFib**<sub>v</sub><sup>2</sup> of categories, which enables us to break down the bottom functor of Fig. 1(right) as a pairing of two functors, one of which is an identity. The other functor maps any natural model (C, *ty*, *tm*, *proj*, *var*) to ℘(*proj*). Recalling Fig. 2(right), this is defined by pulling back *proj* along *ext*, and then post-composing with π<sup>*ty*</sup>.

First of all, pulling back any discrete fibration *p*: *E* → *B* along some functor *f*: *A* → *B* to its base may be viewed as reindexing *p* along *f* for the codomain fibration *cod*: **DFib** → **Cat**. Thus, e.g., reindexing *ty* along *ext* for each (*C*, *ty*, *tm*, *proj*, *var*) is implemented 2-categorically by the cartesian lifting below left.

<figure><img src="image_6.png" /></figure>
Similarly, the “common codomain” functor $cod: \mathbf{DFib}_v^2 \to \mathbf{Cat}$ is a fibration, and mapping each natural model $(C, ty, tm, proj, var)$ to $proj$ forms a functor $U: \mathbf{NatMod} \to \mathbf{DFib}_v^2$, which we may reindex along $ext$ just as before to get $ext^*(proj)$.

This 2-categorical reconstruction of pulling back along $ext$ allows us to prove local presentability. Indeed, Street [30] introduced a notion of fibration internal to a given 2-category. By showing that **RLPCAT** is closed under cartesian lifting in this sense, we are able to prove that $ext^*(U)$ lives in **RLPCAT**.

Postcomposition with $\pi^{ty}$ is subtler. Indeed, postcomposing a discrete fibration $p: E \to B$ with some functor $f: B \to C$ can not in general be viewed as opreindexing for the opfibration $cod: \mathbf{DFib} \to \mathbf{Cat}$. Indeed, opreindexing is rather performed using the comprehensive factorisation system [31]. However, when the functor $f$ is also a discrete fibration, then the composite is again a discrete fibration, hence does indeed provide an opreindexing. In this situation, the opreindexing does lift to **RLPCAT**.

To make this formal, we introduce a notion of opfibration relative to some 2-cell in a 2-category. We then establish a result for transferring opfibration structure in **CAT** to relative opfibration structure in **RLPCAT**. E.g., we may use this transfer result to show that the codomain functor $\mathbf{DFib} \to \mathbf{Cat}$ in **CAT** is an opfibration in **RLPCAT**, relative to natural transformations whose components are discrete fibrations. This allows us to establish that the opcartesian lifting on the right in (1) lives in **RLPCAT**. For each $(C, ty, tm, proj, var)$, the opcartesian lifting returns the composite $\pi^{ty} \circ ext^*(ty)$, as desired. Similarly, the functor $\mathbf{DFib}_v^2 \to \mathbf{Cat}$ is an opfibration relative to natural transformations whose components are discrete fibrations, and the opcartesian lifting of $ext^*(U)$ along $\pi^{ty}$ lives in **RLPCAT**, and acts as desired: it maps $(C, ty, tm, proj, var)$ to $\mathfrak{P}(proj)$.

By cartesian, and then opcartesian lifting, we have reconstructed the crucial functor $\mathbf{NatMod} \to \mathbf{DFib}_v^2$, and showed it lives in **RLPCAT** as desired.

**Applications** After setting up all these constructions, using plain dependent type theory as a running example, we demonstrate their wide applicability by (1) reconstructing the category of models for Gratzer et al.'s multimodal dependent type theory [18], and (2) constructing a category of models for each of Uemura's SOGATs [34].

## 1.5 Plan

We start in §2 by presenting our 2-categorical constructions and stating the results on their preserving local presentability. We then move on to our more substantial applications, multimodal type theory (§3) and SOGATs (§4). Finally, we conclude and give some perspective in §5.

## 1.6 Notation and preliminaries

We assume some good knowledge of basic category theory [27], as well as of notions of Grothendieck (op)fibration and (op)cartesian lifting [20]. (We sometimes
mention some basic enriched [23] and 2-dimensional [26] aspects, but skipping them should not affect reading.)

**Notation 1.** Let **Set** and **Cat** denote the categories of small sets and categories, respectively, while **CAT** denotes the large category of locally small categories. When dealing with 2-categories, we sometimes write $\circ_0$ for composition along objects for disambiguation. Finally, 2 denotes the free-standing arrow.

# 2 Locally presentable toolkit

In this section, we present a detailed version of the constructions mentioned in the introduction as preserving local presentability.

## 2.1 Locally presentable categories

Let us start by recalling the basics of locally presentable categories. We treat the theory like a complete black box, merely giving references to proofs in the literature. Let us recall from the introduction:

**Notation 2.** We denote by **RLPCAT** the 2-category of locally presentable categories, right adjoint functors, and all natural transformations.

Let us record a few basic facts about locally presentable categories, all easy or mentioned in [2].

**Proposition 1.**

1. The categories **Set** and **Cat** are locally presentable.

2. Locally presentable categories are closed in **CAT** under equivalences of categories.

3. Any functor between locally presentable categories is a right adjoint iff it is accessible and continuous.

4. A functor from a locally presentable category to **Set** is a right adjoint iff it is representable.

Here is a harder, yet well known result:

**Proposition 2 ([4, Theorem 2.18])**. The forgetful 2-functor **RLPCAT** $\to$ **CAT** creates products, cotensors, and comma categories (as well as inserters, equifiers, and idempotent splittings).

Finally, we introduce the sub-2-category of **IRLPCAT** and state the announced result about pullbacks.

**Definition 1.** A functor $F: A \to B$ is an isofibration, or is isofibrant iff, for any isomorphism $j: b \to F(a)$, there exists an isomorphism $j': a' \to a$ such that $F(j') = j$. Let **IRLPCAT** denote the wide sub-2-category of **RLPCAT** spanned by right adjoint isofibrations and all natural transformations.
The first, central yet well known result is:

**Proposition 3.** For any pullback in **CAT** as below with $F \in \text{RLPCAT}$ and $G \in \text{IRLPCAT}$, we have $P \in \text{IRLPCAT}$ and $Q \in \text{RLPCAT}$.

<figure><img src="image_7.png" /></figure>

## 2.2 Cotensoring

In this subsection, we sharpen the cotensoring part of Proposition 2. We have two versions of it, one is 2-dimensional but limited<fnref n="1" /> to **Cat**, the other is 1-dimensional but generalised to arbitrary locally presentable categories:

**Proposition 4.**

1. For any small category $V$ and locally presentable category $C$, the category $C^V$ of functors from $V$ to $C$ is locally presentable and is characterised by the following natural isomorphism of categories, for all $D \in \text{RLPCAT}$.

$$ \text{RLPCAT}(D, C^V) \cong \text{CAT}(V, \text{RLPCAT}(D, C)) $$

2. For any small 2-category $\mathcal{K}$, the category $\text{Cat}^{\mathcal{K}}$ of 2-functors from $\mathcal{K}$ to $\text{Cat}$ and 2-natural transformations is locally presentable and is characterised by the following natural isomorphism of categories,

$$ \text{RLPCAT}(C, \text{Cat}^{\mathcal{K}}) \cong |[\mathcal{K}, [C, \text{Cat}]_r]| $$

where $[-, -]$ denotes the hom-2-category of 2-functors, 2-natural transformations, and modifications, the $r$ subscript indicates a restriction to 2-functors whose underlying 1-functor is a right adjoint, and $|-|$ takes the underlying 1-category.

The above characterisations entail the following results (except for the injective-on-objects condition for isofibrations).

**Proposition 5.**

1. For any functor $F: \mathcal{K} \to \mathcal{L}$ between small categories and $G: C \to D$ in **RLPCAT**, the functor $G^F: C^\mathcal{L} \to D^{\mathcal{K}}$ lives in **RLPCAT**. It is furthermore an isofibration when $G$ is, and $F$ is injective on objects.

2. For any 2-functor $F: \mathcal{K} \to \mathcal{L}$ between small 2-categories, the restriction functor $\text{Cat}^{\mathcal{L}} \to \text{Cat}^{\mathcal{K}}$ lives in **RLPCAT**. It is furthermore an isofibration when $F$ is injective on objects.

Let us use this to substantiate some claims from the introduction.

**Notation 3.** Let $\text{adj}$ denote the free-standing adjunction and $\partial_{\text{adj}}: 2 \hookrightarrow \text{adj}$ denote the embedding of the free-standing arrow as the left adjoint.

<footnote n="1">¹ **Cat** could be replaced by any locally presentable category in the **Cat**-enriched sense.</footnote>
*Example 1.* The restriction functor $\partial_{\text{adj}}^* : \text{Cat}^{\text{adj}} \to \text{Cat}^2$ lives in IRLPCAT.

*Example 2.* We reconstruct Awodey’s version [3] of categories with families [14], which are natural models whose base has a terminal object. We start by taking the pullback below left, where the bottom functor maps any $\mathbb{C}$ to the unique functor $\mathbb{C} \to 1$. We then take the pullback below right.

<figure><img src="image_8.png" /></figure>

We further exploit the result for dealing with limiting diagrams.

**Definition 2.** For any small category $\mathbb{C}$, let $\mathbb{C}_{\perp}$ denote the category obtained from $\mathbb{C}$ by freely adding an initial object.

**Lemma 1.** For any categories $\mathbb{C}$ and $\mathbf{E}$, diagrams $\mathbb{C}_{\perp} \to \mathbf{E}$ are in one-to-one correspondence with pairs of a diagram $\mathbb{C} \to \mathbf{E}$ and a cone over it.

**Proposition 6.** For any small $\mathbb{C}$ and locally presentable $\mathbf{E}$, the full subcategory embedding $\mathbf{E}^{(\mathbb{C}_{\perp})_{\text{lim}}} \to \mathbf{E}^{\mathbb{C}_{\perp}}$ spanned by limit cones, lives in IRLPCAT.

*Proof (sketch).* We have $\mathbf{E}^{(\mathbb{C}_{\perp})_{\text{lim}}} \simeq \mathbf{E}^{\mathbb{C}}$, and the embedding $\mathbf{E}^{\mathbb{C}} \to \mathbf{E}^{\mathbb{C}_{\perp}}$ is given by right Kan extension, which is a right adjoint by definition.

*Example 3.* Let $\square = 2 \times 2$ denote the free-standing square, which may be obtained by adding an initial object to the free-standing cospan. Proposition 6 entails that, for any locally presentable $\mathbf{E}$, the composite $\mathbf{E}^{\square_{\text{lim}}} \hookrightarrow \mathbf{E}^{\square} \hookrightarrow \mathbf{E}^{2+2}$ lives in IRLPCAT (see Fig. 1(right)).

## 2.3 Orthogonality

Our next well-known result is about orthogonality.

**Definition 3.** For any class $\mathcal{J}$ of morphisms in a category $\mathbf{E}$, a morphism $p: \mathbf{E} \to \mathbf{B}$ in right orthogonal to $\mathcal{J}$ iff for any $j: \mathbf{X} \to \mathcal{J}$, any commuting square $j \to p$ as below admits a unique lifting $Y \to \mathbf{E}$ making both triangles commute. We let $\mathcal{J}^{\perp}$ denote the full subcategory of $\mathbf{E}^2$ spanned by morphisms that are right orthogonal to $\mathcal{J}$.

<figure><img src="image_9.png" /></figure>

**Proposition 7.** For any set $J$ of morphisms in a locally presentable category $\mathbf{E}$, the embedding $J^{\perp} \hookrightarrow \mathbf{E}^2$ lives in RLPCAT.

Since DFib is precisely $\{\partial_t\}^{\perp}$, where $\partial_t: 1 \to 2$ picks the codomain of the free-standing arrow, this readily entails:

**Proposition 8.** The embedding DFib $\hookrightarrow$ Cat$^2$ lives in RLPCAT.
**Remark 2.** For any set $J$ of morphisms in a locally presentable category, $J^\perp$ is the right class of morphisms of an orthogonal factorisation system. E.g., taking $J = \{\partial_t : 1 \to 2\}$ in **Cat** yields the comprehensive factorisation system [31].

Let us finally use the results of this section to construct categories of the form $\mathbf{DFib}_v^C$, such as $\mathbf{DFib}_v^2$ from §1.4.

**Definition 4.** For any small category $\mathcal{C}$ and set $J$ of morphisms in some locally presentable category $\mathcal{E}$, letting $\mathcal{R} = J^\perp$, we define $\mathcal{R}_v^\mathcal{C}$ as the pullback below left,

<figure><img src="image_10.png" /></figure>

where $\mathbf{E}'$ denotes restriction along the unique functor to 1. Then, for any functor $F: \mathcal{C} \to \mathcal{D}$ in **Cat**, we define $\mathcal{R}_v^F$ by universal property of pullback as above right.

**Remark 3.** Concretely, an object of $\mathcal{R}_v^C$ is a diagram $D: \mathcal{C} \to \mathcal{R}^2$ mapping all objects to morphisms with a common codomain $E \in \mathbf{E}$.

**Proposition 9.** Both diagrams of Definition 4 live in **RLPCAT** (in particular, pullbacks are pullbacks in **RLPCAT**).

**Example 4.** Since $\mathbf{DFib} = \{\partial_t\}^\perp$, any $\mathbf{DFib}_v^C$ is locally presentable, and both projections $\mathbf{Cat} \stackrel{\mathrm{cod}}{\hookrightarrow} \mathbf{DFib}_v^C \hookrightarrow \mathbf{DFib}^C \to (\mathbf{Cat}^2)^C$ live in **RLPCAT**. Taking $\mathcal{C} = 2$ and postcomposing the right-hand projection with $\mathrm{dom}^2 : (\mathbf{Cat}^2)^2 \to \mathbf{Cat}^2$ (using Proposition 5 to show that this lives in **RLPCAT**), we get the bottom morphism of Fig. 1(left).

Combining this with Example 1 and Proposition 3, we obtain:

**Proposition 10.** The pullback in Fig. 1(left) lives in **RLPCAT**, with both vertical morphisms in **IRLPCAT**.

**Example 5.** It is easy to see that the square on the right is a pullback. The bottom functor of Fig. 1(right) may thus be viewed as the pairing $\langle \mathfrak{P}, id \rangle$: **NatMod** $\to \mathbf{DFib}_v^2 \times \mathbf{DFib}_v^2$, where $\mathfrak{P}$ is the pointwise version of $\mathfrak{P}$, in the sense that it maps any $(\mathcal{C}, ty, tm, proj, \dots)$ to $\mathfrak{P}(proj)$. Since the identity functor lives in **RLPCAT**, this leaves us with the task of proving that $\mathfrak{P}$ does so too.

<figure><img src="image_11.png" /></figure>

Let us conclude this subsection by combining Proposition 9 with limit diagrams in the sense of Proposition 6.
**Definition 5.** For any small category $\mathcal{C}$ and set $J$ of morphisms in some locally presentable category $\mathbf{E}$, letting $\mathcal{R} = J^{\perp}$, we define $\mathcal{R}_{\mathbf{v}}^{(\mathcal{C}_{\perp})_{\text{lim}}}$ and its embedding into $\mathcal{R}_{\mathbf{v}}^{\mathcal{C}_{\perp}}$ as the pullback below.

<figure><img src="image_12.png" /></figure>

**Proposition 11.** The whole square of Definition 5 lives in **RLPCAT**, with all marked monos in **IRLPCAT**.

*Example 6.* The composite $\mathbf{DFib}_{\mathbf{v}}^{\square\lim} \hookrightarrow \mathbf{DFib}_{\mathbf{v}} \to \mathbf{DFib}_{\mathbf{v}}^{2+2}$, which is the right-hand functor in Fig. 1(right), lives in **IRLPCAT**.

## 2.4 Cartesian and opcartesian liftings

It remains to show that the bottom functor of Fig. 1(right) lives in **RLPCAT**. We already broke it down as $\langle \mathcal{P}, \text{id} \rangle$ in Example 5. As sketched in the introduction, we now reconstruct $\mathcal{P}$ in a 2-categorical way, relying on the notion of (op)fibration.

**Definition 6 (Street [30]).** A 1-cell $p: E \to B$ in a 2-category $\mathcal{K}$ is a fibration (resp. opfibration) iff each postcomposition functor $[X, p]: [X, E] \to [X, B]$ is a Grothendieck fibration (resp. opfibration), and furthermore, for any $f: X \to Y$, the precomposition functor $[f, E]: [Y, E] \to [X, E]$ preserves cartesian (resp. opcartesian) 2-cells.

We first formalise the fact that all is well for fibrations:

**Proposition 12.** The forgetful functor **RLPCAT** $\hookrightarrow \mathbf{CAT}$ reflects fibrations, in the sense that any morphism in **RLPCAT** which is also a fibration in **CAT**, is in fact a fibration in **RLPCAT**.

*Remark 4.* The real bit of information behind this result is that if we're given a fibration in **CAT** that happens to live in **RLPCAT**, then cartesian liftings of natural transformations in **RLPCAT** along functors in **RLPCAT** will again live in **RLPCAT**.

As announced in the introduction, the situation for opfibrations is more subtle:

**Proposition 13.** There exists a functor in **RLPCAT** which is a fibration in **CAT** but not in **RLPCAT**.

However, in applications, some useful opcartesian liftings are reflected by the forgetful functor. In order to exploit them, we introduce relative opfibrations.
**Definition 7.** In any 2-category $\mathcal{K}$, a 1-cell $p: E \to B$ is an opfibration relative to some 2-cell $\alpha$ as on the right iff any 2-cell factoring through $\alpha$ admits an opcartesian lifting $\bar{\alpha}$ as above right, i.e., for all $q$ and $x$ making the front face commute, $\alpha \circ_0 q$ admits an opcartesian lifting as shown, and furthermore opcartesianness of $\bar{\alpha}$ is preserved under precomposition by arbitrary 1-cells.

<figure><img src="image_13.png" /></figure>

**Remark 5.** An opfibration $p: E \to B$ is an opfibration relative to the canonical 2-cell between cod, dom : $B^2 \to B$.

Our main way of producing relative opfibrations is through right orthogonality classes. We saw in Proposition 7 that embeddings of the form $J^{\perp} \hookrightarrow E^2$ live in RLPCAT. This readily entails that the natural transformation on the right does so too. In fact, we have more:

<figure><img src="image_14.png" /></figure>

**Proposition 14.** For any set $J$ of morphisms in a locally presentable category $\mathbf{E}$, the codomain projection cod : $J^{\perp} \to \mathbf{E}$ is an opfibration relative to $\lambda^J$ and the opcartesian lifting of any $b \xrightarrow{s} c$ along any $a \xrightarrow{t} b$ is given by composition.

<figure><img src="image_15.png" /></figure>

*Example 7.* By Proposition 14 cod is an opfibration relative to $\lambda$, as below left in RLPCAT.

<figure><img src="image_16.png" /></figure>

Using Proposition 3, we deduce that cod : $\mathrm{DFib}_{\mathrm{v}}^2 \to \mathrm{Cat}$ is also an opfibration relative to $\lambda$. This legitimates the opcartesian lifting of $\mathrm{ext}^*(\mathbf{U})$ along $\pi^{\mathrm{ty}}$, which is the $\overline{\mathbb{P}}$ of Example 5, needed for Fig. 1(right).

With this in stock, we have:

**Proposition 15.** All categories constructed in §1.4 are locally presentable.

## 2.5 Bonuses

In this final subsection, we record a few facts that are not useful for the basic applications of §1.4, but that are for the harder applications in the next sections.

**Proposition 16.**
1. For any family $(F_i : \mathbf{A}_i \to \mathbf{B}_i)_{i \in I}$ of functors in **IRLPCAT**, the product $\prod_i F_i : \prod_i \mathbf{A}_i \to \prod_i \mathbf{B}_i$ in **CAT**² is again in **IRLPCAT**.

2. The embedding **RLPCAT** $\hookrightarrow \mathbf{CAT}$ creates transfinite cocompositions of isofibrations, in the sense that for any ordinal $\lambda$ and continuous functor $F: \lambda^{\mathrm{op}} \to \mathbf{IRLPCAT}$, any limiting cone in **CAT** in fact lives in **IRLPCAT** and is limiting in **RLPCAT**.

*Example 8.* For any $\omega$-cochain $\dots \to C_n \to \dots \to C_1 \to C_0$ of morphisms in **IRLPCAT**, any limiting cone in **CAT** lives in **IRLPCAT** and is limiting in **RLPCAT**.

# 3 Application: multimodal type theory

In this section, we exploit our constructions to cover multimodal type theory [18].
We start with the ambient framework, and then consider logical connectives.

## 3.1 Ambient framework: multimodal natural models

The semantic framework for models of multimodal type theory is built up in two stages: multimodal context structures are introduced first; then multimodal natural models are defined on top of that.

We consider a fixed, small 2-category $\mathcal{M}$, throughout the section.

Let us introduce the first-stage structure:

**Definition 8.** A multimodal context structure is a 2-functor $\mathcal{M}^{\mathrm{coop}} \to \mathbf{Cat}$, where $\mathcal{M}^{\mathrm{coop}}$ denotes $\mathcal{M}$ with both 1- and 2-cells reversed, and $\mathbf{Cat}$ here denotes the 2-category of small categories (with 2-dimensional structure).

Multimodal context structures and 2-natural transformations between them form a category, which we denote by $\mathbf{Cat}^{\mathcal{M}^{\mathrm{coop}}}$.

*Remark 6.* Although it is constructed from 2-categories, we are considering the mere 1-category of 2-functors and 2-natural transformations.

**Proposition 17.** The category $\mathbf{Cat}^{\mathcal{M}^{\mathrm{coop}}}$ is locally presentable.

We now move on to the second-stage structure, for which we use the following alternative, yet equivalent definition.

**Definition 9.** A multimodal natural model [18, Definition 5.4] consists of a multimodal context structure $\llbracket - \rrbracket : \mathcal{M}^{\mathrm{coop}} \to \mathbf{Cat}$, equipped with a morphism $\mathrm{proj}_m : tm_m \to ty_m$ of discrete fibrations over $\llbracket m \rrbracket$, such that, for all $\mu : m \to n$ in $\mathcal{M}$, each pullback $\llbracket \mu \rrbracket^*(\mathrm{proj}_m) : \llbracket \mu \rrbracket^*(tm_m) \to \llbracket \mu \rrbracket^*(ty_m)$ is equipped with natural model structure over $\llbracket n \rrbracket$.

We call **MNatMod** the category of multimodal natural models and structure-preserving morphisms between them.

Our constructions allow us to prove:
**Proposition 18.** The category **MNatMod** is locally presentable.

*Proof (sketch).* Starting from $Cat^{\mathbb{M}^{\text{coop}}}$ (using Proposition 17), we take the pullback below left, thus equipping each base category with a morphism of discrete fibrations.

<figure><img src="image_17.png" /></figure>

We then take the pullback above right, where $\text{mor}(\mathbb{M})$ denotes the set of morphisms in $\mathbb{M}$ and $ev_\mu$ denotes the natural transformation $Cat^{\mathbb{M}^{\text{coop}}}_{\text{DFib}_v^2} \xrightarrow{ev_\mu} Cat$ induced by each $\mu: m \to n$ in $\mathbb{M}$. By Propositions 2 and 12, the tupling

$$ \langle ev_{\mu}^{*}(U_{dom}(\mu)) \rangle_{\mu}: Cat^{\mathbb{M}^{\text{coop}}}_{\text{DFib}_v^2} \to (\text{DFib}_v^2)^{\text{mor}(\mathbb{M})} $$

lives again in **RLPCAT**, hence so does the pullback.

## 3.2 Connectives

In this subsection, we sketch a treatment of logical connectives of multimodal type theory. As before, we focus on dependent product.

**Definition 10.** A dependent product structure [18, §5.2.1] on a multimodal natural model ([-], ty, tm, proj, var, ...) consists of morphisms $\mathfrak{P}_\mu(\text{proj}_m) \to \text{proj}_m$, for all morphisms $\mu: m \to n$ in $\mathbb{M}$, whose underlying square is a pullback, where $\mathfrak{P}_\mu$ denotes the composite

$$ \text{DFib}_{[m]}^2 \xrightarrow{[[\mu]]^*} \text{DFib}_{[n]}^2 \xrightarrow{\text{ext}_n^*} \text{DFib}_{ty_n}^2 \xrightarrow{\pi_1^{ty_n}} \text{DFib}_{[n]}^2 $$

**Proposition 19.** The category of multimodal natural models with dependent products and morphisms between them is locally presentable.

*Proof.* We proceed by combining the techniques for plain dependent product (notably Proposition 14) with those for **MNatMod** in the previous subsection (i.e., indexing everything by morphisms in $\mathbb{M}$).

## 4 Application: SOGATs

In this section, we present a second application of §2: we interpret SOGATs as locally presentable categories. By definition, SOGATs pertain to a specific logical framework [33,34]. This logical framework is itself close to standard type theory with dependent products, but departs from it in two main ways:
1. it is indexed by so-called signatures, with a “local” type theory at each sig-nature, and

2. it has two universes * and □ of types, and only dependent products of the form $\prod_A B$ for A : * and B : □ are allowed, with a result in □.

Furthermore, signatures interact with local type theories through some specific signature extension rules. SOGATs are defined as signatures in this logical frame-work, so their semantics will follow if we interpret the latter.

*Remark 7.* Signatures are in fact potentially infinite, which we can accomodate by Proposition 16(2).

The rest of this section is devoted to sketching such an interpretation. We first sketch the over architecture of our interpretation and its central piece (§4.1), a generalised category with families [11,10], and then the interpretation of the log-ical framework’s dependent products (§4.2) and signature extension rules (§4.2). More details are available in the appendix.

## 4.1 Overall architecture

Were we to interpret a plain type theory with dependent products, it would suffice to exhibit something like a CwF with the structure described in Fig. 2. But since we wish our interpretation to live in RLPCAT, we work with categories that are definitely not small. Furthermore, we consider fibrations that are not discrete. We thus need to move from DFib to general fibrations in RLPCAT. Furthermore, we work in the slice 2-category $\mathcal{K} = \text{RLPCAT}/\text{Cat}$ over Cat. All in all, we work in the category FIB($\mathcal{K}$) of general fibrations in $\mathcal{K}$. We thus need to generalise from CwFs to the following:

**Definition 11 ([11,10]).** A generalised category with families<fnref n="2" /> (gecawf) object in a 2-category $\mathcal{K}$ consists of an object C, together with fibrations $\pi^{ty}: ty \to C$ and $\pi^{tm}: tm \to C$ and a fibration morphism $\text{proj}: ty \to tm$ with a right adjoint $\text{var} \vdash \text{proj} \in \mathcal{K}$, such that the unit and counit are cartesian.

*Remark 8.* For coherence reasons, we actually need to work with split fibrations. We gloss over this here for simplicity, and refer the reader to the appendix.

*Example 9.* The prime example of a gecawf in CAT is given below left, where $tm = \text{DFib}_\bullet$ denotes the category of discrete fibrations equipped with a section.

<figure><img src="image_18.png" /></figure>

<footnote n="2">² This is a generalisation of the existing notion of gecawf in an arbitrary 2-category.</footnote>
It remains to figure out the structure needed to interpret indexing over signatures and dependent products as in (1) and (2) above, as well as the interaction between signatures and local theories.

Indexing is taken care of by “homing into”: we exhibit a gecawf with suitable dependent products in $\mathcal{K} = \text{RLPCAT}/\text{Cat}$, as above center, and let the local theory at any signature $\Sigma$ denote the one above right. (This in particular implies that each signature $\Sigma$ is interpreted as a functor $\pi^{\Sigma}: |\Sigma| \to \text{Cat}$ in RLPCAT.)

We now need to prove that the above center triangle is a gecawf:

**Proposition 20.** The functor $\text{DFib}_{\nu}^{\partial_{\mathbb{R}}}: \text{DFib}_{\nu}^{\mathbb{R}} \to \text{DFib}_{\nu}^{2}$ admits a right adjoint $\rho$ over Cat, given by pointwise self pullback, in the sense that the image of any $(C, ty, tm, proj)$ is the pullback of $proj$ with itself, with section the diagonal. Moreover, the unit and counit are vertical over Cat and cartesian with respect to the projections to $\text{DFib}$.

Finally, we upgrade this gecawf to some version with two universes, and exhibit the desired dependent products. The second universe, and the embedding of $*$ as a subuniverse of $\square$, are modelled as the embedding $\text{NatMod} \hookrightarrow \text{DFib}_{\nu}^{2}$.

## 4.2 Dependent products

Accordingly, the polynomial functor $\mathfrak{P}$ used in Fig. 2 to axiomatise dependent products becomes

$$ \text{FIB}(\mathcal{K})_{\text{DFib}}^{2} \xrightarrow{\xi^{*}} \text{FIB}(\mathcal{K})_{\text{NatMod}}^{2} \xrightarrow{\pi_{1}^{ty}} \text{FIB}(\mathcal{K})_{\text{DFib}}^{2}, $$

where $\xi$ and $\pi^{ty}$ denote the functors below, respectively mapping $(C, ty, tm, proj)$ to $tm$ and $ty$.

$$ \text{DFib} \xleftarrow{\text{cod}_{\nu}} \text{DFib}_{\nu}^{2} \xleftarrow{\text{DFib}_{\nu}^{\partial_{\mathbb{R}}}} \text{DFib}_{\nu}^{\mathbb{R}} \xrightarrow{\rho} \text{DFib}_{\nu}^{2} \hookrightarrow \text{NatMod} \hookrightarrow \text{DFib}_{\nu}^{2} \xrightarrow{\text{cod}_{\nu}} \text{DFib}, $$

where $\rho$ is the right adjoint of Proposition 20.

**Remark 9.** The most important point here is perhaps that we use $\text{NatMod}$ rather than $\text{DFib}_{\nu}^{2}$ as the middle object, which accounts for the specific form of dependent products in the logical framework (2).

Now, to show that the given gecawf features such dependent products, we need to exhibit an analogue of a pullback square $\mathfrak{P}(proj) \to proj$. Let us start with the $\text{DFib}_{\nu}^{2}$ component. The pullback below left

<figure><img src="image_19.png" /></figure>
along $\xi$ has as objects all diagrams of the form above right: natural models equipped with a discrete fibration morphism to their terms.

We should now define functors $\lambda$ and $\Pi$ as below left,

<figure><img src="image_20.png" /></figure>

which should be morphisms of fibrations over **DFib** and form a pullback. For $\Pi$, we map any object $(C, ty, tm, \dots, E, p, j)$ to some choice of pullback $var^*(q)$, viewed as a discrete fibration morphism to $\pi^{ty}$, as above right. The functor $\lambda$ component is similar, the only difference being that $q$ has a section. Retractions being closed under pullback, $var^*(q)$ does lift to a functor $\mathcal{P}(\mathcal{DFib}_v^R) \to \mathcal{DFib}_v^R$.

*Remark 10.* It may not be obvious at this point that $\Pi$ and $\lambda$ are relevant for interpreting SOGATs. We explain this in a bit more detail in Example 10 below, but in the meantime, we invite the reader to think of objects of $\mathcal{E}$ as inputs to some operation being specified, which are indexed by terms. This encompasses inputs that are indexed by types: one may pull back along *proj* to index over terms. Then, pulling back along *var* as $\Pi$ does amounts to considering inputs “in an extended context”, which is precisely what is needed for binding operations.

The proof that the obtained square is a pullback is rather technical, and omitted for lack of space.

## 4.3 Signature extension

We conclude by sketching our interpretation of the interaction between signatures and local type theories. This happens mainly through “signature extension” rules. The logical framework features three rules for extending signatures and one for extending contexts, which we include for comparison:

$$ \frac{\Sigma | \Gamma \vdash}{\Sigma, \Gamma \Rightarrow * \vdash} \qquad \frac{\Sigma | \Gamma \vdash}{\Sigma, \Gamma \Rightarrow \square \vdash} \qquad \frac{\Sigma | \Gamma \vdash A : \square}{\Sigma, \Gamma \Rightarrow A \vdash} \qquad \frac{\Sigma | \Gamma \vdash A : \square}{\Sigma | \Gamma, A \vdash} $$

In our interpretation, $\Sigma|\Gamma$ is a context in the local type theory over $\Sigma$, which means a morphism $|\Sigma| \to \mathbf{DFib}$ over **Cat** in RLPCAT. The first three rules construct an signature, while the last one construct a context in the current local type theory. We interpret these rules as below.

<figure><img src="image_21.png" /></figure>
**Remark 11.** An object of $|\Sigma, \Gamma \Rightarrow \square|$ is an object $C \in |\Sigma|$ together with a morphism to $|\Gamma|(C)$ in $\mathbf{DFib}_{\pi^{\Sigma}(C)}$ – same for $|\Sigma, \Gamma \Rightarrow *|$, except that the morphism now should be equipped with a right adjoint. By contrast, an object of $|\Sigma, \Gamma \Rightarrow A|$ is an object $C \in |\Sigma|$ equipped with a section of $\mathrm{proj}^A(C) : |A|(C) \to |\Gamma|(C)$ over $\pi^{\Sigma}(C)$. (This in particular yields a term of type $A$ (weakened) in $\Sigma, \Gamma \Rightarrow \square|(\cdot)$.)

**Example 10.** For some uninteresting reasons, the signature $\Sigma := (\mathrm{ty} : \square, \mathrm{el} : \mathrm{ty} \Rightarrow *)$ is in fact interpreted as **NatMod**. Let us sketch the (hopefully more interesting) interpretation of $\Sigma_\Pi := (\Sigma, \Pi : (A : \mathrm{ty}, B : \coprod_{B:\mathrm{el}(A)} \mathrm{ty}) \Rightarrow \mathrm{ty})$. Briefly, the type $\Sigma|(\cdot) \vdash \mathrm{ty} : \square$ is interpreted as the functor **NatMod** $\to \mathbf{DFib}_v^2$ mapping any $(C, \mathrm{ty}, \mathrm{tm}, \mathrm{proj}, \mathrm{var})$ to the unique morphism $\pi^{\mathrm{ty}} : \mathrm{ty} \to C$ of discrete fibrations over $C$. Furthermore, the context $\Sigma|A : \mathrm{ty}, B : \mathrm{el}(A)$ is interpreted as the functor **NatMod** $\to \mathbf{DFib}$ returning $\pi^{\mathrm{tm}}$. Thus, by local weakening, $\Sigma|A : \mathrm{ty}, B : \mathrm{el}(A) \vdash \mathrm{ty} : \square$ is interpreted as the right-hand pullback square below.

<figure><img src="image_22.png" /></figure>

By definition of the functor $\Pi$ defined in §4.3, the dependent product $\Sigma|A : \mathrm{ty} \vdash \coprod_{B:\mathrm{el}(A)} \mathrm{ty} : \square$ is obtained by further pulling back along $\mathrm{var}$, as in the left-hand square above. Since the bottom composite is in fact $\mathrm{ext}$, $\coprod_{\mathrm{el}(A)} \mathrm{ty}$ as returning $\mathrm{ext}^*(\pi^{\mathrm{ty}})$. Extending the context with this, we get the functor **NatMod** $\to \mathbf{DFib}$ returning the composite $\mathrm{ext}^*(\mathrm{ty}) \xrightarrow{\mathrm{ext}^*(\pi^{\mathrm{ty}})} \mathrm{ty} \xrightarrow{\pi^{\mathrm{ty}}} C$. We have recovered the type component $\mathfrak{P}(\pi^{\mathrm{ty}}) = \pi_1^{\mathrm{ty}}(\mathrm{ext}^*(\pi^{\mathrm{ty}}))$ of Fig. 2(right). Finally, the weakened type $\mathrm{ty} : \square$ takes the product with $\mathrm{ty}$ over $C$, so that the example signature $\Sigma_\Pi$ is interpreted as the category of natural models equipped with sections of $\mathrm{ty}_\gamma \times \coprod_{a \in \mathrm{ty}_\gamma} \mathrm{ty}_{\mathrm{ext}(\gamma, a)} \to \coprod_{a \in \mathrm{ty}_\gamma} \mathrm{ty}_{\mathrm{ext}(\gamma, a)}$, i.e., equivalently, maps $\coprod_{a \in \mathrm{ty}_\gamma} \mathrm{ty}_{\mathrm{ext}(\gamma, a)} \to \mathrm{ty}_\gamma$, as desired.

# 5 Conclusion

We have demonstrated that a few well-known constructions on locally presentable categories may be used to efficiently produce a large class of categories of models of dependent type theories.

The natural next step is to try and design a synthetic theory of locally presentable categories, which would yield a potentially mechanisable formal framework in which to express such constructions. Inspiration for this may be drawn from work by Cisinski et al. [9] and Riehl and Verity [29].

# References

1. Quotient Inductive-Inductive Types, pp. 293–310. Springer International Publishing, Cham (2018). https://doi.org/10.1007/978-3-319-89366-2_16
2. Adámek, J., Rosicky, J.: Locally Presentable and Accessible Categories. Cambridge University Press (1994). https://doi.org/10.1017/CBO9780511600579

3. Awodey, S.: Natural models of homotopy type theory. Mathematical Structures in Computer Science 28(2), 241–286 (Feb 2018). https://doi.org/10.1017/S0960129516000268

4. Bird, G.: Limits in 2-Categories of Locally-Presented Categories. Ph.D. thesis, University of Sydney (1984)

5. Borceux, F.: Handbook of Categorical Algebra 2: Categories and Structures. Encyclopedia of Mathematics and Its Applications, Cambridge University Press (1994)

6. Bourke, J.: Iterated algebraic injectivity and the faithfulness conjecture. Higher Structures 4(2), 183–210 (Jun 2020). https://doi.org/10.21136/HS.2020.13

7. Bourke, J., Garner, R.: Monads and theories. Advances in Mathematics 351, 1024–1071 (Jul 2019). https://doi.org/10.1016/j.aim.2019.05.016

8. Cartmell, J.: Generalised algebraic theories and contextual categories. Annals of Pure and Applied LogicAnn. Pure and Appl. Logic 32, 209–243 (1986). https://doi.org/10.1016/0168-0072(86)90053-9

9. Cisinski, D.C., Cnossen, B., Nguyen, K., Walde, T.: Formalization of Higher Categories (2025), https://drive.google.com/file/d/1lKaq7watGGl3xvjqw9qHjm6SDPFJ2-0o/view

10. Coraglia, G., Di Liberti, I.: Context, judgement, deduction. CoRR abs/2111.09438 (2021), https://arxiv.org/abs/2111.09438

11. Coraglia, G., Emmeneger, J.: A 2-categorical analysis of context comprehension. Theory and Applications of Categories 41, 1476–1512 (2024), http://www.tac.mta.ca/tac/volumes/41/42/41-42.pdf

12. de Boer, M.: A Proof and Formalization of the Initiality Conjecture of Dependent Type Theory (2020), https://urn.kb.se/resolve?urn=urn:nbn:se:su:diva-181640

13. Di Liberti, I., Osmond, A.: Bi-accessible and Bipresentable 2-Categories. Applied Categorical Structures 33(1), 3 (Feb 2025). https://doi.org/10.1007/s10485-024-09794-9

14. Dybjer, P.: Internal type theory. In: Goos, G., Hartmanis, J., Leeuwen, J., Berardi, S., Coppo, M. (eds.) Types for Proofs and Programs, vol. 1158, pp. 120–134. Springer Berlin Heidelberg, Berlin, Heidelberg (1996). https://doi.org/10.1007/3-540-61780-9_66

15. Gabriel, P., Ulmer, F.: Lokal Präsentierbare Kategorien, Lecture Notes in Mathematics, vol. 221. Springer Berlin Heidelberg, Berlin, Heidelberg (1971). https://doi.org/10.1007/BFb0059396

16. Goguen, J., Thatcher, J., Wagner, E.: An initial algebra approach to the specification, correctness and implementation of abstract data types. In: Yeh, R. (ed.) Current Trends in Programming Methodology, IV: Data Structuring. pp. 80–144. Prentice-Hall (1978)

17. Goguen, J.A., Thatcher, J.W.: Initial algebra semantics. In: 15th Annual Symposium on Switching and Automata Theory (SWAT). pp. 63–77. IEEE (1974)

18. Gratzer, D., Kavvos, G.A., Nuyts, A., Birkedal, L.: Multimodal Dependent Type Theory. Logical Methods in Computer Science Volume 17, Issue 3, 7571 (Jul 2021). https://doi.org/10.46298/lmcs-17(3:11)2021

19. Gratzer, D., Sterling, J.: Syntactic categories for dependent type theory: Sketching and adequacy. CoRR abs/2012.10783 (2020), https://arxiv.org/abs/2012.10783

20. Jacobs, B.: Categorical Logic and Type Theory. No. 141 in Studies in Logic and the Foundations of Mathematics, North Holland, Amsterdam (1999)

21. Joyal, A., Street, R.: Pullbacks equivalent to pseudopullbacks. Cahiers de Topologie et Géométrie Différentielle Catégoriques XXXIV(2), 153–156 (1993)
22. Kaposi, A., Xie, S.: Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics. LIPIcs, Volume 299, FSCD 2024 299, 10:1–10:24 (2024). https://doi.org/10.4230/LIPICS.FSCD.2024.10

23. Kelly, G.M.: Basic Concepts of Enriched Category Theory, London Mathematical Society Lecture Note Series, vol. 64. Cambridge University Press (1982)

24. Kelly, G.M.: Structures defined by finite limits in the enriched context, I. Cahiers de topologie et géométrie différentielle catégoriques **23**(1), 3–42 (1982), https://www.numdam.org/item/CTGDC_1982_23_1_3_0.pdf

25. Kelly, G.M.: Elementary observations on 2-categorical limits. Bulletin of the Australian Mathematical Society **39**, 301–317 (1989)

26. Lack, S.: Towards higher categories. The IMA Volumes in Mathematics and Its Applications, vol. 152, chap. A 2-categories companion. Springer (2010). https://doi.org/10.1007/978-1-4419-1524-5

27. Mac Lane, S.: Categories for the Working Mathematician. No. 5 in Graduate Texts in Mathematics, Springer, 2 edn. (1998). https://doi.org/10.1007/978-1-4757-4721-8

28. Makkai, M., Paré, R.: Accessible Categories: The Foundations of Categorical Model Theory, Contemporary Mathematics, vol. 104. American Mathematical Society (1989)

29. Riehl, E., Verity, D.: Elements of $\infty$-Category Theory. Cambridge University Press, 1 edn. (Jan 2022). https://doi.org/10.1017/9781108936880

30. Street, R.: Fibrations and Yoneda's lemma in a 2-category. In: Kelly, G.M. (ed.) Category Seminar, vol. 420, pp. 104–133. Springer Berlin Heidelberg, Berlin, Heidelberg (1974). https://doi.org/10.1007/BFb0063102

31. Street, R., Walters, R.F.C.: The comprehensive factorization of a functor. Bulletin of the American Mathematical SocietyBull. AMS **79**(5) (1973)

32. Streicher, T.: Semantics of Type Theory. Birkhäuser, Boston, MA (1991). https://doi.org/10.1007/978-1-4612-0433-6

33. Uemura, T.: Abstract and Concrete Type Theories. Ph.D. thesis, University of Amsterdam (2021), https://dare.uva.nl/search?identifier=41ff0b60-64d4-4003-8182-c244a9afab3b

34. Uemura, T.: A general framework for the semantics of type theory. Mathematical Structures in Computer ScienceMSCS **33**(3), 134–179 (2023). https://doi.org/10.1017/S0960129523000208

35. Weber, M.: Yoneda structures from 2-toposes. Applied Categorical Structures **15**, 259–323 (2007). https://doi.org/10.1007/s10485-007-9079-2

# A Omitted proofs

## A.1 Proofs for §2

*Proof (Proposition 3).* By [4, Theorem 2.18], the 2-category **RLPCAT** is closed under flexible limits, which entails that it is closed under all bilimits. Indeed, creation of pseudo-limits entails creation of all bilimits by [25, Proposition 6.1], and furthermore creation of flexible limits entails creation of pseudo-limits by [4, Theorem 1.25]. Furthermore, by Joyal and Street [21, Corollary 1], any pullback along an isofibration in a 2-category is in fact a bipullback, hence any the pullback is created – as a bipullback – by the forgetful functor **RLPCAT** $\to$ **CAT**. The fact that it is not only a bipullback but also a pullback in **RLPCAT** follows from the 2-functor **RLPCAT** $\to$ **CAT** being faithful and locally faithful.
*Proof (Propositions 4 and 5).* The 1-dimensional part of these statements mostly follows from the cotensor part of Proposition 2 below (this is in fact [4, Proposition 2.12]). For the isofibrancy part, that $\mathbf{C}^F$ is an isofibration follows from Theorem 9 in §D. Finally, that $\mathbf{G}^{\mathbb{K}}$ is an isofibration follows from isofibrations being pointwise in **CAT**.

Let us now deal with the 2-dimensional part. By Kelly [24, §3.4], the hom-2-category $[\mathbb{K}, \mathbf{Cat}]$ is locally finitely presentable in the **Cat**-enriched sense, so by Kelly [24, §7.5] its underlying category is locally finitely presentable in the plain sense. Moreover, any restriction 2-functor is a right 2-adjoint by 2-cocompleteness of **Cat**, hence the underlying functor is a right adjoint. When $F: \mathbb{K} \to \mathbb{L}$ is an injective-on-objects 2-functor, the restriction functor $F^*: [\mathbb{L}, \mathbf{Cat}] \to [\mathbb{K}, \mathbf{Cat}]$ is an isofibration thanks to Theorem 9 in §D.

It remains to justify the natural isomorphism

$$ \mathrm{RLPCAT}(\mathbf{C}, \mathbf{Cat}^{\mathbb{K}}) \cong |[\mathbb{K}, [\mathbf{C}, \mathbf{Cat}]_r]|. $$

It is enough to show that the isomorphism of categories below restricts to the above one.

$$ \mathbf{CAT}(\mathbf{C}, \mathbf{Cat}^{\mathbb{K}}) \cong |[\mathbb{K}, [\mathbf{C}, \mathbf{Cat}]]| $$

In other words, we must show that a functor $F: \mathbf{C} \to \mathbf{Cat}^{\mathbb{K}}$ is accessible and continuous if and only if the corresponding 2-functor $\mathbb{K} \to [\mathbf{C}, \mathbf{Cat}]$ factors through $[\mathbf{C}, \mathbf{Cat}]_r$, which means that for each object $k$ of $\mathbb{K}$, the functor $F(k, -): \mathbf{C} \to \mathbf{Cat}$ is right adjoint, or equivalently by Proposition 1, that it is accessible and continuous. This follows from the fact that limits and colimits are computed pointwise in a 2-functor 2-category.

*Proof (Example 2).* We need to show that the bottom functor is a right adjoint: it is indeed right adjoint to the functor $\mathbf{Cat}^2 \xrightarrow{\mathrm{dom}} \mathbf{Cat}$.

*Proof (Proposition 6).* Let us readily observe that this functor is an isofibration because limit cones are closed under isomorphism in $[\mathbb{C}_{\perp}, \mathbf{E}]$. Furthermore, by completeness of $\mathbf{E}$ this functor is the full image of the right Kan extension functor $\coprod_{\mathbf{C}}: \mathbf{E}^{\mathbf{C}} \to [\mathbb{C}_{\perp}, \mathbf{E}]$. By full faithfulness of the embedding $\mathbb{C} \hookrightarrow \mathbb{C}_{\perp}$, $\coprod_{\mathbf{C}}$ is fully faithful, hence $\mathbf{E}^{\mathbf{C}} \hookrightarrow [\mathbb{C}_{\perp}, \mathbf{E}]_{\mathrm{lim}}$ is an equivalence. This shows that $[\mathbb{C}_{\perp}, \mathbf{E}]_{\mathrm{lim}}$ is locally presentable, by Proposition 2. Finally, by construction, $\coprod_{\mathbf{C}}$ lives in **RLPCAT**, as a right adjoint functor between locally presentable categories. □

Before proving Proposition 7, we show:

**Lemma 2.** For any locally presentable category $\mathbf{E}$ and set $J$ of morphisms therein, the full subcategory $J^{\perp}$ spanned by objects that are right orthogonal to $J$ is again locally presentable, where $X \in J^{\perp}$ iff for any $j: A \to B$ in $J$, any morphism $A \to X$ uniquely extends to $B$, as below.

<figure><img src="image_23.png" /></figure>
Furthermore, the embedding $J^\perp \hookrightarrow E$ lives in RLPCAT.

*Proof.* This is well known, but here is a concise proof. The functor $J^\perp \hookrightarrow E$ arises by pullback in CAT as below left,

<figure><img src="image_24.png" /></figure>

where for any $(j : a \to b) \in J$, the $j$th component of the bottom functor maps any $E \in E$ to the map $[j, E]: [b, E] \to [a, E]$. The square is a pullback in CAT by definition of $J^\perp$, and the right-hand functor is in IRLPCAT by Proposition 2 and ?? AL: broken ref. Finally, the bottom functor is in RLPCAT by ?? and the fact that each $[j, E]$ corresponds by universal property of $\mathbf{Set}^2$ to the natural transformation above right, which is in RLPCAT by Proposition 1.

*Proof (Proposition 7).* We apply the lemma with the category $\mathbf{E}^2$ and set of arrows, say $J^+$, given by all morphisms $(j, id): j \to id$, as below,

<figure><img src="image_25.png" /></figure>

for $j \in J$. Indeed, the subcategory $(J^+)^\perp$ consists of all morphisms $f: X \to Y$ such that, for all $u$ and $v$ making the back face below commute,

<figure><img src="image_26.png" /></figure>

there exist unique $k$ and $v'$ making the whole diagram commute. But $v'$ must equal $v$, so this is clearly equivalent to $f \in J^\perp$, hence the result.

*Proof (Proposition 9).* Easy by the previous results.

*Proof (Proposition 11).* Easy by the previous results.

*Proof (Proposition 12, due to Ivan Di Liberti (personal communication)).* Let us first treat the case of fibrations. By Weber [35, Theorem 2.7], a morphism $f: A \to B$ in any finitely complete 2-category $\mathcal{K}$ is a fibration iff the canonical morphism $c: A \to B/f$ has a right adjoint in $\mathcal{K}/B$. The canonical morphism is constructed by universal property of $B/f$ as below.
<figure><img src="image_27.png" /></figure>

Having a right adjoint in $\mathcal{K}/B$ boils down to having a right adjoint $r$ in $\mathcal{K}$ such that $fr = \pi_1$, and the unit and counit project to identities, i.e., $f \circ_0 \eta = id_B$ and $\pi_1 \circ_0 \varepsilon = id_B$.

So let us consider any $f: A \to B$ in **RLPCAT** which is a fibration in **CAT**. By Proposition 2, the comma category $B/f$ in **CAT** is also a comma object in **RLPCAT**, so the canonical morphism $c$ is again in **RLPCAT**. It remains to prove that the right adjoint $r$ is a right adjoint in **RLPCAT/B**, which is all trivial.

*Proof (Proposition 13).* The codomain functor $cod: \mathbf{DFib} \to \mathbf{Cat}$ is an opfibration, with opcartesian lifting given by the comprehensive factorisation system [31]. However, $cod$ is not an opfibration in **RLPCAT**. Indeed, let us consider the 2-cell below left.

<figure><img src="image_28.png" /></figure>

Its opcartesian lifting in **CAT** maps any discrete fibration $p: E \to B$ to the unique functor $\pi_0(E) \to 1$, where $\pi_0(E)$ denotes the set of connected components of $E$, viewed as a discrete category. Continuity of this functor is equivalent to continuity of $\pi_0: \mathbf{Cat} \to \mathbf{Set}$, which does not hold. Indeed, e.g., it does not preserve the equaliser above right.

We then work towards proving Proposition 14. We start with a characterisation of relative opfibrations.

**Proposition 21.** Let us consider any $p: E \to B$ and $\alpha: u \to v: P \to B$ in any 2-category $\mathcal{K}$, such that the pullback $P \times_B E$ exists. Then, $p$ is an opfibration relative to $\alpha$ iff

- $\alpha \circ_0 \pi_1$ has an opcartesian lifting $\bar{\alpha}$ along $\pi_2$, as below, and furthermore

- opcartesianness of $\bar{\alpha}$ is preserved under precomposition by arbitrary 1-cells.

<figure><img src="image_29.png" /></figure>
*Proof.* The “only if” direction is clear. For the “if” part, for any $q$ and $x$ as below,

<figure><img src="image_30.png" /></figure>

we find $m: X \to P \times_B P$ by universal property of pullback, and $\bar{\alpha} \circ_0 m$ is opcartesian by construction. $\square$

Let us now give a few results for constructing relative opfibrations in **RLPCAT**.
We start with a sufficient condition (Corollary 1), which relies on the following lemma.

**Lemma 3.** For any opfibration $p$ in **CAT**, $p$-opcartesian 2-cells are pointwise, in the sense that a natural transformation is opcartesian iff all of its components are.

*Proof.* Let us consider an opfibration $p$ in **CAT**. Opfibrations in **CAT** are Grothendieck opfibrations. Thus, given an opcartesian 2-cell $\alpha: u \to v: X \to E$, for any $x \in X$, the whiskering $\alpha \circ_0 x$ is again opcartesian for $p^1: E^1 \to B^1$, hence opcartesian for $p$. Conversely, if $\alpha$ is pointwise opcartesian, then it is easy to show that possesses the 2-categorical opcartesianness property: for any lifting problem, we infer the components of a candidate mediating transformation, which is natural by uniqueness. $\square$

**Corollary 1.** Given $p: E \to B$ and $\alpha$ in **RLPCAT** as below

<figure><img src="image_31.png" /></figure>

such that the pullback $P \times_B E$ in **CAT** is created by the forgetful functor **RLPCAT** $\to$ **CAT**. Then, $p$ is an opfibration relative to $\alpha$ in **RLPCAT** if

- it is an opfibration in **CAT**, and furthermore

- the opcartesian lifting $\alpha_1(\pi_2)$ above is continuous.

*Proof.* The opcartesian lifting being continuous entails that it is opcartesian in **RLPCAT**, hence we conclude by Proposition 21, using Lemma 3. $\square$
We may now prove Proposition 14.

*Proof (Proposition 14).* We apply Corollary 1. That the codomain functor $\mathcal{R} \xrightarrow{cod} \mathbf{C}$ is an opfibration in $\mathbf{CAT}$ is well-known and easy. That the composition functor $\mathcal{R} \to \mathbf{C}^2$ creates limits, or otherwise said that the right-hand class of any strong factorisation on a complete category is closed under pointwise limits. $\square$

*Proof (Proposition 15).* Things follow easily up to **NatMod**. Let us now deal with dependent products. We first add up the morphisms $\lambda$ and $\Pi$, and then incorporate the pullback condition. For adding the desired morphisms, we first consider the reindexing the forgetful functor **U**, along the needed composite, as below left,

<figure><img src="image_32.png" /></figure>

where, at any natural model $(\mathcal{C}, ty, tm, proj, var)$ with $proj \to var$,

- **ctx** returns $\mathcal{C}$,

- **ty** returns $ty$,

- **ext** returns the composite $ty \xrightarrow{var} tm \xrightarrow{\pi^{tm}} \mathcal{C}$.

We check that the involved functors are right adjoints: **ctx** is the composite

$$ \mathrm{NatMod} \xrightarrow{U} \mathrm{DFib}_{\nu}^{2} \to \mathrm{Cat}, $$

while **ty** is the composite

$$ \mathrm{NatMod} \to \mathrm{DFib}_{\nu}^{2} \xrightarrow{cod_{\nu}} \mathrm{DFib} \xrightarrow{dom} \mathrm{Cat}. $$

We then opreindex the result along the projection $\pi^{ty}: ty \to \mathrm{ctx}$, as above right, by virtue of (2)(left). Indeed, the front face above right forms a cone over $\mathrm{DFib} \xrightarrow{dom} \mathrm{Cat} \xleftarrow{cod} \mathrm{DFib}_{\nu}^{2}$. This gives us a functor $A := \pi_{\nu}^{ty} \mathrm{ext}^{*}(\mathbf{U}) : \mathrm{NatMod} \to \mathrm{DFib}_{\nu}^{2}$ in **RLPCAT**. Pairing this with **U** over **Cat**, we obtain a functor

$$ \langle A, \mathbf{U} \rangle : \mathrm{NatMod} \to \mathrm{DFib}_{\nu}^{2+2}, $$

which we take as our arity. Finally, we pull this back along the restriction functor $\mathrm{DFib}_{\nu}^{2 \times \partial}: \mathrm{DFib}_{\nu}^{2} = \mathrm{DFib}_{\nu}^{2+2} \to \mathrm{DFib}_{\nu}^{2+2}$, so that an object of the pullback
<figure><img src="image_33.png" /></figure>

is precisely a natural model equipped with morphisms $\lambda$ and $\Pi$ making the desired square commute.

It remains to incorporate the condition that the given squares are pullbacks. For this, our arity is the functor $\text{NatMod}_{\Pi}^{0} \to \text{DFib}_{\nu}^{\square}$ just constructed, which we pullback along the full subcategory embedding $\text{DFib}_{\nu}^{\square\lim} \hookrightarrow \text{DFib}_{\nu}^{\square}$ of Example 6. $\square$

*Proof (Proposition 16).* The first point is easy. For the pullback case, creation of flexible limits entails creation of all bilimits. Indeed, creation of pseudo-limits entails creation of all bilimits by Proposition 6.1 of [25], and furthermore creation of flexible limits entails creation of pseudo-limits by Theorem 1.25 of [4]. Furthermore, by Joyal and Street [21, Corollary 1], any pullback along an isofibration in a 2-category is in fact a bipullback, hence any such pullback is created by the forgetful functor.

Finally, the result about transfinite cocomposition essentially follows from [6, Proposition A.3(1)].

## A.2 Proofs for §3

*Proof (Proposition 19).*

We first add up the morphisms $\lambda_{\mu}$ and $\Pi_{\mu}$, and then incorporate the pullback condition.

**Notation 4.** We consider the forgetful functor $\text{MNatMod} \to \text{Cat}_{\text{DFib}_{\nu}^{2}}^{\mathbb{M}^{\text{coop}}}$ as an implicit coercion, so that $U_{m}: \text{MNatMod} \to \text{DFib}_{\nu}^{2}$ actually denotes the composite

$$ \text{MNatMod} \to \text{Cat}_{\text{DFib}_{\nu}^{2}}^{\mathbb{M}^{\text{coop}}} \xrightarrow{U_{m}} \text{DFib}_{\nu}^{2}. $$

As before, we proceed by reindexing $U_{m}$, but this time along the needed composite, as below left,

<figure><img src="image_34.png" /></figure>
and then opereindexing the result above right. This gives us a functor $A_\mu := (\pi^{\mathcal{t}n})_! (ev_\mu \mathit{ext}_n)^*(U_m)$: $\mathbf{MNatMod} \to \mathbf{DFib}_v^{2}$ in RLPCAT. Pairing this with $U_n$ over Cat, we obtain a functor

$$ \langle A_\mu, U_n \rangle : \mathbf{MNatMod} \to \mathbf{DFib}_v^{2+2}, $$

which we take as our arity. We then take the pullback

<figure><img src="image_35.png" /></figure>

whose objects are precisely a multimodal natural models equipped with morphisms $\lambda_\mu$ and $\Pi_\mu$ making the desired square commute. As previously, we collect all such squares by raising the arity type to the power of $\mathbf{mor}(\mathcal{M})$ and tupling all arities. □

# B Semantics of Uemura's logical framework

In this section, we present a model of Uemura's logical framework that allows to interpret a SOGAT as its locally presentable category of models. The main ingredient to interpret the logical framework is a generalised CwF in RLPCAT/Cat. We present it in §B.2, and we later enrich it with a class of small types in §B.3, dependent products with small domains in §B.4, and extensional identity types in §B.5. In §B.6, we explain how to account for the empty context in type theories specified by SOGATs. Let us start, in §B.1, with providing an alternative indexed notion of natural models in order to avoid the coherence problems when interpreting the logical framework.

## B.1 Indexed natural models

The definition of natural models that we used so far would not be able to account for strict associativity of substitution. Essentially, this is the standard issue preventing a direct interpretation of dependent type theories in locally cartesian closed categories: the codomain fibration is not split. Therefore, in this section, we work with an alternative description where we work with presheaves rather than discrete fibrations.

**Notation 5.** Let $P \to$ denote the total category Cat//Set of presheaves over small categories; we denote by dfib the functor $P \to \mathbf{Cat}^2$ mapping a presheaf to its associated discrete fibration. This is in RLPCAT by the results of §C, in particular Corollary 3. The induced functors dom and cod from $P \to$ to Cat mapping a presheaf to its category of elements and its base category are respectively denoted by dom and cod.
Let $\mathbf{P}^{\dashrightarrow}$ denote the category of presheaves such that the associated discrete
fibration has a right adjoint var, defined as below.

<figure><img src="image_36.png" /></figure>

Let $\mathbf{P}^{\dashrightarrow}$ denotes the category of presheaves $F$ equipped with a section $1 \to F$,
formally defined as the pullback below

<figure><img src="image_37.png" /></figure>

where $\mathbf{Cat}//1$ is the right adjoint to the projection $\mathbf{Cat}//\mathbf{Set} \to \mathbf{Cat}$, mapping a category to the terminal presheaf over it. We get the projection to $\mathbf{P}^{\dashrightarrow} \to \mathbf{P}^{\dashrightarrow}$ as the composition $\mathbf{P}^{\dashrightarrow} \to \mathbf{Cat}//\mathbf{Set}^2 \xrightarrow{\mathbf{Cat}//\mathbf{Set}^{\mathrm{cod}}} \mathbf{Cat}//\mathbf{Set} = \mathbf{P}^{\dashrightarrow}$.

Given any formal sequence of potentially dashed our double-headed arrows
→ ... →, we define $\mathbf{P}^{→...→}$ by suitable iterated pullbacks of $\mathbf{P}^{→}$, $\mathbf{P}^{→}$, and $\mathbf{P}^{→}$.
For example, $\mathbf{P}^{→→}$ is the pullback of $\mathbf{P}^{→}$ $\xrightarrow{\mathrm{cod}} \mathbf{Cat}$ $\leftarrow^{\mathrm{dom}} \mathbf{P}^{→}$. It is the category
of (indexed) natural models: objects consists of a presheaf ty and a presheaf tm
over $\mathcal{F}$ ty such that $\mathcal{F} tm \to \mathcal{F}$ ty has a right adjoint var.

B.2 Structural rules

The main result that allows us to give semantics to the core structure of Uemura’s
logical framework is the following.

**Proposition 22.** The functors $\mathbf{P}^{\dashrightarrow} \to \mathbf{P}^{\dashrightarrow} \xrightarrow{\pi_2} \mathbf{P}^{\dashleftarrow}$, with their codomain projections to $\mathbf{Cat}$, defines a split generalised category with families (Definition 11) in the slice 2-category RLPCAT/Cat in the following sense:

- the projections $\mathbf{P}^{\dashrightarrow} \xrightarrow{\pi_2} \mathbf{P}^{\dashrightarrow}$ and $\mathbf{P}^{\dashrightarrow} \xrightarrow{\pi_2} \mathbf{P}^{\dashleftarrow}$ are split fibrations internal to RLPCAT/Cat;

- the projection functor $\mathbf{P}^{\dashrightarrow} \to \mathbf{P}^{\dashrightarrow}$ preserves (chosen) cartesian 2-cells and has a right adjoint $\mathbf{R}$ over $\mathbf{Cat}$;

- the unit and counit are cartesian (in the split cleavage) and vertical with respect to the projections to $\mathbf{Cat}$;

- $\mathbf{P}^{\dashrightarrow}$ has a terminal object in RLPCAT/Cat, in the sense that cod: $\mathbf{P}^{\dashrightarrow} \to \mathbf{Cat}$ has a right adjoint over $\mathbf{Cat}$.

*Proof.* First, all the involved functors are right adjoints:
- the left adjoint to cod : $\mathbf{P} \dashrightarrow \mathbf{Cat}$ maps a category to the empty presheaf 0 over it;

- the left adjoint to $\pi_2 : \mathbf{P} \dashrightarrow \mathbf{P} \dashrightarrow \mathbf{P} \dashrightarrow \mathbf{P}$ maps a presheaf $C^{op} \xrightarrow{X} \mathbf{Set}$ to $(X, 0)$;

- the left adjoint to the projection $\mathbf{P} \dashrightarrow \mathbf{P} \dashrightarrow \mathbf{P} \dashrightarrow \mathbf{P}$ maps $(X, Y)$ to $(X, Y + 1)$.

The projections $\mathbf{P} \dashrightarrow \pi_2 \xrightarrow{\pi_2} \mathbf{P} \dashrightarrow \mathbf{P} \dashrightarrow \mathbf{P} \dashrightarrow \mathbf{P}$ and $\mathbf{P} \dashrightarrow \pi_2 \xrightarrow{\pi_2} \mathbf{P} \dashrightarrow \mathbf{P} \dashrightarrow \mathbf{P} \dashrightarrow \mathbf{P}$ are split fibrations in **CAT**, so they are in **RLPCAT**. Then, it is easy to check that a fibration in a 2-category is also a fibration in any slice 2-category, so that we indeed have a fibration in **RLPCAT**/*Cat*. The right adjoint to the projection functor $\mathbf{P} \dashrightarrow \mathbf{P} \dashrightarrow \mathbf{P} \dashrightarrow \mathbf{P}$ maps a pair of presheaves $(C^{op} \xrightarrow{A} \mathbf{Set}, \mathcal{F} A^{op} \xrightarrow{B} \mathbf{Set})$ to $(C^{op} \xrightarrow{B'} \mathbf{Set}, \mathcal{F} B'^{op} \cong \mathcal{F} B^{op} \to \mathcal{F} A^{op} \xrightarrow{B} \mathbf{Set})$, where $B'$ is the image of $B$ by the equivalence $[\mathcal{F} A^{op}, \mathbf{Set}] \cong [C^{op}, \mathbf{Set}]/A$, that is, $B'$ maps $c$ to $\sum_{a \in A(c)} B(a)$. It is straightforward to check that the unit and counit are cartesian and vertical.

Finally, the terminal object in $\mathbf{P} \dashrightarrow$ is given by the terminal presheaf 1 over the terminal category 1,

The right adjoint **Cat**//1 : **Cat** $\to \mathbf{P} \dashrightarrow$ of the last item maps any category to the terminal presheaf over it.

In the following, by cartesian 2-cell with respect to a split fibration, we always mean a 2-cell that is in the split cleavage, which makes the following result trivial.

**Lemma 4.** Given a split fibration $p : E \to B$, two cartesian 2-cells sharing the same 1-cell as codomain are equal if and only if their whiskering by $p$ are equal.

**Definition 12.** We denote the composition $\mathbf{P} \dashrightarrow \mathbf{P} \dashrightarrow \mathbf{P} \dashrightarrow \mathbf{P}$ by $\mathbf{P}^{\circ}$: it maps $(C^{op} \xrightarrow{A} \mathbf{Set}, \mathcal{F} A^{op} \xrightarrow{B} \mathbf{Set})$ to the presheaf on $C$ mapping $c$ to $\sum_{a \in A(c)} B(c, a)$.

**Lemma 5.** The following triangle commutes up to isomorphism.

<figure><img src="image_38.png" /></figure>

With this structure, we are already able to interpret all the structural rules of Uemura's logical framework, potentially involving large types: we list below the interpretation of the judgements, and of the structural rules. Note that the semantics takes place in **RLPCAT**/*Cat*: the 1-cells are required to commute strictly with the projection to **Cat**, and any 2-cell must be vertical with respect to these projections (that is, whiskering it with the projection must yield the identity natural transformation).
**Semantics of judgements** We list below the interpretation of judgements in **RLPCAT/Cat**: 1-cells must commute with the projections to **Cat**, and 2-cells must be vertical with respect to those projections.

<figure><img src="image_39.png" /></figure>

**Semantics of structural rules** We list the interpretation of the main structural rules in **RLPCAT/Cat**. Some of them slightly differ from Uemura's syntactic presentation. Indeed, we are focusing on presenting a semantics for the logical framework rather than an interpretation of the raw syntax and typing rules. Of course, the former entails the latter via the initiality property of the syntactic model [33,12,32].

For legibility, we adopt a named convention for variables in the rules, and weakenings are implicit: for example, we write the first variable of a context extended by $A$ as $x: A$ instead of $x: A[p_A]$ where $p_A$ is the weakening substitution.

<figure><img src="image_40.png" /></figure>
$$ \Sigma | \Gamma \vdash () : () $$

$$ () = \Sigma \xrightarrow{\Gamma} \mathbf{P} \xrightarrow{\Downarrow \eta} \mathbf{Cat} \xrightarrow{\text{Cat//1}} \mathbf{P} $$

$$ \frac{\begin{array}{c} \Sigma | \Gamma \vdash \gamma : \Delta \\ \Sigma | \Delta \vdash A \\ \Sigma | \Gamma \vdash s : A[\gamma] \\ \Sigma \vdash \langle \gamma, s \rangle : (\Delta, x : A) \end{array}}{\langle \gamma, s \rangle = \Sigma} \qquad \begin{array}{c} \Gamma \\ A[\gamma] \\ \eta \\ \Delta, x : A \end{array} $$

We can then recover the following rules from Uemura’s original presentation of the logical framework.

$$ \frac{(\alpha : \Gamma \Rightarrow \Box) \in \Sigma \qquad \Sigma | \Delta \vdash \gamma : \Gamma}{\Sigma | \Delta \vdash \alpha(\gamma) : \Box} $$

$$ \frac{(\alpha : \Gamma \Rightarrow A) \in \Sigma \qquad \Sigma | \Delta \vdash \gamma : \Gamma}{\Sigma | \Delta \vdash \alpha(\gamma) : A[\gamma]} $$

Let us indeed focus on the first rule (the second is similar). The premise $(\alpha : \Gamma \Rightarrow \Box) \in \Sigma$ entails that we have a weakening substitution $w$ from $\Sigma$ to some prefix $\Sigma'$, $\alpha : \Gamma \Rightarrow \Box$ of $\Sigma$. Then we get:

$$ \frac{\begin{array}{c} \Sigma', \alpha : \Gamma \Rightarrow \Box | \Gamma \vdash \alpha : \Box \qquad \Sigma \vdash w : \Sigma' \\ \Sigma | \Gamma \vdash \alpha[w] : \Box \end{array}}{\Sigma | \Delta \vdash \alpha[w][\gamma] : \Box} $$

**Infinite SOGATs** Note that Uemura allows a SOGAT $\Sigma$ to consist of an infinite well-ordered set of declaration of variables. This can be accounted by taking the limit of all the prefixes of $\Sigma$, interpreted as locally presentable categories, with projections between them (which are all isofibrations, as can be seen below from the definitions of SOGAT extensions by pullbacks), thanks to closure of **IRLPCAT** under limits of cochains (see Proposition 16).

## B.3 Small types

In this section we describe the structure that takes small types into account.

**Proposition 23.** The functor $\mathbf{P}^{\dashrightarrow} \to \mathbf{P}^{\leftarrow}$ over $\mathbf{Cat}$ defines a class of small types in the generalised CwF $\mathbf{P}^{\dashrightarrow} \to \mathbf{P}^{\leftarrow} \xrightarrow{\text{cod}} \mathbf{P}^{\leftarrow}$, in the following sense:

- The functor $\pi_2: \mathbf{P}^{\dashrightarrow} \to \mathbf{P}^{\leftarrow}$ is a (split) fibration in **RLPCAT**/$\mathbf{Cat}$;

- $\mathbf{P}^{\dashrightarrow} \to \mathbf{P}^{\leftarrow}$ preserves (chosen) cartesian 2-cells.
Remark 12. Note that the functor $\pi_2: P^{\dashrightarrow} \to P^{\rightarrow}$ is not a fibration in RLPCAT.

We can then interpret the judgements and rules for the kind * of small types, which are analogous to those for □ except that we need to replace $P^{\dashrightarrow}$ with $P^{\rightarrow}$ in the right places. For example $\Sigma|\Gamma \vdash A : *$ denotes a (right adjoint) functor $A$ from $\Sigma$ to $P^{\dashrightarrow}$ compatible with $\Gamma: \Sigma \to P^{\rightarrow}$. Moreover, there is an obvious coercion from $A : *$ to $A : \square$ obtained by postcomposing with the canonical projection $P^{\dashrightarrow} \to P^{\rightarrow}$, accounting for the following rule

$$ \frac{\Sigma | \Gamma \vdash A : *}{\Sigma | \Gamma \vdash A : \square} $$

## B.4 Dependent product

**Proposition 24.** The generalised CwF $P^{\dashrightarrow} \to P^{\rightarrow} \xrightarrow{\pi_2} P^{\rightarrow}$ with class of small types $P^{\dashrightarrow} \to P^{\rightarrow}$ has dependent products with small domain in the sense that there are functors $\lambda$ and $\Pi$ making the following below left square a pullback, and making the right below square commute,

<figure><img src="image_41.png" /></figure>

where

- $P^{\dashrightarrow} \dashrightarrow \lambda$ is the category consisting of natural models $(C^{op} \xrightarrow{\text{ty}} \text{Set}, \mathcal{F}^{ty} \xrightarrow{\text{tm}} \text{Set})$ with a presheaf over $\mathcal{F}^{tm'}$, where $\mathcal{F}^{tm'} : C^{op} \to \text{Set}$ maps $c$ to $\sum_{A \in \text{ty}(c)} \text{tm}(c, A)$;

- $P^{\dashrightarrow} \dashrightarrow \Pi$ is the same but equipped with a section of this presheaf.

Both are formally defined by the pullbacks below.

<figure><img src="image_42.png" /></figure>

**Notation 6.** Given outer commutative squares as below, summarised by the following judgements (the gray parts are implicit in the diagrams), we denote
the mediating morphisms to the pullbacks by $A \vdash B$ and $A \vdash b$.

$$ \Sigma |_{\Gamma, x : A \vdash B : \square} $$

$$ \Sigma |_{\Gamma, x : A \vdash b : B} $$

<figure><img src="image_43.png" /></figure>

<figure><img src="image_44.png" /></figure>

**Remark 13.** This is similar to the notion of dependent product type for the generalised CwF $P \dashv \to \to P \dashv \to \xrightarrow{\pi_2} P$ in the sense of Coraglia and Di Liberti [10, Definition 3.5.1], except that the domain is restricted to small types.

When working with objects of $P \dashv \to \to$), we sometimes omit the isomorphism $\int tm' \cong \int tm$ when it plays no particular role, that is, we work as if it were an identity.

**Remark 14.** The bracketing in the notation $P \dashv \to \to$ or $P \dashv \to \dashv \to$ is here to distinguish the definitions from the *unbiased* one where the domain of the top presheaf is directly over the category of elements of $tm$. The unbiased category is actually isomorphic to the biased one.

Before proving Proposition 24, we show how it allows us to interpret the dependent product of the logical framework.

$$ \frac{\Sigma | \Gamma \vdash A : * \qquad \Sigma | \Gamma, x : A \vdash B : \square}{\Sigma | \Gamma \vdash (x : A) \to B : \square} $$

$$ \Sigma \underset{A \vdash B}{\stackrel{(x : A) \to B}{\longrightarrow}} P \dashv \to \underset{\Pi}{\longrightarrow} P \dashv \to $$

$$ \frac{\Sigma | \Gamma \vdash A : * \qquad \Sigma | \Gamma, x : A \vdash b : B}{\Sigma | \Gamma \vdash \lambda(x : A).b : (x : A) \to B} $$

$$ \Sigma \underset{A \vdash b}{\stackrel{\lambda x.b}{\longrightarrow}} P \dashv \to \underset{\lambda}{\longrightarrow} P \dashv \to $$

$$ \frac{\Sigma | \Gamma \vdash A : * \qquad \Sigma | \Gamma, x : A \vdash B : \square \qquad \Sigma | \Gamma \vdash b : (x : A) \to B}{\Sigma | \Gamma, x : A \vdash \textcolor{red}{\text{app}(b)} : B} $$

<figure><img src="image_45.png" /></figure>
We then recover the usual application rule as follows:

$$
\frac{
  \begin{array}{c}
    \Sigma | \Gamma \vdash A : * \\
    \Sigma | \Gamma, x : A \vdash B : \square \\
    \Sigma | \Gamma \vdash b : (x : A) \to B \\
    \Sigma | \Gamma, x : A \vdash \text{app}(b) : B
  \end{array}
}{
  \Sigma | \Gamma \vdash \text{app}(b)[id_\Gamma, a] : B[id_\Gamma, a]
}
\qquad
\frac{
  \begin{array}{c}
    \Sigma | \Gamma \vdash id_\Gamma : \Gamma \\
    \Sigma | \Gamma \vdash (id_\Gamma, a) : (\Gamma, x : A)
  \end{array}
}{
  \Sigma | \Gamma \vdash id_\Gamma : A
}
$$

The rest of this section is devoted to the proof of Proposition 24. Let us detail
the functors Π: P(· → ) → P(· → ) and λ: P(· → ) → P(· → ) that we are going to
build formally. Given ty: C op → Set, tm: ℘ ty op → Set, X: ℘ tm' op → Set, the
image by Π is a functor ℘ ty → Set mapping a type A in context Γ to Y(Γ, A) =
X(Γ.A, A, v 0 ). Given the same data and an additional section s x ∈ hom(1, X ),
the image by λ is a section s Y mapping (Γ, A) to x (Γ.A, A, v 0 ). Let us now build
these functors formally.

**Building the functor Π** The crucial observation is that (Γ.A, A, v₀) is the image of (Γ, A) by the right adjoint var : ℘ty → ℘tm, so that Π(ty, tm, X) = X ◦ var.

Remark 15. It follows from Uemura [34, Proposition 3.21] that the projection
$$
\mathcal{P} \Pi(\mathcal{Y}, \mathcal{M}, \mathcal{X}) \to \mathcal{P} \mathcal{Y}
$$
is the pushforward of $\mathcal{P} X \to \mathcal{P} \mathcal{M}$ along $\mathcal{P} \mathcal{M} \to \mathcal{P} \mathcal{Y}$ in the
category of discrete fibrations over the base category.

Formally, Π is defined by lifting the bottom composite of 2-cells in the following
diagram, exploiting the split fibration P → cod → Cat, where the natural isomor-
phism follows from Lemma 5.

<figure><img src="image_46.png" /></figure>

**Building the functor λ** We directly build an isomorphism between P(· → ) and the pullback Q of Π along P(· → ) → P(· → ) that is compatible with the pro- jection P(· → ) → P(· → ).
*On objects* Objects of $\mathbf{P}^{\dashrightarrow(\dashrightarrow\dashrightarrow)}$ and $\mathcal{Q}$ share the following components:

- a presheaf $ty$;

- a presheaf $tm$ over $\mathcal{F}ty$;

- a presheaf over $\mathcal{F}tm'$, or equivalently, a presheaf $X$ over $\mathcal{F}tm$;

- a right adjoint $var: \mathcal{F}ty \to \mathcal{F}tm$ to the canonical projection.

On top of that, an object of $\mathbf{P}^{\dashrightarrow(\dashrightarrow\dashrightarrow)}$ includes a section $s: 1 \to X$, while an object of $\mathcal{Q}$ includes a section $s': 1 \to X \circ var^{op}$. Clearly, from $s$ we can define $s'$ as $s \circ var^{op}$. Conversely, from $s'$ we define $s$ by the diagram below. This defines a bijection, by the mate correspondance.

<figure><img src="image_47.png" /></figure>

*On morphisms* Given objects $(ty, tm, X, var, s)$ and $(ty', tm', X', var', s')$ of $\mathbf{P}^{\dashrightarrow(\dashrightarrow\dashrightarrow)}$, a morphism between them and a morphism between their image by the object bijection share the following components:

- a functor $F$ between the base categories;

- a natural transformation $ty_F: ty \to ty' \circ F^{op}$;

- a natural transformation $tm_F: tm \to tm' \circ \mathcal{F}ty_F^{op}$;

- a natural transformation $X_F: X \to X' \circ \mathcal{F}tm_F^{op}$.

The difference is that a morphism in $\mathbf{P}^{\dashrightarrow(\dashrightarrow\dashrightarrow)}$ requires compatibility with the sections $s$ and $s'$ as in (3), while a morphism in $\mathbf{P}^{\dashrightarrow}$ between their image requires compatibility with the sections $s \cdot var^{op}$ and $s \cdot var'^{op}$, which is (3) but pre-whiskered by $\mathcal{F}ty^{op} \xrightarrow{var^{op}} \mathcal{F}tm^{op}$.

$$ \begin{tikzcd} \mathcal{F}tm^{op} \arrow[r, "1"] \arrow[d, "s"] & \mathbf{Set} \arrow[d, "X"] \\ \mathcal{F}tm_F^{op} \arrow[r, "1"] \arrow[d, "X_F"] & \mathcal{F}tm'^{op} \arrow[r, "1"] \arrow[d, "s"] \arrow[Rightarrow,

The following lemma ensures that we indeed have a bijection.

**Lemma 6.** Equation (3) is satisfied if and only if it pre-whiskering by $\mathcal{F}var^{op}$ is.
*Proof.* The only if part is clear. Conversely, it must be that the following equation
holds, since the blue part does, as the pre-whiskered equation.

<figure><img src="image_48.png" /></figure>

We conclude by the fact that $1 \cdot \eta^{op}$ is the identity natural transformation.

## B.5 Extensional identity types

**Proposition 25.** The generalised CwF $P \dashrightarrow \bar{P} \rightarrow \bar{P} \xrightarrow{\pi_2} P$ has extensional identity type [10, Definition 3.6.1] in the sense that there are functors $\text{ld}$ and $\text{refl}$ making the below triangle commutes and the below left square a pullback, where $P \dashrightarrow \bar{P}^{2} \dashrightarrow$ is defined by the below right pullback.

<figure><img src="image_49.png" /></figure>

**Notation 7.** Given an outer commutative square as below, summarised by the
following judgements, we denote the mediating morphism to the pullback by $a, b$.

<figure><img src="image_50.png" /></figure>
Before proving Proposition 25, we show how it allows us to interpret the identity type of the logical framework.

<figure><img src="image_51.png" /></figure>

The rest of this section is devoted to the proof of Proposition 25. Informally, the functor $\mathrm{ld}$ maps a presheaf $A$, a presheaf $B$ over $\mathcal{F}A$ and two sections $s, s': 1 \to B$ to the equaliser $\mathcal{E}$ of $s, s'$. More explicitly, $\mathcal{E}(c)$ is 1 if $x_c = x_{c'}$, or the empty set otherwise. The functor $\mathrm{refl}$ maps a presheaf $A$, a presheaf $B$ over $\mathcal{F}A$ and a section $s: 1 \to B$ to the unique section (which is the identity morphism) of the terminal presheaf 1 over $\mathcal{F}A$.

Let us now build these functors formally.

**Building the functor $\mathrm{ld}$** We construct $\mathrm{ld}$ by universal property of the pullback defining $\mathbf{P} \to \mathbf{P}$ in RLPCAT as below, where the blue arrow is defined in the top
diagram.

<figure><img src="image_52.png" /></figure>

The equaliser functor maps two parallel natural transformations to their equalisers. It is right adjoint to the functor $Cat//Set \xrightarrow{\mathrm{Cat//Set}^1} Cat//Set \twoheadrightarrow$ and is thus in RLPCAT.

**Building the functor** refl Similarly to what we did for the $\lambda$ functor of the dependent product in §B.4, we directly build an isomorphism between $P \twoheadrightarrow$ and the pullback $Q$ of $\mathrm{Id}$ along $P \twoheadrightarrow \mathrm{Id}$.

*On objects* Objects of $P \twoheadrightarrow$ and $Q$ share the following components:

- a presheaf $A$;

- a presheaf $B$ over $\mathcal{B}$ ty;

- a section $s: 1 \to B$.

An object of $P \twoheadrightarrow$ does not have more components, while an object of $Q$ includes another section $s': 1 \to B$ as well as a section $s'': 1 \to E$ of the equaliser $E$ of $s, s'$. By composing it with the equaliser map $E \hookrightarrow 1$, we conclude that $s$ must be equal to $s'$, so that $E = 1$ and $s''$ is the identity map. As a consequence, the two classes of objects are in bijective correspondance.

*On morphisms* Given objects $(A, B, s)$ and $(A', B', s')$ of $P \twoheadrightarrow$, a morphism between them consists of the following components:

- a functor $F$ between the base categories;

- a natural transformation $A_F: A \to A' \circ F^{op}$;
- a natural transformation $B_F : B \to B' \circ \mathcal{F}ty_F^{op}$;

- compatible with the sections, in the sense that $B_F \circ s = s' \circ \mathcal{F}A_F^{op}$.

It is straightforward to check that a morphism in $\mathcal{Q}$ between their images is determined by the same data.

## B.6 The empty context in type theories specified by SOGATs

Our semantics of SOGATs does not guarantee the existence of a terminal object in the base category. For example, the SOGAT $ty : \square, tm : ty \to *$ is interpreted as the category of natural models, without further enforcing the existence of the empty context. This is easy to fix: given a SOGAT $\Sigma$, we can simply consider the pullback of $\Sigma \to \mathbf{Cat} \leftarrow \mathbf{Cat}_1$ to recover the desired category of models.

## C Diagram category

In this subsection, we show that **RLPCAT** is closed under a particular case of the Grothendieck construction, namely the functor mapping any small category $\mathcal{C}$ to the hom-category $[\mathcal{C}, \mathbf{E}]$, for some fixed $\mathbf{E} \in \mathbf{RLPCAT}$. We also prove that “change-of-base” functors $[\mathcal{C}, \mathbf{E}] \to [\mathcal{C}, \mathbf{E}']$ live in $(\mathbf{I})\mathbf{RLPCAT}$ when the underlying functor $\mathbf{E} \to \mathbf{E}'$ does. This is used in §B.

**Definition 13.** For any category $\mathbf{E}$, we denote by $\mathbf{Cat}\//\mathbf{E}$ the category with

- as objects pairs of a small category $\mathcal{C}$ and a functor $X : \mathcal{C}^{op} \to \mathbf{E}$, and

- as morphisms $(\mathcal{C}, X) \to (\mathcal{D}, Y)$ all functors $F : \mathcal{C} \to \mathcal{D}$ equipped with a natural transformation $\alpha$ as below.

<figure><img src="image_53.png" /></figure>

**Proposition 26.** For any locally presentable category $\mathbf{E}$, $\mathbf{Cat}\//\mathbf{E}$ is locally presentable.

Furthermore, for any functor $F : \mathbf{E} \to \mathbf{E}'$, the postcomposition functor

$$ \mathbf{Cat}\//F : \mathbf{Cat}\//\mathbf{E} \to \mathbf{Cat}\//\mathbf{E}' $$

(a) is a right adjoint when $F$ is one, and

(b) is an isofibration when $F$ is one.

**Corollary 2.** For any small category $\mathcal{C}$, the canonical functor $\mathbf{Cat}\//\mathbf{Set}^{\mathcal{C}} \to (\mathbf{Cat}\//\mathbf{Set})^{\mathcal{C}}$ is in $\mathbf{RLPCAT}$.

*Proof.* By universal property of $(\mathbf{Cat}\//\mathbf{Set})^{\mathcal{C}}$ and Proposition 2, it suffices to show that each projection functor $\mathbf{Cat}\//\mathbf{Set}^{\mathcal{C}} \to \mathbf{Cat}\//\mathbf{Set}$ is in $\mathbf{RLPCAT}$, which follows from Proposition 26 with $F : 1 \to \mathcal{C}$ picking the corresponding object.
*Example 11.* Let us consider the refinement

$$ \mathbf{Cat}/\mathbf{Set}^{cod} : \mathbf{Cat}/\mathbf{Set}^2 \to \mathbf{Cat}/\mathbf{Set}. $$

An object in $\mathbf{Cat}/\mathbf{Set}^2$ consists of a small category $\mathcal{C}$ equipped with a natural transformation $p: X \to Y$ in $[\mathcal{C}^{op}, \mathbf{Set}]$. And the forgetful functor maps this to the pair $(\mathcal{C}, Y)$. Pulling back along this functor can be thought of as the refinement “adding a set $X$ with projection to $Y$, all indexed over $\mathcal{C}$”.

**Corollary 3.** For any small $\mathcal{C}$, all functors below

$$ \mathbf{Cat}/\mathbf{Set}^{\mathcal{C}} \to (\mathbf{Cat}/\mathbf{Set})^{\mathcal{C}} \simeq \mathbf{DFib}^{\mathcal{C}} \hookrightarrow ([2, \mathbf{Cat}])^{\mathcal{C}} \xrightarrow{\mathrm{dom}^{\mathcal{C}}, \mathrm{cod}^{\mathcal{C}}} \mathbf{Cat}^{\mathcal{C}} $$

live in RLPCAT.

*Remark 16.* Taking the composite with $\mathcal{C} = 1$ yields the Grothendieck construction functor $\mathcal{F}: \mathbf{Cat}/\mathbf{Set} \to \mathbf{Cat}$.

**Notation 8.** We call $\mathcal{F}^{\mathcal{C}}$ the composite with $\mathrm{dom}$, and $\mathrm{dom}^{\mathcal{C}}$ the one with $\mathrm{cod}$ (because it takes pairs $(\mathcal{C}, F)$ with $F \in [\mathcal{C}^{op}, \mathbf{Set}]$ to $\mathcal{C}$).

# D Restricting along an injective-on-object functor

This section is devoted to the proof of the following statement, used in §A. AL: En fait c'est un cas particulier pullback-power axiom bien connu que verifie les cat de modeles Cat-enrichie comme cat (cf par exemple Lack's homotopy theoretical aspects of 2-monads), en prenant l'un des objets implique comme l'objet terminal. Evidemment le theoreme ci-dessous est plus general, mais cette generalisation n'est pas forcement utile.

**Theorem 9.** Let $V$ be a symmetric closed monoidal category, $F: \mathcal{C} \to \mathcal{D}$ a $V$-functor injective on objects, and $E$ be a $V$-category. Then, the restriction functor $F^*: V\text{-Cat}(\mathcal{D}, E) \to V\text{-Cat}(\mathcal{C}, E)$ is an isofibration.

This is a direct consequence of the following result, taking the right functor to be the identity functor on $E$.

**Proposition 27.** Let $V$ be a symmetric closed monoidal category, and consider a $V$-natural isomorphism $\alpha$ as below left such that the left functor is injective on objects and the right functor is an equivalence, i.e., a fully faithful $V$-functor essentially surjective on objects. Then, there exists a diagonal $V$-functor as below right such that

- The top triangle commutes strictly;

- the bottom triangle commutes up to a natural isomorphism;

- the pasting of the two triangles yields $\alpha$.
<figure><img src="image_54.png" /></figure>

*Proof.* For each object $d$ of $\mathcal{D}$, we define the object $Kd$ of $\mathbf{E}$ as $Gc$ if $d = Fc$ for some object $c$ of $\mathcal{C}$, and as some preimage $U^{-1}Vd$ of $Vd$ by the (surjective) $V$-functor $U$ otherwise. Then, for each object $d$, we have a $V$-natural isomorphism $\beta_d: \mathbf{E}(Kd, -) \cong \mathbf{B}(Vd, U-)$, in the sense of [5, Proposition 6.2.8]. Indeed,

- in the first case, $\mathbf{E}(Kd, -) = \mathbf{B}(Gc, -) \cong \mathbf{B}(UGc, U-) \cong \mathbf{B}(VFc, U-)$, where the first isomorphism comes from the fact that $U$ is fully faithful;

- in the second case, $\mathbf{E}(Kd, -) \cong \mathbf{B}(UKd, U-) \cong \mathbf{B}(Vd, U-)$ where the first isomorphism comes again from the fact that $U$ is fully faithful, and the second one from the definition of $d$.

By Kelly [23, §1.10], there exists a unique $V$-functor $K: \mathbf{B} \to \mathbf{E}$ such that the above isomorphisms are natural in $d$.

Let us show that the upper triangle commutes strictly. On objects, it is by definition. On morphisms, we show that the top and left morphisms below from $\mathcal{C}(c, c')$ to $\mathbf{E}(Gc, Gc')$ are equal, when post-composed with the same isomorphisms, with references to Kelly [23] for the commutation of the subdiagrams.

<figure><img src="image_55.png" /></figure>
We now show that the lower triangle commutes up to isomorphism. First we build a V-natural transformation $I \to \mathbf{B}(Vd, UKd)$ as $I \xrightarrow{id_{Kd}} \mathbf{E}(Kd, Kd) \cong \mathbf{B}(Vd, UKd)$ by applying the extra-variable form of the weak Yoneda lemma [23, §1.9] to $\mathbf{E}(Kd, -) \cong \mathbf{B}(Vd, U-)$. This is actually a pointwise isomorphism: when $d = Fc$, then we get

$$ I \to \mathbf{E}(Kd, Kd) \xrightarrow{U} \mathbf{B}(UKd, UKd) = \mathbf{B}(UGc, UKd) \xrightarrow{\mathbf{B}(\alpha_c, UKd)} \mathbf{B}(VFc, UKd) \quad (4) $$

otherwise we get

$$ I \to \mathbf{E}(Kd, Kd) \xrightarrow{U} \mathbf{B}(UKd, UKd) \xrightarrow{\mathbf{B}(\cong, UKd)} \mathbf{B}(Vd, UKd). $$

In both cases, the first two morphisms yield the identity V-morphism $I \to \mathbf{B}(UKd, UKd)$. Since we compose it with a V-isomorphism in both case, we get an isomorphism.

Finally, the diagram below shows that whiskering this isomorphism yields $\alpha$, where the top-right branch accounts for the isomorphism by (4), with references to Kelly [23] for the commutation of the subdiagrams.

<figure><img src="image_56.png" /></figure>

# E Summary of the constructions in RLPCAT

In this section we list all the constructions we have used in the main body of the paper.

## E.1 Base cases

The categories **Set** and **Cat** are locally presentable. Moreover, any representable functor from a locally presentable category to **Set** is right adjoint.
## E.2 1-dimensional cotensoring

**Construction 1.** **Input** A locally presentable category $\mathcal{C}$ and a small category $\mathbf{D}$.

**Output** A locally presentable category $\mathcal{C}^{\mathbf{D}}$.

**Explicit description** The category $\mathcal{C}^{\mathbf{D}}$ is the category of functors from $\mathbf{D}$ to $\mathcal{C}$.

The output category $\mathcal{C}^{\mathbf{D}}$ has a universal property that enables the following construction.

**Construction 2.** **Input** A functor from a small category $\mathbf{D}$ to RLPCAT($\mathbb{B}$, $\mathcal{C}$);

**Output** A right adjoint functor from $\mathbb{B}$ to $\mathcal{C}^{\mathbf{D}}$.

Moreover we have the following property.

**Proposition 28.** Consider the right adjoint $G^F : \mathbb{B}^E \to \mathcal{C}^\mathbf{D}$ induced by a functor $F : \mathbf{D} \to \mathcal{E}$ between small categories and a right adjoint $G : \mathbb{B} \to \mathcal{C}$ by Construction 2. If $F$ is injective-on-object and $G$ is an isofibration, then so is $G^F$.

We also have the limiting cotensoring.

**Construction 3.** **Input** A small category $\mathbf{D}$ and a locally presentable category $\mathcal{C}$;

**Output** A fully faithful embedding isofibrant functor $\mathcal{C}^{\mathbf{D}_{\perp,\lim}} \hookrightarrow \mathcal{C}^{\mathbf{D}_{\perp}}$ in RLPCAT.

**Explicit description** This is the full subcategory of limiting cones in $\mathcal{C}$ for a diagram of shape $\mathbf{D}$.

## E.3 2-dimensional cotensoring

**Construction 4.** **Input** A small 2-category $\mathbf{D}$.

**Output** A locally presentable category $\mathbf{Cat}^{\mathbf{D}}$.

**Explicit description** The category $\mathbf{Cat}^{\mathbf{D}}$ is the category of 2-functors from $\mathbf{D}$ to $\mathbf{Cat}$ and strict 2-natural transformations between them.

The category $\mathbf{Cat}^{\mathbf{D}}$ has a universal property that enables the following construction.

**Construction 5.** **Input** A 2-functor $\mathbf{D} \to \text{RLPCAT}(\mathbb{B}, \mathbf{Cat})$, where the 2-cells of RLPCAT($\mathbb{B}$, $\mathbf{Cat}$) are the modifications;

**Output** A right adjoint functor from $\mathbb{B}$ to $\mathbf{Cat}^{\mathbf{D}}$.

**Proposition 29.** Consider the right adjoint $\mathcal{C}^F : \mathcal{C}^E \to \mathcal{C}^{\mathbf{D}}$ induced by a functor $F : \mathbf{D} \to \mathcal{E}$ between small categories by Construction 5. If $F$ is injective-on-object, then $\mathcal{C}^F$ is an isofibration.
## E.4 Pullback

*Construction 6. Input A span $C \xrightarrow{F} D \xleftarrow{G} E$ in RLPCAT where G is an isofibration;

*Output A cospan $C \stackrel{p_C}{\leftarrow} C \times_D E \xrightarrow{p_E} E$ that induces a pullback both in CAT and RLPCAT, and such that $p_C$ is an isofibration;

The pullback property enables the following construction.

*Construction 7. Input A commutative square in RLPCAT where the right arrow is an isofibration;

*Output A right adjoint to the pullback making the triangles commutes as below.

<figure><img src="image_57.png" /></figure>

## E.5 Fibrations

The fact that the forgetful 2-functor RLPCAT → CAT creates fibrations enables the following construction.

*Construction 8. Input A natural transformation as below left, such that all the functors are right adjoints, and the right functor is moreover a fibration;

*Output A right adjoint and natural transformation as below right, in red, such that the triangle below right commutes and the two induced natural transformations below left and right are equal.

<figure><img src="image_58.png" /></figure>

## E.6 Right orthogonal class (derived)

This construction is derived from the previous ones. We present it because it is involved in the next one.

*Construction 9. Input A set of morphisms $J$ in some locally presentable category $\mathcal{C}$.

*Output A full subcategory embedding $J^\perp \hookrightarrow \mathcal{C}^2$ in IRLPCAT.
**Explicit description** The category $J^{\perp}$ is the full subcategory of $\mathbb{C}^2$ spaned by morphisms having the right lifting property with respect to morphisms in $J$. This is defined as the following pullback, where $\perp$ denotes the walking isomorphism.

<figure><img src="image_59.png" /></figure>

The right functor is an isofibration by Proposition 29, and the bottom functor is defined from Construction 2 by the family of 2-cells below, inducing a functor from $J \times 2$ to RLPCAT($\mathbb{C}^2$, Set).

<figure><img src="image_60.png" /></figure>

## E.7 Relative opfibrations for orthogonal classes

**Construction 10.** **Input** A set of morphisms $J$ in some locally presentable category $\mathcal{C}$, and a natural transformation as below left, such that all the functors are right adjoints.

**Output** A right adjoint and natural transformation as below right, in red, such that the square below right commutes and the two induced natural transformations below left and right are equal.

<figure><img src="image_61.png" /></figure>