>>So I wonder what he thinks of this new univalent foundation. The Homotopy Type Theory (HoTT) book[1] puts forth a possible interpretation of Conway's thought

>>So I wonder what he thinks of this new univalent foundation. The Homotopy Type Theory (HoTT) book[1] puts forth a possible interpretation of Conway's thoughts about univalent foundations in section 11.6 (look at the bottom of the page for the following very selective and paraphrased quote): "[...] Conway's point was not to complain about ZF in particular, but to argue against all foundational theories at once [...] One might respond that, in fact, univalent foundations is not one of the "standard foundational theories" which Conway had in mind, but rather the metatheory in which we may express our ability to create new theories, and about which we may prove Conway's metatheorem."[2] [1] http://homotopytypetheory.org/book/ http://homotopytypetheory.org/book/ [2] http://www.math.ntnu.no/~stacey/documents/HoTT-online/main126.xhtml http://www.math.ntnu.no/~stacey/documents/HoTT-online/main12... EDIT: I forgot to mention that Voevodsky's definition of "Univalent Foundations" seems to be used interchangeably with the term "Homotopy Type Theory", but in Voevodsky's mind there is a sharp distinction[3]. Voevodsky tried to make this clear in an HoTT Google Groups email thread with the following statement: "HoTT is the study of the type-theoretic approach to the meta-theory of the Univalent Foundations."[4] [3] http://en.wikipedia.org/wiki/Homotopy_type_theory#Univalent_foundations http://en.wikipedia.org/wiki/Homotopy_type_theory#Univalent_... [4] https://groups.google.com/forum/#!topic/homotopytypetheory/zEixM1M3ZDQ%5B1-25%5D https://groups.google.com/forum/#!topic/homotopytypetheory/z...