Foundations of Relative Category Theory
by ,
The current version of these notes is now located on my Forest. Permalinks from the existing website are redirected to the corresponding nodes in the Forest.
We assume knowledge of basic categorical concepts such as categories, functors, and natural transformations. The purpose of this lecture is to develop the notion of a category over another category.
We will draw on the following materials:
 Ahrens and Lumsdaine. Displayed Categories.
 Benabou. Fibered categories and the foundations of naive category theory.
 Borceux. Handbook of Categorical Algebra 2: Categories and Structures.
 Jacobs. Categorical Logic and Type Theory .
 Streicher. Fibered Categories à la Jean Bénabou.
This material is deeply influenced by conversations with Thomas Streicher, as well as his writings.
1. Foundational assumptions [000R]
A metacategory $\mathfrak{C}$ is defined by explaining what an object of $\mathfrak{E}$ is, and, given two objects $x,y\in \mathfrak{E}$, what a morphism from $x$ to $y$ is, together with the following operations:
 for each object $x\in \mathfrak{E}$, an identity map $\Idn{x} : x \to x$,
 for any two maps $f:x\to y$ and $g:y\to z$, a composite map $f;g : x \to z$,
 such that the following equations hold: \[ \Idn{x};h = h\qquad h;\Idn{y} = h\qquad f;(g;h) = (f;g);{h} \]
In our definition above, we have not imposed any restrictions on what kinds of things the objects and morphisms are; our definition is premathematical, so we do not assume beforehand that there is a such thing as a collection of “all” metacategories.
Remark. We may define analogous notions of metafunctor, etc. But we do not assume that the notion of “all metafunctors $\mathfrak{C}\to\mathfrak{D}$” is welldefined; the notion is entirely schematic.
Assumption. We assume a metacategory $\BoldSymbol{\mathfrak{Coll}}$ whose objects we will refer to as “collections”. We assume that the metacategory of all collections satisfies the axioms of Lawvere’s ETCS.
A category $E$ is defined to be a metacategory whose objects are defined to be the elements of some collection, and for any two objects $x,y\in E$ the morphisms $x\to y$ are defined to be the elements of some collection.
Consequently there exists a metacategory $\BoldSymbol{\mathfrak{Cat}}$ of all categories. Following Lawvere (but deviating from some other authors that ground the notion of metacategories in classes) we notice that $\BoldSymbol{\mathfrak{Cat}}$ is cartesian closed; in other words, all functor categories exist regardless of size.
Assumption. At times we may assume that there exists a category $\SET\subseteq\BoldSymbol{\mathfrak{Coll}}$ of collections that we will refer to as sets, such that $\SET$ is closed under the axioms of ETCS. Rather than work with $\SET$ at all times, our approach is to use the tools of relative category theory to objectify the notions of “small” and “locally small” category over any category $B$, generalizing the role of $\SET$ from classical category theory.
2. Displayed categories and fibrations [0008]
Let $B$ be a category. A displayed category $E$ over $B$ is defined by the following data (Ahrens & Lumsdaine, 2019):
 for each object $x\in B$, a collection of displayed objects $E\Sub{x}$,
 for each morphism $f : x \to y\in B$ and displayed objects $\bar{x}\in E\Sub{x}$ and $\bar{y}\in E\Sub{y}$, a family of collections of displayed morphisms $E\Sub{f}(\bar{x},\bar{y})$, which we may also write $\bar{f}:\bar{x}\to\Sub{f} \bar{y}$,
 for each $x\in B$ and $\bar{x}\in E\Sub{x}$, a morphism $\Idn{\bar{x}} \in E\Sub{\Idn{x}}(\bar{x},\bar{x})$,
 for each $f : x \to y$ and $g:y \to z$ in $B$ and objects $\bar{x}\in E\Sub{x}, \bar{y}\in E\Sub{y}, \bar{z}\in E\Sub{z}$, a function \[ E\Sub{f}(\bar{x},\bar{y}) \times E\Sub{g}(\bar{y},\bar{z}) \to E\Sub{f;g}(\bar{x},\bar{z}) \] that we will denote like ordinary (diagrammatic) function composition,
 such that the following equations hold: \[ \Idn{\bar{x}};\bar{h} = \bar{h}\qquad \bar{h};\Idn{\bar{y}} = \bar{h}\qquad \bar{f};(\bar{g};\bar{h}) = (\bar{f};\bar{g});\bar{h} \] Note that these are welldefined because of the corresponding laws for the base category $B$.
Notation. When we have too many subscripts, we will write $E[x]$ instead of $E\Sub{x}$.
Let $E$ be displayed over $B$, and let $f:x\to y \in B$; a morphism $\bar{f}:\bar{x}\to\Sub{f} \bar{y}$ in $E$ is called cartesian over $f$ when for any $m:u\to x$ and $\bar{h}:\bar{u}\to\Sub{m;f} \bar{y}$ there exists a unique $\bar{m} : \bar{u}\to\Sub{m} \bar{x}$ with $\bar{m};\bar{f} = \bar{h}$. We visualize this unique factorization of $\bar{h}$ through $\bar{f}$ over $m$ as follows:
Above we have used the “pullback corner” to indicate $\bar{x}\to\bar{y}$ as a cartesian map. We return to this in our discussion of the selfindexing [0003] of a category.
A displayed category $E$ over $B$ is said to be a cartesian fibration, when for each morphism $f : x \to y$ and displayed object $\bar{y}\in E\Sub{y}$, there exists a displayed object $\bar{x}\in E\Sub{x}$ and a cartesian morphism $\bar{f} : \bar{x}\to\Sub{f} \bar{y}$ in the sense of Definition 2·b [0001]. Note that the pair $(\bar{x},\bar{f})$ is unique up to unique isomorphism, so being a cartesian fibration is a property of a displayed category.
There are other variations of fibration. For instance, $E$ is said to be an isofibration when the condition above holds just for isomorphisms $f : x \cong y$ in the base.
2.1. The fundamental selfindexing [0003]
Let $B$ be an ordinary category; there is an important displayed category $\SelfIx{B}$ over $B$ given fiberwise by the slices of $B$.
 For $x\in B$, we define $\SelfIx{B}\Sub{x}$ to be the collection $\Sl{B}{x}$ of pairs $(\bar{x}\in B,p\Sub{x}:\bar{x}\to x)$.
 For $f : x\to y\in B$, we define $\SelfIx{B}\Sub{f}$ to be the collection of commuting squares in the following configuration:
