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

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

open Precategory B
open Functor

private
module P = Functor P


# 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 and sections we instead think of the set of sections as displayed over The story is similar for morphisms; instead of taking pairs of morphisms and fragments of data that we place those fragments over the morphism

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 2
β« .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!