Showing changes from revision #64 to #65:
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!
Homotopy type theory and Voevodsky's univalent foundations.?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.?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.?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?An introduction to univalent foundations for mathematicians. Dan Grayson, 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. Martín Escardó, web, arxiv
A proposition is the (homotopy) type of its proofs?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 theoryMichael 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
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
Constructing the Propositional Truncation using Non-recursive HITs?Constructing the Propositional Truncation using Non-recursive HITs. Floris van Doorn, arXiV
Constructions with non-recursive higher inductive types?Constructions with non-recursive higher inductive types. Nicolai Kraus, LiCS 2016, pdf
A Descent Property for the Univalent Foundations?Impredicative Encodings of (Higher) Inductive Types , . Egbert Steve Rijke Awodey, doiJonas Frey?, and Sam Speight?. arxiv, 2018
Impredicative Encodings of (Higher) Inductive Types?W-Types with Reductions and the Small Object Argument . ,Steve AwodeyAndrew Swan?, Jonas Frey?arxiv, and Sam Speight?. arxiv, 2018
W-Types with Reductions and the Small Object Argument?Bisimulation as path type for guarded recursive types , Rasmus Ejlers Møgelberg, Niccolò Veltri,Andrew Swan?arxiv, arxiv
Bisimulation Signatures as and path Induction type Principles for guarded Higher recursive Inductive-Inductive types Types? , Rasmus Ejlers Møgelberg, Niccolò Veltri,arxivAmbrus Kaposi?, András Kovács?arXiv:1902.00297
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
Guarded Cubical Type Theory: Path Equality for Guarded Recursion, Lars Birkedal?, Ale? Bizjak?, Ranald Clouston?, Hans Bugge Grathwohl?, Bas Spitters, Andrea Vezzosi, arXiv
A syntax for cubical type theory?A syntax for cubical type theory. Thorsten Altenkirch and Ambrus Kaposi?, PDF
Implementation of Univalence in Cubical Sets?Implementation of Univalence in Cubical Sets, github
A Note on the Uniform Kan Condition in Nominal Cubical Sets?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?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
On Higher Inductive Types in Cubical Type Theory?On Higher Inductive Types in Cubical Type Theory, , Thierry Coquand, Simon Huber, Andes Mortberg?, arxiv, 2018
Weak ∞-Categories from Intensional Type Theory.?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.?Higher Categories from Type Theories.Peter LeFanu Lumsdaine, PhD Thesis: Carnegie Mellon University, 2010. PDF
Model Structures from Higher Inductive Types.?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?A category-theoretic version of the identity type weak factorization system. Jacopo Emmenegger?, arXiv
Locally cartesian closed quasicategories from type theory?Locally cartesian closed quasicategories from type theory. Chris Kapulkin, 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. John Bourke?, arXiv
Canonicity for 2-Dimensional Type Theory.?Canonicity for 2-Dimensional Type Theory.Dan Licata and Robert Harper. POPL 2012. PDF
Philosophy
Structuralism, Invariance, and Univalence?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
A synthetic approach to higher equalities?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?Univalent Foundations as Structuralist Foundations. Dimitris Tsementzis. Forthcoming in Synthese; Pitt-PhilSci
the logic of space?Homotopy type theory: the logic of space. Michael Shulman. To appear in New Spaces in Mathematics and Physics: arxiv