From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.66.40.197 with SMTP id z5mr37602pak.164.1476265560263; Wed, 12 Oct 2016 02:46:00 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.43.80 with SMTP id f16ls3394860otd.28.gmail; Wed, 12 Oct 2016 02:45:59 -0700 (PDT) X-Received: by 10.200.44.7 with SMTP id d7mr47874qta.68.1476265559706; Wed, 12 Oct 2016 02:45:59 -0700 (PDT) Return-Path: Received: from mail-ua0-x232.google.com (mail-ua0-x232.google.com. [2607:f8b0:400c:c08::232]) by gmr-mx.google.com with ESMTPS id t8si854338vkb.2.2016.10.12.02.45.59 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 12 Oct 2016 02:45:59 -0700 (PDT) Received-SPF: pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::232 as permitted sender) client-ip=2607:f8b0:400c:c08::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::232 as permitted sender) smtp.mailfrom=p.l.lu...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-ua0-x232.google.com with SMTP id p25so3789056uaa.0 for ; Wed, 12 Oct 2016 02:45:59 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=zCm8yiNI6uu52WBwMb8UMuuzZy6+6eHf56tA7hqxqu0=; b=uhHEvz/z4OiGDMO2ohsQM0itfvYENu+EhFMhXlkQpOyC1f/ybn28S9lenUI21WC7Y9 tUBaMPFbmgKkfoVgKo4G7+DVgSyJYZa8+y8jSocJfeKcRA3ZzmDaLJvXVhxj9setUOs1 bRxGeafInfRArruTQSbHr7p4nr3RbeOzCQUkKJndcjAn6oqJwp6DS8NMwgtvDAr0pRtz N+pQWpj/g2Eilnfq7BbpcFqtiV2EiXIj9OJIrGhbZoETnMn37yj95CJmfj0VM9edKAvR 1UbVVRtdtzq41cnaQnLTKQC23qcFVoziV90XZfrSial0rLKI5LXFtptzn7bCoxPwnxJe 556A== X-Gm-Message-State: AA6/9RmUYSIqWYXmxVEH/8Fa4TJ3KzxnMOCuUbgb8DAOhBGr6sBMnrVQuXxO5qI6155EijQXI0VuN8lsDK9XBQ== X-Received: by 10.176.85.211 with SMTP id w19mr56779uaa.65.1476265559514; Wed, 12 Oct 2016 02:45:59 -0700 (PDT) MIME-Version: 1.0 Received: by 10.176.82.152 with HTTP; Wed, 12 Oct 2016 02:45:59 -0700 (PDT) In-Reply-To: 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> From: Peter LeFanu Lumsdaine Date: Wed, 12 Oct 2016 11:45:59 +0200 Message-ID: Subject: Re: [HoTT] Re: Joyal's version of the notion of equivalence To: Martin Escardo Cc: =?UTF-8?Q?Joyal=2C_Andr=C3=A9?= , "HomotopyT...@googlegroups.com" Content-Type: multipart/alternative; boundary=f403045ddd8e44f423053ea7dc8a --f403045ddd8e44f423053ea7dc8a Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable > Although I can see formal proofs that Joyal-equivalence is a proposition (or h-proposition), I am still trying to find the best formal proof that uncovers the essence of this fact. This is why I asked the question of were this formulation of equivalence comes from. Like Andr=C3=A9 suggested, I feel the nicest viewpoint is the fact that the =E2=80=9Cfree (=E2=88=9E,1)-category on a Joyal-equivalence=E2=80=9D is con= tractible. At least in terms of intuition, the conceptually clearest argument I know for that is as follows. Look at the *=E2=88=9E-groupoidification* of this free (=E2=88=9E,1)-catego= ry, considered as a space. This is a cell complex which we can easily picture: two points x, y, three paths f, g, g' between x and y, and 2-cells giving homotopies f ~ g, f ~ g'. It=E2=80=99s very clear geometrically that this is contractib= le. But =E2=80=94 the =E2=80=9Cfree (=E2=88=9E,1)-category on a Joyal equivalen= ce=E2=80=9D is already an =E2=88=9E-groupoid =E2=80=94 and =E2=88=9E-groupoidification is idempotent,= since groupoids are a full subcategory. So the original (=E2=88=9E,1)-category is equivalent to = its groupoidification, so is contractible. The same approach works for seeing why half-adjoint equivalences are good, but non-adjoint and bi-adjoint equivalences are not. So as regards intuition, I think this is very nice. However, I suspect that if one looks at all the work that goes into setting up the framework needed, then somewhere one will have already used some form of =E2=80=9Cequivalence is a proposition=E2=80=9D. So this is perhaps a little unsatisfactory formally,= as it (a) needs a lot of background, and (b) may need to rely on some more elementary proof of the same fact. The earliest explicit discussion I know of this issue (i.e.=E2=80=9Ccontrac= tibility of the walking equivalence as a quality criterion for structured notions of equivalence) is in Steve Lack=E2=80=99s =E2=80=9CA Quillen Model Structure = for Bicategories=E2=80=9D, fixing an error in his earlier =E2=80=9CA Quillen Mo= del Structure for 2-categories=E2=80=9D, where he had used non-adjoint equivalences =E2= =80=94 see http://maths.mq.edu.au/~slack/papers/qmc2cat.html Since it=E2=80=99s just 2-categorical, he=E2=80=99s able to use fully adjoint equivalences =E2=80= =94 doesn=E2=80=99t have to worry about half-adjointness/coherent-adjointness. Adjoint equivalences of course go back much further =E2=80=94 but I don=E2=80=99t know anywhere = that this *reason* why they=E2=80=99re better is articulated, before Lack. And for Joyal-equivalences, I don=E2=80=99t know anywhere they=E2=80=99re e= xplicitly discussed at all, before HoTT. Like Mart=C3=ADn, I=E2=80=99d be really int= erested if anyone does know any earlier sources for them! =E2=80=93p. --f403045ddd8e44f423053ea7dc8a Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
> Although I can see formal proofs that Joyal-equi= valence is a proposition (or h-proposition), I am still trying to find the = best formal proof that uncovers the essence of this fact. This is why I ask= ed the question of were this formulation of equivalence comes from.

