open import Cat.Functor.Equivalence.Path
open import Cat.Functor.Equivalence
open import Cat.Prelude

import Cat.Instances.Elements as Contra

module Cat.Instances.Elements.Covariant where

module _ {o β s} {C : Precategory o β} (P : Functor C (Sets s)) where
private module P = Functor P

open Precategory C
open Functor


The covariant category of elementsπ

While the category of elements comes up most often in the context of presheaves (i.e., contravariant functors into the construction makes sense for covariant functors as well.

Sadly, we cannot simply reuse the contravariant construction, instantiating as the resulting category would be the opposite of what we want. Indeed, in both the covariant and contravariant cases, we want the projection to be covariant.

Thus we proceed to dualise the whole construction.

  record Element : Type (o β s) where
constructor elem
field
ob : Ob
section : P Κ» ob

open Element

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 (x .section) β‘ y .section

open 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.β (y .ob) .is-tr (P.β (p j) (x .section)) (y .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 (Sets s)} where instance
Extensional-element-hom
: β {x y : Element P} {βr}
β β¦ ext : Extensional (C .Precategory.Hom (x .Element.ob) (y .Element.ob)) βr β¦
β Extensional (Element-hom P x y) βr
Extensional-element-hom β¦ ext β¦ = injectionβextensional
(C .Precategory.Hom-set _ _) (Element-hom-path P) ext

module _ {o β s} {C : Precategory o β} (P : Functor C (Sets s)) where
private module P = Functor P

open Precategory C
open Element-hom
open Element
open Functor

  β« : Precategory (o β s) (β β s)
β« .Precategory.Ob = Element P
β« .Precategory.Hom = Element-hom 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) (x .section) β‘ z .section
comm =
P.β (f .hom β g .hom) (x .section)       β‘β¨ happly (P.F-β (f .hom) (g .hom)) (x .section) β©β‘
P.β (f .hom) (P.β (g .hom) (x .section)) β‘β¨ ap (P.Fβ (f .hom)) (g .commute)  β©β‘
P.β (f .hom) (y .section)                β‘β¨ f .commute β©β‘
z .section β
β« .Precategory.idr f = ext (idr (f .hom))
β« .Precategory.idl f = ext (idl (f .hom))
β« .Precategory.assoc f g h = ext (assoc (f .hom) (g .hom) (h .hom))

Οβ : Functor β« C
Οβ .Fβ x = x .ob
Οβ .Fβ f = f .hom
Οβ .F-id = refl
Οβ .F-β f g = refl


We can now relate the two constructions: the covariant category of elements of is the opposite of the contravariant category of elements of seen as a contravariant functor on (thus a functor

  co-β« : β« β‘ Contra.β« (C ^op) P ^op
co-β« = Precategory-path F F-is-precat-iso where
F : Functor β« (Contra.β« (C ^op) P ^op)
F .Fβ e = Contra.elem (e .ob) (e .section)
F .Fβ h = Contra.elem-hom (h .hom) (h .commute)
F .F-id = refl
F .F-β _ _ = ext refl

F-is-precat-iso : is-precat-iso F
F-is-precat-iso .is-precat-iso.has-is-iso = is-isoβis-equiv Ξ» where
.is-iso.inv e β elem (e .Contra.Element.ob) (e .Contra.Element.section)
.is-iso.rinv e β refl
.is-iso.linv e β refl
F-is-precat-iso .is-precat-iso.has-is-ff = is-isoβis-equiv Ξ» where
.is-iso.inv h β elem-hom (h .Contra.Element-hom.hom) (h .Contra.Element-hom.commute)
.is-iso.rinv h β ext refl
.is-iso.linv h β ext refl