There is a lot about HoTT beyond the collaboration of a Fields Medal winner with other mathematicians, mediated through git, and producing an open access book in less than a year. I spent a few hours puzzling over it when it was released, but got distracted.
The core of HoTT is an executable version of mathematical proof. The book is an unpacking of things which have been demonstrated to be true but not completely understood even by the group who wrote the book, and a translation of the received foundations of mathematics into HoTT. A proof in HoTT is a construction of an exemplar of the truth asserted. There is no general existential assertion, only particulars. So you cannot assert the existence of a set of all sets which are not subsets of themselves and then proceed to confuse yourself with the consequential fallout, because that is not a "homotopy type" of which an example can be constructed. If HoTT works as anticipated then it becomes an alternative to set theory and logic as a foundation of mathematics. Definitely worth a spin if you feel like taking on a new foundation of mathematics that's less than a year old. -- rec -- On Fri, Sep 6, 2013 at 8:47 AM, MacKichan Barry < [email protected]> wrote: > FWIW, Voevodsky won the Fields medal (aka the 'Mathematician's Nobel) in > 2002. > --Barry > > On Sep 5, 2013, at 11:45 AM, Owen Densmore <[email protected]> wrote: > > Cool! "two dozen mathematicians who wrote a 600 page book in less than > half a year" > > http://homotopytypetheory.org/book/ > .. and its on GitHub! > > Interesting blog post on the process: > http://math.andrej.com/2013/06/20/the-hott-book/ > > -- Owen > > ============================================================ > FRIAM Applied Complexity Group listserv > Meets Fridays 9a-11:30 at cafe at St. John's College > to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com > > > > ============================================================ > FRIAM Applied Complexity Group listserv > Meets Fridays 9a-11:30 at cafe at St. John's College > to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com >
============================================================ FRIAM Applied Complexity Group listserv Meets Fridays 9a-11:30 at cafe at St. John's College to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com
