I intend to read most of the book, possibly over a long period of time.
I would say that HOL is more grounded in set theory than type theory as
described in that book.
For example, the only judgements for HOL are of the form ps |- p (meaning p
is true, assuming ps), where p is a term of type bool.
I suppose there are also typing judgements like p : bool, but they don't
play a big role, and are treated as set-membership (which is just what the
first paragraph you quoted is trying to get away from).
In type theory, one would instead have judgements of the form a : p
(meaning that p is true) and, more interestingly, a == b.
As far as I can tell, it's quite a different way of looking at things.
On Sun, Jun 23, 2013 at 4:27 AM, Bill Richter <rich...@math.northwestern.edu
> 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
