# UnivLE #

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

expresses that `u ≤ v`

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

.

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

See also `Mathlib.CategoryTheory.UnivLE`

for the statement
`UnivLE.{u,v} ↔ EssSurj (uliftFunctor : Type v ⥤ Type max u v)`

.

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

expresses that `u ≤ v`

.

There are (at least) two plausible definitions for `u ≤ v`

:

- strong:
`∀ α : Type max u v, Small.{v} α`

- weak:
`∀ α : Type u, Small.{v} α`

The weak definition has the advantage of being transitive.
However only under the strong definition do we have `Small.{v} ((α : Type u) → (β : Type v))`

,
which is essential for proving that `Type v`

has `Type u`

-indexed limits when `u ≤ v`

.

The strong definition 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!