| _version_ | 1866901253202640896 |
|---|---|
| author | Revista, Zen MATH, 10 |
| author_facet | Revista, Zen MATH, 10 |
| contents | This paper explores the utility of elementary toposes as a foundational framework for synthetic higher category theory. While traditional higher category theory often relies on complex combinatorial or topological models, a synthetic approach aims to define and reason about higher categorical structures directly from a small set of axioms within a suitable foundational system. Elementary toposes, with their rich internal logic equivalent to intuitionistic type theory and their ability to model various mathematical universes, offer a compelling environment for such a synthetic development. We delve into how the internal language of an elementary topos can interpret dependent type theory, including identity types, thereby providing a setting where the fundamental concepts of higher categories, such as higher cells, equivalences, and compositions, can be expressed axiomatically without explicit reference to underlying sets or spaces. The paper discusses the theoretical underpinnings, examines the benefits of this approach in terms of conceptual clarity and formal rigor, and compares it with alternative foundational paradigms like Homotopy Type Theory. We argue that elementary toposes provide a robust, flexible, and conceptually coherent foundation for building synthetic higher categories, opening new avenues for formalization and reasoning in advanced mathematics. |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_17805995 |
| institution | Zenodo |
| language | |
| publishDate | 2025 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | Elementary Toposes as Foundations for Synthetic Higher Categories Revista, Zen MATH, 10 This paper explores the utility of elementary toposes as a foundational framework for synthetic higher category theory. While traditional higher category theory often relies on complex combinatorial or topological models, a synthetic approach aims to define and reason about higher categorical structures directly from a small set of axioms within a suitable foundational system. Elementary toposes, with their rich internal logic equivalent to intuitionistic type theory and their ability to model various mathematical universes, offer a compelling environment for such a synthetic development. We delve into how the internal language of an elementary topos can interpret dependent type theory, including identity types, thereby providing a setting where the fundamental concepts of higher categories, such as higher cells, equivalences, and compositions, can be expressed axiomatically without explicit reference to underlying sets or spaces. The paper discusses the theoretical underpinnings, examines the benefits of this approach in terms of conceptual clarity and formal rigor, and compares it with alternative foundational paradigms like Homotopy Type Theory. We argue that elementary toposes provide a robust, flexible, and conceptually coherent foundation for building synthetic higher categories, opening new avenues for formalization and reasoning in advanced mathematics. |
| title | Elementary Toposes as Foundations for Synthetic Higher Categories |
| url | https://doi.org/10.5281/zenodo.17805995 |