Note to Self: Explaining System F

When explaining Church encodings of data types in System F, we can say that we first come up with a type that encompasses the fundamental structure of what we can do with that type and then by quantifying over all possible types that have that property, you necessarily create a type that has only that behavior as a least common denominator. 

Need to figure out a better way of saying this, of creating the proper picture, before I give that second part of my talk where I talk about typed calculi.