mathlib documentation

category_theory.limits.yoneda

The colimit of coyoneda.obj X is punit

We calculate the colimit of Y ↦ (X ⟶ Y), which is just punit.

(This is used later in characterising cofinal functors.)

The colimit cocone over coyoneda.obj X, with cocone point punit.

Equations
@[simp]
theorem category_theory.coyoneda.colimit_cocone_ι_app {C : Type v} [category_theory.small_category C] (X : Cᵒᵖ) (X_1 : C) :
(category_theory.coyoneda.colimit_cocone X).ι.app X_1 = id (λ (ᾰ : (category_theory.coyoneda.obj X).obj X_1), id (λ (X : Cᵒᵖ) (X_1 : C) (ᾰ : opposite.unop X X_1), punit.star) X X_1 ᾰ)