Prove that $\SelfIx{B}$ from [001X] is a cartesian fibration if and only if $B$ has pullbacks.
2.2. The generalized pullback lemma [0014]
In light of [0003], the following result for displayed categories generalizes the ordinary “pullback lemma.”
Let $\bar{f} : \bar{x}\to\Sub{f}\bar{y}$, and suppose that $\bar{g} : \bar{y}\to\Sub{g}\bar{z}$ is cartesian over $g$. Then $\bar{f};\bar{g}$ is cartesian over $f;g$ if and only if $\bar{f}$ is cartesian over $f$.
Proof. Suppose first that $\bar{f}$ is cartesian. To see that $\bar{f};\bar{g}$ is cartesian, we must construct a unique factorization as follows: Because $\bar{g}$ is cartesian, we can factor $\bar{h} = i;\bar{g}$ for a unique $i:\bar{u}\to\Sub{m;f}\bar{y}$. Then, because $\bar{f}$ is cartesian, we can further factor $i = j;\bar{f}$ for a unique $j:\bar{u}\to\Sub{m}\bar{x}$. We conclude that there is a unique $j:\bar{u}\to\Sub{m}\bar{x}$ for which $\bar{h} = j;\bar{f};\bar{g}$, as required.
Conversely, suppose that $\bar{f};\bar{g}$ is cartesian. To see that $\bar{f}$ is cartesian, we must construct a unique factorization as follows: Because $\bar{f};\bar{g}$ is cartesian, we can factor $\bar{h};\bar{g} = i;\bar{f};\bar{g}$ for a unique $i:\bar{u}\to\Sub{m}\bar{x}$. On the other hand, because $\bar{g}$ is cartesian, there is a unique $j:\bar{u}\to\Sub{m;f}\bar{y}$ for which $\bar{h};\bar{g} = j;\bar{g}$; as both $\bar{h}$ and $i;\bar{f}$ satisfy this condition, we conclude $\bar{h}=i;\bar{f}$. Therefore, there is a unique $i:\bar{u}\to\Sub{m}\bar{x}$ for which $\bar{h} = i;\bar{f}$, as required. ∎
2.3. An alternative definition of fibration [0029]
Warning. Some authors including Grothendieck (Revêtements Étales Et Groupe Fondamental (SGA 1), 1971) give an equivalent definition of cartesian fibration that factors through a nonequivalent definition of cartesian morphisms. Such authors refer to our notion of cartesian morphism as hypercartesian (Streicher, 2018).
Let $E$ be displayed over $B$, and let $f:x\to y \in B$; a morphism $\bar{f}:\bar{x}\to\Sub{f} \bar{y}$ in $E$ is called hypocartesian over $f$ when for any $\bar{u}\in E\Sub{x}$ and $\bar{h}:\bar{u}\to\Sub{f} \bar{y}$ there exists a unique $i : \bar{u}\to\Sub{\Idn{x}} \bar{x}$ with $i;\bar{f} = \bar{h}$ as follows:
Cartesian morphisms are clearly hypocartesian (setting $u=x$ and $m=\Idn{x}$), but the converse does not hold. The problem is that in an arbitrary displayed category, hypocartesian morphisms may not be closed under composition.
Let $E$ be a cartesian fibration in the sense of Definition 2·c [0002], and let $\bar{f} : \bar{x}\to\Sub{f}\bar{y}$ be displayed over $f:x\to y$. The displayed morphism $\bar{f}$ is cartesian if and only if it is hypocartesian.
Proof. Any cartesian map is clearly hypocartesian. To see that a hypocartesian map $\bar{f}:\bar{x}\to\Sub{f}\bar{y}$ in a cartesian fibration is cartesian, we consider the cartesian lift of $f:x\to y$ under $\bar{y}$:
As the cartesian lift $\bar{x}\tick\to \bar{y}$ is also hypocartesian, it follows that there is a unique vertical isomorphism identifying $\bar{x}$ with $\bar{x}\tick$ factoring $\bar{f} : \bar{x}\to\Sub{f}\bar{y}$ through $\bar{f}\tick : \bar{x}\tick\to\Sub{f}\bar{y}$. Being cartesian over $f$ is clearly stable under isomorphism, hence we conclude that $\bar{f}$ is cartesian from the fact that $\bar{f}\tick$ is cartesian. ∎
Grothendieck (Revêtements Étales Et Groupe Fondamental (SGA 1), 1971) defines a fibration in terms of (what we refer to as) hypocartesian morphisms rather than (what we refer to as) cartesian morphisms, and therefore imposes the additional constraint that the hypocartesian morphisms be closed under composition. In Lemma 2.3·c [002B] below, we verify that these two definitions of cartesian fibration coincide.
Let $E$ be displayed over $B$. Then $E$ is a cartesian fibration in the sense of Definition 2·c [0002] if and only if the following two conditions hold:
 Hypocartesian lifts. For each $f:x\to y\in B$ and $\bar{y}\in E\Sub{y}$ there exists a displayed object $\bar{x}\in E\Sub{x}$ and hypocartesian morphism $\bar{f}:\bar{x}\to\Sub{f}\bar{y}$.
 Closure under composition. If $\bar{f}:\bar{x}\to\Sub{f}\bar{y}$ and $\bar{g}:\bar{y}\to\Sub{g}\bar{z}$ are hypocartesian, then $\bar{f};\bar{g}$ is hypocartesian.
Proof. Suppose first that $E$ is a cartesian fibration in our sense. Then $E$ has hypocartesian lifts because it has cartesian lifts. For closure under composition, fix hypocartesian $\bar{f},\bar{g}$; by Lemma 2.3·b [002C] we know that $\bar{f},\bar{g}$ are also cartesian and hence by Lemma 2.2·a [001H] so is the composite $\bar{f};\bar{g}$; therefore it follows that $\bar{f};\bar{g}$ is also hypocartesian.
Conversely, suppose that $E$ is a cartesian fibration in the sense of Grothendieck, and let $\bar{f}:\bar{x}\to\Sub{f}\bar{y}$ be the hypocartesian lift of $f:x\to y$ at $\bar{y}\in E\Sub{y}$; we shall see that $\bar{f}$ is also a cartesian lift of $f$ at $\bar{y}$ by constructing a unique factorization as follows: Let $\bar{m}:\bar{u}\tick\to\Sub{m}\bar{x}$ be the hypocartesian lift of $m$ at $\bar{x}$, where $\bar{u}\tick\in E\Sub{u}$. By hypothesis, the composite $\bar{m};\bar{f} : \bar{u}\tick\to\Sub{m;f}\bar{y}$ is hypocartesian, so $\bar{h}$ factors uniquely through $\bar{m};\bar{f}$ over $\Idn{u}$: The composite $i;\bar{m} : \bar{u}\to\Sub{m}\bar{x}$ is the required (cartesian) factorization of $\bar{h}$ through $\bar{f}$ over $m$. To see that $i;\bar{m}$ is the unique such map, we observe that all morphisms $\bar{u}\to\Sub{m}\bar{x}$ factor uniquely through $\bar{m}$ over $\Idn{u}$ as a consequence of $\bar{m}$ being hypocartesian. ∎
Hypocartesian [002A] and cartesian [0001] morphisms can be thought of as two distinct ways to generalize the concept of a pullback, depending on what one considers the essential properties of pullbacks. Hypocartesian morphisms more directly generalize the “little picture” universal property of pullbacks as limiting cones, whereas cartesian morphisms generalize the “big picture” dynamics of the pullback pasting lemma. As we have seen in Lemma 2.3·b [002C] these two notions coincide in any cartesian fibration; the instance of this result for the fundamental selfindexing (Construction 2.1·a [001X]) verifies that pullbacks can be equivalently presented in terms of cartesian morphisms, as we have pointed out in Exercise 2.1·b [001Y].
2.4. Displayed and fibered functors [0004]
Let $E$ be displayed over $B$ and let $F$ be displayed over $C$. If $U:B \to C$ is an ordinary functor, than a displayed functor from $E$ to $F$ over $U$ is given by the following data:
 for each displayed object $\bar{x}\in E\Sub{x}$, a displayed object $\bar{U}\bar{x}\in F\Sub{Ux}$,
 for each displayed morphism $\bar{f} : \bar{x}\to\Sub{f}\bar{y}$, a displayed morphism $\bar{U}\bar{f} : \bar{U}\bar{x}\to\Sub{Uf}\bar{U}\bar{y}$,
 such that the assignment $\bar{U}f$ preserves displayed identities and displayed composition.
From this notion, we can see the variation of displayed categories over their base categories itself has a “displayed categorical” structure; up to size issues, we could speak of the displayed bicategory of displayed categories.
Note. The correct notion of morphism between cartesian fibrations is given by displayed functors that preserve cartesian maps. We will call these fibered functors.
2.5. Fiber categories and vertical maps [0005]
Let $E$ be a category displayed over $B$. A vertical map in $E$ is defined to be one that lies over the identity map in $B$. For every $b\in B$, there the collection $E\Sub{b}$ of displayed objects has the structure of a category; in particular, we set $E\Sub{b}(u,v)$ to be the collection of vertical maps $u\to\Sub{\Idn{b}}v$.
2.6. Opposite categories [000Q]
We adapt Bénabou’s construction as reported by Streicher (Fibred Categories à La Jean Bénabou, 2018).
Let $E$ be fibered over $B$; we may define the opposite fibered category $\OpCat{E}$ over $B$ like so:

