Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

June 20, 2013

The HoTT Book

Posted by Mike Shulman

Many of you have heard murmurings about this book for several months now. I’m happy to report that it’s now out!

At the link you can download electronic versions for screen, ereader, or printer, and order paperback and hardback bound copies at cost from The book is CC BY-SA licensed, which in particular means it will always be freely available.

So where did this book come from? As it says in the preface, we did not set out to write a book. It all began last fall when Peter Aczel proposed to start a working group on informal type theory. I’ve mentioned this idea before: the point is that type theory is usually a very formalized system (even to the point of being implemented in computer proof assistants), whereas mathematicians are accustomed to speak instead in informal “mathematical English” (or French, Russian, etc.). The usual implicit assumption is that mathematical English could be formalized in a set-theoretic foundation such as ZFC, and this requires various conventions on what we can and can’t say in mathematical English. The goal of informal type theory is to develop conventions for a version of mathematical English whose “implicit underlying foundation” is instead type theory — specifically, homotopy type theory.

The informal type theory working group met a few times and had some good arguments, but after a while we realized we needed something to focus our discussions. So we began a project of writing down some of our recent results in homotopy type theory in informal mathematical English, and to give the project some coherence (and an incentive to settle on uniform conventions) we thought of what we were writing as chapters in a book. Eventually we noticed that an actual book was starting to take shape, and that such a book could be extremely valuable, both as a “report” on the progress of the special year, and as an introduction for newcomers to the field not requiring them to know or learn any formalized type theory. Hence, the HoTT Book.

Due to its origins, some of the material in the book has already been published elsewhere, while some of it was “common knowledge” in the HoTT community before the IAS program but may not have been written down anywhere (except perhaps in a computer proof assistant). On the other hand, a good amount of the material is new, and may yet be published elsewhere by the people responsible for it (or, in a couple of cases, was published elsewhere during the writing of the book). Making the latter possible is one reason we chose a permissive license.

I want to emphasize that the book is specifically intended to be readable by mathematicians who do not know any type theory, any computer science — or even any homotopy theory! If you are reading this blog, chances are you are in the intended audience. So you should go have a look!

That said, type theory can be very difficult to explain to a mathematical audience. We did our best to give a “working mathematician’s” introduction to type theory in the first couple of chapters of the book, but I am certain that for many readers, it will still be confusing. We want your feedback! We will be releasing “bug fix” enhancements on a rolling basis based on reader feedback, and eventually there may be an official Second Edition. Tell us what is confusing, where you got lost, where there are typos, where the math is just wrong, etc. etc. We’d prefer if you open a github issue on the book project, but it’s also fine to just put a comment on the HoTT blog. And of course we’re very happy to discuss what’s in the book as well.

To whet your appetite, I will end this post with an annotated table of contents of the book.

  1. Type theory. This chapter is a brief introduction to dependent type theory without any homotopical features. It begins with an overview of how type theory differs from set theory as a foundation for mathematics (influenced by discussions such as this and this), and then introduces concepts like type universes, dependent types (which in the book we call type families), λ\lambda-abstraction, induction and recursion, and propositions-as-types. It also establishes notation and conventions for the rest of the book.

  2. Homotopy type theory. This chapter introduces the homotopical viewpoint on type theory, where “proofs of equality” are regarded as paths in a space or equivalences in an \infty-groupoid. It also adds to type theory the function extensionality and univalence axioms — of which the latter, due to Voevodsky, is one of the main innovations of homotopy type theory. Finally, it explains how to “compute” with paths in various kinds of types, and proves that many types have universal properties.

  3. Sets and logic. This chapter begins by defining a class of types called sets, which have no “higher homotopy” and hence behave basically like the sets in a (structural) set theory such as ETCS. Then it discusses various aspects of logic in homotopy type theory, introducing “mere propositions” ((1)(-1)-truncated types) and the corresponding propositional truncation, and statements of the law of excluded middle, the axiom of choice, and the propositional resizing axiom (none of which we need to use very much in the rest of the book).

  4. Equivalences. This chapter studies several equivalent ways to define the notion of “equivalence of types” in a well-behaved way. It also proves some useful general facts about equivalences, and that the univalence axiom implies the function extensionality axiom.

  5. Induction. This chapter adds to our type theory the general notion of inductive type, which includes most of the type forming operations from chapter 1 as special cases. It proves (by a sufficiently general example, namely Martin-Löf’s WW-types) that inductive types can equivalently be characterized as homotopy-initial algebras for polynomial endofunctors, and describes briefly several generalizations of inductive types such as inductive families, inductive-inductive types, and inductive-recursive types.

  6. Higher inductive types. Next to univalence, HITs are the most important new aspect of homotopy type theory, allowing us to construct higher-dimensional “spaces” such as spheres and tori; perform homotopical constructions such as suspensions, truncations, localizations, and homotopy colimits; and generate free algebraic structures of all sorts. This chapter introduces them by way of many examples.

  7. Homotopy nn-types. This chapter studies the general notion of nn-type, which includes sets (0-types), mere propositions ((1)(-1)-types), and contractible types ((2)(-2)-types) as special cases. It defines the nn-truncation operation using higher inductive types, and constructs the (nn-connected, nn-truncated) orthogonal factorization system on types. It ends with a brief discussion of more general “modalities”.

  8. Homotopy theory. Here we finally start to get the payoff. Combining higher inductive types with univalence, we calculate π 1(S 1)\pi_1(S^1), π n(S n)\pi_n(S^n), and π 3(S 2)\pi_3(S^2), construct long exact sequences and the Hopf fibration, and prove the Freudenthal suspension theorem and the van Kampen theorem. We also prove that Whitehead’s theorem holds for nn-types for any finite nn, and observe that its general form can be regarded as a foundational axiom (“Whitehead’s principle”) akin to excluded middle or choice. This chapter incorporates a lot of new work that was done this past winter and spring.

  9. Category theory. I blogged about the contents of this chapter already. The basic idea is that if we define “categories” appropriately, requiring them to satisfy a “local” version of the univalence axiom, then all proofs and constructions will automatically be invariant under isomorphism of objects in a category and under equivalence of categories. In particular, equivalent categories become equal.

  10. Set theory. This chapter begins by proving that the “sets” (as defined in chapter 3) do in fact satisfy the axioms of ETCS (or a constructive version thereof, depending on whether we assume excluded middle and choice). Then it studies a few topics from traditional “set theory”, such as cardinal and ordinal numbers, finding that they behave mostly like their classical versions, but are slightly improved by univalence. Finally, it constructs a model of ZF-style set theory inside homotopy type theory, using a higher inductive type to model the cumulative hierarchy.

  11. Real numbers. This chapter explores two definitions of the real numbers. First there are the Dedekind reals, which behave just as expected (modulo issues of constructivity and predicativity). Then there are the Cauchy reals, for which we can use a higher inductive-inductive type to improve on the usual constructive treatment. If we assume excluded middle, then both definitions agree and behave like the real numbers we are all familiar with. It ends by sketching another higher inductive-inductive definition: Conway’s surreal numbers.