Like Andr=C3=A9 suggested, I feel the nicest viewpoint is = the fact that the =E2=80=9Cfree (=E2=88=9E,1)-category on a Joyal-equivalen= ce=E2=80=9D is contractible.=C2=A0 At least in terms of intuition, the conc= eptually clearest argument I know for that is as follows.

Look at the *=E2=88=9E-groupoidification* of this free (=E2=88=9E,1)= -category, considered as a space.=C2=A0 This is a cell complex which we can= easily picture: two points x, y, three paths f, g, g' between x and y,= and 2-cells giving homotopies f ~ g, f ~ g'.=C2=A0 It=E2=80=99s very c= lear geometrically that this is contractible.

But = =E2=80=94 the =E2=80=9Cfree (=E2=88=9E,1)-category on a Joyal equivalence= =E2=80=9D is already an =E2=88=9E-groupoid =E2=80=94 and =E2=88=9E-groupoid= ification is idempotent, since groupoids are a full subcategory.=C2=A0 So t= he original (=E2=88=9E,1)-category is equivalent to its groupoidification, = so is contractible.

The same approach works for se= eing why half-adjoint equivalences are good, but non-adjoint and bi-adjoint= equivalences are not.=C2=A0 So as regards intuition, I think this is very = nice.=C2=A0 However, I suspect that if one looks at all the work that goes = into setting up the framework needed, then somewhere one will have already = used some form of =E2=80=9Cequivalence is a proposition=E2=80=9D.=C2=A0 So = this is perhaps a little unsatisfactory formally, as it (a) needs a lot of = background, and (b) may need to rely on some more elementary proof of the s= ame fact.


The earliest ex= plicit discussion I know of this issue (i.e.=E2=80=9Ccontractibility of the= walking equivalence as a quality criterion for structured notions of equiv= alence) is in Steve Lack=E2=80=99s =E2=80=9CA Quillen Model Structure for B= icategories=E2=80=9D, fixing an error in his earlier =E2=80=9CA Quillen Mod= el Structure for 2-categories=E2=80=9D, where he had used non-adjoint equiv= alences =E2=80=94 see http://maths.mq.edu.au/~slack/papers/qmc2cat.html =C2=A0Since = it=E2=80=99s just 2-categorical, he=E2=80=99s able to use fully adjoint equ= ivalences =E2=80=94 doesn=E2=80=99t have to worry about half-adjointness/co= herent-adjointness.=C2=A0 Adjoint equivalences of course go back much furth= er =E2=80=94 but I don=E2=80=99t know anywhere that this *reason* why they= =E2=80=99re better is articulated, before Lack.=C2=A0

<= div>And for Joyal-equivalences, I don=E2=80=99t know anywhere they=E2=80=99= re explicitly discussed at all, before HoTT.=C2=A0 Like Mart=C3=ADn, I=E2= =80=99d be really interested if anyone does know any earlier sources for th= em!

=E2=80=93p.
--f403045ddd8e44f423053ea7dc8a--