Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(category/subobject): complete_lattice instance #6809

Closed
wants to merge 63 commits into from
Closed

[Merged by Bors] - feat(category/subobject): complete_lattice instance #6809

wants to merge 63 commits into from

Conversation

semorrison
Copy link
Collaborator

@semorrison semorrison commented Mar 22, 2021 •
edited by github-actions bot
Loading

@semorrison
feat(order/lattice): add complete_semilattice_Sup/Inf
01d19eb
@semorrison
refactor(category_theory/subobject): split into smaller files
efb52c0
@semorrison
reduce imports
01f3359
@semorrison
separate lattices
9108fa5
@semorrison
cleanup
3926fb9
@semorrison
fix import and add default
412d2c6
@semorrison
weird @
b1daf91
@semorrison
fix
8566c0a
@semorrison
Merge branch 'complete_semilattice_Sup' into subobject_complete_lattice
e90ba38
@semorrison
hmm, universe issues
aca8175
@semorrison
well_powered
066b8b2
@semorrison
looking okay
6bdc303
@semorrison
Merge remote-tracking branch 'origin/master' into subobject_complete_…
f7614b7 
…lattice
@semorrison
add files
45baed3
@semorrison
feat(category_theory): essentially_small categories
3ea58ca
@semorrison
Merge branch 'essentially_small' into subobject_complete_lattice
2f26019
@semorrison
split file
700673a
@semorrison
Merge branch 'essentially_small' into subobject_complete_lattice
e05b7cc
@semorrison
Merge branch 'essentially_small' into well_powered
7551642
@semorrison
feat(category/subobject): well-powered categories
ab7a762
@semorrison
Merge branch 'well_powered' into subobject_complete_lattice
eabeff2
@semorrison
fix
a825805
@semorrison
lint
28c4efe
@semorrison
Merge remote-tracking branch 'origin/master' into essentially_small
63c3a68
@semorrison
merge
51c9782
@semorrison
Merge branch 'well_powered' into subobject_complete_lattice
9479234
@semorrison
complete_semilattice_Inf
f89a1c5
@semorrison
how does Sup_le work?
a7f5675
@semorrison
finished
66d923b
@semorrison semorrison requested a review from b-mehta March 22, 2021 01:10
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 31, 2021
@github-actions github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed merge-conflict Please `git merge origin/master` then a bot will remove this label. blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Mar 31, 2021
@github-actions
Copy link

github-actions bot commented Apr 2, 2021

🎉 Great news! Looks like all the dependencies have been resolved:

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

b-mehta
b-mehta reviewed Apr 2, 2021
View reviewed changes
src/category_theory/subobject/lattice.lean Outdated Show resolved Hide resolved
src/category_theory/subobject/lattice.lean Outdated Show resolved Hide resolved
src/category_theory/subobject/lattice.lean Show resolved Hide resolved
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 5, 2021
@bryangingechen bryangingechen added the awaiting-author A reviewer has asked the author a question or requested changes label Apr 5, 2021
@semorrison semorrison added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 6, 2021
@semorrison semorrison requested a review from b-mehta April 6, 2021 04:47
jcommelin
jcommelin reviewed Apr 6, 2021
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

src/category_theory/limits/shapes/wide_pullbacks.lean Outdated Show resolved Hide resolved
src/category_theory/limits/shapes/wide_pullbacks.lean Outdated Show resolved Hide resolved
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Apr 6, 2021
@semorrison @jcommelin
Apply suggestions from code review
eb65f03 
Co-authored-by: Johan Commelin <johan@commelin.net>
@semorrison semorrison added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 6, 2021
@semorrison
Copy link
Collaborator Author

(For future reference, I'm very happy if people just click "commit changes" on any obvious suggestions they make to my PRs right away. I don't feel any need to review proposed whitespace changes. :-)

jcommelin
jcommelin approved these changes Apr 7, 2021
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Apr 7, 2021
bors bot pushed a commit that referenced this pull request Apr 7, 2021
@semorrison
feat(category/subobject): complete_lattice instance (#6809)
893173d 


Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Apr 7, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(category/subobject): complete_lattice instance [Merged by Bors] - feat(category/subobject): complete_lattice instance Apr 7, 2021
@bors bors bot closed this Apr 7, 2021
@bors bors bot deleted the subobject_complete_lattice branch April 7, 2021 19:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin approved these changes

@b-mehta b-mehta Awaiting requested review from b-mehta

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@semorrison @jcommelin @b-mehta @bryangingechen