For more blogging about the HoTT Book, see the official announcement post by Steve Awodey, which discusses the paradigm of “unformalization”, and this post by Andrej Bauer, which discusses the socio-technological aspects of writing the book (which was a new and fascinating experience).

Posted at June 20, 2013 7:30 PM UTC

TrackBack URL for this Entry:

50 Comments & 2 Trackbacks

Re: The HoTT Book

Wow, impressive! I just placed my order. PDF is all very well, but for something this size, I want an actual book book.

As I’ve probably said before, I very much like the idea of informal type theory. The syntax of the subject is such a barrier. Anyway, huge congratulations on getting this amazing thing done.

Posted by: Tom Leinster on June 20, 2013 10:50 PM | Permalink | Reply to this

Re: The HoTT Book

Great job, Mike (and others)! I’ve really been looking forward to this. One question: Are there any plans to create a central index of formalizations of theorems from the book in Coq/Agda? I know that more or less everything is available in (on?) GitHub, but as far as I can tell, there’s no way to directly find all formalizations of Theorem such-and-such from the book. The closest thing appears to be this wiki page, but it doesn’t include any theorem numbers from the book. I think it’d be really useful to be able to switch quickly between the book and the formalizations while reading.

Posted by: Evan Jenkins on June 20, 2013 11:05 PM | Permalink | Reply to this

Re: The HoTT Book

Good question! There was some discussion of creating such a thing, and some people started work on it, but I don’t know how far they got or whether they are planning to continue. I think mostly we decided to focus on finishing the book and then worry about supplementary material such as this. I don’t have the time or energy for it right now myself (for a variety of reasons), but I agree that it would be a useful thing to have.

Posted by: Mike Shulman on June 21, 2013 12:56 AM | Permalink | Reply to this

Re: The HoTT Book

Everything is set up for linking the HoTT book with the Coq formalization, Favonia and I worked on this. We just need some crowdsourcing to make it happen.

If you look at HoTT/HoTT you will find etc/ and contrib/HoTTBook.v. Both are amply documented. I’ll be happy to accept pull requests if anyone gets around to doing this.

Posted by: Andrej Bauer on June 21, 2013 10:58 AM | Permalink | Reply to this

Re: The HoTT Book

For Agda, sorry but we are heavily refactoring the whole library now. :O

Posted by: Favonia on June 21, 2013 9:00 PM | Permalink | Reply to this

Re: The HoTT Book

Two more blog posts about the book: Bob Harper and Carlo Angiuli.

Posted by: Mike Shulman on June 21, 2013 12:57 AM | Permalink | Reply to this

Re: The HoTT Book

I may have to read this book just for the last topic in the last chapter!

Posted by: Blake Stacey on June 21, 2013 5:25 AM | Permalink | Reply to this

Re: The HoTT Book

Fortunately for you, you don’t need to read the whole book to get to the last chapter. I forgot to mention this in the post, but the last four chapters are largely independent of each other, and they don’t all depend on everything in the first seven chapters either. Check out the section of the introduction called ‘how to read this book’.

Posted by: Mike Shulman on June 21, 2013 5:37 AM | Permalink | Reply to this

Re: The HoTT Book

Good to know—thanks!

Posted by: Blake Stacey on June 24, 2013 8:06 PM | Permalink | Reply to this

