References (Rev #61, changes)

Showing changes from revision #60 to #61:
Added | ~~Removed~~ | ~~Chan~~ged

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
- Synthetic homotopy theory
- Higher category theory
- Homotopical ideas and truncations in type theory
- General models
- Univalence
- Inductive and higher-inductive types
- Formalizations
- Applications to computing
- Cubical models and cubical type theory
- Syntax of type
~~theory:~~theory - Strict equality types
- Directed type theory
- Cohesion and modalities
- Theories and models
- Computational
~~interpretation:~~interpretation ~~Philosophy:~~Philosophy~~Other:~~Other

Steve Awodey, 2010. (To appear.) PDF~~Type theory and homotopy.~~Type theory and homotopy.?Álvaro Pelayo and Michael A. Warren, 2012. (Bulletin of the AMS, forthcoming) arXiv~~Homotopy type theory and Voevodsky’s univalent foundations.~~Homotopy type theory and Voevodsky's univalent foundations.?Steve Awodey, Álvaro Pelayo, and Michael A. Warren, October 2013, Notices of the American Mathematical Society 60(08), pp.1164-1167. arXiv~~Voevodsky’s Univalence Axiom in homotopy type theory.~~Voevodsky's Univalence Axiom in homotopy type theory.?*Homotopy Type Theory: A synthetic approach to higher equalities*. Michael Shulman. To appear in*Categories for the working philosopher*; arXivAnthony Bordg, 2017. PDF~~Univalent Foundations and the UniMath library.~~Univalent Foundations and the UniMath library.?*Homotopy type theory: the logic of space*. Michael Shulman. To appear in*New Spaces in Mathematics and Physics*: arxiv. Dan Grayson, arxiv~~An introduction to univalent foundations for mathematicians~~An introduction to univalent foundations for mathematicians?. Martín Escardó, web, arxiv~~A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom~~A self-contained, brief and complete formulation of Voevodsky's Univalence Axiom?. Steve Awodey. arxiv, 2017~~A proposition is the (homotopy) type of its proofs~~A proposition is the (homotopy) type of its proofs?*Homotopy Type Theory: Univalent Foundations of Mathematics*, The Univalent Foundations Program, Institute for Advanced Study, 2013. homotopytypetheory.org/book

See also Philosophy, below.

*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

*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*). Emily Riehl, Michael Shulman. arxiv, 2017~~A type theory for synthetic~~A type theory for synthetic $\infty$-categories?~~$\infty$~~~~-categories~~. Paolo Capriotti, Nicolai Kraus, arxiv, 2017~~Univalent Higher Categories via Complete Semi-Segal Types~~Univalent Higher Categories via Complete Semi-Segal Types?

. Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. TLCA 2013, pdf~~Generalizations of Hedberg?s Theorem~~Generalizations of Hedberg?s Theorem?. Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. pdf~~Notions of anonymous existence in Martin-Lof type theory~~Notions of anonymous existence in Martin-Lof type theory?. Michael Shulman, arXiv~~Idempotents in intensional type theory~~Idempotents in intensional type theory?. Paolo Capriotti, Nicolai Kraus, and Andrea Vezzosi. CSL 2015 arxiv~~Functions out of Higher Truncations~~Functions out of Higher Truncations?. Nicolai Kraus, PhD Thesis: University of Nottingham, 2015. pdf~~Truncation levels in homotopy type theory~~Truncation levels in homotopy type theory?. Auke Bart Booij?, Martín Hötzel Escardó, Peter LeFanu Lumsdaine, Michael Shulman. arxiv~~Parametricity, automorphisms of the universe, and excluded middle~~Parametricity, automorphisms of the universe, and excluded middle?

*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

