[FOM] Low consistency strength for a Univalent Universe

[Colin McLarty]

Kapulkin, Lumsdaine, and Voevodsky (mathematics arXiv, 1211.2851v2) use ZFC
plus two Grothendieck universes to prove consistency of a Univalent
Universe in Martin-Löf Type Theory.  They even show that if the Universe is
to be defined by a cardinal bound on the sets, then that bound must be a
strong inaccessible.

I have just posted http://arxiv.org/abs/1412.6714 showing that the use of a
definability bound instead of cardinality allows essentially the same model
construction to work at the consistency strength of finite order
arithmetic.

To work at that strength we must give up dependent products for large
dependent types, which is natural when you see what it means.  And this is
an equiconsistency result.

For the ASL next week I expect to present a proof that I am now checking,
to show Zermelo set theory plus existence of a standard model of Zermelo
set theory suffices to prove consistency of a Univalent universe with full
Martin-Löf type theory -- though I am not yet clear what would make an
equiconsistency result for this case.

best, Colin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20141226/ca66f5a3/attachment.html>