The n-Category Café

Fibres: from functions to functors

By way of motivating example, we begin with a comparison of notions of fibre for functions between sets and functors between categories, respectively. Recall that, for any function $f : X \to Y$ and $y \in Y$, the fibre of $y$ is the subset $f^{-1}\{y\} = \{ x \in X \mid f(x) = y\}$, as in the following picture:

It follows straightforwardly that $X = \bigsqcup_{y \in Y} f^{-1}\{y\}$, i.e. $X$ is equal to the disjoint union of the fibres of $f$. Hence we can always recover the domain of a function from its fibres.

There is an analogous notion of fibre for functors. Let $p : \mathcal{E} \to \mathcal{B}$ be a functor, and consider an object $b \in \mathcal{B}$. The fibre $\mathcal{E}_b$ of $p$ over $b$ is defined to be the subcategory of $\mathcal{E}$ consisting of all objects $e \in \mathcal{E}$ such that $p(e) = b$, and all morphisms $f : e \to e' \in \mathcal{E}$ such that $p(f) = id_b$.

Can we similarly recover the domain of a functor from its fibres, just as we could for functions? As it turns out, we can in general recover the objects of $\mathcal{E}$ from the fibres of $p$, but not necessarily the morphisms of $\mathcal{E}$, since some morphisms may not belong to any fibre.

This naturally prompts the question: what additional structure is needed on $p$ in order to be able to recover $\mathcal{E}$ from its fibres? The answer to this question lies in the notion of a Grothendieck fibration.

Fibrations, Graphically

From Functors to Prisms

We begin by developing a graphical framework for representing the structure of a functor $p : \mathcal{E} \to \mathcal{B}$, based upon that of Sterling and Angiuli. Given objects $a \in \mathcal{E}$ and $b \in \mathcal{B}$ such that $p(a) = b$, we may think of $a$ as an object living in the fibre of $p$ over $b$

and we depict this arrangement as a dashed vertical arrow from $a$ to $b$:

Similarly, given morphisms $f : c \to a \in \mathcal{E}$ and $g : d \to b \in \mathcal{B}$ such that $p(a) = b$, $p(c) = d$, and $p(f) = g$, we think of $f$ as lying over $g$

and depict this as a square between the two dashed arrows corresponding to $a$ and $c$, respectively:

Squares of this form can be composed horizontally:

In fact, this is just another way of saying that $p$ preserves composition of morphisms, as in the following picture:

Given two such squares that horizontally compose to a third, these naturally arrange themselves into a triangular prism:

More generally, since $p$ must preserve all commuting diagrams in $\mathcal{E}$, for any diagram in $\mathcal{E}$ living over one in $\mathcal{B}$, there is a corresponding depiction of this as a prism – e.g. a commuting square in $\mathcal{E}$ over one in $\mathcal{B}$ gives a cube:

Cartesian Arrows

Definition. A morphism $f : c \to a \in \mathcal{E}$ lying over $g : d \to b \in \mathcal{B}$

is called Cartesian if any partial prism as below can be uniquely completed to a prism:

In this case, we suggestively write

to indicate that the arrow $f$ is Cartesian.

More generally, for a Cartesian arrow $f$ as above, any partial prism missing an incoming morphism to $c$ may be uniquely completed to a corresponding prism, since every commuting diagram may be decomposed into commuting triangles. E.g. any partial cube as below may be uniquely completed to a cube as follows:

The analogy of Cartesian squares to pullbacks is no accident – a Cartesian arrow as above may be informally viewed as a “limit” of the following diagram:

Following Johnson and Yau, we refer to a diagram of the former shape as a pre-lift, and to a Cartesian arrow completing the square as above as a Cartesian lift.

Like ordinary limits, Cartesian lifts are unique up to isomorphism, as shown in the following diagram:

Similarly, the composition of two Cartesian lifts is again Cartesian, since we have

Example. For any functor $p : \mathcal{E} \to \mathcal{B}$, every identity in $\mathcal{E}$ is Cartesian:

