Mike has released this new preprint on the arXiv:

    All (∞,1)-toposes have strict univalent universes 
<https://arxiv.org/abs/1904.07004>

Quoting the abstract:

Thus, homotopy type theory can be used as a formal language for reasoning 
internally to (∞, 1)-toposes, just as higher-order logic is used for 
1-toposes.

:))

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.