mathlib3

ddefd965 - feat(category_theory/subobject): kernels and images as subobjects (#6301)

feat(category_theory/subobject): kernels and images as subobjects (#6301) Further work on subobjects, building on the initial definition in #6278. * Add noncomputable functions to obtain representatives of subobjects. * Realise kernel/equalizer/image as subobjects. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>