Bicategorical type theory: semantics and syntax

Abstract

We develop semantics and syntax for bicategorical type theory. Bicategorical type theory features contexts, types, terms, and directed reductions between terms. This type theory is naturally interpreted in a class of structured bicategories. We start by developing the semantics, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; we study both specific examples as well as classes of examples constructed from other data. From the notion of comprehension bicategory, we extract the syntax of bicategorical type theory, that is, judgment forms and structural inference rules. We prove soundness of the rules by giving an interpretation in any comprehension bicategory. The semantic aspects of our work are fully checked in the Coq proof assistant, based on the UniMath library.

1. Introduction

In recent years, efforts have been made to develop directed type theory. Roughly, directed type theory should correspond to Martin-Löf type theory ( $\mathsf{MLTT}$ ) as $\infty$ -categories correspond to $\infty$ -groupoids. Besides theoretical interest in directed type theory, it is hoped that such a type theory can serve as a framework for synthetic directed homotopy theory and synthetic $\infty$ -category theory. Applications of those, in turn, include reasoning about concurrent processes (Fajstrup et al. 2016).

Several proposals for syntax for directed type theory have been given (reviewed in Section 2.3.2), but are ad hoc and are not always semantically justified. The semantic aspects of directed type theory are particularly underdeveloped; a general notion of model of a directed type theory is still lacking. Indeed these proposals often provide an interpretation of their syntax in categories. They either employ preexisting 1-categorical semantical tools, thus forcing them to interpret their syntax into a 1-category of categories, as in the work by North (2019), or, in the absence of 2-categorical tools, give an ad hoc interpretation of their syntax into the 2-category of categories, as done by Licata and Harper (2011). We rectify this situation by providing a 2-categorical semantical structure.

Specifically, in this work, we introduce comprehension bicategories as a suitable mathematical structure for higher-dimensional (directed) type theory. Approaching the development of directed type theory from the semantic side, we extract from this the core syntax – judgment forms and structural inference rules – of a two-dimensional dependent type theory that can accommodate directed type theory. We also give a soundness proof of our structural rules. In future work, we will equip our syntax and semantics with variances and type and term formers for directed type theory.

To motivate our approach, we analyze in Section 1.1 how higher-groupoidal structure arises in $\mathsf{MLTT}$ through an interplay of judgmental equality and typal identity. Our analysis thus leads to the desiderata listed in Section 1.2. In Section 1.3, we discuss the foundations we work in, and aspects of the computer formalization of some of our results.

1.1 Judgmental and typal higher dimensions

The judgment forms of traditional $\mathsf{MLTT}$ specify types, contexts, terms, and judgmental equality (conversion) between types and terms. There is, prima facie, nothing higher-dimensional about these judgments, and an interpretation of types as sets and terms as elements of sets seems perfectly adequate. In this sense, Martin-Löf type theory is 1-dimensional. However, $\mathsf{MLTT}$ is often said to be $\infty$ -dimensional. The higher dimensions are generated by the identity type, which internalizes the judgmental equality; specifically, the well-known reflexivity rule generates a typal identity from a judgmental equality. Since the identity type can be iterated, judgmental equality then also becomes available for terms of the identity type itself. This mutual interaction between judgmental equality and typal identity provides the infrastructure to “lift” judgmental equality to higher dimensions without extending the judgmental structure of $\mathsf{MLTT}$ . The tower of types $(A, {{{\mathsf{Id}}}}_A,{{{\mathsf{Id}}}}_{{{{\mathsf{Id}}}}_A},\ldots)$ then can be given the structure of an $\infty$ -groupoid, as shown by Van den Berg and Garner (2011) and Lumsdaine (2010).

When developing a directed type theory, with models in $\infty$ -categories, the analogous ingredients are the following:

I1: A judgment of directed reductions between types and terms, analogous to judgmental equality;

I2: A type former for homomorphisms between terms, analogous to identity types;

I3: A notion of model in which to interpret the judgments and type formers.

In the present work, we propose a judgmental framework (I1), and a suitable general notion of semantics (I3), for higher-dimensional and directed type theory. In a separate work, we will expand this core by a system of variances suitable for accommodating a type former akin to North’s hom-types (I2), to build a fully functional higher-dimensional type theory.

1.2 Deriving syntax from semantics

Previous work on higher-dimensional and directed type theory – reviewed in detail in Section 2 – has focused on syntax (I1/I2). Licata and Harper (2011, 2012) andNuyts (2015) devise judgmental structure for higher-dimensional and directed type theory. North (2019) devises a type former for directed homomorphisms between terms, on top of the judgmental structure of $\mathsf{MLTT}$ . None of these works propose a general definition of model of directed type theory. Garner (2009) defines a notion of higher-dimensional model, but considers only undirected type theory.

Our approach is different from that of previous work on directed and higher-dimensional type theory. Specifically, we choose to approach the challenge from the other direction: we start by devising a suitable categorical structure for directed type theory and extract a syntax from it.

We refine the ingredients above to the following list of desiderata for our work:

D1: A system of inference rules for dependent types with directed reductions;

D2: A definition of mathematical structures suitable for the mathematical modelling of the syntactic rules;

D3: An interpretation of the inference rules in such a mathematical structure;

D4: A syntax for type and term formers on top of D1;

D5: A semantic structure for the interpretation of type and term formers.

In the present work, we achieve desiderata D1, D2, and D3. The study of variances and type and term constructors will be reported on elsewhere. In Section 2, we refer back to these desiderata for describing related work.

The semantics we propose are described in Section 5, and the extracted syntax is described in Section 8. Both our syntax and semantics are quite general; for instance, our reductions are proof-relevant – like those considered by Licata and Harper (2011, 2012), and unlike judgmental equality in MLTT, which is proof-irrelevant. Syntax and semantics could reasonably be simplified or specialized. Crucially, our work provides a framework to modify syntax and semantics in lockstep, with a clear mechanism to analyze changes to the syntax on the semantic side and vice versa. We suggest some possible variants in Section 10.

1.3 Foundations and formalization in UniMath

The main results presented here are agnostic to foundations: they can be formalized in both set theory and type theory.

However, some of the notions we employ can economically be formulated using dependent types. In particular, we work with cloven (Grothendieck) fibrations of (bi)categories, whose formulation in set theory usually relies on postulating equality of objects. Using dependent types, a formulation of such concepts can be given that avoids any reasoning about equality of objects; instead, these concepts are formulated in terms of fibers. For this reason, we use type-theoretic language throughout the paper; see also, e.g., Remark 25.

We carefully distinguish data and property; in particular, we postulate entities in categories (e.g., limits) to be explicitly given as data rather than to merely exist. We do not rely on any choice axioms or on excluded middle.

The results of Sections 3–7 of this work are checked in $\mathsf{Coq}$ (Coq Development Team 2022), based on the library (Voevodsky et al. 2022) of univalent mathematics. In univalent mathematics, we distinguish strict (bi)categories and univalent (bi)categories (Ahrens et al. 2021, Section 4). Our definitions are agnostic to this difference; hence, our definition of bicategory (Definition 1) does not make a commitment to either strictness or univalence. Specific examples can then be strict (such as Example 11) or univalent (such as Example 49); see also Remark 2.

Our code has been integrated into The computer-checked definitions and results are accompanied by a link (e.g., ) to the corresponding definition in an HTML version of that commit. The code written specifically for this work comprises approximately 33,600 lines of code; specifically, the coqwc tool counts as follows:

We build upon an existing library of (bi)category theory by Ahrens et al. (2015, 2021) and use heavily the displayed machinery, developed for 1-categories by Ahrens and Lumsdaine (2019) and extended to bicategories by Ahrens et al. (2021). In particular, the formalized notions of cloven Grothendieck fibration we are using (in the 1-categorical case) and developing (in the bicategorical case) are based on displayed (bi)categories; we can thus discuss these notions without postulating equality of objects.

The syntax presented in Section 8 and its interpretation given in Section 9 are not computer-checked; we therefore give these constructions in more detail in the paper.

1.4 Synopsis

In Section 2, we review related work. In Section 3, we review (displayed) bicategories and functors. In Section 4, we define cloven global and local (op/iso)fibrations of bicategories, and we use these notions to define comprehension bicategories. In Section 5, we discuss some examples of comprehension bicategories. In Section 6, we discuss Street (op)fibrations internal to bicategories, which form our main examples of comprehension bicategories. In Section 7, we define display map bicategories, and we show how any display map bicategory gives rise to a comprehension bicategory. In Section 8, we present structural type-theoretic rules for the syntax of a two-dimensional type theory, which we call $\mathsf{BTT}$ . In Section 9, we give an interpretation of $\mathsf{BTT}$ in any comprehension bicategory. In Section 10, we discuss variations of $\mathsf{BTT}$ and the semantic structures these variations correspond to. In Section 11, we explain the difference between terms in $\mathsf{BTT}$ and terms in other approaches to directed type theory.

1.5 Version history

A shorter version of this paper was published in the proceedings of Logic in Computer Science under a different name (Ahrens et al. 2022). Compared to that shorter version, the following material has been added in the present version:

• We provide more instantiations of Example 57. In particular, we show that several bicategories of structured categories have pullbacks (Example 19).

• We give more detail on the specific comprehension bicategory given by functors into the 1-category of strict categories, in Example 44. We also present a formalization of that example.

• We introduce display map bicategories and show that any display map bicategory gives rise to a comprehension bicategory.

• We present the type theory $\mathsf{BTT}$ in more detail and specify more of its type-theoretic rules.

• We give more detail in the interpretation of the rules of $\mathsf{BTT}$ in any comprehension bicategory.

Furthermore, compared to the short version, we have added the definition of weak comprehension bicategory (see Definition 38 and Remark 40), where the comprehension $\chi$ is not required to preserve (op)cartesian cells. Our interpretation of $\mathsf{BTT}$ works in any such weak comprehension bicategory.

2. Related Work

In this section, we review work with a similar goal to ours, as well as work we rely on. We pay particular attention to the desiderata outlined in Section 1.2 and to the difference between judgmental and typal dimensions.

2.1 Nondependent type theories

The following works satisfy a nondependent variant of D1, together with suitable adaptations of D2 and D3. However, due to the absence of type dependency, they do not immediately compare to our work.

Seely (1987) presents a syntax for a two-dimensional simply-typed lambda calculus, consisting of types, terms, and reductions between terms. Seely then constructs a 2-category out of that syntax. Tabareau (2011) frames aspect-oriented programming in a 2-categorical way, developing a lambda calculus that provides an internal language for 2-categories. Hirschowitz (2013) constructs a 2-adjunction between 2-signatures for lambda calculi (where such signatures specify types, terms, and reductions) and the category of Cartesian closed 2-categories. Fiore and Saville (2019) construct an internal language for cartesian closed bicategories; the result is a class (parametrized by a notion of signature for constants) of simple 2-dimensional type theories or lambda calculi. This last work shares one aspect with ours that the others do not: it uses (weak) bicategorical structure, rather than (strict) 2-categorical structure.

2.2 Theories for higher categories

There is a body of work on designing type theories for $\omega$ -groupoids and $\omega$ -categories. In these type theories, one works, semantically speaking, within one fixed $\infty$ -groupoid (or $\omega$ -category). Compare this to, e.g., Martin-Löf type theory, where one manipulates $\infty$ -groupoids (types and identity types) and $\infty$ -functors (functions) between them. Analogously, in our type theory, each type can be thought of as a category. Despite these different goals, we mention some of the work in this area.

Brunerie (2016) constructs a type theory whose models are weak $\infty$ -groupoids. Benjamin et al. (2021) (see also the work by Finster and Mimram 2017) design a type theory whose models are precisely $\omega$ -categories à la Grothendieck–Maltsiniotis. Finster et al. (2022) study meta-theoretic properties of a language for strictly unital $\infty$ -categories. There are also computer tools implementing such type theories, see, e.g., the work by Bar et al. (2018) and Reutter and Vicary (2019).

2.3 Theories with dependent types

In this section, we review work on higher-dimensional and directed type theory with dependent types. We start with a review of work on undirected type theory.

2.3.1 Undirected type theory

The idea of considering higher-dimensional interpretations of type theory stems from Hofmann and Streicher’s groupoid interpretation of Martin-Löf type theory by Hofmann and Streicher (1994). This interpretation is generalized to stacks (poset-indexed groupoids satisfying a sheaf condition) in order to prove the independence of several logical principles by Coquand et al. (2017). It is furthermore generalized, from different angles, to higher dimensions, see, e.g., work by Van den Berg and Garner (2011), Lumsdaine (2010), and Kapulkin and Lumsdaine (2021). All of this work considers the Martin-Löf identity type, which is undirected.

Licata and Harper (2012) develop a two-dimensional dependent type theory with a judgment for equivalences $\Gamma \vdash \alpha : M \simeq_A N$ between terms $M,N:A$ . These equivalences are postulated to have (strict) inverses. The authors give an interpretation of types as groupoids: terms are (interpreted as) objects in the interpreting groupoid, and equivalences are morphisms, necessarily invertible. No general notion of semantic structure is discussed; this work hence satisfies an undirected version of D1, but not D2.

Coraglia and Di Liberti (2021) introduce judgmental theories and calculi for them as a general framework to present and study deductive systems. They instantiate their framework to obtain a type theory that describes an internal language of 2-toposes (Coraglia and Di Liberti 2021, Section 5.3); however, they only consider a one-dimensional type theory à la Martin-Löf, and thus their work does not satisfy D1.

