Commit 2020-04-11 07:17 8556499f

feat(category_theory): make defining groupoids easier (#2360) The point of this PR is to lower the burden of proof in showing that a category is a groupoid. Rather than constructing well-defined two-sided inverses everywhere, with groupoid.of_trunc_split_mono you'll only need to show that every morphism has some retraction. This makes defining the free groupoid painless. There the retractions are defined by recursion on a quotient, so this saves the work of showing that all the retractions agree. I used trunc instead of nonempty to avoid choice / noncomputability. I don't understand why the @'s are needed: it seems Lean doesn't know what category structure C has without specifying it?