module Cat.Instances.Elements.Covariant where

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
  ∫ : Precategory (o βŠ” s) (β„“ βŠ” s)
  ∫ .Precategory.Ob = Element P
  ∫ .Precategory.Hom = Element-hom P
  ∫ .Precategory.Hom-set = Element-hom-is-set P
  ∫ .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