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: port/CategoryTheory.Sites.Limits #3463

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - feat: port/CategoryTheory.Sites.Limits #3463

wants to merge 9 commits into from

Conversation

kbuzzard
Copy link
Member

@kbuzzard kbuzzard commented Apr 16, 2023 •
edited by Parcly-Taxel
Loading

Open in Gitpod

@kbuzzard
feat: port CategoryTheory.Sites.Limits
12fd719
@kbuzzard
Initial file copy from mathport
02f41f6
@kbuzzard
automated fixes
fbd7580 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@kbuzzard kbuzzard added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Apr 16, 2023
@kbuzzard kbuzzard added help-wanted The author needs attention to resolve issues and removed help-wanted The author needs attention to resolve issues labels Apr 16, 2023
@kbuzzard kbuzzard added help-wanted The author needs attention to resolve issues and removed WIP Work in progress labels Apr 16, 2023
@kbuzzard
Copy link
Member Author

OK so I've basically got this file compiling, but it's no good. Typeclass inference can't solve certain universe problems, which means that the instances defined in this file aren't going to fire.

@kbuzzard
Copy link
Member Author

Ok so it looks like a good fix is to change the objects of C to live in Type u. I've done this in mathlib3 at leanprover-community/mathlib#18817 and will then forward-port to this and the instances should then fire.

@kbuzzard
Copy link
Member Author

I think the only thing left with this PR is an erw which is generating two extra goals in lean 4 which it wasn't doing in lean 3. I think one can be closed with (F.obj k).cond but I'm not sure about the other one; it can't be hard though, if lean 3 was closing it automatically.

@adamtopaz
Copy link
Contributor

I think the only thing left with this PR is an erw which is generating two extra goals in lean 4 which it wasn't doing in lean 3. I think one can be closed with (F.obj k).cond but I'm not sure about the other one; it can't be hard though, if lean 3 was closing it automatically.

I got the file to build. The proof was hidden under two layers of definitions, so it was just a matter of unfolding the right stuff.

@Parcly-Taxel Parcly-Taxel added awaiting-review and removed help-wanted The author needs attention to resolve issues labels Apr 18, 2023
@ChrisHughes24
Copy link
Member

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Apr 19, 2023
bors bot pushed a commit that referenced this pull request Apr 19, 2023
@kbuzzard @joelriou
@Parcly-Taxel @adamtopaz
feat: port/CategoryTheory.Sites.Limits (#3463)
96f9551 
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: adamtopaz <github@adamtopaz.com>
@bors
Copy link

bors bot commented Apr 19, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port/CategoryTheory.Sites.Limits [Merged by Bors] - feat: port/CategoryTheory.Sites.Limits Apr 19, 2023
@bors bors bot closed this Apr 19, 2023
@bors bors bot deleted the port/CategoryTheory.Sites.Limits branch April 19, 2023 13:42
semorrison pushed a commit that referenced this pull request May 10, 2023
@kbuzzard @joelriou
@Parcly-Taxel @adamtopaz
feat: port/CategoryTheory.Sites.Limits (#3463)
f951c54 
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: adamtopaz <github@adamtopaz.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@kbuzzard @adamtopaz @ChrisHughes24 @Parcly-Taxel @joelriou