Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] Joyal's definition of elementary higher topos
@ 2020-02-21 13:23 Bas Spitters
  2020-02-21 22:13 ` Michael Shulman
  0 siblings, 1 reply; 3+ messages in thread
From: Bas Spitters @ 2020-02-21 13:23 UTC (permalink / raw)
  To: homotopytypetheory

In 2014, Andra Joyal proposed a definition of an elementary higher topos.

"This lecture contains a proposed definition that is not an
(∞,1)-category but a presentation of one by a model category-like
structure; this is closer to the type theory, but further from the
intended examples. In particular, there are unresolved coherence
questions even as to whether every Grothendieck (∞,1)-topos can be
presented by a model in Joyal’s sense (in particular, how strict can a
universe be made, and can the natural numbers object be made
fibrant)."
https://ncatlab.org/nlab/show/elementary+%28infinity%2C1%29-topos

Has there been any progress on these coherence questions?

-- 
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuQc317E8qUEOWJ2JQD_iXAFyE%3DWcttruqd5A8tRpHqttg%40mail.gmail.com.

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

end of thread, other threads:[~2020-02-23 23:56 UTC | newest]

Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-02-21 13:23 [HoTT] Joyal's definition of elementary higher topos Bas Spitters
2020-02-21 22:13 ` Michael Shulman
2020-02-23 23:56   ` 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).