From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.63.238 with SMTP id i43mr1778047ote.5.1476362931199; Thu, 13 Oct 2016 05:48:51 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.29.203 with SMTP id w11ls631866otw.37.gmail; Thu, 13 Oct 2016 05:48:50 -0700 (PDT) X-Received: by 10.237.55.229 with SMTP id j92mr1652951qtb.10.1476362930673; Thu, 13 Oct 2016 05:48:50 -0700 (PDT) Return-Path: Received: from mail-vk0-x22a.google.com (mail-vk0-x22a.google.com. [2607:f8b0:400c:c05::22a]) by gmr-mx.google.com with ESMTPS id p131si2171959vkf.1.2016.10.13.05.48.50 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 13 Oct 2016 05:48:50 -0700 (PDT) Received-SPF: pass (google.com: domain of e.m....@gmail.com designates 2607:f8b0:400c:c05::22a as permitted sender) client-ip=2607:f8b0:400c:c05::22a; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of e.m....@gmail.com designates 2607:f8b0:400c:c05::22a as permitted sender) smtp.mailfrom=e.m....@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-vk0-x22a.google.com with SMTP id q126so22980564vkd.2 for ; Thu, 13 Oct 2016 05:48:50 -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=c+vYLkBTv0jxfLvO9LHQ5gMK9QqMNB8GS+7gnNL/RBY=; b=YMnNFJrvnSvdTt7ufX6oZaRBxjPdIWN+UU+E+rdCmAfh6bqzHYbrFyDCX2MkpmciQj B9aBdNruNjquoe6jFtkhtmw6XElMXf/i9al8zk1tPY2fg4tgAqPrDMwSJuoINtGFbZUT hzgsZNd4T8NDqeWM4XV7FL9x9DgEW6TJMLnvGl2pwJ7TLPNphRjf8/dojizwenq0wNxA hCxbZiuFakh2rKEv8Rx0iNbSR08hH6lk/6jeCQFbejRnxQr5x1F0cN8s2dwvYVaFaY9f E/ejKCXN52zL9pNJArv0XG7rWx5GS5ov7HJ/omOCOAVB/Gy1bjlXlWwMmMJYNlJOitYH A+2Q== X-Gm-Message-State: AA6/9RlF3yDbENVTjjPqhoxi7bvlvt4x9p4mWr+0ZMw78U613o4fig19OE2BU8K5tFStJ3/pKuA9YF5tRvgb9w== X-Received: by 10.194.171.225 with SMTP id ax1mr7091439wjc.48.1476362930242; Thu, 13 Oct 2016 05:48:50 -0700 (PDT) MIME-Version: 1.0 Received: by 10.80.186.15 with HTTP; Thu, 13 Oct 2016 05:48:49 -0700 (PDT) Received: by 10.80.186.15 with HTTP; Thu, 13 Oct 2016 05:48:49 -0700 (PDT) In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B138BD0019@Pli.gst.uqam.ca> 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> <8C57894C7413F04A98DDF5629FEC90B138BD0019@Pli.gst.uqam.ca> From: Egbert Rijke Date: Thu, 13 Oct 2016 08:48:49 -0400 Message-ID: Subject: RE: [HoTT] Re: Joyal's version of the notion of equivalence To: =?UTF-8?B?QW5kcsOpIEpveWFs?= Cc: "HomotopyT...@googlegroups.com" , Martin Escardo , Peter LeFanu Lumsdaine , Vladimir Voevodsky Content-Type: multipart/alternative; boundary=089e013c689e04484c053ebe8889 --089e013c689e04484c053ebe8889 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Dear all, I agree with Vladimir that his notion of equivalence is a very clear one, but that doesn't take away that on some occasions it is really helpful to have Joyal's notion around. For instance, in the definition of localization as a higher inductive type we use Joyal-equivalence, simply to avoid 2-path constructors. With kind regards, Egbert On Oct 13, 2016 3:14 AM, "Joyal, Andr=C3=A9" wrote: > Dear Vladimir, > > I completely agree with you. > > Andr=C3=A9 > ------------------------------ > *From:* homotopyt...@googlegroups.com [homotopytypetheory@ > googlegroups.com] on behalf of Vladimir Voevodsky [vlad...@ias.edu] > *Sent:* Wednesday, October 12, 2016 6:17 PM > *To:* Peter LeFanu Lumsdaine > *Cc:* Prof. Vladimir Voevodsky; Martin Escardo; Joyal, Andr=C3=A9; > HomotopyT...@googlegroups.com > *Subject:* Re: [HoTT] Re: Joyal's version of the notion of equivalence > > 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. > > > > > > On Oct 12, 2016, at 5:45 AM, Peter LeFanu Lumsdaine < > p.l.lu...@gmail.com> wrote: > > > 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 we= re > this formulation of equivalence comes from. > > 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 c= ontractible. 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)-cate= gory, considered > as a space. This is a cell complex which we can easily picture: two poin= ts > 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 contract= ible. > > 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-groupoidification is idempoten= t, since groupoids are a > full subcategory. So the original (=E2=88=9E,1)-category is equivalent t= o 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 loo= ks > 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 formall= y, 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=9Ccontractibility of the walking equivalence as a quality cri= terion 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 > Model 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.h= tml > Since it=E2=80=99s just 2-categorical, he=E2=80=99s able to use fully ad= joint equivalences > =E2=80=94 doesn=E2=80=99t have to worry about half-adjointness/coherent-a= djointness. > 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, be= fore Lack. > > 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 be really i= nterested 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 > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > > > -- > 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. > > -- > 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. > --089e013c689e04484c053ebe8889 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

