GrokRxiv:2026.05/math.CT • math.LO • math.HO

The Univalent Correspondence

Six perspectives on what a number is — identified up to equivalence

7Papers
6Perspectives
1Correspondence
Synthesis paper cover
Synthesis

The Univalent Correspondence: How Six Perspectives on Number Become One

This synthesis paper unifies the six-part series. Under Voevodsky's univalence axiom, the four perspectives of Papers III through VI are not analogous but literally identical: an initial successor structure, a representing presheaf, a contractible Σ-type of NNO structures, and a structural invariant of arithmetic model…

Read SynthesisPDF
FoundationsPapers I–IIPre-formal and set-theoretic levels: numbers as symbols, quantities, and pure-set encodings.
Cover for The Naive Perspective: Numbers as Symbols and Quantities
Part I28p • math.HO

The Naive Perspective

This is the first paper in a six-part series, plus synthesis, on what we call the Univalent Correspondence: six perspectives on what a natural number "is". We t…

ReadPDFCode
Cover for The Set-Theoretic Perspective: von Neumann Ordinals
Part II32p • math.LO

The Set-Theoretic Perspective

We examine the set-theoretic level, in which natural numbers are reduced to particular elements of the cumulative hierarchy of pure sets. Working primarily in Z…

ReadPDFCode
StructuralPapers III–IVUniversal properties and representable functors: numbers defined by their relationships.
Cover for The Universal Property Perspective: Initial Successor Structures
Part III35p • math.CT

The Universal Property Perspective

We develop the universal-property perspective on the natural numbers, presenting the NNO (N, 0, succ) as the initial pointed set with endomorphism. From this un…

ReadPDFCode
Cover for The Yoneda Perspective: Representable Functors
Part IV38p • math.CT

The Yoneda Perspective

We develop the Yoneda perspective: the Yoneda embedding y: C → [C^op, Set] is fully faithful for any locally small category C. The corollary X ≅ Y ↔ Hom(−,X) ≅…

ReadPDFCode
Synthetic + InvariantPapers V–VIHomotopy type theory and categorical structuralism: encoding-free and isomorphism-invariant accounts.
Cover for The HoTT Perspective: Inductive Types up to Path Equivalence
Part V40p • math.LO

The HoTT Perspective

We give a self-contained development of Homotopy Type Theory as the synthetic language in which natural numbers admit an encoding-free description. The natural…

ReadPDFCode
Cover for The Categorical / Structural Perspective: Invariants of Structure-Preserving Morphisms
Part VI36p • math.CT

The Categorical / Structural Perspective

We develop the structural answer to "what is a number?" by treating numerals as invariants under all structure-preserving morphisms between models of arithmetic…

ReadPDFCode