Homotopy Type Theory is a remarkable research area, linking Mathematical Logic, Theoretical Computer Science, Algebraic Topology, and Category Theory. In light of the breadth of these connections and of the depth of some of the key achievements in the subject, it is easy to forget that Homotopy Type Theory is still a young discipline. To put things into perspective, one should remember that the special program on Univalent Foundations at the Institute for Advanced Study in Princeton took place in the academic year 2012/13 and that the First International Conference in Homotopy Type Theory was held in 2019, at Carnegie Mellon University.

The Second International Conference on Homotopy Type Theory was held from 22 to 25 May, 2023, again at Carnegie Mellon University. The event, which attracted over 80 participants, not only offered an occasion to assess the progress in the area and highlight promising directions for future research but also provided the impetus for this special issue of Mathematical Structures in Computer Science. We hope that the papers published in this special issue, which include some of those presented at that conference, make the current state of the art in Homotopy Type Theory accessible to a wide audience.

The current issue contains the first papers that have been accepted for the special issue and were produced before the end of 2024. From 1 January, 2025, Mathematical Structures in Computer Science will move to continuous publishing. The current papers will be linked to a collection with the same name “Advances in Homotopy Type Theory,” together with the other papers that will be accepted for the special issue and produced in 2025. Let us now provide a brief overview of the 2024 papers presented here.

The papers “On Hofmann–Streicher universes” by Steve Awodey and “Groupoidal realizability for intensional type theory” by Sam Speight contribute to the study of the semantics of Homotopy Type Theory, which continues to be a very active research topic. The links with set theory are instead the focus of “The category of iterative sets in homotopy type theory and univalent foundations” by Daniel Gratzer, Håkon Gylteroud, Anders Mörtberg, and Elisabeth Stenholm. Finally, we come to connections with Algebraic Geometry and Algebraic Topology. The paper “Smooth and proper maps with respect to a fibration” by Mathieu Anel and Jonathan Weinberger illustrates analogies between geometric and type-theoretic concepts, using (higher) category theory as a unifying framework, while “Symmetric monoidal smash products in homotopy type theory” by Axel Ljungström takes another important step in the development of synthetic Algebraic Topology within Homotopy Type Theory, which is amenable to formalization in proof-checking computer systems. Finally, “A Foundation for Synthetic Algebraic Geometry”, by Felix Cherubini, Thierry Coquand and Matthias Hutzler, takes important steps in developing an axiomatic approach to Algebraic Geometry within Homotopy Type Theory.

We expect that all these directions will continue to be subject of intense research in future years and look forward to seeing new exciting developments.