feat(category_theory/limits): add kernel pairs (#3925)
Add a subsingleton data structure expressing that a parallel pair of morphisms is a kernel pair of a given morphism.
Another PR from my topos project. A pretty minimal API since I didn't need much there - I also didn't introduce anything like `has_kernel_pairs` largely because I didn't need it, but also because I don't know that it's useful for anyone, and it might conflict with ideas in the prop-limits branch.
