A univalent universe in finite order arithmetic

TL;DR

This paper demonstrates that homotopy type theory with a univalent universe can be interpreted within finite order arithmetic, removing the need for Grothendieck universes and certain axioms.

Contribution

It provides a novel interpretation of univalent foundations in a weaker logical framework, simplifying foundational assumptions.

Findings

Eliminates Grothendieck universes in the interpretation

Avoids the axiom of replacement

Bounds all uses of separation

Abstract

Homotopy Type Theory with a univalent universe $\,\mathcal{U}_0$ is interpreted at the strength of finite order arithmetic. We eliminate Grothendieck universes, avoid the axiom of replacement, and bound all uses of separation.