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 binders 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?