Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

I'm slowly grasping this, though the different formulations of type theory make it difficult.

In types can only be formed from *, i, and a->b when a and b are Types.

In (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?

share|cite|improve this question

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.

share|cite|improve this answer

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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.