# Commit 2020-04-20 07:17 9b255781

View on Github →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.