Homotopy Type Theory References > history (Rev #18)

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
  • 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. 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
  • Uniform Fibrations and the Frobenius Condition, Nicola Gambino, Christian Sattler, 2015. arXiv
  • Fibred fibration categories, Taichi Uemura, 2016, arXiv

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

Inductive 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

Formalizations of set-level mathematics

  • 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

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
  • 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, PDF and code

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
  • Idempotents in intensional type theory. Michael Shulman, arXiv

Applications to computing

  • Homotopical patch theory. Carlo Angiuli, Ed Morehouse, Dan Licata, Robert Harper, PDF

Cubical models and cubical type theory

  • A Cubical Approach to Synthetic Homotopy Theory. Dan Licata and Guillaume Brunerie, 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
  • Uniform Fibrations and the Frobenius Condition, Nicola Gambino, Christian Sattler. 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.
  • 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

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

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
  • 2-Dimensional Directed Dependent Type Theory. Dan Licata and Robert Harper. MFPS 2011. See also Chapters 7 and 8 of Dan?s thesis. PDF

Revision on April 19, 2016 at 18:13:13 by Mike Shulman. See the history of this page for a list of all contributions to it.