# 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.