A univalent universe in finite order arithmetic

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.

This version makes some response to Steve Awodey's comment that the coherence problem was not handled in the first version