*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?~~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 Types in Homotopy Type Theory.~~Inductive Types in Homotopy Type Theory.?~~S.~~~~Awodey,~~~~N.~~~~Gambino,~~~~K.~~~~Sojakova.~~~~To~~~~appear~~~~in~~~~LICS~~~~2012.~~S. Awodey, N. Gambino, K. Sojakova. To appear in LICS 2012. arXiv.~~W-types in homotopy type theory~~W-types in homotopy type theory?~~Benno~~~~van~~~~den~~~~Berg~~~~and~~~~Ieke~~~~Moerdijk,~~Benno van den Berg and Ieke Moerdijk?, arXiv~~Homotopy-initial algebras in type theory~~Homotopy-initial algebras in type theory?~~Steve~~~~Awodey,~~~~Nicola~~~~Gambino,~~~~Kristina~~~~Sojakova.~~Steve Awodey, Nicola Gambino, Kristina Sojakova. arXiv, Coq code.~~The General Universal Property of the Propositional Truncation~~The General Universal Property of the Propositional Truncation?~~Nicolai~~~~Kraus,~~Nicolai Kraus, arXiv.~~Non-wellfounded trees in Homotopy Type Theory~~Non-wellfounded trees in Homotopy Type Theory?~~Benedikt~~~~Ahrens,~~~~Paolo~~~~Capriotti,~~~~Régis~~~~Spadotti.~~~~TLCA~~~~2015,~~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~~Constructing the Propositional Truncation using Non-recursive HITs?~~Floris~~~~van~~~~Doorn,~~Floris van Doorn, arXiV.~~Constructions with non-recursive higher inductive types~~Constructions with non-recursive higher inductive types?~~Nicolai~~~~Kraus,~~~~LiCS~~~~2016,~~Nicolai Kraus, LiCS 2016, pdf.~~The join construction~~The join construction~~Egbert~~~~Rijke,~~Egbert Rijke, arXiv.~~Semantics of higher inductive types~~Semantics of higher inductive types?~~Michael~~~~Shulman~~~~and~~~~Peter~~~~LeFanu~~~~Lumsdaine,~~Michael Shulman and Peter LeFanu Lumsdaine, arXiv,~~A Descent Property for the Univalent Foundations~~A Descent Property for the Univalent Foundations?~~Egbert~~~~Rijke,~~Egbert Rijke, doi.~~Impredicative Encodings of (Higher) Inductive Types~~Impredicative Encodings of (Higher) Inductive Types?~~Steve~~~~Awodey,~~~~Jonas~~~~Frey,~~~~and~~~~Sam~~~~Speight.~~Steve Awodey, Jonas Frey?, and Sam Speight?. arxiv, 2018,~~W-Types with Reductions and the Small Object Argument~~W-Types with Reductions and the Small Object Argument?~~Andrew~~~~Swan,~~Andrew Swan?, arxiv

*An experimental library of formalized Mathematics based on the univalent foundations?*,*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,*A preliminary univalent formalization of the p-adic numbers.*Álvaro Pelayo, Vladimir Voevodsky, Michael A. Warren, 2012. arXiv*Univalent categories and the Rezk completion*.*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*)*internal categories in HoTT*)*The HoTT Library: A formalization of homotopy type theory in Coq*,*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

*Homotopical patch theory*.~~Carlo~~~~Angiuli,~~~~Ed~~~~Morehouse,~~~~Dan~~~~Licata,~~~~Robert~~~~Harper,~~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,~~Lars Birkedal?, Ale? Bizjak?, Ranald Clouston?, Hans Bugge Grathwohl?, Bas Spitters, Andrea Vezzosi, arXiv

