Homotopy Type Theory References > history (Rev #78)

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!

A good place to start

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
• Homotopy Type Theory: A synthetic approach to higher equalities. Michael Shulman. To appear in Categories for the working philosopher; arXiv
• Univalent Foundations and the UniMath library. Anthony Bordg, 2017. PDF
• Homotopy type theory: the logic of space. Michael Shulman. To appear in New Spaces in Mathematics and Physics: arxiv
• An introduction to univalent foundations for mathematicians. Dan Grayson, arxiv
• A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom. Martín Escardó, web, arxiv
• A proposition is the (homotopy) type of its proofs. Steve Awodey. arxiv, 2017
• Introduction to Univalent Foundations of Mathematics with Agda. Martín Escardó,web, arxiv, 2019
• Introduction to Homotopy Type Theory. Egbert Rijke, to appear 2021
• Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study, 2013. homotopytypetheory.org/book

See also Philosophy, below.

Synthetic homotopy theory

• Calculating the fundamental group of the circle in homotopy type theory. Dan Licata and Michael Shulman, LICS 2013, available here and on arXiv
• $\pi_n(S^n)$ in Homotopy Type Theory, Dan Licata and Guillaume Brunerie, Invited Paper, CPP 2013, PDF
• Homotopy limits in type theory. Jeremy Avigad, Chris Kapulkin, Peter LeFanu Lumsdaine, Math. Structures Comput. Sci. 25 (2015), no. 5, 1040?1070. arXiv
• Eilenberg-MacLane Spaces in Homotopy Type Theory. Dan Licata and Eric Finster, LICS 2014, PDF and code
• A Cubical Approach to Synthetic Homotopy Theory. Dan Licata and Guillaume Brunerie, LICS 2015, PDF
• Synthetic Cohomology in Homotopy Type Theory, Evan 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
• The Seifert-van Kampen Theorem in Homotopy Type Theory?, Kuen-Bang Hou and Michael Shulman, PDF
• On the homotopy groups of spheres in homotopy type theory, Guillaume Brunerie, Ph.D. Thesis, 2016, arxiv
• The real projective spaces in homotopy type theory, Ulrik Buchholtz and Egbert Rijke, LICS 2017, arxiv
• Covering Spaces in Homotopy Type Theory, Kuen-Bang Hou (Favonia), doi
• Higher Groups in Homotopy Type Theory, Ulrik Buchholtz, Floris van Doorn, Egbert Rijke, arXiv:1802.04315
• On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory, Floris van Doorn, Ph.D. Thesis 2018 arXiv:1808.10690
• Localization in Homotopy Type Theory, J. Daniel Christensen, Morgan Opie, Egbert Rijke, Luis Scoccola, arXiv:1807.04155
• Cellular Cohomology in Homotopy Type Theory, Ulrik Buchholtz, Kuen-Bang Hou (Favonia), arXiv:1802.02191
• The join construction. Egbert Rijke, arXiv:1701.07538
• Nilpotent Types and Fracture Squares in Homotopy Type Theory?. Luis Scoccola, arXiv:1903.03245

Higher category theory

• 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 (on internal categories in HoTT)
• A type theory for synthetic $\infty$-categories?. Emily Riehl, Michael Shulman. arxiv, 2017
• Univalent Higher Categories via Complete Semi-Segal Types?. Paolo Capriotti, Nicolai Kraus, arxiv, 2017
• Bicategories in Univalent Foundations?, Benedikt Ahrens, Dan Frumin?, Marco Maggesi?, Niels van der Weide?, arXiv:1903.01152

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
• Notions of anonymous existence in Martin-Lof type theory?. Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. pdf
• Idempotents in intensional type theory?. Michael Shulman, arXiv
• Functions out of Higher Truncations?. Paolo Capriotti, Nicolai Kraus, and Andrea Vezzosi. CSL 2015 arxiv
• Truncation levels in homotopy type theory?. Nicolai Kraus, PhD Thesis: University of Nottingham, 2015. pdf
• Parametricity, automorphisms of the universe, and excluded middle?. Auke Bart Booij?, Martín Hötzel Escardó, Peter LeFanu Lumsdaine, Michael Shulman. 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. arXiv
• 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
• Natural models of homotopy type theory, Steve Awodey, 2015. arXiv
• Subsystems and regular quotients of C-systems, Vladimir Voevodsky, 2014. arXiv
• C-system of a module over a monad on sets, Vladimir Voevodsky, 2014. arXiv
• A C-system defined by a universe category, Vladimir Voevodsky, 2014. arXiv
• B-systems, Vladimir Voevodsky, 2014. arXiv
• 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
• Products of families of types in the C-systems defined by a universe category, Vladimir Voevodsky, 2015. arXiv
• Martin-Lof identity types in the C-systems defined by a universe category, Vladimir Voevodsky, 2015. arXiv
• The Frobenius Condition, Right Properness, and Uniform Fibrations, Nicola Gambino, Christian Sattler?. arXiv
• Fibred fibration categories, Taichi Uemura, 2016, arXiv
• A homotopy-theoretic model of function extensionality in the effective topos, Daniil Frumin?, Benno van den Berg, arxiv
• Polynomial pseudomonads and dependent type theory, Steve Awodey, Clive Newstead?, 2018, arxiv
• Towards a Topological Model of Homotopy Type Theory, Paige North, doi
• The Equivalence Extension Property and Model Structures, Christian Sattler?, arxiv
• Univalent polymorphism, Benno van den Berg, arxiv
• All (∞,1)-toposes have strict univalent universes, Mike Shulman, arXiv:1904.07004

Univalence

• The equivalence axiom and univalent models of type theory (talk at CMU, February 4th, 2010), Vladimir Voevodsky. arXiv
• Univalence in simplicial sets. Chris Kapulkin, Peter LeFanu Lumsdaine, Vladimir Voevodsky. arXiv
• Univalence for inverse diagrams and homotopy canonicity. 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
• The univalence axiom for elegant Reedy presheaves. Michael Shulman, arXiv
• Univalent universes for elegant models of homotopy types. Denis-Charles Cisinski, arXiv
• A univalent universe in finite order arithmetic. Colin McLarty?, arXiv
• Constructive Simplicial Homotopy. Wouter Pieter Stekelenburg, arXiv
• Higher Homotopies in a Hierarchy of Univalent Universes. Nicolai Kraus and Christian Sattler?, arXiv, DOI
• Univalence for inverse EI diagrams. Michael Shulman, arXiv
• Univalent completion. Benno van den Berg, Ieke Moerdijk?, arXiv
• On lifting univalence to the equivariant setting. Anthony Bordg, arXiv
• Univalence in locally cartesian closed $\infty$-categories. David Gepner? and Joachim Kock?. Forum Math. 29 (2017), no. 3, 617–652

Inductive, coinductive, and higher-inductive types

• Inductive Types in Homotopy Type Theory. S. Awodey, N. Gambino, K. Sojakova. To appear in LICS 2012. arXiv
• W-types in homotopy type theory. Benno van den Berg and Ieke Moerdijk?, arXiv
• Homotopy-initial algebras in type theory Steve Awodey, Nicola Gambino, Kristina Sojakova. arXiv, Coq code
• The General Universal Property of the Propositional Truncation. Nicolai Kraus, arXiv
• Non-wellfounded trees in Homotopy Type Theory. Benedikt Ahrens, Paolo Capriotti, Régis Spadotti?. TLCA 2015, doi:10.4230/LIPIcs.TLCA.2015.17, arXiv
• Constructing the Propositional Truncation using Non-recursive HITs. Floris van Doorn, arXiV
• Constructions with non-recursive higher inductive types. Nicolai Kraus, LiCS 2016, pdf
• Semantics of higher inductive types. Michael Shulman and Peter LeFanu Lumsdaine, arXiv
• A Descent Property for the Univalent Foundations, Egbert Rijke, doi
• Impredicative Encodings of (Higher) Inductive Types. Steve Awodey, Jonas Frey?, and Sam Speight?. arxiv, 2018
• W-Types with Reductions and the Small Object Argument, Andrew Swan?, arxiv
• Bisimulation as path type for guarded recursive types, Rasmus Ejlers Møgelberg?, Niccolò Veltri?, arxiv
• Signatures and Induction Principles for Higher Inductive-Inductive Types?, Ambrus Kaposi?, András Kovács? arXiv:1902.00297

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 journal
• A preliminary univalent formalization of the p-adic numbers.? Álvaro Pelayo, Vladimir Voevodsky, Michael A. Warren, 2012. arXiv
• 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 (on 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

Applications to computing

• Homotopical patch theory. Carlo Angiuli, Ed Morehouse, Dan Licata, Robert Harper, PDF
• Guarded Cubical Type Theory: Path Equality for Guarded Recursion, Lars Birkedal?, Ale? Bizjak?, Ranald Clouston?, Hans Bugge Grathwohl?, Bas Spitters, Andrea Vezzosi, arXiv

Cubical models and cubical type theory

• A Cubical Approach to Synthetic Homotopy Theory. Dan Licata and Guillaume Brunerie, LICS 2015, PDF
• A syntax for cubical type theory. Thorsten Altenkirch and Ambrus Kaposi?, PDF
• Implementation of Univalence in Cubical Sets, github
• A Note on the Uniform Kan Condition in Nominal Cubical Sets, Robert Harper and Kuen-Bang Hou. arXiv
• 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
• Cubical Type Theory: a constructive interpretation of the univalence axiom, Cyril Cohen?, Thierry Coquand, Simon Huber, and Anders Mortberg, arxiv and github implementation
• Canonicity for cubical type theory, Simon Huber, arxiv.
• Nominal Presentation of Cubical Sets Models of Type Theory]], Andrew M. Pitts, pdf
• Axioms for Modelling Cubical Type Theory in a Topos, Ian Orton and Andrew M. Pitts, pdf Agda code
• Computational Higher Type Theory I: Abstract Cubical Realizability, Carlo Angiuli, Robert Harper, Todd Wilson?, arxiv, 2016
• Computational Higher Type Theory II: Dependent Cubical Realizability, Carlo Angiuli, Robert Harper, arxiv, 2016
• Computational Higher Type Theory III: Univalent Universes and Exact Equality, Carlo Angiuli, Kuen-Bang Hou, Robert Harper, arxiv, 2017
• Computational Higher Type Theory IV: Inductive Types, Evan Cavallo, Robert Harper, arxiv, 2018
• The univalence axiom in cubical sets. Marc Bezem?, Thierry Coquand, Simon Huber. arxiv, 2017
• A Cubical Model of Homotopy Type Theory. Steve Awodey. arxiv, 2016
• Cartesian Cubical Computational Type Theory, Carlo Angiuli, Favonia, Robert Harper. pdf
• On Higher Inductive Types in Cubical Type Theory, Thierry Coquand, Simon Huber, Andes Mortberg?, arxiv, 2018
• Homotopy canonicity for cubical type theory, Thierry Coquand, Simon Huber, Christian Sattler?, arXiv, 2019

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.
• Model Structures from Higher Inductive Types. P. LeFanu Lumsdaine. Unpublished note, Dec. 2011. PDF
• A category-theoretic version of the identity type weak factorization system. Jacopo Emmenegger?, arXiv
• Locally cartesian closed quasicategories from type theory. Chris Kapulkin, arXiv.
• Note on the construction of globular weak omega-groupoids from types, topological spaces etc. John Bourke?, arXiv
• The Homotopy Theory of Type Theories. Chris Kapulkin and Peter LeFanu Lumsdaine, arXiv.
• Polynomial Pseudomonads and Dependent Type Theory. Steve Awodey and Clive Newstead?. arxiv, 2018

