Next Thursday, 10th September, Guillaume Brunerie and Peter LeFanu Lumsdaine are going to present a talk Initiality for Martin-Löf type theory in the HoTT electronic seminar … with a proof of the initiality conjecture!Here’s the abstract:
“Initiality” is the principle that the term model of some type theory should be an initial object in the category of models of that type theory. Thomas Streicher gave a careful proof of initiality for the Calculus of Constructions in 1991. Since then, initiality for more complex type theories (such as Martin-Löf type theory) has often been treated as established, as a straightforward extension of Streicher’s result, but never written up carefully for a larger theory.
Around 2010, various researchers (notably Voevodsky) raised the question of whether these extensions really were sufficiently straightforward to consider them established without further proof. Since then, views on the status of initiality have varied within the field; but the issue has been, at least, a frustrating unresolved point.
In this talk, we present a proof of initiality for a full-featured Martin-Löf type theory. The proof is formalised in Agda, to dispel any question of thoroughness (and also partly formalised in Coq), and is carefully designed for extensibility to other type theories. The proof is based on Streicher’s, using some improvements of Hofmann and further refinements by the present authors. The two formalisations present slightly different versions of the statement — using contextual categories in Agda, categories with attributes in Coq — but the core of the proof is parallel.
Joint work with Menno de Boer and Anders Mörtberg.
This was a big concern of Vladimir Voevodsky and it’s good to finally have it sorted out, with a formalised proof, as it should have.
Unfortunately it’s live at 1am, so I’ll have to grab the recording…