An object of $\OpCat{E}\Sub{x}$ is given by an object of $E\Sub{x}$.

Given $f : x \to y\in B$, a morphism $\bar{x}\to_f \bar{y}$ in $\OpCat{E}$ is given in terms of $E$ by a cartesian map $\bar{y}\Sub{f} : \bar{y}\Sub{x} \to\Sub{f} \bar{y}$ together with a vertical map $h : \bar{y}\Sub{x}\to\Sub{\Idn{x}} \bar{y}$ as depicted below: such that $\brc{\bar{x} \leftarrow \bar{y}\Sub{x}\Sup{1}\to \bar{y}}$ is identified with $\brc{\bar{x}\leftarrow\bar{y}\Sub{x}\Sup{2}\to \bar{y}}$ when they agree up to the unique vertical isomorphism $\bar{y}\Sub{x}\Sup{1}\cong\bar{y}\Sub{x}\Sup{2}$ induced by the universal property of cartesian maps in the sense that the following diagram commutes:
2.6.1. Characterization of cartesian maps [000T]
There is a simple characterization of cartesian maps in $\OpCat{E}$.
A morphism $\bar{f}:\bar{x}\to\Sub{f} \bar{y}\in\OpCat{E}$ is cartesian over $f:x\to y$ if and only if the vertical leg of $f$ is an isomorphism.
Proof. Suppose that $\bar{f} : \bar{x}\to\Sub{f}\bar{y}$ is represented by a span $\brc{\bar{x}\leftarrow\bar{y}\Sub{x}\to\bar{y}}$ in $E$ in which the vertical leg $\bar{x}\leftarrow\bar{y}\Sub{x}$ is an isomorphism. We must show that $\bar{x}\to_f\bar{y}$ is cartesian in $\OpCat{E}$. We fix a morphism $\bar{h}:\bar{w}\to\Sub{m;f}\bar{y}\in \OpCat{E}$ where $m:w\to x$, depicted below in terms of $\OpCat{E}$:
We must define the unique intervening map $\bar{w}\to_m \bar{x}$ in $\OpCat{E}$. We first translate the above into the language of $E$ by unfolding definitions:
The desired intervening map $\bar{w}\to\Sub{m} \bar{x}\in \OpCat{E}$ shakes out in the language of $E$ to be a span $\brc{\bar{w}\leftarrow \bar{x}\Sub{w}\to\Sub{m} \bar{x}}$ in which the lefthand leg is vertical and the righthand leg is cartesian over $m:w\to x$. But the lefthand span $\brc{\bar{w}\leftarrow\bar{y}\Sub{w}\to \bar{y}\Sub{x}\cong \bar{x}}$ in the diagram above is exactly what we need.
We leave the converse to the reader. ∎
2.6.2. Cartesian lifts in the opposite category [000U]
The foregoing characterization of cartesian maps in $\OpCat{E}$ immediately implies that $\OpCat{E}$ is fibered over $B$.
The displayed category $\OpCat{E}$ is a cartesian fibration.
Proof. Fixing $\bar{y}\in \OpCat{E}\Sub{y}$ and $f:x\to y\in B$, we must exhibit a cartesian lift $\bar{f} : \bar{x}\to\Sub{f}\bar{y}\in \OpCat{E}$. By the characterization [000T] it suffices to find any map over $f$ whose vertical component is an isomorphism. Writing $\bar{y}\Sub{x}\to\Sub{f}\bar{y}$ for the cartesian lift of $f$ in $E$, consider the map in $\OpCat{E}$ presented by the following span in $E$: ∎
2.6.3. Exegesis of opposite categories [000S]
The construction of fibered opposite categories (Construction 2.6·a [001Z]) does appear quite involved, but it can be seen to be inevitable from the perspective of the fiber categories $\OpCat{E}\Sub{x}$ (Section 2.5 [0005]). Indeed, let $u,v\in \OpCat{E}\Sub{x}$ and fix a vertical map $h : u \to v\in \OpCat{E}\Sub{x}$; by unfolding definitions, we see that the vertical map $h : u \to v$ is uniquely determined by a morphism $v\to u\in E\Sub{x}$.
Proof. A displayed morphism $u\to\Sub{\Idn{x}} v\in \OpCat{E}$ is determined by a span $\brc{u\leftarrow v\Sub{x} \to v}\in E$ where the righthand map is cartesian over $\Idn{x} : x\to x$ and the lefthand map is vertical, taken up to the identification of different cartesian lifts $v\Sub{x}\to x$. A displayed morphism that is cartesian over the identity is an isomorphism; hence, displayed morphisms $u\to\Sub{\Idn{x}} v\in\OpCat{E}$ are equivalently determined by vertical maps $v\to u \in E$. ∎
2.7. Example: the family fibration [0006]
Any ordinary category $C$ can be viewed as a displayed category $\FAM{C}$ over $\SET$:
 For $S\in \SET$, an object in $\FAM{C}[S]$ is specified by a functor $C^S$ where $S$ is regarded as a discrete category.
 Given $f : S \to T$ in $\SET$ and $x\in C^S$ and $y\in C^T$, a morphism $x \to\Sub{f} y$ is given by a morphism $x\to \InvImg{f}y$ in $C^S$ where $\InvImg{f} : C^T \to C^S$ is precomposition with $f$.
The displayed category $\FAM{C}$ is in fact a cartesian fibration. This family fibration is the starting point for developing a relative form of category theory, the purpose of this lecture. By analogy with viewing an ordinary category $C$ as a fibration $\FAM{C}$ over $\SET$, we may reasonably define a “relative category” over another base $B$ to be a fibration over $B$.
This story for relative category theory reflects the way that ordinary categories are “based on” $\SET$ in some sense in spite of the fact that they do not necessarily have sets of objects or even sets of morphisms between objects. Being small and locally small respectively will later be seen to be properties of a family fibration over an arbitrary base $B$, strictly generalizing the classical notions.
2.8. Change of base [0007]
Suppose that $E$ is displayed over $B$ and $F : X\to B$ is a functor; then we may define a displayed category $\InvImg{F}E$ as over $X$ follows:

An object of $(\InvImg{F}E)\Sub{x}$ is an object of $E\Sub{Fx}$.

Given $\bar{x}\in (\InvImg{F}E)\Sub{x}$, $\bar{y}\in (\InvImg{F}E)\Sub{y}$ and $f : x \to y$, a morphism $\bar{x}\to\Sub{f}\bar{y}$ in $\InvImg{F}E$ is given by a morphism $\bar{x}\to\Sub{Ff}\bar{y}$ in $E$.
We visualize the change of base scenario as follows:
2.9. Full subfibrations and figure shapes [002J]
In a category $E$, a morphism $f : x\to y$ can be thought of as a “figure” of shape $x$ drawn in $y$. For instance, if $x$ is the point (i.e. $x=\ObjTerm{E}$) then a morphism $x\to y$ is a “point” of the “space” $y$. We refer to $x$ as the figureshape in any such scenario. The perspective of morphisms as figures is developed in more detail by Lawvere and Schanuel (Conceptual Mathematics: A First Introduction to Categories, 2009).
It often happens that a useful class of figure shapes can be arranged into a setindexed family $\prn{u\Sub{i}}\Sub{i\in I}$; viewed from the perspective of the family fibration $\FAM{E}$ (Section 2.7 [0006]), this family is just a displayed object $\bar{u}$ over $I$ and then a figure shape “in” this family is given by any cartesian morphism $\bar{z}\to\bar{u}$. We will generalize this situation to the case of an arbitrary fibration, by constructing the full subfibration spanned by displayed objects equipped with a cartesian morphism into $\bar{u}$ in Construction 2.9·a [0010] below.
Let $E$ be a cartesian fibration over $B$; then any displayed object $\bar{x} \in E\Sub{x}$ induces a full subfibration $\FullSubfib{\bar{u}}\subseteq E$ spanned by displayed objects that are classified by $\bar{u}$, i.e. arise from $\bar{u}$ by cartesian lift.

