# Commit 2021-10-07 06:14 a7784aad

View on Github →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.