Re: The HoTT Book

This looks great! I plan to dig in – I’m hoping type theory will finally make sense to me after seeing this.

My only disappointment is that the book is rather lamely authored by “Univalent Foundations Program”. Could not a mysterious collective alter-ego be constructed, ala Nick Bourbaki?

Posted by: Charles Rezk on June 21, 2013 1:41 PM | Permalink | Reply to this

Re: The HoTT Book

that’s already been done.

Posted by: Nicolas Bourbaki on June 21, 2013 3:03 PM | Permalink | Reply to this

Re: The HoTT Book

It looks wonderful! Congratulations to all.

Posted by: John Huerta on June 21, 2013 3:17 PM | Permalink | Reply to this

Re: The HoTT Book

Trying to understand what this stuff is about… apologies that I don’t speak the language and will probably get the terminology wrong.

Fix a context consisting of some type variables and some terms belonging to types that one can construct from them.

From this data, I guess one can extract a category C whose objects are the types that we can construct, and where morphisms from A to B are occupants of the type [A -> B] modulo equivalence, where f and g are considered equivalent if the type [f = g] is occupied?

Is the idea that C should be the homotopy category of “the free abc on xyz” where “abc” = infty-categories with some additional structures, and “xyz” is something which depends on the context you started with?

Posted by: Jacob Lurie on June 22, 2013 12:24 AM | Permalink | Reply to this

Re: The HoTT Book

Yes, but its not really necessary to identify the function terms and pass to the homotopy category right from the start. You can just take the category of types and terms of function type (no identifications), together with all the higher identity terms, and this should be the free abc on xyz – at least that’s the idea. Then if you 0-truncate the Homs you get the homotopy 1-category. Showing that the first step is really the free abc is still work in progress, though.

Posted by: Steve Awodey on June 22, 2013 3:15 AM | Permalink | Reply to this

Re: The HoTT Book

To add a bit to what Steve said, what we do know is that the category of types and terms (technically, the terms are taken modulo judgmental equality) is the free efgh on xyz, where efgh is a special kind of category of fibrant objects, i.e. a certain kind of presentation of an \infty-category. Not every \infty-category can be presented by a category of this sort, but every locally cartesian closed, locally presentable one can be. Thus, since type theory gives us the free such, we get semantics of type theory in any such \infty-category via the unique map out of the free thing. But we don’t yet know that this free efgh actually presents the free abc.

(That’s for type theory without univalence. When we add the univalence axiom, it essentially restricts our known semantics to \infty-toposes. There are some coherence details yet to be worked out there in the case of general \infty-toposes, but I think they aren’t really of great importance; at worst, we’ll have to modify the type theory a bit.)

Unfortunately, no one can seem to agree on the exact definition of an efgh or what to call them. In this paper I called them “type-theoretic fibration categories”. André Joyal has a slightly different version that he calls “tribes”. I think Steve also has a slightly different version involving a free fibration construction. And they’re all adaptations/reformulations of the various kinds of categorical semantics of type theory that type theorists have studied for many years (as is the theorem about initiality of the syntactic category).

Posted by: Mike Shulman on June 22, 2013 6:19 AM | Permalink | Reply to this

Re: The HoTT Book


So, when you say that an efgh is a presentation of an \infty-category, what is the relationship between that \infty-category and the category of types and terms? (If the former is going to be locally presentable, it surely must have many more objects than the latter?)

Is there a 0-categorical version of this that I could keep in mind? (Where you are presenting some special class of posets, maybe locales, rather than \infty-categories?)

Posted by: Jacob Lurie on June 22, 2013 12:57 PM | Permalink | Reply to this

Re: The HoTT Book

The free \infty-category is not locally presentable — in fact, it’s small. It’s obtained from the category of types and terms in the usual way, with homotopies being maps into path objects, etc. We only use local presentability in going the other way, showing that an \infty-category can be presented by some efgh. Obviously not every \infty-category that can be presented by an efgh is locally presentable, but we don’t know a general method for constructing such presentations other than via model categories. (Probably we could also deal with any small locally cartesian closed \infty-category via its Yoneda embedding.)

The 0-categorical version is constructing the Lindenbaum-Tarski algebra of a propositional logic. From intuitionistic logic, you get Heyting algebras, which of course include locales. The Lindenbaum-Tarski algebra of a propositional intuitionistic theory is then the free Heyting algebra generated by that theory.

Posted by: Mike Shulman on June 22, 2013 7:04 PM | Permalink | Reply to this

Re: The HoTT Book

I see. So, is the idea that with univalence, you’re giving a presentation of free “elementary” \infty-topoi?

Is there a precise conjecture about what the “abc” should be? (Either with or without univalence?)

Posted by: Jacob Lurie on June 22, 2013 10:52 PM | Permalink | Reply to this

Re: The HoTT Book

Yes, exactly.

There is a precise conjecture that with only dependent function types and dependent pair types (including unit type) plus function extensionality, “abc” is just “locally cartesian closed \infty-category”. The meaning of some of the additional type constructors should be obvious, e.g. coproduct types should correspond to coproducts, the natural numbers type should correspond to a NNO, etc. The meaning of univalence is a little trickier, and I don’t know whether anyone has written down a precise conjecture, but it’s not hard to imagine roughly how it would look: for however many univalent universes there are, the \infty-category should have that many object classifiers. For general higher inductive types, things are even trickier, but one imagines some kind of statement about existence of free monads and colimits of monads.

Posted by: Mike Shulman on June 23, 2013 1:54 AM | Permalink | Reply to this

Re: The HoTT Book

yes, that’s definitely the idea. but again: it’s w.i.p., since, unfortunately, we still don’t know how to get from the syntactic category, which evidently has an \infty-category structure of some kind, to an actual quasicategory or similar. What we can do is make a finitely complete QMC and go from there.

Posted by: Steve Awodey on June 23, 2013 2:26 AM | Permalink | Reply to this

Re: The HoTT Book

actually, we can do more: Peter Lumsdaine showed in his thesis that the syntactic category is indeed a globular \infty-category, in the sense of Batanin. It’s the simplicial (,1)(\infty, 1)-structure that we don’t have yet.

Posted by: Steve Awodey on June 23, 2013 4:37 AM | Permalink | Reply to this

Re: The HoTT Book

There’s another way to get an \infty-category from the syntactic category: just do Dwyer-Kan localization at the equivalences of types. That gives a simplicially enriched category, and then we can take the coherent nerve to get a quasicategory. If we knew how to get between Batanin \infty-categories and simplicial-style ones, then we could ask whether this agreed with Peter’s construction.

Posted by: Mike Shulman on June 23, 2013 4:47 AM | Permalink | Reply to this

Re: The HoTT Book

right – Chris K. and I looked at this a bit. The “problem” with it is that it doesn’t make much use of all the higher paths that we already have. Another idea was to give each type a simplicial “framing”, using a system of n-fold Id-types, defined as HITs. This actually seemed more promising, but there were other problems – nothing insurmountable, but more work needs to be done.

Posted by: Steve Awodey on June 23, 2013 3:40 PM | Permalink | Reply to this

Re: The HoTT Book


I have one comment/question.

If we assume excluded middle, then both definitions agree and behave like the real numbers we are all familiar with.

Countable choice should also be enough to make them agree and then they should behave like Bishop's real numbers. Does HoTT have anything to say about the presentation axiom (CoSHEP)?

Posted by: Toby Bartels on June 22, 2013 1:06 AM | Permalink | Reply to this

Re: The HoTT Book

Indeed, countable choice also suffices. Both are mentioned in chapter 11; I just omitted countable choice in my summary for brevity.

Of course, the presentation axiom is a weak form of the axiom of choice, so some of the remarks about AC in chapter 3 will apply to it with modifications. In particular, there is a question of h-level restrictions: AC becomes inconsistent with univalence if you assert that all types are projective, so the proper version of AC is that all sets are projective. For the presentation axiom, we could ask that every type admit a surjection from a projective set, or from a projective type, or ask only that sets admit such surjections. We can also consider stronger or weaker forms of projectivity involving h-level restrictions or not, see e.g. Exercise 7.8. I don’t know whether there can be interesting projective types that are not sets. Finally, we could also ask that the surjection merely exist or purely exist. (For sets, AC implies that it purely exists, being the identity map.)

Note that the statement that every type admits a surjection from a set is consistent to assume, but seems not to be provable — one might consider it also a form of “presentation axiom”. It follows from the strong form of choice called AC ,1AC_{\infty,-1} in the book; see Exercises 7.8–7.9.

Posted by: Mike Shulman on June 22, 2013 6:32 AM | Permalink | Reply to this

Re: The HoTT Book

Indeed, countable choice also suffices.

It won't suffice to make ‘the real numbers we are all familiar with’, unless ‘we are all’ constructivists. But that's OK, the comment was just what made me think of the question, and your answers are interesting enough.

Posted by: Toby Bartels on June 24, 2013 5:59 AM | Permalink | Reply to this

Re: The HoTT Book

I asked:

Does HoTT have anything to say about the presentation axiom (CoSHEP)?

Now having read Chapter 11 of the HoTT book, I think that I have an answer! To wit: if you seem to need the presentation axiom, then maybe you're using the wrong set, and you should take advantage of HoTT's powerful higher inductive definitions to get the set that you really want. And that's exactly what the HoTT book does with the Cauchy real numbers.

Posted by: Toby Bartels on June 30, 2013 8:10 PM | Permalink | Reply to this

Re: The HoTT Book

That’s a good answer! Much better than mine.

It also ties nicely into something else I’ve been thinking about recently, namely homological algebra. Classical homological algebra depends on projective and/or injective resolutions, but those are a bit tricky to come by in the absence of some form of AC. The presentation axiom suffices for the existence of projective resolutions, although I don’t know how much traditional homological algebra can be done with the presentation axiom but without LEM. And the usual proof of the existence of injective resolutions uses full AC (in the form of Zorn’s lemma).

However, the “modern” perspective is that homological algebra is just the degenerate case of stable homotopy theory where the base ring spectrum is the Eilenberg–Mac Lane spectrum HRH R of some set-ring RR. And spectra are something we have at least a bit of a handle on in homotopy type theory.

Consider, for instance, the Ext-groups (of abelian groups, say, for simplicity). Classically, one motivation for these is that they quantify the non-exactness of Hom, in the sense that for any short exact sequence of abelian groups 0ABC0 0 \to A \to B \to C\to 0 and any abelian group MM, we have a long exact sequence 0Hom(M,A)Hom(M,B)Hom(M,C)Ext 1(M,A)Ext 1(M,B)Ext 1(M,C). 0 \to Hom(M,A) \to Hom(M,B) \to Hom(M,C) \to Ext^1(M,A) \to Ext^1(M,B) \to Ext^1(M,C) \to \cdots. Classically, this sequence (for abelian groups) also stops after Ext 1Ext^1. This appears to have to do with the fact that subgroups of free abelian groups are free, which is also unprovable constructively, so we might expect the sequence not to necessarily terminate without LEM. But without projective or injective resolutions, it’s not even clear how to construct it.

Now it’s not hard to show in HoTT, using the LES of a fibration, that any SES as above induces a fiber sequence of Eilenberg–Mac Lane types: K(A,n)K(B,n)K(C,n) K(A,n) \to K(B,n) \to K(C,n) for any nn. Moreover, these fit together into a fiber sequence of spectra: HAHBHC H A\to H B \to H C where HAH A is the spectrum with (HA) nK(A,n)(H A)_n \coloneqq K(A,n) and the standard equivalences K(A,n)=ΩK(A,n+1)K(A,n) = \Omega K(A,n+1). (In general, a spectrum in homotopy type theory is a sequence of types X nX_n and equivalences X n=ΩX n+1X_n = \Omega X_{n+1}.)

Now let Map(X,Y)Map(X,Y) denote the mapping spectrum between two spectra, defined by setting Map(X,Y) nMap(X,Y)_n to be the type of spectrum maps XΩ nYX \to \Omega^{-n} Y. (The unlooping of a spectrum is defined by (Ω 1Y) kY k+1(\Omega^{-1} Y)_k \coloneqq Y_{k+1}.) Then it shouldn’t be hard to show that there is an induced fiber sequence Map(HM,HA)Map(HM,HB)Map(HM,HC) Map(H M,H A) \to Map(H M, H B) \to Map(H M, H C) and therefore a LES of homotopy groups π 0Map(HM,HA)π 0Map(HM,HB)π 0Map(HM,HC)π 1Map(HM,HA). \cdots \to \pi_0 Map(H M,H A) \to \pi_0 Map(H M, H B) \to \pi_0 Map(H M, H C) \to \pi_{-1} Map(H M,H A) \to \cdots. (The homotopy groups of a spectrum XX are defined by π nX=π n+kX k\pi_n X = \pi_{n+k} X_k for any kk such that n+k0n+k\ge 0.)

Now it ought to be provable that for any abelian groups MM and NN, we have Map(HM,HN) 0=Hom(M,N)Map(H M,H N)_0 = Hom(M,N). This is just the type of spectrum maps HMHNH M\to H N, i.e. functions K(M,0)=MN=K(N,0)K(M,0) = M \to N = K(N,0) equipped with all compatible deloopings — and the latter ought to exist uniquely just when the map MNM\to N is a group homomorphism. Thus, we have π 0Map(HM,HA)=Hom(M,A)\pi_0 Map(H M,H A) = Hom(M,A), and π nMap(HM,HA)=0\pi_n Map(H M,H A) = 0 for n>0n\gt 0, so the above LES reduces to 0Hom(M,A)Hom(M,B)Hom(M,C) π 1Map(HM,HA)π 1Map(HM,HB)π 1Map(HM,HC). \array{0 \to Hom(M,A) \to Hom(M,B) \to Hom(M,C) \to \\ \pi_{-1} Map(H M,H A) \to \pi_{-1} Map(H M,H B) \to \pi_{-1} Map(H M,H C) \to \cdots. } So clearly the negative homotopy groups of Map(HM,HN)Map(H M,H N) are functioning like some kind of Ext group. However, they are not quite the classical Ext groups: in EKMM they are called Ext over the sphere spectrum, Ext S n(HM,HN)π nMap(HM,HN)Ext^n_S(H M, H N) \coloneqq \pi_{-n} Map(H M,H N).

More generally, EKMM defined Ext over any E E_\infty ring spectrum RR of RR-module spectra MM and NN to be the homotopy groups of Map R(M,N)Map_R(M,N), and showed that we recover the classical Ext of abelian groups if we consider HMH M and HNH N as modules over HH \mathbb{Z}. Unfortunately, we don’t yet know how to define E E_\infty ring spectra and modules in homotopy type theory — it’s the same sort of problem as defining simplicial types, perhaps even harder — but if we did, then we would have a (presumably constructive) definition of Ext that retains at least some of the properties of the classical one, and reduces to the classical one if we assume AC.

But lacking that, we can still use Ext over the sphere spectrum. I think it’s not uncommon in stable homotopy theory to see this sort of thing: in some ways the integers are much more complicated than the sphere spectrum. Homotopy type theory seems to be telling us that constructive homological algebra is also much easier to do over the sphere spectrum than over the integers.

Posted by: Mike Shulman on July 1, 2013 5:05 AM | Permalink | Reply to this

