From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.41.21 with SMTP id p21mr3353098ywp.2.1477588112699; Thu, 27 Oct 2016 10:08:32 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.103.2 with SMTP id u2ls4788itc.19.gmail; Thu, 27 Oct 2016 10:08:31 -0700 (PDT) X-Received: by 10.107.20.82 with SMTP id 79mr3095626iou.87.1477588111356; Thu, 27 Oct 2016 10:08:31 -0700 (PDT) Return-Path: Received: from pps3.ias.edu (pps3.ias.edu. [192.16.204.88]) by gmr-mx.google.com with ESMTPS id x14si895299vkd.3.2016.10.27.10.08.31 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 27 Oct 2016 10:08:31 -0700 (PDT) Received-SPF: pass (google.com: domain of vlad...@ias.edu designates 192.16.204.88 as permitted sender) client-ip=192.16.204.88; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of vlad...@ias.edu designates 192.16.204.88 as permitted sender) smtp.mailfrom=vlad...@ias.edu; dmarc=pass (p=NONE dis=NONE) header.from=ias.edu Received: from pps.reinject (pps3.ias.edu [127.0.0.1]) by pps3.ias.edu (8.15.0.59/8.15.0.59) with ESMTPS id u9RH8UpA009599 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Thu, 27 Oct 2016 13:08:30 -0400 Received: from pps3.ias.edu (pps3.ias.edu [127.0.0.1]) by pps.reinject (8.15.0.59/8.15.0.59) with SMTP id u9RH8UH8009593; Thu, 27 Oct 2016 13:08:30 -0400 X-Proofpoint-Sentinel: stfsU2FsdGVkX1+SYmVd1fRtFSEmAHoG/jFs9gNWtJlch8OU9Hc8bBxax0zy KWtEZaeNBHyns5HXO1IZf3fB29wz8zqejYnPn6+YRyvsJARMeW9x9o95UX/kntR56TE55hfs Received: from imap.math.ias.edu (imap.math.ias.edu [172.16.41.5]) by pps3.ias.edu with ESMTP id u9RH8U4R009592 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Thu, 27 Oct 2016 13:08:30 -0400 Received: from vladimirs-mbp-2.wireless.ias.edu ([172.16.158.102]) by imap.math.ias.edu with esmtpsa (TLSv1.2:DHE-RSA-AES256-GCM-SHA384:256) (Exim 4.80.1) (envelope-from ) id 1bzoAI-0000u5-BE; Thu, 27 Oct 2016 13:08:30 -0400 From: Vladimir Voevodsky Message-Id: <08DC660F-0BA0-400D-821B-D7132A843D8F@ias.edu> Content-Type: multipart/alternative; boundary="Apple-Mail=_96FC99C1-CD63-4F21-9E77-3EDBEA45FA9F" Mime-Version: 1.0 (Mac OS X Mail 10.0 \(3226\)) Subject: Re: [HoTT] Is [Equiv Type_i Type_i] contractible? Date: Thu, 27 Oct 2016 13:08:29 -0400 In-Reply-To: Cc: "Prof. Vladimir Voevodsky" , homotopytypetheory To: Matthieu Sozeau References: X-Mailer: Apple Mail (2.3226) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-10-27_11:,, signatures=0 X-Proofpoint-Spam-Reason: safe X-IAS-PPS-SPAM: NO X-Proofpoint-Spam-Details: rule=ias_safe policy=ias score=0 spamscore=0 suspectscore=0 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=donotscan adjust=0 reason=safe scancount=1 engine=8.0.1-1609300000 definitions=main-1610270281 X-IAS-PPS-PHISH: NO --Apple-Mail=_96FC99C1-CD63-4F21-9E77-3EDBEA45FA9F Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 In the univalent simplicial model it is not contractible at all. For exampl= e Type_i has many connected components that are contractible and any permut= ation of these components is an equivalence of the ambient type.=20 This implies that iscontr (weq Type_i Type_i) is not provable in any contex= t that is compatible with the univalent simplicial model. Vladimir. > On Oct 27, 2016, at 11:15 AM, Matthieu Sozeau wrote= : >=20 > Dear all, >=20 > we've been stuck with N. Tabareau and his student Th=C3=A9o Winterhalte= r on the above question. Is it the case that all equivalences between a uni= verse and itself are equivalent to the identity? We can't seem to prove (or= disprove) this from univalence alone, and even additional parametricity as= sumptions do not seem to help. Did we miss a counterexample? Did anyone inv= estigate this or can produce a proof as an easy corollary? What is the situ= ation in, e.g. the simplicial model? >=20 > -- Matthieu >=20 > --=20 > 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 . --Apple-Mail=_96FC99C1-CD63-4F21-9E77-3EDBEA45FA9F Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 In the univalent s= implicial model it is not contractible at all. For example Type_i has many = connected components that are contractible and any permutation of these com= ponents is an equivalence of the ambient type. 

This implies that iscontr (weq Type_i Type_i)= is not provable in any context that is compatible with the univalent simpl= icial model.

Vlad= imir.

On Oct 27, 2016, at 11:15 AM= , Matthieu Sozeau <mat= thie...@inria.fr> wrote:

Dear all,

  we've been stuck with N. T= abareau and his student Th=C3=A9o Winterhalter on the above question. Is it= the case that all equivalences between a universe and itself are equivalen= t to the identity? We can't seem to prove (or disprove) this from univalenc= e 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 e= mail to H= omotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--Apple-Mail=_96FC99C1-CD63-4F21-9E77-3EDBEA45FA9F--