Garner (2009) studies a typal two-dimensional type theory à la Martin-Löf: the forms of judgment are the same as in Martin-Löf type theory. Garner calls a type X “discrete” if it satisfies identity reflection (that is, if any identity $p : x = y$ between elements $x,y:X$ induces a judgmental equality $x \equiv y$ . Rules are then added that turn any identity type into a discrete type, effectively making every type into a 1-type, in the sense of the h-levels of homotopy type theory. Garner defines a notion of two-dimensional model based on (strict) comprehension 2-categories. Exploiting the restriction to 1-truncated types, a sound and complete interpretation of that two-dimensional type theory in any model is then given. The Martin-Löf identity type is undirected; correspondingly, Garner defines their comprehension 2-categories to consist of locally groupoidal 2-categories. Thus, Garner’s work satisfies D1 for undirected reductions, using the identity type for this purpose. Garner also considers type constructors such as dependent pair types and dependent product types, thus satisfying D4 and D5 in this case. ¹

2.3.2 Directed type theory

Licata and Harper (2011) (see also Licata 2011, Chapter 7) also design a directed two-dimensional type theory and give an interpretation for it in the strict 2-category of categories. Their syntax has a judgment for substitutions between contexts, written $\Gamma \vdash \theta : \Delta$ , and transformations between parallel substitutions. An important aspect of their work is variance of contexts/types, built into the judgments. The type formers there have a certain variance – covariance or contravariance – in each of the arguments. They do not define a general notion of model for their theory; this work hence satisfies D1, but not D2.

Nuyts (Nuyts 2015, Section 1.3.1) observes that the type theory developed by Licata andHarper (2011) does not allow for a nontrivial Martin-Löf identity type – any such type would coincide with the directed transformations. Nuyts thus attempts to generalize the treatment of variance by Licata and Harper, and designs a directed type theory with additional variances, such as isovariance and invariance. Nuyts does not provide any interpretation of their syntax, and thus no proof of (relative) consistency; the work hence does not satisfy D2.

North (2019) develops a type former for directed types of morphisms, resulting in a typal higher-dimensional directed type theory based on the judgments of $\mathsf{MLTT}$ . North’s work thus does not satisfy D1. The model given by North is in the 2-category of categories, similar to the model by Licata and Harper (2011).

Shulman (2012), in unfinished work, aims to develop 2-categorical logic, including a two-dimensional notion of topos and a suitable internal language for such toposes. Specifically, Shulman sketches two internal languages for 2-toposes. The first language (Shulman 2011) is undirected, consisting only of types and terms. The second language (Shulman 2010) is only described in a short sketch; it is a kind of directed type theory featuring, in particular, variances. Our work is similar to Shulman’s in the sense that both start from a (bi)categorical notion and extract a language from it, with the goal of developing a precise correspondence between extensions of the syntax and additional structure on the semantics. Unfortunately, Shulman’s work is unfinished, which makes a more complete evaluation difficult. However, it contains several ideas that have influenced the present work. For instance, Shulman (2019) emphasizes the usefulness of restricting to (op)fibrations instead of considering all 1-cells when constructing bicategories of arrows – we do this in our main examples of comprehension bicategory, Examples 45 and 57.

Riehl and Shulman (2017) design a simplicial type theory (STT) featuring a directed interval type, as a synthetic theory of $(\infty, 1)$ -categories. As a notion of model, they introduce “comprehension categories with shapes” (Riehl and Shulman 2017, Def. A.5). These are (1-categorical) towers of fibrations accounting for several layers of contexts. Further work on STT was done, among others, by Weaver and Licata (2020) and Buchholtz and Weinberger (2021). STT is not higher dimensional in the sense of Licata and Harper (2011) or the present work; in particular, reductions, both in the tope layer and in the type layer, are undirected. This work thus does not satisfy D1.

Summary In the present work, we define bicategorical semantics for the interpretation of types, terms, and reductions and derive from it a system of inference rules; our work thus satisfies D1, D2, and D3. We do not handle D4 and D5 in this work.

Among the described related work, our work is closest to work by Licata and Harper (2011) and Garner (2009). Compared to Licata andHarper (2011), we add a general definition of “model” of a directed two-dimensional type theory and provide many examples of models. Compared to Garner (2009), we cover directed reductions and provide many instances of our general definition of model. Compared to both works, we do not handle type and term formers.

3 Preliminaries

Here, we sketch some definitions used later on. Many would be very long if given in full; instead, we try to convey some intuition while pointing to the formalized definitions. As a reference for bicategory theory, see Bénabou (1967). We use here the vocabulary and notation introduced by Ahrens et al. (2021).

Definition 1 A bicategory consists of a type $\mathsf{B}_0$ of 0-cells (or objects), a type $a \to b$ of 1-cells from a to b for every $a,b: \mathsf{B}_0$ , and a set $f \Rightarrow g$ of 2-cells from f to g for every $a,b: \mathsf{B}_0$ and $f,g: a \to b$ . We have identity $\operatorname{id}_1(a) : a \to a$ and composition of 1-cells $f \cdot g : a \to c$ (also written fg), which we write in diagrammatical order. These operations do not satisfy the axioms for a 1-category. Instead, we have, for instance, the left unitors, that is, invertible 2-cells $\ell_{f} : \operatorname{id}_1(a) \cdot f \Rightarrow f$ for any 1-cell f, and similarly right unitors $r_{f} :\, f \cdot \operatorname{id}_1(b) \Rightarrow f$ . Analogously, we have the associators, a family of invertible 2-cells $\alpha(\,f, g, h) :\, f \cdot (g \cdot h) \to (\,f \cdot g) \cdot h$ . For 2-cells $\theta :\, f \Rightarrow g$ and $\tau : g \Rightarrow h$ (where $f,g,h : a \to b$ for some $a,b : \mathsf{B}_0$ ), we have a vertical composition $\theta \bullet \tau :\, f \Rightarrow h$ . For any 1-cell $f : a \to b$ , we have an identity 2-cell $\operatorname{id}_2(\,f) :\, f \Rightarrow f$ , which is neutral with respect to vertical composition: $\operatorname{id}_2(\,f) \bullet \theta = \theta$ . For any two objects a and b, the 1-cells from a to b, and 2-cells between them, form the objects and morphisms of the hom-category $\underline{\mathsf{B}(a,b)}$ , with composition given by vertical composition of $\mathsf{B}$ . We also have left and right whiskering; given a 2-cell $\theta :\, f \Rightarrow g : b \to c$ and a 1-cell $e : a \to b$ , we have the left whiskering $e \vartriangleleft \theta : e \cdot f \Rightarrow e \cdot g$ , and, similarly, the right whiskering $\theta \vartriangleright h :\, f \cdot h \Rightarrow g \cdot h$ for $h : c \to d$ . We do not list the axioms that these operations satisfy; the interested reader can consult, e.g., Def. 2.1 of Ahrens et al. (2021).

We occasionally write $1_a$ for $\operatorname{id}_1(a)$ and $1_f$ for $\operatorname{id}_2(\,f)$ .

Remark 2. We do not generally require that our bicategories (and displayed bicategories, see Definition 4) are univalent in the sense of Ahrens et al. (2021).

Sometimes it is still interesting to assume that a given (displayed) bicategory is univalent; in such cases, fibrations are better behaved, since lifts can be shown to be actually unique rather than just essentially unique (see, for instance, Proposition 26). Whenever we state such a result, the assumption on the (displayed) bicategory to be univalent is stated explicitly.

We denote by $\mathsf{Cat}$ the bicategory of categories, and by $\mathsf{Grpd}$ the bicategory of groupoids. The bicategory $\mathsf{B}^{\mathsf{op}}$ has the same objects as $\mathsf{B}$ , but 1-cells from x to y in $\mathsf{B}^{\mathsf{op}}$ are 1-cells $f : y \rightarrow x$ in $\mathsf{B}$ . The 2-cells in $\mathsf{B}^{\mathsf{op}}$ are 2-cells in $\mathsf{B}$ . The bicategory $\mathsf{B}^{\mathsf{co}}$ has the same objects and 1-cells as $\mathsf{B}$ , but 2-cells from f to g in $\mathsf{B}^{\mathsf{co}}$ are the same as 2-cells from g to f in $\mathsf{B}$ .

Definition 3 Given two bicategories $\mathsf{B}$ and $\mathsf{B}'$ , a pseudofunctor $F : \mathsf{B} \to \mathsf{B}'$ is given by maps $F_0 : \mathsf{B}_0 \to \mathsf{B}'_0$ , $F_1 : (a\to b) \to (F_0a \to F_0b)$ , ² and $p_2 : (\,f \Rightarrow g) \to (F_1f \Rightarrow F_1g)$ , preserving structure on 1-cells up to invertible 2-cells in $\mathsf{B}'$ (specified as part of the functor F) and preserving structure on 2-cells up to equality.

We build complicated bicategories from simpler ones by adding structure at all dimensions. The additional structure should come with its own composition and identity, which should lie suitably over composition and identity of the original bicategory. This idea is formalized in the notion of displayed bicategory – a layer of data over a base bicategory – and the resulting total bicategory – the bicategory of pairs $(b,\overline{b})$ of a cell b in the base and a cell $\overline{b}$ “over” b. We also obtain a pseudofunctor from the total bicategory into the base, given at all dimensions by the first projection.

Definition 4 (Ahrens et al. 2021, Def. 6.1, disp_bicat). Let $\mathsf{B}$ be a bicategory. A displayed bicategory $\mathsf{D}$ over $\mathsf{B}$ consists of

1. (1) for any $b : \mathsf{B}_0$ , a type ${{{{\mathsf{D}}_{b}}}}$ of objects over b;

2. (2) for any $f : a\to b$ and $x : {{{{\mathsf{D}}_{a}}}}$ and $y : {{{{\mathsf{D}}_{b}}}}$ , a type $x \xrightarrow{f} y$ of 1-cells over f;

3. (3) for any $\theta :\, f \Rightarrow g$ and $\overline{f} : x \xrightarrow{f} y$ and $\overline{g} : x \xrightarrow{g} y$ , a set $\overline{f} \buildrel {\theta} \over \Rightarrow \overline{g}$ of 2-cells over $\theta$ ;

together with suitably typed composition (over composition in $\mathsf{B}$ ) and identity (over identity in $\mathsf{B}$ ) for both 1- and 2-cells. These operations are subject to “axioms over axioms in $\mathsf{B}$ ”.

Definition 5 (Ahrens et al. 2021, Def. 6.2, total_bicat). Given a displayed bicategory $\mathsf{D}$ over $\mathsf{B}$ , we define the total bicategory $\int\!\!{\mathsf{D}}$ to have, as cells at dimension i, pairs $(b,\overline{b})$ where b is a cell of $\mathsf{B}$ at dimension i and $\overline{b}$ is a cell of $\mathsf{D}$ over b, with the obvious source and target.

We define the projection pseudofunctor $\pi : \int\!\!{\mathsf{D}} \to \mathsf{B}$ to be given, on any cell, by $(b,\overline{b})\mapsto b$ .

Definition 6 Suppose that we have a bicategory $\mathsf{B}$ , a predicate $P_0$ on the 0-cells (by which we mean a proposition $P_0(a)$ for every 0-cell a), and a predicate $P_1$ on the 1-cells. Furthermore, we assume that $P_1$ is closed under identity and composition; that is, $P_1(\!\operatorname{id}(x))$ holds for every x satisfying $P_0$ and that for all $f : x \rightarrow y$ and $g : y \rightarrow z$ between 0-cells satisfying $P_0$ we have $P_1(\,f \cdot g)$ if we have both $P_1(\,f)$ and $P_1(g)$ . Then we define a displayed bicategory $\mathsf{SubBicat}(P_0, P_1)$ on $\mathsf{B}$ such that

• the type of displayed objects over x is $P_0(x)$ ;

• the type of displayed 1-cells over $f : x \rightarrow y$ is $P_1(\,f)$ ; and

• the type of displayed 2-cells over $\theta :\, f \Rightarrow g$ is the unit type.

The total bicategory of this bicategory selects 0-cells and 1-cells from the original bicategory $\mathsf{B}$ . Its objects are objects $x : \mathsf{B}$ such that $P_0(x)$ , its 1-cells are 1-cells $f : x \rightarrow y$ in $\mathsf{B}$ such that $P_1(\,f)$ , and its 2-cells are the same as 2-cells $\tau :\, f \Rightarrow g$ in $\mathsf{B}$ . The projection pseudofunctor $\pi : \mathsf{SubBicat}(P_0, P_1) \to \mathsf{B}$ is the inclusion.

Remark 7. Note that Definition 6 is defined slightly differently in the formalization. In we do not require that $P_0$ and $P_1$ are propositions. Instead, we only require this in the theorem that shows the univalence of this displayed bicategory.

We instantiate Definition 6 to define bicategories of categories with a certain structure.

Example 8 We define the following displayed bicategories over $\mathsf{Cat}$ :

• $\mathsf{D}_{\mathsf{Terminal}}$ where $P_0(\mathsf{C})$ says that $\mathsf{C}$ has a terminal object and $P_1(F)$ says that F preserves terminal objects. We denote its total bicategory by $\mathsf{Cat}_{\mathsf{Terminal}}$ .

• $\mathsf{D}_{\mathsf{BinProd}}$ where $P_0(\mathsf{C})$ says that $\mathsf{C}$ has binary products and $P_1(F)$ says that F preserves binary products. We denote its total bicategory by $\mathsf{Cat}_{\mathsf{BinProd}}$ .

• $\mathsf{D}_{\mathsf{Pullback}}$ where $P_0(\mathsf{C})$ says that $\mathsf{C}$ has pullbacks and $P_1(F)$ says that F preserves pullbacks. We denote its total bicategory by $\mathsf{Cat}_{\mathsf{Pullback}}$ .

• $\mathsf{D}_{\mathsf{FinLim}}$ where $P_0(\mathsf{C})$ says that $\mathsf{C}$ has finite limits and $P_1(F)$ says that F preserves finite limits. We denote its total bicategory by $\mathsf{Cat}_{\mathsf{FinLim}}$ .

• $\mathsf{D}_{\mathsf{Initial}}$ where $P_0(\mathsf{C})$ says that $\mathsf{C}$ has an initial object and $P_1(F)$ says that F preserves initial objects. We denote its total bicategory by $\mathsf{Cat}_{\mathsf{Initial}}$ .

• $\mathsf{D}_{\mathsf{BinSum}}$ where $P_0(\mathsf{C})$ says that $\mathsf{C}$ has binary coproducts and $P_1(F)$ says that F preserves binary coproducts. We denote its total bicategory by $\mathsf{Cat}_{\mathsf{BinSum}}$ .

The above examples can be defined using Definition 6 assuming that the categories involved are univalent, since then the type families $P_0$ and $P_1$ stating a choice of limits are indeed predicates. For nonunivalent categories, one could consider instead the truncated predicates stating mere existence of limits.

The total bicategories of the displayed bicategories in Example 8 are bicategories of categories with certain (co)limits. In addition, we can combine the structure of these by taking the product of the suitable displayed bicategories. Note that we could use similar methods to construct bicategories of extensive categories, regular categories, exact categories, and (pre)toposes.

The following (displayed) bicategories are used:

Example 9 Given bicategories $\mathsf{B}_1$ and $\mathsf{B}_2$ , we define a displayed bicategory ${{{{\mathsf{B}_1}^{+{\mathsf{B}_2}}}}}$ over $\mathsf{B}_1$ as follows:

• The displayed 0-cells over $x : \mathsf{B}_1$ are 0-cells $y : \mathsf{B}_2$ .

• The displayed 1-cells over $f : x_1 \to x_2$ from $y_1 : \mathsf{B}_2$ to $y_2 : \mathsf{B}_2$ are 1-cells $g : y_1 \to y_2$ in $\mathsf{B}_2$ .

• The displayed 2-cells over $\theta :\, f \Rightarrow g$ from $g_1 : y_1 \rightarrow y_2$ to $g_2 : y_1 \rightarrow y_2$ are 2-cells $\tau : g_1 \Rightarrow g_2$ in $\mathsf{B}_2$ .

The total bicategory is $\int\!\!{{\mathsf{B}_1}^{+{\mathsf{B}_2}}} \simeq \mathsf{B}_1 \times \mathsf{B}_2$ with projection $\pi : \mathsf{B}_1 \times \mathsf{B}_2 \to \mathsf{B}_1$ .

Example 10 Let $\mathsf{B}$ be a bicategory. Define a displayed bicategory $\mathsf{B}^{\downarrow}$ over $\mathsf{B}$ as follows:

• The displayed objects over $y : \mathsf{B}$ are 1-cells $x \rightarrow y$ .

• The displayed 1-cells over $g : y_1 \rightarrow y_2$ from $h_1 : x_1 \rightarrow y_1$ to $h_2 : x_2 \rightarrow y_2$ are pairs consisting of a 1-cell $f : x_1 \rightarrow x_2$ and an invertible 2-cell $\gamma : g \cdot h_2 \Rightarrow h_1 \cdot f$ .

• Given displayed 1-cells $f_1 : x_1 \rightarrow x_2$ with $\gamma_1 : g_1 \cdot h_2 \Rightarrow h_1 \cdot f_1$ , and $f_2 : x_1 \rightarrow x_2$ with $\gamma_2 : g_2 \cdot h_2 \Rightarrow h_1 \cdot f_2$ , we define the displayed 2-cells over $\theta : g_1 \Rightarrow g_2$ from $(\,f_1, \gamma_1)$ to $(\,f_2, \gamma_2)$ as 2-cells $\tau :\, f_1 \Rightarrow f_2$ such that $\gamma_1 \bullet (h_1 \vartriangleleft \tau) = (\theta \vartriangleright h_2) \bullet \gamma_2$ .

The generated total bicategory is the arrow bicategory, $\int\!\!{\mathsf{B}^{\downarrow}} = \mathsf{B}^{\rightarrow}$ with projection given by the codomain, ${{{\mathsf{cod}}}} : \mathsf{B}^{\rightarrow} \to \mathsf{B}$ .

In the next example, we write $\mathsf{StrictCat}$ for the bicategory of strict categories and $\underline{\mathsf{StrictCat}}$ for the category of strict categories.

Example 11 We define a displayed bicategory $\mathsf{IndexedCat}$ over $\mathsf{StrictCat}$ as follows:

• The displayed objects over $\mathsf{C} : \mathsf{StrictCat}$ are functors $G : \mathsf{C} \rightarrow \underline{\mathsf{StrictCat}}$ .

• The displayed 1-cells over $F : \mathsf{C}_1 \rightarrow \mathsf{C}_2$ from $G_1 : \mathsf{C}_1 \rightarrow \underline{\mathsf{StrictCat}}$ to $G_2 : \mathsf{C}_2 \rightarrow \underline{\mathsf{StrictCat}}$ are natural transformations $\gamma : G_1 \Rightarrow F \cdot G_2$ .

• The displayed 2-cells over $n : F_1 \Rightarrow F_2$ from $\gamma_1 : G_1 \Rightarrow F_1 \cdot G_2$ to $\gamma_2 : G_1 \Rightarrow F_2 \cdot G_2$ are proofs that for all $x : \mathsf{C}$ we have $\gamma_1(x) \cdot G_2(n(x)) = \gamma_2(x)$ .

The associated projection pseudofunctor $\pi : \int\!\!{\mathsf{IndexedCat}} \to \mathsf{StrictCat}$ maps functors $\mathsf{C} \rightarrow \underline{\mathsf{StrictCat}}$ to their domain.

Example 12 We define a displayed bicategory $\mathsf{OpCleav}$ over $\mathsf{Cat}$ as follows:

• The displayed objects over $\mathsf{C} : \mathsf{Cat}$ are displayed categories $\mathsf{D}$ over C together with an opcleaving.

• The displayed 1-cells over $F : \mathsf{C}_1 \rightarrow \mathsf{C}_2$ from $\mathsf{D}_1$ to $\mathsf{D}_2$ are displayed functors $\overline{F}$ from $\mathsf{D}_1$ to $\mathsf{D}_2$ that preserve opcartesian morphisms.

• The displayed 2-cells over $\theta : F \Rightarrow G$ from $\overline{F} : \mathsf{D}_1 \xrightarrow{F} \mathsf{D}_2$ to $\overline{G} : \mathsf{D}_1 \xrightarrow{G} \mathsf{D}_2$ are displayed natural transformations from $\overline{F}$ to $\overline{G}$ over $\theta$ .

The associated projection pseudofunctor $\pi : \int\!\!{\mathsf{OpCleav}} \to \mathsf{Cat}$ maps any opcleaving to its codomain category.

Similarly, we define displayed bicategories $\mathsf{Cleav}$ and $\mathsf{IsoFib}$ of cleavings and isocleavings, respectively.

The idea of displayed (bi)categories transfers to functors:

Definition 13 (Ahrens et al. 2021, Def. 8.2, disp_psfunctor). Given $F : \mathsf{B} \to \mathsf{B}'$ and $\mathsf{D}$ and $\mathsf{D}'$ displayed bicategories over $\mathsf{B}$ and $\mathsf{B}'$ , respectively, a displayed pseudofunctor $\overline{F}$ over F consists of

• for all objects $x : \mathsf{B}$ and $\overline{x} : {{{{\mathsf{D}}_{x}}}}$ an object $\overline{F}(\overline{x}) : {{{{\mathsf{D}'}_{F(x)}}}}$ ;

• for all displayed morphisms $\overline{f} : \overline{x} \xrightarrow{f} \overline{y}$ , a displayed 1-cell $\overline{F}(\overline{f}) : \overline{F}(\overline{x}) \xrightarrow{F(\,f)} \overline{F}(\overline{y})$ ;

• for all displayed 2-cells $\overline{\theta} : \overline{f} \buildrel {\theta} \over \Rightarrow\overline{g}$ , a displayed 2-cell $\overline{F}(\overline{\theta}) : \overline{F}(\overline{f}) \buildrel {F(\theta)} \over \Rightarrow \overline{F}(\overline{g})$ ;

• coherence isomorphisms for identity and composition of displayed 1-cells, over the analogous isomorphisms in the base;

• satisfying suitable equations over the corresponding equations in the base.

We denote by $\int\!\!{\overline{F}} : \int\!\!{\mathsf{D}} \to \int\!\!{\mathsf{D}'}$ the induced total pseudofunctor.

Remark 14. The square of pseudofunctors

induced by $\overline{F}$ over F commutes up to judgmental equality.

Furthermore, we need pullbacks and products in bicategories.

Definition 15 Let $\mathsf{B}$ be a bicategory, and suppose we have two 1-cells $f : a \rightarrow c$ and $g : b \rightarrow c$ . A pullback structure for f and g on an object $x : \mathsf{B}$ together with two 1-cells $\pi_1 : x \rightarrow a$ and $\pi_2 : x \rightarrow b$ and an invertible 2-cell $\gamma : p \cdot f \Rightarrow q \cdot g$ is given by the following data:

• for all 1-cells $p' : z \rightarrow a$ and $q' : z \rightarrow b$ and invertible 2-cells $\gamma' : p' \cdot f \Rightarrow q' \cdot g$ , we have a 1-cell $u : z \rightarrow x$ together with invertible 2-cells $\theta : u \cdot p \Rightarrow p'$ and $\tau : u \cdot q \Rightarrow q'$ such that

  $ \alpha \bullet \theta \vartriangleright f \bullet \gamma' = u \vartriangleleft \gamma \bullet \alpha^{-1} \bullet \tau \vartriangleright g. $

• for all 1-cells $u_1, u_2 : z \rightarrow x$ and 2-cells $\theta : u_1 \bullet p \Rightarrow u_2 \bullet p$ and $\tau : u_1 \bullet q \Rightarrow u_2 \bullet q$ such that

  $ u_1 \vartriangleleft \gamma \bullet \alpha \bullet \tau \vartriangleright q \bullet \alpha^{-1} = \alpha \bullet \theta \vartriangleright f \bullet \alpha^{-1} \bullet u_2 \vartriangleleft \gamma, $
  we have a unique 2-cell $\nu : u_1 \Rightarrow u_2$ such that $\nu \vartriangleright p = \theta$ and $\nu \vartriangleright q = \tau$ .

In Definition 15, it is irrelevant if we postulate data to be given explicitly or to merely exist, provided the bicategory $\mathsf{B}$ is univalent:

Proposition 16 If $\mathsf{B}$ is univalent, then the type of pullback structures on $(x,\pi_1,\pi_2, \gamma)$ is a proposition.

Remark 17. There are different notions of pullback in bicategories depending on whether $p \cdot f$ and $q \cdot g$ are postulated to be related up to an equality, invertible 2-cell or even just a 2-cell. In Definition 15, the square commutes up to invertible 2-cell. One could also define strict pullbacks: this is done similarly to Definition 15, but all involved squares must commute up to equality rather than just up to invertible 2-cell.

Example 18 The bicategory of groupoids has pullbacks.

The bicategory $\mathsf{Cat}$ also has pullbacks, and they are given by iso-comma categories. These are defined as follows: given categories $\mathsf{C}_1$ , $\mathsf{C}_2$ , and $\mathsf{C}_3$ and functors $F : \mathsf{C}_1 \rightarrow \mathsf{C}_3$ and $G : \mathsf{C}_2 \rightarrow \mathsf{C}_3$ , we define the iso-comma category $F \mathbin{/_\simeq} G$

• Its objects consist of objects $x : \mathsf{C}_1$ and $y : \mathsf{C}_2$ together with an isomorphism $f : F(x) \rightarrow G(y)$

• The morphisms from $(x_1, y_1, f_1)$ to $(x_2, y_2, f_2)$ consists of morphisms $g : x_1 \rightarrow x_2$ and $h : y_1 \rightarrow y_2$ such that the following diagram commutes:

We define functors $\pi_1^\simeq : F \mathbin{/_\simeq} G \rightarrow \mathsf{C}_1$ and $\pi_2^\simeq : F \mathbin{/_\simeq} G \rightarrow \mathsf{C}_2$ and a natural isomorphism $n^\simeq : \pi_1^\simeq \cdot F \Rightarrow \pi_2^\simeq \cdot G$ . The category $F \mathbin{/_\simeq} G$ together with the functors $\pi_1^\simeq,\pi_2^\simeq$ and natural isomorphism $n^\simeq$ is universal among such data, making it the pullback of F and G.

Example 19 The bicategories defined in Example 8 all have pullbacks as well. This is because taking the iso-comma category preserves the desired (co)limits and the projections and pairing functors preserve them.

As a special case of pullbacks in the presence of terminal objects, we can define products in bicategories If $\mathsf{B}$ has chosen products, we write $x \times y$ for the product of x and y, and we denote the projections by $\pi_1 : x \times y \rightarrow x$ and $\pi_2 : x \times y \rightarrow y$ .

Notation 20. In the following, given a cloven fibration, we notate the pullback (or reindexing) of A along f by ${{{{f}^*{A}}}}$ . Given a cloven opfibration, we notate the pushforward of A along f by ${{{{f}_!{A}}}}$ .

4. Comprehension Bicategories

In this section, we define the notion of global cleaving and local (op)cleavings of bicategories. Afterward, we use these notions to define comprehension bicategories. We are guided by Buckley (2014), where local and global fibrations are defined, and we add definitions for local cloven iso- and opfibrations. However, there is an important difference: while Buckley works in a set-theoretic setting, we reformulate the definitions in a type-theoretic setting using the displayed technology developed by Ahrens et al. (2021) and reviewed in Section 3 – see also Remark 25.

Throughout this section, we assume that $\mathsf{B}$ is a bicategory and $\mathsf{D}$ is a displayed bicategory over $\mathsf{B}$ .

Definition 21 (Buckley 2014, Def. 3.1.1, cartesian_1cell). Let $f : a \to b$ be a 1-cell in $\mathsf{B}$ , and let $\overline{f} : \overline{a} \xrightarrow{f} \overline{b}$ be a displayed 1-cell over f in $\mathsf{D}$ . A cartesian structure on $\overline{f}$ consists of the following data. Note that we draw diagrams in the displayed category on the left side and diagrams in the base category on the right side.

1. (1) For any $\overline{g} : \overline{c} \xrightarrow{h \cdot f} \overline{b}$ , a choice of a displayed morphism $\overline{h} : \overline{c} \xrightarrow{h} \overline{a}$ and a displayed isomorphism $\theta$ over the identity isomorphism on $h \cdot f$ in $\mathsf{B}$ .

We call $(\overline{h},\theta)$ the lift of $(h,\overline{g})$ .

1. (2) Given lifts $(\overline{h}_1,\theta_1)$ and $(\overline{h}_2, \theta_2)$ of $(h_1,\overline{g}_1)$ and $(h_2,\overline{g}_2)$ , respectively, and $\delta : h_1 \Rightarrow h_2$ , and a 2-cell $\overline{\sigma} : \overline{g}_1 \Rightarrow \overline{g}_2$ over $\delta \vartriangleright f$ , we have a unique 2-cell $\overline{\delta} : \overline{h}_1 \Rightarrow \overline{h}_2$ over $\delta$ such that $\overline{\delta}\vartriangleright \overline{f} \bullet \theta_2 = \theta_1 \bullet \overline{\sigma}$ .

Given a cartesian structure on $\overline{f}$ , we call ${{{\mathsf{F_1}(\overline{f},\overline{g})}}} := \overline{h}$ and ${{{\mathsf{F_2}(\overline{f},\overline{g})}}} := \theta$ . We also call ${{{\mathsf{E}(\delta,\overline{\sigma})}}} := \overline{\delta}$ .

Proposition 22. We have the following cartesian 1-cells:

• () The identity $\overline{\operatorname{id}_1} : \overline{a} \rightarrow \overline{a}$ is cartesian.

• () If $\overline{f} : \overline{a} \rightarrow \overline{b}$ and $\overline{g} : \overline{b} \rightarrow \overline{c}$ are cartesian, then so is $\overline{f} \cdot \overline{g}$ .

Problem 23. Given two cartesian 1-cells $\overline{f} : \overline{a} \rightarrow \overline{b}$ and $\overline{f}' : \overline{a}' \rightarrow \overline{b}$ , to construct an adjoint equivalence $e : \overline{a} \rightarrow \overline{a}'$ over the identity and an invertible 2-cell from $\overline{f}$ to $e \cdot \overline{f}'$ .

Construction 24 for Problem 23; (). The 1-cells of the adjoint equivalence are constructed as cartesian factorizations (first item of Definition 21). In that way, we also obtain the desired invertible 2-cell.

Remark 25. Recall that a displayed 1-cell $\overline{f} : \overline{a} \xrightarrow{f} \overline{b}$ in $\mathsf{D}$ gives rise to the 1-cell $(\,f,\overline{f})$ in the total bicategory $\int\!\!{\mathsf{D}}$ . The definition of cartesian structure on $\overline{f}$ in $\mathsf{D}$ of Definition 21 gives rise to a notion of cartesian structure for $(\,f,\overline{f})$ in $\int\!\!{\mathsf{D}}$ . By expressing the definition of cartesian 1-cell in the displayed bicategory (instead of in the resulting projection $\pi : \int\!\!{\mathsf{D}} \to \mathsf{B}$ ), we can postulate that a lift in $\int\!\!{\mathsf{D}}$ lies definitionally over a given cell in $\mathsf{B}$ , not just modulo an invertible 2-cell.

Buckley (2014) shows, in Remark 3.1.6, that these two definitions are equivalent.

Proposition 26 (). Suppose that $\mathsf{D}$ is a univalent displayed bicategory over $\mathsf{B}$ , and let $\overline{f}$ be a displayed 1-cell in $\mathsf{D}$ over f in $\mathsf{B}$ . Then the type of cartesian 1-cell structures on $\overline{f}$ is a proposition.

Definition 27 A global cleaving on $\mathsf{D}$ is a choice, for any $f : a \to b$ in $\mathsf{B}$ and $\overline{b} : {{{{\mathsf{D}}_{b}}}}$ , of

1. (1) a displayed object $\overline{a}$ over a;

2. (2) a displayed 1-cell $\overline{f} : \overline{a} \xrightarrow{f} \overline{b}$ ;

3. (3) a cartesian structure on $\overline{f}$ .

Given a global cleaving on $\mathsf{D}$ , we use the notation $\overline{b}[f] := \overline{a}$ and $L_{f}(\overline{b}) := \overline{f}$ to denote the choice given by the cleaving.

Remark 28. The notion of global cleaving as in Definition 27 gives rise to a notion of cloven fibration on the total bicategory $\int\!\!{\mathsf{D}}$ .

Next we look at local cleavings and opcleavings. A 2-cell is opcartesian if and only if it is opcartesian in the 1-categorical sense for the hom-functor. However, in the formalization, we give the following direct definition not relying on hom-categories and prove the characterization via hom-categories afterward Similarly, we give an unfolded definition of local opcleaving.

Definition 29 Suppose we have 1-cells $f, g : x \rightarrow y$ , a 2-cell $\theta :\, f \Rightarrow g$ , and displayed objects $\overline{x}$ and $\overline{y}$ over x and y, respectively. Given displayed 1-cells $\overline{f} : \overline{x} \xrightarrow{f} \overline{y}$ and $\overline{g} : \overline{x} \xrightarrow{g} \overline{y}$ and a displayed 2-cell $\overline{\theta} : \overline{f} \buildrel {\theta} \over \Rightarrow \overline{g}$ , we say that $\overline{\theta}$ is 2-opcartesian (or just opcartesian) if for all 1-cells $h : x \rightarrow y$ , displayed 1-cells $\overline{h} : \overline{x} \xrightarrow{h} \overline{y}$ , 2-cells $\tau : g \Rightarrow h$ , and displayed 2-cells $\overline{\gamma} : \overline{f} \buildrel {\tau \bullet \theta} \over \Rightarrow \overline{h}$ , there is a unique displayed 2-cell $\overline{\tau} : \overline{g} \buildrel {\tau} \over \Rightarrow \overline{h}$ such that $\overline{\theta} \bullet \overline{\tau} = \overline{\gamma}$ .

Being an opcartesian 2-cell is always a property. The notion of cartesian 2-cells is analogous.

Definition 30 A local opcleaving on $\mathsf{D}$ is given by, for every $\theta :\, f \Rightarrow g$ and $\overline{f} : \overline{x} \xrightarrow{f} \overline{y}$ , a displayed 1-cell $\overline{g} : \overline{x} \xrightarrow{g} \overline{y}$ and an opcartesian 2-cell $\overline{\theta} : \overline{f} \buildrel {\theta} \over \Rightarrow \overline{g}$ .

The notions of local cleaving and local isocleaving are defined analogously.

Remark 31. Every displayed bicategory on a univalent bicategory has a local isocleaving. The construction is the same as for categories

(Ahrens and Lumsdaine 2019, Construction 5.12).

Remark 32. The notions of opcartesian 2-cell and of local opcleaving as in Definition 30 give rise to notions of opcartesian 2-cell and of cloven local opfibration on the total bicategory $\int\!\!{\mathsf{D}}$ .

Note that one can construct a local isocleaving from either a local cleaving or a local opcleaving.

Proposition 33 Suppose that $\mathsf{B}$ is a univalent bicategory and $\mathsf{D}$ is a univalent displayed bicategory over $\mathsf{D}$ . Then the types of local (resp. global) (op)cleavings on $\mathsf{D}$ are propositions.

Now let us look at some examples of these notions.

Example 34. The trivial displayed bicategory ${{{{\mathsf{B}_1}^{+{\mathsf{B}_2}}}}}$ over $\mathsf{B}_1$ comes equipped with a cloven global fibration. Cartesian 1-cells in ${{{{\mathsf{B}_1}^{+{\mathsf{B}_2}}}}}$ correspond to adjoint equivalences in $\mathsf{B}_2$ . As such, we can take the identity 1-cell as the global lift. In addition, ${{{{\mathsf{B}_1}^{+{\mathsf{B}_2}}}}}$ also has both a cloven local fibration and a cloven local opfibration.

Example 35. Suppose that $\mathsf{B}$ is a locally groupoidal bicategory with pullbacks. Since cartesian 1-cells in $\mathsf{B}^{\downarrow}$ correspond to pullback squares, we can construct a global cleaving for $\mathsf{B}^{\downarrow}$ by taking pullbacks. Note that all 2-cells in $\mathsf{B}^{\downarrow}$ are cartesian, because $\mathsf{B}$ is locally groupoidal, and thus $\mathsf{B}^{\downarrow}$ also has a local cleaving and a local opcleaving.

Example 36 The displayed bicategory $\mathsf{IndexedCat}$ has a global cleaving and a local opcleaving. To construct these, we first observe that a displayed 1-cell $\gamma : G_1 \Rightarrow F_1 \cdot G_2$ from $G_1 : \mathsf{C}_1 \rightarrow \underline{\mathsf{StrictCat}}$ to $G_2 : \mathsf{C}_2 \rightarrow \underline{\mathsf{StrictCat}}$ is cartesian if and only if it is a natural isomorphism. Now we construct a global cleaving for $\mathsf{IndexedCat}$ as follows: whenever we have functors $F : \mathsf{C}_1 \rightarrow \mathsf{C}_2$ and $G : \mathsf{C}_2 \rightarrow \underline{\mathsf{StrictCat}}$ , then we also get a functor $F \cdot G : \mathsf{C}_1 \rightarrow \underline{\mathsf{StrictCat}}$ .

Every displayed 2-cell in $\mathsf{IndexedCat}$ is opcartesian. To find local opcartesian lifts, suppose that we have functors $F_1, F_2 : \mathsf{C}_1 \rightarrow \mathsf{C}_2$ , $G_1 : \mathsf{C}_1 \rightarrow \underline{\mathsf{StrictCat}}$ and $G_2 : \mathsf{C}_2 \rightarrow \underline{\mathsf{StrictCat}}$ , and natural transformations $n : F_1 \Rightarrow F_2$ and $\gamma : G_1 \Rightarrow F_1 \cdot G_2$ . Our goal is to construct a natural transformation $G_1 \Rightarrow F_2 \cdot G_2$ , and for the desired transformation we take $\gamma \bullet (n \vartriangleright G_2)$ . Hence, $\mathsf{IndexedCat}$ has a local opcleaving.

Example 37 The displayed bicategory $\mathsf{OpCleav}$ has a global cleaving and a local opcleaving. Given a functor $F : \mathsf{C}_1 \rightarrow \mathsf{C}_2$ and a displayed category $\mathsf{D}_2$ over $\mathsf{C}_2$ , we construct a displayed category $F^*(\mathsf{D}_2)$ over $\mathsf{C}_1$ :

• The displayed objects over $x : \mathsf{C}_1$ are displayed objects in $\mathsf{D}_2$ over F(x).

• The displayed morphisms over $f : x \rightarrow y$ from $\overline{x}$ to $\overline{y}$ are displayed morphisms over $\overline{x} \xrightarrow{F(\,f)} \overline{y}$ .

Note that $F^*(\mathsf{D}_2)$ inherits any opcleaving from $\mathsf{D}_2$ . In addition, we have a displayed functor over F from $F^*(\mathsf{D}_2)$ to $\mathsf{D}_2$ that preserves cartesian morphisms.

Opcartesian 2-cells in $\mathsf{OpCleav}$ correspond to displayed natural transformations of which all components are opcartesian. We form local lifts pointwise. Since displayed 1-cells in $\mathsf{OpCleav}$ preserve cartesian morphisms, cartesian 2-cells are preserved under both left and right whiskering.

Similarly, we can show that the displayed bicategory $\mathsf{Cleav}$ has a global and a local cleaving We finish this section by defining comprehension bicategories. Examples of those are given in Section 5.

Definition 38 A weak comprehension bicategory is given by a bicategory $\mathsf{B}$ , a displayed bicategory $\mathsf{D}$ over $\mathsf{B}$ , and a displayed pseudofunctor $\chi$ over the identity on $\mathsf{B}$ as pictured below,

satisfying the following properties (see also Proposition 33):

1. (1) $\mathsf{D}$ is equipped with a cloven global fibration;

2. (2) $\mathsf{D}$ has a cloven local opfibration;

3. (3) opcartesian 2-cells of $\mathsf{D}$ are preserved under both left and right whiskering.

A comprehension bicategory is a weak comprehension bicategory such that

1. (4) $\chi$ preserves cartesian 1-cells and opcartesian 2-cells.

Remark 39. Recall from Remarks 14, 28, and 32 that the displayed pseudofunctor $\chi : \mathsf{D} \to \mathsf{B}^{\downarrow}$ of Definition 38 gives rise to a strictly commuting diagram of pseudofunctors

with the structure of a global fibration and local opfibration in the sense of

Buckley (2014).

Remark 40. In the definition of comprehension categories, one usually requires that the functor $\chi$ preserves cartesian morphisms. The analogous requirement for comprehension bicategories is that the pseudofunctor $\chi$ preserves both cartesian 1-cells and opcartesian 2-cells – this is condition 4 in Definition 38.

We have factored out this requirement, since for our interpretation of the language $\mathsf{BTT}$ (introduced in Section 8), we do not need this condition; that is, we can interpret $\mathsf{BTT}$ in any weak comprehension bicategory. The reason has to do with how we interpret terms of the language $\mathsf{BTT}$ in a (weak) comprehension bicategory. Traditionally, in a comprehension category, terms of $\mathsf{MLTT}$ are interpreted as sections of projections. Specifically, every type A in context $\Gamma$ gives rise, in the interpretation, to a morphism $\pi_A : \Gamma . A \rightarrow \Gamma$ in the arrow category. A term of type A in context $\Gamma$ in $\mathsf{MLTT}$ is then interpreted as a section of $\pi_A$ .

In our setting, terms of $\mathsf{BTT}$ will be interpreted differently. Instead of interpreting $\mathsf{BTT}$ terms as sections of projections, we interpret them as morphisms over the identity. More concretely, in a bicategory $\mathsf{D}$ displayed over $\mathsf{B}$ , a term in context $\Gamma$ of type B with source A of $\mathsf{BTT}$ is interpreted as a morphism from A to B over the identity of $\Gamma$ .

In the 1-categorical case, these two ways of interpreting terms are equivalent in many examples. The reason is that, in practice, most comprehension categories are full, which means that $\chi$ is fully faithful, and that every fiber has a terminal object. From these two assumptions, one can conclude that these two ways of interpreting terms are actually equivalent. However, in the bicategorical setting, these two ways are often not equivalent: for example, in the comprehension bicategory of displayed categories with opcleavings, i.e. opfibrations (Examples 12, 37, and 45). There, morphisms over the identity are required to preserve opcartesian morphisms, but such a requirement is not present for sections of the projection. If one were to include $\mathsf{MLTT}$ style terms (which are interpreted as sections of projections) in $\mathsf{BTT}$ , then to give an interpretation one would also need that $\chi$ preserves cartesian 1-cells and opcartesian 2-cells in order to interpret substitution. This is why we present here both definitions.

In short, all the examples presented in Section 5 are comprehension bicategories; the interpretation of $\mathsf{BTT}$ given in Section 8 only requires a weak comprehension bicategory.

Remark 41. Contravariant and isovariant comprehension bicategories are defined analogously with the notions of (iso)cleaving and (iso)cartesian taking the place of opcleaving and opcartesian in Items 2 and 3 of Definition 38. Some of our examples of comprehension bicategories can similarly be equipped with a contravariant and isovariant comprehension structure.

5. Examples of Comprehension Bicategories

In this section, we give several (classes of) instances of comprehension bicategories. In some of these instances, we recognize structures studied previously in the context of higher-dimensional and directed type theory.

Example 42 Suppose we have a bicategory $\mathsf{B}$ with products. Then we have the following comprehension bicategory

The displayed pseudofunctor $\chi : {{{{\mathsf{B}}^{+{\mathsf{B}}}}}} \rightarrow \mathsf{B}^{\downarrow}$ sends the object $y_2$ over $y_1$ to the product projection $y_1 \times y_2 \to y_1$ , that is, the corresponding total pseudofunctor $\mathsf{B} \times \mathsf{B} \to \mathsf{B}^{\downarrow}$ is defined by $(y_1,y_2)\mapsto \pi_1 : y_1 \times y_2 \to y_1$ .

Example 42 corresponds roughly to the semantics studied by Fiore and Saville (2019), but without the type formers.

Another example of a comprehension bicategory comes from locally groupoidal bicategories, such as $\mathsf{Grpd}$ .

Example 43 Let $\mathsf{B}$ be a locally groupoidal bicategory with pullbacks. Then we get the following comprehension bicategory

Since every 2-cell is opcartesian in $\mathsf{B}^{\downarrow}$ if $\mathsf{B}$ is locally groupoidal, the displayed bicategory $\mathsf{B}^{\downarrow}$ has a local opcleaving.

Example 43 models undirected reductions between terms. It is thus related to the groupoid model of type theory by Hofmann and Streicher (1994) and to the definition of comprehension 2-category by Garner (2009). A more detailed comparison to Garner’s comprehension 2-categories is given in Remark 65.

We can also consider directed versions of this example by using categories instead of groupoids.

Example 44 We construct the following comprehension bicategory using cloven split opfibrations.

To define $\chi$ , we use the Grothendieck construction. Specifically, from a functor $G : \mathsf{C} \rightarrow \underline{\mathsf{StrictCat}}$ we construct a category $\int G$ as follows

1. (1) The objects of $\int G$ are pairs (x, y) where $x : \mathsf{C}$ and $y : G(x)$ .

2. (2) The morphisms from $(x_1, y_1)$ to $(x_2, y_2)$ are pairs $(\,f, g)$ where $f : x_1 \rightarrow x_2$ and $g : G(\,f)(y_1) \rightarrow y_2$ .

Note that we also have a projection $\pi_1 : \int G \rightarrow \mathsf{C}$ . In addition, from a displayed 1-cell $\gamma : G_1 \Rightarrow F \cdot G_2$ , we get a functor $\int \gamma : \int G_1 \rightarrow \int G_2$ and a natural isomorphism $\gamma_c : \pi_1 \cdot F \Rightarrow \int \gamma \cdot \pi_1$ . If we have $p : \gamma_1(x) \cdot G_2(n(x)) = \gamma_2(x)$ for every $x : \mathsf{C}_1$ , then we get a natural transformation $\int p$ from $\int \gamma_1$ to $\int \gamma_2$ .

Example 44 is related to the interpretations given by Licata andHarper (2011) and North (2019) in their works on directed type theories, albeit without considering type formers. However, their notion of term, in both the syntax and the interpretation, is different from ours; see Section 10 for details.

In Example 44, contexts are categories and types over a context $\mathsf{C}$ are cloven split opfibrations on $\mathsf{C}$ . We also consider a version of this interpretation where there are more types: instead of looking at only those opfibrations that are split, all opfibrations are considered.

Example 45 From opcleavings we build the following comprehension bicategory:

The pseudofunctor $\chi$ sends a displayed category $\mathsf{D}$ over $\mathsf{C}$ to the functor $\pi_1 : \int\!\!{\mathsf{D}} \rightarrow \mathsf{C}$ .

Similarly, we can define a contravariant comprehension bicategory using cleavings instead of opcleavings.

6. Internal Street (Op)Fibrations

In this section, we discuss Street (op)fibrations internal to a fixed bicategory $\mathsf{B}$ . They will yield, in Section 7, many examples of comprehension bicategories, see Example 57 and Remark 59. The examples of Street opfibrations internal to bicategories of stacks are particularly interesting (see Remark 59).

Note that $\mathsf{B}^{\downarrow}$ comes equipped with a cloven global fibration if $\mathsf{B}$ has pullbacks. However, to obtain a local (op)cleaving, we used that $\mathsf{B}$ is locally groupoidal in Example 35. This assumption is avoided in Example 37 where $\mathsf{B} = \mathsf{Cat}$ : instead of looking at arbitrary functors, one only considers the opfibrations. We can generalize this idea to arbitrary bicategories by using internal Street (op)fibrations (Buckley 2014).

The displayed bicategory $\mathsf{OpCleav}$ has a local opcleaving where the desired lifts are constructed pointwise. To generalize this to arbitrary bicategories, we need to adjust this definition so that we can lift arbitrary 2-cells. Furthermore, the notion of cloven Grothendieck opfibration of categories is stricter than appropriate for bicategories. If we have $x \rightarrow y$ and an object over y, then a cloven Grothendieck fibration gives an object strictly living over x, while a Street fibration only gives an object living weakly over x (i.e., up to an isomorphism). More information can be found in work by Loregian and Riehl (Loregian and Riehl 2020, Example 4.1.2).

Definition 46 Let $p : e \rightarrow b$ be a 1-cell in a bicategory $\mathsf{B}$ . Then p is an internal Street fibration if

• For every $x : \mathsf{B}$ , the functor $p_* :$ $\mathsf{B}(x,e)$ $\rightarrow$ $\mathsf{B}(x,b)$ of hom-categories is a Street fibration.

• For every $f : x \rightarrow y$ , the following square is a morphism of Street fibrations:

  

A 1-cell is called an internal Street opfibration if it is an internal Street fibration in $\mathsf{B}^{\mathsf{co}}$

In $\mathsf{Cat}$ , internal Street fibrations are the same as Street fibrations of categories. However, the notion of internal Street fibrations can be applied in a wider variety of settings: for example, one could also look at internal Street fibrations in the bicategories from Example 8 or in presheaves or stacks valued in $\mathsf{Cat}$ . A classical result on internal Street (op)fibrations is that they are closed under taking pullbacks, see Gray (1966) and Street (1980).

Proposition 47 Street (op-)fibrations are closed under pullback. Concretely, given a pullback square

where $p_2$ is a Street (op)fibration, then $p_1$ is so, too.

7. Display Map Bicategories

In this section, we introduce “display map bicategories” as a convenient way to build comprehension bicategories.

Let $\mathsf{B}$ be a bicategory with pullbacks. We aim to construct a displayed bicategory $\mathsf{SOpFib}(\mathsf{B})$ of Street opfibrations over $\mathsf{B}$ with both a global cleaving and a local opcleaving. The construction should be done in a modular and general way, since using the same techniques we aim to construct a displayed bicategory $\mathsf{SFib}(\mathsf{B})$ of Street fibrations over $\mathsf{B}$ with a global and local cleaving. One can imagine more examples, such as the intersection of Street opfibrations with discrete or fully faithful 1-cells.

The common pattern among all these examples is that the displayed bicategory actually represents a subbicategory of the arrow bicategory of $\mathsf{B}$ . In the 1-categorical case, such examples are captured by display map categories (Taylor 1999). We adapt that notion to the bicategorical setting.

However, there is a difference between the 1-categorical and the bicategorical case. A display map category on a 1-category $\mathsf{C}$ is a full subcategory of the arrow category on $\mathsf{C}$ satisfying some requirements. Such a notion would not be useful in the bicategorical case, since neither $\mathsf{SOpFib}(\mathsf{B})$ nor $\mathsf{SFib}(\mathsf{B})$ are full subbicategories of $\mathsf{B}^{\downarrow}$ . Indeed, the 1-cells in $\mathsf{SOpFib}(\mathsf{B})$ and $\mathsf{SFib}(\mathsf{B})$ are required to preserve (op)cartesian cells, which is not required in $\mathsf{B}^{\downarrow}$ . As such, to obtain a notion of display map bicategory that captures these two examples, some care is needed in the definition of display map bicategories.

For that reason, our notion of display map bicategory comes in three different flavors. ³

Definition 48 Let $\mathsf{B}$ be a bicategory. A display map bicategory on $\mathsf{B}$ consists of

1. (1) a predicate P on the 1-cells of $\mathsf{B}$ , and

2. (2) a choice of pullbacks along 1-cells satisfying P

such that

1. (3) if a morphism satisfies P, then it is an internal Street opfibration, and

2. (4) P is closed under pullback.

Given a display map bicategory $\mathsf{B}$ , a display map of $\mathsf{B}$ is a 1-cell of $\mathsf{B}$ together with a proof of the predicate P.

We also define notions of contravariant display map bicategory and isovariant display map bicategory: for the former, condition (3) above is replaced by the condition that the display maps are required to be internal Street fibrations, while for the latter, condition (3) is omitted. The reason for this terminology is that every display map bicategory of a given variance gives rise to a comprehension bicategory with the same variance.

Example 49 Let $\mathsf{B}$ be a locally univalent bicategory with pullbacks. Since $\mathsf{B}$ has pullbacks, pullbacks exist along all 1-cells, and in particular, along Street opfibrations. In addition, Street opfibrations are closed under pullbacks by Proposition 47. Hence, we have a display map bicategory in which the predicate P says that a 1-cell is an internal Street opfibration.

Remark 50 Note that in Example 49, we assume $\mathsf{B}$ to be locally univalent. This is to guarantee that the notion of being a Street opfibration is actually a proposition as required in Definition 48. However, we expect that this assumption can be dropped by suitably truncating the notion of Street opfibration.

Analogously, one can define a contravariant display map bicategory of Street fibrations. There are other examples of display map bicategories as well, for instance discrete Street opfibrations. To define those, we first need the notion of discrete morphisms. ⁴

Definition 51 A 1-cell $f : a \rightarrow b$ in a bicategory $\mathsf{B}$ is called

• faithful if for every object x, the functor $f_* : \underline{\mathsf{B}(x,a)} \rightarrow \underline{\mathsf{B}(x,b)}$ given by postcomposition with f is faithful;

• conservative if for every object x, the functor $f_* : \underline{\mathsf{B}(x,a)} \rightarrow \underline{\mathsf{B}(x,b)}$ is conservative;

• discrete if for every object x, the functor $f_* : \underline{\mathsf{B}(x,a)} \rightarrow \underline{\mathsf{B}(x,b)}$ is faithful and conservative.

Example 52 Let $\mathsf{B}$ be a bicategory with pullbacks. Since both faithful and conservative 1-cells are closed under pullbacks, discrete 1-cells are as well. Hence, we get a display map bicategory of discrete Street opfibrations.

Every display map bicategory gives rise to a displayed bicategory as follows.

Definition 53 Let $\mathsf{B}$ be a bicategory and let $\mathsf{D}$ be a display map bicategory on $\mathsf{B}$ . We define a displayed bicategory $\overline{\mathsf{D}}$ over $\mathsf{B}$ as follows:

• The objects over $b : B$ are pairs $e : \mathsf{B}$ and $p : e \rightarrow b$ such that p is a display map;

• The 1-cells over $f : b_1 \rightarrow b_2$ from $p_1 : e_1 \rightarrow b_1$ to $p_2 : e_2 \rightarrow b_2$ are pairs of a 1-cell $g : e_1 \rightarrow e_2$ and an invertible 2-cell $g \cdot p_2 \Rightarrow p_1 \cdot f$ such that g preserves opcartesian 2-cells;

• The 2-cells are as in Example 10.

Similarly, every contravariant display map bicategory gives rise to a displayed bicategory. However, the 1-cells are required to preserve cartesian 2-cells. For isovariant display map bicategories, we do not make any restriction on the 1-cells. This way, we obtain displayed bicategories $\mathsf{SOpFib}(\mathsf{B})$ and $\mathsf{SFib}(\mathsf{B})$ over a bicategory $\mathsf{B}$ with pullbacks. In $\mathsf{SOpFib}(\mathsf{B})$ , 2-cells are the same as 2-cells in $\mathsf{B}^{\rightarrow}$ . However, 1-cells are a bit different: while 1-cells in $\mathsf{B}^{\rightarrow}$ are squares

that commute up to invertible 2-cell, 1-cells in $\mathsf{SOpFib}(\mathsf{B})$ have the additional requirement that whiskering with $f_e$ preserves opcartesian 2-cells. Similarly, we can define the bicategory $\mathsf{SFib}(\mathsf{B})$ where the objects are internal Street fibrations and where the 1-cells preserve cartesian 2-cells.

Now we can construct the desired cleavings.

Example 54 Let $\mathsf{B}$ be a bicategory and let $\mathsf{D}$ be a display map bicategory. As in Example 35, cartesian 1-cells are the same as pullback squares. Hence, we can construct a global cleaving for $\mathsf{D}$ using pullbacks and Proposition 47. To construct a local opcleaving for $\mathsf{D}$ , we use that it is contained in $\mathsf{SOpFib}(\mathsf{B})$ , and then we can use the same construction as for $\mathsf{SFib}(\mathsf{B})$ (Buckley 2014, Example 3.4.6).

Similarly, given a contravariant display map bicategory, one obtains both a global and a local cleaving. However, from an isovariant display map bicategory, one only gets a global cleaving and a local isocleaving. One can instantiate Example 54 to internal Street opfibrations to obtain a global cleaving and a local opcleaving for $\mathsf{SOpFib}(\mathsf{B})$ if $\mathsf{B}$ has pullbacks.

Using Example 54, we can generalize the example of (op)fibrations to arbitrary display map bicategories. We discuss the interest in this generalization in Remark 59.

Problem 55. Given a display map bicategory $\mathsf{D}$ on a bicategory $\mathsf{B}$ , to define a comprehension bicategory.

Construction 56 for Problem 55; From bicategory $\mathsf{B}$ and a display map bicategory $\mathsf{D}$ on $\mathsf{B}$ , we construct the comprehension bicategory

The (displayed) pseudofunctor $\chi$ is the inclusion of $\mathsf{D}$ into $\mathsf{B}^{\downarrow}$ .

Similarly, we get a contravariant comprehension bicategory from a contravariant display map bicategory, and an isovariant comprehension bicategory from an isovariant display map bicategory. We can instantiate Example 56 to internal Street opfibrations to get the following comprehension bicategory.

Example 57 For a bicategory $\mathsf{B}$ with pullbacks (see, e.g., Example 7), we construct the comprehension bicategory

The (displayed) pseudofunctor $\chi$ forgets that the morphisms in $\mathsf{SOpFib}(\mathsf{B})$ are internal Street opfibrations.

Example 58 By Example 57 any bicategory with pullbacks, thus in particular any bicategory of stacks (Street 1982), gives rise to a comprehension bicategory.

Remark 59. Recall from Section 2.3.1 that Coquand et al. (2017) constructed models of $\mathsf{MLTT}$ in stacks valued in groupoids. Using those models, they proved the independence of countable choice in univalent foundations.

With our comprehension bicategories of stacks (not just ones valued in groupoids), one could follow Coquand et al. (2017) and study the validity and independence of logical principles in directed type theory.

Note that we can specialize Example 57 to each of the examples given in Example 8. This is because we showed in Example 19 that those bicategories have pullbacks. In the case of $\mathsf{Cat}_{\mathsf{Terminal}}$ , we get a comprehension bicategory in which

• the “contexts” are categories with a terminal object; and

• the “types” are cloven opfibrations of categories which preserve terminal objects.

Similarly, we can instantiate this to the other categories mentioned in Example 8.

Remark 60. Note that, similarly, we can construct a contravariant comprehension bicategory from $\mathsf{SFib}(\mathsf{B})$ .

8. The Type Theory $\mathsf{BTT}$

In this section, we extract a core syntax for two-dimensional type theory from our semantic model. We call the resulting type theory Bicategorical Type Theory ( $\mathsf{BTT}$ ). In Section 9, we prove soundness of our syntax by giving an interpretation of the syntax in any weak comprehension bicategory.

The syntax extracted here is maximally general, in the sense that it reflects the structure of a general comprehension bicategory. In Section 10, we propose several orthogonal simplifications to the syntax, along with the corresponding semantic structure and properties. As such, our syntax and semantics are to be viewed as a framework to study different semantic structures and their corresponding internal languages, rather than as one particular pair of syntax and semantics.

In Section 8.1 we present the judgment forms of $\mathsf{BTT}$ , as well as the rules extracted from the bicategories of contexts and of types, respectively. In Sections 8.2 and 8.3 we present the comprehension and substitution rules, respectively.

For reasons of space we omit here several rules, namely the naturality rules in Figs. 8 and 9, and the coherencies of trifunctors. Such rules, written out in the “linear” syntax used here, would take up several lines and would be difficult to understand. Consequently, the syntax presented here is not complete. The presentation of the complete syntax and a suitable completeness theorem is left for future work.

8.1 Judgments and basic rules

$\mathsf{BTT}$ features contexts, substitutions, types, generalized terms, and reductions between terms. As befits the bicategorical semantics, judgmental equality is only postulated between parallel reductions.

There are eight kinds of judgments in $\mathsf{BTT}$ :

1. (1) $\Gamma \ \mathsf{ctx}$ , which is read as “ $\Gamma$ is a context”;

2. (2) $\Delta \vdash s : \Gamma$ (given $\Delta, \Gamma \ \mathsf{ctx}$ ), which is read as “s is a substitution from $\Delta$ to $\Gamma$ ”;

3. (3) $\Delta \vdash r : s \mathrel{\rightsquigarrow} t : \Gamma$ (where $\Delta \vdash s,t : \Gamma$ ), which is read as “r is a reduction from s to t”;

4. (4) $\Delta \vdash r \equiv r' : s \mathrel{\rightsquigarrow} t : \Gamma$ (where $\Delta \vdash r,r' : s \mathrel{\rightsquigarrow} t : \Gamma$ ), which is read as “r is equal to r”’;

5. (5) $\Gamma \vdash T \ \mathsf{type}$ (where $\Gamma \ \mathsf{ctx}$ ), which is read as “T is a type in context $\Gamma$ ”;

6. (6) $\Gamma \hspace{0.01em} \mid \hspace{0.01em} S \vdash t : T$ (where $\Gamma \vdash S, T \ \mathsf{type}$ ), which is read as “t is a term in T depending on S in context $\Gamma$ ”;

7. (7) $\Gamma \hspace{0.01em} \mid \hspace{0.01em} S \vdash \rho : t \mathrel{\rightsquigarrow} t' : T$ (where $\Gamma \hspace{0.01em} \mid \hspace{0.01em} S \vdash t,t' : T$ ), which is read as “ $\rho$ is a reduction from t to t”’;

8. (8) $\Gamma \hspace{0.01em} \mid \hspace{0.01em} S \vdash \rho \equiv \rho' : t \mathrel{\rightsquigarrow} t' : T$ (where $\Gamma \hspace{0.01em} \mid \hspace{0.01em} S \vdash \rho , \rho' : t \mathrel{\rightsquigarrow} t' : T$ ), which is read as “ $\rho$ is equal to $\rho'$ ”.

We often abbreviate the above judgments and write, e.g., just $\rho : t \mathrel{\rightsquigarrow} t'$ instead of $\Gamma \hspace{0.01em} \mid \hspace{0.01em} S \vdash \rho : t \mathrel{\rightsquigarrow} t' : T$ . For these judgments, we have rules that express the bicategorical structure of contexts and types. Rules are given in Fig. 1 for the bicategory of contexts, and in Fig. 2 for the bicategory of types.

Figure 1. Rules for the bicategory of contexts.

Figure 2. Rules for the the bicategory of types.

We also introduce symbols which read like judgments but stand for several judgments, using the composition and identities introduced in Figs. 1 and 2.

1. (1) $\Delta \vdash \rho : s \mathrel{\tilde{\mathrel{\rightsquigarrow}}} t : \Gamma$ stands for the following four judgments.

   • $\Delta \vdash \rho : s \mathrel{\rightsquigarrow} t : \Gamma$ $\Delta \vdash \rho^{-1} : t \mathrel{\rightsquigarrow} s : \Gamma$

   • $\rho \bullet \rho^{-1} \equiv 1_s$ $\rho^{-1} \bullet \rho \equiv 1_t$

2. (2) $\Gamma \hspace{0.01em} \mid \hspace{0.01em} S \vdash \rho : t \mathrel{\tilde{\mathrel{\rightsquigarrow}}} t' : T$ stands for the following four judgments.

   • $\Gamma \hspace{0.01em} \mid \hspace{0.01em} S \vdash \rho : t \mathrel{\rightsquigarrow} t' : T$ $\Gamma \hspace{0.01em} \mid \hspace{0.01em} S \vdash \rho ^{-1}: t' \mathrel{\rightsquigarrow} t : T$

   • $\rho \bullet \rho^{-1} \equiv 1_t$ $\rho^{-1} \bullet \rho \equiv 1_{t'}$

3. (3) $\Delta\ \tilde \vdash\ s : \Gamma$ stands for the following four judgments.

   • $\Delta \vdash s : \Gamma$ $\Gamma \vdash s^{-1} : \Delta$

   • $s^\ell: s s ^{-1} \mathrel{\tilde{\mathrel{\rightsquigarrow}}} 1_\Delta$ $s^\rho: s^{-1} s \mathrel{\tilde{\mathrel{\rightsquigarrow}}} 1_\Gamma$

We also require that $s^\ell$ and $s^\rho$ form an adjoint equivalence. This can be specified by formulating the usual triangle equalities as equality judgments.

• (4) $\Gamma \mid S \ \tilde \vdash\ t : T$ stands for the following four judgments.

  • $\Gamma \hspace{0.01em} \mid \hspace{0.01em} S \vdash t : T$ $\Gamma \hspace{0.01em} \mid \hspace{0.01em} T \vdash t^{-1} : S$

  • $t^\ell: t t ^{-1} \mathrel{\tilde{\mathrel{\rightsquigarrow}}} 1_S$ $t^\rho : t^{-1} t \mathrel{\tilde{\mathrel{\rightsquigarrow}}} 1_T$

Remark 61. By abuse of notation, we write several topically related rules that share all the same hypotheses as one rule with several conclusions. These rules then also share the same name, e.g., When referring to a rule by name, it will be clear from the context which of the possible rules we refer to. The names of inference rules in the text are hyperlinks to the corresponding rules (e.g., ). The equality $\equiv$ is assumed to be a congruence for every other constructor and judgment. For brevity, we have not recorded here the resulting rules. When parentheses are omitted, everything is associated to the left: that is, rst stands for ((rs)t). Note also that in several rules in which it is necessary to re-associate several four or more terms or substitutions, we have written $\alpha$ instead of a long composition of whiskered associators $\alpha_{\bullet, \bullet, \bullet}$ in the interest of readability.

8.2 Comprehension structure

Comprehension, that is, context extension, is extracted from the pseudofunctor $\chi$ . The rules for comprehension are given in Fig. 3. There are some notable differences to comprehension in $\mathsf{MLTT}$ . First, the rule which forms a substitution, comes together with a reduction that expresses the commutativity of a triangle. Second, we also have a rule that extends a substitution with a reduction. Since reductions are proof-relevant, this rule comes with a coherency on the commutativity.

Figure 3. Rules for comprehension.

8.3 Substitution structure

Substitution is given, in the semantics, by the global and local (op)cleaving structure. We reflect this into the syntax as explicit substitution, as was also used, e.g., by Fiore and Saville (2019), Licata and Harper (2012) in their respective settings.

The rules for substitution are given in Figs. 4, 5, 6, 7, 8, and 9. We distinguish them based on whether we need the global cleaving or the local opcleaving to interpret them. There are several important observations to be made about these rules. First, in line with our truly bicategorical approach, we do not assume the comprehension bicategory is split. In particular, no equality between $T[\!\operatorname{id}]$ and T is postulated. Instead, there is an equivalence between them (see sub-id and sub-comp), and terms of these types are transported along the equivalence.

Figure 4. Rules for global substitution.

Figure 5. Rules for global substitution (preservation of identity).

Figure 6. Rules for global substitution (preservation of composition).

Figure 7. Rules for local substitution.

Figure 8. Some rules for local substitution (preservation).

Figure 9. Some of the rules for coherence of substitution.

The rule expresses that each type T behaves “functorially”: for each $\Delta \vdash s : \Gamma$ (i.e., object in “ $\hom(\Delta,\Gamma)$ ”) we get a type T[s] (i.e., object in “the category of types in context $\Delta$ ”) by and for each $r: s \mathrel{\rightsquigarrow} s'$ (i.e., morphism in ‘ $\hom(\Delta,\Gamma)$ ’) we get a term $\Delta \hspace{0.01em} \mid \hspace{0.01em} T[s] \vdash \mathsf{map} \ T \ \theta : T[s']$ (i.e., morphism in “the category of types in context $\Delta$ ”) by . The rules and ensure that $T[-]$ preserves identity and composition. With we can then understand terms to be “natural transformations.”

Remark 62. For contravariant comprehension bicategories (Remark 41), the rule would be in the opposite direction, while for isovariant comprehension bicategories, this rule would be restricted to isomorphisms in the base.

Remark 63. Using the Grothendieck construction, we can view the rules from the perspective of fiber bicategories. If $P : \mathsf{E} \rightarrow \mathsf{B}$ has a global cleaving and a local opcleaving, and furthermore opcartesian 2-cells are preserved under whiskering, then we obtain a trifunctor $\mathsf{B}^{\mathsf{op}} \rightarrow \mathsf{Bicat}$ , which sends every $x : \mathsf{B}$ to the fiber of x along P. The rules given in Fig. 4 say that any 1-cell in the base gives rise to a pseudofunctor. For example, the rules represent the actions on objects, 1-cells, and 2-cells, respectively, while represent the invertible 2-cells that witness the preservation of the identity and composition of 1-cells. The other rules in that table are the coherence laws of pseudofunctors: for example, is the preservation of identity 2-cells.

Figs. 5 and 6 give pseudonatural equivalences expressing that the assignment of the previously mentioned pseudofunctor is actually pseudofunctorial: the identity and composition are preserved up to pseudonatural equivalence. For example, the rules in Fig. 5 represent the action on objects and the naturality squares. On the other hand, are the usual coherencies of pseudonatural transformations.

The rules of Fig. 7 state that we obtain a pseudonatural transformation from a 2-cell in the base. The action on objects and 1-cells is given by respectively, while describe the usual coherencies of pseudonatural transformations. The remaining rules can be found in Fig. 8. In this figure, four invertible modifications are described: describe the preservation of identity and composition, respectively, while describe the preservation of both left and right whiskering. Note that we left out the naturality conditions of these modifications. In addition, two additional coherencies are required which express that all this data together forms a trifunctor. We do not write them down, but instead, we refer the reader to Definition 3.3.1 of Gurski (2006).

Remark 64. A similar rule to of Fig. 7 appears in work of

Johnstone (1993). There, it is shown that a 1-cell p in a 2-category is an internal fibration in a sense similar to our Definition 46 if and only if a specific functor given by precomposition with p has a semi-oplax right adjoint satisfying some properties, assuming that pullbacks along p exist. In Lemma 2.5 of Johnstone (1993), another equivalent characterization of p being a fibration is given assuming that pullbacks of p exist. This characterization uses several operations and compatibility requirements. One of the operations is described by the following diagram:

We assume that pullbacks along p are given; in particular, we have $f^* e$ and $g^* e$ . The characterization of p being a fibration entails, in particular, that for every 2-cell $\alpha :\, f \Rightarrow g$ there is a 1-cell $\hat{p}(\alpha) :\, f^*e \rightarrow g^*e$ . This takes place in a 2-category, though Johnstone claims that such a characterization would also hold in a bicategory. Modulo this difference, this operation is expressed by rule of Fig.7.

9. Soundness: Interpretation in Comprehension Bicategories

In this section, we give an interpretation of $\mathsf{BTT}$ in any weak comprehension bicategory. To this end, we fix a comprehension bicategory ${\mathsf{D}} \mathop{\longrightarrow}\limits^{\chi}\mathsf{B}^{\downarrow}$ over ${\mathsf{B}}$ . We interpret the judgments as follows.

• $\Gamma \ \mathsf{ctx}$ is interpreted as an object ${[\![} \Gamma {]\!]}$ of $\mathsf{B}$ .

• $\Delta \vdash s : \Gamma$ is interpreted as a 1-cell ${[\![} s {]\!]} : {[\![} \Delta {]\!]} \rightarrow {[\![} \Gamma {]\!]}$ in $\mathsf{B}$ .

• $\Delta \vdash r : s \mathrel{\rightsquigarrow} t : \Gamma$ is interpreted as a 2-cell ${[\![} r {]\!]} : {[\![} s {]\!]} \Rightarrow {[\![} t {]\!]}$ in $\mathsf{B}$ .

• $\Delta \vdash r \equiv r' : s \mathrel{\rightsquigarrow} t : \Gamma$ is interpreted as an equality ${[\![} r {]\!]} = {[\![} r' {]\!]}$ .

• $\Gamma \vdash T \ \mathsf{type}$ is interpreted as an object ${[\![} T {]\!]}$ in $\mathsf{D}$ over ${[\![} \Gamma {]\!]}$ .

• $\Gamma \hspace{0.01em} \mid \hspace{0.01em} S \vdash t : T$ is interpreted as a 1-cell ${[\![} t {]\!]} : {[\![} S {]\!]} \rightarrow {[\![} T {]\!]}$ over the identity on ${[\![} \Gamma {]\!]}$ .

• $\Gamma \hspace{0.01em} \mid \hspace{0.01em} S \vdash r: t \mathrel{\rightsquigarrow} t' : T$ is interpreted as a 2-cell ${[\![} r {]\!]} : {[\![} t {]\!]} \Rightarrow {[\![} t' {]\!]}$ over the identity 2-cell.