An object of $\FullSubfib{\bar{u}}\Sub{x}$ is specified by an object $\bar{x}\in E\Sub{x}$ together with a cartesian morphism $\bar{x}\to \bar{u}$.

Given $f:x\to y\in B$, a morphism from $\bar{x}\to \bar{u}$ to $\bar{y}\to\bar{u}\in$ over $f$ is given by any displayed morphism $\bar{x}\to\Sub{f}\bar{y}$.
Let $E$ be a cartesian fibration and let $\FullSubfib{\bar{s}}\subseteq E$ be the full subfibration determined by a displayed object $\bar{s}\in E$ as in Construction 2.9·a [0010]. We now develop the following vocabulary:

We will refer to each object of $\FullSubfib{\bar{s}}$ as a $\bar{s}$figure shape.

A displayed morphism $\bar{z}\to \bar{x}$ is called a $\bar{s}$figure whenever $\bar{z}\in\FullSubfib{\bar{s}}$.
3. The Grothendieck construction [0009]
3.1. The total category and its projection [000A]
Note that any displayed category $E$ over $B$ can be viewed as an undisplayed category $\TotCat{E}$ equipped with a projection functor $p\Sub{E}: \TotCat{E}\to B$; in this case $\TotCat{E}$ is called the total category of $E$.
 An object of $\TotCat{E}$ is given by a pair $(x,\bar{x})$ where $x\in B$ and $\bar{x}\in E\Sub{x}$.
 A morphism $(x,\bar{x})\to (y,\bar{y})$ in $\TotCat{E}$ is given by a pair $(f,\bar{f})$ where $f:x\to y$ and $\bar{f}:\bar{x}\to\Sub{f}\bar{y}$.
The construction of the total category of a displayed category is called the Grothendieck construction.
Prove that the total category $\TotCat{\SelfIx{B}}$ of the fundamental selfindexing (Section 2.1 [0003]) is the arrow category $B^{\to}$, and the projection is the codomain functor.
3.2. Displayed categories from functors [000B]
In many cases, one starts with a functor $P:E\to B$; if it were meaningful to speak of equality of objects in an arbitrary category then there would be an obvious construction of a displayed category $P\Sub{\bullet}$ from $P$; we would simply set $P\Sub{x}$ to be the collection of objects $u\in E$ such that $Pu=x$. As it stands there is a more subtle version that will coincide up to categorical equivalence with the naïve one in all cases that the latter is meaningful.

We define an object of $P\Sub{x}$ to be a pair $(u,\phi\Sub{u})$ where $u\in E$ and $\phi\Sub{u} : Pu\cong x$. It is good to visualize such a pair as a “crooked leg” like so:

A morphism $(u,\phi\Sub{u})\to\Sub{f} (v,\phi\Sub{v})$ over $f : x \to y$ is given by a morphism $h : u\to v$ that lies over $f$ modulo the isomorphisms $\phi\Sub{u},\phi\Sub{v}$ in sense depicted below:
Suppose that $B$ is an internal category in $\mathbf{Set}$, i.e. it has a set of objects. Exhibit an equivalence of displayed categories between $P\Sub{\bullet}$ as described above, and the naïve definition which $E\Sub{x}$ is the collection of objects $u\in E$ such that $Pu = x$.
We have a functor $\TotCat{P\Sub{\bullet}}\to E$ taking a pair $(x,(u,\phi\Sub{u}))$ to $u$.
Explicitly construct the functorial action of $\TotCat{P\Sub{\bullet}}\to E$.
Verify that $\TotCat{P\Sub{\bullet}}\to E$ is a categorical equivalence.
3.2.1. Relationship to Street's fibrations [000C]
In classical category theory, cartesian fibrations are defined by Grothendieck (Revêtements Étales Et Groupe Fondamental (SGA 1), 1971) to be certain functors $E\to B$ such that any morphism $f:x\to Pv$ in $B$ lies strictly underneath a cartesian morphism in $E$. As we have discussed, this condition cannot be formulated unless equality is meaningful for the collection of objects of $B$.
There is an alternative definition of cartesian fibration (Street, 1980) that avoids equality of objects; here we require for each $f:x\to Pv$ a cartesian morphism $h:\InvImg{f}v \to v$ together with an isomorphism $\phi : P(\InvImg{f}v)\cong x$ such that $\phi^{1};Ph = f$.
By unrolling definitions, it is not difficult to see that the displayed category $P\Sub{\bullet}$ is a cartesian fibration in our sense if and only if the functor $P:E\to B$ was a fibration in Street’s sense. Moreover, it can be seen that the Grothendieck construction yields a Grothendieck fibration $\TotCat{P\Sub{\bullet}}\to B$; hence we have introduced by accident a convenient destription of the strictification of Street fibrations into equivalent Grothendieck fibrations.
3.3. Iteration and pushforward [000D]
It also makes sense to speak of categories displayed over other displayed categories; one way to formalize this notion is as follows. Let $E$ be displayed over $B$; we define a category displayed over $E$ to be simply a category displayed over the total category $\TotCat{E}$.
Now let $F$ be displayed over $E$ over $B$. Then we may regard $F$ as a displayed category $B\Sub{!}F$ over $B$ as follows:
 An object of $(B\Sub{!}F)\Sub{x}$ is a pair $(\bar{x},{\ddot{x}})$ with $\bar{x}\in E\Sub{x}$ and ${\ddot{x}}\in F\Sub{\bar{x}}$.
 A morphism $(\bar{x},{\ddot{x}})\to\Sub{f}(\bar{y},{\ddot{y}})$ is given by a pair $(\bar{f},{\ddot{f}})$ where $\bar{f}:\bar{x}\to\Sub{f}\bar{y}$ in $E$ and ${\ddot{f}}:{\ddot{x}}\to\Sub{\bar{f}} {\ddot{y}}$ in $F$.
By virtue of Section 3.2 [000B], we may define the pushforward of a displayed category along a functor. In particular, let $E$ be displayed over $B$ and let $U:B\to C$ be an ordinary functor; then we may obtain a displayed category $U\Sub{!}E$ over $C$ as follows:
 First we construct the displayed category $U\Sub{\bullet}$ corresponding to the functor $U:B \to C$.
 We recall that there is a canonical equivalence of categories $\TotCat{U\Sub{\bullet}}\to B$.
 Because $E$ is displayed over $B$, we may regard it as displayed over the equivalent total category $\TotCat{U\Sub{\bullet}}$ by change of base (Section 2.8 [0007]).
 Hence we may define the pushforward $U\Sub{!}E$ to be the displayed category $(U\Sub{\bullet})\Sub{!}E$ as defined above.
