This special issue collects papers on homotopy type theory and univalent foundations. This research area studies topics at the intersection of type theory, category theory, and homotopy theory. For example, homotopical and higher categorical ideas have led to new extensions of dependent type theory and new dependent type theories, and these type theories have been used in proof assistants to formalize mathematics. In August 2019, the International Conference on Homotopy Type Theory (HoTT 2019) was held in at Carnegie Mellon University, with scientific organization by Steve Awodey, Andrej Bauer, Thierry Coquand, Nicola Gambino, Peter LeFanu Lumsdaine, and Michael Shulman. This special issue of MSCS contains work presented at the HoTT 2019 conference and work on related topics.
This volume is the first of two volumes for this special issue.
We begin with Cubical Methods in Homotopy Type Theory and Univalent Foundations by Anders Mörtberg, an introduction to cubical type theory and cubical models of homotopy type theory, which were the first constructive and computational models of univalence and higher inductive types. The paper introduces the basics of cubical type theory from a user’s point of view and discusses the mathematical foundations of these new type theories. The article is based on a course delivered at the HoTT 2019 Summer School.
Continuing the topic of cubical type theory, Bruno Bentzen’s Naive cubical type theory proposes and explores a vocabulary for cubical type theory in non-formalized mathematical prose, filling a gap that has been strongly felt since the topic’s roots in computer formalization, and paralleling one of the original motivations of the Homotopy Type Theory book.
On Church’s Thesis in Cubical Assemblies, by Andrew Swan and Taichi Uemura, sheds new light on anticlassical, homotopically nontrivial interpretations of type theory, providing powerful tools for their further investigation. The paper constructs and investigates the model in cubical assemblies; in particular, it shows that Church’s Thesis (CT) holds not in the whole cubical assemblies model, but in a reflective submodel, showing that CT is consistent with univalence.
The next two papers develop applications of homotopy type theory to programming languages. Synthetic topology in Homotopy Type Theory for probabilistic programming by Martin E. Bidlingmaier, Florian Faissole, and Bas Spitters uses synthetic topology to model continuous distributions for probabilistic computations. This mathematical setting is used to interpret a programming language with probabilistic choice.
The Scott model of PCF in univalent type theory by Tom de Jong develops and formalizes the Scott model of (general) recursion within univalent type theory, showing that univalent foundations support the constructive and predicative formalization of domain-theoretic denotational semantics of programming languages. The development makes use of homotopy propositions and propositional truncation, representing partiality via subobjects.
The final paper of the volume gives an application of homotopy type theory to the development and formalization of mathematics. Earlier work has developed category theory in univalent foundations, exploring the interesting questions that arise when defining categories in a foundation based on spaces rather than sets. Bicategories in univalent foundations by Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, and Niels van der Weide extends these ideas to bicategories (weak 2-categories) and develops a formalized library of bicategory theory within the UniMath library for Coq.
