From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.194.86.234 with SMTP id s10mr829301wjz.18.1477597483558; Thu, 27 Oct 2016 12:44:43 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.109.87 with SMTP id i84ls69575wmc.21.canary-gmail; Thu, 27 Oct 2016 12:44:42 -0700 (PDT) X-Received: by 10.194.40.68 with SMTP id v4mr832208wjk.12.1477597482809; Thu, 27 Oct 2016 12:44:42 -0700 (PDT) Return-Path: Received: from mail-lf0-x234.google.com (mail-lf0-x234.google.com. [2a00:1450:4010:c07::234]) by gmr-mx.google.com with ESMTPS id o62si307067wmg.3.2016.10.27.12.44.42 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 27 Oct 2016 12:44:42 -0700 (PDT) Received-SPF: pass (google.com: domain of rwilli...@gmail.com designates 2a00:1450:4010:c07::234 as permitted sender) client-ip=2a00:1450:4010:c07::234; 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::234 as permitted sender) smtp.mailfrom=rwilli...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-lf0-x234.google.com with SMTP id b81so40560570lfe.1 for ; Thu, 27 Oct 2016 12:44:42 -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=9JflhqsmsvUpvSKzEeoSLbekU6ZqBoMszXWk3fUbmyI=; b=l+p/3N+AIXwUunPPtVgfM7QoL3kId05zan9B9rzfYooRShlnqkFWhDMft7kB0UBFy/ 9/Ek9LpbEktzT5Nk/Wf5laLC0BrUuVfOvhSsrYqDzy3n2iAFpy3a9AHP0YUDOiSqU94i cedsIpxiqorZhZUX2gQJEWeuRgpdILEZzwLwqCM7VsmnwEdpPvTkwG4qxC2bOapaOdU/ ZBsQhXgJE0x6kHw05ZG6dKkx3IaEjMu8x5nJ2Nzvf3f81bKyxyhF+QOsPXiISEE5k5WM Aaco5k3UO1AnJhfnr9dkk/+BtxB8plMErrSFm9B7QFBSn/xoQusXFAoS8b9g5Onf4QDd gzvQ== X-Gm-Message-State: ABUngvfZJlun/cdi8cc1LNrk30rH4KNcogplnEwY1odpNv6I+YDG0i8h/q+xEAmnKm9z/Q== X-Received: by 10.25.26.73 with SMTP id a70mr7608694lfa.108.1477597482114; Thu, 27 Oct 2016 12:44:42 -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 y131sm1500217lfd.26.2016.10.27.12.44.40 (version=TLS1_2 cipher=ECDHE-RSA-CHACHA20-POLY1305 bits=256/256); Thu, 27 Oct 2016 12:44:41 -0700 (PDT) Date: Thu, 27 Oct 2016 21:44:40 +0200 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: <20161027194440.GA826@richard> References: <9ced56b8-66bb-4f7f-996e-bbbb84c227ab@googlegroups.com> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: <9ced56b8-66bb-4f7f-996e-bbbb84c227ab@googlegroups.com> User-Agent: Mutt/1.7.0 (2016-08-17) 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.