Re: The HoTT Book

the integers are much more complicated than the sphere spectrum.

Do you think this is part of a general lesson that homotopy truncation (so here, the free abelian 1-group on one generator from the free abelian \infty-group on one generator) tends to make things more complicated?

So the cobordism hypothesis was easier after the move from nn-categories to (,n)(\infty, n)-categories. And, maybe, dependent sums are messier after (1)(-1)-truncation.

Posted by: David Corfield on July 2, 2013 12:27 PM | Permalink | Reply to this

Re: The HoTT Book

I think that’s not an unreasonable generalization, as long as you still include my qualifier “in some ways”. (-:

Posted by: Mike Shulman on July 3, 2013 1:46 PM | Permalink | Reply to this

Re: The HoTT Book

Another way to say that over \mathbb{Z} all suitable \mathbb{Z}-modules have vanishing Ext 2+nExt^{2+n} is that every such module has a Moore Space, for by the universal coefficient theorem,

(1)0Ext(R,G)H n(M n(R),G))Hom(H n(M n(R)),G)0 0 \to Ext ( R, G ) \to H^n ( M_n(R),G) ) \to Hom ( H_n(M_n(R)), G) \to 0

but for dimension reasons, H n(M n(R),G)H^n(M_n(R),G) is equivalent to Map(M n(R),K n(G))Map (M_n(R), K_n(G)), the latter being an hSet. So, whenever one has an M nM_n, one might choose to define ExtExt by this formula.

So… hmmm… one way to read the existence of short xx-ive resolutions is that, classically, every reasonable abelian group is the reduced homology of some space with only one interesting ordinary-homology group. Without enough Choice to presume these things generically, one can still (I think) highlight this class of spaces/abelian groups (though it seems much easier to say they have only two interesting co-homology groups, one torsion ( can we say “torsion”? ) and the other somethingelse, in adjacent dimensions); hearkening back to this note of yours, I’d of course like to muse (or ask) whether localizing at a small number of K(,n)K(\mathbb{Z},n)s does what I seem to think it ought to, and if it can be fit in the class of localizations you describe there. Or I might be talking nonsense, now. But if it weren’t nonsense, that would mean that one can still reflect a generic group into the good groups by a HIT, and say potentially interesting things about them.

As a last resort, since the not-quite-Moore-space of elements-mod-all-relations still has the right H nH_n (arguably), one might also choose to define ExtExt relative to that model, call it WW, as the kernel of the natural map H n(W,G)Hom(H n(W),G) H^n(W,G) \to Hom (H_n(W),G); this seems to return to the question of defining H n(W)H_n(W)… and is that natural map still surjective, constructively?

Posted by: Jesse C. McKeown on July 4, 2013 4:53 AM | Permalink | Reply to this

Re: The HoTT Book

I’m afraid you’ve totally lost me. What does the argument about Moore spaces and UCT have to do with Ext 2+nExt^{2+n}? What is an “xx-ive resolution”? What do you mean by “localizing at a small number of K(,n)K(\mathbb{Z},n)s” and what is it that you’d expect it to do? And what is the “not-quite-Moore-space” you mention?

Posted by: Mike Shulman on July 4, 2013 5:00 AM | Permalink | Reply to this

Re: The HoTT Book

The construction of a Moore space works (when it does) because one can choose a presentation of the given abelian group without syzygys; that is, the vanishing of the Ext 2(A,)Ext^2(A,-) (algebraic, choicy) is why one can have H n(M)AH_n(M) \sim A and H m>n(M)*H_{m\gt n}(M)\sim *; in a context where you don’t always have such minimal presentations, there is still a simply-connected space whose first interesting homology is H n(M)AH_{n}(M) \sim A; of course there are lots, but for instance,

HigherInductive presn (A) ( m : A -> A -> A) :=
  z : presn A m