• $\Gamma \hspace{0.01em} \mid \hspace{0.01em} S \vdash r \equiv r' : t \mathrel{\rightsquigarrow} t' : T$ is interpreted as an equality ${[\![} r {]\!]} = {[\![} r' {]\!]}$ .

Regarding the “bicategorical” rules of Figs. 1 and 2, each rule is analogous to one of the operations or laws of a bicategory – see, for instance, Definition 3.1 of Ahrens et al. (2021). This also indicates how it is interpreted.

9.1 Comprehension

In this section, we interpret the rules related to comprehension of Fig. 3. Suppose that we have a context $\Gamma : \mathsf{B}$ and a type T over $\Gamma$ . Its image $\chi(T)$ in $\mathsf{B}^{\downarrow}$ gives rise to an object $\Gamma . T : \mathsf{B}$ and a 1-cell $\pi_{\Gamma.T} : \Gamma . T \rightarrow \Gamma$ which interprets For a 1-cell t from S to T over the identity, the resulting 1-cell $\chi(t)$ is part of a triangle

which commutes up to invertible 2-cell. This yields the interpretation of the rules in Furthermore, a reduction $r : t \mathrel{\rightsquigarrow} t'$ is mapped by $\chi$ to a 2-cell from $\chi(t)$ to $\chi(t')$ in $\mathsf{B}^{\downarrow}$ , and this is how we interpret are interpreted by the identitor and compositor of $\chi$ , respectively, while the remaining rules in Fig. 3 are satisfied because they translate to the laws that express that this data forms a pseudofunctor.

9.2 Global substitution

Next, we interpret the rules for global substitution of Fig. 4 (in Sections 9.2.1, 9.2.2, 9.2.3, and 9.2.4) and the rules regarding preservation of identity under global substitution of Fig. 5 (in Sections 9.2.6, 9.2.5, and 9.2.7). The interpretation of the rules regarding preservation of composition of Fig. 6 is analogous to that of Fig. 5 and is not spelled out.

The interpretation of the rule is given directly by the global cleaving. The interpretation of the other rules require more explanation.

9.2.1 Interpretation of sub-tm

To interpret , we assume that we have a substitution $s : \Delta \rightarrow \Gamma$ between contexts $\Delta$ and $\Gamma$ . We also assume that we have types S, T over $\Gamma$ and a morphism $t : S \to T$ over $1_\Gamma$ . This situation is encapsulated in the following diagram, using the notation introduced in Definition 27.

Our goal is to construct a 1-cell $t[s] : S[s] \rightarrow T[s]$ that lies over the identity on $\Delta$ . Since the morphism $L_{s}(T) : T[s] \rightarrow T$ is cartesian, it suffices to construct a 1-cell, say, $\beta : S[s] \rightarrow T$ that lies over $1_\Delta \cdot s$ . We then obtain the desired 1-cell as the factorization ${{{\mathsf{F_1}(L_{s}(T),\beta)}}}$ of that 1-cell via $L_{s}(T)$ . (Recall that ${{{\mathsf{F_1}(\_,\_)}}}$ was defined in Definition 21.) We have an invertible 2-cell $r_{s} \bullet {\ell_{s}}^{-1} : s \cdot 1_\Gamma \Rightarrow 1_\Delta \cdot s$ , and we set $\beta := {{{{(r_{s} \bullet {\ell_{s}}^{-1})}_!{(L_{s}(S) \cdot t)}}}}$ . Define

\[t[s] := {{{\mathsf{F_1}(L_{s}(T),\beta)}}}.\]

Overall, we can summarize the construction with the following diagram.

9.2.2 Interpretation of sub-red

To interpret , we assume that we have a substitution $s : \Delta \rightarrow \Gamma$ and types S and T in context $\Gamma$ . We also assume that we have 1-cells $t, t' : S \to T$ over $1_\Gamma$ and a 2-cell $\rho : t \Rightarrow t'$ . Consider the following diagram.

Our goal is to construct a 2-cell from t[s] to t[s’] over the identity on $\Delta$ . The source and target, respectively, were constructed by factoring a 1-cell via a cartesian 1-cell, as follows.

To construct the desired 2-cell $\rho[s] : t[s] \Rightarrow t[s']$ , we use Item 2 of Definition 21. More specifically, it suffices to construct

• a 2-cell $\delta$ from $1_\Delta$ to $1_\Delta$ , and

• a 2-cell $\overline{\sigma}$ from $\beta$ to $\beta'$ .

Once we have defined those, we define $\rho[s] := {{{\mathsf{E}(\delta,\overline{\sigma})}}}$ .

For the first of the two, we take the identity 2-cell $1_{1_{\Delta}}$ . For the second, we take the composition of 2-cells shown in the following diagram.

The interpretation of the rules follows from the uniqueness of factorization 2-cells.

9.2.3 Interpretation of sub-pres-id

The rules are interpreted similarly, and we show the interpretation of . Suppose that we have a substitution $s : \Delta \rightarrow \Gamma$ and a type T in context $\Gamma$ . We consider two morphisms: the identity on T[s] and $1_T[s]$ . These are illustrated in the following diagram.

Our goal is to construct an invertible 2-cell from $1_{T[s]}$ to $1_T[s]$ . To do so, we first recall the construction of $1_T[s]$ .

To construct the desired invertible 2-cell, we again use Item 2 of Definition 21. As such, we need to construct the following:

• An invertible 2-cell $\delta$ from $1_\Delta$ to $1_\Delta$ ; and

• An invertible 2-cell $\overline{\sigma}$ from $1_T[s] \cdot L_{s}(T)$ to $1_{T[s]} \cdot L_{s}(T)$ .

With those in place, we define $\mathsf{Sub_I}(s)^{-1} := {{{\mathsf{E}(\delta,\overline{\sigma})}}}$ . For $\delta$ , we take the identity, while for $\overline{\sigma}$ , we take the following composition.

$1_{T[s]} \cdot L_{s}(T) \cong L_{s}(T) \cdot 1_T \cong \beta \cong 1_T[s] \cdot L_{s}(T)$

9.2.4 Interpretation of sub-pres-lunitor

The remaining laws stating equalities of 2-cells, such as , are all proven in a similar way. Our goal is to prove an equality $\overline{\alpha} = \overline{\beta}$ with 1-cells and 2-cells as in the diagram below:

Here t and t’ live over s and s’, respectively, while $\overline{\alpha}$ and $\overline{\beta}$ live over $\alpha$ and $\beta$ , respectively. To prove the equality, we take the following steps.

• (1) We construct an invertible 2-cell $\theta$ from $t \cdot L_{s''}(T)$ to $t' \cdot L_{s''}(T)$ .

• (2) We prove that $\alpha = \beta$ .

• (3) We prove that $\overline{\alpha} \vartriangleright L_{s''}(T) = \theta = \overline{\beta} \vartriangleright L_{s''}(T)$ .

From the first item, we get that both t and t’ are cartesian factorizations of the same $S \rightarrow T$ . From the second and third item, we get that both $\overline{\alpha}$ and $\overline{\beta}$ are factorization 2-cells from t to t’, and since such 2-cells are unique, we get $\overline{\alpha} = \overline{\beta}$ .

We demonstrate this for . Suppose we have a substitution $s : \Delta \rightarrow \Gamma$ , types S and T in context $\Gamma$ , and a morphism $t : S \to T$ over $1_\Gamma$ . We are in the following situation.

Here, we define $\alpha := (1_{1_\Delta} \vartriangleright 1_\Delta) \bullet \ell_{1_\Delta}$ and $\beta := 1_{1_\Delta \cdot 1_\Delta} \bullet \ell_{1_\Delta}$ . We also define $\overline{\alpha}$ and $\overline{\beta}$ as follows.

$\overline{\alpha} := (\mathsf{Sub_I}(s)^{-1} \vartriangleright t[s]) \bullet \ell_{t[s]}\quad \quad\overline{\beta} := \mathsf{Sub_C}(1_S, t, s) \bullet \ell_t[s]$

Then by construction, both $\alpha$ and $\beta$ are equal to $\ell_{1_\Delta}$ , and hence, $\alpha = \beta$ .

Next we construct an invertible 2-cell from $1_S[s] \cdot t[s] \cdot L_{s}(T)$ to $t[s] \cdot L_{s}(T)$ . By construction of t[s], we have an invertible 2-cell $\theta_1 : t[s] \cdot L_{s}(T) \cong \cdot L_{s}(S) \cdot t$ . In addition, we have an invertible 2-cell $\theta_2 : 1_S[s] \cdot L_{s}(S) \cong L_{s}(S) \cdot 1_S$ . This is illustrated in the following diagram.

Now we define an invertible 2-cell $\theta_3 : 1_S[s] \cdot t[s] \cdot L_{s}(T) \cong L_{s}(S) \cdot t$ as follows.

$\theta_3 := \alpha^{-1} \bullet (1_S[s] \vartriangleleft \theta_2) \bullet \alpha \bullet (\theta_1 \vartriangleright t) \bullet (r_\sigma \vartriangleright t)$

The desired invertible 2-cell $\theta : 1_S[s] \cdot t[s] \cdot L_{s}(T) \cong t[s] \cdot L_{s}(T)$ is $\theta_3 \bullet \theta_2^{-1}$ .

For the last step, we only prove that $\overline{\alpha} \vartriangleright L_{s}(T) = \theta$ . We first recall how we constructed $\mathsf{Sub_I}(s)$ . For brevity, we write $\sigma := L_{s}(S)$ and $\tau := L_{s}(T)$ .

By construction, we have that $(\mathsf{Sub_I}(s)^{-1} \vartriangleright \sigma) \bullet \ell_\sigma \bullet r_\sigma^{-1} = \theta_1$ . In particular, we have $\mathsf{Sub_I}(s)^{-1} \vartriangleright \sigma = \theta_1 \bullet r_\sigma \bullet \ell_{\sigma}^{-1}$ .

To show that $((\mathsf{Sub_I}(s)^{-1} \vartriangleright t[s]) \bullet \ell_{t[s]}) \vartriangleright \tau = \theta_3 \bullet \theta_2^{-1}$ , it suffices to show that $((\mathsf{Sub_I}(s)^{-1} \vartriangleright t[s]) \bullet \ell_{t[s]}) \vartriangleright \tau \bullet \theta_2 = \theta_3$ . This follows from the following chain of equalities.

$ \begin{align*} & \quad \alpha^{-1} \bullet (1_S[s] \vartriangleleft \theta_2^{-1}) \bullet \alpha \bullet ((\mathsf{Sub_I}(s)^{-1} \vartriangleright t[s]) \bullet \ell_{t[s]}) \vartriangleright \tau \bullet \theta_2 \bullet (r_\sigma \vartriangleright t)^{-1} \\ &= \alpha^{-1} \bullet (1_S[s] \vartriangleleft \theta_2^{-1}) \bullet \alpha \bullet (\mathsf{Sub_I}(s)^{-1} \vartriangleright t[s]) \vartriangleright \tau \bullet (\ell_{t[s]} \vartriangleright \tau) \bullet \theta_2 \bullet (r_\sigma \vartriangleright t)^{-1} \\ &= \alpha^{-1} \bullet (1_S[s] \vartriangleleft \theta_2^{-1}) \bullet \mathsf{Sub_I}(s)^{-1} \vartriangleright (t[s] \cdot \tau) \bullet \alpha \bullet (\ell_{t[s]} \vartriangleright \tau) \bullet \theta_2 \bullet (r_\sigma \vartriangleright t)^{-1} \\ &= \alpha^{-1} \bullet \mathsf{Sub_I}(s)^{-1} \vartriangleright (\sigma \cdot t) \bullet (1_{S[s]} \vartriangleleft \theta_2^{-1}) \bullet \alpha \bullet (\ell_{t[s]} \vartriangleright \tau) \bullet \theta_2 \bullet (r_\sigma \vartriangleright t)^{-1} \\ &= \mathsf{Sub_I}(s)^{-1} \vartriangleright \sigma \vartriangleright t \bullet \alpha^{-1} \bullet (1_{S[s]} \vartriangleleft \theta_2^{-1}) \bullet \alpha \bullet (\ell_{t[s]} \vartriangleright \tau) \bullet \theta_2 \bullet (r_\sigma \vartriangleright t)^{-1} \\ &= (\theta_1 \bullet r_\sigma \bullet \ell_{\sigma}^{-1}) \vartriangleright t \bullet \alpha^{-1} \bullet (1_{S[s]} \vartriangleleft \theta_2^{-1}) \bullet \alpha \bullet (\ell_{t[s]} \vartriangleright \tau) \bullet \theta_2 \bullet (r_\sigma \vartriangleright t)^{-1} \\ &= \theta_1 \vartriangleright t \bullet ({r_\sigma \bullet \ell_{\sigma}^{-1}}) \vartriangleright t \bullet \alpha^{-1} \bullet (1_{S[s]} \vartriangleleft \theta_2^{-1}) \bullet \alpha \bullet (\ell_{t[s]} \vartriangleright \tau) \bullet \theta_2 \bullet (r_\sigma \vartriangleright t)^{-1} \\ &= \theta_1 \vartriangleright t \bullet ({r_\sigma \bullet \ell_{\sigma}^{-1}}) \vartriangleright t \bullet \alpha^{-1} \bullet (1_{S[s]} \vartriangleleft \theta_2^{-1}) \bullet \ell_{t[s] \tau} \bullet \theta_2 \bullet (r_\sigma \vartriangleright t)^{-1} \\ &= \theta_1 \vartriangleright t \bullet ({r_\sigma \bullet \ell_{\sigma}^{-1}}) \vartriangleright t \bullet \alpha^{-1} \bullet \ell_{\sigma \cdot t} \bullet \theta_2^{-1} \bullet \theta_2 \bullet (r_\sigma \vartriangleright t)^{-1} \\ &= \theta_1 \vartriangleright t \bullet ({r_\sigma \bullet \ell_{\sigma}^{-1}}) \vartriangleright t \bullet \alpha^{-1} \bullet \ell_{\sigma \cdot t} \bullet (r_\sigma \vartriangleright t)^{-1} \\ &= \theta_1 \vartriangleright t \bullet ({r_\sigma \bullet \ell_{\sigma}^{-1}}) \vartriangleright t \bullet \ell_{\sigma} \vartriangleright t \bullet (r_\sigma \vartriangleright t)^{-1} \\ &= \theta_1 \vartriangleright t\end{align*}$

9.2.5 Interpretation of sub-id

Next we interpret Suppose we have a context $\Gamma$ and a type T in $\Gamma$ . Note that we have a diagram as follows.

We interpret $\mathsf{sub}_{\mathsf{id}}(T)$ ⁵ by $L_{1_\Gamma}(T)$ , so it suffices to show that $L_{1_\Gamma}(T)$ is an equivalence. To construct the inverse, we use the following diagram.

We set $\iota := {{{\mathsf{F_1}(L_{1_\Gamma}(T),1_T \cdot 1_T)}}}$ , and it remains to show that we have an invertible 2-cell from $L_{1_\Gamma}(T) \cdot \iota$ to $1_T$ . To do so, we use Item 2 of Definition 21, and we consider the following diagram.

We need to construct an invertible 2-cell $\delta$ from $1_\Gamma \cdot 1_\Gamma$ to $1_\Gamma$ and an invertible 2-cell $\overline{\sigma}$ from $L_{1_\Gamma}(T) \cdot \iota \cdot L_{1_\Gamma}(T)$ to $1_{T[s]} \cdot L_{1_\Gamma}(T)$ . For $\delta$ , we take $\lambda$ . For $\overline{\sigma}$ , we use that $\iota \cdot L_{1_\Gamma}(T) \cong 1_T \cdot 1_T$ , and thus we have the following composition of invertible 2-cells.

$ \begin{equation*}\begin{split}L_{1_\Gamma}(T) \cdot \iota \cdot L_{1_\Gamma}(T)&\cong L_{1_\Gamma}(T) \cdot 1_T \cdot 1_T\\&\cong L_{1_\Gamma}(T)\\&\cong 1_{T[s]} \cdot L_{1_\Gamma}(T)\end{split}\end{equation*}$

The desired invertible 2-cell is thus defined by ${{{\mathsf{E}(\delta,\overline{\sigma})}}}$ .

9.2.6 Interpretation of sub-comp

To interpret we suppose that we have substitutions $s' : \Theta \rightarrow \Delta$ and $s : \Delta \rightarrow \Gamma$ , and a type T in $\Gamma$ . Hence, we have the following diagram.

Note that both $L_{s \cdot s'}(T)$ and $L_{s}(T[s']) \cdot L_{s'}(T)$ are cartesian 1-cells over $s \cdot s'$ , since cartesian 1-cells are closed under composition by Proposition 22. For that reason, we get an adjoint equivalence $\mathsf{sub}_{\mathsf{comp}}(s, s') : T[s'][s] \rightarrow T[s \cdot s']$ making the diagram below commute up to invertible 2-cell by Construction 24.

9.2.7 Interpretation of tm-sub-id

Next we interpret and for that, we suppose that we have a context $\Gamma$ , types S and T over $\Gamma$ , and a 1-cell $t : S \to T$ over $1_\Gamma$ . We need to construct an invertible 2-cell from $\mathsf{sub}_{\mathsf{id}}^{-1} \ \cdot t[1_{\Gamma}] \cdot \mathsf{sub}_{\mathsf{id}}$ to t, and for that, it suffices to construct an invertible 2-cell from $t[1_{\Gamma}] \cdot \mathsf{sub}_{\mathsf{id}}$ to $\mathsf{sub}_{\mathsf{id}} \cdot t$ . Recall that we defined $\mathsf{sub}_{\mathsf{id}}$ to be $L_{1_\Gamma}(T)$ and recall that we defined $t[1_\Gamma]$ as follows.

By composing the two invertible 2-cells depicted in this diagram, we get the desired invertible 2-cell. The rule is interpreted analogously.

9.3 Local substitution

Next we interpret the rules in Fig. 7 (in Sections 9.3.1 and 9.3.2), Fig. 8 (in Sections 9.3.3 and 9.3.4), and Fig. 9 (in Section 9.3.5). For the interpretation, we use the local opcleaving.

9.3.1 Interpretation of map

We start with Suppose we have two substitutions $s, s' : \Delta \rightarrow \Gamma$ and a 2-cell $\rho : s \Rightarrow s'$ . In addition, we assume that we have a type T in context $\Gamma$ . Our goal is to construct a 1-cell $\mathsf{map} \ T \ \rho : T[s] \rightarrow T[s']$ . From the local opcleaving, we obtain $\mu_{\rho}(L_{s}(T))$ over $1_\Delta \cdot s'$ as the pushforward of $L_{s}(T)$ along $\rho \bullet \ell_{s'}^{-1}$ .

Since $L_{s'}(T)$ is cartesian, we can factor $\mu_{\rho}(L_{s}(T))$ through it. From that, we obtain $\mathsf{map} \ T \ \rho$ .

9.3.2 Interpretation of rew-tm

Next, we give the interpretation for the rule Suppose we have two 1-cells $s, s' : \Delta \rightarrow \Gamma$ and a 2-cell $\rho : s \rightarrow s'$ . In addition, we assume that we have types S, T in context $\Gamma$ and a 1-cell $\Gamma \hspace{0.01em} \mid \hspace{0.01em} S \vdash t : T$ . Our goal is to construct an invertible 2-cell between $t[s] \bullet (\mathsf{map} \ T \ \rho)$ and $(\mathsf{map} \ S \ \rho) \bullet t[s']$ . For that it suffices to construct:

1. (1) An invertible 2-cell $\delta$ from $1_\Delta \cdot 1_\Delta$ to $1_\Delta \cdot 1_\Delta$ ; and

2. (2) An invertible 2-cell $\overline{\sigma}$ from $t[s] \bullet (\mathsf{map} \ T \ \rho) \bullet L_{s'}(T)$ to $(\mathsf{map} \ S \ \rho) \bullet t[s'] \bullet L_{s'}(T)$ .

Then we define $t[\rho]$ to be ${{{\mathsf{E}(\delta,\overline{\sigma})}}}$ . For $\delta$ we take $1_{1_\Delta \cdot 1_\Delta}$ .

To construct $\overline{\sigma}$ , we first note that by construction of t[s’], we have the following invertible 2-cell.

$(\mathsf{map} \ S \ \rho) \bullet t[s'] \bullet L_{s'}(T)\cong(\mathsf{map} \ S \ \rho) \bullet L_{s'}(S) \bullet t$

Note that by construction of $\mathsf{map} \ S \ \rho$ , the following triangle commutes up to invertible 2-cell.

Hence, we get

$\gamma_1 : (\mathsf{map} \ S \ \rho) \bullet L_{s'}(S) \bullet t\cong\mu_{\rho}(L_{s}(S)) \bullet t.$

Similarly, we have an invertible 2-cell $\mathsf{map} \ T \ \rho \cdot L_{s'}(S) \cong \mu_{\rho}(L_{s}(T))$ , and thus we obtain

$\gamma_2 : t[s] \bullet (\mathsf{map} \ T \ \rho) \bullet L_{s'}(T)\cong t[s] \bullet \mu_{\rho}(L_{s}(T)).$

It thus suffices to construct an invertible 2-cell from $t[s] \bullet \mu_{\rho}(L_{s}(T))$ to $\mu_{\rho}(L_{s}(S)) \bullet t$ . We can depict the situation with the following square.

In this diagram, $\tau$ and $\tau'$ are the opcartesian 2-cells coming from the opcartesian lift. Note that by construction of t[s], the outer square of this diagram commutes. More precisely, we have an invertible 2-cell $\theta : t[s] \cdot L_{s}(T) \cong L_{s}(S) \cdot t$ .

To construct an invertible 2-cell from $\mu_{\rho}(L_{s}(S)) \cdot t$ to $t[s] \cdot \mu_{\rho}(L_{s}(T))$ , we are going to construct two opcartesian 2-cells. First, note that we have a 2-cell

$\tau \vartriangleright t : L_{s}(S) \cdot t \Rightarrow \mu_{\rho}(L_{s}(S)) \cdot t'$

that lies over $\beta_1 := (\rho \bullet l^{-1}) \vartriangleright 1_\Gamma : s \cdot 1_\Gamma \Rightarrow (1_\Delta \cdot s') \cdot 1_\Gamma$ . This 2-cell is opcartesian, because opcartesian 2-cells are closed under right whiskering.

Note that we also have the 2-cell

$\theta^{-1} \bullet t[s] \vartriangleleft \tau : L_{s}(S) \cdot t \Rightarrow t[s] \cdot \mu_{\rho}(L_{s}(T))$

which lies over $\beta_2 := r \bullet \ell^{-1} \bullet 1_{\Gamma} \vartriangleleft (\rho \bullet \ell^{-1}) : s \cdot 1_{\Gamma} \Rightarrow 1_{\Delta} \cdot (1_{\Delta} \cdot s')$ . It is opcartesian, because left whiskering also preserves opcartesian 2-cells.

We also have the following invertible 2-cell

$\beta_3 := r \bullet \ell^{-1}:(1_\Delta \cdot s') \cdot 1_\Gamma\cong1_{\Delta} \cdot (1_{\Delta} \cdot s'),$

and note that $\beta_1 \bullet \beta_3 = \beta_2$ by naturality of the unitors. From all of this we get the desired invertible 2-cell $\mu_{\rho}(L_{s}(S)) \cdot t \cong t[s] \cdot \mu_{\rho}(L_{s}(T))$ .

9.3.3 Interpretation of map-id

To interpret we assume that we have a 1-cell $s : \Delta \rightarrow \Gamma$ and a type T in context $\Gamma$ . Our goal is to construct an invertible 2-cell between the following compositions.

To do so, we need to construct:

1. (1) An invertible 2-cell $\delta$ from $1_\Delta$ to $1_\Delta$ ; and

2. (2) An invertible 2-cell $\overline{\sigma}$ from $\mathsf{map} \ T \ 1_s \cdot L_{s}(T)$ to $L_{s}(T)$ .

The desired 2-cell is then defined to be ${{{\mathsf{E}(\delta,\overline{\sigma})}}}$ . For $\delta$ we take $1_{1_\Delta}$ .

To construct $\overline{\sigma}$ , we first note that by construction of $\mathsf{map} \ T \ \rho$ , the following triangle commutes up to an invertible 2-cell $\tau : \mathsf{map} \ T \ \rho \cdot L_{s'}(T) \cong \mu_{\rho}(L_{s}(T))$ .

Next we recall that $\mu_{\rho}(L_{s}(T))$ was constructed as the following pushforward.

Since $\ell_{s}^{-1}$ is invertible, the opcartesian lift $\theta$ is invertible as well. Hence, we define $\overline{\sigma} := \tau \bullet \theta^{-1}$ . We interpret similarly.

9.3.4 Interpretation of map-lwhisker

To interpret we use the same idea, and we need to use that we assumed that opcartesian 2-cells are closed under whiskering. We give the precise details for Suppose we have a 1-cell $s : \Theta \rightarrow \Delta$ , a 2-cell $\rho : s' \Rightarrow s''$ where $s', s'' : \Delta \rightarrow \Gamma$ , and a type T in context $\Gamma$ . Our goal is to construct an invertible 2-cell from $\mathsf{map} \ T \ (s \vartriangleleft \rho)$ to $\mathsf{sub}_{\mathsf{comp}}^{-1}(s, s') \cdot (\mathsf{map} \ T \ \rho)[s] \cdot \mathsf{sub}_{\mathsf{comp}}(s, s'')$ . Since $\mathsf{map} \ T \ \rho$ was constructed as a cartesian factorization, it suffices to construct:

1. (1) An invertible 2-cell $\delta$ from $1_\Delta$ to $1_\Delta \cdot 1_\Delta \cdot 1_\Delta$ ; and

2. (2) An invertible 2-cell $\overline{\sigma}$ from $\mathsf{map} \ T \ (s \vartriangleleft \rho) \cdot L_{s \cdot s''}(T)$ to $\mathsf{sub}_{\mathsf{comp}}^{-1}(s, s') \cdot (\mathsf{map} \ T \ \rho)[s] \cdot \mathsf{sub}_{\mathsf{comp}}(s, s'') \cdot L_{s \cdot s''}(T)$ .

With those in place, the desired invertible 2-cell is defined to be ${{{\mathsf{E}(\delta,\overline{\sigma})}}}$ . We define $\delta$ to be $\ell_{1_\Delta}^{-1} \cdot \ell_{1_\Delta \cdot 1_\Delta}^{-1}$ .

For the construction of $\overline{\sigma}$ , let us start by recalling the construction of $\mathsf{map} \ T \ (s \vartriangleleft \rho)$ .

Next we inspect the definition of $\mathsf{sub}_{\mathsf{comp}}(s, s'')$ .

From this, we already get the following invertible 2-cell.

$\begin{align*}\gamma_1 : & \mathsf{sub}_{\mathsf{comp}}^{-1}(s, s') \cdot (\mathsf{map} \ T \ \rho)[s] \cdot \mathsf{sub}_{\mathsf{comp}}(s, s'') \cdot L_{s \cdot s''}(T) \\ & \cong \\ & \mathsf{sub}_{\mathsf{comp}}^{-1}(s, s') \cdot (\mathsf{map} \ T \ \rho)[s] \cdot L_{s}(T[s'']) \cdot L_{s''}(T)\end{align*}$

We also inspect the construction of $(\mathsf{map} \ T \ \rho)[s]$ , from which we get the following invertible 2-cell.

As such, we get another invertible 2-cell as follows.

$ \begin{align*}\gamma_2 : & \mathsf{sub}_{\mathsf{comp}}^{-1}(s, s') \cdot (\mathsf{map} \ T \ \rho)[s] \cdot L_{s}(T[s'']) \cdot L_{s''}(T) \\ & \cong \\ & \mathsf{sub}_{\mathsf{comp}}^{-1}(s, s') \cdot L_{s}(T[s']) \cdot \mathsf{map} \ T \ \rho \cdot L_{s''}(T).\end{align*}$

Let us recall the construction of $\mathsf{map} \ T \ \rho$ as well.

From this, we obtain yet another invertible 2-cell.

$ \begin{align*} \gamma_3 : & \mathsf{sub}_{\mathsf{comp}}^{-1}(s, s') \cdot (\mathsf{map} \ T \ \rho)[s] \cdot L_{s}(T[s'']) \cdot L_{s''}(T) \\ & \cong \\ & \mathsf{sub}_{\mathsf{comp}}^{-1}(s, s') \cdot L_{s}(T[s']) \cdot \mu_{\rho}(L_{s''}(T))\end{align*}$

Hence, we achieve our goal if we construct an invertible 2-cell of the following form.

$\gamma_4 :\mathsf{sub}_{\mathsf{comp}}^{-1}(s, s') \cdot L_{s}(T[s']) \cdot \mu_{\rho}(L_{s'}(T))\cong\mu_{s \vartriangleleft \rho}(L_{s \cdot s'}(T))$

We can depict this situation as follows.

Here $\tau$ and $\tau'$ are the 2-cells coming from the opcartesian lifts.

Since whiskering preserves opcartesian 2-cells, the following 2-cell is opcartesian.

$\begin{align*}(\mathsf{sub}_{\mathsf{comp}}^{-1}(s, s') \cdot L_{s}(T[s'])) \vartriangleleft \tau\enspace : \enspace & \mathsf{sub}_{\mathsf{comp}}^{-1}(s, s') \cdot L_{s}(T[s']) \cdot L_{s'}(T) \\ & \Rightarrow \\ & \mathsf{sub}_{\mathsf{comp}}^{-1}(s, s') \cdot L_{s}(T[s']) \cdot \mu_{\rho}(L_{s'}(T))\end{align*}$

Now we unfold the definition of $\mathsf{sub}_{\mathsf{comp}}(s, s')$ , and from that we get the following invertible 2-cell.

Since invertible 2-cells are opcartesian and opcartesian 2-cells are closed under composition, we get an opcartesian 2-cell

$\theta : L_{s \cdot s'}(T)\Rightarrow\mathsf{sub}_{\mathsf{comp}}^{-1}(s, s') \cdot L_{s}(T[s']) \cdot \mu_{\rho}(L_{s'}(T)).$

Since we already had an opcartesian 2-cell $\tau' : L_{s \cdot s'}(T) \Rightarrow \mu_{s \vartriangleleft \rho}(L_{s \cdot s'}(T))$ , we get an invertible 2-cell between the codomains of $\theta$ and $\tau'$ . Hence, we obtain an invertible 2-cell

$\gamma_5 : \mathsf{sub}_{\mathsf{comp}}^{-1}(s, s') \cdot L_{s}(T[s']) \cdot \mu_{\rho}(L_{s'}(T))\cong\mu_{s \vartriangleleft \rho}(L_{s \cdot s'}(T)).$

By chaining all the invertible 2-cells, we get the desired 2-cell $\overline{\sigma}$ .

9.3.5 Interpretation of sub-comp-map-id-r

Finally, we show how to interpret Suppose that we have objects $\Gamma$ and $\Delta$ , an object T over $\Gamma$ , and a 1-cell $s : \Delta \rightarrow \Gamma$ . Our goal is to construct an invertible 2-cell from $\mathsf{sub}_{\mathsf{comp}}(s, 1_\Delta) {(\mathsf{map} \ T \ r_{s})}$ to $\mathsf{sub}_{\mathsf{id}}$ . To do so, it suffices to construct an invertible 2-cell from $\mathsf{sub}_{\mathsf{comp}}(s, 1_\Delta) \cdot (\mathsf{map} \ T \ r_{s}) \cdot L_{s}(T)$ to $\mathsf{sub}_{\mathsf{id}} \cdot L_{s}(T)$ . Our situation is depicted in the following diagram.

Recall that $\mathsf{sub}_{\mathsf{id}} : T[s][1_\Delta] \rightarrow T[s]$ is defined to be $L_{1_\Delta}(T[s])$ . By construction, we have an invertible 2-cell

$\varphi_1 :\mathsf{map} \ T \ r_{s} \cdot L_{s}(T)\Rightarrow\mu_{r_{s}}(L_{s \cdot 1_{\Delta}}(T)) .$

In addition, since $\mathsf{map} \ T \ r_{s}$ was constructed as an opcartesian lift, we have the following invertible 2-cell.

$\varphi_2 :L_{s \cdot 1_{\Delta}}(T)\Rightarrow\mu_{r_{s}}(L_{s \cdot 1_{\Delta}}(T))$

Note that $\varphi_2$ is invertible: this is because it is the opcartesian lift of an invertible 2-cell. By construction of $\mathsf{sub}_{\mathsf{comp}}(s, 1_\Delta)$ , we have the following invertible 2-cell.

$\varphi_3 :\mathsf{sub}_{\mathsf{comp}}(s, 1_\Delta) \cdot L_{s \cdot 1_{\Delta}}(T)\Rightarrow L_{1_{\Delta}}(T[1_\Delta]) \cdot L_{s}(T) .$

The composition $\varphi_3 \bullet \varphi_2 \bullet \varphi_1^{-1}$ yields the desired 2-cell.

We omit the description of the verification of several equalities. All in all, we can state the following theorem.

Theorem (Soundness). We can interpret $\mathsf{BTT}$ in any weak comprehension bicategory.

10. Variations on Syntax

$\mathsf{BTT}$ is a very complicated type theory and might not be feasible to implement or use in practice. Its main purpose is to serve as a framework for studying specialized syntax and the corresponding semantics. Based on a user’s goal, they might adopt some of the following simplifications.

V1: Strictness. The rules in Figs. 1 and 2 are aimed at bicategories. When working with strict 2-categories instead, the unitors and associators would become equalities, and as a result, rules for inverse laws, naturality, and the pentagon and triangle equations are not needed. For this variant, an equality judgment on contexts, types, substitutions, and terms would be added to $\mathsf{BTT}$ .

V2: Splitness. We could assume the comprehension bicategory to be split in addition to being strict; thus, in particular, the rules would collapse into ordinary equalities.

V3: Undirected TT. We could add a rule postulating inverses of reductions. Semantically, this would amount to working in groupoid-enriched categories.

V4: Proof-irrelevant reductions. Our syntax and the semantics allow us to distinguish parallel reductions (2-cells). We could instead “truncate” them, by moving to proof-irrelevant reductions, making the judgmental equality on them superfluous. This would yield a directed analog to the judgments of $\mathsf{MLTT}$ ; semantically, it corresponds to working in poset-enriched categories instead of general bicategories.

We have developed comprehension bicategories with the explicit goal of encompassing previously defined interpretations of higher-dimensional and directed type theory. In the following remarks, we summarize the relationship with two previous works.

Remark 65. (Comparison to

Garner 2009). To summarize the differences between Garner’s comprehension 2-categories (Garner 2009) and our comprehension bicategories: the former are full, strict, split, undirected (i.e., locally groupoidal), and incorporate type constructors.

Remark 66. (Licata and Harper’s work).

Licata and Harper (2011) interpret a type in context $\Gamma$ as a strict 1-functor from the category interpreting $\Gamma$ into a 1-category $\mathsf{CAT}$ of categories. Formally, they thus consider the slice bicategory $\mathsf{Cat}/\mathsf{CAT}$ , where $\mathsf{Cat}$ is the bicategory of categories, in which $\mathsf{CAT}$ is assumed to be a 0-cell. The “domain” pseudofunctor ${{{\mathsf{dom}}}} : \mathsf{Cat}/\mathsf{CAT} \to \mathsf{Cat}$ carries the structure of a global cleaving and local opcleaving; this is more generally the case for any “domain” pseudofunctor ${{{\mathsf{dom}}}} : \mathsf{B}/a \to \mathsf{B}$ (). To construct the comprehension pseudofunctor, one needs to use specifics of the category of strict categories, namely the Grothendieck construction of functors into $\mathsf{CAT}$ .

11. Terms in Directed Type Theory

The notion of term in $\mathsf{BTT}$ , and the interpretation of these terms, is different from the notion of term studied in the syntax and semantics by Licata and Harper (2011) or North (2019). Specifically, our terms correspond to 1-cells in the (total) category of types and are interpreted as such. Terms in the sense of Licata and Harper, and North, instead correspond to particular 1-cells in the category of contexts, specifically, to sections of the canonical projections $\pi_{\Gamma,A} : \Gamma.A \to \Gamma$ .

One might attempt to reconcile these two, on the syntactic side, by

• (1) adding a unit type to $\mathsf{BTT}$ ; and

• (2) asking for context morphisms to be built from terms, that is, from type morphisms. (Semantically, this corresponds to asking for $\chi$ to be full.)

However, note that most of our comprehension bicategories are not full. Furthermore, this syntactic modification would still leave a difference between the interpretations of terms given by Licata and Harper, and North, on the one hand, and our interpretation on the other hand. Specifically, in Example 45, terms are interpreted as functors that preserve opcartesian cells; by the Grothendieck construction, terms can equivalently be interpreted as pseudonatural transformations. In contrast, terms are interpreted as lax natural transformations by others (Licata and Harper 2011; North 2019). Hence, there is a mismatch between how terms are interpreted in comprehension bicategories compared to other interpretations.

We can analyze this mismatch more closely and suggest a potential way of reconciling it, by looking again at the intended interpretation of two-dimensional and directed type theory in categories via the opcleaving model. Taking this mismatch seriously leads us in the direction of directed type theory, where there can be different flavors of terms. For example, in work by Nuyts (2015) terms can be used isovariantly, covariantly, and contravariantly. In the opcleaving model (Example 45), these different notions of terms would correspond to different kinds of natural transformations: pseudonatural transformations, lax natural transformations, and oplax natural transformations.

To reconcile this difference, one would need to modify the syntax and the definition of comprehension bicategory. In the syntax, one would need to add a term judgment for every kind of term present in directed type theory. Accordingly, one would also add the corresponding operations like substitution. The notion of comprehension bicategory would also require slight modifications for this purpose; one necessary requirement would be that $\chi$ preserves both cartesian 1-cells and opcartesian 2-cells. The reason for this change is that this would be necessary to interpret substitution of a certain class of terms. More precisely, in the opfibration model, lax transformations can be identified with sections of the projections $\int \mathsf{D} \rightarrow \mathsf{C}$ . To interpret substitution for these, we need that certain squares in the arrow bicategory are pullbacks; to guarantee that, one requires that $\chi$ preserves cartesian 1-cells.

It is an open problem to develop categorical semantics for type theories that feature terms with different variances.

12. Conclusion

We have introduced the notion of comprehension bicategory, inspired by the notion of comprehension category. From this semantic notion, we have extracted a two-dimensional core syntax for dependent types, terms, and reductions and an interpretation of that syntax in comprehension bicategories. In future work, we hope to accompany this soundness result with a completeness result.

Our work is very general. We hope that it gives future investigations into two-dimensional and directed type theories a firm foundation. For instance, as outlined in Section 1.1, in future work, we will extend our structural rules with variances and a suitable hom-type former à la North (2019).