Type universes confusion

Stream: new members

[Rado Kirov]

Let's start with this valid Lean code:

example (x: Nat): False := sorry

since #check Nat tells me Nat is of type Type = Type 0, I can abstract like this

example (T: Type) (x: T): False := sorry

So far so good, but when I repeat this one more time - type of Type is Type 1

example (T': Type 1) (T: T') (x: T): False := by sorry

I get a Lean error. What am I missing that explains this behavior?

[Stepan Nesterov]

Why do you think that if (T: T') then T is a type?

[Rado Kirov]

What else could it be?

[Stepan Nesterov]

It is a term of type T'

[Stepan Nesterov]

Well, ok, in this example we can have T' = Type.
Then Type : Type 1 ok, T : Type ok

[Rado Kirov]

Yes, I am just generalizing the types that were previously accepted

[Stepan Nesterov]

But I suppose that if T' : Type 1 is any other thing than T' = Type then terms of T' are just that: terms? :thinking:

[Rado Kirov]

Yes, I was wondering what would those other things be, because the error doesn’t specify. Also the error is in x: T only so T:T’ is accepted

[Stepan Nesterov]

Well, another thing it can be is T' = ℕ × Type, for example. Then T' : Type 1 ok, T : ℕ × Type ok, but x : T not ok. T isn't a type, it's a pair (natural number + type)

[Stepan Nesterov]

I think T : Type 1 is more like "T is a type so large it doesn't fit into Type" than "T is a metatype whose terms are types"

[Stepan Nesterov]

I don't know if there is a way to say the latter in Lean, that's an interesting question

[Matt Diamond]

@Rado Kirov T' could be Cardinal.{0}, for instance. In that case T would be a specific cardinal, and it wouldn't make sense to say x : T

[Matt Diamond]

Also the error is in x: T only so T:T’ is accepted

This isn't too surprising... you've declared that T' is a type, so it makes sense to say that you have a term T of type T'. The problem arises when you try to assume that T is also a type.

[Kenny Lau]

Rado Kirov said:

Yes, I am just generalizing the types that were previously accepted

well, that's not how maths/lean works...
the only time you can ever do a double colon is with Prop and Type _ (both are collective called Sort _)

[Matt Diamond]

Would it be accurate to say that there's only a single type at any non-zero universe level whose terms are also types?

[Kenny Lau]

that's circular, what does "at universe level X" mean

[Matt Diamond]

like one of the terms of Type 10 is Type 9, which itself has types as terms, but the other terms of Type 10 don't... though now that I say this, I'm realizing that it doesn't take ULift into consideration

[Matt Diamond]

like you could also lift Type 5 so that it's a term of Type 10 (I think?)

[Kenny Lau]

I see, yes that's correct (if we believe in unique typing)

[Aaron Liu]

Matt Diamond said:

like one of the terms of Type 10 is Type 9, which itself has types as terms, but the other terms of Type 10 don't... though now that I say this, I'm realizing that it doesn't take ULift into consideration

This isn't a question you can ask in Lean

[Aaron Liu]

"does term x have type T" isn't a question you can ask in Lean

[Matt Diamond]

I'm not sure I follow... I'm not asking if a term has a specific type, I'm asking if a term is a type

[Matt Diamond]

is it not accurate to say that some types are type universes and other types are just types?

[Aaron Liu]

You would have to say what a universe is

[Aaron Liu]

Matt Diamond said:

I'm not sure I follow... I'm not asking if a term has a specific type, I'm asking if a term is a type

The way to say a term t is a type is to write t : Type _ so that's the same thing

[Aaron Liu]

You're asking if t has type Type _

[Kenny Lau]

@Matt Diamond note that this code does not compile:

inductive IsSort : Type → Prop where
  | intro (T : Type) (x : T) (y : x) : IsSort T

[Matt Diamond]

I'm just saying that Type (u+1) has a single term called Type u whose terms are also types, and the rest of the terms of Type (u+1) do not seem to have this property... I understand that this isn't a mathematical fact that one could prove in Lean, but is actually the structure of Lean itself

[Aaron Liu]

What does it mean for a term to "be a type"

[Kenny Lau]

I confirmed that above, saying that it's true if we assume unique typing

[Rado Kirov]

@Matt Diamond 's question makes a lot of sense to me.

When I write something like

example (x : (3:ℕ)) := False

Lean errors with type expected, got (3 : ℕ) which basically is saying 3 is not a type. Same with my example

example (T': Type 1) (T: T') (x: T): False := by sorry

Clearly this has nothing to do with the LHS of the : it is just the name of the free variable, so there is some internal determination on what is a type, i.e. what can I write RHS of : and what not.

[Matt Diamond]

@Kenny Lau I know, I'm just responding to @Aaron Liu's question about whether or not what I'm saying is sufficiently defined

[Aaron Liu]

basically, x : t does not typecheck unless inferring the type of t gives you a Sort _

[Matt Diamond]

yes, that's what it means for t to be a type

[Aaron Liu]

and this property of t is not preserved under definitional equality

[Matt Diamond]

could you give me an example of that? it does sound like it complicates the picture I had of what makes something a type

[Matt Diamond]

I didn't realize you could have a situation where x : t typechecks but y : u doesn't even though t and u are definitionally equal

[Riccardo Brasca]

I am not totally sure, but I think that the point is that you can have two terms t and u that are ideally definitionally equal (the "true" definitional equality"), but Lean fails to realize so, and in practice you can write x : t but not x : u

[Aaron Liu]

Matt Diamond said:

could you give me an example of that? it does sound like it complicates the picture I had of what makes something a type

I just checked and it seems to have been patched out

[Aaron Liu]

so maybe it was a bug

[Matt Diamond]

hmm... so maybe the distinction between "X is a type" and "X is not a type" is mostly clear-cut, at least for now :sweat_smile:

[Riccardo Brasca]

I am (almost) sure that there is theorem/axiom/whatever in type theory saying that if you have x : t and y : u with x ≡ y then t ≡ u, where ≡ is the ideal definitional equality (the one that is transitive but undecidable in Lean).

[James E Hanson]

Riccardo Brasca said:

I am not totally sure, but I think that the point is that you can have two terms t and u that are ideally definitionally equal (the "true" definitional equality"), but Lean fails to realize so, and in practice you can write x : t but not x : u

This is discussed in Section 3.1.1 of Mario's thesis. Specifically, the form of definitional equality actually checked by Lean isn't transitive.

[James E Hanson]

Riccardo Brasca said:

I am (almost) sure that there is theorem/axiom/whatever in type theory saying that if you have x : t and y : u with x ≡ y then t ≡ u, where ≡ is the ideal definitional equality (the one that is transitive but undecidable in Lean).

I think you're thinking of unique typing, which is a metatheoretical property, rather than something you posit explicitly.

[Rado Kirov]

My original question is answered (thank you all that contributed) - (T : ?) (x : T) is accepted if ? is Sort _ otherwise not. A good counter example is Nat x Type (or Nat -> Type). The terminology “? Is a type” when the property above is true is probably bad and confusing, but I don’t know what else to call it.

[Matt Diamond]

I'm still curious about @Aaron Liu's claim that "X is a type" is an ambiguous statement... it seems like Lean is able to discriminate between something that "is a type" and "is not a type" when you get the error message "type expected, got..." but I'm wondering if this distinction is more superficial than it appears

[Robert Maxton]

I would argue that "X is a type" is merely not a proposition internal to Lean, but it certainly is a proposition at a meta level
It's a little Godelian, in that it may be a true statement but it's not something you can prove within Lean.

[James E Hanson]

I wouldn't really call it 'Gödelian' per se. The distinction between propositions and judgments is a pretty intentional design choice baked into the formalism of Martin-Löf type theory. So a statement like "X is a type" isn't even formalizable in type theory as a proposition. A Gödelian thing would be something that is formalizable and is true in intended models of the theory, but isn't provable.