module Cat.Displayed.Fibre {o β o' β'} {B : Precategory o β} (E : Displayed B o' β') where open Precategory B open Displayed E open Ds open Dr E

## Fibre categoriesπ

A displayed
category can be thought of as representing data of a βfamily of
categoriesβ^{1}. Given an object
$x:B$
of the base category, the morphisms in the fibre over x, or
**vertical morphisms**, are those in the set
$Hom_{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
$B$
as being a like a grab-bag of categories, admitting a map into
$B$
(the total
category perspective), a situation examplified by the diagram below.
Here,
$β«E$
is the total space of a category
$E$
displayed over
$B,$
and
$Ο$
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
$idβid=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
$idβid$
to lying over
$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
$idβid$
is equal to
$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 $E$ is displayed over $Sets,$ then composition of morphisms is definitionally unital, so transporting is redundant; but without regularity, the transports along reflexivity would still pile up.

Fibre' X fix coh .Precategory.idr f = fix (f β' id') β‘β¨ coh (f β' id') β©β‘ hom[ idl id ] (f β' id') β‘β¨ Ds.disp! E β©β‘ f β Fibre' X fix coh .Precategory.idl f = fix (id' β' f) β‘β¨ coh (id' β' f) β©β‘ hom[ idl id ] (id' β' f) β‘β¨ from-pathp (idl' f) β©β‘ f β Fibre' X fix coh .Precategory.assoc f g h = fix (f β' fix (g β' h)) β‘β¨ ap (Ξ» e β fix (f β' e)) (coh _) β coh _ β©β‘ hom[ idl id ] (f β' hom[ idl id ] (g β' h)) β‘β¨ Ds.disp! E β©β‘ hom[ idl id ] (hom[ idl id ] (f β' g) β' h) β‘β¨ sym (coh _) β ap (Ξ» e β fix (e β' h)) (sym (coh _)) β©β‘ fix (fix (f β' g) β' h) β

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β©οΈ