Theorem CategoryTheory.shrinkYonedaEquiv_naturality

Modification history

2025-12-11 08:08
Mathlib/CategoryTheory/ShrinkYoneda.lean
feat(CategoryTheory): the Yoneda embedding for a locally small category (#32424) …
Added CategoryTheory.shrinkYonedaEquiv_naturalityView on Github →