New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(category_theory): make defining groupoids easier #2360
Conversation
@dwarn, let's try an experiment. Our new PR merging system allows delegating approval. Let's try it. I'll write |
bors d+ |
✌️ dwarn can now approve this pull request. To approve and merge a pull request, simply reply with |
Looks good! |
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?
Build succeeded |
Pull request successfully merged into master. |
…munity#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?
…munity#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?
…munity#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?
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 ofnonempty
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?
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list