Strict equality types

• Homotopy Type System, Vladimir Voevodsky
• Extending Homotopy Type Theory with Strict Equality?, Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus, CSL 2016, arXiv
• Two-Level Type Theory and Applications?, Danil Annenkov?, Paolo Capriotti, Nicolai Kraus, arxiv, 2017

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. PDF
• A type theory for synthetic $\infty$-categories?. Emily Riehl, Michael Shulman. arxiv
• Synthetic fibered (∞,1)-category theory. Ulrik Buchholtz, Jonathan Weinberger. arxiv, 2021.
• Limits and colimits of synthetic ∞-categories. César Bardomiano Martínez. arxiv, 2022.
• A Synthetic Perspective on (∞,1)-Category Theory: Fibrational and Semantic Aspects. Jonathan Weinberger. PhD Thesis; arxiv, 2022.
• Two-sided cartesian fibrations of synthetic (∞,1)-categories. Jonathan Weinberger, arxiv.

Cohesion and modalities

• Quantum gauge field theory in cohesive homotopy type theory?. Urs Schreiber and Michael Shulman. arxiv
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory?. Michael Shulman. To appear in MSCS; arxiv
• Modalities in homotopy type theory. Egbert Rijke, Michael Shulman, Bas Spitters. arxiv

Theories and models

• Homotopy Model Theory I: Syntax and Semantics, Dimitris Tsementzis, arXiv

Computational interpretation

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

Philosophy

• Structuralism, Invariance, and Univalence. Steve Awodey. Philosophia Mathematica (2014) 22 (1): 1-11. online
• Identity in Homotopy Type Theory, Part I: The Justification of Path Induction. James Ladyman and Stuart Presnell. Philosophia Mathematica (2015), online
• Homotopy Type Theory: A synthetic approach to higher equalities. Michael Shulman. To appear in Categories for the working philosopher; arXiv
• Univalent Foundations as Structuralist Foundations. Dimitris Tsementzis. Forthcoming in Synthese; Pitt-PhilSci
• Homotopy type theory: the logic of space. Michael Shulman. To appear in New Spaces in Mathematics and Physics: arxiv

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
• Space-Valued Diagrams, Type-Theoretically (Extended Abstract). Nicolai Kraus and Christian Sattler?. arXiv
• Homotopy and Type Theory (Project description). S. Awodey, 2009. Unpublished grant proposal. HoTT proposal 2009.