LOGICAL ASPECTS OF INFINITY-TOPOI
Abstract
The theory of higher categories has become an important paradigm of mathematics in the last 30 years. Higher categories satisfy needs from sources as diverse as topology, geometry, physics, and logic. A guiding principle of higher category theory is Grothendieck’s homotopy hypothesis which postulates an equivalence between infinity-groupoids and homotopy types of topological spaces. The homotopy hypothesis establishes connections between higher categories and homotopy type theory – a new homotopy-theoretic interpretation of Martin-Löf’s constructive type theory that has been intensively studied at Carnegie Mellon University, and elsewhere, in the past years. On the one hand, the structure of iterated identity types allows syntactic types in HoTT to be viewed as higher groupoids, and on the other hand we can regard HoTT as an internal language for the infinity-category of homotopy types – a category which plays a similarly fundamental role in higher category theory as the category of sets does in ordinary category theory. More generally, Shulman recently proved that homotopy type theory can be interpreted in arbitrary higher topoi, whose theory has been developed in algebraic topology and algebraic geometry. The idea to interpret intensional type theory in higher topoi was motivated by the well-known fact that extensional type theory admitted interpretations in arbitrary 1-topoi. Shulman’s result proves that – just as 1-topoi – higher topoi have an intimate relationship with logic, but many important aspects of this relation are still waiting to be investigated.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Aug 12, 2021
- Source ID
- FA95502010305
Entities
People
- Steve Awodey
Organizations
- Air Force Office of Scientific Research
- Carnegie Mellon University
- United States Air Force