From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.200.53.22 with SMTP id y22mr1030846qtb.58.1476316559270; Wed, 12 Oct 2016 16:55:59 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.12.76 with SMTP id w73ls1760823ioi.3.gmail; Wed, 12 Oct 2016 16:55:56 -0700 (PDT) X-Received: by 10.107.195.194 with SMTP id t185mr1165809iof.7.1476316556606; Wed, 12 Oct 2016 16:55:56 -0700 (PDT) Return-Path: Received: from sun60.bham.ac.uk (sun60.bham.ac.uk. [147.188.128.137]) by gmr-mx.google.com with ESMTPS id t8si1478035vkb.2.2016.10.12.16.55.56 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 12 Oct 2016 16:55:56 -0700 (PDT) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) client-ip=147.188.128.137; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Received: from [147.188.128.54] (helo=mailer3) by sun60.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1buTNK-0001bh-PO; Thu, 13 Oct 2016 00:55:54 +0100 Received: from host86-137-209-253.range86-137.btcentralplus.com ([86.137.209.253] helo=[192.168.1.73]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1buTNK-0002d3-FU using interface auth-smtp.bham.ac.uk; Thu, 13 Oct 2016 00:55:54 +0100 Subject: Re: [HoTT] Re: Joyal's version of the notion of equivalence To: Vladimir Voevodsky , Peter LeFanu Lumsdaine References: <963893a3-bfdf-d9bd-8961-19bab69e0f7c@googlemail.com> <25c7daf7-8c0f-97de-7d3d-34851bf50a98@googlemail.com> <8C57894C7413F04A98DDF5629FEC90B138BCC04E@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B138BCCE8B@Pli.gst.uqam.ca> Cc: =?UTF-8?Q?Joyal=2c_Andr=c3=a9?= , "HomotopyT...@googlegroups.com" From: Martin Escardo Message-ID: <99874c3d-46e7-cf41-e58e-63183ae10d74@googlemail.com> Date: Thu, 13 Oct 2016 00:55:54 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.3.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-BHAM-SendViaRouter: yes X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom) On 12/10/16 23:17, Vladimir Voevodsky wrote: > I think the clearest formulation is my original one - as the condition > of contractibility of the h-fibers. > > This is also the first form in which it was introduced and the first > explicit formulation and proof of the fact that it is a proposition. Vladimir, I agree with what you say above. I was just trying to understand a particular, interesting case of a situation where we have types P(f) and Q(f) that are not hpropositions in general, but such that the product type P(f)xQ(f) is always an hproposition, as explained in my previous messages. I hoped to get a motivation from homotopy theory, and Andre tried to explain this to me. I do find it rather interesting that the cartesian product of two such types that are not in general hpropositions is always an hproposition. A function can have a section in zillions of ways, and also have retraction in just as many ways, and we know in set theory that a function can have both a section and a retraction in at most one way. This is not surprising. But it does surprise me, for the moment, that this is the case in univalent mathematics too, given that we do know that the type of two-sided inverses is in general *not* an hproposition. Best, Martin