Equivalence between subobjects and quotients in an abelian category #
In an abelian category, the subobjects and quotient objects of an object
order-isomorphic via taking kernels and cokernels.
Implemented here using subobjects in the opposite category,
since mathlib does not have a notion of quotient objects at the time of writing.