mathlib

a7784aad - feat(category_theory/*): Yoneda extension is Kan (#9574)

feat(category_theory/*): Yoneda extension is Kan (#9574) - Proved that `(F.elements)ᵒᵖ ≌ costructured_arrow yoneda F`. - Verified that the yoneda extension is indeed the left Kan extension along the yoneda embedding.