The Adjoint is Language: Why Infinity Groupoids Appear in Martin-L"of Type Theory
Abstract
We resolve a thirty-year open question in the foundations of mathematics: why do infinity groupoids appear in Martin-L\"of type theory without being axiomatically introduced? Awodey (2025) calls this ``an amazing coincidence.'' Voevodsky had the homotopical intuition but no causal account. Hofmann--Streicher (1994) demonstrated the phenomenon but could not explain it. We prove the answer is ontological: infinity groupoids appear because the type theory is constructed on language, and language carries infinity groupoid structure inherently. Drawing on five prior results---the Rigidity Constraint on coherent type-theoretic semantics, the Simply Connected Site, the Spectral Encoding of Expander Cayley Graphs, the Terminal $\infty$-Topos, and the Unified Structural Invariants of Adjoint Mathematics---we prove that the universal adjoint resolution identified across five domains of contemporary mathematics \emph{is} the linguistic operation, and that the three unifying invariants ($\pi_1 = 0$, trace class, terminality) are three descriptions of a single ontological fact: language is prior to mathematical structure. We prove this identification is not a relabeling by exhibiting five predictions---regarding methodology, truncation, cross-domain invariants, obstruction locus, and compression content---each confirmed by independent results.
Fields of Study & Subjects
Homotopy and Cohomology in Algebraic Topology
Logic
programming
and type systems
Advanced Algebra and Logic
Publication details
- Journal / source
- Zenodo (CERN European Organization for Nuclear Research)
- Publication date
- 8 March 2026
- Language
- EN
- Document type
- Preprint