Question regarding `Sort` and `Type`

Stream: new members

[Rajiv]

I am new to lean and am trying to understand Pi Types.

In Theorem Proving in Lean, in Section 4.1, following is mentioned.

It is the typing rule for Pi types, and the universal quantifier in particular, that distinguishes Prop from other types. Suppose we have α : Sort i and β : Sort j, where the expression β may depend on a variable x : α. Then Π x : α, β is an element of Sort (imax i j), where imax i j is the maximum of i and j if j is not 0, and 0 otherwise.

Something similar is also mentioned in Lean Reference Manual, Section 3.1 3.2.

an expression imax u v, where u and v are universe levels. The last one denotes the universe level 0 if v is 0, and max u v otherwise.

(Π x : α, β) : Sort (imax u v) where α : Sort u, and β : Sort v assuming x : α

When I tried the following example,

-- α : Sort 1
variable α : Type

-- m_ty : Sort 1 → Sort 1
variable m_ty : Type → Type

-- x₀ : Sort 1
constant x₀ : Type

-- m_ty x₀ : Sort 1
#check m_ty x₀

-- α : Type / Sort 1,
-- β = m_ty x₀, β : Sort 1,
#check Π (x : Type), m_ty x₀

-- Sort (imax 1 1) = Sort 1 = Type or Type 0

For some reason which I don't understand, #check Π (x : Type), m_ty x₀ is giving Type → m_ty x₀ : Type 1.

Shouldn't the expression Type → m_ty x₀ be of type Sort 1 or Type 0 (that is Sort (imax 1 1))?

I was wondering what mistake I might be doing in my thinking?

[Reid Barton]

To fit Π (x : Type), m_ty x₀ into the scheme Π x : α, β, we have α = Type, not α : Type.

[Rajiv]

Thanks @Reid Barton I see my error now. Π (x : α), m_ty x₀ expression does the right thing.