Example. For any category $\mathcal{C}$, let $\mathcal{C}^\to$ be the arrow category of $\mathcal{C}$, i.e. the category whose objects are arrows in $\mathcal{C}$ and whose morphisms are commuting squares. Let $\mathsf{cod} : \mathcal{C}^\to \to \mathcal{C}$ be the functor that sends an arrow to its codomain. Then a Cartesian arrow for $\mathsf{cod}$ is a pullback in $\mathcal{C}$.

To see as much, note that in the graphical representation of $\mathsf{cod}$ the dashed arrows correspond to actual arrows, so e.g.~a square over $g : d \to b$ is a commuting square

Such a square is Cartesian if any diagram as below can be uniquely completed to a prism:

which is equivalent to the universal property of a pullback.

Definition. A functor $p : \mathcal{E} \to \mathcal{B}$ is a Grothendieck fibration (or fibration for short) if every pre-lift has a Cartesian lift. Much like ordinary limits, although Cartesian lifts are unique up to isomorphism, there may in fact be many possible choices of such lifts. A cloven fibration is a fibration equipped with a specific choice, for each pre-lift, of a corresponding Cartesian lift. A cloven fibration is called split if:

• for every object $b \in \mathcal{B}$, the chosen lift of $id_b$ and $a \in \mathcal{E}_b$ is $id_a$

• for every pair $k : s \to d, ~ g : d \to b \in \mathcal{B}$ of composable morphisms, the chosen lift of $g \circ k$ and $a \in \mathcal{E}_b$ is equal to the composite of the chosen lift of $g$ and the chosen lift of $k$.

Example. If $\mathcal{B}$ is a discrete category (i.e. every morphism is an identity) then any functor $p : \mathcal{E} \to \mathcal{B}$ is a fibration, since, as we have already seen, the Cartesian lift of any identity in $\mathcal{B}$ is an identity in $\mathcal{E}$.

In particular, since sets are equivalently discrete categories, and functions between sets are equivalently functors between discrete categories, it follows that every function between sets (viewed as discrete categories) is a fibration. So in our initial motivating example concerning fibres of functions, we were in fact already implicitly working with fibrations.

Example. A category $\mathcal{C}$ for which $\mathsf{cod} : \mathcal{C}^\to \to \mathcal{C}$ is a fibration is equivalently a category with all pullbacks. $\mathsf{cod}$ is moreover a split fibration if and only if the operation of taking successive pullbacks is strictly (unital and) associative, i.e.

This is particularly relevant when interpreting pullbacks as a kind of substitution, as in e.g. the categorical semantics of dependent type theory.

