Commit 2023-11-24 09:10 988870b7

feat: switch to weaker UnivLE (#8556) Switch from the strong version of UnivLE ∀ α : Type max u v, Small.{v} α to the weaker version ∀ α : Type u, Small.{v} α. Transfer Has/Preserves/Reflects(Co)limitsOfSize from a larger size (higher universe) to a smaller size. In a few places it's now necessary to make the type explicit (for Lean to infer the Small instance, I think). Also prove a characterization of UnivLE and the totality of the UnivLE relation. A pared down version of #7695.