Cardinality of universes

Stream: Type theory

[Nir Paz]

Is the following true in lean's type theory?

example : #(Type 0) = #(Cardinal.{0}) := sorry

Cardinal.{0} easily injects into Type, but the other direction seems more difficult (if it's even decidable). The analogous set theory statement |V_k| = k is true for inaccessible k, so I thought there might be a way to build up Type 0 in steps and get a similar result.

More generally, if all types in a universe inject into a type, does that universe inject into it? Since a universe is bigger than any one type in it, I think this is the same as asking if there are cardinalities between sup #α, α : Type u and #(Type u).

[Matt Diamond]

Take a look at this thread for some discussion: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/The.20cardinal.20.60.23.28Type.20u.29.60/near/273258468

[Nir Paz]

ah, I looked in the wrong stream. Thanks!