From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.200.38.232 with SMTP id 37mr983547qtp.14.1476312357715; Wed, 12 Oct 2016 15:45:57 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.33.198 with SMTP id s64ls4487616otb.15.gmail; Wed, 12 Oct 2016 15:45:57 -0700 (PDT) X-Received: by 10.13.231.68 with SMTP id q65mr972065ywe.58.1476312357192; Wed, 12 Oct 2016 15:45:57 -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 p131si1669783vkf.1.2016.10.12.15.45.57 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 12 Oct 2016 15:45:57 -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 1buSHc-0005R3-O4 for HomotopyT...@googlegroups.com; Wed, 12 Oct 2016 23:45:56 +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 1buSHc-0006RN-E9 for HomotopyT...@googlegroups.com using interface auth-smtp.bham.ac.uk; Wed, 12 Oct 2016 23:45:56 +0100 Subject: Re: [HoTT] Re: Joyal's version of the notion of equivalence To: Homotopy Type Theory List 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> <878ttt3dq1.fsf_-_@uwo.ca> From: Martin Escardo Message-ID: Date: Wed, 12 Oct 2016 23:45:55 +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: <878ttt3dq1.fsf_-_@uwo.ca> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit 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 14:21, Dan Christensen wrote: > On Oct 12, 2016, Peter LeFanu Lumsdaine wrote: > >> And for Joyal-equivalences, I don’t know anywhere they’re explicitly >> discussed at all, before HoTT. Like Martín, I’d be really interested if >> anyone does know any earlier sources for them! > > I'm not sure if this is what you are looking for, but Exercise 11 in > Chapter 0 of Hatcher's "Algebraic Topology" says: > > Show that f : X -> Y is a homotopy equivalence if there exist maps > g, h : Y -> X such that fg ≃ 1 and hf ≃ 1. More generally, show that > f is a homotopy equivalence if fg and hf are homotopy equivalences. Nice for the historical record as asked by Peter L. But let me try dissect this from the point of view of univalent type theory, and relate it to my question. Joyal-equivalence(f:X->Y) := f has a section * f has a retraction. f has a section := Sigma(g:Y->X), fg ≃ 1. f has a retraction := Sigma(h:Y->X), hf ≃ 1. Remark 1. "Sigma" is not the same thing as "exists". Remark 2. The type "f has a section" is not an hproposition. This means that having a section is structure rather than property. Similarly for "f has a retraction". Remark 3. Existence is truncated structure. So there is no problem *at all* in seeing that f is an equivalence := ||f has a section|| * ||f has a retraction||. (Which is what the above exercise says a priori.) But my question was why, although each of f has a section and f has a retraction individually are structure on f, they become property of f when put together. I know why, as I said, because I am in possession of a proof. But I don't feel I am in possession of a conceptual explanation. Best, Martin