From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.198.13 with SMTP id w13mr7265637iof.32.1476037922541; Sun, 09 Oct 2016 11:32:02 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.156.13 with SMTP id f13ls2963601ioe.45.gmail; Sun, 09 Oct 2016 11:31:59 -0700 (PDT) X-Received: by 10.107.161.1 with SMTP id k1mr3053872ioe.52.1476037919572; Sun, 09 Oct 2016 11:31:59 -0700 (PDT) Return-Path: Received: from sun61.bham.ac.uk (sun61.bham.ac.uk. [147.188.128.150]) by gmr-mx.google.com with ESMTPS id a62si1856618vke.2.2016.10.09.11.31.59 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 09 Oct 2016 11:31:59 -0700 (PDT) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) client-ip=147.188.128.150; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 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 sun61.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1btItC-0008Bj-Mr; Sun, 09 Oct 2016 19:31:58 +0100 Received: from host86-137-209-253.range86-137.btcentralplus.com ([86.137.209.253] helo=[192.168.1.112]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1btItC-0008KT-Cw using interface auth-smtp.bham.ac.uk; Sun, 09 Oct 2016 19:31:58 +0100 Subject: Re: [HoTT] Re: Joyal's version of the notion of equivalence To: =?UTF-8?Q?Joyal=2c_Andr=c3=a9?= , "HomotopyT...@googlegroups.com" References: <963893a3-bfdf-d9bd-8961-19bab69e0f7c@googlemail.com> <25c7daf7-8c0f-97de-7d3d-34851bf50a98@googlemail.com> <8C57894C7413F04A98DDF5629FEC90B138BCC04E@Pli.gst.uqam.ca> From: Martin Escardo Message-ID: Date: Sun, 9 Oct 2016 19:31:58 +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: <8C57894C7413F04A98DDF5629FEC90B138BCC04E@Pli.gst.uqam.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) Thanks, Andre. I guess I will have to learn more to understand/appreciate this. Nevertheless, it is still quite interesting that (1) Joyal-equivalence is always a proposition in MLTT + funext, and that (2) it is MLTT+funext (logically) equivalent to Voevodsky equivalence. Independently of the homotopical motivation, this formulation of equivalence is intriguing and elegant. Best, Martin On 08/10/16 18:34, Joyal, André wrote: > Dear Martin, > > I would be surprised if this characterisation of (homotopy) equivalence has not been considered by other peoples. > The characterisation arises naturally in the theory of quasi-categories. > Let me try to explain. > > Let J is the nerve of the groupoid generated by one isomorphism u:0--->1. > It happens that an arrow $f$ in a quasi-category C is invertible in the homotopy category Ho(C) if > and only if it is the image of the arrow $u$ by a map J--->C. > The n-skeleton S^n of the simplicial set J is a simplicial model of the n-sphere (with two nodes 0 and 1). > For example, the 1-skeleton S^1 is a graph with two nodes 0 and 1 and two arrows u:0--->1 and v:1--->0. > The 2-skeleton S^2 is a obtained from S^1 by attaching two triangles (=2-simplices) representing two > homotopies vu-->id_0 and uv-->id_1. But none of the inclusions S^n--->J > is a weak categorical equivalence (in fact none is a weak homotopy equivalence). > Let me say that an extension Delta[1]--->K (=monomorphism) is a *good approximation* of J > if the map K-->pt is a weak categorical equivalence (ie if K is weakly categorically contractible) > For example, the n-skeleton S^n of J is the union of two n-disks S^n(+) and S^n(-). > If n\geq 3, then the disks S^n(+) and S^n(-) are good approximation if J. > In general, an extension Delta[1]--->K is a good approximation of J if and only > if Ho(K) is a groupoid and the map K--->1 is a weak homotopy equivalence (ie $K$ is weakly homotopy contractible). > For example, let U be the union of the outer faces \partial_3Delta[3] and \partial_0Delta[3] > of the 3-simplex Delta[3]. The simplicial set U consists of two triangles 0-->1--->2 and > 1--->2---->3 glued together along the edge 1-->2. Consider the quotient q:U--->K > obtained by identifying the edge 0-->2 to a point q(0)=q(2) and the edge 1-->3 of to a point q(1)=q(3). > The simplicial set K has two vertices, q(0) and q(1), and three edges > a:q(0)-->q(1), b:q(1)--->q(0) and c:q(0)-->q(1) respectively the image by q of the edges 0-->1, 1--->2 and 2--->3. > It is easy to verify that Ho(K) is a groupoid and that K is weakly homotopy contractible. > > > I hope these explanations are not too obscure! > > > Best regards, > André > > > ________________________________________ > From: 'Martin Escardo' via Homotopy Type Theory [HomotopyT...@googlegroups.com] > Sent: Friday, October 07, 2016 8:21 PM > To: HomotopyT...@googlegroups.com > Subject: Re: [HoTT] Re: Joyal's version of the notion of equivalence > > On 08/10/16 00:51, 'Martin Escardo' via Homotopy Type Theory wrote: >> This shouldn't have happened (it seems like a bug): > > Oh, well. Let me retype everything again from memory, in a shorter > way, and then this time send it to everybody. > > The main insight of univalent type theory is the formulation of > equivalence (as e.g. the contractibility of all fibers) so that it is > a proposition. > > An equivalent formulation, attributed to Joyal, and discussed in the > Book, is that the function has a given left inverse and that the > function also has a given right inverse, where both "given" are > expressed with Sigma. One can prove that this notion of > Joyal-equivalence is a proposition, in MLTT, assuming funext, which is > nice and slightly surprising at first sight. > > But where does this formulation of the notion of equiavelence come from? > > Best, > Martin > > -- > 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. >