Structures · Logic and sets

UnivLE

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 cannot 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.lean for the statement that the stronger definition is equivalent to EssSurj (uliftFunctor : Type v ⥤ Type max u v).

Defined in

Mathlib.Logic.UnivLE

Shape

0 explicit arguments · adds small