open import Cat.Displayed.Base
open import Cat.Prelude

import Cat.Displayed.Reasoning as DR
import Cat.Reasoning as CR

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

open Displayed E
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:Bx : \ca{B} of the base category, the morphisms in the fibre over x, or vertical morphisms, are those in the set Homidx(x,y)\hom_{\id{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\ca{B} as being a like a grab-bag of categories, admitting a map into B\ca{B} (the total space perspective), a situation examplified by the diagram below. Here, ∫E\int E is the total space of a category EE displayed over B\ca{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\id{id}\circ\id{id}=\id{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.

Fibre : Ob β†’ Precategory _ _
Fibre x .Precategory.Ob = Ob[ x ]
Fibre x .Precategory.Hom a b = Hom[ id ] a b
Fibre x .Precategory.Hom-set = Hom[ id ]-set
Fibre x .Precategory.id = idβ€²
Fibre x .Precategory._∘_ f g = hom[ idl id ] (f βˆ˜β€² g)
Fibre x .Precategory.idr f =
  hom[ idl id ] (f βˆ˜β€² idβ€²) β‰‘βŸ¨ reindex _ _ βŸ©β‰‘
  hom[ idr id ] (f βˆ˜β€² idβ€²) β‰‘βŸ¨ from-pathp (idrβ€² f) βŸ©β‰‘
  f                        ∎
Fibre x .Precategory.idl f = from-pathp (idlβ€² f)
Fibre x .Precategory.assoc f g h =
  hom[ idl id ] (f βˆ˜β€² hom[ idl id ] (g βˆ˜β€² h))                     β‰‘βŸ¨ ap hom[] (whisker-r (idl id)) βˆ™ hom[]-βˆ™ _ _ βŸ©β‰‘
  hom[ ap (id ∘_) (idl id) βˆ™ idl id ] (f βˆ˜β€² g βˆ˜β€² h)               β‰‘βŸ¨ reindex _ _ βŸ©β‰‘
  hom[ assoc _ _ _ βˆ™ ap (_∘ id) (idl id) βˆ™ idl id ] (f βˆ˜β€² g βˆ˜β€² h) β‰‘Λ˜βŸ¨ hom[]-βˆ™ _ _ βŸ©β‰‘Λ˜
  hom[ ap (_∘ id) (idl id) βˆ™ idl id ] (hom[] (f βˆ˜β€² g βˆ˜β€² h))       β‰‘βŸ¨ ap hom[] (from-pathp (assocβ€² _ _ _)) βŸ©β‰‘
  hom[ ap (_∘ id) (idl id) βˆ™ idl id ] ((f βˆ˜β€² g) βˆ˜β€² h)             β‰‘Λ˜βŸ¨ ap hom[] (whisker-l (idl id)) βˆ™ hom[]-βˆ™ _ _ βŸ©β‰‘Λ˜
  hom[ idl id ] (hom[ idl id ] (f βˆ˜β€² g) βˆ˜β€² h)                     ∎

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