MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

The basic idea is that a polymorphic construction (in a polymorphic lambda calculus) must behave uniformly, and so must preserve relations. For example, any term of type $\Pi X. X\to X$ must be the identity function, and every term of type $\Pi X Y. X\times Y\to X$ must be the first projection.