mathlib

25df2671 - feat(category_theory/limits/presheaf): free cocompletion (#4740)

feat(category_theory/limits/presheaf): free cocompletion (#4740) Fill in the missing part of #4401, showing that the yoneda extension is unique. Also adds some basic API around #4401.