Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Synthetic perspectives on spaces and categories

Emily Riehl

TL;DR

This note develops a synthetic vantage on spaces and categories by juxtaposing homotopy type theory and simplicial type theory. It introduces path induction and arrow induction as core proof techniques, and constructs univalent and directed univalent universes to support equivalence-based reasoning and synthetic categorification. Key contributions include a rigorous account of a very convenient category of spaces, a Yoneda-style arrow induction principle for covariant families, and the first concrete realization of a directed univalent universe yielding a synthetic category. Together, these developments offer a coherent foundation for synthetic mathematics, with implications for formalization, higher category theory, and multimodal logical frameworks.

Abstract

Recently discovered domain-specific formal systems -- specifically homotopy type theory and simplicial type theory -- provide new perspectives on spaces and categories in a natively equivalence-invariant setting. In this note, we expose fundamental proof techniques from these parallel settings: describing induction principles over paths or arrows and constructions involving universes that are either univalent or directed univalent.

Synthetic perspectives on spaces and categories

TL;DR

This note develops a synthetic vantage on spaces and categories by juxtaposing homotopy type theory and simplicial type theory. It introduces path induction and arrow induction as core proof techniques, and constructs univalent and directed univalent universes to support equivalence-based reasoning and synthetic categorification. Key contributions include a rigorous account of a very convenient category of spaces, a Yoneda-style arrow induction principle for covariant families, and the first concrete realization of a directed univalent universe yielding a synthetic category. Together, these developments offer a coherent foundation for synthetic mathematics, with implications for formalization, higher category theory, and multimodal logical frameworks.

Abstract

Recently discovered domain-specific formal systems -- specifically homotopy type theory and simplicial type theory -- provide new perspectives on spaces and categories in a natively equivalence-invariant setting. In this note, we expose fundamental proof techniques from these parallel settings: describing induction principles over paths or arrows and constructions involving universes that are either univalent or directed univalent.
Paper Structure (22 sections, 17 theorems, 17 equations)

This paper contains 22 sections, 17 theorems, 17 equations.

Table of Contents

  1. Introduction.
  2. On spaces.
  3. On categories.
  4. Outline.
  5. A very convenient category of spaces.
  6. Families of spaces.
  7. Path induction.
  8. Univalent universes.
  9. Propositions as spaces.
  10. Constructing univalent universes.
  11. Applications of Univalence.
  12. A language for synthetic categories
  13. Arrow induction.
  14. Arrow induction for covariant families.
  15. The Yoneda Lemma.
  16. ...and 7 more sections

Key Result

Theorem 2.1

There is a right proper simplicial model structure on simplicial sets whose cofibrations are the monomorphisms.

Theorems & Definitions (29)

  • Theorem 2.1: Quillen Quillen1967
  • Lemma 2.2
  • Lemma 2.4
  • Proposition 3.1: path induction, preliminary form
  • Proposition 3.3: path induction, intermediate form
  • Proposition 3.6: path induction, final form
  • Remark 3.7
  • Lemma 4.2
  • Lemma 4.4
  • Definition 4.6: Voevodsky KapulkinLumsdaine2021
  • ...and 19 more