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 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 .

  : (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 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 : 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β†©οΈŽ