4. Properties of fibrations [000E]
4.1. Locally small fibrations [000F]
There are a number of (equivalent) variations on the definition of a locally small fibration. We attempt to provide some intuition for these definitions.
4.1.1. Warmup: locally small family fibrations [000G]
An ordinary category $E$ is called locally small when for any $x,y\in E$ the collection of morphisms $x\to y$ is a set. This property of $E$ can be rephrased in terms of its family fibration (Section 2.7 [0006]) $\FAM{E}$ over $\SET$ as follows.
Consider an index set $I\in \SET$ and two families $u,v\in C^I$. We may define an $I$indexed collection $[u,v]\Sub{i\in I}$ consisting (pointwise) of all the morphisms $u\Sub{i}\to v\Sub{i}$ in $C$:
If $C$ is locally small, $[u,v]\Sub{i\in I}$ is in fact a family of sets for any $I\in\SET$ as each $[u,v]\Sub{i}$ is a set. Conversely, if $[u,v]\Sub{i\in I}$ is a family of sets for any $I\in \SET$, then $C$ is locally small as we may consider in particular the case that $I=\mathbf{1}$.
4.1.2. A more abstract formulation [000H]
We will reformulate the above in a way that uses only the language that makes sense for an arbitrary cartesian fibration, though for now we stick with $\FAM{C}$. Given $u,v\in \FAM{C}[I]$, we have a “relative hom family” $[u,v]\in\Sl{\SET}{I}$, defined in Section 4.1.1 [000G]. The fact that each $[u,v]\Sub{i}$ is the set of all morphisms $u\Sub{i}\to v\Sub{i}$ can be rephrased more abstractly.
First we consider the restriction of $u\in \FAM{C}[I]$ to $\FAM{C}[[u,v]]$ as follows: Explicitly the family $\InvImg{[u,v]}u$ is indexed in a pair of an element $i\in I$ and a morphism $u\Sub{i}\to v\Sub{i}$. We can think of $\InvImg{[u,v]}u$ as the object of elements of $u\Sub{i}$ indexed in pairs $(i,u\Sub{i}\to v\Sub{i})$.
There is a canonical map $\epsilon\Sub{[u,v]}:\InvImg{[u,v]}u\to\Sub{p\Sub{[u,v]}} v$ that “evaluates” each indexing morphism $u\Sub{i}\to v\Sub{i}$.
That each $[u,v]\Sub{i}$ is the set of all morphisms $u\Sub{i}\to v\Sub{i}$ can be rephrased as a universal property: for any family $h\in\Sl{\SET}{I}$ and morphism $\epsilon\Sub{h} : \InvImg{h}u\to\Sub{h} v$ in $\FAM{C}$, there is a unique cartesian map $\InvImg{h}u\to \InvImg{[u,v]}u$ factoring $\epsilon\Sub{h}$ through $\epsilon\Sub{[u,v]}$ in the sense depicted below:
To convince ourselves of this, we note that the family $H \coloneqq \brc{u\Sub{i}\to v\Sub{i}}\Sub{i\in I}$ itself satisfies the universal property above. Indeed, fix a candidate $h \in \Sl{\SET}{I}$ equipped with a map $\epsilon\Sub{h} : \InvImg{h}u \to_h v$. Unfolding the meaning of this map in set theoretical notation, we see that it amounts to a family of maps $\epsilon\Sub{h}[i] : \prod\Sub{x\in h_i} \brc{u_i\to v_i}$ for each $i\in I$; such a family immediately induces the desired map $h\to H$. ∎
4.1.3. The definition of local smallness [000I]
Based on our explorations above, we are now prepared to write down (and understand) the proper definition of local smallness for an arbitrary cartesian fibration $E$ over $B$, which should be thought of as a (potentially large) category relative to $B$.
For any $x\in B$ and displayed objects $u,v\in E\Sub{x}$, we define a hom candidate for $u,v$ to be a span $u\leftarrow \bar{h} \rightarrow v$ in $E$ in which the lefthand leg is cartesian:
In the above, $h$ should be thought of as a candidate for the “hom object” of $u,v$, and $\epsilon\Sub{h}$ should be viewed as the structure of an “evaluation map” for $h$. This structure can be rephrased in terms of a displayed category $\CandHom{x}{u}{v}$ over $\Sl{B}{x}$:

Given $h\in \Sl{B}{x}$, an object of $\CandHom{x}{u}{v}\Sub{h}$ is given by a hom candidate whose apex in the base is $h$ itself. We will write $\bar{h}$ metonymically for the entire hom candidate over $h$.

Given $\alpha:l\to h\in\Sl{B}{x}$ and hom candidates $\bar{l}\in \CandHom{x}{u}{v}\Sub{l}$ and $\bar{h}\in \CandHom{x}{u}{v}\Sub{h}$, a morphism $\bar{h}\to\Sub{\alpha} \bar{l}$ is given by a cartesian morphism $\bar\alpha:\bar{l}\to\Sub{\alpha}\bar{h}$ in $E$ such that the following diagram commutes:
A cartesian fibration $E$ over $B$ is locally small if and only if for each $x\in B$ and $u,v\in E\Sub{x}$, the total category $\TotCat{\CandHom{x}{u}{v}}$ has a terminal object.
4.2. Globally small fibrations [000J]
In ordinary category theory, a category $C$ is called small when the objects of $C$ can be arranged into a set, and so can for every $x,y\in C$ the collection of morphisms $x\to y$. It is useful to separate these two conditions when we generalize them to fibrations. The latter is called local smallness and is discussed and defined in Section 4.1 [000F]; the former is called global smallness by Jacobs (Categorical Logic and Type Theory, 1999) and factors through an important concept: the generic object.
An ordinary category is called globally small when it has a set of objects.
4.2.1. Generic objects [000K]
Up to equivalence of categories, we may detect global smallness of a category $C$ from the perspective of the family fibration $\FAM{C}$ (Section 2.7 [0006]). In particular, a category is equivalent to a globally small category when its family fibration has a generic object in the following sense.
Let $E$ be a cartesian fibration over $B$; a generic object for $E$ is defined to be an object $\bar{u}\in \TotCat{E}$ such that for any $\bar{z}\in \TotCat{E}$ there exists a cartesian map $\bar{z}\to \bar{u}$.
Warning. Our terminology differs from that of Jacobs (Categorical Logic and Type Theory, 1999); what we refer to as a generic object here is Jacobs’ weak generic object. We prefer the unqualified terminology, as generic objects in the stronger sense are very rare.
An ordinary category $C$ is equivalent to a globally small category if and only if the fibration $\FAM{C}$ has a generic object.
Proof. To see that this is the case, suppose that $C$ has a set of objects. Then $C\in\SET$ and we define $\lfloor{C}\rfloor$ to be the displayed object $\brc{x}\Sub{x\in C}\in \FAM{C}[C]$. Fixing $I\in \SET$ and $z\in C^I$, we consider the cartesian map displayed over $z : I \to C$:
Conversely assume that $\FAM{C}$ has a generic object $\bar{u}\in\FAM{C}[U]$ for some $U\in \SET$; then we may equip $U$ with the structure of a globally small category such that $U$ is equivalent to $C$, using a construction that is similar to our implementation of the opposite fibration (Section 2.6 [000Q]). In particular we define a morphism $x\to y\in U$ to be given by the following data:
 a cartesian map $a\to\Sub{x} \bar{u}$ over $x : 1\to U$,
 a cartesian map $b\to\Sub{y} \bar{u}$ over $y : 1\to U$,
 and a vertical map $h:a\to b$ in $\FAM{C}[1]\simeq C$,
