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

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 XX and sections ss, we instead think of the set of sections as displayed over XX. The story is similar for morphisms; instead of taking pairs of morphisms ff and fragments of data that P(f)(x)=yP(f)(x) = y, we place those fragments over the morphism ff.

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 _ _ _ _)