Dear all,

I agree with Vladimir that his notion of equivalence is a ve= ry clear one, but that doesn't take away that on some occasions it is r= eally helpful to have Joyal's notion around.

For instance, in the definition of localization as a higher = inductive type we use Joyal-equivalence, simply to avoid 2-path constructor= s.

With kind regards,
Egbert


On Oct 13, 2016 3= :14 AM, "Joyal, Andr=C3=A9" <joyal...@uqam.ca> wrote:
Dear Vladimir,

I completely agree with you.

Andr=C3=A9
From: homotopytypetheory@googlegroups.com [homotopytypetheory@googlegroups.com] on behalf of V= ladimir Voevodsky [vla= d...@ias.edu]
Sent: Wednesday, October 12, 2016 6:17 PM
To: Peter LeFanu Lumsdaine
Cc: Prof. Vladimir Voevodsky; Martin Escardo; Joyal, Andr=C3=A9; HomotopyTyp= eTheory@googlegroups.com
Subject: Re: [HoTT] Re: Joyal's version of the notion of equival= ence

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 e= xplicit formulation and proof of the fact that it is a proposition.=C2=A0

Vladimir.





On Oct 12, 2016, at 5:45 AM, Peter LeFanu Lumsdaine <p.l.lu...@gmail.com> wrot= e:

> Although I can see formal proofs that Joyal-equivalence is a prop= osition (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 o= f 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 co= ntractible.=C2=A0 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)-c= ategory, considered as a space.=C2=A0 This is a cell complex which we can e= asily picture: two points x, y, three paths f, g, g' between x and y, a= nd 2-cells giving homotopies f ~ g, f ~ g'.=C2=A0 It=E2=80=99s very clear geometrically that this is contractible.

But =E2=80=94 the =E2=80=9Cfree (=E2=88=9E,1)-category on a Joyal equi= valence=E2=80=9D is already an =E2=88=9E-groupoid =E2=80=94 and =E2=88=9E-g= roupoidification is idempotent, since groupoids are a full subcategory.=C2= =A0 So the original (=E2=88=9E,1)-category is equivalent to its groupoidifi= cation, so is contractible.

The same approach works for seeing why half-adjoint equivalences are g= ood, but non-adjoint and bi-adjoint equivalences are not.=C2=A0 So as regar= ds intuition, I think this is very nice.=C2=A0 However, I suspect that if o= ne 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 same fact.


The earliest explicit discussion I know of this issue (i.e.=E2=80=9Cco= ntractibility of the walking equivalence as a quality criterion for structu= red notions of equivalence) is in Steve Lack=E2=80=99s =E2=80=9CA Quillen M= odel 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 used non-adjoint equivalences =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 equiv= alences =E2=80=94 doesn=E2=80=99t have to worry about half-adjointness/cohe= rent-adjointness.=C2=A0 Adjoint equivalences of course go back much fu= rther =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.=C2=A0

And for Joyal-equivalences, I don=E2=80=99t know anywhere they=E2=80= =99re 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= them!

=E2=80=93p.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
--089e013c689e04484c053ebe8889--