HoTT is not an interpretation of MLTT into abstract homotopy theory

HoTT is not an interpretation of MLTT into abstract homotopy theory

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.