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:

Benedick Ahrens;
Peter LeFanu Lumsdaine.
**Displayed Categories**.
In: *Logical Methods in Computer Science*.
Mar 5, 2019.
10.23638/LMCS-15%281%3A20%292019.
[ahrens-lumsdaine-2019]

**Displayed Categories**. In:

*Logical Methods in Computer Science*. Mar 5, 2019. 10.23638/LMCS-15%281%3A20%292019. [ahrens-lumsdaine-2019]

*displayed categories*. A displayed category over a category C is equivalent to “a category D and functor F : D \to C , but instead of having a single collection of “objects of D ” with a map to the objects of C , the objects are given as a family indexed by objects of C , and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Grothendieck fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as certain displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer formalisation, unifying and abstracting common constructions and proof techniques of category theory, and enabling modular reasoning about categories of multi-component structures. As such, most of the material of this article has been formalised in Coq over the UniMath library, with the aim of providing a practical library for use in further developments.

Jean Bénabou.
**Fibered categories and the foundations of naïve category theory**.
[benabou-1985]

**Fibered categories and the foundations of naïve category theory**. [benabou-1985]

Francis Borceux.
**Handbook of Categorical Algebra 2: Categories and Structures**.
[borceux-hca-2]

**Handbook of Categorical Algebra 2: Categories and Structures**. [borceux-hca-2]

Bart Jacobs.
**Categorical logic and type theory**.
*Studies in Logic and the Foundations of Mathematics*.
Jan 14, 1999.
[jacobs-1999]

**Categorical logic and type theory**.

*Studies in Logic and the Foundations of Mathematics*. Jan 14, 1999. [jacobs-1999]

Thomas Streicher.
**Fibred Categories à la Jean Bénabou**.
Dec 16, 2022.
10.48550/arXiv.1801.02927.
[streicher-fcjb]

**Fibred Categories à la Jean Bénabou**. Dec 16, 2022. 10.48550/arXiv.1801.02927. [streicher-fcjb]

These lecture notes are deeply influenced by Thomas Streicher.

# Foundational Assumptions
[frct-000R]

# Foundational Assumptions [frct-000R]

Definition
(meta-category)
[frct-001F]

A *meta-category* \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}

Remark
(collections)
[frct-003J]

In the definition of meta-category, we have not imposed any restrictions on what kinds of things the objects and morphisms are; our definition is pre-mathematical, so we do not assume beforehand that there is a such thing as a collection of “all” meta-categories.

We may define analogous notions of meta-functor, etc. But we do not assume that the notion of “all meta-functors \mathfrak{C}\to\mathfrak{D} ” is well-defined; the notion is entirely schematic.

**Assumption.** We assume a meta-category \BoldSymbol{\mathfrak{Coll}}
whose objects we will refer to as “collections”. We assume that the meta-category of all collections satisfies the axioms of Lawvere’s ETCS.

Definition
(category)
[frct-001G]

*category*E is defined to be a meta-category 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.

Remark
(cartesian closure of the meta-category of all categories)
[frct-003K]

Consequently there exists a meta-category \BoldSymbol{\mathfrak{Cat}}
of all
categories. Following Lawvere (but deviating from some other authors that
ground the notion of meta-categories 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.

# Displayed Categories and Fibrations
[frct-0008]

# Displayed Categories and Fibrations [frct-0008]

Definition
(displayed category)
[frct-0000]

Let B
be a category. A *displayed category* E
over B
is defined by the following data according to (Ahrens and Lumsdaine):

for each object x\in B , a collection of

*displayed objects*E\Sub{x} ,for each morphism \Mor{f}{x}{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*\Hom{E\Sub{f}}{\bar{x}}{\bar{y}} , an element of which shall denote by \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}} ,for each x\in B and \bar{x}\in E\Sub{x} , a displayed morphism \DispMor{\Idn{\bar{x}}}{\Idn{x}}{\bar{x}}{\bar{x}} ,

for each \Mor{f}{x}{y} and \Mor{g}{y}{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

\Hom{E\Sub{f}}{\bar{x}}{\bar{y}} \times \Hom{E\Sub{g}}{\bar{y}}{\bar{z}} \to \Hom{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 well-defined because of the corresponding laws for the base category B .

Notation
(square brackets for subscripts)
[frct-003R]

Definition
(cartesian morphisms)
[frct-0001]

Let E
be displayed over B
, and let \Mor{f}{x}{y} \in B
; a morphism \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}}
in E
is called *cartesian* over f
when for any \Mor{m}{u}{x}
and \DispMor{\bar{h}}{m;f}{\bar{u}}{\bar{y}}
there exists a unique \DispMor{\bar{m}}{m}{\bar{u}}{\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 self-indexing (the fundamental self-indexing) of a category.

Definition
(cartesian fibration)
[frct-0002]

A displayed category E
over B
is said to be a *cartesian fibration*, when
for each morphism \Mor{f}{x}{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
\DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}}
in the sense of cartesian morphisms. 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.

