Stream: new members
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?
Reid Barton (Nov 29 2020 at 13:39):
Π (x : Type), m_ty x₀ into the scheme Π x : α, β, we have
α = Type, not
α : Type.
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