Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] All (∞,1)-toposes have strict univalent universes
@ 2019-04-16 12:06 Ali Caglayan
  2019-04-17 22:59 ` 'Martin Escardo' via Homotopy Type Theory
  0 siblings, 1 reply; 5+ messages in thread
From: Ali Caglayan @ 2019-04-16 12:06 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- Attachment #1.1: Type: text/plain, Size: 648 bytes --]

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.

[-- Attachment #1.2: Type: text/html, Size: 935 bytes --]

^ permalink raw reply	[flat|nested] 5+ messages in thread

end of thread, other threads:[~2019-04-18 10:17 UTC | newest]

Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-04-16 12:06 [HoTT] All (∞,1)-toposes have strict univalent universes Ali Caglayan
2019-04-17 22:59 ` 'Martin Escardo' via Homotopy Type Theory
2019-04-17 23:44   ` Michael Shulman
2019-04-18 10:09     ` [HoTT] All (???,1)-toposes " Thomas Streicher
2019-04-18 10:16       ` Michael Shulman

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).