Zulip Chat Archive

Stream: new members

Topic: Question regarding `Sort` and `Type`

view this post on Zulip Rajiv (Nov 29 2020 at 13:27):

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?

view this post on Zulip Reid Barton (Nov 29 2020 at 13:39):

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

view this post on Zulip Rajiv (Nov 29 2020 at 13:51):

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

Last updated: May 06 2021 at 20:13 UTC