Why do we need a separate notation for П-types?

Main

I am confused about the motivation behind the need for a separate notation for П-types, that you can find in type systems from λ2 on. The answer usually goes like so - think about how one can represent a signature of identity function - it can be λa:type.λx:a.x or λb:type.λx:b.x. The subtle part, they say, is that these two signatures not only not equal, they are not alpha-equivalent as type variables a and b are free variables inside their correspondent abstractions. So to overcome this pesky syntactic issue, we present П binder that plays nicely with alpha-conversion.

So the question: why is that? Why not just fix the notion of alpha-equivalence?
UPDATE z:

Oh, silly of me, λa:type.λx:a.x and λb:type.λx:b.x are alpha equivalent. But why a:type -> a -> a and b:type -> b -> b arent then.
UPDATE suc z:

Aha, interesting, I guess this is a perfect example of selective blindness =D

I am reading the book Type Theory and Formal Proof, and in the chapter about lambda2 author motivates the existence of П using exactly that kind of argumentation - one cant say that \t:.\v:t.v : -> t -> t because this makes two alpha-equivalent terms\t:.\v:t.v and \g:.\v:g.v have different types, as corresponding types are not alpha-equivalent, where types like t: -> t -> t are in fact alpha-invariant. Mind the difference between t: -> t -> t and * -> t -> t. But, doesn't it make this argument a bit trivial, and is it even something meaningful to talk about type a -> b where a and b are unbound by any quantifiers variables.
Andrej Bauer pointed out in the comments that П is indeed resembles a lambda abstraction with a few additional bells and whistles.

All in all, I am done with that one, thank you guys.

I think we just need to get some things straight here:

• In the expression $\lambda a : \mathsf{type} . \lambda x : a . x$ the variable $a$ is bound (by the outer $\lambda$). The expressions $\lambda a : \mathsf{type} . \lambda x : a . x$ and $\lambda b : \mathsf{type} . \lambda x : b . x$ are $\alpha$-equal.

• The expression $\lambda a : \mathsf{type} . \lambda x : a . x$ is the identity function, it is not the "signature of the identity function".

• If by "signature of the identity function" you mean to say "the type of the identity function", then it would be something like $\Pi_{a : \mathsf{type}} . (a \to a)$, or if you want only product types, then it is $\Pi_{a : \mathsf{type}} \Pi_{x : a} a$.

Is there still a question?

Maybe this will help:

• the type of the identity function $\lambda x : a . x$ is $a \to a$

• the type of the identity function $\lambda y : b . y$ is $b \to b$

• the functions $\lambda x : a . x$ and $\lambda y : b . y$ are different

• the types $a \to a$ and $b \to b$ are different

• the type of the polymorphic identity function $\lambda c : \mathsf{type} . \lambda z : c . z$ is $\Pi_{c : \mathsf{type}} . c \to c$.

• the functions $\lambda a : \mathsf{type} . \lambda x : a . x$ and $\lambda c : \mathsf{type} . \lambda z : c . z$ are $\alpha$-equal

• the types $\Pi_{a : \mathsf{type}} . a \to a$ and $\Pi_{c : \mathsf{type}} . c \to c$ are $\alpha$-equal.

Supplemental: After talking to Alex Simpson over a cup of tea, there is one more thing I can say. We don't need separate $\lambda$ and $\Pi$ constructors, as they both have precisely the same syntactic shape (take two arguments, bind one variable). In fact, if my memory serves me right, Automath used the same notation for $\lambda$-abstractions and $\Pi$-types. But the point is that we want to use two different constructors because they denote different concepts.

StackExchange Computer Science Q#129539, answer score: 8