Commit 2020-04-20 07:17 9b255781

fix(category_theory/limits): avoid a rewrite in a definition (#2458) The proof that every equalizer of f and g is an isomorphism if f = g had an ugly rewrite in a definition (introduced by yours truly). This PR reformulates the proof in a cleaner way by working with two morphisms f and g and a proof of f = g right from the start, which is easy to specialze to the case (f, f), instead of trying to reduce the (f, g) case to the (f, f) case by rewriting. This also lets us get rid of fork.eq_of_ι_ι, unless someone wants to keep it, but personally I don't think that using it is ever a good idea.