nLab
homotopy type theory - references
Contents
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
Contents
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 , 2017Introduction to Univalent Foundations of Mathematics with Agda . Martín Escardó,web , arxiv , 2019Introduction to Homotopy Type Theory . Egbert Rijke, to appear 2021Homotopy Type Theory: Univalent Foundations of Mathematics 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 π n ( S n ) \pi_n(S^n) 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 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-Dimensional Types in the Mechanization of Homotopy Theory , Kuen-Bang Hou (Favonia) , Ph. D. Thesis 2017, pdf 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 . Emily Riehl , Michael Shulman . arxiv , 2017Univalent Higher Categories via Complete Semi-Segal Types . Paolo Capriotti , Nicolai Kraus , arxiv , 2017Bicategories 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 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 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 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 . 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. Steve Awodey , Nicola Gambino , Kristina 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 , 2018W-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
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 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 , 2016Computational Higher Type Theory II: Dependent Cubical Realizability , Carlo Angiuli , Robert Harper , arxiv , 2016Computational Higher Type Theory III: Univalent Universes and Exact Equality , Carlo Angiuli , Kuen-Bang Hou , Robert Harper , arxiv , 2017Computational Higher Type Theory IV: Inductive Types , Evan Cavallo , Robert Harper , arxiv , 2018The univalence axiom in cubical sets . Marc Bezem , Thierry Coquand , Simon Huber . arxiv , 2017A Cubical Model of Homotopy Type Theory . Steve Awodey . arxiv , 2016Cartesian 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. Peter 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 . 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
Theories and models
Computational interpretation
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
Last revised on June 9, 2022 at 18:03:50.
See the history of this page for a list of all contributions to it.