cardinal

Stream: Is there code for X?

[Kenny Lau]

Can I express "the set of cardinal.{u} that comes from Type v for v < u"?

[Reid Barton]

If u is of the form u' + 1...

[Reid Barton]

what do you need it for?

[Kenny Lau]

curiosity

[Kenny Lau]

as in, {#(Type 0), #(Type 1), #(Type 2)} : set cardinal.{3}

[Reid Barton]

oh I see

[Reid Barton]

I thought you meant all the cardinals that come from a smaller universe

[Reid Barton]

I'm pretty sure the answer must be no

[Reid Barton]

The cardinals that are of this form have to be inaccessible cardinals in cardinal.{u} (which you can define easily as infinite cardinals closed under sigmas and pis) but not every inaccessible has to be one of the Type v with v < u

[Reid Barton]

well hmm maybe you can do it with an inductive predicate

[Gabriel Ebner]

As Reid said, Type can be any sequence of strongly inaccessible cardinals in the set-theoretic model. Every definition and inductive in Lean only depends on a finite number of universes, no matter what concrete levels you instantiate the universe parameters with. A potential definition of cardinal_set.{u} could hence only refer to, say, 3, universes, and therefore cardinal_set.{5} can be interpreted as different sets depending on how you interpret the sequence Type. (In fact you can think of definitions/inductives as schemes. Every definition/inductive generates an infinite number of definitions/inductives that only differ by the universe levels.)