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! * table of contents {:toc} ##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. [arXiv](http://arxiv.org/abs/1208.5683) * _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) * _Natural models of homotopy type theory_, Steve Awodey, 2015. [arXiv](http://arxiv.org/abs/1406.3219) * _Subsystems and regular quotients of C-systems_, Vladimir Voevodsky, 2014. [arXiv](http://arxiv.org/abs/1406.7413) * _C-system of a module over a monad on sets_, Vladimir Voevodsky, 2014. [arXiv](http://arxiv.org/abs/1407.3394) * _A C-system defined by a universe category_, Vladimir Voevodsky, 2014. [arXiv](http://arxiv.org/abs/1409.7925) * _B-systems_, Vladimir Voevodsky, 2014. [arXiv](http://arxiv.org/abs/1410.5389) * _The local universes model: an overlooked coherence construction for dependent type theories_, Peter LeFanu Lumsdaine, Michael A. Warren, to appear in ACM Transactions on Computational Logic, 2014. [arXiv](http://arxiv.org/abs/1411.1736) * _Products of families of types in the C-systems defined by a universe category_, Vladimir Voevodsky, 2015. [arXiv](http://arxiv.org/abs/1503.07072) * _Martin-Lof identity types in the C-systems defined by a universe category_, Vladimir Voevodsky, 2015. [arXiv](http://arxiv.org/abs/1505.06446) * _The Frobenius Condition, Right Properness, and Uniform Fibrations_, Nicola Gambino, Christian Sattler. [arXiv](http://arxiv.org/abs/1510.00669) * _Fibred fibration categories_, Taichi Uemura, 2016, [arXiv](http://arxiv.org/abs/1602.08206) ##Univalence:## * _The equivalence axiom and univalent models of type theory_ (talk at CMU, February 4th, 2010), Vladimir Voevodsky. [arXiv](http://arxiv.org/abs/1402.5556) * _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-home.math.uwo.ca/~kkapulki/notes/fiber_bundles_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) * _Univalent universes for elegant models of homotopy types_. Denis-Charles Cisinski, [arXiv](http://arxiv.org/abs/1406.0058) * _A univalent universe in finite order arithmetic_. Colin McLarty, [arXiv](http://arxiv.org/abs/1412.6714) * _Constructive Simplicial Homotopy_. Wouter Pieter Stekelenburg, [arXiv](http://arxiv.org/abs/1604.04746) * _Higher Homotopies in a Hierarchy of Univalent Universes_. Nicolai Kraus and Christian Sattler, [arXiv](http://arxiv.org/abs/1311.4002), [DOI](http://dl.acm.org/citation.cfm?doid=2737801.2729979) * _Univalence for inverse EI diagrams_. Michael shulman, [arXiv](http://arxiv.org/abs/1508.02410) * _Univalent completion_. Benno van den Berg, Ieke Moerdijk, [arXiv](http://arxiv.org/abs/1508.04021) * _On lifting univalence to the equivariant setting_. Anthony Bordg, [arXiv](http://arxiv.org/abs/1512.04083) ##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) * _Non-wellfounded trees in Homotopy Type Theory_. Benedikt Ahrens, Paolo Capriotti, Régis Spadotti. TLCA 2015, [doi:10.4230/LIPIcs.TLCA.2015.17](http://dx.doi.org/10.4230/LIPIcs.TLCA.2015.17), [arXiv](https://arxiv.org/abs/1504.02949) * _Constructing the Propositional Truncation using Non-recursive HITs_. Floris van Doorn, [arXiV](http://arxiv.org/abs/1512.02274) * _Constructions with non-recursive higher inductive types_. Nicolai Kraus, LiCS 2016, [pdf](http://www.cs.nott.ac.uk/~psznk/docs/pseudotruncations.pdf) * _The join construction_. Egbert Rijke, [arXiv](https://arxiv.org/abs/1701.07538) * _Semantics of higher inductive types_. Michael Shulman and Peter LeFanu Lumsdaine, [arXiv](https://arxiv.org/abs/1705.07088) ##Formalizations## * _An experimental library of formalized Mathematics based on the univalent foundations_, Vladimir Voevodsky, Math. Structures Comput. Sci. 25 (2015), no. 5, pp 1278-1294, 2015. [arXiv](http://arxiv.org/abs/1401.0053) [journal](http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=9679046) * _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:1303.0584](http://arxiv.org/abs/1303.0584) (on _[[nLab:internal categories in HoTT]]_) * _The HoTT Library: A formalization of homotopy type theory in Coq_, Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman, Matthieu Sozeau, Bas Spitters, 2016 [arxiv](https://arxiv.org/abs/1610.04591) ##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) * _$\pi_n(S^n)$ in Homotopy Type Theory_, Dan Licata and Guillaume Brunerie, Invited Paper, CPP 2013, [PDF](http://dlicata.web.wesleyan.edu/pubs/lb13cpp/lb13cpp.pdf) * _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, LICS 2014, [PDF](http://dlicata.web.wesleyan.edu/pubs/lf14em/lf14em.pdf) and [code](https://github.com/dlicata335/hott-agda/blob/master/homotopy/KGn.agda) * _A Cubical Approach to Synthetic Homotopy Theory_. Dan Licata and Guillaume Brunerie, LICS 2015, [PDF](http://dlicata.web.wesleyan.edu/pubs/lb15cubicalsynth/lb15cubicalsynth.pdf) * _Synthetic Cohomology in Homotopy Type Theory_, Evan Cavallo, [PDF](http://www.cs.cmu.edu/~rwh/theses/cavallo.pdf) * _A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory_, LICS 2016 Kuen-Bang Hou (Favonia), Eric Finster, Dan Licata, Peter LeFanu Lumsdaine, [arXiv](http://arxiv.org/abs/1605.03227) * _The Seifert-van Kampen Theorem in Homotopy Type Theory_, Kuen-Bang Hou and Michael Shulman, [PDF]( http://www.cs.cmu.edu/~kuenbanh/files/vankampen.pdf) * _On the homotopy groups of spheres in homotopy type theory_, Guillaume Brunerie, Ph.D. Thesis, 2016, [arxiv](https://arxiv.org/abs/1606.05916) * _The real projective spaces in homotopy type theory_, Ulrik Buchholtz and Egbert Rijke, LICS 2017, [arxiv](https://arxiv.org/abs/1704.05770) ##Homotopical ideas and truncations in type theory## * _Generalizations of Hedberg?s Theorem_. Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch.TLCA 2013, [pdf](http://www.cs.bham.ac.uk/~mhe/papers/hedberg.pdf) * _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) * _Functions out of Higher Truncations_. Paolo Capriotti, Nicolai Kraus, and Andrea Vezzosi. CSL 2015 [arxiv](http://arxiv.org/abs/1507.01150) * _Truncation levels in homotopy type theory_. Nicolai Kraus, PhD Thesis: University of Nottingham, 2015. [pdf](http://www.cs.nott.ac.uk/~psznk/docs/thesis_nicolai.pdf) * _Parametricity, automorphisms of the universe, and excluded middle_. Auke Bart Booij, Martín Hötzel Escardó, Peter LeFanu Lumsdaine, Michael Shulman. [arxiv](https://arxiv.org/abs/1701.05617) ##Applications to computing## * _Homotopical patch theory_. Carlo Angiuli, Ed Morehouse, Dan Licata, Robert Harper, [PDF](http://dlicata.web.wesleyan.edu/pubs/amlh14patch/amlh14patch.pdf) * _Guarded Cubical Type Theory: Path Equality for Guarded Recursion_, Lars Birkedal, Ale? Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi, [arXiv]( https://arxiv.org/abs/1606.05223) ##Cubical models and cubical type theory## * _A Cubical Approach to Synthetic Homotopy Theory_. Dan Licata and Guillaume Brunerie, LICS 2015, [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) * _The Frobenius Condition, Right Properness, and Uniform Fibrations_, Nicola Gambino, Christian Sattler. (Note: this is a duplicate of an entry in the section "General Models" above; accident?) [arXiv](http://arxiv.org/abs/1510.00669) * _Cubical Type Theory: a constructive interpretation of the univalence axiom_, Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mortberg, [arxiv](https://arxiv.org/abs/1611.02108) and [github implementation](https://github.com/mortberg/cubicaltt) * _Nominal Presentation of Cubical Sets Models of Type Theory_, Andrew M. Pitts, [pdf](http://drops.dagstuhl.de/opus/volltexte/2015/5498/pdf/12.pdf) * _Axioms for Modelling Cubical Type Theory in a Topos_, Ian Orton and Andrew M. Pitts, [pdf](http://drops.dagstuhl.de/opus/volltexte/2016/6564/pdf/LIPIcs-CSL-2016-24.pdf) [Agda code](http://www.cl.cam.ac.uk/~rio22/agda/cubical-topos/root.html) * _Computational Higher Type Theory I: Abstract Cubical Realizability_, Carlo Angiuli, Robert Harper, Todd Wilson, [arxiv](https://arxiv.org/abs/1604.08873), 2016 * _Computational Higher Type Theory II: Dependent Cubical Realizability_, Carlo Angiuli, Robert Harper, [arxiv](https://arxiv.org/abs/1606.09638), 2016 ##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). * _Note on the construction of globular weak omega-groupoids from types, topological spaces etc_. John Bourke, [arXiv](http://arxiv.org/abs/1602.07962) * _The Homotopy Theory of Type Theories_. Chris Kapulkin and Peter LeFanu Lumsdaine, [arXiv](https://arxiv.org/abs/1610.00037). ##Strict equality types## * [[Homotopy type system]], Vladimir Voevodsky * _Extending Homotopy Type Theory with Strict Equality_, Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus, CSL 2016, [arXiv](http://arxiv.org/abs/1604.03799) * _Two-Level Type Theory and Applications_, Danil Annenkov, Paolo Capriotti, Nicolai Kraus, [arxiv](https://arxiv.org/abs/1705.03307) ##Directed type theory## * _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) * _A type theory for synthetic $\infty$-categories_. Emily Riehl, Michael Shulman. [arxiv](https://arxiv.org/abs/1705.07442) ##Cohesion and modalities## * _Quantum gauge field theory in cohesive homotopy type theory_. Urs Schreiber and Michael Shulman. [arxiv](https://arxiv.org/abs/1408.0054) * _Brouwer's fixed-point theorem in real-cohesive homotopy type theory_. Michael Shulman. To appear in MSCS; [arxiv](http://arxiv.org/abs/1509.07584) ##Theories and models## * _Homotopy Model Theory I: Syntax and Semantics_, Dimitris Tsementzis, [arXiv](http://arxiv.org/abs/1603.03092) ##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) ##Philosophy:## * _Structuralism, Invariance, and Univalence_. Steve Awodey. Philosophia Mathematica (2014) 22 (1): 1-11. [online](http://philmat.oxfordjournals.org/content/22/1/1.abstract) * _Identity in Homotopy Type Theory, Part I: The Justification of Path Induction_. James Ladyman and Stuart Presnell. Philosophia Mathematica (2015), [online](http://philmat.oxfordjournals.org/content/early/2015/06/01/philmat.nkv014.abstract#fn-2) * _Homotopy Type Theory: A synthetic approach to higher equalities_. Michael Shulman. To appear in _Categories for the working philosopher_; [arXiv](http://arxiv.org/abs/1601.05035) * _Univalent Foundations as Structuralist Foundations_. Dimitris Tsementzis. Forthcoming in _Synthese_; [Pitt-PhilSci] (http://philsci-archive.pitt.edu/12070/) * _Homotopy type theory: the logic of space_. Michael Shulman. To appear in _New Spaces in Mathematics and Physics_: [arxiv](https://arxiv.org/abs/1703.03007) ##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) * _Space-Valued Diagrams, Type-Theoretically (Extended Abstract)_. Nicolai Kraus and Christian Sattler. [arXiv](https://arxiv.org/abs/1704.04543)