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