module Cat.Displayed.Fibre
  {o β„“ oβ€² β„“β€²} {B : Precategory o β„“}
  (E : Displayed B oβ€² β„“β€²)

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:Bx : \mathcal{B} of the base category, the morphisms in the fibre over x, or vertical morphisms, are those in the set Homid⁑x(x,y)\mathbf{Hom}_{\operatorname{id}_{x}}(x, y) of morphisms over the identity map (on xx).

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

In this diagram, the map gg, which is displayed over the identity on aa, is literally… vertical! A map such as hh, between objects in two different fibres (hence displayed over a non-identity map ff), is not drawn vertically. Additionally, the unwritten (displayed) identity morphisms on aa, bb, cc, and dd are all vertical.

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

  : (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 = 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⁑\operatorname{id}_{} \circ \operatorname{id}_{} to lying over id⁑\operatorname{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⁑\operatorname{id}_{} \circ \operatorname{id}_{} is equal to id⁑\operatorname{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\mathcal{E} is displayed over Sets\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)

  1. Though note that unless the displayed category is a Cartesian fibration, this β€œfamily” might not be functorially-indexedβ†©οΈŽ