[Solved]: What were the research outcomes of the Univalent Foundations Program year (Homotopy Type Theory)

Problem Detail: 

The Institute for Advanced Study has had a year-long special program devoted to the Univalent Foundations Program.

At the end of this they have produced a book and a code repository.

At the end of this we see a blog entry in Scientific American claiming:

...it could provide a new, self-contained foundation for all of mathematics.

Now this is a bold claim. By contrast I can see humbler claims such as a simple proof in Agda that the sum of two odds is always an even.

My question is: What novel research did these guys actually produce at the end of the year? All the article indicates is that they wrote some code in Agda. Is it just that we have a new view of Martin-Löf type theory with some applications?

Assumptions

• I understand the broader ideas of Martin-Löf type theory as it relates to the isomorphism between Types and Proofs.

Asked By : hawkeye

Answered By : Ethan A. Kuefner

The book is itself representative of the research product of the program. The code that they wrote actually is mostly in Coq, to my knowledge, and certainly the development that accompanies the book was written in Coq.

Homotopy Type Theory itself essentially constitutes Martin-Löf, together with the univalence axiom, which essentially states that equivalent types are equal. The notion of equivalence comes from a view that establishes a connection between a synthetic homotopy theory and Martin-Löf type theory, hence the name. This axiom gives way to a powerful type theory that the book shows is capable of reasoning about a lot of important existing foundational mathematics.

In fact, part 2 of the book comprises developments of a more traditional, topologically-motivated version of homotopy theory, set theory, category theory, and a nice constructive presentation of the real numbers. I have not explored the Coq code that much yet, but my understanding is that all of these presentations are accompanied by corresponding Coq source. Since we can formulate all of these important foundations entirely within homotopy type theory, the hypothesis that it might be an important foundation for mathematics going forward makes sense. The idea is that mathematicians will be able to extend these seminal developments towards more results in fields like algebra, topology, and analysis.

Inasmuch as homotopy type theory pertains to being able to do mathematics in Coq via the Curry-Howard correspondence, you can think of homotopy type theory as corresponding to a more powerful instance of Curry-Howard. The most exciting contribution of this work is really that it gives mathematicians language for speaking about mathematics in terms of type theory, and the idea is that this should enable on the one hand, more mathematics being accompanied by mechanized proofs in provers like Coq, as well as computer proofs that correspond more closely to their plain English equivalents. Anyone who has used Coq will tell you that the proofs that you produce often don't end up looking much like equivalent plain-English proofs at all.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/19001