such that $(a\Sub{1},b\Sub{1},h\Sub{1})$ is identified with $(a\Sub{2},b\Sub{2},h\Sub{2})$ when $h_1$ and $h_2$ are equal modulo the (unique) vertical isomorphisms between the cartesian lifts in the sense depicted below:
Remember that a cartesian map $a\to\Sub{x}\bar{u}$ is standing for a choice of an object of $C$ encoded by $x\in U$. Because such choices are unique only up to isomorphism, we must include them explicitly in the data. ∎
A cartesian fibration $E$ over $B$ is called globally small when it has a generic object in the sense of Definition 4.2.1·a [001E].
4.3. Separators for cartesian fibrations [002E]
Let $E$ be an ordinary category. In general, to compare two morphisms $f,g:x\to y$ in $E$, it is not enough to see if they agree on global points $u:1\to x$, because the behavior of $u,v$ may differ only on generalized elements. In some cases, however, there is a family of objects $\prn{s\Sub{i}}\Sub{i\in I}\in E$ are together adequate for comparing morphisms of $E$ in the sense of Definition 4.3·a [002G] below.
Given an ordinary category $E$, a setindexed family $\prn{s\Sub{i}}\Sub{i\in I}$ of $E$objects is called a small separating family for $E$ when, assuming that for all $i\in I$ and all $u:s_i\to x$ we have $u;f=u;g$, we then have $f=g$.
The intuition of Definition 4.3·a [002G] is that to compare two morphisms $f,g:x\to y\in E$, it suffices to check that they behave the same on all $s\Sub{i}$shaped figures when $\prn{s\Sub{i}}\Sub{i\in I}$ is a separating family for $E$.
In the category of sets, to compare two morphisms it is enough to check that they agree on global points. This means that the unary family $\brc{\ObjTerm{\SET}}$ is a separator for $\SET$, a property referred to more generally as wellpointedness.
We will now generalize Definition 4.3·a [002G] to the case of a cartesian fibration.
Let $\bar{s}$ be a displayed object in a cartesian fibration $E$ over $B$. A pair of displayed morphisms $f,g:\bar{x}\to \bar{y}\in E$ are said to agree on $\bar{s}$figures when for any $\bar{s}$figure $h : \bar{z}\to \bar{x}$ in the sense of Definition 2.9·b [002K], we have $h;f = h;g : \bar{z}\to \bar{y}$.
Let $E$ be a cartesian fibration over $B$ such that $B$ has binary products. A displayed object $\bar{s}\in E\Sub{s}$ is said to be a small separator for $E$ when any two vertical maps $f,g:\bar{u}\to\Sub{\Idn{x}}\bar{v}\in E\Sub{x}$ are equal when they are agree on $\bar{s}$figures in the sense of Definition 4.3·c [002I].
4.4. Definable classes à la Bénabou [002L]
A class of sets $\mathfrak{C}$ is sometimes said to be formally definable when there is a formula $\prn{x \mid \phi\Sub{\mathfrak{C}}\prn{x}}$ in the language of set theory such that a set $S$ lies in $\mathfrak{C}$ if and only if $\phi\Sub{\mathfrak{C}}\prn{S}$ holds. This concept is a bit sensitive, as it presupposes that we have a notion of “class” whose constituents are not all definable in this sense.
A better behaved notion of definability for sets than the formal one is given modeltheoretically, i.e. relative to a model $\mathscr{M}$ of set theory in some ambient set theory (Bénabou, 1985). We will refer to an element of $\mathscr{M}$ as a set, and a subcollection of $\mathscr{M}$ as a class.
A class of sets $\mathfrak{C}\subseteq\mathscr{M}$ is called representable when there is a set $C\in\mathscr{M}$ such that $U\in C$ if and only if $U\in\mathfrak{C}$.
A class of sets $\mathfrak{C}\subseteq\mathscr{M}$ is called definable when for any representable class $\mathfrak{S}$, the class $\mathfrak{C}\cap\mathfrak{S}$ is representable.
Bénabou then generalizes the definitions above to an arbitrary fibration, in such a way that the general fibered notion of definable class is equivalent in the fundamental selfindexing $\SelfIx{\mathscr{M}}$ to that of definable classes in the sense of Definition 4.4·b [002V].
4.4.1. Settheoretic intuition for Bénabou's definability [002Q]
To motivate Bénabou’s general notion of definability, we will first develop an alternative perspective on definability for classes of sets in terms of families of sets.
Let $\mathfrak{C}\subseteq\mathscr{M}$ be a class of sets; there exists a class $\bar{\mathfrak{C}}$ of families of sets that contains $\prn{S\Sub{i}}\Sub{i\in I}$ exactly when each $S\Sub{i}$ lies in $\mathfrak{C}$. We will refer to $\bar{\mathfrak{C}}$ as the closure under base change of $\mathfrak{C}$, a name motivated by the fact that when $\prn{S\Sub{i}}\Sub{i\in I}$ lies in $\bar{\mathfrak{C}}$, then for any $u:J\to I$, the base change $\prn{S\Sub{uj}}\Sub{j\in J}$ also lies in $\bar{\mathfrak{C}}$.
Conversely to Construction 4.4.1·a [002M] we may take a class of families of sets $\mathfrak{F}$ to the the class of sets $\mathfrak{F}\Sub{1}\subseteq{\mathscr{M}}$ spanned by sets $S$ such that the singleton family $\brc{S}$ lies in $\mathfrak{C}$.
A class of families of sets $\mathfrak{F}$ is said to be definable when it is stable and moreover, for any family of sets $\prn{S\Sub{i}}\Sub{i\in I}$, there exists a subset $J\subseteq I$ such that the base change $\prn{S\Sub{j}}\Sub{j\in J}$ lies in $\mathfrak{F}$, and moreover, such that $u:K\to I$ factors through $J\subseteq I$ whenever the base change $\prn{S\Sub{uk}}\Sub{k\in K}$ lies in $\mathfrak{F}$.
In other words, a stable class of families of sets is definable when any family of sets can be restricted to a “biggest” subfamily that lies in the class.
Let $\mathfrak{C}\subseteq\mathscr{M}$ be a class of sets; then $\bar{\mathfrak{C}}$ is a definable class of families of sets if and only if $\mathfrak{C}$ is a definable class of sets.
Proof. Suppose that $\mathfrak{C}$ is a definable class of sets. To check that $\bar{\mathfrak{C}}$ is a definable class of families of sets, we fix a family $\prn{S\Sub{i}}\Sub{i\in I}$ not necessarily lying in $\bar{\mathfrak{C}}$. Because $\mathfrak{C}$ is definable, the intersection $\mathfrak{C}\cap \bigcup\Sub{i\in I}S\Sub{i}$ is represented by a set $U$. We therefore take the subset $J = \brc{i \in I\mid S_i\in U}\subseteq I$, and verify that the base change $\prn{S\Sub{j}}\Sub{j\in J}$ is the largest approximation of $\prn{S\Sub{i}}\Sub{i\in I}$ by a family lying in $\bar{\mathfrak{C}}$.
Conversely suppose that $\bar{\mathfrak{C}}$ is a definable class of families of sets. To see that $\mathfrak{C}$ is definable, we fix a class $\mathfrak{U}$ represented by a set $U\in\mathscr{M}$ to check that $\mathfrak{C}\cap\mathfrak{U}$ is representable. We consider the family of sets $\prn{u}\Sub{u\in U}$; because $\bar{\mathfrak{C}}$ is definable, there is a largest subset $V\subseteq U$ such that the change of base $\prn{v}\Sub{v\in V}$ lies in $\bar{\mathfrak{C}}$, i.e. such that each $v\in V$ lies in $\mathfrak{C}$. Therefore $\mathfrak{C}\cap\mathfrak{U}$ is represented by the set $V$. ∎
4.4.2. Bénabou's notion of definability [002S]
We will now construe Section 4.4.1 [002Q] as the instantiation at the fundamental selfindexing $\SelfIx{\mathscr{M}}$ of a more general notion of definability for classes of objects in a cartesian fibration, defined forthwith. The following definition of definability in a cartesian fibration is due to Bénabou, but is discussed in print by Borceux (Handbook of Categorical Algebra 2 – Categories and Structures, 1994), Jacobs (Categorical Logic and Type Theory, 1999), Streicher (Fibred Categories à La Jean Bénabou, 2018).
Let $E$ be a cartesian fibration over $B$. A definable class $\mathfrak{F}$ in $E$ is a stable subcollection of the displayed objects of $E$ such that for any $\bar{u}\in E\Sub{u}$, there exists a cartesian map $\bar{v}\to \bar{u}$ lying over a monomorphism $v\rightarrowtail u$ such that $\bar{v}\in \mathfrak{F}$ and, moreover, any cartesian morphism $\bar{w}\to\bar{u}$ such that $\bar{w}\in\mathfrak{F}$ factors through $\bar{v}\to\bar{u}$.
Let $\mathscr{M}$ be a model of ETCS; and let $\mathfrak{C}$ be a class of families of sets in $\mathscr{M}$. Then $\mathfrak{C}$ is a class of objects in the fundamental selfindexing $\SelfIx{\mathscr{M}}$ over $\mathscr{M}$. Furthermore, $\mathscr{M}$ a definable class in $\SelfIx{\mathscr{M}}$ in the sense of Definition 4.4.2·a [002W] if and only if it is a definable class of families of sets in the sense of Definition 4.4.1·c [002P].
5. Small fibrations and internal categories [000N]
The purpose of this section is to develop the relationship between internal categories (categories defined in the internal language of a category $B$) and cartesian fibrations over $B$, generalizing the relationship between categories internal to $\SET$ (i.e. small categories) and their family fibrations over $\SET$.
A cartesian fibration is called small when it is both locally small [000I] and globally small [000J].
We have already seen in Section 4.1.1 [000G] and Theorem 4.2.1·b [000L] that smallness in the sense of the definition above appropriately generalizes the ordinary notion of smallness for categories over $\SET$. Another perspective on smallness is given by the internal language, in which a category is viewed as an algebra for the “theory of categories” computed in another category with enough structure. The notion of internal categories is credited (independently) to Alexander Grothendieck and Charles Ehresmann.
5.1. Internal categories [000O]
The notion of a (meta)category is an essentially algebraic theory. As such it is possible to compute models of this theory in any category that has finite limits.
Let $E$ be a category with finite limits; then an internal category in $E$ is defined by the following data:
 an object of objects $C\Sub{0}\in E$,
 an object of morphisms $C\Sub{1}\in E$,
 source and target morphisms $s,t:C\Sub{1}\to C\Sub{0}$,
 a generic identity morphism $C\Sub{0}\to C\Sub{1}$,
 a generic composition morphism $C\Sub{1}\times\Sub{C\Sub{0}}C\Sub{1}\to C\Sub{1}$,
 satisfying a number of laws corresponding to those of a category.
