From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.194.54.101 with SMTP id i5mr1842601wjp.16.1477861020983; Sun, 30 Oct 2016 13:57:00 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.193.195 with SMTP id r186ls842379lff.22.gmail; Sun, 30 Oct 2016 13:56:59 -0700 (PDT) X-Received: by 10.25.22.104 with SMTP id m101mr1870625lfi.2.1477861019432; Sun, 30 Oct 2016 13:56:59 -0700 (PDT) Return-Path: Received: from mail-lf0-x22e.google.com (mail-lf0-x22e.google.com. [2a00:1450:4010:c07::22e]) by gmr-mx.google.com with ESMTPS id d62si1034000wmd.0.2016.10.30.13.56.59 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 30 Oct 2016 13:56:59 -0700 (PDT) Received-SPF: pass (google.com: domain of rwilli...@gmail.com designates 2a00:1450:4010:c07::22e as permitted sender) client-ip=2a00:1450:4010:c07::22e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of rwilli...@gmail.com designates 2a00:1450:4010:c07::22e as permitted sender) smtp.mailfrom=rwilli...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-lf0-x22e.google.com with SMTP id b81so90522920lfe.1 for ; Sun, 30 Oct 2016 13:56:59 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=date:from:to:cc:subject:message-id:references:mime-version :content-disposition:content-transfer-encoding:in-reply-to :user-agent; bh=uRxje84vX2ETkmEAA9TbgsBhElZbtK1aFk20QLnjKvo=; b=D85lbNdKex2QBVRyy0FYKp5Jfs/RWKBYohcSyzMLQl9M5DmDETh1yEzWxkNnpP8fXs KUYKT82rOSQAQDuzaJjS/2Hx2zxxy7ryCMi+Ij+/mE2BIF4wtm/qcBACW/yP0E+eQjfa uT7MYWYXhHozCCyqg5RknspuZkRZZ9HshSw02+1YWx0HcZRbNi4NdrZ2E9f3eISRILAS AdFDprIFwgdaUuDHDKl1mUHSP56uhvxFz72IVhhWLwZnudIDXmDMgaNiUpagjxvwK4pg QfGlSiFeFpPnERQM+ClwyJRt2UmuwDbcvKk8SKjkf8vghBoFYvXWPt4rlvUgoJCRvuj4 oiwA== X-Gm-Message-State: ABUngvfAew7svv0AjGQmtrgH877/Cade0JnUT05H+5kX2b6u5kpmJ0RP89JcvFErl5dMeQ== X-Received: by 10.25.211.80 with SMTP id k77mr14870487lfg.71.1477861018910; Sun, 30 Oct 2016 13:56:58 -0700 (PDT) Return-Path: Received: from localhost (203.228.16.62.customer.cdi.no. [62.16.228.203]) by smtp.gmail.com with ESMTPSA id 144sm4002647ljf.6.2016.10.30.13.56.57 (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Sun, 30 Oct 2016 13:56:57 -0700 (PDT) Date: Sun, 30 Oct 2016 21:56:56 +0100 From: Richard Williamson To: Ulrik Buchholtz Cc: Homotopy Type Theory , matthie...@inria.fr Subject: Re: [HoTT] Re: Is [Equiv Type_i Type_i] contractible? Message-ID: <20161030205656.GA1487@richard> References: <9ced56b8-66bb-4f7f-996e-bbbb84c227ab@googlegroups.com> <20161027194440.GA826@richard> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: User-Agent: Mutt/1.7.0 (2016-08-17) 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 . > > > > > 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.