Commit 2023-11-24 14:23 afb00b05

refactor(CategoryTheory/Idempotents): replacing equalities of functors by isomorphisms (#8562) In the context of idempotent completion of categories and the Dold-Kan equivalence, constructing some isomorphisms was very slow in Lean 3 but has been much faster in Lean 4, while using equalities of functors in Lean 3 was fast, but in Lean 4 it became very slow. In this PR, we switch to using mostly isomorphisms of functors: this also became necessary in order to make the refactor #8531 possible.