# UnivLE #

A proposition expressing a universe inequality. `UnivLE.{u, v}`

expresses that `u ≤ v`

,
in the form `∀ α : Type u, Small.{v} α`

.

See the doc-string for the comparison with an alternative stronger definition.

A class expressing a universe inequality. `UnivLE.{u, v}`

expresses that `u ≤ v`

.

There used to be a stronger definition `∀ α : Type max u v, Small.{v} α`

that immediately implies
`Small.{v} ((α : Type u) → (β : Type v))`

which is essential for proving that `Type v`

has
`Type u`

-indexed limits when `u ≤ v`

. However the current weaker condition
`∀ α : Type u, Small.{v} α`

also implies the same, so we switched to use it for
its simplicity and transitivity.

The strong definition easily implies the weaker definition (see below),
but we can not prove the reverse implication.
This is because in Lean's type theory, while `max u v`

is at least at big as `u`

and `v`

,
it could be bigger than both!
See also `Mathlib.CategoryTheory.UnivLE`

for the statement that the stronger definition is
equivalent to `EssSurj (uliftFunctor : Type v ⥤ Type max u v)`

.

## Equations

- UnivLE.{u, v} = ∀ (α : Type u), Small.{v, u} α