For the details of these laws, we refer to the nLab (internal category).
5.2. The externalization of an internal category [000V]
Let $C$ be an internal category in $E$. We may define a fibered category $\brk{C}$ over $E$ called the externalization of $C$.

Given $x\in E$, an object of $\brk{C}\Sub{x}$ is defined to be a morphism $x\to C\Sub{0}$ in $E$.

Given $x,y\in E$ and $f:x\to y$ and $u \in \brk{C}\Sub{x}$ and $v\in \brk{C}\Sub{y}$, a morphism $u\to\Sub{f} v$ is defined to be a morphism $h : x\to C\Sub{1}$ in $E$ such that the following diagram commutes:
The externalization [000V] is a cartesian fibration.
Proof. Given an object $v\in \brk{C}\Sub{y}$ and a morphism $f:x\to y$ in $E$, we may define a cartesian lift $\InvImg{f}v\to\Sub{f} v$ by setting $\InvImg{f}v = v\circ f : x \to C\Sub{0}$. ∎
The externalization [000V] is globally small
Proof. We may choose a generic object [000K] for $\brk{C}$, namely the identity element $(C\Sub{0},\Idn{C\Sub{0}})\in \TotCat{\brk{C}}$. Given any object $(x,u)\in \TotCat{\brk{C}}$ the cartesian map $(x,u)\to (C\Sub{0},\Idn{C\Sub{0}})$ is given as follows: ∎
The externalization [000V] is locally small
Proof. Fix $x\in E$ and $u,v\in \brk{C}\Sub{x}$, we must exhibit a terminal object to the (total) category $\TotCat{\CandHom{x}{u}{v}}$ of “hom candidates” defined in [000I]. First we define $\brk{u,v}$ to be the following pullback in $E$:
We define $\overline{p}:\InvImg{\brk{u,v}}{u}\to\Sub{p} u\in \brk{C}\Sub{\brk{u,v}}$ to be the cartesian lift of $u\in \brk{C}\Sub{x}$ along $p:\brk{u,v}\to x$:
We need to define a displayed evaluation map $\epsilon : \InvImg{\brk{u,v}}u\to\Sub{p} v$; unraveling the definition of a displayed morphism in the externalization of $C$, we choose the following diagram:
Putting all this together, we assert that the terminal object of $\TotCat{\CandHom{x}{u}{v}}$ is the following span in $\brk{C}$:
Fixing another such candidate hom span $\brc{u \leftarrow \bar{h}\rightarrow v}\in\TotCat{\CandHom{x}{u}{v}}$, according to [000I] we must exhibit a unique cartesian morphism $\bar\alpha : \bar{h}\to \InvImg{\brk{u,v}}{u}$ making the following diagram commute:
First we note that the evaluation map $\epsilon\Sub{h} : \bar{h}\to v$ amounts to an internal morphism $h\to C\Sub{1}$ satisfying the appropriate compatibility conditions. Therefore we may define the base $\alpha:h\to \brk{u,v}$ of the universal map using the universal property of the pullback that defines $\brk{u,v}$:
The morphism $\alpha:h\to \brk{u,v}$ defined above is the unique map in $E$ satisfying the conditions required of the base for $\bar\alpha$; therefore, it suffices to show that there exists a cartesian morphism $\bar\alpha:\bar{h}\to\Sub{\alpha}\InvImg{\brk{u,v}}u$ since it will be unique if it exists. We define $\bar\alpha$ using the universal property of the cartesian lift:
That $\bar{\alpha}:\bar{h}\to\Sub{\alpha}\InvImg{\brk{u,v}}u$ is cartesian follows from the “generalized pullback lemma” for cartesian morphisms [0014]: it suffices to observe that both $\bar{p}\Sub{h}:\bar{h}\to u$ and its second factor $\bar{p}:\InvImg{\brk{u,v}}u\to u$ are cartesian. ∎
5.3. The full internal subcategory associated to a displayed object [0011]
The full internal subfibration (Construction 2.9·a [0010]) associated to a displayed object $\bar{u}$ of a locally small cartesian fibration $E$ over $B$ can be seen to be equivalent to the externalization of an internal category $\gl{\bar{u}}$ in $B$. In particular, we let the object of objects $\gl{\bar{u}}\Sub{0}$ be $u$ itself; defining the object of arrows $\gl{\bar{u}}\Sub{1}$ is more complex, making critical use of the local smalness of $E$ over $B$.
We will think of the fiber $E\Sub{u\times u}$ as the category of objects indexed in the boundary (source and target) of a morphism. Restricting $\bar{u}$ along the source and target projections, we obtain the displayed objects of “points of the source” and “points of the target” respectively:
Because $E$ is locally small, there is an object $\brk{\bar\partial\Sub{1},\bar\partial\Sub{2}}\in \Sl{B}{u\times u}$ that behaves as the “generic hom set”. We define $\gl{\bar{u}}\Sub{1}\in B$ and its source and target projections to be this very object.
The externalization $\brk{\gl{\bar{u}}}$ of the internal category $\gl{\bar{u}}$ is equivalent to $\FullSubfib{\bar{u}}$.
Proof. We will define a fibred equivalence $F : \brk{\gl{\bar{u}}}\to \FullSubfib{\bar{u}}$ over $B$.

Fix $x\in B$ and $\chi\Sub{x} \in \brk{\gl{\bar{u}}}\Sub{x}$, i.e. $\chi\Sub{x} : x\to u$; we define $F\prn{\chi\Sub{x}}$ to be an arbitrary cartesian map $\phi\Sub{x} : \bar{x}\to\Sub{\chi\Sub{x}} \bar{u}$. (Here we have used the axiom of choice for collections [000R].)

