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} {z} {f} {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' _ = prop! β« .Displayed.idl' _ = prop! β« .Displayed.assoc' _ _ _ = prop!