open import Cat.Displayed.Base open import Cat.Prelude import Cat.Displayed.Reasoning as Dr import Cat.Displayed.Solver as Ds import Cat.Reasoning as Cr module Cat.Displayed.Fibre {o β oβ² ββ²} {B : Precategory o β} (E : Displayed B oβ² ββ²) where open Displayed E open Ds open Dr E open Cr B

## Fibre categoriesπ

A displayed category can be thought of as representing data of a
βfamily of categoriesβ^{1}. Given an object
$x : \mathcal{B}$
of the base category, the morphisms in the fibre over x, or
**vertical morphisms**, are those in the set
$\mathbf{Hom}_{\mathrm{id}_{x}}(x, y)$
of morphisms over the identity map (on
$x$).

The intuition from the term *vertical* comes from
*literally* thinking of a category
$E$
displayed over
$\mathcal{B}$
as being a like a grab-bag of categories, admitting a map into
$\mathcal{B}$
(the total space perspective), a
situation examplified by the diagram below. Here,
$\int E$
is the total space of a category
$E$
displayed over
$\mathcal{B}$,
and
$\pi$
is the corresponding projection functor.

In this diagram, the map $g$, which is displayed over the identity on $a$, is literallyβ¦ vertical! A map such as $h$, between objects in two different fibres (hence displayed over a non-identity map $f$), is not drawn vertically. Additionally, the unwritten (displayed) identity morphisms on $a$, $b$, $c$, and $d$ are all vertical.

This last observation, coupled with the equation
$\mathrm{id}_{}\circ\mathrm{id}_{}=\mathrm{id}_{}$
from the base category, implies that the set of vertical arrows over an
object
$x$
contain identities and are closed under composition, the **fibre
(pre)category over
$x$**.

Fibreβ² : (X : Ob) β (fix : {x y : Ob[ X ]} β Hom[ id β id ] x y β Hom[ id ] x y) β (coh : β {x y} (f : Hom[ id β id ] x y) β fix f β‘ hom[ idl id ] f) β Precategory _ _ Fibreβ² X fix coh .Precategory.Ob = Ob[ X ] Fibreβ² X fix coh .Precategory.Hom = Hom[ id ] Fibreβ² X fix coh .Precategory.Hom-set = Hom[ id ]-set Fibreβ² X fix coh .Precategory.id = idβ² Fibreβ² X fix coh .Precategory._β_ f g = fix (f ββ² g)

The definition of Fibreβ²
has an extra degree of freedom: it is parametrised over how to reindex a
morphism from lying over
$\mathrm{id}_{} \circ \mathrm{id}_{}$
to lying over
$\mathrm{id}_{}$.
You donβt get *that* much freedom, however: there is a canonical
way of doing this reindexing, which is to transport the composite
morphism (since
$\mathrm{id}_{} \circ \mathrm{id}_{}$
is equal to
$\mathrm{id}_{}$),
and the provided method *must* be homotopic to this canonical one
β to guarantee that the resulting construction is a precategory.

It may seem that this extra freedom serves no purpose, then, but there are cases where itβs possible to transport without actually transporting: For example, if $\mathcal{E}$ is displayed over $\mathbf{Sets}$, then composition of morphisms is definitionally unital, so transporting is redundant; but without regularity, the transports along reflexivity would still pile up.

Fibre : Ob β Precategory _ _ Fibre X = Fibreβ² X _ (Ξ» f β refl)

Though note that unless the displayed category is a Cartesian fibration, this βfamilyβ might not be functorially-indexedβ©οΈ