Higher tripos theory links logic and infinity category models
Higher Tripos Theory
Logic in Computer Science
Summary
This paper develops an advanced mathematical framework called higher tripos theory, which connects logic systems with structures known as ∞-toposes. The authors extend classical methods to build logical models supporting complex infinite hierarchies called univalent universes. They also explore computability aspects and provide new results that clarify how these models behave logically and computationally. Their work advances a research program focused on understanding constructive mathematics using higher category theory.
What this means in practice
- •For proof assistants developers: Incorporate higher tripos constructions to support univalent universes in formal verification tools.
- •For type theory engineers: Use logical preservation criteria to extend interpretations of dependent types in higher-order type systems.
A theory result. No direct application yet.
Authors
Yoshihiro Maruyama
Abstract
Tripos theory constructs categorical models of higher-order logic from indexed logical data. We develop higher tripos theory and higher tripos-to-topos construction recovering the classical construction on zero-types through a covering criterion. The higher tripos-to-topos construction yields elementary $\infty$-toposes with closed bounded hierarchies of univalent universes, thus establishing a logical adjunction between $\infty$-triposes and elementary $\infty$-toposes with univalent universes. We also construct a logically conservative higher completion of regular $1$-categories with weak section families and a finite-limit-closed projective cover. This completion preserves original maps, predicates, and existing dependent products, and gives criteria for extending interpretations while preserving logical structure. With strongly inaccessible size bounds, Kleene assemblies instantiate the construction, producing a cumulative hierarchy of univalent universes that classifies every family in the completion and recovering the effective topos as the category of zero-types. We then establish an arithmetical completeness result: for a uniformly computably presented family, the numerical index set for identity with a fixed classifier code is $Π^0_2$-complete. We also construct two inequivalent univalent classifiers with the same global homotopy type: every internal map from one to the natural-number object is constant, whereas the other admits a nonconstant such map. These reconstruction, preservation, and computability results contribute to the higher effective-topos program of Awodey-Emmenegger and Anel-Awodey-Barton.