mathlib
5dc6092d - chore(topology/sheaves): revert universe generalizations from #19153 (#19230)

Commit
2 years ago
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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading