Showing changes from revision #57 to #58:
Added | Removed | Changed
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!
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
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 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
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
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
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. arXivjournal
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
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
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
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
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, pdfAgda 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
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
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
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
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
Revision on September 28, 2018 at 11:34:25 by
Richard Williamson?.
See the history of this page for a list of all contributions to it.