Homotopy Type Theory References > history (Rev #59, changes)

Showing changes from revision #58 to #59: 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!

Surveys

• Type theory and homotopy. Steve Awodey, 2010. (To appear.)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)Á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.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 inMichael Shulman. To appear in Categories for the working philosopher; arXiv
• Univalent Foundations and the UniMath library. Anthony Bordg, 2017.Anthony Bordg, 2017. PDF
• Homotopy type theory: the logic of space . Michael Shulman. To appear inMichael Shulman. To appear in New Spaces in Mathematics and Physics: arxiv
• An introduction to univalent foundations for mathematicians . Dan Grayson,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.Steve Awodey. arxiv, 2017

See also Philosophy, below.

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).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.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.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.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).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.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.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.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.Steve Awodey, 2015. arXiv
• Subsystems and regular quotients of C-systems , Vladimir Voevodsky, 2014.Vladimir Voevodsky, 2014. arXiv
• C-system of a module over a monad on sets , Vladimir Voevodsky, 2014.Vladimir Voevodsky, 2014. arXiv
• A C-system defined by a universe category , Vladimir Voevodsky, 2014.Vladimir Voevodsky, 2014. arXiv
• B-systems , Vladimir Voevodsky, 2014.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.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.Vladimir Voevodsky, 2015. arXiv
• Martin-Lof identity types in the C-systems defined by a universe category , Vladimir Voevodsky, 2015.Vladimir Voevodsky, 2015. arXiv
• The Frobenius Condition, Right Properness, and Uniform Fibrations , Nicola Gambino, Christian Sattler.Nicola Gambino, Christian Sattler?. arXiv
• Fibred fibration categories , Taichi Uemura, 2016,Taichi Uemura, 2016, arXiv
• A homotopy-theoretic model of function extensionality in the effective topos , Daniil Frumin, Benno van den Berg,Daniil Frumin?, Benno van den Berg, arxiv
• Polynomial pseudomonads and dependent type theory , Steve Awodey, Clive Newstead, 2018,Steve Awodey, Clive Newstead?, 2018, arxiv
• Towards a Topological Model of Homotopy Type Theory , Paige North,Paige North, doi
• The Equivalence Extension Property and Model Structures , Christian Sattler,Christian Sattler?, arxiv
• Univalent polymorphism , Benno van den Berg,Benno van den Berg, arxiv

Univalence

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

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
• 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
• The join construction. Egbert Rijke, 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. 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

Synthetic homotopy theory

