nLab Initiality Project - References

See also

Steve Awodey, Natural models of homotopy type theory

Math. Structures Comput. Sci. 28 (2018), no. 2, 241–286.

arXiv:1406.3219, doi:10.1017/S0960129516000268, MR, BibTeX

Krzysztof Kapulkin and Peter LeFanu Lumsdaine, The simplicial model of univalent foundations (after Voevodsky)

2012, Revised 2018 as v5

Conjecture 1.2.9 in the article says,

Let $\mathbf{T}$ be the type theory given by the structural rules of Section A.1, plus any combination of the logical rules of Sections A.2, A.3. Then $\mathcal{C}(\mathbf{T})$ is initial among contextual categories with the correspondingly-named extra structure.

The next paragraph of the article says,

In other words, if $\mathcal{C}$ is a contextual category with structure corresponding to the logical rules of a type theory $\mathbf{T}$ , then there should be a unique homomorphism $\mathcal{C}(\mathbf{T}) \to \mathcal{C}$ interpreting the syntax of $\mathbf{T}$ in $\mathcal{C}$ . As discussed at the beginning of this section, the Correctness Theorem of [Str91, Ch. III, p. 181] gives an analogous fact for a rather smaller type theory, while the status of the present conjecture is debated, accepted by some but not all in the ﬁeld as a straightforward extension of that theorem.

Thomas Streicher, Semantics of type theory, Correctness, completeness and independence results

With a foreword by Martin Wirsing, Progress in Theoretical Computer Science, Birkhäuser Boston, Inc., Boston, MA, 1991, xii+298 pp., ISBN: 0-8176-3594-7

doi:10.1007/978-1-4612-0433-6, MR, BibTeX

This book was suggested by Mike Shulman, in an nForum message, as a primary reference for the Initiality Project.

Vladimir Voevodsky, HoTT is not an interpretation of MLTT into abstract homotopy theory

Article at the homotopytypetheory.org blog, January 11, 2015

URL, BibTeX

There is a discussion of the initiality conjecture in the last four paragraphs of the article.

Vladimir Voevodsky, From syntax to semantics of dependent type theories — formalized

Slides of a lecture at RDP 2015, Warsaw, June 30, 2015

URL, BibTeX

There is a statement of the initiality conjecture on slide 18. Slide 19 has some remarks on the difficulty of the conjecture, and slide 20 has some remarks on the importance of the conjecture.

Vladimir Voevodsky, Mathematical theory of type theories and the initiality conjecture

Research proposal to the Templeton Foundation, 2016

URL, BibTeX

Vladimir Voevodsky, The meta-theory of dependent type theories

Video, Members Seminar, Institute for Advanced Study, Princeton, NJ, USA, February 27, 2017

URL, BibTeX

Vladimir Voevodsky, Models, interpretations and the initiality conjectures

Lecture at the special session on category theory and type theory in honor of Per Martin-Löf on his 75th birthday, August 17–19, 2017, during the Logic Colloquium 2017, August 14–20, 2017, Stockholm

URL, BibTeX

The annotation at the URL of the document says, “This is a clear and enlightening sketch of Voevodsky’s entire program!”.