Foundations of Relative Category Theory

Let $B$ be an ordinary category; there is an important displayed category $\SelfIx{B}$ over $B$ given fiberwise by the slices of $B$.

1. 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)$.
2. 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.

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. ∎

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:

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. ∎

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:

1. 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}$.
2. 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 self-indexing (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].

Let $E$ be fibered over $B$; we may define the opposite fibered category $\OpCat{E}$ over $B$ like so:

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

2. 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:

There is a simple characterization of cartesian maps in $\OpCat{E}$.

The foregoing characterization of cartesian maps in $\OpCat{E}$ immediately implies that $\OpCat{E}$ is fibered over $B$.

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 right-hand map is cartesian over $\Idn{x} : x\to x$ and the left-hand 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$. ∎

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.

1. 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}$.

2. 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:

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

2. A displayed morphism $\bar{z}\to \bar{x}$ is called a $\bar{s}$-figure whenever $\bar{z}\in\FullSubfib{\bar{s}}$.

Prove that the total category $\TotCat{\SelfIx{B}}$ of the fundamental self-indexing (Section 2.1 [0003]) is the arrow category $B^{\to}$, and the projection is the codomain functor.

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$.

Explicitly construct the functorial action of $\TotCat{P\Sub{\bullet}}\to E$.

Verify that $\TotCat{P\Sub{\bullet}}\to E$ is a categorical equivalence.

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.

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}$.

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$. ∎

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$.

An ordinary category is called globally small when it has a set of objects.

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.

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].

Given an ordinary category $E$, a set-indexed 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$.

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 well-pointedness.

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].

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.

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.

We will now construe Section 4.4.1 [002Q] as the instantiation at the fundamental self-indexing $\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 category with finite limits; then an internal category in $E$ is defined by the following data:

1. an object of objects $C\Sub{0}\in E$,
2. an object of morphisms $C\Sub{1}\in E$,
3. source and target morphisms $s,t:C\Sub{1}\to C\Sub{0}$,
4. a generic identity morphism $C\Sub{0}\to C\Sub{1}$,
5. a generic composition morphism $C\Sub{1}\times\Sub{C\Sub{0}}C\Sub{1}\to C\Sub{1}$,
6. satisfying a number of laws corresponding to those of a category.

For the details of these laws, we refer to the nLab (internal category).

Let $C$ be an internal category in $E$. We may define a fibered category $\brk{C}$ over $E$ called the externalization of $C$.

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

2. 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. ∎

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$.

1. 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].)

2. 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: ∎

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}$:

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}$.

Warning. Do not confuse this construction with Construction 2.6·a [001Z], which produces a displayed category over $B$ and not $\OpCat{B}$.

Recall that the fundamental self-indexing $\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.

Dually to the fundamental self-indexing (Construction 2.1·a [001X]), every category $B$ can also be displayed over itself via its coslices $\CoSl{x}{B}$.

A cartesian fibration $E$ over $B$ is said to be a right fibration when all displayed morphisms in $E$ are cartesian.

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$: ∎