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 of the base category, the morphisms in the fibre over x, or vertical morphisms, are those in the set of morphisms over the identity map (on ).
The intuition from the term vertical comes from literally thinking of a category displayed over as being a like a grab-bag of categories, admitting a map into (the total category perspective), a situation examplified by the diagram below. Here, is the total space of a category displayed over , and is the corresponding projection functor.
In this diagram, the map , which is displayed over the identity on , is literally⦠vertical! A map such as , between objects in two different fibres (hence displayed over a non-identity map ), is not drawn vertically. Additionally, the unwritten (displayed) identity morphisms on , , , and are all vertical.
This last observation, coupled with the equation from the base category, implies that the set of vertical arrows over an object contain identities and are closed under composition, the fibre (pre)category over .
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
to lying over
.
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
is equal to
),
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 is displayed over , 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β©οΈ