From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.165.14 with SMTP id c14mr770683ywh.67.1476310665328; Wed, 12 Oct 2016 15:17:45 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.44.208 with SMTP id e16ls4301672otd.6.gmail; Wed, 12 Oct 2016 15:17:44 -0700 (PDT) X-Received: by 10.200.41.78 with SMTP id z14mr907935qtz.33.1476310664769; Wed, 12 Oct 2016 15:17:44 -0700 (PDT) Return-Path: Received: from pps3.ias.edu (pps3.ias.edu. [192.16.204.88]) by gmr-mx.google.com with ESMTPS id w124si691257ywc.4.2016.10.12.15.17.44 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 12 Oct 2016 15:17:44 -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 u9CMHhYe011235 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Wed, 12 Oct 2016 18:17:43 -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 u9CMHhMW011228; Wed, 12 Oct 2016 18:17:43 -0400 X-Proofpoint-Sentinel: stfsU2FsdGVkX19Uy+ZM3QtPGDmVUy2d3vxbA1PJIbeRQEWjaAHstkO4WeYJ Pc/7b7vmfsQWZ1se2sH2AVBzos0jr5zBo1p1TMyVo+coMyuBkeWUCBYqgIrFaXxruQ6C7eon Received: from imap.math.ias.edu (imap.math.ias.edu [172.16.41.5]) by pps3.ias.edu with ESMTP id u9CMHhPI011227 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Wed, 12 Oct 2016 18:17:43 -0400 Received: from pool-173-72-20-3.cmdnnj.fios.verizon.net ([173.72.20.3] helo=vladimirs-mbp-2.home) by imap.math.ias.edu with esmtpsa (TLSv1:DHE-RSA-AES256-SHA:256) (Exim 4.80.1) (envelope-from ) id 1buRqJ-0005LF-An; Wed, 12 Oct 2016 18:17:43 -0400 Subject: Re: [HoTT] Re: Joyal's version of the notion of equivalence Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) Content-Type: multipart/signed; boundary="Apple-Mail=_065855AC-DD89-4BB5-BC92-6F9B4F433AF8"; protocol="application/pgp-signature"; micalg=pgp-sha512 X-Pgp-Agent: GPGMail From: Vladimir Voevodsky In-Reply-To: Date: Wed, 12 Oct 2016 18:17:42 -0400 Cc: "Prof. Vladimir Voevodsky" , Martin Escardo , =?utf-8?Q?=22Joyal=2C_Andr=C3=A9=22?= , "HomotopyT...@googlegroups.com" Message-Id: 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> To: Peter LeFanu Lumsdaine X-Mailer: Apple Mail (2.3124) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-10-12_13:,, 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-1610120371 X-IAS-PPS-PHISH: NO --Apple-Mail=_065855AC-DD89-4BB5-BC92-6F9B4F433AF8 Content-Type: multipart/alternative; boundary="Apple-Mail=_47439F64-49CB-4CEC-8007-2AE70AC006B6" --Apple-Mail=_47439F64-49CB-4CEC-8007-2AE70AC006B6 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 I think the clearest formulation is my original one - as the condition of c= ontractibility of the h-fibers. This is also the first form in which it was introduced and the first explic= it formulation and proof of the fact that it is a proposition. Vladimir. > On Oct 12, 2016, at 5:45 AM, Peter LeFanu Lumsdaine = wrote: >=20 > > Although I can see formal proofs that Joyal-equivalence is a propositio= n (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. >=20 > Like Andr=C3=A9 suggested, I feel the nicest viewpoint is the fact that t= he =E2=80=9Cfree (=E2=88=9E,1)-category on a Joyal-equivalence=E2=80=9D is = contractible. At least in terms of intuition, the conceptually clearest ar= gument I know for that is as follows. >=20 > Look at the *=E2=88=9E-groupoidification* of this free (=E2=88=9E,1)-cate= gory, considered as a space. This is a cell complex which we can easily pi= cture: two points x, y, three paths f, g, g' between x and y, and 2-cells g= iving homotopies f ~ g, f ~ g'. It=E2=80=99s very clear geometrically that= this is contractible. >=20 > But =E2=80=94 the =E2=80=9Cfree (=E2=88=9E,1)-category on a Joyal equival= ence=E2=80=9D is already an =E2=88=9E-groupoid =E2=80=94 and =E2=88=9E-grou= poidification is idempotent, since groupoids are a full subcategory. So th= e original (=E2=88=9E,1)-category is equivalent to its groupoidification, s= o is contractible. >=20 > The same approach works for seeing why half-adjoint equivalences are good= , but non-adjoint and bi-adjoint equivalences are not. So as regards intui= tion, I think this is very nice. However, I suspect that if one looks at a= ll 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 propositi= on=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 elementa= ry proof of the same fact. >=20 >=20 > The earliest explicit discussion I know of this issue (i.e.=E2=80=9Ccontr= actibility of the walking equivalence as a quality criterion for structured= notions of equivalence) is in Steve Lack=E2=80=99s =E2=80=9CA Quillen Mode= l Structure for Bicategories=E2=80=9D, fixing an error in his earlier =E2= =80=9CA Quillen Model Structure for 2-categories=E2=80=9D, where he had use= d non-adjoint equivalences =E2=80=94 see http://maths.mq.edu.au/~slack/pape= rs/qmc2cat.html Since = 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. 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. >=20 > And for Joyal-equivalences, I don=E2=80=99t know anywhere they=E2=80=99re= explicitly discussed at all, before HoTT. Like Mart=C3=ADn, I=E2=80=99d b= e really interested if anyone does know any earlier sources for them! >=20 > =E2=80=93p. >=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=_47439F64-49CB-4CEC-8007-2AE70AC006B6 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 I think the cleare= st formulation is my original one - as the condition of contractibility of = the h-fibers.

