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 record where from e = elem (e .Contra.Element.ob) (e .Contra.Element.section) rinv e = refl linv e = refl F-is-precat-iso .is-precat-iso.has-is-ff = is-iso→is-equiv record where from h = elem-hom (h .Contra.Element-hom.hom) (h .Contra.Element-hom.commute) rinv h = ext refl linv h = ext refl