Dependent Type Theory Section

Stream: Lean for the curious mathematician 2020

[ccn]

Hi I'm reading said section from the book "Theorem Proving in Lean", and I'm having a few questions hopefully I can get some help:

image.png

Here' I'm experimenting with universe variables but I don't get why it says u_1 instead of just u also u is representing some natural number right?

[Heather Macbeth]

Hi @ccn, please ask this question in #new members, this is an old stream dedicated to a conference in 2020.

[ccn]

Heather Macbeth said:

Hi ccn, please ask this question in #new members, this is an old stream dedicated to a conference in 2020.

Ah ok, my bad I missed the 2020 at the end.