Variables in Types in type theory

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?

-

Martin-Löf type theory has free variables. If $A$ is type and the free variable $x$ is of type $A$, then we can think of $B(x)$ as a family of types indexed by $A$. We can then form the product type, written $\Pi_{x \in A} B(x)$ corresponding to product or universal quantification, and the sum type $\Sigma_{x \in A}B(x)$ corresponding to disjoint union or existential quantification.

-
It seems that what you seen is simply typed lambda calculus, in which types form an algebra freely generated by basic types via the operations $+$,$\times$ and $\rightarrow$.
For the Curry-Howard isomorphism you can identify types with proposition of the intuizionistic propositional logic and so the type operations $+$,$\times$ and $\rightarrow$ become $\lor$,$\land$ and $\rightarrow$ respectively. But in this case you're dealing with a propositional logic, not a predicative one.