UnivLE

A proposition expressing a universe inequality. UnivLE.{u, v} expresses that u ≤ v, in the form ∀ α : Type u, Small.{v} α.

This API indirectly provides an instance for Small.{u, max u v}, which could not be declared directly due to https://github.com/leanprover/lean4/issues/2297.

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

@[reducible, inline]

abbrev UnivLE : Prop

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.5, ?u.4} = ∀ (α : Type ?u.5), Small.{?u.4, ?u.5} α

theorem univLE_max : UnivLE.{u, max u v}

theorem Small.trans_univLE (α : Type w) [hα : Small.{u, w} α] [h : UnivLE.{u, v} ] : Small.{v, w} α

theorem UnivLE.trans [UnivLE.{u, v} ] [UnivLE.{v, w} ] : UnivLE.{u, w}

instance univLE_of_max [UnivLE.{max u v, v} ] : UnivLE.{u, v}

Equations

• ⋯ = ⋯