ICM 2026 Invited Section Lecture - Emily Riehl

Value of the Information & Strength of the Argument

The talk offers a compelling and well-argued case for adopting synthetic approaches in higher category theory. Riehl demonstrates the value by showing how formal systems like homotopy type theory and simplicial type theory simplify proofs, make definitions more natural, and enable computer formalization—a significant advantage over traditional analytic methods. She argues that the synthetic perspective collapses distinctions between contractibility and uniqueness, effectively hiding higher-categorical complexity. The argumentation is clear and structured, moving from historical motivation to technical details, and uses concrete examples (e.g., the moduli space of contractibility) to illustrate abstract ideas.

Scientific Rigor, Source Quality, Title Accuracy

The lecture is rigorous, with precise definitions and references to collaborative work. Riehl cites specific researchers (Dominic Verity, Mike Shulman, Evan Cavallo, Christian Sattler, etc.) and mentions ongoing projects, as well as funding agencies. The talk references established sources such as the HoTT book and joint papers. The title accurately captures the content, as the lecture indeed presents synthetic perspectives on higher structures. No comments were provided for analysis.

The title accurately reflects the content: the lecture focuses on synthetic perspectives on higher structures, as detailed in the abstract and talk.

9/10

The lecture is given by a leading expert in higher category theory, presents a well-structured and rigorous overview of synthetic approaches, with appropriate references to ongoing work and historical context.

Markers derived by PSI from the transcript: the creator did not define chapters.

• 00:00Introduction and acknowledgments, including funding agencies and mentors.
• 05:00Historical overview of higher category theory: analytic, axiomatic, and synthetic phases.
• 12:00Motivation for synthetic mathematics: amenability to computer formalization, examples from homotopy type theory.
• 18:00Plan of the talk: synthetic perspectives on spaces (HoTT) and categories (simplicial type theory).
• 25:00Families of spaces and the role of quantifiers; locally cartesian closed categories.
• 30:00Moduli spaces of propositions: contractibility and equivalence conditions.
• 35:00Univalent universes and the structure identity principle.
• 40:00Synthetic theory of categories: definition, path/arrow induction, and directed univalence.

• Homotopy Type Theory: Univalent Foundations of Mathematics — The collaborative book project mentioned in the talk as the primary reference for homotopy type theory.
• Type Theory for Synthetic ∞-categories — Joint work by Emily Riehl and Mike Shulman introducing simplicial type theory, the synthetic formalism for higher categories.