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

import Cat.Displayed.Reasoning as Dr
import Cat.Displayed.Solver as Ds

module Cat.Displayed.Fibre
  {o ℓ o' ℓ'} {B : Precategory o ℓ} (E : Displayed B o' ℓ') where

open Precategory B
open Dr E
open Ds

Fibre categories🔗

A displayed category can be thought of as representing data of a “family of categories”¹. Given an object $x:\mathcal{B}$ of the base category, the morphisms in the fibre over x, or vertical morphisms, are those in the set ${\mathbf{Hom}}_{{\mathrm{id}}_x}(x^{\prime },y^{\prime })$ of morphisms over the identity map (on $x\text{).}$

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

In this diagram, the map $g\text{,}$ which is displayed over the identity on $a\text{,}$ is literally… vertical! A map such as $h\text{,}$ between objects in two different fibres (hence displayed over a non-identity map $f\text{),}$ is not drawn vertically. Additionally, the unwritten (displayed) identity morphisms on $a\text{,}$ $b\text{,}$ $c\text{,}$ and $d$ are all vertical.

This last observation, coupled with the equation $\mathrm{id}\circ \mathrm{id}=\mathrm{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) → Precategory _ _
Fibre X .Precategory.Ob = Ob[ X ]
Fibre X .Precategory.Hom = Hom[ id ]
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') ≡⟨ Ds.disp! E ⟩≡
  f                        ∎
Fibre X .Precategory.idl f =
  hom[ idl id ] (id' ∘' f) ≡⟨ from-pathp[] (idl' f) ⟩≡
  f                        ∎
Fibre X .Precategory.assoc f g h =
  hom[ idl id ] (f ∘' hom[ idl id ] (g ∘' h)) ≡⟨ Ds.disp! E ⟩≡
  hom[ idl id ] (hom[ idl id ] (f ∘' g) ∘' h) ∎