# Commit 2020-04-11 07:17 8556499f

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