7
$\begingroup$

I'm trying to determine the cardinality of Type u in Lean 3. So far I've been able to prove two inequalities:

  1. univ.{u u+1} ≤ # (Type u) (using quotient.out as an injection from cardinals to types)
  1. lift.{u+2} (# (Type u)) < univ.{u+1 u+2} (as # (Type u) is a cardinal in u + 1, and the universal cardinal of a given universe level is greater than all other cardinals in that level)

So I know that the cardinality of Type u is greater than or equal to the universal cardinal of u and less than the universal cardinal of u + 1. However, I'm wondering if I can narrow it down further. I suspect it might be equal to univ.{u}, but I don't know how to prove it.

Does anyone have any hints as to how to narrow down the cardinality of Type u?

$\endgroup$
2
  • 2
    $\begingroup$ We reached the same conclusions in this thread on Zulip: leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/… I expect that univ.{u u+1} = # (Type u) is independent of Lean. Almost anything that talks about equality of types is independent of Lean. For example, I wouldn't be surprised if # {A : Type u // is_empty A } > univ.{u u+1} is consistent with Lean. $\endgroup$ Jul 18 at 8:50
  • 2
    $\begingroup$ @FlorisvanDoorn you can probably craft a model where this inequality holds using some flavour of the "times bool" model of MLTT (see Section 5.1 from this paper), by replacing bool by some adequate type. AFAIK the model is simple enough to scale to all the extensions from the Lean type theory, including choice and whatnot. $\endgroup$ Jul 18 at 11:47

1 Answer 1

3
$\begingroup$

Equality is not provable. Indeed, it is consistent that univ.{u u+1} < #(Type u) at every level u.

Recall that the universe level operations that Lean allows are quite limited. (See Mario Carneiro, The Type Theory of Lean, for all the details.) The level terms are built from universe variables using only: 0, ∙+1, max(∙,∙) and imax(∙,∙). Because these operations are so limited, it is possible to give nontrivial self-interpretations of Lean's type theory in itself.

Let f be any strictly increasing function from levels to levels such that f(0) = 0. Consider the interpretation of Lean in itself where Sort u is reinterpreted as Sort f(u). Thus the new universe levels are only those in the range of f and the successor operation ∙+1 is reinterpreted so that f(u)+1 is now f(u+1). Everything in Lean's type theory works as-is with just a few exceptions. For example, Sort u : Sort u+1 doesn't work on-the-nose; similarly with some inductive types. There's a couple of different ways to patch this, the details are immaterial. (If Lean's type theory were cumulative there would essentially be nothing to fix.)

Now consider this self-interpretation where, for example, f(0)=0, f(1) = 1, ..., f(42) = 42 but f(43) = 44, f(44) = 45, etc. In this interpretation, Type 41 (= Sort 42) is unchanged but Type 42 is now the old Type 43. It follows that univ.{41 42} (which is basically the old univ.{41 43}) is strictly smaller than #(Type 42) (which is the old #(Type 43)). This is because the original univ.{42 43} and #(Type 42) still exists in between these two cardinals, even though they have lost their particular meaning in the new interpretation.

$\endgroup$
2
  • 2
    $\begingroup$ I guess the moral here is that one shouldn't think of Type (u+1) as the next universe after Type u but rather as the next designated universe; there might be plenty of could-be universes in between that have no special designation. $\endgroup$ Jul 24 at 10:01
  • $\begingroup$ Thanks for the answer! $\endgroup$ Jul 28 at 1:23

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.