A univalent universe in finite order arithmetic

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.