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

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}$, and $\pi$ is the corresponding projection functor.

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

This last observation, coupled with the equation $\operatorname{id}_{}\circ\operatorname{id}_{}=\operatorname{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)
β (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 .Precategory.id = 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 $\operatorname{id}_{} \circ \operatorname{id}_{}$ to lying over $\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 $\operatorname{id}_{} \circ \operatorname{id}_{}$ is equal to $\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 $\mathcal{E}$ is displayed over $\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β² X fix coh .Precategory.idr f =
fix (f ββ² idβ²)           β‘β¨ coh (f ββ² idβ²) β©β‘
hom[ idl id ] (f ββ² idβ²) β‘β¨ Ds.disp! E β©β‘
f                        β
Fibreβ² X fix coh .Precategory.idl f =
fix (idβ² ββ² f)           β‘β¨ coh (idβ² ββ² f) β©β‘
hom[ idl id ] (idβ² ββ² f) β‘β¨ from-pathp (idlβ² f) β©β‘
f                        β
Fibreβ² X fix coh .Precategory.assoc f g h =
fix (f ββ² fix (g ββ² h))                     β‘β¨ ap (Ξ» e β fix (f ββ² e)) (coh _) β coh _ β©β‘
hom[ idl id ] (f ββ² hom[ idl id ] (g ββ² h)) β‘β¨ Ds.disp! E β©β‘
hom[ idl id ] (hom[ idl id ] (f ββ² g) ββ² h) β‘β¨ sym (coh _) β ap (Ξ» e β fix (e ββ² h)) (sym (coh _)) β©β‘
fix (fix (f ββ² g) ββ² h)                     β

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β©οΈ