open import Cat.Prelude

module Cat.Instances.Elements where

module _ {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 is a means of unpacking the data of the presheaf. Its objects are pairs of an object and a section

  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 If then the category of elements of will have three objects in place of the one: and Weβve erased all the boundaries of each of the sets associated with and are left with a big soup of points.

We do something similar for morphisms, and turn functions into a huge collection of morphisms between points. We do this by defining a morphism to be a morphism in as well as a proof that 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 on each point of we have a bunch of tiny bits of data that only describe the action of 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

unquoteDecl H-Level-Element-hom = declare-record-hlevel 2 H-Level-Element-hom (quote Element-hom)

module _ {o β s} {C : Precategory o β} {P : Functor (C ^op) (Sets s)} where instance
open Element

Extensional-element-hom
: β {x y : Element C P} {βr}
β β¦ ext : Extensional (C .Precategory.Hom (x .ob) (y .ob)) βr β¦
β Extensional (Element-hom C P x y) βr
Extensional-element-hom β¦ ext β¦ = injectionβextensional
(C .Precategory.Hom-set _ _) (Element-hom-path C P) ext

module _ {o β s} (C : Precategory o β) (P : Functor (C ^op) (Sets s)) where
private module P = Functor P
open Precategory C
open Functor
open Element-hom
open Element


One interesting fact is that morphisms in induce morphisms in the category of elements for each

  induce : β {x y} (f : Hom x y) (py : P Κ» y)
β Element-hom C P (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

  β« : Precategory (o β s) (β β s)
β« .Precategory.Ob = Element C P
β« .Precategory.Hom = Element-hom C P
β« .Precategory.Hom-set _ _ = hlevel 2
β« .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 = ext (idr _)
β« .Precategory.idl f = ext (idl _)
β« .Precategory.assoc f g h = ext (assoc _ _ _)


## Projectionπ

The category of elements is equipped with a canonical projection functor 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 For instance, if we look at the fibre over each we get back the set

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