Smallness inequality

Stream: Is there code for X?

[Nir Paz]

Do we have something like this?

example {α} (hα : Small.{u} α) (h : Small.{v + 1} (Type u)) : Small.{v} α := by
  sorry

apply apparantly ignores universes, so it suggests wrong things.
If we don't, any tips would be nice (:

[Daniel Weber]

There's a fair chance that this is independent of Lean's axioms

[Daniel Weber]

This is equivalent to

example (h : Small.{v + 1} (Type u)) : UnivLE.{u, v} := sorry

[Daniel Weber]

And I believe that's equivalent to

example : UnivLE.{u, v} ∨ UnivLE.{v + 1, u} := sorry

although I haven't proved that

[Mario Carneiro]

Yes, this is definitely independent. There is no axiom saying that universes are linearly ordered

[Daniel Weber]

Mario Carneiro said:

Yes, this is definitely independent. There is no axiom saying that universes are linearly ordered

(deleted)

EDIT: nvm, this is just docs#univLE_total

[Daniel Weber]

The main thing you can't prove is u < v + 1 → u ≤ v, right?

[Mario Carneiro]

I see, univLE_total makes it clear that this is not really a statement about universes, but rather about the size of the sets those universes produce, which is of course a total order because we have the axiom of choice

[Mario Carneiro]

This is arguably not a faithful translation of the <= relation on universes (meaning that max u v = v), and in fact there isn't even a clear notion of < on universes, since lean, being non-cumulative, only has the relation u <: v defined as "Type u : Type v typechecks", which basically only holds when v = u+1 in the syntactical theory

[Nir Paz]

The problem is that v + 1 doesn't have to be the next universe after v. If the claim is wrong, then univ.{v} < univ.{u} < univ.{v + 1}:

open Cardinal

example {α} (hα : Small.{u} α) (h : Small.{v + 1} (Type u)) (h' : ¬Small.{v} α) :
    univ.{v, u + 1} < univ.{u, v + 1} ∧ univ.{u, v + 2} < univ.{v + 1, u + 1} := by
  constructor
  · by_contra! hu
    rw [← univLE_iff_cardinal_le] at hu
    rcases hα.equiv_small with ⟨β, ⟨hβ⟩⟩
    specialize hu β
    refine h' ?_
    rw [small_iff]
    rcases hu with ⟨γ, ⟨hγ⟩⟩
    exact ⟨γ, ⟨hβ.trans hγ⟩⟩
  · by_contra! hu
    rw [← univLE_iff_cardinal_le] at hu
    rcases h.equiv_small with ⟨β, ⟨hβ⟩⟩
    rcases hu β with ⟨γ, ⟨hγ⟩⟩
    apply not_small_type.{u, u}
    rw [small_iff]
    exact ⟨γ, ⟨hβ.trans hγ⟩⟩