Commit 2023-07-04 07:03 5dc6092d

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.