I started reading it yesterday. It would be interesting to know if there is something like an "Univalence Axiom" for HOL and what its implications would be.
- Steven On 23 Jun 2013, at 04:27, Bill Richter wrote: > 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 ------------------------------------------------------------------------------ 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
