A univalent universe in finite order arithmetic

Colin McLarty

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…