open import Cat.Prelude

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

open Precategory C
open Functor

private
module P = Functor P


# The category of elementsπ

The (contravariant1) category of elements of a presheaf $P : \mathcal{C}^{\mathrm{op}} \to \mathbf{Sets}$ is a means of unpacking the data of the presheaf. Its objects are pairs of an object $x$, and a section $s : 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 $P$. If $P(x) = \{x_0, x_1, x_2\}$, then the category of elements of $P$ will have three objects in place of the one: $(x, x_0)$, $(x, x_1)$, and $(x, x_2)$. Weβve erased all the boundaries of each of the sets associated with $P$, and are left with a big soup of points.

We do something similar for morphisms, and turn functions $P(f) : P(Y) \to P(X)$ into a huge collection of morphisms between points. We do this by defining a morphism $(x, x_0) \to (y, y_0)$ to be a morphism $f : X \to Y$ in $\mathcal{C}$, as well as a proof that $P(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)$ on each point of $P(Y)$, we have a bunch of tiny bits of data that only describe the action of $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

private unquoteDecl eqv = declare-record-iso eqv (quote Element-hom)
Element-hom-is-set : β (x y : Element) β is-set (Element-hom x y)
Element-hom-is-set x y = Isoβis-hlevel 2 eqv T-is-set where
T-is-set : is-set _
T-is-set = hlevel!


One interesting fact is that morphisms $f : X \to Y$ in $C$ induce morphisms in the category of elements for each $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 $P$!

β« : 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 $\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 $\mathcal{C}$. For instance, if we look at the fibre over each $X : \mathcal{C}$, we get back the set $P(X)$!

1. there is a separate covariant category of elements for covariant functorsβ©οΈ