A Communal Proof of an Initiality Theorem
Posted by Mike Shulman
One of the main reasons I’m interested in type theory in general, and homotopy type theory (HoTT) in particular, is that it has categorical semantics. More precisely, there is a correspondence between (1) type theories and (2) classes of structured categories, such that any proof in a particular type theory can be interpreted into any category with the corresponding structure. I wrote a lot about type theory from this perspective in The Logic of Space. The basic idea is that we construct a particular structured category out of the syntax of the type theory, and prove that it is the initial such category. Then we can interpret any syntactic object in a structured category by regarding as living in and applying the unique structured functor .
Unfortunately, we don’t currently have any very general definitions of what “a type theory” is, what the “corresponding class of structured categories” is, or a very general proof of this “initiality theorem”. The idea of such proofs is easy — just induct over the construction of syntax — but its realization in practice can be long and tedious. Thus, people are understandably reluctant to take the time and space to write out such a proof explicitly, when “everyone knows” how the proof should go and probably hardly anyone would really read such a proof in detail anyway. This is especially true for dependent type theory, which is qualitatively more complicated in various ways than non-dependent type theories; to my knowledge only one person (Thomas Streicher) has ever written out anything approaching a complete proof of initiality for a dependent type theory.
There is currently some disagreement in the HoTT community over how much a problem this is. On one side, the late Vladimir Voevodsky argued that it is completely unacceptable, delayed the publication of his seminal model of type theory in simplicial sets because of his dissatisfaction with the situation, and spent the last years of his life working on the problem. (Others, less dogmatic in philosophy, are nevertheless also working on the problem — specifically, attempting to give a general definition of “type theory” and prove a general initiality theorem for all such “type theories”.) On the other side, plenty of people point out reasonably that functorial semantics has been well-understood for decades, and why should we worry so much about a particular instance of it all of a sudden now? Unfortunately, the existence of this disagreement is not good for the perception of our discipline among other mathematicians.
In my experience, arguments about the importance of initiality often tend to devolve into disagreements about questions like: Is Streicher’s proof hard to understand? Does it generalize “easily” to other type constructors? How “easy” is “easily”? What kinds of type constructors? Is it hard to deal with variable binding? Is the categorical structure really “exactly” the same as the type-theoretic structure? Where is the “hard part” of an initiality proof? Is there even a “hard part” at all? Plenty of people have opinions about these questions, but for most of us these opinions are not based on actual experience of trying to prove such a theorem.
Last month at the nForum, Richard Williamson suggested the (in hindsight obvious) solution: let’s get a bunch of people together and work together to write out a complete proof of an initiality theorem, in modern language, for a basic uncomplicated dependent type theory. If we have enough contributors to divide up the work, the verbosity and tedium shouldn’t be overwhelming. We can use the nLab wikilink features to organize the proof in a “drill-down” manner so that a reader can get a high level idea and then delve into as many or as few details as desired. Hopefully, this will increase overall public awareness of how such proofs work, so that they seem less “magic”. Moreover, all the contributors will get some actual experience “in the trenches” with an initiality proof, thereby hopefully leading us to more informed opinions.
I don’t view such a project as a replacement for proving one general theorem, but as a complementary effort, whose goals are primarily understanding and exposition. However, if it’s successful, the result will be a complete initiality theorem for at least one dependent type theory; and we can add as many bells and whistles to this theory as we have time and energy for, hopefully in a relatively modular way.
We had some preliminary discussion about this project at the nForum here, at which enough people expressed interest in participating that I think the project can get off the ground. But the more the merrier! If you’d like to help out, even just a little bit, just add your name to the list of participants on this nLab page and join the conversation when it begins. (Some other people have informally told me they’re interested, but I didn’t keep a record of their names, so I didn’t add them to the list; if you fall in that category, please add yourself!)
I’m not sure yet how we will do most of our communication and coordination. We’ll probably have one or more nForum threads for discussion. I think it might be nice to have some scheduled videoconference meetings for those who can make it, especially during the early stages when we’ll have to make various decisions that will affect the overall course of the project; but I’m not wedded to that if others aren’t interested. Most of the work will probably be individual people writing out proofs of inductive cases on nLab pages.
Some of the decisions we’ll have to make at the beginning include:
What type theory should we aim for as a first target? We can always add more to it later, so it should be something fairly uncomplicated, but nontrivial enough to exhibit the interesting features. For instance, I think it should certainly have -types. What about universes?
Exactly how should we present the syntax? In particular, should we represent variable binding with named variables, de Bruijn indices, or some other method? Should all terms be fully annotated?
What categorical structure should we use as the substrate? Options include contextual categories (a.k.a. “C-systems”), categories with families, split comprehension categories, etc.
How should we structure the proof? The questions here are hard to describe concisely, but for instance one of them was mentioned by Peter Lumsdaine at the nForum thread: Streicher phrases the induction using an “existential quantifier” for interpretation of contexts, but it is arguably easier to use a “universal quantifier” in the same place.
Feel free to use the comments of this post to express opinions about any of these, or about the project overall. My current plan is to wait a couple weeks to give folks a chance to sign up, then “officially” start making plans as a group.
Re: A Communal Proof of an Initiality Theorem
I have heard that some folks at Stockholm University are working on something just along these lines. I attended a talk by Guillaume Brunerie some weeks ago, where he outlined a definition for a general type theory and proof of initiality for its syntactic category. Peter LeFanu Lumsdaine has been working on the same things, collaborating with someone else (can’t remember who!) independently of Guillaume. So perhaps we are in good luck if we just wait for their papers to appear! :)