## Stream: Is there code for X?

### Topic: cardinal

#### Kenny Lau (Jan 09 2021 at 18:37):

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

#### Reid Barton (Jan 09 2021 at 18:40):

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

#### Reid Barton (Jan 09 2021 at 18:40):

what do you need it for?

curiosity

#### Kenny Lau (Jan 09 2021 at 18:43):

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

oh I see

#### Reid Barton (Jan 09 2021 at 18:45):

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

#### Reid Barton (Jan 09 2021 at 18:47):

I'm pretty sure the answer must be no

#### Reid Barton (Jan 09 2021 at 18:48):

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 (Jan 09 2021 at 18:48):

well hmm maybe you can do it with an inductive predicate

#### Gabriel Ebner (Jan 11 2021 at 15:45):

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.)

Last updated: May 16 2021 at 05:21 UTC