Has anyone read the book Homotopy type theory by Vladimir Voevodsky's group http://hottheory.files.wordpress.com/2013/03/hott-online.pdf ? Being a homotopy theorist myself, I'll try to read it, and I expect Rob Arthan will too. Tom Hales is listed as a contributor. I wonder if HOL could profit from any of their work, done in Coq. The only advantage that I know Coq has over HOL is type quantification, but HOL_omega also has this. Here's two nuggets from the intro which I find arresting and mystifying:
One problem in understanding type theory from a mathematical point of view, however, has always been that the basic concept of type is unlike that of set in ways that have been hard to make precise. We believe that the new idea of regarding types, not as strange sets (perhaps constructed without using classical logic), but as spaces, viewed from the perspective of homotopy theory, is a significant step forward. In particular, it solves the problem of understanding how the notion of equality of elements of a type differs from that of elements of a set. [...] consider first the basic concept of type theory, namely that the term a is of type A, which is written: a: A. This expression is traditionally thought of as akin to: ``a is an element of the set A.'' However, in homotopy type theory we think of it instead as: ``a is a point of the space A.'' Similarly, every function f : A ! B in type theory is regarded as a continuous map from the space A to the space B. We should stress that these ``spaces'' are treated purely homotopically, not topologically. For instance, there is no notion of ``open subset'' of a type or of ``convergence'' of a sequence of elements of a type. -- Best, Bill ------------------------------------------------------------------------------ This SF.net email is sponsored by Windows: Build for Windows Store. http://p.sf.net/sfu/windows-dev2dev _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