This is a= lso the first form in which it was introduced and the first explicit formul= ation and proof of the fact that it is a proposition. 

Vladimir.
<= br class=3D"">


On Oc= t 12, 2016, at 5:45 AM, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrote:

=
> Although I can see formal proofs that Joyal-equivalenc= e is a proposition (or h-proposition), I am still trying to find the best f= ormal 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 fe= el the nicest viewpoint is the fact that the =E2=80=9Cfree (=E2=88=9E,1)-ca= tegory on a Joyal-equivalence=E2=80=9D is contractible.  At least in t= erms 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)-cat= egory, considered as a space.  This is a cell complex which we can eas= ily picture: two points x, y, three paths f, g, g' between x and y, and 2-c= ells giving homotopies f ~ g, f ~ g'.  It=E2=80=99s very clear geometr= ically 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-groupoidification is idempotent, since groupoids are a full subc= ategory.  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 e= quivalences are good, but non-adjoint and bi-adjoint equivalences are not.&= nbsp; 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 fra= mework 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 lit= tle unsatisfactory formally, as it (a) needs a lot of background, and (b) m= ay need to rely on some more elementary proof of the same fact.


The earliest explicit discussion I know of th= is issue (i.e.=E2=80=9Ccontractibility of the walking equivalence as a qual= ity 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 a= n error in his earlier =E2=80=9CA Quillen Model Structure for 2-categories= =E2=80=9D, where he had used non-adjoint equivalences =E2=80=94 see http://ma= ths.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-adjointne= ss.  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 bette= r is articulated, before Lack. 

And for Joyal-equivalences, I don=E2=80=99t know anywhe= re they=E2=80=99re explicitly discussed at all, before HoTT.  Like Mar= t=C3=ADn, I=E2=80=99d be really interested if anyone does know any earlier = sources for them!

=E2=80=93p.

--
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=_47439F64-49CB-4CEC-8007-2AE70AC006B6-- --Apple-Mail=_065855AC-DD89-4BB5-BC92-6F9B4F433AF8 Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=signature.asc Content-Type: application/pgp-signature; name=signature.asc Content-Description: Message signed with OpenPGP using GPGMail -----BEGIN PGP SIGNATURE----- Comment: GPGTools - https://gpgtools.org iQEcBAEBCgAGBQJX/raGAAoJEH5eMY79Hy7tMU8IAI1aEu6NG27N+TRGpgqvnMnd K46TyWByp88y09rzv57dyQP44rcYJMnidV5abkEXcHBhEAwfRzE6v6UACH6GC54O oDDocPWAyk25ckX93sStaVbr+Wxmgqn1PLFtBK2pypn/gH0GLdhpIA6SsEujz4Vr 35l9UwMVh7KNIpb+wnjw1ro9sx5/MghpISSOsqSj1KyXqzG0IzxzPnfnsdTua4Qa aypr/NYaLMKiTuLRoXqCUTNrvmYy48Gaf/zcqnznpcLOB+8EQLDtMt886l79CCDL ZvzSfu6kdF02CVlJ7DXrbkt5cvKtR7ObPD3+tBs2PvX/+QSNAEe+FchVHFfoKkc= =kDxQ -----END PGP SIGNATURE----- --Apple-Mail=_065855AC-DD89-4BB5-BC92-6F9B4F433AF8--