Almost at the top of the HoTT website are the words:
“Homotopy Type Theory refers to a new interpretation of Martin-Löf’s system of intensional, constructive type theory into abstract homotopy theory. ”
I think it is time to change these words into something that, at least, is not wrong.
Is there an interpretation of the MLTT into abstract homotopy theory? This would be the case if the 2007/2009 paper by Awodey and Warren defined, as it is often claimed today, an interpretation of MLTT into any Quillen model category.
However, that paper did not provide a construction of any interpretation of the MLTT . It outlined several ideas connecting the factorization axioms of Quillen model categories with the introduction and elimination rules for the identity types in the intensional Martin-Lof Type Theory. These ideas did not quite work out because the operations that one can define on a general Quillen model category do not satisfy the relations that are present in the MLTT .
Using an analogy from the representation theory, they noticed that there is a similarity between the generators of a certain “group” (MLTT) and operations in some categories. This would define representations of the group in such categories but it turned out that one of the most important relations in the group did not hold in the categories. The paper claimed (without a proof) that there is a new “group” that they called “a form of MLTT” that did not have this relation in its definition and stated the main result by saying that “there is an interpretation of a form of MLTT in any Quillen model category”.
The truth concerning the interpretations of MLTT into homotopy theory is different.
1. No interpretation of the MLTT into abstract homotopy theory (general Quillen model category) is known. Moreover, it is unreasonable to expect such an interpretation to exist if only because not every Quillen model category is locally cartesian closed. For example, the category of complexes of abelian groups is a Quillen model category that is not even cartesian closed.
2. The interpretation of the rules for identity types on model categories from a class that contains such important examples as topological spaces and simplicial sets was constructed in a 2008/2012 paper by Benno van den Berg and Richard Garner.
3. An interpretation of the rules for the dependent products, dependent sums, identity types and universes on the category of simplicial sets was constructed by Vladimir Voevodsky in 2009. The outline of the construction was made publicly available in the early 2010 and then written up in a 2012 paper by Chris Kapulkin, Peter LeFanu Lumsdaine and Vladimir Voevodsky.
There is a substantial difficulty in adding the rules for universes to the rules for the dependent products, dependent sums and identity types. These three groups of rules are independent from each other and can be studied separately. The rules for a universe connect the rules from these three groups to each other making it necessary to coordinate their interpretations.
4. An interpretation of the the same complement of rules on the categories of special diagrams of simplicial sets was constructed in 2012/13 by Michael Shulman. This was an important advance since it proved that an interpretation of these rules that satisfy the univalence axiom need not satisfy the excluded middle property.
The results mentioned above all provide interpretation of the various *rules* of the MLTT not of the MLTT itself.
MLTT is a syntactic object. Its definition starts with a specification of the “raw” syntax. Then one considers four sets that consist of all the sentences of four standard shapes that can be written in this syntax. Then, one takes the smallest quadruple of subsets of these sets that is closed under certain operations (the “rules”). Then one performs an extra step of taking the quotient of the two of the resulting sets by equivalences relations determined by the other two sets.
At this point one is left with two sets and a number of operations on these two sets. From this structure one constructs, using yet another procedure, a category. This category is called the syntactic category of the MLTT.
An interpretation of the MLTT is a functor from the syntactic category to another category.
There is a way to define interpretation of the rules of the MLTT on any category with some additional structure. It is a long standing conjecture that the syntactic category of the MLTT is the initial object among categories where the interpretation of the rules of the MLTT is given.
This conjecture is far from being proved.
In a remarkable 1991 book by Thomas Streicher proved an analog of this conjecture for a much more simple type theory called the Calculus of Constructions (not to be confused with the Calculus of Inductive Constructions!). At the moment it remains to be the only substantially non-trivial analog of this conjecture known.
Until this conjecture is proved, all of the previous papers can only claim interpretation of the rules of the MLTT not an interpretation of the MLTT. Proving this conjecture in a way that will also enable us to prove its analogs for yet more complex type theories such as the Calculus of Inductive Constructions and its extensions with new classes of inductive types is the most important, from my point of view, goal that needs to be achieved in the development of the UF and HoTT.
Homotopy Type Theory 
Does that imply, for example, that the introduction of the paper by Kapulkin, Lumsdaine, and Voevodsky, is written too optimistically, when it says such things as “we construct a model of type theory in the category sSet of simplicial sets, and show that it satisfies the Univalence Axiom” and “it also follows from this model that the Univalent Foundations are consistent, provided that the classical foundations we use are”?
Yes. We will re-write the introduction.
There is also the question of the difference between a “model” and an “interpretation”. An interpretation is a functor from the syntactic category. What a model is is not clearly defined. One can choose to call a category with families together with an interpretation of a given system of rules on it, a model of this system of the rules. Then a model of a set of rules does not define an interpretation of a type theory based on these rules until the initially conjecture for this particular type theory was proved.
No one has claimed that MLTT can be interpreted into “any QMC” — most of the result you mention use only a WFS with some additional conditions. The issue of coherence is discussed carefully in the paper by A&W, and in more detail in Warren’s thesis, and a coherent model in sSets (and elsewhere) is described in both. Subsequent work by vdB&G also gives perfectly correct, coherent models in (structured) categories with WFSs. Regarding your (1), LCCC is not required for
-types, because these are only needed for dependent type along dependent types — not all maps. Recent work such as the coherence theorem by Lumsdaine and Warren give perfectly precise models of the syntax of MLTT in WFSs and QMCs satisfying precisely stated conditions (which are also necessary, as shown by the syntactic model). You may want to mean something different by an “interpretation into abstract homotopy theory”, but that is not a matter of what the “truth” is. The results you criticize are perfectly correct, even if you would like to see something else proved.
Also, regarding (3), you say that your 2009 notes contained a treatment of Id-types, but did it? How was the coherence problem for the J-terms supposed to be handled (which is a different problem than the coherence of pullbacks)? No solution was given in that setting until the write-up by KLV in 2012. A solution using intervals was contained in A&W, and Warren’s thesis, and a different one in the work cited by vdB&G.
VV’s 2009 notes did already have (the key point of) the approach to strict stability of J that we give in more detail in the KLV write-up — it’s rather terse, and wasn’t easy to see at first what was going on, but it’s there. Michael W gave a very helpful exegesis of it in seminars at Dalhousie around the time of the Oberwolfach meeting. His analysis of what really made it work became the “weak stability” that we use in our local universes paper
There is a complete description of what an Id-structure on a universe is on pp.6-7 of the notes/slides for my February 2010 CMU talk, see 2010_CMU repo on my github.
Michael Warren’s thesis requires the interval to be a strict co-category object. Such intervals are not available in simplicial sets. vnB&G circumvent this problem by using Moore path objects that do not arise from intervals.
That the abstract homotopy theory in question is locally cartesian closed seems to have been clear enough all along, also for outsiders. Mike Shulman gave excellent lectures to general mathematical audiences amplifying this point already almost three years back, see around slide 44 here: http://www.math.ias.edu/~mshulman/hottminicourse2012/03models.pdf The excellent article that goes with this (http://arxiv.org/abs/1203.3253) has the details around def. 2.12 and notices in the examples there that — by a noteworthy observation independently due to Cisinski-Shulman and Gepner-Kock — every locally cartesian closed infinity-category has a type theoretic model category presentation.
To put differently what Steve and Urs have already said, to say that MLTT interprets into “abstract homotopy theory” is not to claim that it interprets into every model category, so it’s not wrong. Analogously, prior to HoTT we could have said that MLTT interprets into abstract category theory, even though it doesn’t interpret into every category. The phrases “homotopy theory” and “category theory” are being used as descriptions of a subject, not a specific mathematical object. It’s also true, as you say, that a proof of the initiality of the syntactic category has not been written out in all cases in fully gory detail; but I think this also doesn’t affect the correctness of the quoted sentence as an informal thumbnail description. The first sentence of the web site should be describing the entire subject area informally to newcomers, not getting into the nitty-gritty about what exactly has and hasn’t been done.
I think Vladimir really has two separate criticisms here. The first is that he reads “…into abstract homotopy theory” as suggesting “…into any QMC”, which certainly would be incorrect. Like you and others, I think it’s clear enough (not just to insiders) that no-one is saying this, and I don’t think anyone would read that sentence in the introduction as a precise claim to that effect.
But I think the second criticism, on the status of the initiality of the syntactic category, is a bit harder to dismiss. I feel, like you do, that it’s well-established, and we all know how to prove it, it’s just so long and ugly that no-one wants to write it out (and no-one would want to read it). But the more I try to defend it in my head against an imaginary inquisitor, the less comfortable I feel with the situation. “We all know it’s true.” “How? Is it proven?” “Well, no, but it’s a straightforward extension of an existing proof.” “How can you be sure?” “Well, if you understand Streicher’s proof, then you can see it’s easy to extend it.” “Are you sure you’re not missing some details?” “No, there aren’t any tricky details.” “Then why not write it up?” “Well, there are just so many fiddly details…”
I am still confident that initiality (for MLTT, and other specific type theories) is a straightforward extension of Streicher’s proof. But I no longer feel that confidence justifies treating it as proven. We can’t be certain that it’s as straightforward as we think it is until someone has actually written it out — carefully, correctly, and publicly, so that multiple sets of eyes can check for errors.
Or, on a slightly different approach: Håkon Gylterud, Erik Palmgren, and I are currently working on formalising a version of Streicher’s proof in Coq. It’s much too early to be sure we’ll be able to make it go through, but it seems to be going well so far. We’re aiming to make it modular enough that it should extend well to further type theories.
Of course, the eventual ideal goal would be to have a general statement of the theorem, for a class of type theories including CoC and MLTT as special cases. But this — unlike doing the special cases individually — is certainly not straightforward.
I agree, it’s shouldn’t get into nitty-gritty details. But insofar as it’s an informal adumbration of a precise statement, that precise statement should be something proven (or else there should be some qualification in the phrasing). I don’t doubt the correctness of the statement, in this case, but I have come around to somewhat sharing Vladimir’s misgivings about treating it as an established theorem.
How about something like “Homotopy Type Theory refers to a new field of study relating Martin-Löf’s system of intensional, constructive type theory and abstract homotopy theory.”?
That sounds good to me! Another option could be to borrow a phrasing from Jaap van Oosten’s review, and replace “interpretation” in the current version by “ontology”. (I very much liked that point in the review, that the ontology is one of the most novel aspects of HoTT/UF.) But perhaps that kind of use of philosophical terminology would be offputting to some mathematical readers.
I guess I was reading the word “interpretation” informally, rather than as indicating or claiming any precise theorem. As a reader, I wouldn’t expect a sentence placed like that to refer to any precise theorem anyway. But I’m perfectly happy with Steve’s suggestion.
I think that’s how it was intended, informally, and how it is most naturally understood. But if there is a risk that it could be read uncharitably as saying something else, then I guess we should change it.
Yes, I’d agree that I think it was all intended in the informal, broader senses of the words, and under that reading it’s an excellent and succinct description. It would be nice to find something as succinct and informative, that doesn’t allow the misreading as a precise and not-quite-established statement.
I like Steve’s suggestion for a replacement lead sentence, because it seems not to suggest a precise, but false, statement to some readers.
Do we want to exclude other systems of intentional constructive type theory such as the Calculus of Inductive Constructions from the study?
I don’t think anyone has ever intended that exclusion. This seems like another broad/narrow sense issue: “Martin-Löf Type Theory” has long been used both to refer to certain specific type theories, and to the general area of study of these and similar type theories. I don’t think the broad usage is at all unreasonable — just as someone can say they work in “abstract homotopy theory”, without meaning that everything they prove holds in an arbitrary model category.
We could say something like “Martin-Lof-style type theory”. Or, I suppose, just “dependent type theory”.
But of course Martin-Löf’s Identity-types are crucial, so I think it is justified to specifically mention M-L type theory.
Just so that I understand. When you say “abstract homotopy theory” you actually mean “an (infty,1)-topos”, right? This is why you want to keep the word “abstract” there? Then the real interest is in finding interpretations of the rules of type-theoretic nature on (infty,1)-toposes. Interpretation of the syntax (functors from the syntactic category) is then secondary. Then it becomes the extension of the theory of (infty,1)-toposes by means of ideas and constructions originated in the type theory and vice versa.
When we figure out what directed type theory is it will be interpretation of various rules on (infty,2)-toposes. This will be further away from abstract homotopy theory.
Maybe we can say that HoTT is a field of study centered on the univalent model of the MLTT in the homotopy category of spaces.
Then in the next paragraph we can say that HoTT studies both the variations of this model based on new type theories such as the cubical type theory and the extension of the structures on the homotopy category that this model defines from the standard homotopy category of spaces to more general (infty,1)-toposes and model categories.
When I say “abstract homotopy theory”, I don’t mean anything so precise as “(infty,1)-toposes” or “Quillen model categories”: I mean the field of mathematics that studies abstract structures that exhibit homotopical behavior. Such structures include model categories, (infty,1)-categories, (infty,2)-categories, categories of fibrant objects, A-infinity categories, enriched and unenriched, etc. etc.
I wouldn’t say that HoTT is centered on any particular model. Certainly the model in spaces plays a distinguished role, just as (say) the category of sets plays a distinguished role in category theory, but as a description of the subject area in general I think it would be too specific to mention any particular model, even the most important one.
There is a certain flavor that mathematicians and homotopy theorists in particular attach to the phrase “abstract homotopy theory”. The word “abstract” is only used when someone wants to emphasize that the study concerns model categories.
I don’t that makes sense logically (other models for homotopy theory are just as abstract as model categories), and it hasn’t been my experience. A quick google search for abstract homotopy theory turns up as the first few hits:
I wrote to Mike Hopkins asking him about his reaction to the phrase “abstract homotopy theory”. Here is an excerpt from our conversation:
V.V:
Hi Mike,
how would you characterize in the shortest possible way the subject area of “abstract homotopy theory”?
…
M.H.:
I think that the most elemental form of abstract homotopy theory takes place in a category equipped with a set of morphisms called “weak equivalences,” which one intends to invert. So as soon as one is in a situation where one wants to regard some maps as being equivalences one is doing abstract homotopy theory. (one could say this happens in all of mathematics)
Why do you ask?
V.V:
Have al look at the argument that I have started at the HoTT website
https://homotopytypetheory.org/2015/01/11/hott-is-not-an-interpretation-of-mltt-into-abstract-homotopy-theory/
…
Do you mind if I cite your reply there?
Vladimir.
M.H.:
…
I read through the argument. I took your question to be asking how I would communicate something about abstract homotopy theory to a lay person. In that case talking about a category with weak equivalences is the easiest way to go (and often the easiest to write about, as the Quillen axioms sometime unnecessarily obfuscate what one is doing –notice how often one needs to introduce a special class of objects on which derived functors can be computed). quasicategoies are also good places to do homotopy theory. But I would probably modify what I said to say that whenever you have a collection of things you wish to regard as equivalent, you are doing abstract homotopy theory. I’d even advocate for removing the word “abstract” here, in the same way we no longer talk about “generalized cohomology theories”. You’re just doing homotopy theory. So were I to weigh in I would suggest removing the word “abstract” for that reason.
….
That said, you can certainly quote our conversation, but I’d ask you to keep it in context.
****
Thanks! That seems to me to accord pretty well with what I’ve been saying. I would favor still keeping the word “abstract”, though, to make it clearer to the non-expert that what we’re talking about isn’t just the classical homotopy theory of spaces. I don’t see that the word “abstract” does any harm.
The word “abstract” might be taken to exclude consideration of interpretations of type theory into the concrete homotopy theory of simplicial sets, so should be removed also for that reason.
I disagree. The concrete is always a special case of the abstract, so doing something in an abstract case cannot exclude a concrete case. Whatever “abstract homotopy theory” is, it had better include the classical concrete homotopy theory to be deserving of the name!
I agree with Mike. “Abstract” is there to mean “not only concrete”, ie. not just spaces (but that too). This intro page is for very general consumption, and is to be understood informally.
Another problem with the word “interpretation” is that it suggests that the field is all, or mainly, about semantics of type theory. That would exclude synthetic mathematics done in type theory as a foundational system. A word like “relation” or “dictionary” would also be better for this reason.