open import Cat.Displayed.Base open import Cat.Prelude module Cat.Displayed.Cartesian {o β oβ² ββ²} {B : Precategory o β} (E : Displayed B oβ² ββ²) where open Precategory B open Displayed E

# Cartesian morphisms and Fibrationsπ

While displayed categories give the essential framework we need to
express the idea of families of categories indexed by a category, they
do not *quite* capture the concept precisely. The problem is that
while a category
$\ca{E}$
displayed over
$\ca{B}$
does indeed give a *collection* of fibre categories
$\ca{E}^*(x)$,
this assignment isnβt necessarily functorial!

More precisely, we should have that a collection of categories,
indexed by a category, should be a *pseudofunctor*
$\ca{B} \to \Cat$,
where
$\Cat$
is a bicategory of categories. It turns
out that we can characterise this assignment entirely in terms of the
displayed objects and morphisms in
$\ca{E}$!

Fix an arrow
$f : a \to b$
in the base category
$\ca{B}$,
an object
$a'$
over
$a$
(resp.
$b'$
over
$b$),
and an arrow
$f' : a' \to_f b'$
over
$f$.
We say that
$f'$
is **cartesian** if, up to very strong handwaving, it fits
into a βpullback diagramβ. The barred arrows with triangle tips here
indicate the βprojectionβ from a displayed object to its base, and so
are implicit in the type dependency.

record Cartesian {a b aβ² bβ²} (f : Hom a b) (fβ² : Hom[ f ] aβ² bβ²) : Type (o β β β oβ² β ββ²) where no-eta-equality

More specifically, let $u : \ca{B}$ and $u'$ be over $u$, and suppose that we have a map $m : u \to a$ (below, in violet), and a map $h' : u' \to_m b'$ lying over the composite $fm$ (in red). The universal property of a Cartesian map says that we have a universal factorisation of $h'$ through a map $u' \to a'$ (in green, marked $\exists!$).

field universal : β {u uβ²} (m : Hom u a) (hβ² : Hom[ f β m ] uβ² bβ²) β Hom[ m ] uβ² aβ² commutes : β {u uβ²} (m : Hom u a) (hβ² : Hom[ f β m ] uβ² bβ²) β fβ² ββ² universal m hβ² β‘ hβ² unique : β {u uβ²} {m : Hom u a} {hβ² : Hom[ f β m ] uβ² bβ²} β (mβ² : Hom[ m ] uβ² aβ²) β fβ² ββ² mβ² β‘ hβ² β mβ² β‘ universal m hβ²

Given a βright cornerβ like that of the diagram below, and note that the input data consists of $a$, $b$, $f : a \to b$ and $b'$ over $a$,

we call an object
$a'$
over
$a$
together with a Cartesian arrow
$f' : a' \to b'$
a *Cartesian lift* of
$f$.
Cartesian lifts, defined by universal property as they are, are unique
when they exist, so that βhaving Cartesian liftsβ is a
*property*, not a structure.

record Cartesian-lift {x y} (f : Hom x y) (yβ² : Ob[ y ]) : Type (o β β β oβ² β ββ²) where no-eta-equality field {xβ²} : Ob[ x ] lifting : Hom[ f ] xβ² yβ² cartesian : Cartesian f lifting open Cartesian cartesian public

We note that the classical literature often differentiates between
*fibrations* β those displayed categories for which *there
exist* Cartesian lifts for every right corner β and *cloven
fibrations*, those for which the Cartesian lifts are βalgebraicβ in
a sense. This is because, classically, *essentially unique* means
that there are still some choices to be made, and invoking the axiom of
choice makes an βarbitraryβ set of such choices. But, in the presence of
univalence, there is exactly *one* choice to be made, that is, no
choice at all. Thus, we do not dwell on the distinction.

record Cartesian-fibration : Type (o β β β oβ² β ββ²) where no-eta-equality field has-lift : β {x y} (f : Hom x y) (yβ² : Ob[ y ]) β Cartesian-lift f yβ²

A Cartesian fibration is a displayed category having Cartesian lifts for every right corner.

## Why?π

Admittedly, the notion of Cartesian morphism is slightly artificial. It arises from studying the specific properties of the pullback functors $f^* : \ca{C}/y \to \ca{C}/x$ which exist in a category of pullbacks, hence the similarity in universal property!

In fact, the quintessential example of a Cartesian fibration is the
*codomain
fibration*, which is a category displayed over
$\ca{C}$,
where the fibre over
$x$
is the slice category
$\ca{C}/x$.
We may investigate further (to uncover the name βcodomainβ): the total
space of this fibration is the arrow category
$\id{Arr}(\ca{C})$,
and the projection functor is the codomain functor
$\id{Arr}(\ca{C}) \to \ca{C}$.

This displayed category extends to a pseudofunctor exactly when
$\ca{C}$
has all pullbacks, because in a world where the vertical arrows are
β*just*β arrows, a Cartesian morphism is exactly a pullback
square.

Other examples exist:

- The family fibration exhibits any category $\ca{C}$ as displayed over $\sets$. The fibres are functor categories (with discrete domains), reindexing is given by composition.

- The category of modules is fibred over the category of rings. The fibre over a ring $R$ is the category of $R$-modules, Cartesian lifts are given by restriction of scalars.