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?
