Commit 2022-04-05 19:36 d34cbcf6

refactor(algebra/homology, category_theory/*): declassify exactness (#13153) Having exact be a class was very often somewhat inconvenient, so many lemmas took it as a normal argument while many others had it as a typeclass argument. This PR removes this inconsistency by downgrading exact to a structure. We lose very little by doing this, and using typeclass inference as a Prolog-like "automatic theorem prover" is rarely a good idea anyway.