From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.13.253.197 with SMTP id n188mr7935902ywf.114.1476039423471; Sun, 09 Oct 2016 11:57:03 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.33.60 with SMTP id i57ls8261367otb.48.gmail; Sun, 09 Oct 2016 11:57:02 -0700 (PDT) X-Received: by 10.157.52.225 with SMTP id t30mr4158332otd.129.1476039422917; Sun, 09 Oct 2016 11:57:02 -0700 (PDT) Return-Path: Received: from data.hamecon.telecom.uqam.ca (mail2.uqam.ca. [132.208.246.165]) by gmr-mx.google.com with ESMTP id w124si1073850ywc.4.2016.10.09.11.57.02 for ; Sun, 09 Oct 2016 11:57:02 -0700 (PDT) Received-SPF: pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.165 as permitted sender) client-ip=132.208.246.165; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.165 as permitted sender) smtp.mailfrom=JOYAL...@uqam.ca Authentication-Results: data2.hamecon.telecom.uqam.ca; spf=None smtp.mailfrom=joyal...@uqam.ca; spf=None smtp.helo=postm...@MISSIVE.gst.uqam.ca Received-SPF: None (data2.hamecon.telecom.uqam.ca: no sender authenticity information available from domain of joyal...@uqam.ca) identity=mailfrom; client-ip=132.208.246.209; receiver=data2.hamecon.telecom.uqam.ca; envelope-from="joyal...@uqam.ca"; x-sender="joyal...@uqam.ca"; x-conformance=spf_only Received-SPF: None (data2.hamecon.telecom.uqam.ca: no sender authenticity information available from domain of postm...@MISSIVE.gst.uqam.ca) identity=helo; client-ip=132.208.246.209; receiver=data2.hamecon.telecom.uqam.ca; envelope-from="joyal...@uqam.ca"; x-sender="postm...@MISSIVE.gst.uqam.ca"; x-conformance=spf_only X-Cloudmark-SP-Filtered: true X-Cloudmark-SP-Result: =?us-ascii?q?v=3D2=2E1_cv=3DWODfJiYR_c=3D1_sm=3D2_tr?= =?us-ascii?q?=3D0_a=3DzdVg5ADNf/sAC0uRWyjItQ=3D=3D=3A17?= =?us-ascii?q?_a=3DSgJDDHH=5FwjgA=3A10_a=3D8nJEP1OIZ-IA=3A10_a=3DCH0kA5Ccgfc?= =?us-ascii?q?A=3A10_a=3DmK=5FAVkanAAAA=3A8?= =?us-ascii?q?_a=3D4RBUngkUAAAA=3A8_a=3D1XWaLZrsAAAA=3A8_a=3DbG0RpiU70iA5N75?= =?us-ascii?q?-CGEA=3A9?= =?us-ascii?q?_a=3DqJ72w3QHVfVChz5m=3A21_a=3DL0tI1LXobtEuwQW3=3A21_a=3DwPNLv?= =?us-ascii?q?fGTeEIA=3A10?= =?us-ascii?q?_a=3Dc4S9Whzb7AQA=3A10_a=3D3gWm3jAn84ENXaBijsEo=3A22_a=3D=5Fsb?= =?us-ascii?q?A2Q-Kp09kWB8D3iXc=3A22?= =?us-ascii?q?_a=3DnJcEw6yWrPvoIXZ49MH8=3A22?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A2BkBQCrkfpX/9H20IRdHQYMgz0BAQEBA?= =?us-ascii?q?R1XfAcBgzegdpY8GweFfgKBejwQAQIBAQEBAQEBXieEYQEBAQQnJzsCAQgNBAQ?= =?us-ascii?q?BAQEKJDEBHQgCBAEHBwQBBxUEiBUDFw69BQ2DZAEBAQEBAQEBAgEBAQEBAQEBG?= =?us-ascii?q?wWLEoJHgVIRAR6DLoIvBY51iwqGJ5NWhXSMd4N/NR8lhQByB4VagSABfwEBAQ?= X-IPAS-Result: =?us-ascii?q?A2BkBQCrkfpX/9H20IRdHQYMgz0BAQEBAR1XfAcBgzegdpY?= =?us-ascii?q?8GweFfgKBejwQAQIBAQEBAQEBXieEYQEBAQQnJzsCAQgNBAQBAQEKJDEBHQgCB?= =?us-ascii?q?AEHBwQBBxUEiBUDFw69BQ2DZAEBAQEBAQEBAgEBAQEBAQEBGwWLEoJHgVIRAR6?= =?us-ascii?q?DLoIvBY51iwqGJ5NWhXSMd4N/NR8lhQByB4VagSABfwEBAQ?= X-IronPort-AV: E=Sophos;i="5.31,468,1473134400"; d="scan'208";a="161878195" Received: from unknown (HELO MISSIVE.gst.uqam.ca) ([132.208.246.209]) by data2.hamecon.telecom.uqam.ca with ESMTP/TLS/AES256-SHA; 09 Oct 2016 14:56:39 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.160]) by MISSIVE.gst.uqam.ca ([169.254.4.137]) with mapi id 14.02.0387.000; Sun, 9 Oct 2016 14:56:39 -0400 From: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= To: Martin Escardo , "HomotopyT...@googlegroups.com" Subject: RE: [HoTT] Re: Joyal's version of the notion of equivalence Thread-Topic: [HoTT] Re: Joyal's version of the notion of equivalence Thread-Index: AQHSIPWqfQhwWQWowESuICWJpmirZ6Cd9QCAgACq52CAAhgRAP//vsuy Date: Sun, 9 Oct 2016 18:56:38 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B138BCCE8B@Pli.gst.uqam.ca> References: <963893a3-bfdf-d9bd-8961-19bab69e0f7c@googlemail.com> <25c7daf7-8c0f-97de-7d3d-34851bf50a98@googlemail.com> <8C57894C7413F04A98DDF5629FEC90B138BCC04E@Pli.gst.uqam.ca>, In-Reply-To: Accept-Language: en-US, en-CA Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [132.208.216.81] Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 Dear Martin, There are many variations. For example, a homotopy equivalence can be defin= ed to be a pair of maps f:a--->b and g:b--->a equipped with a pair of homotopies= =20 alpha:gf--->id_a and beta:fg --->id_b satisfying *one*(and only one) of the= adjunction (=3Dtriangle) identities. Best, Andr=E9 ________________________________________ From: Martin Escardo [escardo...@googlemail.com] Sent: Sunday, October 09, 2016 2:31 PM To: Joyal, Andr=E9; HomotopyT...@googlegroups.com Subject: Re: [HoTT] Re: Joyal's version of the notion of equivalence 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=E9 wrote: > Dear Martin, > > I would be surprised if this characterisation of (homotopy) equivalence h= as 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 h= omotopy 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 (=3D= 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 equiva= lence). > Let me say that an extension Delta[1]--->K (=3Dmonomorphism) is a *good a= pproximation* of J > if the map K-->pt is a weak categorical equivalence (ie if K is weakly c= ategorically contractible) > For example, the n-skeleton S^n of J is the union of two n-disks S^n(+) a= nd 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 an= d 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)=3Dq(2) and the edg= e 1-->3 of to a point q(1)=3Dq(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 homoto= py contractible. > > > I hope these explanations are not too obscure! > > > Best regards, > Andr=E9 > > > ________________________________________ > From: 'Martin Escardo' via Homotopy Type Theory [HomotopyT...@googlegroup= s.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. >