Limit properties relating to the (co)yoneda embedding. #

We calculate the colimit of Y ↦ (X ⟶ Y), which is just PUnit. (This is used in characterising cofinal functors.)

We also show the (co)yoneda embeddings preserve limits and jointly reflect them.

theorem CategoryTheory.Coyoneda.colimitCocone_ι_app {C : Type v} [CategoryTheory.SmallCategory C] (X : Cᵒᵖ) (X_1 : C) (a : (CategoryTheory.coyoneda.obj X).obj X_1) :

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

Instances For

    The proposed colimit cocone over coyoneda.obj X is a colimit cocone.

    Instances For

      The colimit of coyoneda.obj X is isomorphic to PUnit.

      Instances For

        The yoneda embedding yoneda.obj X : Cᵒᵖ ⥤ Type v for X : C preserves limits.

        The coyoneda embedding coyoneda.obj X : C ⥤ Type v for X : Cᵒᵖ preserves limits.

        The yoneda embeddings jointly reflect limits.

        Instances For

          The coyoneda embeddings jointly reflect limits.

          Instances For