The HoTT Book

Homotopy type theory: Univalent foundations of mathematics

Homotopy Type Theory:
Univalent Foundations of Mathematics
The Univalent Foundations Program
Institute for Advanced Study

About the book

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.


We have released the book under a permissive Creative Commons licence which allows everyone to participate and improve it. We would love to hear your comments, suggestions, and corrections. The best way to provide feedback is by creating an issue on the book repository. Git users may also fork the book and make pull requests. (Would you like to understand the last sentence? Learn git in 15 minutes!)


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. The most recent update was on March 6, 2014 and its version marker is “first-edition-611-ga1a258c”.

A list of corrections and clarifications that have been made so far (except for trivial formatting and spacing changes), along with the version marker in which they were first made, can be found in the errata file. While the page numbering may differ between copies with different version markers (and indeed, already differs between the letter/A4 and printed/ebook copies with the same version marker), we promise that the numbering of chapters, sections, theorems, and equations will remain constant, and no new mathematical content will be added, unless and until there is a second edition.

Citing the book

Since the book has no “publisher” in the traditional sense, it may not be obvious how to cite it. Here is one possible BibTeX entry:

  author =    {The {Univalent Foundations Program}},
  title =     {Homotopy Type Theory: Univalent Foundations of Mathematics},
  publisher = {\url{}},
  address =   {Institute for Advanced Study},
  year =      2013}

13 Responses to The HoTT Book

  1. I love how you have developed this book and for this reason I will buy a couple of copies.
    One for myself and one for someone I know.

  2. Jason Gross says:

    This is now available on google books at Perhaps the list should be updated?

  3. gluejar says:

    Google books doesn’t know about the the ebook.

    Internet Archive does, and has conversions to other formats: has added it to their list of CC licensed ebooks:

  4. sirinath says:

    When is the 2nd edition planed?

    Perhaps you could have 1st edition revision x merging the errata and format changes and perhaps minor additions. Waiting for the second edition may be a bit too long.

    • Mike Shulman says:

      As explained above under “Updates”, new versions of the first edition incorporating the errata are already being posted periodically. There are not yet any plans for a second edition.

  5. Marco says:

    There link to the paperback version seems dead right now.

    • Mike Shulman says:

      Yeah, lulu changed their software and broke the cover image. Andrej is working on it (go Andrej!).

      • Marco says:

        Now everything seems to work, the paperback version is back, great job. On the plus side i’ve noticed that this problem made the paperback version jump to “first-edition-667-g42d8475″ from the “-611″ of the pdf.
        Are the physical copy printed on demand from the last github’s sources or lulu has a stock of books which is updated with the new releases only when the remaining stock is low?

        • Mike Shulman says:

          Lulu prints on demand from the most recent version that’s been uploaded to their servers by us. We don’t do that for every github commit, of course. Usually we update the lulu and pdf versions together, but to fix this problem I guess Andrej had to upload a new version.

  6. Henry says:

    Thanks for using Lulu and not expensive publishers like Springer-Verlag.

  7. Sébastien Noton says:

    A lot
    For the Creative Commons licence
    A for the content

  8. Mike Shulman says:

    You’re right; Lulu seems to have changed the price on the paperback version without warning. In the US it’s currently $27.36, while the hardback version is still $21.83. I wonder what’s up.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s