Commit 2024-06-30 17:16 8c938d7d

View on Github →

feat(CategoryTheory): two more versions of the Yoneda lemma (#14295)

Estimated changes

Modified Mathlib/CategoryTheory/Types.lean

added theorem CategoryTheory.uliftFunctor_obj

Modified Mathlib/CategoryTheory/Yoneda.lean

added def CategoryTheory.coyonedaCompYonedaObj

added def CategoryTheory.largeCurriedCoyonedaLemma

added def CategoryTheory.largeCurriedYonedaLemma

added def CategoryTheory.yonedaOpCompYonedaObj