Discussion of Homotopy Type Theory and Univalent Foundations
 help / 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

* Re: [HoTT] All (∞,1)-toposes have strict univalent universes
  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
  0 siblings, 1 reply; 5+ messages in thread
From: Martin Escardo' via Homotopy Type Theory @ 2019-04-17 22:59 UTC (permalink / raw)
  To: Ali Caglayan, Homotopy Type Theory

On 16/04/2019 13:06, Ali Caglayan wrote:
> 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.

This is awesome.

Perhaps it deserves a short explanation (or at least listing) of the 
crucial steps gere in this list.

Best,
Martin

-- 
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.

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

* Re: [HoTT] All (∞,1)-toposes have strict univalent universes
  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
  0 siblings, 1 reply; 5+ messages in thread
From: Michael Shulman @ 2019-04-17 23:44 UTC (permalink / raw)
  To: Martin Escardo; +Cc: Homotopy Type Theory

Here's a brief summary of the steps:

1. Every Grothendieck (∞, 1)-topos can be presented by an accessible
left exact left Bousfield localization of an injective model structure
on a category of enriched simplicial presheaves.

2. Such presentations are right proper Cisinski model categories,
hence (as we already knew) model MLTT, even with many HITs, but not
previously known to model universes.

3. The fibrations in an injective model structure have no explicit
"cofibrantly generated" description in terms of a lifting property,
but it turns out they do have a fairly explicit "algebraic"
description in terms of the rectifiability of homotopy coherent
natural transformations (a homotopical version of "coflexible
algebras").

4. Now define a presheaf U by U(x) = the set of injective fibrations
over the representable C(-,x) *equipped with* such fibrancy structure
(suitably rectified to become a strict presheaf), and we get a fibrant
and univalent universe.

5. Finally, any accessible left exact localization can be presented
internally by a lex modality (using the recent characterization
thereof by Anel-Biedermann-Finster-Joyal), and the universe of modal
types for a lex modality is modal, giving a universe for the localized
model structure.

For more detail, you can read the introduction to the paper (or the
whole thing, of course), or look at these slides from last month's
Midwest HoTT seminar:
http://home.sandiego.edu/~shulman/papers/injmodel-talk.pdf

On Wed, Apr 17, 2019 at 3:59 PM 'Martin Escardo' via Homotopy Type
Theory <HomotopyTypeTheory@googlegroups.com> wrote:
>
> On 16/04/2019 13:06, Ali Caglayan wrote:
> > 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.
>
> This is awesome.
>
> Perhaps it deserves a short explanation (or at least listing) of the
> crucial steps gere in this list.
>
> Best,
> Martin
>
> --
> 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.

-- 
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.

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

* Re: [HoTT] All (???,1)-toposes have strict univalent universes
  2019-04-17 23:44   ` Michael Shulman
@ 2019-04-18 10:09     ` " Thomas Streicher
  2019-04-18 10:16       ` Michael Shulman
  0 siblings, 1 reply; 5+ messages in thread
From: Thomas Streicher @ 2019-04-18 10:09 UTC (permalink / raw)
  To: Michael Shulman; +Cc: Martin Escardo, Homotopy Type Theory

I only had a rough glance at your paper. But as it seems you don't
interpret directly in the infty toposes but rather in some
representing model structure.
No complaint because I don't expect otherwise.

In any case it is quite an achievement to get universes "strongly `a
la Tarski".

Thomas

-- 
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.

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

* Re: [HoTT] All (???,1)-toposes have strict univalent universes
  2019-04-18 10:09     ` [HoTT] All (???,1)-toposes " Thomas Streicher
@ 2019-04-18 10:16       ` Michael Shulman
  0 siblings, 0 replies; 5+ messages in thread
From: Michael Shulman @ 2019-04-18 10:16 UTC (permalink / raw)
  To: Thomas Streicher; +Cc: Martin Escardo, Homotopy Type Theory

Right, I would say that interpreting in a representing model structure
is the limit of current technology.  Maybe one day we'll be able to
interpret directly in an infinity-topos, but not yet.

On Thu, Apr 18, 2019 at 3:09 AM Thomas Streicher
<streicher@mathematik.tu-darmstadt.de> wrote:
>
> I only had a rough glance at your paper. But as it seems you don't
> interpret directly in the infty toposes but rather in some
> representing model structure.
> No complaint because I don't expect otherwise.
>
> In any case it is quite an achievement to get universes "strongly `a
> la Tarski".
>
> Thomas
>
> --
> 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.

-- 
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.

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

end of thread, back to index

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

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/ public-inbox