Commit 2023-07-07 10:02 0f6207a5
View on Github →feat: using UnivLE to generalize universes in UniqueGluing (#5726)
This is a test of the UnivLE proposal. The UniqueGluing file was one place where we couldn't forward port the universe generalisations made in mathlib3 in https://github.com/leanprover-community/mathlib/pull/19153.
Diff relative to #5724 is https://github.com/leanprover-community/mathlib4/compare/UnivLE_types...UnivLE_UniqueGluing.