Fix $f : x\to y\in B$ and $\chi\Sub{x} :x\to u$ and $\chi\Sub{y}:y\to u$ and a diagram representing a displayed morphism $h$ from $\chi\Sub{x}$ to $\chi\Sub{y}$ over $f$ as below:
We must define $F\prn{h}:\bar{x}\to\Sub{f} \bar{y}$, fixing arbitrary cartesian maps $\bar\chi\Sub{x}:\bar{x}\to\Sub{\chi\Sub{x}}\bar{u}$ and $\bar\chi\Sub{y}:\bar{y}\to\Sub{\chi\Sub{y}}\bar{u}$. First we lift $h:x\to \brk{\bar\partial\Sub{1},\bar\partial\Sub{2}}$ into $E$ using the universal property of the cartesian lift:
By composition with the “evaluation map” for our hom object, we have a map $\bar{x}\to\Sub{f;\chi\Sub{y}}\bar{u}$:
Next we define $F\prn{h}:\bar{x}\to\Sub{f}\bar{y}$ using the universal property of (another) cartesian lift: ∎
5.4. The internalization of a small fibration [000Z]
Let $C$ be a small cartesian fibration (Definition 5·a [001Q]) over $B$ a category with finite limits, i.e. a cartesian fibration that is both locally small (Definition 4.1.3·b [001B]) and globally small (Definition 4.2·b [000P]). We will show that $C$ is equivalent to the externalization [000V] of an internal category [000O] $\underline{C}$ in $B$, namely the full internal subcategory [0011] associated to the generic object $\bar{u}\in C$.
By Theorem 5.3·a [001S] we know that the externalization of $\underline{C}$ sodefined is equivalent to the full subfibration $\FullSubfib{\bar{u}}$ of $C$ spanned by objects that are “classified” by $\bar{u}$. Because $\bar{u}$ is generic, we know that every object of $C$ is classified by $\bar{u}$, so we are done.
6. Other kinds of fibrations [0012]
6.1. Cocartesian fibrations [0015]
Cocartesian fibrations are a dual notion to cartesian fibrations, in which the variance of indexing is reversed.
Let $E$ be displayed over $B$, and let $f:x\to y \in B$; a morphism $\bar{f}:\bar{x}\to\Sub{f} \bar{y}$ in $E$ is called cocartesian over $f$ when for any $m:y\to u$ and $\bar{h}:\bar{x}\to\Sub{f;m} \bar{u}$ there exists a unique $\bar{m} : \bar{y}\to\Sub{m} \bar{u}$ with $\bar{f};\bar{m} = \bar{h}$:
We use a “pushout corner” to indicate $\bar{x}\to\bar{y}$ as a cocartesian morphism, a notation justified by Section 6.1.3 [0019].
A displayed category $E$ over $B$ is a cocartesian fibration when for each $f : x \to y\in B$ and $\bar{x}\in E\Sub{x}$, there exists a displayed object $\bar{y}\in E\Sub{y}$ and a cocartesian morphism $\bar{f} : \bar{x}\to\Sub{f} \bar{y}$.
Remark. These are also known as opfibrations.
6.1.1. The total opposite of a displayed category [0018]
Let $E$ be displayed over $B$; we define its total opposite $\TotOpCat{E}$ displayed over $\OpCat{B}$ as follows:

An object of $\TotOpCat{E}\Sub{x}$ is given by an object of $E\Sub{x}$.

Given $f : x \to y\in \OpCat{B}$, a displayed morphism $\bar{x}\to\Sub{f} \bar{y}$ in $\TotOpCat{E}$ is given by a displayed morphism $\bar{y}\to\Sub{f} \bar{x}$ in $E$.
Warning. Do not confuse this construction with Construction 2.6·a [001Z], which produces a displayed category over $B$ and not $\OpCat{B}$.
Let $E$ be displayed over $B$. Prove that the total category (Section 3.1 [000A]) $\TotCat{\TotOpCat{E}}$ is $\OpCat{\prn{\TotCat{E}}}$, and its projection functor is $\OpCat{\prn{p\Sub{E}}} : \OpCat{\TotCat{E}}\to\OpCat{B}$.
Let $E$ be displayed over $B$, and let $f:x\to y\in B$. Prove that a morphism $\bar{f}:\bar{x}\to\Sub{f}\bar{y}$ is cartesian over $f$ in $E$ if and only if $\bar{f}:\bar{y}\to\Sub{f}\bar{x}$ is cocartesian over $f$ in $\TotOpCat{E}$.
Prove that a displayed category $E$ is a cartesian fibration over $B$ if and only if $\TotOpCat{E}$ is a cocartesian fibration over $\OpCat{B}$.
6.1.2. Example: Revisiting the fundamental selfindexing [002X]
Recall that the fundamental selfindexing $\SelfIx{B}$ (Construction 2.1·a [001X]) of a category $B$ is a displayed category with $\SelfIx{B}\Sub{x} = \Sl{B}{x}$. As discussed in Exercise 2.1·b [001Y], $\SelfIx{B}$ is a cartesian fibration over $B$ if and only if $B$ has pullbacks. However, $\SelfIx{B}$ is unconditionally a cocartesian fibration.
Prove that $\SelfIx{B}$ from [001X] is a cocartesian fibration for any category $B$.
6.1.3. Example: The dual selfindexing [0019]
Dually to the fundamental selfindexing (Construction 2.1·a [001X]), every category $B$ can also be displayed over itself via its coslices $\CoSl{x}{B}$.
Let $B$ be a category. Define the displayed category $\overline{B}$ over $B$ as follows:
 For $x\in B$, define $\overline{B}\Sub{x}$ as the collection of pairs $(\bar{x}\in B,p\Sub{x}:x\to\bar{x})$.
 For $f : x\to y\in B$, define $\overline{B}\Sub{f}$ to be the collection of commuting squares in the following configuration:
Prove that $\overline{B}$ is a cocartesian fibration if and only if $B$ has pushouts.
Prove that the total category (Section 3.1 [000A]) of $\overline{B}$ is the arrow category $B^{\to}$, and the projection is the domain functor.
Prove that $\overline{B}$ is a cartesian fibration for any category $B$.
6.2. Right fibrations [0013]
A cartesian fibration $E$ over $B$ is said to be a right fibration when all displayed morphisms in $E$ are cartesian.
Recall from Section 2.5 [0005] that for every $b\in B$, the collection of displayed objects $E\Sub{b}$ and vertical maps $E\Sub{1\Sub{b}}$ forms a category. When $E$ is a right fibration over $B$, this category is in fact a groupoid.
A cartesian fibration $E$ over $B$ is a right fibration if and only if all its vertical maps are isomorphisms.
Proof. Suppose that $E$ is a right fibration over $B$, and fix $b\in B$, $\bar{b}\in E\Sub{b}$, and a vertical map $f:\bar{b}\to\Sub{1\Sub{b}} \bar{b}$. Using the hypothesis that $f$ is cartesian, it has a unique section $g:\bar{b}\to\Sub{1\Sub{b}} \bar{b}$ as follows: Likewise, because $g$ is cartesian, $f$ is the unique section of $g$; thus $f$ is an isomorphism in $E\Sub{b}$.
Conversely, suppose that $E$ is a cartesian fibration whose vertical maps are isomorphisms. Fix $f:x\to y \in B$ and an arbitrary displayed morphism $\bar{g}:\bar{x}\to\Sub{f}\bar{y}$. Then $\bar{g}$ is the precomposition of a cartesian lift $\bar{f}:\bar{x}\tick\to\Sub{f}\bar{y}$ with a vertical map: Because vertical maps are isomorphisms and $\bar{f}$ is cartesian, we can observe that $\bar{g}$ is cartesian as follows, writing $\bar{m} : \bar{u}\to\Sub{m} \bar{x}\tick$ for the unique factorization of $\bar{h}$ through $\bar{f}$ over $m$: ∎
Bibliography

Ahrens, B., & Lumsdaine, P. L. F. (2019). Displayed Categories. Logical Methods in Computer Science, 15(1). https://doi.org/10.23638/LMCS15(1:20)2019 arXiv:1705.04296.Details

Grothendieck, A. (1971). Revêtements étales et groupe fondamental (SGA 1) (Vol. 224). SpringerVerlag.Details

Streicher, T. (2018). Fibred Categories à la Jean Bénabou. arXiv:1801.02927.Details

Lawvere, F. W., & Schanuel, S. H. (2009). Conceptual Mathematics: A First Introduction to Categories (2nd ed.). Cambridge University Press.Details

Street, R. (1980). Fibrations in bicategories. Cahiers De Topologie Et Géométrie Différentielle Catégoriques, 21(2), 111–160. http://eudml.org/doc/91227Details

Jacobs, B. (1999). Categorical Logic and Type Theory (Number 141). North Holland.Details

Bénabou, J. (1985). Fibered categories and the foundations of naive category theory. Journal of Symbolic Logic, 50(1), 10–37. https://doi.org/10.2307/2273784Details

Borceux, F. (1994). Handbook of Categorical Algebra 2 – Categories and Structures. Cambridge University Press.Details