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 $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

  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 $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) (record { Functor P }) ^op
co-∫ = Precategory-path F F-is-precat-iso where
  F : Functor ∫ (Contra.∫ (C ^op) (record { Functor 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.from 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.from 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