Commit 2021-02-26 19:47 ddefd965

View on Github →

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.

Estimated changes