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! * table of contents {:toc} ##Surveys## * _[[Type theory and homotopy.]]_ [[Steve Awodey]], 2010. (To appear.) [PDF](http://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf) * _[[Homotopy type theory and Voevodsky's univalent foundations.]]_ [[Álvaro Pelayo]] and [[Michael A. Warren]], 2012. (Bulletin of the AMS, forthcoming) [arXiv](http://arxiv.org/abs/1210.5658) * _[[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](http://arxiv.org/abs/1302.4731) * _Homotopy Type Theory: A synthetic approach to higher equalities_. [[Michael Shulman]]. To appear in _Categories for the working philosopher_; [arXiv](http://arxiv.org/abs/1601.05035) * _[[Univalent Foundations and the UniMath library.]]_ [[Anthony Bordg]], 2017. [PDF](https://drive.google.com/open?id=0B63Vr5tVwiAjdEJhSW03YXBNMVE) * _Homotopy type theory: the logic of space_. [[Michael Shulman]]. To appear in _New Spaces in Mathematics and Physics_: [arxiv](https://arxiv.org/abs/1703.03007) * _[[An introduction to univalent foundations for mathematicians]]_. [[Dan Grayson]], [arxiv](https://arxiv.org/abs/1711.01477) * _[[A self-contained, brief and complete formulation of Voevodsky's Univalence Axiom]]_. Martín Escardó, [web](http://www.cs.bham.ac.uk/~mhe/agda-new/UnivalenceFromScratch.html), [arxiv](https://arxiv.org/abs/1803.02294) * _[[A proposition is the (homotopy) type of its proofs]]_. [[Steve Awodey]]. [arxiv](https://arxiv.org/abs/1701.02024), 2017 * _[[HoTT book|Homotopy Type Theory: Univalent Foundations of Mathematics]]_, The Univalent Foundations Program, Institute for Advanced Study, 2013. [homotopytypetheory.org/book](http://homotopytypetheory.org/book) See also [Philosophy](#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](http://www.cs.cmu.edu/~drl/pubs.html) and on [arXiv](http://arxiv.org/abs/1301.3443) * _[[$\pi_n(S^n)$ in Homotopy Type Theory]]_, [[Dan Licata]] and [[Guillaume Brunerie]], Invited Paper, CPP 2013, [PDF](http://dlicata.web.wesleyan.edu/pubs/lb13cpp/lb13cpp.pdf) * _[[Homotopy limits in type theory]]_. [[Jeremy Avigad]], [[Chris Kapulkin]], [[Peter LeFanu Lumsdaine]], Math. Structures Comput. Sci. 25 (2015), no. 5, 1040?1070. [arXiv](http://arxiv.org/abs/1304.0680) * _[[Eilenberg-MacLane Spaces in Homotopy Type Theory]]_. [[Dan Licata]] and [[Eric Finster]], LICS 2014, [PDF](http://dlicata.web.wesleyan.edu/pubs/lf14em/lf14em.pdf) and [code](https://github.com/dlicata335/hott-agda/blob/master/homotopy/KGn.agda) * _[[A Cubical Approach to Synthetic Homotopy Theory]]_. [[Dan Licata]] and [[Guillaume Brunerie]], LICS 2015, [PDF](http://dlicata.web.wesleyan.edu/pubs/lb15cubicalsynth/lb15cubicalsynth.pdf) * _[[Synthetic Cohomology in Homotopy Type Theory]]_, [[Evan Cavallo]], [PDF](http://www.cs.cmu.edu/~rwh/theses/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](http://arxiv.org/abs/1605.03227) * _[[The Seifert-van Kampen Theorem in Homotopy Type Theory]]_, [[Kuen-Bang Hou]] and [[Michael Shulman]], [PDF]( http://www.cs.cmu.edu/~kuenbanh/files/vankampen.pdf) * _[[On the homotopy groups of spheres in homotopy type theory]]_, [[Guillaume Brunerie]], Ph.D. Thesis, 2016, [arxiv](https://arxiv.org/abs/1606.05916) * _[[The real projective spaces in homotopy type theory]]_, [[Ulrik Buchholtz]] and [[Egbert Rijke]], LICS 2017, [arxiv](https://arxiv.org/abs/1704.05770) * _[[Covering Spaces in Homotopy Type Theory]]_, [[Kuen-Bang Hou (Favonia)]], [doi](https://doi.org/10.1007/978-3-319-21284-5_15) * _[[Higher Groups in Homotopy Type Theory]]_, [[Ulrik Buchholtz]], [[Floris van Doorn]], [[Egbert Rijke]], [arXiv:1802.04315](https://arxiv.org/abs/1802.04315) * _[[On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory]]_, [[Floris van Doorn]], Ph.D. Thesis 2018 [arXiv:1808.10690](https://arxiv.org/abs/1808.10690) * _[[Localization in Homotopy Type Theory]]_, [[J. Daniel Christensen]], [[Morgan Opie]], [[Egbert Rijke]], [[Luis Scoccola]], [arXiv:1807.04155](https://arxiv.org/abs/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](http://arxiv.org/abs/1303.0584) (on _[[nLab:internal categories in HoTT]]_) * _[[A type theory for synthetic $\infty$-categories]]_. [[Emily Riehl]], [[Michael Shulman]]. [arxiv](https://arxiv.org/abs/1705.07442), 2017 * _[[Univalent Higher Categories via Complete Semi-Segal Types]]_. [[Paolo Capriotti]], [[Nicolai Kraus]], [arxiv](https://arxiv.org/abs/1707.03693), 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](http://www.cs.bham.ac.uk/~mhe/papers/hedberg.pdf) * _[[Notions of anonymous existence in Martin-Lof type theory]]_. [[Nicolai Kraus]], [[Martín Escardó]], [[Thierry Coquand]], and [[Thorsten Altenkirch]]. [pdf](http://www.cs.nott.ac.uk/~txa/publ/jhedberg.pdf) * _[[Idempotents in intensional type theory]]_. [[Michael Shulman]], [arXiv](http://arxiv.org/abs/1507.03634) * _[[Functions out of Higher Truncations]]_. [[Paolo Capriotti]], [[Nicolai Kraus]], and [[Andrea Vezzosi]]. CSL 2015 [arxiv](http://arxiv.org/abs/1507.01150) * _[[Truncation levels in homotopy type theory]]_. [[Nicolai Kraus]], PhD Thesis: University of Nottingham, 2015. [pdf](http://www.cs.nott.ac.uk/~psznk/docs/thesis_nicolai.pdf) * _[[Parametricity, automorphisms of the universe, and excluded middle]]_. [[Auke Bart Booij]], [[Martín Hötzel Escardó]], [[Peter LeFanu Lumsdaine]], [[Michael Shulman]]. [arxiv](https://arxiv.org/abs/1701.05617) ##General models## * [_The groupoid interpretation of type theory._](http://homotopytypetheory.org/references/hofmann-streicher-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](http://www.mathematik.tu-darmstadt.de/~streicher/venedig.ps.gz) * [_Homotopy theoretic models of identity types._](http://homotopytypetheory.org/references/awodey-warren-homotopy-theoretic-models-of-identity-types/) [[Steve Awodey]] and [[Michael Warren]], Mathematical Proceedings of the Cambridge Philosophical Society, 2009. [PDF](http://www.andrew.cmu.edu/user/awodey/preprints/homotopy.pdf) * _Homotopy theoretic aspects of constructive type theory._ [[Michael A. Warren]], Ph.D. thesis: Carnegie Mellon University, 2008. [PDF](http://mawarren.net/papers/phd.pdf) * _Two-dimensional models of type theory_, [[Richard Garner]], Mathematical Structures in Computer Science 19 (2009), no. 4, pages 687--736. [RG's website](http://web.science.mq.edu.au/~rgarner/Papers/2-LCCC.pdf) * _Topological and simplicial models of identity types._ [[Richard Garner]] and [[Benno van den Berg]], to appear in ACM Transactions on Computational Logic (TOCL). [PDF](http://tocl.acm.org/accepted/467garner.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](http://mawarren.net/papers/crmp1295.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](http://arxiv.org/abs/1208.5683) * _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](http://arxiv.org/abs/1205.5527) * _Natural models of homotopy type theory_, [[Steve Awodey]], 2015. [arXiv](http://arxiv.org/abs/1406.3219) * _Subsystems and regular quotients of C-systems_, [[Vladimir Voevodsky]], 2014. [arXiv](http://arxiv.org/abs/1406.7413) * _C-system of a module over a monad on sets_, [[Vladimir Voevodsky]], 2014. [arXiv](http://arxiv.org/abs/1407.3394) * _A C-system defined by a universe category_, [[Vladimir Voevodsky]], 2014. [arXiv](http://arxiv.org/abs/1409.7925) * _B-systems_, [[Vladimir Voevodsky]], 2014. [arXiv](http://arxiv.org/abs/1410.5389) * _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](http://arxiv.org/abs/1411.1736) * _Products of families of types in the C-systems defined by a universe category_, [[Vladimir Voevodsky]], 2015. [arXiv](http://arxiv.org/abs/1503.07072) * _Martin-Lof identity types in the C-systems defined by a universe category_, [[Vladimir Voevodsky]], 2015. [arXiv](http://arxiv.org/abs/1505.06446) * _The Frobenius Condition, Right Properness, and Uniform Fibrations_, [[Nicola Gambino]], [[Christian Sattler]]. [arXiv](http://arxiv.org/abs/1510.00669) * _Fibred fibration categories_, [[Taichi Uemura]], 2016, [arXiv](http://arxiv.org/abs/1602.08206) * _A homotopy-theoretic model of function extensionality in the effective topos_, [[Daniil Frumin]], [[Benno van den Berg]], [arxiv](https://arxiv.org/abs/1701.08369) * _Polynomial pseudomonads and dependent type theory_, [[Steve Awodey]], [[Clive Newstead]], 2018, [arxiv](https://arxiv.org/abs/1802.00997) * _Towards a Topological Model of Homotopy Type Theory_, [[Paige North]], [doi](https://doi.org/10.1007/978-3-319-21284-5_16) * _The Equivalence Extension Property and Model Structures_, [[Christian Sattler]], [arxiv](https://arxiv.org/abs/1704.06911) * _Univalent polymorphism_, [[Benno van den Berg]], [arxiv](https://arxiv.org/abs/1803.10113) ##Univalence## * _The equivalence axiom and univalent models of type theory_ (talk at CMU, February 4th, 2010), [[Vladimir Voevodsky]]. [arXiv](http://arxiv.org/abs/1402.5556) * _Univalence in simplicial sets._ [[Chris Kapulkin]], [[Peter LeFanu Lumsdaine]], [[Vladimir Voevodsky]]. [arXiv](http://arxiv.org/abs/1203.2553) * _Univalence for inverse diagrams and homotopy canonicity._ [[Michael Shulman]]. [arXiv](http://arxiv.org/abs/1203.3253) * _Fiber bundles and univalence._ Lecture by [[Ieke Moerdijk]] at the Lorentz Center, Leiden, December 2011. [Lecture notes by Chris Kapulkin](http://www-home.math.uwo.ca/~kkapulki/notes/fiber_bundles_univalence.pdf) * _A model of type theory in simplicial sets: A brief introduction to Voevodsky's homotopy type theory._ [[Thomas Streicher]], 2011. [PDF](http://www.mathematik.tu-darmstadt.de/~streicher/sstt.pdf) * _Univalence and Function Extensionality._ Lecture by [[Nicola Gambino]] at Oberwohlfach, February 2011. [Lecture notes by Chris Kapulkin and Peter Lumsdaine](http://www.pitt.edu/~krk56/UA_implies_FE.pdf) * _The Simplicial Model of Univalent Foundations._ [[Chris Kapulkin]] and [[Peter LeFanu Lumsdaine]] and [[Vladimir Voevodsky]], 2012. [arXiv](http://arxiv.org/abs/1211.2851) * _The univalence axiom for elegant Reedy presheaves_. [[Michael Shulman]], [arXiv](http://arxiv.org/abs/1307.6248) * _Univalent universes for elegant models of homotopy types_. [[Denis-Charles Cisinski]], [arXiv](http://arxiv.org/abs/1406.0058) * _A univalent universe in finite order arithmetic_. [[Colin McLarty]], [arXiv](http://arxiv.org/abs/1412.6714) * _Constructive Simplicial Homotopy_. Wouter Pieter Stekelenburg, [arXiv](http://arxiv.org/abs/1604.04746) * _Higher Homotopies in a Hierarchy of Univalent Universes_. [[Nicolai Kraus]] and [[Christian Sattler]], [arXiv](http://arxiv.org/abs/1311.4002), [DOI](http://dl.acm.org/citation.cfm?doid=2737801.2729979) * _Univalence for inverse EI diagrams_. [[Michael Shulman]], [arXiv](http://arxiv.org/abs/1508.02410) * _Univalent completion_. [[Benno van den Berg]], [[Ieke Moerdijk]], [arXiv](http://arxiv.org/abs/1508.04021) * _On lifting univalence to the equivariant setting_. [[Anthony Bordg]], [arXiv](http://arxiv.org/abs/1512.04083) * _Univalence in locally cartesian closed $\infty$-categories_. [[David 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](http://arxiv.org/abs/1201.3898) * _[[W-types in homotopy type theory]]_. [[Benno van den Berg]] and [[Ieke Moerdijk]], [arXiv](http://arxiv.org/abs/1307.2765) * _[[Homotopy-initial algebras in type theory]]_ [[Steve Awodey]], [[Nicola Gambino]], [[Kristina Sojakova]]. [arXiv](http://arxiv.org/abs/1504.05531), [Coq code](https://github.com/kristinas/hinitiality) * _[[The General Universal Property of the Propositional Truncation]]_. [[Nicolai Kraus]], [arXiv](http://arxiv.org/abs/1411.2682) * _[[Non-wellfounded trees in Homotopy Type Theory]]_. [[Benedikt Ahrens]], [[Paolo Capriotti]], [[Régis Spadotti]]. TLCA 2015, [doi:10.4230/LIPIcs.TLCA.2015.17](http://dx.doi.org/10.4230/LIPIcs.TLCA.2015.17), [arXiv](https://arxiv.org/abs/1504.02949) * _[[Constructing the Propositional Truncation using Non-recursive HITs]]_. [[Floris van Doorn]], [arXiV](http://arxiv.org/abs/1512.02274) * _[[Constructions with non-recursive higher inductive types]]_. [[Nicolai Kraus]], LiCS 2016, [pdf](http://www.cs.nott.ac.uk/~psznk/docs/pseudotruncations.pdf) * _[[The join construction]]_. [[Egbert Rijke]], [arXiv](https://arxiv.org/abs/1701.07538) * _[[Semantics of higher inductive types]]_. [[Michael Shulman]] and [[Peter LeFanu Lumsdaine]], [arXiv](https://arxiv.org/abs/1705.07088) * _[[A Descent Property for the Univalent Foundations]]_, [[Egbert Rijke]], [doi](https://doi.org/10.1007/978-3-319-21284-5_18) * _[[Impredicative Encodings of (Higher) Inductive Types]]_. [[Steve Awodey]], [[Jonas Frey]], and [[Sam Speight]]. [arxiv](https://arxiv.org/abs/1802.02820), 2018 * _[[W-Types with Reductions and the Small Object Argument]]_, [[Andrew Swan]], [arxiv](https://arxiv.org/abs/1802.07588) ##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](http://arxiv.org/abs/1401.0053) [journal](http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=9679046) * _[[A preliminary univalent formalization of the p-adic numbers.]]_ Álvaro Pelayo, [[Vladimir Voevodsky]], [[Michael A. Warren]], 2012. [arXiv](http://arxiv.org/abs/1302.1207) * _[[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](http://arxiv.org/abs/1303.0584) (on _[[nLab: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](https://arxiv.org/abs/1610.04591) ##Applications to computing## * _Homotopical patch theory_. [[Carlo Angiuli]], [[Ed Morehouse]], [[Dan Licata]], [[Robert Harper]], [PDF](http://dlicata.web.wesleyan.edu/pubs/amlh14patch/amlh14patch.pdf) * _Guarded Cubical Type Theory: Path Equality for Guarded Recursion_, [[Lars Birkedal]], [[Ale? Bizjak]], [[Ranald Clouston]], [[Hans Bugge Grathwohl]], [[Bas Spitters]], [[Andrea Vezzosi]], [arXiv]( https://arxiv.org/abs/1606.05223) ##Cubical models and cubical type theory## * _[[A Cubical Approach to Synthetic Homotopy Theory]]_. [[Dan Licata]] and [[Guillaume Brunerie]], LICS 2015, [PDF](http://dlicata.web.wesleyan.edu/pubs/lb15cubicalsynth/lb15cubicalsynth.pdf) * _[[A syntax for cubical type theory]]_. [[Thorsten Altenkirch]] and [[Ambrus Kaposi]], [PDF](http://www.cs.nott.ac.uk/~txa/publ/ctt.pdf) * _[[Implementation of Univalence in Cubical Sets]]_, [github](https://github.com/simhu/cubical) * _[[A Note on the Uniform Kan Condition in Nominal Cubical Sets]]_, [[Robert Harper]] and [[Kuen-Bang Hou]]. [arXiv](http://arxiv.org/abs/1501.05691) * _[[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](http://arxiv.org/abs/1510.00669) * _Cubical Type Theory: a constructive interpretation of the univalence axiom_, [[Cyril Cohen]], [[Thierry Coquand]], [[Simon Huber]], and [[Anders Mortberg]], [arxiv](https://arxiv.org/abs/1611.02108) and [github implementation](https://github.com/mortberg/cubicaltt) * _[[Canonicity for cubical type theory]]_, [[Simon Huber]], [arxiv](https://arxiv.org/abs/1607.04156). * _[[Nominal Presentation of Cubical Sets Models of Type Theory]]_, [[Andrew M. Pitts]], [pdf](http://drops.dagstuhl.de/opus/volltexte/2015/5498/pdf/12.pdf) * _[[Axioms for Modelling Cubical Type Theory in a Topos]]_, [[Ian Orton]] and [[Andrew M. Pitts]], [pdf](http://drops.dagstuhl.de/opus/volltexte/2016/6564/pdf/LIPIcs-CSL-2016-24.pdf) [Agda code](http://www.cl.cam.ac.uk/~rio22/agda/cubical-topos/root.html) * _Computational Higher Type Theory I: Abstract Cubical Realizability_, [[Carlo Angiuli]], [[Robert Harper]], [[Todd Wilson]], [arxiv](https://arxiv.org/abs/1604.08873), 2016 * _Computational Higher Type Theory II: Dependent Cubical Realizability_, [[Carlo Angiuli]], [[Robert Harper]], [arxiv](https://arxiv.org/abs/1606.09638), 2016 * _[[The univalence axiom in cubical sets]]_. [[Marc Bezem]], [[Thierry Coquand]], [[Simon Huber]]. [arxiv](https://arxiv.org/abs/1710.10941), 2017 * _[[A Cubical Model of Homotopy Type Theory]]_. [[Steve Awodey]]. [arxiv](https://arxiv.org/abs/1607.06413), 2016 * _[[Cartesian Cubical Computational Type Theory]]_, [[Carlo Angiuli]], [[Favonia]], [[Robert Harper]]. [pdf](https://www.cs.cmu.edu/~cangiuli/papers/ccctt.pdf) ##Syntax of type theory## * [_The identity type weak factorisation system._](http://homotopytypetheory.org/references/gambino-garner-the-identity-type-weak-factorisation-system/) [[Nicola Gambino]] and [[Richard Garner]], Theoretical Computer Science 409 (2008), no. 3, pages 94?109. [RG?s website](http://www.comp.mq.edu.au/~rgarner/Idtype/Idtype.html) * _[[Types are weak ∞-groupoids.]]_ [[Richard Garner]] and [[Benno van den Berg]], to appear. [RG?s website](http://www.comp.mq.edu.au/~rgarner/Typesom/Typesom.html) * _[[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](http://www.mathstat.dal.ca/~p.l.lumsdaine/research/Lumsdaine-Weak-omega-cats-from-ITT-LMCS.pdf) * _[[Higher Categories from Type Theories.]]_ [[Peter LeFanu Lumsdaine]], PhD Thesis: Carnegie Mellon University, 2010. [PDF](http://www.mathstat.dal.ca/~p.l.lumsdaine/research/Lumsdaine-2010-Thesis.pdf) * [_A coherence theorem for Martin-Löf?s type theory.]]_](http://homotopytypetheory.org/references/hedberg/) [[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. [PDF](http://www.mathstat.dal.ca/~p.l.lumsdaine/research/Lumsdaine-Model-strux-from-HITs.pdf) * _[[A category-theoretic version of the identity type weak factorization system]]_. [[Jacopo Emmenegger]], [arXiv](http://arxiv.org/abs/1412.0153) * _[[Locally cartesian closed quasicategories from type theory]]_. [[Chris Kapulkin]], [arXiv](http://arxiv.org/abs/1507.02648). * _[[Note on the construction of globular weak omega-groupoids from types, topological spaces etc]]_. [[John Bourke]], [arXiv](http://arxiv.org/abs/1602.07962) * _[[The Homotopy Theory of Type Theories]]_. [[Chris Kapulkin]] and [[Peter LeFanu Lumsdaine]], [arXiv](https://arxiv.org/abs/1610.00037). * _[[Polynomial Pseudomonads and Dependent Type Theory]]_. [[Steve Awodey]] and [[Clive Newstead]]. [arxiv](https://arxiv.org/abs/1802.00997), 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](http://arxiv.org/abs/1604.03799) * _[[Two-Level Type Theory and Applications]]_, [[Danil Annenkov]], [[Paolo Capriotti]], [[Nicolai Kraus]], [arxiv](https://arxiv.org/abs/1705.03307), 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](http://www.cs.cmu.edu/~drl/pubs/thesis/thesis.pdf). [PDF](http://www.cs.cmu.edu/~drl/pubs/lh102dtt/lh102dtt.pdf) * _[[A type theory for synthetic $\infty$-categories]]_. [[Emily Riehl]], [[Michael Shulman]]. [arxiv](https://arxiv.org/abs/1705.07442) ##Cohesion and modalities## * _[[Quantum gauge field theory in cohesive homotopy type theory]]_. [[Urs Schreiber]] and [[Michael Shulman]]. [arxiv](https://arxiv.org/abs/1408.0054) * _[[Brouwer's fixed-point theorem in real-cohesive homotopy type theory]]_. [[Michael Shulman]]. To appear in MSCS; [arxiv](http://arxiv.org/abs/1509.07584) * _[[Modalities in homotopy type theory]]_. [[Egbert Rijke]], [[Michael Shulman]], [[Bas Spitters]]. [arxiv](https://arxiv.org/abs/1706.07526) ##Theories and models## * _Homotopy Model Theory I: Syntax and Semantics_, [[Dimitris Tsementzis]], [arXiv](http://arxiv.org/abs/1603.03092) ##Computational interpretation## * _[[Canonicity for 2-Dimensional Type Theory.]]_ [[Dan Licata]] and [[Robert Harper]]. POPL 2012. [PDF](http://www.cs.cmu.edu/~drl/pubs/lh112tt/lh122tt-final.pdf) ##Philosophy## {#Philosophy} * _[[Structuralism, Invariance, and Univalence]]_. [[Steve Awodey]]. Philosophia Mathematica (2014) 22 (1): 1-11. [online](http://philmat.oxfordjournals.org/content/22/1/1.abstract) * _Identity in Homotopy Type Theory, Part I: The Justification of Path Induction_. [[James Ladyman]] and [[Stuart Presnell]]. Philosophia Mathematica (2015), [online](http://philmat.oxfordjournals.org/content/early/2015/06/01/philmat.nkv014.abstract#fn-2) * _[[Homotopy Type Theory: A synthetic approach to higher equalities]]_. [[Michael Shulman]]. To appear in _Categories for the working philosopher_; [arXiv](http://arxiv.org/abs/1601.05035) * _[[Univalent Foundations as Structuralist Foundations]]_. [[Dimitris Tsementzis]]. Forthcoming in _Synthese_; [Pitt-PhilSci] (http://philsci-archive.pitt.edu/12070/) * _[[Homotopy type theory: the logic of space]]_. [[Michael Shulman]]. To appear in _New Spaces in Mathematics and Physics_: [arxiv](https://arxiv.org/abs/1703.03007) ##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](http://mathstat.dal.ca/~mwarren/Papers/mc.pdf), [arXiv](http://arxiv.org/abs/0906.4521) * _[[Space-Valued Diagrams]], Type-Theoretically (Extended Abstract)_. [[Nicolai Kraus]] and [[Christian Sattler]]. [arXiv](https://arxiv.org/abs/1704.04543) [[!redirects references]] category: references