Re: [HoTT] Re: Is [Equiv Type_i Type_i] contractible?

[Eric Finster <ericf...@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 5810 bytes --]

Just wanted to mention quickly for those who are interested in this kind of
thing that a similar statement for the *stable* homotopy category is a
theorem of Stefan Schwede's:

http://www.math.uni-bonn.de/people/schwede/rigid.pdf

Eric


On Sun, Oct 30, 2016 at 9:57 PM Richard Williamson <rwilli...@gmail.com>
wrote:

> Hi Ulrik,
>
> I mis-remembered the history a little: Corollary 5.2.2 of the
> following paper of Toën and Vezzozi, from 2002, also gives a
> proof of a lifting of the hypothèse inspiratrice.
>
> https://arxiv.org/abs/math/0212330
>
> As one would expect, the paper 'La théorie de l'homotopie de
> Grothendieck' of Maltsiniotis also briefly discusses the original
> hypothèse inspiratrice, early on in the introduction (see especially
> the footnote).
>
> I don't think that I know of other direct references beyond these,
> except possibly in other writings of these authors; though the
> quasi-categorical literature also, as one would expect, has a proof of
> the same theorem as in the papers of Cisinski and Toën-Vezzosi.
>
> I think that the Cisinski's paper gives a very clear reason to
> expect the result to be true when formulated in the language of a
> sufficiently rich 'homotopical category theory', whether the
> language be that of derivators, (∞,1)-categories, or whatever.
>
> It is remarkable that the result can be proven relatively easily
> when formulated in a certain language, but if one insists on the
> original version at the level of homotopy categories, then there seems
> to be no way to approach it. This is the aspect of the hypothesis that
> I am most interested in. A proof that the original hypothesis is
> independent of ZFC would no doubt shed some very interesting light on
> this dichotomy.
>
> Best wishes,
> Richard
>
> On Thu, Oct 27, 2016 at 01:38:15PM -0700, Ulrik Buchholtz wrote:
> > Thanks, Richard!
> >
> > Of course, this is not directly pertaining to Matthieu, Nicolas and
> Théo's
> > question, but it's trying to capture an intuition that a universe should
> be
> > rigid, at least when considered together with some structure.
> >
> > How much structure suffices to make the universe rigid, and can we define
> > this extra structure in HoTT? (We don't know how to say yet that the
> > universe can be given the structure of an infinity-category strongly
> > generated by 1, for example.)
> >
> > Do you know other references that pertain to the inspiring
> assumption/hypothèse
> > inspiratrice?
> >
> > Best wishes,
> > Ulrik
> >
> > On Thursday, October 27, 2016 at 9:44:43 PM UTC+2, Richard Williamson
> wrote:
> > >
> > > I think the earliest proof of some version of Grothendieck's
> > > hypothèse inspiratrice is in the following paper of Cisinki.
> > >
> > > http://www.tac.mta.ca/tac/volumes/20/17/20-17abs.html
> > >
> > > It is my belief that Grothendieck's original formulation, which
> > > was for the homotopy category itself (as opposed to a lifting of
> > > it), is independent of ZFC. A proof of this would be fascinating.
> > > I have occasionally speculated about trying to use HoTT to give
> > > such an independence proof. Vladimir's comment suggests that one
> > > direction of this is already done.
> > >
> > > Best wishes,
> > > Richard
> > >
> > > On Thu, Oct 27, 2016 at 10:12:50AM -0700, Ulrik Buchholtz wrote:
> > > > This is (related to) Grothendieck's “inspiring assumption” of
> Pursuing
> > > > Stacks section 28.
> > > >
> > > > I only know of the treatment by Barwick and Schommer-Pries in On the
> > > > Unicity of the Homotopy Theory of Higher Categories:
> > > > https://arxiv.org/abs/1112.0040
> > > >
> > > > Theorem 8.12 for n=0 says that the Kan complex of homotopy theories
> of
> > > > (infinity,0)-categories is contractible. Of course this depends on
> their
> > > > axiomatization, Definition 6.8. Perhaps some ideas can be adapted.
> > > >
> > > > Cheers,
> > > > Ulrik
> > > >
> > > > On Thursday, October 27, 2016 at 5:15:45 PM UTC+2, Matthieu Sozeau
> > > wrote:
> > > > >
> > > > > Dear all,
> > > > >
> > > > >   we've been stuck with N. Tabareau and his student Théo
> Winterhalter
> > > on
> > > > > the above question. Is it the case that all equivalences between a
> > > universe
> > > > > and itself are equivalent to the identity? We can't seem to prove
> (or
> > > > > disprove) this from univalence alone, and even additional
> > > parametricity
> > > > > assumptions do not seem to help. Did we miss a counterexample? Did
> > > anyone
> > > > > investigate this or can produce a proof as an easy corollary? What
> is
> > > the
> > > > > situation in, e.g. the simplicial model?
> > > > >
> > > > > -- Matthieu
> > > > >
> > > >
> > > > --
> > > > 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 HomotopyTypeThe...@googlegroups.com
> <javascript:>.
> > >
> > > > 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 HomotopyTypeThe...@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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

[-- Attachment #2: Type: text/html, Size: 10181 bytes --]