search

leanprover-community / mathlib

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.66k stars 297 forks source link

[Merged by Bors] - chore(topology/sheaves): revert universe generalizations from #19153 #19230

Closed semorrison closed 1 year ago

semorrison commented 1 year ago

This reverts commit 13361559d66b84f80b6d5a1c4a26aa5054766725.

These are just too difficult to forward port as is because of the max u v =?= max u ?v issue https://github.com/leanprover/lean4/issues/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.

Open in Gitpod

jcommelin commented 1 year ago

Thanks :tada:

If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.

bors d+

bors[bot] commented 1 year ago

:v: semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

semorrison commented 1 year ago

bors merge

bors[bot] commented 1 year ago

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. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.