A univalent universe in finite order arithmetic
Logic
2015-01-13 v2
Abstract
Homotopy Type Theory with a univalent universe is interpreted at the strength of finite order arithmetic. We eliminate Grothendieck universes, avoid the axiom of replacement, and bound all uses of separation.
Cite
@article{arxiv.1412.6714,
title = {A univalent universe in finite order arithmetic},
author = {Colin McLarty},
journal= {arXiv preprint arXiv:1412.6714},
year = {2015}
}
Comments
This version makes some response to Steve Awodey's comment that the coherence problem was not handled in the first version