module Cat.Instances.Elements where

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


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β†©οΈŽ