Fwd: The HoTT Book | Homotopy Type Theory

[Owen Densmore]

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

[Barry MacKichan]

FWIW, Voevodsky won the Fields medal (aka the 'Mathematician's Nobel) in 2002.

--Barry

On Sep 5, 2013, at 11:45 AM, Owen Densmore <[hidden email]> 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

[Roger Critchlow-2]

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 <[hidden email]> 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 <[hidden email]> 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

[Marcus G. Daniels]

Roger writes:

"Definitely worth a spin if you feel like taking on a new foundation of
mathematics that's less than a year old."

Or even if you are a programmer that wants to write better programs...
Several of those authors are involved in the development of new
dependently-typed languages like Agda.

Marcus

--------------------------------------------------------------------
mail2web.com – What can On Demand Business Solutions do for you?
http://link.mail2web.com/Business/SharePoint



============================================================
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