Reading about Univalent Foundations

Voevodsky’s proposal to the NSF and IAS(2010) consists of 13 pages. The slides from his talk in Goteborg (Sept 2011) are easier to understand. Both can be found  in the univalent foundations page.

There is also the page on Homotopy Type Theory tout court, with more information on other researchers' views. 

Homotopy Type Theory refers to a new interpretation of Martin-Löf’s system of intensional, constructive type theory into abstract homotopy theory.  Propositional equality is interpreted as homotopy and type isomorphism as homotopy equivalence. Logical constructions in type theory then correspond to homotopy-invariant constructions on spaces, while theorems and even proofs in the logical system inherit a homotopical meaning. Slides from Thierry Coquand following this kind of explanation in Oberwolfach are  linked from here.

The original work that is the basis of this stuff is the groupoid model of Martin-Loeuf's CTT by Thomas Streicher and Martin Hofmann, here.

The broad motivation behind univalent foundations is a desire to have a system in which mathematics can be formalised in a manner which is as natural as possible. Whilst it is possible to encode all of mathematics into Zermelo-Fraenkel set theory, the manner in which this is done is frequently ugly; worse, when one does so, there remain many statements of ZF which are mathematically meaningless. This problem becomes particularly pressing in attempting a computer formalisation of mathematics; in the standard foundations, to write down in full even the most basic definitions—of isomorphism between sets, or of group structure on a set—requires many pages of symbols.

Univalent foundations seeks to improve on this situation by providing a system, based on Martin-Loef’s dependent type theory, whose syntax is tightly wedded to the intended semantical interpretation in the world of everyday mathematics. In particular, it allows the direct formalisation
of the world of homotopy types; indeed, these are the basic entities dealt with.

Constructing a model of the univalent foundations in the category of simplicial sets Voevodsky shows the consistency of these foundations relative to the usual ones. But this is just a first sanity check, if the new foundations are to be used, what do we need to know about them?

Some highlights of the Voevodsky proposal (first pages only).

1. We're close to "a new era which will be characterized by the widespread use of automated tools for proof construction and verification". yeah.
2. V came up with "a new semantics for dependent type theories - the class of formal systems which are widely used in the theory of programming languages"    Cool about the new semantics. I wish the bit about 'widely used' was true.
3.  "univalent semantics" interprets types as homotopy types. "the key property of the univalent interpretation is that it satisfies the univalence axiom a new axiom which makes it possible to automatically transport constructions and proofs between types which are connected by appropriately defined weak equivalences."    ok, need definitions...
4.  The key features of  "univalent foundations":

•  axiomatization of n-categorical structure
•  language is dependent type theory
•  based on homotopy types, not sets
•  both constructive and non-constructive maths