7
$\begingroup$

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.
$\endgroup$
  • 2
    $\begingroup$ I don't see the connection between the Univalent Foundations Program and the Simple Agda proof. $\endgroup$ – Dave Clarke Dec 15 '13 at 9:43
  • $\begingroup$ My question was getting at what 'their Agda/Coq proofs' added up to. I presented a simple example of another well written Agda proof that didn't claim to be the foundations of mathematics. $\endgroup$ – hawkeye Dec 15 '13 at 10:46
  • 1
    $\begingroup$ Giant apples vs small oranges. $\endgroup$ – Dave Clarke Dec 15 '13 at 11:12
7
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ So you're essentially saying they spent some time doing the building blocks - but they haven't added up to anything of consequence yet. $\endgroup$ – hawkeye Dec 15 '13 at 10:48
  • 2
    $\begingroup$ It really depends on what you mean by "consequence". Some really non-trivial theorems (like $\pi_1(S^1)=\mathbb{Z}$) have been formally proven in this framework, with the advantage that both the expression and proof are relatively simple with this new formulation. The blog has many discussions of such results. homotopytypetheory.org/blog $\endgroup$ – cody Dec 18 '13 at 13:23
  • $\begingroup$ what do you mean by "synthetic homotopy theory"? $\endgroup$ – jonaprieto Jan 18 '18 at 15:03
  • 2
    $\begingroup$ @jonaprieto Synthetic homotopy theory means that we deduce theorems about the homotopy types of spaces using only model-invariant properties of those types and not specific models, like CW-complexes, topological spaces or simplicial sets. This is analogous to e.g. synthetic Euclidean geometry, which proves theorems by directly manipulating with curves using geometric constructions, as opposed to the analytic approach, which chooses one of the non-unique encodings of those curves as solutions to equations and manipulates those representing equations. $\endgroup$ – Anton Fetisov Feb 14 '18 at 2:30
  • $\begingroup$ Similarly, in synthetic homotopy theory we may talk about contractibility of certain spaces, about path fibrations and homotopies, but we cannot e.g. talk about the set of points of some space, distinguish homotopy equivalent spaces, like $\mathbb R^n$ for various $n$, or use homotopy non-invariant properties, like the definition of a circle as a subset in $\mathbb R^2$ (since the plane and all its subsets are contractible). $\endgroup$ – Anton Fetisov Feb 14 '18 at 2:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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