• Calculating the fundamental group of the circle in homotopy type theoryCalculating the fundamental group of the circle in homotopy type theory . Dan Licata and Michael Shulman, LICS 2013, availableDan Licata and Michael Shulman, LICS 2013, available here and on arXiv
• $\pi_n(S^n)$$\pi_n(S^n)$ in Homotopy Type Theory in Homotopy Type Theory , Dan Licata and Guillaume Brunerie, Invited Paper, CPP 2013,Dan Licata and Guillaume Brunerie, Invited Paper, CPP 2013, PDF
• Homotopy limits in type theoryHomotopy limits in type theory . Jeremy Avigad, Chris Kapulkin, Peter LeFanu Lumsdaine, Math. Structures Comput. Sci. 25 (2015), no. 5, 1040?1070.Jeremy Avigad, Chris Kapulkin, Peter LeFanu Lumsdaine, Math. Structures Comput. Sci. 25 (2015), no. 5, 1040?1070. arXiv
• Eilenberg-MacLane Spaces in Homotopy Type TheoryEilenberg-MacLane Spaces in Homotopy Type Theory . Dan Licata and Eric Finster, LICS 2014,Dan Licata and Eric Finster, LICS 2014, PDF and code
• A Cubical Approach to Synthetic Homotopy TheoryA Cubical Approach to Synthetic Homotopy Theory . Dan Licata and Guillaume Brunerie, LICS 2015,Dan Licata and Guillaume Brunerie, LICS 2015, PDF
• Synthetic Cohomology in Homotopy Type TheorySynthetic Cohomology in Homotopy Type Theory , Evan Cavallo,Evan Cavallo, PDF
• A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type TheoryA mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory , LICS 2016 Kuen-Bang Hou (Favonia), Eric Finster, Dan Licata, Peter LeFanu Lumsdaine,Kuen-Bang Hou (Favonia), Eric Finster, Dan Licata, Peter LeFanu Lumsdaine, arXiv
• The Seifert-van Kampen Theorem in Homotopy Type TheoryThe Seifert-van Kampen Theorem in Homotopy Type Theory? , Kuen-Bang Hou and Michael Shulman,Kuen-Bang Hou and Michael Shulman, PDF
• On the homotopy groups of spheres in homotopy type theoryOn the homotopy groups of spheres in homotopy type theory , Guillaume Brunerie, Ph.D. Thesis, 2016,Guillaume Brunerie, Ph.D. Thesis, 2016, arxiv
• The real projective spaces in homotopy type theoryThe real projective spaces in homotopy type theory , Ulrik Buchholtz and Egbert Rijke, LICS 2017,Ulrik Buchholtz and Egbert Rijke, LICS 2017, arxiv
• Covering Spaces in Homotopy Type TheoryCovering Spaces in Homotopy Type Theory , Kuen-Bang Hou (Favonia),Kuen-Bang Hou (Favonia), doi
• Higher Groups in Homotopy Type TheoryHigher Groups in Homotopy Type Theor?y , Ulrik Buchholtz, Floris van Doorn, Egbert Rijke,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

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,Dan Licata and Guillaume Brunerie, LICS 2015, PDF
• A syntax for cubical type theory . Thorsten Altenkirch and Ambrus Kaposi,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.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?)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,Cyril Cohen?, Thierry Coquand, Simon Huber, and Anders Mortberg, arxiv and github implementation
• Canonicity for cubical type theory , Simon Huber,Simon Huber, arxiv.
• Nominal Presentation of Cubical Sets Models of Type Theory , Andrew M. Pitts,Andrew M. Pitts, pdf
• Axioms for Modelling Cubical Type Theory in a Topos , Ian Orton and Andrew M. Pitts,Ian Orton and Andrew M. Pitts, pdf Agda code
• Computational Higher Type Theory I: Abstract Cubical Realizability , Carlo Angiuli, Robert Harper, Todd Wilson,Carlo Angiuli, Robert Harper, Todd Wilson?, arxiv, 2016
• Computational Higher Type Theory II: Dependent Cubical Realizability , Carlo Angiuli, Robert Harper,Carlo Angiuli, Robert Harper, arxiv, 2016
• The univalence axiom in cubical sets . Marc Bezem, Thierry Coquand, Simon Huber.Marc Bezem?, Thierry Coquand, Simon Huber. arxiv, 2017
• A Cubical Model of Homotopy Type Theory . Steve Awodey.Steve Awodey. arxiv, 2016
• Cartesian Cubical Computational Type Theory , Carlo Angiuli, Favonia, Robert Harper.Carlo Angiuli, [[Favonia?, Robert Harper. pdf

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

Strict equality types

• Homotopy Type System , Vladimir VoevodskyVladimir Voevodsky
• Extending Homotopy Type Theory with Strict Equality , Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus, CSL 2016,Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus, CSL 2016, arXiv
• Two-Level Type Theory and Applications , Danil Annenkov, Paolo Capriotti, Nicolai Kraus,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 ofDan 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.Emily Riehl, Michael Shulman. arxiv

Cohesion and modalities

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

Theories and models

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

Computational interpretation:

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

Philosophy:

• Structuralism, Invariance, and Univalence . Steve Awodey. Philosophia Mathematica (2014) 22 (1): 1-11.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),James Ladyman and Stuart Presnell. Philosophia Mathematica (2015), online
• Homotopy Type Theory: A synthetic approach to higher equalities . Michael Shulman. To appear inMichael Shulman. To appear in Categories for the working philosopher; arXiv
• Univalent Foundations as Structuralist Foundations . Dimitris Tsementzis. Forthcoming inDimitris Tsementzis. Forthcoming in Synthese; Pitt-PhilSci
• Homotopy type theory: the logic of space . Michael Shulman. To appear inMichael 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

category: references