| cell : A -> (idpath z) = (idpath z)
| rel (a a' :A) : cell a @ cell a' = cell (m a a') .

The difficulty (apart from saying what homology is) is that this probably has nontrivial homology in degree 3; the extra homology might be spanned by sphere classes (so that killing it is easy), and yet it might not. I’m pretty sure it is, choice-wise, because there should be a subfamily of rel that presents exactly what’s wanted, and one is only adding cells along nulhomotopic maps after that, but constructing such an argument returns to the original problem.

Localizing “at a space XX” (maybe I should say “over XX”) is short-hand for localizing at the maps ABA \to B that induce equivalences on Map(B,X)Map(A,X)Map (B,X)\to Map(A,X); or, at least, it should mean that. Again, I might be confused about something else, and thus writing nonsense around that point.

It seems I also have to correct myself: Map(M n(A),K(G,n))Map(M_n(A),K(G,n)) isn’t an hSet (unless, maybe, AA is torsion…), so take the set of components…

Posted by: Jesse C. McKeown on July 5, 2013 12:05 AM | Permalink | Reply to this

Re: The HoTT Book

Yes, certainly the usual construction of Moore spaces depends on having length-2 free resolutions of abelian groups. I think it also depends on the wedge axiom for homology holding for possibly-infinite wedges (that being the justification for using cellular homology), which may also be questionable constructively. (It might also be okay, though, I’m not sure — we do know that the infinite wedge axiom for cohomology is problematic in the absence of choice, but homology might be different.)

It sounded like you were also saying that the existence of a Moore space would conversely imply the vanishing of Ext 2+nExt^{2+n}; is that right? Why?

In case it matters, I don’t know whether we should expect the classical universal coefficient theorem to hold either — that might also depend on the vanishing of Ext 2+nExt^{2+n}. If we had a good theory of ring spectra, then I think we could construct a universal coefficient spectral sequence, but offhand it seems like it would only be the vanishing of Ext 2+nExt^{2+n} that would cause the UCSS to collapse into the classical UCT. (We’ve made a bit of progress on spectral sequences since the last time I mentioned them here — I think we can now construct the Atiyah-Hirzebruch SS for parametrized cohomology, and perhaps homology, and from that the corresponding Serre SS.)

Posted by: Mike Shulman on July 5, 2013 5:42 AM | Permalink | Reply to this

Re: The HoTT Book

The problem with localizing at the XX-equivalences is that there are too many of them. In classical homotopy theory, you have to play some cardinality game to get a small number of them that suffices to localize at, but I don’t know of any way to do something analogous in type theory.

Posted by: Mike Shulman on July 5, 2013 1:41 PM | Permalink | Reply to this
Read the post Homotopy Type Theory
Weblog: François G. Dorais
Excerpt: After a productive year at the Institute for Advanced Study, the Univalent Foundations Program has written a book on Homotopy Type Theory (HoTT). The foreword gives a succinct description of the purpose of this book: We did not set out to write a book....
Tracked: June 23, 2013 6:59 PM

Re: The HoTT Book

I’m enjoying picking through this, no matter how slow it goes. When I read your first post on HTT, I found myself in the odd position of thinking it was one of the most fascinating things I had ever read, the answer to all our dreams, foundations as it should be, the kind a working mathematician could support etc etc, while not understanding the meaning of a single sentence.

Anyway, here is a question. As I understand it, the proofs of any given proposition form a homotopy type, essentially by definition, which would be the answer to another old dream. Now is there any hope of identifying this homotopy type in any explicit sense? For example, what if P is the proposition 2+2=42+2=4 or quadratic reciprocity or…? Or is there some kind of uncomputability obstruction to determining it in general, as in Kolmogorov complexity? If so, are there any propositions for which something nontrivial (beyond it being empty or not) can be said about its space of proofs? Could it be that the space of proofs that the equation x 2+y 2=1x^2+y^2=1 has a real solution is a cicle? (Seems unlikely – why take the usual real topology on the space of solutions?) Are these questions hopelessly naive?

Posted by: James Borger on June 25, 2013 12:55 PM | Permalink | Reply to this

Re: The HoTT Book

Since natural numbers, integers, rational numbers, and real numbers form 0-types, any proposition of equality between them is a (-1)-type, i.e. contractible as soon as it is inhabited. So, for instance, 2+2=42+2=4 is contractible. For more complicated propositions, it depends on how you translate them into type theory. Many connectives and quantifiers, like implication, negation, conjunction, and universal quantification, preserve (-1)-types automatically, so any proposition constructed from those and equalities in 0-types will again be contractible as soon as it is inhabited. (Of course, a false proposition like 2+2=52+2=5 is always the empty type.)

However, the straightforward propositions-as-types translations of disjunction and existential quantification do not preserve (-1)-types, and so proofs of such propositions contain nontrivial “witnesses” of their truth. For instance, the proposition “there exist x,yx,y\in\mathbb{R} such that x 2+y 2=1x^2+y^2=1” is the set (0-type) of such pairs, i.e. the “circle” as a subset of \mathbb{R}. It has no topology, since like any proposition it is just a type, whereas a topological space is a structured type: a type equipped with a family of open sets. This is also not to be confused with the higher inductive “circle” S 1S^1 which is the \infty-groupoid freely generated by a point and a loop, and is not a set. In classical algebraic topology, the latter is the fundamental \infty-groupoid of the former (equipped with its subspace topology) — in homotopy type theory the relationship between them is less clear.

On the other hand, there are also “modified” versions of disjunction and existential quantification which destroy this extra information and result in (-1)-types. Sometimes this is what you want, e.g. these are necessary in order to state the law of excluded middle and the axiom of choice correctly. In the book, we write the modified existential quantifier as “there merely exists”; thus the type “there merely exist x,yx,y\in\mathbb{R} such that x 2+y 2=1x^2+y^2=1” is again contractible (since it is inhabited). These matters are discussed more thoroughly in chapter 3.

Posted by: Mike Shulman on June 25, 2013 6:47 PM | Permalink | Reply to this

Re: The HoTT Book

Ah, I see. Thanks for clearing that up.

Posted by: James Borger on June 26, 2013 9:33 AM | Permalink | Reply to this

Re: The HoTT Book

Hello Mr. Shulman and congratulations for the book.

I wanted to know what kind of background is needed to read (and understand) the book. Since you say it is, at some point in time, intended to serve as foundations for all of mathematics, I would expect the book to be pretty accessible, but I would like to clarify.


Posted by: Almeida on June 25, 2013 4:22 PM | Permalink | Reply to this

Re: The HoTT Book

I would like to say that the book should be readable by any mathematician. In practice, some prior exposure to category theory and homotopy theory is probably helpful, although we did try in particular to make it readable by computer scientists who we wouldn’t expect to have any knowledge of homotopy theory. Let us know if there are things you find confusing and help us make it more accessible!

Posted by: Mike Shulman on June 25, 2013 6:37 PM | Permalink | Reply to this

Re: The HoTT Book

“Popular” press coverage in New Scientist: “Mathematicians think like machines for perfect proofs”.

Of course it is New Scientist and they don’t mention the word “homotopy”. Their account is along the lines of “computer proof verification is good” and “in type theory proofs are types”, and you might get the impression that the IAS group invented this technique.

Posted by: RodMcGuire on June 25, 2013 4:55 PM | Permalink | Reply to this

Re: The HoTT Book


Posted by: Mike Shulman on June 25, 2013 6:33 PM | Permalink | Reply to this

Re: The HoTT Book

Posted by: Toby Bartels on June 25, 2013 8:38 PM | Permalink | Reply to this

Re: The HoTT Book

Would you say that this field is a continuation of Lawvere’s project through “Sets for Mathematics”?

Also, do you have any estimates on the progress being made for detailing the application of this field to parallel computing?

Posted by: Mark on July 5, 2013 8:44 AM | Permalink | Reply to this

Re: The HoTT Book

Well, sort of, in that Lawvere’s project is a “structural” foundation for mathematics, and so is type theory. But type theory was around before Lawvere, and it has a rather different style. And the new thing about homotopy type theory is the homotopy, not the type theory.

I know of no expected applications of this field to parallel computing.

Posted by: Mike Shulman on July 5, 2013 1:39 PM | Permalink | Reply to this

Re: The HoTT Book

Ok, I’m looking forward to reading the book :D

Haskell is becoming quite important for parallel computing. I wonder if this would even more significantly apply to a further developed Homotopy Type Theory. I believe so.

Posted by: Mark on July 6, 2013 8:07 AM | Permalink | Reply to this

Re: The HoTT Book

Hi Mike,

Homotopy theory (especially in its directed variants) does have significant applications to distributed and concurrent programming – see especially the work of Eric Goubault, for example his article Some Geometric Perspectives in Concurrency Theory.

The basic idea is that you can view the set of possible executions of a concurrent program as a space. Then, “bad” executions are forbidden areas in this space, and you can use things like homotopies to tell you if one good execution trace can be deformed (i.e., rescheduled) into another without running into the forbidden area. A variant of this idea netted Maurice Herlihy and Nir Shavit the 2004 Goedel Prize, where they proved that certain classes of distributed algorithm are impossible because their existence would imply homological invariants on the space of computations that don’t actually hold.

This is one of the reasons I found HTT so surprising: it’s really strange that homotopy theory has two apparently unrelated applications to computation!

Posted by: Neel Krishnaswami on July 8, 2013 10:23 AM | Permalink | Reply to this

Re: The HoTT Book

I thought the question was about applications of homotopy type theory to parallel computing. That’s what I’m not aware of. Although I suppose if people ever manage to come up with a directed version of homotopy type theory, then it might, conceivably, have similar uses to directed homotopy theory.

Personally, I don’t find it especially surprising that homotopy theory has more than one application to some other subject, any more than I would find it surprising that category theory does. I think it’s becoming increasingly clear that both of them are general organizing principles of mathematics.

Posted by: Mike Shulman on July 8, 2013 10:47 AM | Permalink | Reply to this
Read the post The HoTT Approach to Physics
Weblog: The n-Category Café
Excerpt: Urs's book published
Tracked: October 30, 2013 10:50 AM

Re: The HoTT Book

Hi, experts! I am a student reading this book and have some questions. It seems that there exists group where research level questions can be asked, but could someone please point out some active place where students trying to learn HoTT can ask questions?

One of my question is regarding page 281 of the book,where the book writes:

When xx varies along loop, we need to prove that:

refl baseap λx.x(loop)=ap λx.μ(x,base)(loop)refl baserefl_{base}\cdot ap_{\lambda x.x}(loop) = ap_{\lambda x.\mu(x,base)}(loop)\cdot refl_{base}

I tried manupulating the definition of “a path lying over sfloop\sf loop” by myself, but I cannot get there. In particular, I do not know where does the sfap\sf ap stuff comes from. Any help please? Thank you!

I also have a suggestion: On page 279, the book says:

a function z: a:Y+ZC(a)E totz : \sum_{a : Y + Z} C(a) \to E^{tot'}

where we are trying to use the flattening lemma. But in the statement of the flattening lemma, PiPi type is used rather then Σ\Sigma-type. I know it is not a typo but just the parsing of brankets, but the first time I read it I got very confused.

Thank you for any response

Posted by: Yiming Xu on March 14, 2019 12:21 PM | Permalink | Reply to this

Re: The HoTT Book

There is the hott-cafe google group.

(I answered your other two questions where you asked them at MSE and on github; I just wanted to record this answer here for future readers.)

Posted by: Mike Shulman on March 14, 2019 8:33 PM | Permalink | Reply to this

Post a New Comment