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!
Equations
- UnivLE.{u, v} = ∀ (α : Type (max u v)), Small.{v, max u v} α