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 $Sets),$ the construction makes sense for covariant functors as well.

Sadly, we cannot simply reuse the contravariant construction, instantiating $C$ as $C^{op} :$ the resulting category would be the opposite of what we want. Indeed, in both the covariant and contravariant cases, we want the projection $π : \int F \to C$ 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 _ _ = 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 $P$ is the opposite of the contravariant category of elements of $P$ seen as a contravariant functor on $C^{op}$ (thus a functor $(C^{op})^{op} = C \to Sets).$

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