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

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

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

open Displayed E
open Ds
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 = idβ€²
Fibre x .Precategory._∘_ f g = hom[ idl id ] (f βˆ˜β€² g)
Fibre x .Precategory.idr f = Ds.disp! E
Fibre x .Precategory.idl f = from-pathp (idlβ€² f)
Fibre x .Precategory.assoc f g h = Ds.disp! E

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