Commit 2025-11-07 12:32 91325891
View on Github →feat(CategoryTheory/Yoneda): add curried version of Yoneda lemma for heterogeneous universes, and other version of homNatIso (#27819)
Prove a curried version of yonedaCompUliftFunctorEquiv, ie a completely functorial version of the Yoneda lemma with heterogeneous universes. Dually, prove a curried version of coyonedaCompUliftFunctorEquiv, ie a completely functorial version of the coYoneda lemma with heterogeneous universes.
In addition, prove a functorial version of FullyFaithful.natEquiv using coyoneda instead of yoneda (previously, the only functorial version of FullyFaithful.natEquiv were homNatIso, which is written using yoneda).