Lemma. Let $p : \mathcal{E} \to \mathcal{B}$ be a fibration and let $f':c'\to c$ be any morphism in $\mathcal{E}$. It follows that $f'$ factors as $f'=f \circ \gamma$ where $f:a\to c$ is the Cartesian lift of $p(f')$ and $\gamma:c'\to a$ is in the fibre of $d$.

Hence every morphism in $\mathcal{E}$ factors as a composite of a Cartesian arrow, and an arrow in the fibre of an object in $\mathcal{B}$. Intuitively, Cartesian lifts “connect” the fibres of $p$ to one another. In fact, we can make this idea precise, by the following observation:

Observation. In a Grothendieck fibration, every morphism $g : d \to b \in \mathcal{B}$ determines a functor $g^* : \mathcal{E}_b \to \mathcal{E}_d$, defined on objects as follows:

and on morphisms as follows:

Hence in a fibration $p : \mathcal{E} \to \mathcal{B}$, the morphisms in $\mathcal{B}$ provide a way to “travel” from one fibre to another, as in the following picture:

This structure of functors between fibres determines a pseudofunctor $\mathcal{B}^{op} \to \mathbf{Cat}$ that maps an object $b\in \mathcal{B}$ to $\mathcal{E}_b$; and maps a morphism $g$ in $\mathcal{B}$ to $g*$.

The above answers our original motivating question of how to recover the morphisms of $\mathcal{E}$ from the structure of the fibres of $p$. In fact, we can go even further and construct (a category isomorphic to) $\mathcal{E}$ out of the fibres of $p$ by “gluing” them together along the functors induced by morphisms in $\mathcal{B}$. This is precisely what the Grothendieck construction accomplishes.

The Grothendieck Construction

A principal raison d’être behind fibrations is to simplify the process of working with indexed categories. Given a base category $\mathcal{B}$, a $\mathcal{B}$-indexed category is a family of categories $F(x)$ indexed by objects $x \in \mathcal{B}$, such that morphisms $x \to y \in \mathcal{B}$ contravariantly induce a functors $F(y) \to F(x)$, in a manner which preserves identities and composition of morphisms in $\mathcal{B}$ up to coherent isomorphism. Equivalently, a $\mathcal{B}$-indexed category is a pseudofunctor $\mathcal{B}^{op} \to \mathbf{Cat}$.

We have just seen how every fibration $p : \mathcal{E} \to \mathcal{B}$ gives rise to a $\mathcal{B}$-indexed category structure on its fibres. In fact, as we shall see, indexed categories are equivalent to fibrations. The key construct behind this equivalence is the Grothendieck construction, which can be viewed more generally as a way of reconstructing a functor from its graphical representation as described above. To make this idea precise, we make use of the notion of displayed categories – introduced by Ahrens and Lumsdaine – as a common generalization of indexed categories and the graphical representation of functors given above.

Definition. Given a base category $\mathcal{B}$, a displayed category over $\mathcal{B}$ is a formal description of the graphical structure of a functor with codomain $\mathcal{B}$, consisting of:

• For each object $b \in \mathcal{B}$, a set of vertical arrows

  

• for each morphism $g : d \to b \in \mathcal{B}$ with vertical arrows $a$ into $b$ and $c$ into $d$, a set of squares

  

  together with identity squares and an operation of horizontal composition of squares that is unital and associative.

By definition, for any $\mathcal{B}$-displayed category $\mathcal{D}$, taking vertical arrows of $\mathcal{D}$ as objects, and squares between these as morphisms, defines a category $\int^{b \in \mathcal{B}} \mathcal{D}(b)$ – the Grothendieck Construction of $\mathcal{D}$

Straightforwardly, there is a functor $\pi : \left( \int^{b \in \mathcal{B}}\mathcal{D}(b) \right) \to \mathcal{B}$, which sends each vertical arrow/square in $\mathcal{D}$ to the object/morphism in $\mathcal{B}$ over which it lies. This construction of $\pi$ realizes $\mathcal{D}$ as a functor into $\mathcal{B}$, such that the graphical representation of $\pi$ is precisely $\mathcal{D}$.

Conversely, given a functor $p : \mathcal{E} \to \mathcal{B}$, the Grothendieck construction of its corresponding displayed category yields a functor $p' : \mathcal{E}' \to \mathcal{B}$ such that there is an isomorphism of categories $e : \mathcal{E} \cong \mathcal{E}'$ that commutes with $p$ and $p'$.

Hence functors are equivalent to displayed categories, via the Grothendieck construction, and we have already seen how every fibration gives rise to an indexed category. To show that the Grothendieck construction descends to an equivalence between fibrations and indexed categories, it thus suffices to show that every indexed category corresponds to a displayed category with the universal property of a fibration.

From pseudofunctors to fibrations: Let $F : \mathcal{B}^{op} \to \mathbf{Cat}$ be a pseudofunctor. We define a displayed category $\int F$ over $\mathcal{B}$ as follows:

• For each object $b \in \mathcal{B}$, an object lying over $b$ is an object of $F(b)$.

• For each morphism $g : d \to b \in \mathcal{B}$, for objects $c \in F(d)$ and $a \in F(b)$, a morphism $f$ from $c$ to $a$ over $g$ is a morphism $$f : c \to F(g)(a) \in F(d)$$ where $F(g) : F(b) \to F(d)$ is the functorial action of $F$ on $g$.

• For each object $b \in \mathcal{B}$ with $a \in F(b)$, the identity square is given by $id_a : a \to F(id_b)(a)$, and the composition of $f : a \to F(g)(c)$ and $h : c \to F(k)(e)$ is given by $$a \xrightarrow{f} F(g)(c) \xrightarrow{F(g)(h)} F(g)(F(k)(e)) \simeq F(k \circ g)(e)$$

Moreover, $\int F$ has the universal property of a fibration, since for any pre-lift consisting of $g : d \to b \in \mathcal{B}$ and $a \in F(b)$ as below, we may take the Cartesian lift to be the object $F(g)(a) \in F(d)$, along with the identity $id_{F(g)(a)} : F(g)(a) \to F(g)(a)$:

which is indeed Cartesian, since any diagram as below can be uniquely completed to a triangular prism, by pseudofunctoriality:

This correspondence between indexed categories and fibrations can be extended to a 2-equivalence between the 2-category of $\mathcal{B}$-indexed categories and the 2-category $\mathbf{Fib}\mathcal{B}$ of fibrations over $\mathcal{B}$:

Theorem. There is a 2-equivalence $\int : [\mathcal{B}^{op},\mathbf{Cat}]^{ps} \to \mathbf{Fib}\mathcal{B}$.

We provide a brief description of these 2-categories and how $\int$ acts on cells in the following subsections.

The 2-category of $B$-indexed categories

In this subsection, we introduce the 2-category $[\mathcal{B}^{op},\mathbf{Cat}]^{ps}$.

Definition. For any category $\mathcal{B}$, the 2-category denoted as $[\mathcal{B}^{op},\mathbf{Cat}]^{ps}$ consist of the following:

Objects. Pseudounctors $F:\mathcal{B}^{op}\to \mathbf{Cat}$.

1-cells. Strong natural transformations. A strong natural transformation $\sigma: F \to G$ consists of a collection of functors $\sigma_b: F(b)\to G(b)$ indexed by object $b\in \mathcal{B}$. For every morphism $g:d\to b$ in $\mathcal{B}$, the following diagram must commute up to coherent isomorphism:

2-cells. Modifications. A modification $\Gamma:\sigma\to \sigma'$ between two strong natural transformations $\sigma', \sigma: F\to G$ is a collection of natural transformations $\Gamma_b: \sigma_b\to \sigma'_b$ for every $b\in \mathcal{B}$, such that for any $g:d\to b$ in $\mathcal{B}$, the following whiskering diagram commutes:

The 2-category of fibrations

Definition. For any category $\mathcal{B}$, the 2-category denoted as $\mathbf{Fib}\mathcal{B}$ consists of the following:

Objects. Fibrations $p:\mathcal{E}\to \mathcal{B}$.

1-cells. The 1-cells between two fibrations $p:\mathcal{E}\to \mathcal{B}$ and $q:\mathcal{E}'\to \mathcal{B}$ are cartesian functors. Those are functors $\Lambda: \mathcal{E}\to \mathcal{E}'$ that make the diagram commute

and send cartesian arrows to cartesian arrows.

2-cells. The 2-cells are vertical natural transformations, which is to say: natural transformations $\eta:\Lambda \to \Lambda'$ between cartesian functors $\Lambda: p \to q$ and $\Lambda':p\to q$ that make the following whiskering diagram commute:

In the first part of this section, we described how to construct a fibration $p:\int F \to \mathcal{B}$ from a pseudofunctor $\mathcal{B}^{op} \to \mathbf{Cat}$. Finally, in order to better understand the 2-equivalence $\int$, we define its action on 1-cells and 2-cells:

Definition. Let $F:\mathcal{B}^{op}\to\mathbf{Cat}$ and $G:\mathcal{B}^{op}\to\mathbf{Cat}$ be objects in $[\mathcal{B}^{op},\mathbf{Cat}]^{ps}$, and let $\sigma:F\to G$ be a natural transformation. The cartesian functor $\int\sigma: \int F \to \int G$:

• maps objects according to $\sigma$

  

• similarly, it maps morphisms according to $\sigma$

  

Definition. Let $\Gamma: \sigma\to \sigma'$ be a modification. The vertical natural transformation $\int\Gamma: \int\sigma \to \int\sigma'$ is defined for every pair $(b,a)$ in $\int F$ as the morphism

Example. Given an indexed category $F : \mathcal{B}^{op} \to \mathbf{Cat}$, its fibrewise opposite is the pseudofunctor $F(-)^{op} : \mathcal{B}^{op} \to \mathbf{Cat}$ that maps $b \in \mathcal{B}$ to $F(b)^{op}$.

Passing from this to the functor $\pi : \left( \int^{b \in \mathcal{B}} F(b)^{op} \right) \to \mathcal{B}$ via the Grothendieck construction, the objects of each fibre of $\pi$ are the same as those of $F$, but now for any morphism $g : d \to b \in \mathcal{B}$, a morphism $f$ lying over this in $\int^{b \in \mathcal{B}} F(b)^{op}$ goes in the opposite direction as $g$. We may depict this graphically as a “twisted” square:

and we refer to squares of this form as “lenses”. Lenses compose horizontally, but note now how composition upstairs goes in the opposite direction as downstairs:

The category $\int^{b \in \mathcal{B}}F(b)^{op}$ obtained from this construction is called the category of lenses of $F$, and is of central importance in the emerging field of categorical systems theory. The essential idea behind the use of lenses in categorical systems theory is that lenses provide a good model of bidirectional processes – i.e. processes that interact with one another by both sending information (along the lower – “forward” – map) and receiving information (along the upper – “backward” – map).

Myers has shown how this definition of lenses gives rise to a certain kind of doubly-indexed category, whose structure allows one to study the compositional properties of behaviors of dynamical systems. Such a doubly-indexed category should correspond, via a double-categorical analogue of the Grothendieck construction, to a particular double fibration.

To better understand constructions of this sort, and their applications in categorical systems theory and beyond, we are interested in developing methods of working with such higher-categorical structures that allow us to manage the oft-complicated coherence conditions that arise thereabouts. For this purpose, it is useful to work synthetically with such structures – i.e. by working in the internal language of some well-structured category in which these structures naturally reside. As it happens, we have already been implicitly using such a synthetic approach in our discussion of fibrations up to this point, which we now specify more precisely.

Fibrations, Synthetically

In our previous – prismatic – study of fibrations, we saw how the property of being a Cartesian arrow for a functor/displayed category could be reduced to that of every commuting triangle in the base category with a specified boundary lifting uniquely to a filling for the corresponding triangular prism. This suggests that a synthetic framework for reasoning about shapes such as triangles, prisms, etc., ought to be a good setting in which to study the sorts of constructions we have encountered in previous sections.

A suitable category whose internal language allows us to represent and reason about such shapes is the category of simplicial sets $\widehat{\Delta}$. There are several properties of $\widehat{\Delta}$ that make it a good setting for the synthetic study of (higher) categories, fibrations, etc. In particular, it is a (presheaf) topos, which for our purposes means that its internal language supports all the usual constructs of dependent type theory, specifically:

• Types $A$, containing elements $x : A$.

• Subtypes, where $\{x\mid \phi(x)\} \subseteq A$ is the type containing all elements $x : A$ that satisfy $\phi(x)$.

• Dependent types, where a family $B(x)$ of types dependent upon $x : A$ is such that $B(a)$ is a type for each $a : A$.

• Dependent function types, where $\Pi_{x : A} B(x)$ is the type of functions $f$ such that $f(a) : B(a)$ for all $a : A$. In the case where $B$ does not depend upon $A$, this reduces to the usual function type $A \to B$.

• Dependent pair types, where $\Sigma_{x : A} B(x)$ is the type of pairs $(a,b)$ such that $a : A$ and $b : B(a)$. In the case where $B$ does not depend upon $A$, this reduces to the usual product type $A \times B$.

A key property of the internal type-theoretic language of $\widehat{\Delta}$ (as developed in the more general setting of simplicial spaces by Riehl and Shulman) is that it includes a special type $\Delta^1$, corresponding to the standard 1-simplex, equipped with the following additional structure:

• There are two distinguished elements $0,1 : \Delta^1$

• $\Delta^1$ is totally ordered by a binary relation $\leq$ for which $0$ is the least element and $1$ is the greatest element.

(For those who know a bit of topos theory, this is due to the fact that $\widehat{\Delta}$ is the classifying topos of bounded total orders). We think of $\Delta^1$ as representing an abstract line segment or path with $0$ and $1$ as designated endpoints, as follows:

Using the language of dependent type theory, we can then build more complex shapes out of such paths. In particular, the Cartesian product of two line segments – i.e. $\Delta^1 \times \Delta^1$ – is a square, i.e.

while a triangle may be represented as the portion of such a square lying above the diagonal:

corresponding to the following subtype of the square $\Delta^1 \times \Delta^1$: $$\Delta^2 := \{(x,y) \mid x \leq y\} \subseteq \Delta^1 \times \Delta^1$$ More generally, the standard $n$-simplex may be defined as the type $$\Delta^n := \{(x_1, \dots, x_n) \mid x_1 \leq \dots \leq x_n \} \subseteq \Delta^1 \times \dots \times \Delta^1$$ as these are in fact equivalent to the Yoneda embeddings in $\widehat{\Delta}$ of the standard simplices in the simplex category $\Delta$.

We may then use these abstract shapes to detect corresponding structure in other types by mapping into them. E.g. a path from $a$ to $b$ in a type $A$ is a function $f : \Delta^1 \to A$ such that $f(0) = a$ and $f(1) = b$, and we write $\mathsf{Path}_A(a,b)$ for the type of such paths, and depict them the same as morphisms in categories, using directed arrows, i.e.

In particular, there are three non-trivial (i.e. non-constant) functions $\Delta^1 \to \Delta^2$, namely the functions that map $i : I$ to $(0,i), ~ (i,1)$, and $(i,i)$, respectively, which together pick out the three paths on the boundary of $\Delta^2$ as follows:

Hence given a type $A$ with $a,b,c : A$ and $f : \mathsf{Path}_A(a,b)$ and $g : \mathsf{Path}_A(b,c)$ and $h : \mathsf{Path}_A(a,c)$, a triangle in $A$ with boundary given by $f,g,h$ as depicted below

is a function $k : \Delta^2 \to A$ such that $k(0,i) = f(i)$, $k(i,1) = g(i)$, and $k(i,i) = h(i)$ for all $i : \Delta^1$.

In order to recover ordinary category theory in this setting, we should have some way of viewing the language of categories as somehow embedded in that of simplicial sets. For a given type $A$ in the language of simplicial sets, a triangle

in $A$ may be thought of as a witness to the fact that $h$ is a valid solution to the problem of composing $f$ and $g$. A category is then just a type where – in the internal language of $\widehat{\Delta}$ – every such “composition problem” has a unique solution, i.e. for any $a,b,c : A$ with $f : \mathsf{Path}_A(a,b)$ and $g : \mathsf{Path}_A(b,c)$, there is a unique completion of this to a triangle as follows:

One straightforwardly verifies that the uniqueness of such solutions implies the associativity of composition, since for any composable sequence of paths $a \xrightarrow{f} b \xrightarrow{g} c \xrightarrow{h} d \in A$, a solution to the composition problem for the triangle formed by $g \circ f$ and $h$ is also a solution to the composition problem for $f$ and $h \circ g$, and vice versa, so these two solutions must be identical. Unitality of composition follows by similar reasoning.

Hence, in the language of simplicial sets, being a category is only a property of a type. In fact, this definition of categories is equivalent to the embedding $\mathbf{Cat} \hookrightarrow \widehat{\Delta}$ given by the nerve functor. In particular, any function $f : A \to B$, where $A,B$ are both categories in the above sense, is automatically a functor in the usual sense, since any path $g : \mathsf{Path}_A(a,b)$ in $A$ is taken to a path $f \circ g : \mathsf{Path}_B(f(a),f(b))$ in $B$, and similarly for triangles, hence $f$ preserves composition, etc. We can thus suppress much of the bookkeeping to do with checking functoriality conditions, etc., by treating categories as a special kind of simplicial sets, and working in the internal language of the latter.

This simplification is especially apparent when we consider the interpretation of our prior treatment of displayed categories and the Grothendieck construction in this framework. Given a family of types $E(x)$ dependent upon $x : B$, we may think of an element $a : E(b)$ for $b : B$ as living over $a$ in the structure of $E$, and represent this using our dashed vertical arrow notation from before:

Then for $b,d : A$ with $a : E(b)$ and $c : E(d)$ and a path $g : \mathsf{Path}_B(d,b)$, we may define a path from $c$ to $a$ lying over $g$ as a dependent function $f : \Pi_{i : \Delta^1}. C(f(i))$ such that $f(0) = c$ and $f(1) = a$. We may depict this just as we did in the case of functors/displayed categories as a square, i.e.:

And similarly, for such a family of types $E(x)$ dependent upon $x : B$, given a triangle $k : \Delta^2 \to B$ with boundary $f,g,h$ in $B$, and paths $f',g',h'$ lying over these, respectively, a prism as depicted in the following diagram

corresponds to a dependent function $k' : \Pi_{(i,j) : \Delta^2} . C(k(i,j))$ such that $k'(0,i) = f'(i)$, $k'(i,1) = g'(i)$ and $k'(i,i) = h'(i)$ for all $i : I$.

Given such a type family $E(x)$ dependent upon $x : B$, the Grothendieck construction of $E$ may be interpreted in $\widehat{\Delta}$ as the dependent pair type $\Sigma_{x : B} . E(x)$ whose elements are pairs $(b,a)$ with $b : B$ and $a : E(b)$.

That a path $(d,c) \to (b,a)$ in $\Sigma_{x : B} . E(x)$ is equivalently a square consisting of $g : d \to b$ and $f : c \to a$ follows from the distributivity of function types over pair types, i.e. $$\Delta^1 \to \Sigma_{x : B} . E(x) \cong \Sigma_{f : \Delta^1 \to B} . \Pi_{i : \Delta^1} . E(f(i))$$

If $B$ is a category in $\widehat{\Delta}$, then a type family $E(x)$ dependent upon $x : B$ is a displayed category if every partial prism has a unique completion as follows:

And just as before, a dependent path $f$ lying over $g$ is Cartesian iff every partial prism has a unique completion as follows:

Hence we can interpret all of our previous definitions and constructions regarding fibrations, the Grothendieck construction, etc., into this simplicial framework, by simply translating the shapes occurring in these constructions into corresponding types and functions in the internal language of simplicial sets.

As a final illustration of this, we now sketch how this technique may be used to give economical definitions of both double categories and double fibrations.

A Recipe for Double-Categorical Structure

In the above, we have defined categories in one way as certain types in the internal language of $\widehat{\Delta}$. But since this internal language supports all the usual constructs of dependent type theory, we can just as well define category objects internally in simplicial set in the usual way, i.e. as a type of objects $\text{Ob}$ and a type family $\text{Hom}(x,y)$ dependent upon $x,y : \text{Ob}$ together with an associative and unital composition operation and identities.

Recall that a (strict) double category is equivalently a category object internal to $\mathbf{Cat}$. Since the definition of an internal category object makes use only of (finite) limits, which are preserved by the nerve functor $\mathbf{Cat} \to \widehat{\Delta}$ (since it is a right adjoint), it follows that an internal category object in $\widehat{\Delta}$ whose component types are all nerves of categories is equivalently a strict double category.

Hence again in the language of simplicial sets, we can reduce being a double category to a mere property of an internal category object (namely the property that its types of objects and morphisms are themselves nerves of categories). Moreover, an (internal) functor between such categories is then automatically a double functor.

Finally, we note that such a double functor, viewed as an ordinary functor in the language of simplicial sets, may be considered a fibration in two distinct ways: either by requiring that it satisfy the ordinary property of a Grothendieck fibration – as a functor between internal categories – or that each of its component functions (i.e. those mapping objects/morphisms of the domain to those of the codomain) themselves be fibrations in the simplicial sense defined above. We conjecture that requiring both of these properties to hold is equivalent (in the strict case) to the definition of double fibrations given by Cruttwell, Lambert, Pronk and Szyld, wherein they define a double fibration as an internal category in the 2-category of fibrations over arbitrary bases. We hope to further explore this connection and perhaps prove this conjecture during the upcoming research week for the Adjoint School!

Much remains to be done in fleshing out the theory of double fibrations. We hope that the above-described framework may be a valuable tool for this direction of study. In particular, we are interested to know how much of the ordinary theory of fibrations translates to double fibrations, and we hope that this framework can unify and simplify the task of answering these questions, by translating ordinary categorical definitions into the internal language of simplicial sets, and seeing how these interact with properties arising from nerves of categories. Because of its type-theoretic flavor, it should moreover be possible to formalize this treatment of (double) fibrations in a proof assistant such as Agda or Lean. All these and other applications we hope to explore further during the Adjoint School research week. For now, we hope to have sufficiently demonstrated the utility and simplifying power of the simplicial approach to fibrations in both pure and applied category theory.