**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.