I'm slowly grasping this, though the different formulations of type theory make it difficult.
In http://imps.mcmaster.ca/doc/seven-virtues.pdf types can only be formed from *, i, and a->b when a and b are Types.
In http://www.youtube.com/watch?v=IWuWpLTiM3g (9:00) types can be constructed more liberally where A and B are Types then A or B, A and B, A implies B. However later in the video it is mentioned that a higher order type system could be constructed.
What I think I understand: Types are statements and their inhabitants are proofs. Since there is no way (that I can see) to quantify over these types they would define a simple predicate logic. Is this a correct assessment?
How can a type theory that allows quantification over types be constructed?