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