module Cat.Displayed.Instances.Elements {o β s} (B : Precategory o β) (P : Functor (B ^op) (Sets s)) where

# The Displayed Category of Elementsπ

It is useful to view the category of elements of a
presheaf P as a displayed category. Instead of
considering pairs of objects
$X$
and sections
$s$,
we instead think of the set of sections as displayed *over*
$X$.
The story is similar for morphisms; instead of taking pairs of morphisms
$f$
and fragments of data that
$P(f)(x) = y$,
we place those fragments over the morphism
$f$.

In a sense, this is the more natural presentation of the category of elements, as we obtain the more traditional definition by taking the total category of β«.

β« : Displayed B s s Displayed.Ob[ β« ] X = β£ P.β X β£ Displayed.Hom[ β« ] f P[X] P[Y] = P.β f P[Y] β‘ P[X] Displayed.Hom[ β« ]-set _ _ _ = hlevel! β« .Displayed.idβ² = happly P.F-id _ β« .Displayed._ββ²_ {x = x} {y = y} {z = z} {f = f} {g = g} p q = pf where abstract pf : P.β (f β g) z β‘ x pf = P.β (f β g) z β‘β¨ happly (P.F-β g f) z β©β‘ P.β g (P.β f z) β‘β¨ ap (P.β g) p β©β‘ P.β g y β‘β¨ q β©β‘ x β β« .Displayed.idrβ² _ = to-pathp (P.β _ .is-tr _ _ _ _) β« .Displayed.idlβ² _ = to-pathp (P.β _ .is-tr _ _ _ _) β« .Displayed.assocβ² _ _ _ = to-pathp (P.β _ .is-tr _ _ _ _)