. Dan Licata and Guillaume Brunerie, LICS 2015, PDF~~A Cubical Approach to Synthetic Homotopy Theory~~A Cubical Approach to Synthetic Homotopy Theory. Thorsten Altenkirch and Ambrus Kaposi?, PDF~~A syntax for cubical type theory~~A syntax for cubical type theory?, github~~Implementation of Univalence in Cubical Sets~~Implementation of Univalence in Cubical Sets?, Robert Harper and Kuen-Bang Hou. arXiv~~A Note on the Uniform Kan Condition in Nominal Cubical Sets~~A Note on the Uniform Kan Condition in Nominal Cubical Sets?, Nicola Gambino, Christian Sattler?. (Note: this is a duplicate of an entry in the section “General Models” above; accident?) arXiv~~The Frobenius Condition, Right Properness, and Uniform Fibrations~~The Frobenius Condition, Right Properness, and Uniform Fibrations?*Cubical Type Theory: a constructive interpretation of the univalence axiom*, Cyril Cohen?, Thierry Coquand, Simon Huber, and Anders Mortberg, arxiv and github implementation, Simon Huber, arxiv.~~Canonicity for cubical type theory~~Canonicity for cubical type theory?, Andrew M. Pitts, pdf~~Nominal Presentation of Cubical Sets Models of Type Theory~~Nominal Presentation of Cubical Sets Models of Type Theory?, Ian Orton and Andrew M. Pitts, pdf Agda code~~Axioms for Modelling Cubical Type Theory in a Topos~~Axioms for Modelling Cubical Type Theory in a Topos?*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. Marc Bezem?, Thierry Coquand, Simon Huber. arxiv, 2017~~The univalence axiom in cubical sets~~The univalence axiom in cubical sets?. Steve Awodey. arxiv, 2016~~A Cubical Model of Homotopy Type Theory~~A Cubical Model of Homotopy Type Theory?,~~Cartesian Cubical Computational Type Theory~~Cartesian Cubical Computational Type Theory?~~Carlo Angiuli, [[Favonia?~~Carlo Angiuli, Favonia, Robert Harper. pdf

*The identity type weak factorisation system.*Nicola Gambino and Richard Garner, Theoretical Computer Science 409 (2008), no. 3, pages 94?109. RG?s websiteRichard Garner and Benno van den Berg, to appear. RG?s website~~Types are weak ∞-groupoids.~~Types are weak ∞-groupoids.?Peter LeFanu Lumsdaine, TLCA 2009, Brasília, Logical Methods in Computer Science, Vol. 6, issue 23, paper 24. PDF~~Weak ∞-Categories from Intensional Type Theory.~~Weak ∞-Categories from Intensional Type Theory.?Peter LeFanu Lumsdaine, PhD Thesis: Carnegie Mellon University, 2010. PDF~~Higher Categories from Type Theories.~~Higher Categories from Type Theories.?*A coherence theorem for Martin-Löf?s type*Michael Hedberg?, Journal of Functional Programming 8 (4): 413?436, July 1998.~~theory.~~theory.]]P. LeFanu Lumsdaine. Unpublished note, Dec. 2011. PDF~~Model Structures from Higher Inductive Types.~~Model Structures from Higher Inductive Types.?. Jacopo Emmenegger?, arXiv~~A category-theoretic version of the identity type weak factorization system~~A category-theoretic version of the identity type weak factorization system?. Chris Kapulkin, arXiv.~~Locally cartesian closed quasicategories from type theory~~Locally cartesian closed quasicategories from type theory?. John Bourke?, arXiv~~Note on the construction of globular weak omega-groupoids from types, topological spaces etc~~Note on the construction of globular weak omega-groupoids from types, topological spaces etc?. Chris Kapulkin and Peter LeFanu Lumsdaine, arXiv.~~The Homotopy Theory of Type Theories~~The Homotopy Theory of Type Theories?. Steve Awodey and Clive Newstead?. arxiv, 2018~~Polynomial Pseudomonads and Dependent Type Theory~~Polynomial Pseudomonads and Dependent Type Theory?

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

Dan Licata and Robert Harper. MFPS 2011. See also Chapters 7 and 8 of Dan?s thesis. PDF~~2-Dimensional Directed Dependent Type Theory.~~2-Dimensional Directed Dependent Type Theory.?. Emily Riehl, Michael Shulman. arxiv~~A type theory for synthetic~~A type theory for synthetic $\infty$-categories?~~$\infty$~~~~-categories~~

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

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

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

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

~~Martin-Löf Complexes.~~Martin-Löf Complexes?.~~S.~~~~Awodey,~~~~P.~~~~Hofstra~~~~and~~~~M.A.~~~~Warren,~~~~2013,~~~~Annals~~~~of~~~~Pure~~~~and~~~~Applied~~~~Logic,~~~~164(10),~~~~pp.~~~~928-956.~~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)~~Space-Valued Diagrams?, Type-Theoretically (Extended Abstract)~~Nicolai~~~~Kraus~~~~and~~~~Christian~~~~Sattler.~~Nicolai Kraus and Christian Sattler?. arXiv

category: references

Revision on October 10, 2018 at 15:04:13 by Ali Caglayan. See the history of this page for a list of all contributions to it.