[Merged by Bors] - chore(topology/sheaves/*): universe generalizations #19153
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
semorrison
added
awaiting-review
github-actions
bot
removed
the
awaiting-CI
|
bors r+ |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Jun 4, 2023
Necessary but sadly insufficient for the request at https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2319146.20sheaves.20on.20manifolds Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 21, 2023
….lift_mk_le` (#5325) `Cardinal.lift_le` and `Cardinal.lift_mk_le` have their universes out of order, in the sense that persistently through the rest of the library we need to specify the 2nd universe (resp 3rd), while the others are solved by unification. This PR reorders the universes so it's easier to specify the thing you need to specify! (This PR doesn't get rid of all the occurrences of `\.\{_,` in the library, but I'd like to do that later.) I do have a hidden agenda here, which is that I've been experimenting with solutions to the dreaded "Can't solve `max u v = max v ?u`" universe unification issue (which is making life hellish forward porting leanprover-community/mathlib#19153), and my favourite (but still hacky) solution doesn't like some of the occasions where we reference a lemma filling in some of its universe arguments with `_` but then fully specify a later one. (e.g. `rw [← lift_le.{_, max u v}, lift_lift, lift_mk_le.{_, _, v}]` in `ModelTheory/Skolem.lean`). Hence the cleanup proposed in this PR makes my life easier working on these experiments. :-) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
alexkeizer
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 22, 2023
….lift_mk_le` (#5325) `Cardinal.lift_le` and `Cardinal.lift_mk_le` have their universes out of order, in the sense that persistently through the rest of the library we need to specify the 2nd universe (resp 3rd), while the others are solved by unification. This PR reorders the universes so it's easier to specify the thing you need to specify! (This PR doesn't get rid of all the occurrences of `\.\{_,` in the library, but I'd like to do that later.) I do have a hidden agenda here, which is that I've been experimenting with solutions to the dreaded "Can't solve `max u v = max v ?u`" universe unification issue (which is making life hellish forward porting leanprover-community/mathlib#19153), and my favourite (but still hacky) solution doesn't like some of the occasions where we reference a lemma filling in some of its universe arguments with `_` but then fully specify a later one. (e.g. `rw [← lift_le.{_, max u v}, lift_lift, lift_mk_le.{_, _, v}]` in `ModelTheory/Skolem.lean`). Hence the cleanup proposed in this PR makes my life easier working on these experiments. :-) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
1 task
semorrison
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 23, 2023
….lift_mk_le` (#5325) `Cardinal.lift_le` and `Cardinal.lift_mk_le` have their universes out of order, in the sense that persistently through the rest of the library we need to specify the 2nd universe (resp 3rd), while the others are solved by unification. This PR reorders the universes so it's easier to specify the thing you need to specify! (This PR doesn't get rid of all the occurrences of `\.\{_,` in the library, but I'd like to do that later.) I do have a hidden agenda here, which is that I've been experimenting with solutions to the dreaded "Can't solve `max u v = max v ?u`" universe unification issue (which is making life hellish forward porting leanprover-community/mathlib#19153), and my favourite (but still hacky) solution doesn't like some of the occasions where we reference a lemma filling in some of its universe arguments with `_` but then fully specify a later one. (e.g. `rw [← lift_le.{_, max u v}, lift_lift, lift_mk_le.{_, _, v}]` in `ModelTheory/Skolem.lean`). Hence the cleanup proposed in this PR makes my life easier working on these experiments. :-) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
semorrison
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 23, 2023
….lift_mk_le` (#5325) `Cardinal.lift_le` and `Cardinal.lift_mk_le` have their universes out of order, in the sense that persistently through the rest of the library we need to specify the 2nd universe (resp 3rd), while the others are solved by unification. This PR reorders the universes so it's easier to specify the thing you need to specify! (This PR doesn't get rid of all the occurrences of `\.\{_,` in the library, but I'd like to do that later.) I do have a hidden agenda here, which is that I've been experimenting with solutions to the dreaded "Can't solve `max u v = max v ?u`" universe unification issue (which is making life hellish forward porting leanprover-community/mathlib#19153), and my favourite (but still hacky) solution doesn't like some of the occasions where we reference a lemma filling in some of its universe arguments with `_` but then fully specify a later one. (e.g. `rw [← lift_le.{_, max u v}, lift_lift, lift_mk_le.{_, _, v}]` in `ModelTheory/Skolem.lean`). Hence the cleanup proposed in this PR makes my life easier working on these experiments. :-) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
semorrison
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 25, 2023
….lift_mk_le` (#5325) `Cardinal.lift_le` and `Cardinal.lift_mk_le` have their universes out of order, in the sense that persistently through the rest of the library we need to specify the 2nd universe (resp 3rd), while the others are solved by unification. This PR reorders the universes so it's easier to specify the thing you need to specify! (This PR doesn't get rid of all the occurrences of `\.\{_,` in the library, but I'd like to do that later.) I do have a hidden agenda here, which is that I've been experimenting with solutions to the dreaded "Can't solve `max u v = max v ?u`" universe unification issue (which is making life hellish forward porting leanprover-community/mathlib#19153), and my favourite (but still hacky) solution doesn't like some of the occasions where we reference a lemma filling in some of its universe arguments with `_` but then fully specify a later one. (e.g. `rw [← lift_le.{_, max u v}, lift_lift, lift_mk_le.{_, _, v}]` in `ModelTheory/Skolem.lean`). Hence the cleanup proposed in this PR makes my life easier working on these experiments. :-) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 28, 2023
Preliminary to the full forward port of leanprover-community/mathlib#19153, this is a slight generalization along with explanation of the problem with the instances. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
semorrison
added a commit
that referenced
this pull request
Jul 4, 2023
This reverts commit 1336155.
bors bot
pushed a commit
that referenced
this pull request
Jul 4, 2023
…19230) This reverts commit 1336155. These are just too difficult to forward port as is because of the `max u v =?= max u ?v` issue leanprover/lean4#2297. We have another candidate approach to this, using a new `UnivLE` typeclass, and I would prefer if we investigated that without the pressure of the port at the same time. This will delay @hrmacbeth's plans to define meromorphic functions, perhaps. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
1 task
kbuzzard
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jul 6, 2023
Preliminary to the full forward port of leanprover-community/mathlib#19153, this is a slight generalization along with explanation of the problem with the instances. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jul 7, 2023
This is a test of the `UnivLE` proposal. The `UniqueGluing` file was one place where we couldn't forward port the universe generalisations made in mathlib3 in leanprover-community/mathlib#19153. Diff relative to #5724 is UnivLE_types...UnivLE_UniqueGluing. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Matthew Robert Ballard <matt@mrb.email> Co-authored-by: Bulhwi Cha <chabulhwi@semmalgil.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Pol'tta / Miyahara Kō <pol_tta@outlook.jp> Co-authored-by: Oliver Nash <github@olivernash.org> Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com> Co-authored-by: Tobias Grosser <tobias@grosser.es> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Moritz Firsching <moritz.firsching@gmail.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com> Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com>
qawbecrdtey
pushed a commit
to qawbecrdtey/greedoid-mathlib4
that referenced
this pull request
Jul 7, 2023
…r-community#5726) This is a test of the `UnivLE` proposal. The `UniqueGluing` file was one place where we couldn't forward port the universe generalisations made in mathlib3 in leanprover-community/mathlib#19153. Diff relative to leanprover-community#5724 is leanprover-community/mathlib4@UnivLE_types...UnivLE_UniqueGluing. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Matthew Robert Ballard <matt@mrb.email> Co-authored-by: Bulhwi Cha <chabulhwi@semmalgil.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Pol'tta / Miyahara Kō <pol_tta@outlook.jp> Co-authored-by: Oliver Nash <github@olivernash.org> Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com> Co-authored-by: Tobias Grosser <tobias@grosser.es> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Moritz Firsching <moritz.firsching@gmail.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com> Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com>
bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jul 16, 2023
This forward-ports the revert (leanprover-community/mathlib#19230) of changes that were never forward-ported (leanprover-community/mathlib#19153). Therefore only the SHA needs updating.
semorrison
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Aug 14, 2023
Preliminary to the full forward port of leanprover-community/mathlib#19153, this is a slight generalization along with explanation of the problem with the instances. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
semorrison
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Aug 14, 2023
This is a test of the `UnivLE` proposal. The `UniqueGluing` file was one place where we couldn't forward port the universe generalisations made in mathlib3 in leanprover-community/mathlib#19153. Diff relative to #5724 is UnivLE_types...UnivLE_UniqueGluing. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Matthew Robert Ballard <matt@mrb.email> Co-authored-by: Bulhwi Cha <chabulhwi@semmalgil.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Pol'tta / Miyahara Kō <pol_tta@outlook.jp> Co-authored-by: Oliver Nash <github@olivernash.org> Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com> Co-authored-by: Tobias Grosser <tobias@grosser.es> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Moritz Firsching <moritz.firsching@gmail.com> Co-authored-by: Jireh Loreaux <loreaujy@gmail.com> Co-authored-by: Christopher Hoskin <christopher.hoskin@gmail.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Necessary but sadly insufficient for the request at https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2319146.20sheaves.20on.20manifolds