References

The list of references below is now superseded by the catalog of references on our wiki. Please refer to that catalog instead, and feel free to edit the information there. The list below is preserved for historical reasons, and is not up to date.

 

A roughly taxonomised listing of some of the papers on Homotopy Type Theory. Titles link to more details, bibdata, etc.

Surveys:

• Type theory and homotopy. Steve Awodey, 2010. (To appear.) [PDF]
• Homotopy type theory and Voevodsky’s univalent foundations. Álvaro Pelayo and Michael A. Warren, 2012. (Bulletin of the AMS, forthcoming) [arXiv]
• Voevodsky’s Univalence Axiom in homotopy type theory. Steve Awodey, Álvaro Pelayo, and Michael A. Warren, October 2013, Notices of the American Mathematical Society 60(08), pp.1164-1167. [arXiv]

General models:

• The groupoid interpretation of type theory. Thomas Streicher and Martin Hofmann, in Sambin (ed.) et al., Twenty-five years of constructive type theory. Proceedings of a congress, Venice, Italy, October 19—21, 1995. Oxford: Clarendon Press. Oxf. Logic Guides. 36, 83-111 (1998). [PostScript]
• Homotopy theoretic models of identity types. Steve Awodey and Michael Warren, Mathematical Proceedings of the Cambridge Philosophical Society, 2009. [PDF]
• Homotopy theoretic aspects of constructive type theory. Michael A. Warren, Ph.D. thesis: Carnegie Mellon University, 2008. [PDF]
• Two-dimensional models of type theory, Richard Garner, Mathematical Structures in Computer Science 19 (2009), no. 4, pages 687–736. RG’s website.
• Topological and simplicial models of identity types. Richard Garner and Benno van den Berg, to appear in ACM Transactions on Computational Logic (TOCL). [PDF]
• The strict ω-groupoid interpretation of type theory Michael Warren, in Models, Logics and Higher-Dimensional Categories: A Tribute to the Work of Mihály Makkai, AMS/CRM, 2011.[PDF]
• Homotopy-Theoretic Models of Type Theory. Peter Arndt and Chris Kapulkin. In Typed Lambda Calculi and Applications, volume 6690 of Lecture Notes in Computer Science, pages 45–60.
• Combinatorial realizability models of type theory, Pieter Hofstra and Michael A. Warren, 2013, Annals of Pure and Applied Logic 164(10), pp. 957-988. [arXiv]

Univalence:

• Univalence in simplicial sets. Chris Kapulkin, Peter LeFanu Lumsdaine, Vladimir Voevodsky. [arXiv]
• The univalence axiom for inverse diagrams. Michael Shulman. [arXiv]
• Fiber bundles and univalence.  Lecture by Ieke Moerdijk at the Lorentz Center, Leiden, December 2011.  Lecture notes by Chris Kapulkin.
• A model of type theory in simplicial sets: A brief introduction to Voevodsky’s homotopy type theory.  Thomas Streicher, 2011. [PDF]
• Univalence and Function Extensionality.  Lecture by Nicola Gambino at Oberwohlfach, February 2011.  Lecture notes by Chris Kapulkin and Peter Lumsdaine.
• The Simplicial Model of Univalent Foundations. Chris Kapulkin and Peter LeFanu Lumsdaine and Vladimir Voevodsky, 2012. [arXiv]
• A preliminary univalent formalization of the p-adic numbers. Álvaro Pelayo, Vladimir Voevodsky, Michael A. Warren, 2012. [arXiv]

Syntax of type theory:

• The identity type weak factorisation system. Nicola Gambino and Richard Garner, Theoretical Computer Science 409 (2008), no. 3, pages 94–109. RG’s website.
• Types are weak ω-groupoids. Richard Garner and Benno van den Berg, to appear. RG’s website.
• Weak ω-Categories from Intensional Type Theory. Peter LeFanu Lumsdaine, TLCA 2009, Brasília, Logical Methods in Computer Science, Vol. 6, issue 23, paper 24. [PDF]
• Higher Categories from Type Theories. Peter LeFanu Lumsdaine, PhD Thesis: Carnegie Mellon University, 2010. [PDF]
• A coherence theorem for Martin-Löf’s type theory. Michael Hedberg, Journal of Functional Programming 8 (4): 413–436, July 1998.

Computational interpretation:

• Canonicity for 2-Dimensional Type Theory. Dan Licata and Robert Harper. POPL 2012. [PDF]

Other:

• Martin-Löf Complexes. S. Awodey, P. Hofstra and M.A. Warren, 2013, Annals of Pure and Applied Logic, 164(10), pp. 928-956. [PDF], [arXiv]
• Inductive Types in Homotopy Type Theory. S. Awodey, N. Gambino, K. Sojakova. To appear in LICS 2012.  [arXiv]
• Model Structures from Higher Inductive Types.  P. LeFanu Lumsdaine.  Unpublished note, Dec. 2011. [PDF]
• 2-Dimensional Directed Dependent Type Theory. Dan Licata and Robert Harper. MFPS 2011. See also Chapters 7 and 8 of Dan’s thesis. [PDF]

To have a listing added, email one of the maintainers, or leave a comment below.