Explore
Homotopy Type Theory: Univalent Foundations of Mathematics
7 Ungluers have
Faved this Work
Login to Fave
Homotopy type theory is a new branch of mathematics that combines
aspects of several different fields in a surprising way. It is based on a
recently discovered connection between homotopy theory and type theory.
It touches on topics as seemingly distant as the homotopy groups of
spheres, the algorithms for type checking, and the definition of weak
∞-groupoids. Homotopy type theory offers a new “univalent” foundation of
mathematics, in which a central role is played by Voevodsky’s
univalence axiom and higher inductive types. The present book is
intended as a first systematic exposition of the basics of univalent
foundations, and a collection of examples of this new style of reasoning
— but without requiring the reader to know or learn any formal logic,
or to use any computer proof assistant. We believe that univalent
foundations will eventually become a viable alternative to set theory as
the “implicit foundation” for the unformalized mathematics done by most
mathematicians.
This is the first (and to date, only) edition of the book. For the benefit of all readers, the available PDF and printed copies are being updated on a rolling basis with minor corrections and clarifications as we receive them. Every copy has a version marker that can be found on the title page and is of the form “first-edition-XX-gYYYYYYY”, where XX is a natural number and YYYYYYY is the git commit hash that uniquely identifies the exact version. Higher values of XX indicate more recent copies. This update was on August 30, 2015 and its version marker is "first-edition-967-g0b0914e". The most recent builds, as well as PDFs with other form factors are available on GitHub. Printed copies may be purchased via the books homepage.
This is the first (and to date, only) edition of the book. For the benefit of all readers, the available PDF and printed copies are being updated on a rolling basis with minor corrections and clarifications as we receive them. Every copy has a version marker that can be found on the title page and is of the form “first-edition-XX-gYYYYYYY”, where XX is a natural number and YYYYYYY is the git commit hash that uniquely identifies the exact version. Higher values of XX indicate more recent copies. This update was on August 30, 2015 and its version marker is "first-edition-967-g0b0914e". The most recent builds, as well as PDFs with other form factors are available on GitHub. Printed copies may be purchased via the books homepage.
Why read this book? Have your say.
You must be logged in to comment.
mohansigma
Rights Information
Are you the author or publisher of this work? If so, you can claim it as yours by registering as an Unglue.it rights holder.Downloads
This work has been downloaded 745 times via unglue.it ebook links.
- 516 - pdf (CC BY-SA) at Internet Archive.
Keywords
- Mathematical analysis
- Mathematics
- Nonfiction
Links
web: http://homotopytypetheory.org/book/Editions