Six open problems in homotopy type theory, unified toward ζ(s)=0 as a HoTT-native statement. Analytic number theory reformulated through coinductive structures, cubical type theory, and categorical foundations.
The univalent presentation of the real numbers admits two profoundly different formulations: an inductive one, in which is built as a higher inductive--inductive type (HIIT) of Cauchy sequences modulo…
The Cauchy reals admit a higher inductive--inductive presentation in Book HoTT (HoTT Book 11.3, Booij 2020), and this presentation underwrites the unique-existence definitions of and e used throughout…
We undertake a three-way structural comparison of three foundational systems: Lawvere's Elementary Theory of the Category of Sets (ETCS, 1964), Friedman's Intuitionistic Zermelo--Fraenkel set theory (…
The natural numbers object (NNO) of an elementary topos is, classically, an object equipped with a global element 0 and an endomorphism s such that the resulting pointed dynamical system is initial. I…
Voevodsky's univalence axiom equates path identification with type-equivalence and lies at the heart of homotopy type theory (HoTT). Its directed analogue --- which would equate hom-types in the unive…
We address what the synthesis of our prior series of papers identified as the principal open problem in homotopy type theory's interface with contemporary mathematics: the absence of a HoTT-native for…
This paper synthesises six independent investigations into a single research programme directed at what our prior series identified as the principal open problem in homotopy type theory's interface wi…