# The Fundamental Self-Indexing
[frct-0003]

# The Fundamental Self-Indexing [frct-0003]

Construction
(the fundamental self-indexing)
[frct-001X]

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,\Mor{p\Sub{x}}{\bar{x}}{x}) .
- For \Mor{f}{x}{y}\in B , we define \SelfIx{B}\Sub{f} to be the collection of commuting squares in the following configuration:

Exercise
[frct-001Y]

# The Generalized Pullback Lemma
[frct-0014]

# The Generalized Pullback Lemma [frct-0014]

In light of the fundamental self-indexing, the following result for displayed categories generalizes the ordinary “pullback lemma.”

Lemma
(generalized pullback lemma)
[frct-001H]

Let \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}} , and suppose that \DispMor{\bar{g}}{g}{\bar{y}}{\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 \DispMor{i}{m;f}{\bar{u}}{\bar{y}} . Then, because \bar{f} is cartesian, we can further factor i = j;\bar{f} for a unique \DispMor{j}{m}{\bar{u}}{\bar{x}} . We conclude that there is a unique \DispMor{j}{m}{\bar{u}}{\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 \DispMor{i}{m}{\bar{u}}{\bar{x}} . On the other hand, because \bar{g} is cartesian, there is a unique \DispMor{j}{m;f}{\bar{u}}{\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 \DispMor{i}{m}{\bar{u}}{\bar{x}} for which \bar{h} = i;\bar{f} , as required.

# An Alternative Definition of Fibration
[frct-0029]

# An Alternative Definition of Fibration [frct-0029]

**Warning.** Some authors including Grothendieck 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* (see Streicher).

Definition
(hypocartesian morphisms)
[frct-002A]

Let E
be displayed over B
, and let f:x\to y \in B
; a morphism \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}}
in E
is called *hypocartesian* over f
when for any \bar{u}\in E\Sub{x}
and \DispMor{\bar{h}}{f}{\bar{u}}{\bar{y}}
there exists a
unique \DispMor{i}{\Idn{x}}{\bar{u}}{\bar{x}}
with i;\bar{f} = \bar{h}
as follows:

Remark
[frct-003G]

Lemma
(hypocartesian = cartesian in a cartesian fibration)
[frct-002C]

Let E be a cartesian fibration in the sense of cartesian fibration, and let \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}} be displayed over \Mor{f}{x}{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 \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}} in a cartesian fibration is cartesian, we consider the cartesian lift of \Mor{f}{x}{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 \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}} through \DispMor{\bar{f}\tick}{f}{\bar{x}\tick}{\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 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 equivalence with Grothendieck's fibrations below, we verify that these two definitions of cartesian fibration coincide.

Lemma
(equivalence with Grothendieck's fibrations)
[frct-002B]

Let E be displayed over B . Then E is a cartesian fibration 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}\DispTo{f}\bar{y} .*Closure under composition.*If \bar{f}:\bar{x}\DispTo{f}\bar{y} and \bar{g}:\bar{y}\DispTo{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} ; because hypocartesian and cartesian maps coincide in a cartesian fibration we know that \bar{f},\bar{g} are also cartesian and hence by the generalized pullback lemma 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}\DispTo{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\DispTo{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\DispTo{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}\DispTo{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}\DispTo{m}\bar{x} factor uniquely through \bar{m} over \Idn{u} as a consequence of \bar{m} being hypocartesian.

Remark
(two ways to generalize pullbacks)
[frct-002D]

# Displayed and Fibered Functors
[frct-0004]

# Displayed and Fibered Functors [frct-0004]

Let E
be displayed over B
and let F
be displayed over C
. If \Mor{U}{B}{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 \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}} , a displayed morphism \DispMor{\bar{U}\bar{f}}{Uf}{\bar{U}\bar{x}}{\bar{U}\bar{y}} ,

such that the assignment \bar{U}f preserves displayed identities and displayed composition.

From this notion, we can see that 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*.

# Fiber Categories and Vertical Maps
[frct-0005]

# Fiber Categories and Vertical Maps [frct-0005]

*vertical map*in E is defined to be one that lies over the identity map in B . For every