A roughly taxonomised listing of some of the papers on Homotopy Type Theory. Titles link to more details, bibdata, etc. Currently very incomplete; please add! ##Surveys:## * _Type theory and homotopy._ Steve Awodey, 2010. (To appear.) [PDF](http://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf) * _Homotopy type theory and Voevodsky?s univalent foundations._ Álvaro Pelayo and Michael A. Warren, 2012. (Bulletin of the AMS, forthcoming) [arXiv](http://arxiv.org/abs/1210.5658) * _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](http://arxiv.org/abs/1302.4731) ##General models:## * [_The groupoid interpretation of type theory._](http://homotopytypetheory.org/references/hofmann-streicher-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](http://www.mathematik.tu-darmstadt.de/~streicher/venedig.ps.gz) * [_Homotopy theoretic models of identity types._](http://homotopytypetheory.org/references/awodey-warren-homotopy-theoretic-models-of-identity-types/) Steve Awodey and Michael Warren, Mathematical Proceedings of the Cambridge Philosophical Society, 2009. [PDF](http://www.andrew.cmu.edu/user/awodey/preprints/homotopy.pdf) * _Homotopy theoretic aspects of constructive type theory._ Michael A. Warren, Ph.D. thesis: Carnegie Mellon University, 2008. [PDF](http://mawarren.net/papers/phd.pdf) * _Two-dimensional models of type theory_, Richard Garner, Mathematical Structures in Computer Science 19 (2009), no. 4, pages 687?736. [RG?s website](http://www.comp.mq.edu.au/~rgarner/2-LCCC/2-LCCC.html) * _Topological and simplicial models of identity types._ Richard Garner and Benno van den Berg, to appear in ACM Transactions on Computational Logic (TOCL). [PDF](http://tocl.acm.org/accepted/467garner.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](http://mawarren.net/papers/crmp1295.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](http://arxiv.org/abs/1205.5527) ##Univalence:## * _Univalence in simplicial sets._ Chris Kapulkin, Peter LeFanu Lumsdaine, Vladimir Voevodsky. [arXiv](http://arxiv.org/abs/1203.2553) * _Univalence for inverse diagrams and homotopy canonicity._ Michael Shulman. [arXiv](http://arxiv.org/abs/1203.3253) * _Fiber bundles and univalence._ Lecture by Ieke Moerdijk at the Lorentz Center, Leiden, December 2011. [Lecture notes by Chris Kapulkin](http://www.andrew.cmu.edu/user/awodey/hott/papers/moerdijk_univalence.pdf) * _A model of type theory in simplicial sets: A brief introduction to Voevodsky?s homotopy type theory._ Thomas Streicher, 2011. [PDF](http://www.mathematik.tu-darmstadt.de/~streicher/sstt.pdf) * _Univalence and Function Extensionality._ Lecture by Nicola Gambino at Oberwohlfach, February 2011. [Lecture notes by Chris Kapulkin and Peter Lumsdaine](http://www.pitt.edu/~krk56/UA_implies_FE.pdf) * _The Simplicial Model of Univalent Foundations._ Chris Kapulkin and Peter LeFanu Lumsdaine and Vladimir Voevodsky, 2012. [arXiv](http://arxiv.org/abs/1211.2851) * _The univalence axiom for elegant Reedy presheaves_. Michael Shulman, [arXiv](http://arxiv.org/abs/1307.6248) * _A univalent universe in finite order arithmetic_. Colin McLarty, [arXiv](http://arxiv.org/abs/1412.6714) * _Realizability of Univalence: Modest Kan complexes_. Wouter Pieter Stekelenburg, [arXiv](http://arxiv.org/abs/1406.6579) * _Univalence for inverse EI diagrams_. Michael shulman, [arXiv](http://arxiv.org/abs/1508.02410) ##Inductive and higher-inductive types## * _Inductive Types in Homotopy Type Theory._ S. Awodey, N. Gambino, K. Sojakova. To appear in LICS 2012. [arXiv](http://arxiv.org/abs/1201.3898) * _W-types in homotopy type theory_. Benno van den Berg and Ieke Moerdijk, [arXiv](http://arxiv.org/abs/1307.2765) * _Homotopy-initial algebras in type theory_ Steve Awodey, Nicola Gambino, Kristina Sojakova. [arXiv](http://arxiv.org/abs/1504.05531), [Coq code](https://github.com/kristinas/hinitiality) * _The General Universal Property of the Propositional Truncation_. Nicolai Kraus, [arXiv](http://arxiv.org/abs/1411.2682) ##Formalizations of set-level mathematics## * _A preliminary univalent formalization of the p-adic numbers._ Álvaro Pelayo, Vladimir Voevodsky, Michael A. Warren, 2012. [arXiv](http://arxiv.org/abs/1302.1207) * _Univalent categories and the Rezk completion_. Benedikt Ahrens, Chris Kapulkin, Michael Shulman, Math. Structures Comput. Sci. 25 (2015), no. 5, 1010?1039. [arXiv](http://arxiv.org/abs/1303.0584) ##Synthetic homotopy theory## * _Calculating the fundamental group of the circle in homotopy type theory_. Dan Licata and Michael Shulman, LICS 2013, available [here](http://www.cs.cmu.edu/~drl/pubs.html) and on [arXiv](http://arxiv.org/abs/1301.3443) * _Homotopy limits in type theory_. Jeremy Avigad, Chris Kapulkin, Peter LeFanu Lumsdaine, Math. Structures Comput. Sci. 25 (2015), no. 5, 1040?1070. [arXiv](http://arxiv.org/abs/1304.0680) * _Eilenberg-MacLane Spaces in Homotopy Type Theory_. Dan Licata and Eric Finster, [PDF](http://dlicata.web.wesleyan.edu/pubs/lf14em/lf14em.pdf) and [code](https://github.com/dlicata335/hott-agda/blob/master/homotopy/KGn.agda) ##Homotopical ideas and truncations in type theory## * _Notions of anonymous existence in Martin-Lof type theory_. Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. [pdf](http://www.cs.nott.ac.uk/~txa/publ/jhedberg.pdf) * _Idempotents in intensional type theory_. Michael Shulman, [arXiv](http://arxiv.org/abs/1507.03634) ##Applications to computing## * _Homotopical patch theory_. Carlo Angiuli, Ed Morehouse, Dan Licata, Robert Harper, [PDF](http://dlicata.web.wesleyan.edu/pubs/amlh14patch/amlh14patch.pdf) ##Cubical models and cubical type theory## * _A Cubical Approach to Synthetic Homotopy Theory_. Dan Licata and Guillaume Brunerie, [PDF](http://dlicata.web.wesleyan.edu/pubs/lb15cubicalsynth/lb15cubicalsynth.pdf) * _A syntax for cubical type theory_. Thorsten Altenkirch and Ambrus Kaposi, [PDF](http://www.cs.nott.ac.uk/~txa/publ/ctt.pdf) * _Implementation of Univalence in Cubical Sets_, [github](https://github.com/simhu/cubical) * _A Note on the Uniform Kan Condition in Nominal Cubical Sets_, Robert Harper and Kuen-Bang Hou. [arXiv](http://arxiv.org/abs/1501.05691) ##Syntax of type theory:## * [_The identity type weak factorisation system._](http://homotopytypetheory.org/references/gambino-garner-the-identity-type-weak-factorisation-system/) Nicola Gambino and Richard Garner, Theoretical Computer Science 409 (2008), no. 3, pages 94?109. [RG?s website](http://www.comp.mq.edu.au/~rgarner/Idtype/Idtype.html) * _Types are weak ∞-groupoids._ Richard Garner and Benno van den Berg, to appear. [RG?s website](http://www.comp.mq.edu.au/~rgarner/Typesom/Typesom.html) * _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](http://www.mathstat.dal.ca/~p.l.lumsdaine/research/Lumsdaine-Weak-omega-cats-from-ITT-LMCS.pdf) * _Higher Categories from Type Theories._ Peter LeFanu Lumsdaine, PhD Thesis: Carnegie Mellon University, 2010. [PDF](http://www.mathstat.dal.ca/~p.l.lumsdaine/research/Lumsdaine-2010-Thesis.pdf) * [_A coherence theorem for Martin-Löf?s type theory._](http://homotopytypetheory.org/references/hedberg/) Michael Hedberg, Journal of Functional Programming 8 (4): 413?436, July 1998. * _Model Structures from Higher Inductive Types._ P. LeFanu Lumsdaine. Unpublished note, Dec. 2011. [PDF](http://www.mathstat.dal.ca/~p.l.lumsdaine/research/Lumsdaine-Model-strux-from-HITs.pdf) * _A category-theoretic version of the identity type weak factorization system_. Jacopo Emmenegger, [arXiv](http://arxiv.org/abs/1412.0153) * _Locally cartesian closed quasicategories from type theory_. Chris Kapulkin, [arXiv](http://arxiv.org/abs/1507.02648). ##Computational interpretation:## * _Canonicity for 2-Dimensional Type Theory._ Dan Licata and Robert Harper. POPL 2012. [PDF](http://www.cs.cmu.edu/~drl/pubs/lh112tt/lh122tt-final.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](http://mathstat.dal.ca/~mwarren/Papers/mc.pdf), [arXiv](http://arxiv.org/abs/0906.4521) * _2-Dimensional Directed Dependent Type Theory._ Dan Licata and Robert Harper. MFPS 2011. See also Chapters 7 and 8 of [Dan?s thesis](http://www.cs.cmu.edu/~drl/pubs/thesis/thesis.pdf). [PDF](http://www.cs.cmu.edu/~drl/pubs/lh102dtt/lh102dtt.pdf)