mathlib3

d11893b4 - fix(*): missing universe polymorphism (#18644)

fix(*): missing universe polymorphism (#18644) These are all just typo fixes, no proof adaptations. This deliberately leaves alone things related to category theory and algebraic geometry, as there the lack of polymorphism is likely deliberate.