Commit 2020-08-28 14:11 31db0bdd

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.