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.

As aws pointed out above to extend the Curry-Howard isomorphism from propositional calculus to first order logic you need to extend your type theory to have dependents type, and if I'm not mistaken that is exactly what Martin Löf did: trying to extend Curry Howard isomorphism to predicates it created the his dependent type theory. In dependent type theory types are terms which can contain variables, since types correspond to propositions, is natural to reguard dependent types (i.e. types with variables) as dependent propositions (i.e. predicates).

If you're interested to go deep in such type theory I suggest to you to take a look this link and if you want to go even deeper I suggest to take a look to first chapter of Homotopy type theory book.

-