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 -&gt; a -&gt; a and b:type -&gt; b -&gt; 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 : * -&gt; t -&gt; 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:* -&gt; t -&gt; t are in fact alpha-invariant. Mind the difference between t:* -&gt; t -&gt; t and * -&gt; t -&gt; t. But, doesn't it make this argument a bit trivial, and is it even something meaningful to talk about type a -&gt; 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 &quot;signature of the identity function&quot;.
If by &quot;signature of the identity function&quot; you mean to say &quot;the type of the identity function&quot;, 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.