Commit 2023-07-04 07:03 5dc6092dView on Github →
chore(topology/sheaves): revert universe generalizations from #19153 (#19230)
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.