Commit 2025-12-11 08:08 2bf8d4ba
View on Github →feat(CategoryTheory): the Yoneda embedding for a locally small category (#32424)
Let C be a locally w-small category. We define the Yoneda embedding shrinkYoneda : C ⥤ Cᵒᵖ ⥤ Type w.
feat(CategoryTheory): the Yoneda embedding for a locally small category (#32424)
Let C be a locally w-small category. We define the Yoneda embedding shrinkYoneda : C ⥤ Cᵒᵖ ⥤ Type w.