open import Cat.Prelude

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

The Category of ElementsπŸ”—

The category of elements of a presheaf P:Cop→SetsP : C\op \to \sets is a means of unpacking the data of the presheaf. Its objects are pairs of an object xx, and a section s:Pxs : P x.

record Element : Type (o βŠ” s) where
  constructor elem
  field
    ob : Ob
    section : ∣ P.β‚€ ob ∣

open Element

We can think of this as taking an eraser to the data of PP. If P(x)={x0,x1,x2}P(x) = \{x_0, x_1, x_2\}, then the category of elements of PP will have three objects in place of the one: (x,x0)(x, x_0), (x,x1)(x, x_1), and (x,x2)(x, x_2). We’ve erased all the boundaries of each of the sets associated with PP, and are left with a big soup of points.

We do something similar for morphisms, and turn functions P(f):P(Y)→P(X)P(f) : P(Y) \to P(X) into a huge collection of morphisms between points. We do this by defining a morphism (x,x0)→(y,y0)(x, x_0) \to (y, y_0) to be a morphism f:X→Yf : X \to Y in C\ca{C}, as well as a proof that P(f)(y0)=x0P(f)(y_0) = x_0 This too can be seen as erasing boundaries, just this time with the data associated with a function. Instead of having a bunch of data bundled together that describes the action of P(f)P(f) on each point of P(Y)P(Y), we have a bunch of tiny bits of data that only describe the action of P(f)P(f) on a single point.

record Element-hom (x y : Element) : Type (β„“ βŠ” s) where
  constructor elem-hom
  no-eta-equality
  field
    hom : Hom (x .ob) (y .ob)
    commute : P.₁ hom (y .section) ≑ x .section

open Element-hom

As per usual, we need to prove some helper lemmas that describe the path space of Element-hom

Element-hom-path : {x y : Element} {f g : Element-hom x y} β†’ f .hom ≑ g .hom β†’ f ≑ g
Element-hom-path p i .hom = p i
Element-hom-path {x = x} {y = y} {f = f} {g = g} p i .commute =
  is-propβ†’pathp (Ξ» j β†’ P.β‚€ (x .ob) .is-tr (P.₁ (p j) (y .section)) (x .section))
    (f .commute)
    (g .commute) i

One interesting fact is that morphisms f:X→Yf : X \to Y in CC induce morphisms in the category of elements for each py:P(y)py : P(y).

induce : βˆ€ {x y} (f : Hom x y) (py : ∣ P.β‚€ y ∣)
       β†’ Element-hom (elem x (P.₁ f py)) (elem y py)
induce f _ = elem-hom f refl

Using all this machinery, we can now define the category of elements of PP!

∫ : Precategory (o βŠ” s) (β„“ βŠ” s)
∫ .Precategory.Ob = Element
∫ .Precategory.Hom = Element-hom
∫ .Precategory.Hom-set = Element-hom-is-set
∫ .Precategory.id {x = x} = elem-hom id  Ξ» i β†’ P.F-id i (x .section)
∫ .Precategory._∘_ {x = x} {y = y} {z = z} f g = elem-hom (f .hom ∘ g .hom) comm
  where
    abstract
      comm : P.₁ (f .hom ∘ g .hom) (z .section) ≑ x .section
      comm =
        P.₁ (f .hom ∘ g .hom) (z .section)       β‰‘βŸ¨ happly (P.F-∘ (g .hom) (f .hom)) (z .section) βŸ©β‰‘
        P.₁ (g .hom) (P.₁ (f .hom) (z .section)) β‰‘βŸ¨ ap (P.F₁ (g .hom)) (f .commute)  βŸ©β‰‘
        P.₁ (g .hom) (y .section)                β‰‘βŸ¨ g .commute βŸ©β‰‘
        x .section ∎
∫ .Precategory.idr f = Element-hom-path (idr (f .hom))
∫ .Precategory.idl f = Element-hom-path (idl (f .hom))
∫ .Precategory.assoc f g h = Element-hom-path (assoc (f .hom) (g .hom) (h .hom))

ProjectionπŸ”—

The category of elements is equipped with a canonical projection functor Ο€p:∫Pβ†’C\pi_p : \int P \to C, which just forgets all of the points and morphism actions.

Ο€β‚š : Functor ∫ C
Ο€β‚š .Fβ‚€ x = x .ob
Ο€β‚š .F₁ f = f .hom
Ο€β‚š .F-id = refl
Ο€β‚š .F-∘ f g = refl

This functor makes it clear that we ought to think of the category of elements as something defined over C\ca{C}. For instance, if we look at the fibre over each X:CX : \ca{C}, we get back the set P(X)P(X)!