Homotopy Type Theory:
Univalent Foundations of Mathematics
The Univalent Foundations Program
Institute for Advanced Study
- Buy a hardcover copy for $21.00.
[620 pages, 6″ × 9″ size, hardcover, first-edition-1277-g3274cb3] - Buy a paperback copy for $14.00.
[620 pages, 6″ × 9″ size, paperback, first-edition-1277-g3274cb3] - Download PDF for on-screen viewing.
[490+ pages, letter size, in color, with color links] - Download PDF for e-books.
[622+ pages, size 6″ × 9″, small margins, black and white] - Download PDF for printing on letter paper and color cover.
[492+ pages, letter size, black and white, separate color cover] - Download PDF for printing on A4 paper and color cover.
[454+ pages, A4 size, black and white, separate color cover] - Download errata for previous versions (see below).
- Nightly builds page (with direct links to the most recent versions; the above “released” versions are redirects to these)
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.
Feedback
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 github.com 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!)
Updates
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 date and version marker of the most recent update can be found on the nightly builds page.
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:
@Book{hottbook,
author = {The {Univalent Foundations Program}},
title = {Homotopy Type Theory: Univalent Foundations of Mathematics},
publisher = {\url{https://homotopytypetheory.org/book}},
address = {Institute for Advanced Study},
year = 2013}
Homotopy Type Theory 
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.
This is now available on google books at http://books.google.com/books?id=LkDUKMv3yp0C. Perhaps the list should be updated?
Google books doesn’t know about the the ebook.
Internet Archive does, and has conversions to other formats: https://archive.org/details/HottOnline
Unglue.it has added it to their list of CC licensed ebooks: https://unglue.it/work/128678/
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.
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.
There link to the paperback version seems dead right now.
Yeah, lulu changed their software and broke the cover image. Andrej is working on it (go Andrej!).
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?
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.
Thanks for using Lulu and not expensive publishers like Springer-Verlag.
Thanks
A lot
For the Creative Commons licence
A for the content
And for the content 🙂
I am struggling with the exercises even in the first chapter, and when I am finished I am not sure if I have the right answer. Would it be possible to publish some of the solutions to the exercises?
A few solutions (basically, those that anyone happened to be motivated to write up) are available in the file exercise_solutions.tex in the github repository.
How have you published this?
We posted the PDF online here, and we made a Lulu account so that people can buy a printed version. It took a bit of effort to get the formatting correct for Lulu, but overall it wasn’t very hard. Is that what you mean?
Well mainly how you managed to print and publish a copy that you could sell while also giving it away for free. I wouldn’t have thought most publishers would allow that – how did you manage to get the physical copies printed?
Ah, I see now, Lulu seems like a good service.
The book is beautifully typeset! It would be instructive to see the latex (or context?) preamble for this book.
You can find it in the github repository (linked above).
Hi, me again. I’m currently just about to enter my first year of an undergraduate degree, but I’ve been reading ahead for about a year now, and so have a decent grasp at basic abstract algebra (up to Galois), very basic analysis, linear algebra, number theory, and axiomatic set theory (not much, I know, but there’s only so much one can do while still doing A-levels). I started learning about axiomatic set theory (specifically the book on ZFC by P. Suppes) because I really like knowing at least roughly the logical path from the basic assumptions to what I’m currently learning. I feel it helps my understanding somewhat.
The problem I found was that, in fact, ZFC was not really practiced in any of my other books – for example they write that N is a subset of Q, or that every field is a subset of its polynomial ring, in my Abstract Algebra book. This had me looking for a more suitable foundation, and after having a look at ETCS as well as some non-ETCS category theory I eventually stumbled here. Exams and so on distracted me for a bit, until now.
Given my background, do you think I’d be able to get through this book? What kind of a level of mathematical maturity is assumed? More to the point, is it worth me trying to learn this? I have this niggling fear that if I learn from this book and then come to think in terms of types and write as such I’ll find it nearly impossible to fit in new information without having to file it into ‘Non-Hott’ and ‘Hott’ mathematics. I’m somewhat afraid that it won’t be possible for me to complete a problem sheet, for example, while using HoTT, because it will seem like nonsense from the point of view of my professors.
Are these fears unfounded? Can I learn HoTT and work in HoTT while still keeping recognisable notational conventions and thought patterns? How much does using HoTT as my foundation affect my mathematical practise? Can I just avoid some of the more idiosyncratic parts of it when I need to?
You should post to the HoTT-Cafe google group.
Notify me of new posts via email.
PDF download links give 404.
Here are working links: https://github.com/HoTT/book/wiki/Nightly-Builds
They work for me right now. Occasionally the server that hosts the redirects goes down, but it usually comes back up quickly. The nightly build page is also linked from up top.
The current link to the PDF yields a 404 error:
Click to access hott-online-1194-g81c15ec.pdf
A bit of rooting around yields the most current version to be located here instead:
Click to access hott-online-1198-geeccc59.pdf
Note: All of the other free links are also currently down, with the exception of the nightly github page, which contains the correct links to all of them.
Thanks for reporting, I think maybe now I see what the problem is; will try to fix.
So you link to http://saunders.phil.cmu.edu/book/* that redirects to nightly builds.
Isn’t it better to link to webpages hosted on GitHub pages that redirects to nightly builds using javascript:
https://www.w3schools.com/howto/howto_js_redirect_webpage.asp
and using Travis to automatically update the redirection with each build?
If you’d like to submit a pull request at the book repository, feel free. I’ve never learned how to configure Travis myself.
I am just student trying to learn HoTT via this book, could someone please tell me where to post questions regarding understanding the book? I can see the mailing list on https://homotopytypetheory.org/links/ but I cannot go into the chat room, it tells me:
##hott Cannot join channel (+r) – you need to be identified with services
See https://freenode.net/kb/answer/registration
The following concern is in the interest of clearing up notational confusion and I hope is not viewed as nit-picky. In Exercise 1.1 we are asked to define composition of f : A -> B and g : B -> C, where the composition is denoted g • f : A -> C. Now, in Lemme 2.12 composition of identity paths are addressed while finding a function (x = y) -> (y = z) -> (x = z). We have p : x = y and q : y = z and it is stated that p • q : x = z. But in light of the homotopy notion of equalities as paths this seems overall an inconsistent choice of notation. Because p is a path from x to y and q a path from y to z. In my opinion q • p : x = z is a more consistent notation. Because the composition in truth takes x and feeds it into a path to y (via p) and then feeds y into a path to z (via q.)
My mathematical maturity is at most on undergraduate level. I wish and have tried to study and comprehend this book. But as I try to study, I find that I always feel the need of some prerequisites to comprehend this book, and the problem is that I don’t know how to figure out what kinds of prerequisites are needed and which prerequisites to start. Does anyone have similar experiences when facing this book? Can anyone discuss with me to help me know where to start and give some study advice on comprehending this book?
The book assumes familiarity with basic logic and topology at a level that would usually be taught in an advanced undergraduate or beginning graduate course.
Thanks for the reply!
By “topology at a level that would usually be taught in an advanced undergraduate or beginning graduate course” do you mean the level the same as “Munkres’ Topology”?
Actually I haven’t fully studied a text on axiomatic set thery or mathematical logic or type theory or homotopy theory or category theory. But HoTT is still appealing to me. So which prerequisite subject(s) is/are recommended to get familiar with firstly?
I know a young mathematician named Evan Chen, who is currently a math PhD student at MIT, providing abundent free study materials on higher mathematics on his website, which he called “The Napkin project” ( https://web.evanchen.cc/napkin.html ) . I am guessing, can Napkin be used as a prerequisite to HoTT?
A better place for such a discussion would be the mailing lists on the Links page.
Could you please also add the EPUB version to the versions above?
Thank you very much.
What epub version?
I placed an order for the paperback copy 14 days ago (28 December 2020) and received a copy with version `first-edition-1174-g29279f5`, corresponding I guess to [this commit](https://github.com/HoTT/book/commit/29279f5d00f1fdb013d5c7fbe804b49cb25e61b1) from 19 April 2018. The online pdfs are currently up-to-date with the [most recent commit](https://github.com/HoTT/book/commit/d98a32f95e1858e1b619cae02f643334f2ce9022) (version `first-edition-1274-gd98a32f`).
I don’t see anything on Lulu mentioning which version is currently being shipped. Can this please be updated, and maybe we can have the current version/date be part of the book’s description on Lulu so that buyers can cross-reference before purchase?
Thank you!
Thanks for the heads-up, and sorry about this! The lulu version has now been updated (unfortunately this has to be done manually), and the links above now include the information of which version is available from lulu. Thanks Andrej! If the lulu version gets significantly behind the online version again, anyone can feel free to post a comment here requesting that it be updated.
I wonder if the Lulu API (https://developers.lulu.com/home) allows automatic updating, or if there’s a way to script that process…
I expect anyone who wants to look into that would be more than welcome! Talk to Andrej Bauer about our lulu setup.
I Bought $21.00 hard copy from lulu one month now, I still have not received it yet, Lulu support in not responding, please consider change your hardcovers Provider
Got the book after 20 days, shipping issue during lockdown
Thanks for following up.
all pdf download links yield 404 😦
they seem to be working for me (now).
Could you make an epub please? Or an HTML file?
There was some abortive work on this before, but it didn’t go anywhere. I don’t think any of the original authors have the time to work on it right now. If it’s going to happen, someone else who cares about it will have to step up to take the lead.
Have you considered submitting your textbook to the AIM for inclusion in their Open Textbook Initiative? I read through the evaluation criteria and came to the conclusion that this book would fit right smack in their. Maybe under the Logic Section? Link to the AIM site: https://aimath.org/textbooks/
How do I order this book in Canada?
the error pdf is cut
From the Lulu links above, it looks like the physical version is using this commit from a little over 3 years ago. Any chance it could be updated?