From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.36.50.149 with SMTP id j143mr357073ita.15.1476278476398; Wed, 12 Oct 2016 06:21:16 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.24.75 with SMTP id t11ls3580391ott.34.gmail; Wed, 12 Oct 2016 06:21:16 -0700 (PDT) X-Received: by 10.13.227.2 with SMTP id m2mr231977ywe.98.1476278476022; Wed, 12 Oct 2016 06:21:16 -0700 (PDT) Return-Path: Received: from NAM01-BY2-obe.outbound.protection.outlook.com (mail-by2nam01on0109.outbound.protection.outlook.com. [104.47.34.109]) by gmr-mx.google.com with ESMTPS id i124si599061itf.2.2016.10.12.06.21.15 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Wed, 12 Oct 2016 06:21:15 -0700 (PDT) Received-SPF: pass (google.com: domain of j...@uwo.ca designates 104.47.34.109 as permitted sender) client-ip=104.47.34.109; Authentication-Results: gmr-mx.google.com; dkim=pass head...@uwoca.onmicrosoft.com; spf=pass (google.com: domain of j...@uwo.ca designates 104.47.34.109 as permitted sender) smtp.mailfrom=j...@uwo.ca DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=uwoca.onmicrosoft.com; s=selector1-uwo-ca; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version; bh=Q+PlB6QGuCewJhKrwODLTY8e87S17FhZ7Hp/ZAQH0P0=; b=C5Df5ii3zwgIZyonZQgz/FQu86RA8LMoBClCbZlJyq3BFwusloqI0BU1Vz2Shb/2uFvhJlN2EBAMtwmKAOhnj3GcZa6v/fb8OFQC/eMzaXVubYqiXC1Y/a/zI2D83/kjgoEbQIskiRYY/9LNA/Q6H9CUEWyRVIa+FyMj7QZ1OEA= Authentication-Results: spf=none (sender IP is ) smtp.mailfrom=j...@uwo.ca; Received: from speedy (174.116.245.222) by BN6PR11MB1730.namprd11.prod.outlook.com (10.175.98.149) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384_P384) id 15.1.659.11; Wed, 12 Oct 2016 13:21:14 +0000 Received: by speedy (Postfix, from userid 1000) id B435B4C16D9; Wed, 12 Oct 2016 09:21:10 -0400 (EDT) From: Dan Christensen To: Homotopy Type Theory List Subject: Re: Joyal's version of the notion of equivalence In-Reply-To: (Peter LeFanu Lumsdaine's message of "Wed, 12 Oct 2016 11:45:59 +0200") 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> User-Agent: Gnus/5.130014 (Ma Gnus v0.14) Emacs/24.3 (gnu/linux) Mail-Copies-To: never X-Hashcash: 1:24:161012:homotopytypetheory@googlegroups.com::77NRNWCAOag7/As6:00000000000000000000000000D5Yp Date: Wed, 12 Oct 2016 09:21:10 -0400 Message-ID: <878ttt3dq1.fsf_-_@uwo.ca> MIME-Version: 1.0 Content-Type: text/plain; charset="utf-8" Content-Transfer-Encoding: quoted-printable X-Originating-IP: [174.116.245.222] X-ClientProxiedBy: BN6PR20CA0026.namprd20.prod.outlook.com (10.171.173.12) To BN6PR11MB1730.namprd11.prod.outlook.com (10.175.98.149) Return-Path: j...@uwo.ca X-MS-Office365-Filtering-Correlation-Id: 9bb2268f-5a58-4426-8ead-08d3f2a2a468 X-Microsoft-Exchange-Diagnostics: 1;BN6PR11MB1730;2:AXHxLIsthYpYK3EzRBx6By3GnbfGutb/F1Xn9Lf/oh/ubqopgA4MB7vBhFhh7O6LU+vaBPBVZy+hBwpgCgSoHNujBoitry0E/aAhETk4hQlM+kTyZdYoq3FjyZGSTi63DKNInb/S+ogIYRm5MEF+TBxVLCMJDpnp7+pX+B/5jILD+YDFYOuDZxICwUq6b0ITajL1OboDBsOqU1Y+oPCreA==;3:rU9GDg8g3KQSFrxYr9ye7Mp80WtyEkwuSRc6LKllQpCGbLHKSTuKc8kXeu9jf2lYNndlMzh3HqRlHuO51Bc+FaaPs/yeYylv3xcpCy2YIP5Ukb3OkMpSUpOhi/j7q24+9ad92W6UrNesrp54OHIq7Q==;25:EyerP4RPXMzsqVgP/prTZVcnVNS/7m9AApxiNVk6zcEwuFTDow+mqS5C4+SxLO/TjRVuq4/4az7RLJglkcbCqWmP9ES3CMC7m5vGKOb+Du3gs6AeyE1+ZGPd8hQJ80wqGqc+gIRzCyBMdHkg8MC61UMmRpRu5tglckypzV3IoagK8v/m+uI1QRhL1Pqu0+ZNnGDewCBI1xiOzi9oSFAUWAMkUhJyyLC2st2/yEj+Wj5guB2O+o+LzY8PFqVUJfAI8Qb9SD8UWZAglc0tx82MOyUMVrgIP/jCMZ2jF3fKfSOuu6H4JFVuXd6Daoz/GnfBpov/3nUWsXFibCLxroOVGtsKQv89v+0+Gs6IrNJfpR4G5EQzUI0hFaX4JrXG01rBPFxwKVA9MlcHDjxOw6V8DWI68NNfB7xbk/E+UgrGyAg7s3hIgjOzIMTdECcYNRNl X-Microsoft-Antispam: UriScan:;BCL:0;PCL:0;RULEID:;SRVR:BN6PR11MB1730; X-Microsoft-Exchange-Diagnostics: 1;BN6PR11MB1730;31:q9RL7Zy7/RzpOIy2lPQ72/yzID+4P+IJuICOY67d7dAwgaCq1WRb7XkUBN2Syd3CbSMV2xjwrRUgkKhoe/lIDb6GRlxTKXCObW2WPG4In6rw2gjWIXoR0Z2N4d9FPktabxX+aEbYW/3GijS0GrHb7euaS2ajguWNKz3tDzgf9CfjpCpvNkQEVXGaGFm0rtn0efeUdIjCYCenobKxrlshB1zkvBmslctqrkHiPaP/gnDsI2cDjOZrMRjmpDYymHgy;20:nOoXYHvMrZ0tstYii2CpRFtqVhSIozgOL7I+7zj+ROTK7jDQNNQwl7/8JUPph5r+a3f7Pjs8I07NzrxTFx2gi4PHFFppskJtJQFXQftZSn5w0J+uPdh+WzSsloY71NZzs8ZmRgbn8cBakAErkDOonFk2ub2VgjyniGb/rAjNUmFSyVpSwpTvwEhbwgdjdhw9UiTYJSUpXrXBOvZ/qswiAKIp0NbhEjz/92a0V9RRUh29OzQznB4vI83jcsg5HvLp/IzkgYei22RnhegDtgigdbAGxvR8qeMWlobkowNQEjW6T8BWCUOSwaofGDO3715uiS9ku4joCgthqI3+sgZBRaMJihvrmAZRH50Cw6T0Jcj38qp1/GAQHx1Bs3dgdc5wkPL3Q4feyXOIIqdbkQ9Bum6dNk02AC+ZzyMQn4FMHPYagxOnw6eggnVzRMZ2GmqX5miQS0d+Vsr6D7NXhkaRZV2Mo6oRpkImky/nv1Cx3dsKxWqNyZJKSIt1JJa31NCb X-Microsoft-Antispam-PRVS: X-Exchange-Antispam-Report-Test: UriScan:; X-Exchange-Antispam-Report-CFA-Test: BCL:0;PCL:0;RULEID:(6040176)(601004)(2401047)(8121501046)(5005006)(3002001)(10201501046);SRVR:BN6PR11MB1730;BCL:0;PCL:0;RULEID:;SRVR:BN6PR11MB1730; X-Microsoft-Exchange-Diagnostics: 1;BN6PR11MB1730;4:zcUCFvgb86zGqcJVkj+1F/9oc9VJH0ebVN5cLRqW/EJVjpH7m1AC2jQZuXZIelaISRUjTXa3Ec+1PHqzWYuu/10ogYGih7IzmOBWxsQZLiupqhznip90WJzyVLYgft0pmc+OXHy/ZSWV04JbpteOfac21A40x6ghcNfEO04zoU0Nt/rNHNFhlBvY5OxmsBFxofBmwvZwoIceSfsF5e7RJNMvh8vPx8O4iJupdR1V/aBLpofyx80Ngb1bxDuu8N0C6fpG4L9BW6AMioxuRZ/9m6b8JcQv1MCe52QLF5N5Kda9LsSczU4T/BWj+nGTCBQps5UqAMt75zm9YAgG46YR5IDYDukUFAw+G5E76JsU+HL7iKxmf8ujsyLQcyxngykZNnOjBK06EsJ7dBqRwnMAPA== X-Forefront-PRVS: 0093C80C01 X-Forefront-Antispam-Report: SFV:NSPM;SFS:(10019020)(4630300001)(6009001)(7916002)(189002)(24454002)(199003)(50986999)(50466002)(97736004)(93886004)(36756003)(3846002)(586003)(101416001)(6116002)(46386002)(45336002)(23676002)(8746002)(76176999)(4001350100001)(54356999)(33646002)(450100001)(6916009)(47776003)(2950100002)(107886002)(122856001)(68736007)(5660300001)(92566002)(66066001)(2906002)(83506001)(86362001)(110136003)(7736002)(42186005)(305945005)(105586002)(7846002)(19580405001)(90966002)(19580395003)(106356001)(8676002)(189998001)(52956003)(81166006)(81156014)(74482002);DIR:OUT;SFP:1102;SCL:1;SRVR:BN6PR11MB1730;H:speedy;FPR:;SPF:None;PTR:InfoNoRecords;MX:1;A:1;LANG:en; Received-SPF: None (protection.outlook.com: uwo.ca does not designate permitted sender hosts) X-Microsoft-Exchange-Diagnostics: =?utf-8?B?MTtCTjZQUjExTUIxNzMwOzIzOllRS3VJeG5wYWdBU2xlQ2FvR1BlZU0rbFRt?= =?utf-8?B?SDdWdEZUQ1RSNzJ6RndVRXEwZmQwMm5xNzVIcG1iNGU3SzN5WldPZjBpS3Vz?= =?utf-8?B?RWRNd3REemRVS0IxWnBPQ1JSZmo2T2YzMnQvck11TW5UZ29BSW1aaC9qbG1P?= =?utf-8?B?V3hwa2dwY3Nhd0g1YXIxTVVRN0RqK1RMcnBtV2Vxd3U5RXVmQlJ0YXR1K0ox?= =?utf-8?B?aGxaUGphdk04UnMvd3E1M29HeHgvbGRWMUgyUDhRdUhSNkx6TXRQRDZmWmNF?= =?utf-8?B?cEV6T0c4dHdqU0oyZnowSjhhMXhQT2tSUVdWZXIzZHE1eGp3a2dZeEE4cTdq?= =?utf-8?B?dURVd1htcHJDUmhKNzRTa0ZwMDFOQ3VWcGVUdTFHV3JEbWFNaU9zazk0VEFT?= =?utf-8?B?d2xEQXk4RnZPd1lyb0FvZ3J4cWxZTE5tSVA2VlNnSjBBNE9EbFRXTE9sRFE3?= =?utf-8?B?MC82Y1RYOUg3ZTBkZXVHOHBXamxaemJFRFZMWStnaFgxYjZhUFVyMlNhSW5v?= =?utf-8?B?K2lRbmVnSDJ4eVMxcFI2ZkViYlRSRzJjV0dkb0FSY05jUERYaDhreFVIdkxo?= =?utf-8?B?OTVKUkI4eG9EKzJzanFVck41bVUyQkFuTXZDSEZOTzRWRjlYSGZ4Wi81SFRw?= =?utf-8?B?WXZta0lZMWVxeFlhVVBaQjUxclQrRjVyb2NzM2VSOENaNHlZTkx1ZUpxWVBt?= =?utf-8?B?bnp3RTM2dS9KS1JqbVZ6aVhuazFpc1RxeVlpbkpTVU1LZTRUQWxvYmx1UUVr?= =?utf-8?B?UFBrSk9xVWNJR25BcXNXR3lmM25xd2dUTjg3aEtjV0s5V1JSMTBSVDV1M2wv?= =?utf-8?B?c3VuU2kxTTFBaXdEZDRnVGJsQjFXejFtZW1wQ3IrZGx5UXhKTmhFVyt1WGJw?= =?utf-8?B?WXdZN0YzSlhlOU5nRGNQYW9vL3BuQUQxVllXQy9hL1RmdTlETExBMGtRTzNm?= =?utf-8?B?U1IweG5kQ1hhbG1valF4SGN4clZxam02TThGcExncGhMczU3Z0tZczJHdVdm?= =?utf-8?B?NmdSRzd5UTMxK29nbEtMZmRDUTdPMW1UUGtlUGJLQ1hOeG1PNXV5QjFJaXg1?= =?utf-8?B?SlpRL014L1g1ekRPME1nUDR0Z1dMWW9nM001MyswOEZaT2xxcmZ5cGxhSlpO?= =?utf-8?B?Wm5HdnplYmhpRVR1VldRdFovWnlaZ0kzS2twYm1nVjdjSTJCMGJiZ0hrbFlC?= =?utf-8?B?V3VOdUpjalVpWFEyOWdISHdqc0Y5a2NnYzh1NmRHaE1FRWg1RTJnSmRwV3hp?= =?utf-8?B?ZHJoV0Z3UkVpM1UzNHZLREU3dnNtNXEvRW1zNjRKczBjbys1dFc3WFhuYlpX?= =?utf-8?B?WXBTY1V1cFQxU05qcVNXUUhEdVl5aUZ2Zy9KNityN3lTRDNLU3VmcUJ2UEl2?= =?utf-8?B?Zk52OFg0eFBPTlMrRVBzQXY4bDlLTUZGNDlDbDRBVTVhYytLVDJuUmV6R24y?= =?utf-8?B?NnRwSXJBa25Qc3ExdzdPS2hXNGsxUWx3MUZLQTgva2dHdW54QXZFRjMwZVdr?= =?utf-8?B?b1Y0a0VoUCtibUtKeHk2Tkc0YVlwZlRCY2RacThacmp2ZzBqY21aZUNzMlhv?= =?utf-8?B?L3ZQSEJJSFc4cU9jMmZIRWZkK2dUYXFMajlZeG9JLzVBVTZHUCtsTVRNOFFk?= =?utf-8?B?QlNEcDd4Nk5xZC9yYmFNU1E2eDNGckZ0U2JBNk5WRWVRMGo1blA1ODZobjBY?= =?utf-8?B?SW1NWG1xQjVnc2lTU1hPUGtHbjVFcUdRd1dsV0xNNTY4dmpjWEpkRFl5emo2?= =?utf-8?B?MDZrM1dIWkZsMkI1MWhEZz09?= X-Microsoft-Exchange-Diagnostics: 1;BN6PR11MB1730;6:hRYkeQ0vyK6vCI3NgOINYWwAA/kxWtEyHPy5Qm9Fb4cp5Tw3dBFAITK381ImAJt4Z8fJb3iAC1nLcHdO61yE7OMUZs15c6UZwkpAQLpW3p9krtr4TTQzUgQrMdHVhgdhrRvC3Wit30TqudlVib5iR6iYK0MOagO3dQw5BKHSwHykVAIBr//7WswbfGyqw6HMMAwMiGYr5fIegYDdSCjSU3wRKGUonXcgoTG4AfddarhPGraZQlWhekHWq/Brnk6AUNBGA1MUq02zzjFSEmYZpi64n0xSYgdIXTbbdHHFCOgHK5Ns8R5ce0L0Bir8Xnqh;5:NP2mbL3akM61hlS5guyYuVUNm+KOF2TevjmP+XBsUvrmo9Tw/8MdZ0yxvHX5D2AmtK2yubiRYJWYKeoZDPvUh0LN7/baNqMvDJWC4TgLu9/X6eduNAmnMPkZuMr9+Qyqi7KqhFc2/z3Vwpp6tsbl5emMrWg6OOGBLNSzN7bJUVw=;24:Xb9pmkmxU8P5rhdSRK3ctLXMY0OcyrsQgNrAq9GwmraVNy2P6X18fH64a3MJdQGOvVLRogPKfJCveE1Fytm8tmWie4TtdSe0UZCPPmgCiVU=;7:ZBzVC+EVKi9+P0wAjyR4TjDa9N+0l9hwcCphTevzpscrA3eJukHPcj4OeXdK+QiG/w9SOJGg9wa9rVxwjf1E4fXLKu9VH7PMMiEnPb4pGAZ8FF9BoJB2ZIvjD+uuRg4h2lG50MUaoiF9bi4jnKmFAcb2s0NSGrnGDUyvdEcJwShDWxbCFCEBUpDIZuJP2iL0wrERnbDU/dsxK8w+wITtMbFShTH+nH6sfsFaqHD/FvwHOfnmlZGf5fMvFaI3q3NrP3EzUeF8vIhD2nNMgJYK4RNl/IxZMIL60bfu6Xzpnador8UFUD9liXAP/C1NCVGMmTSDIQb/LaHsShomSmj5fkRBPbXnwY3CXaY4QtAENWU= SpamDiagnosticOutput: 1:99 SpamDiagnosticMetadata: NSPM X-OriginatorOrg: uwo.ca X-MS-Exchange-CrossTenant-OriginalArrivalTime: 12 Oct 2016 13:21:14.5790 (UTC) X-MS-Exchange-CrossTenant-FromEntityHeader: Hosted X-MS-Exchange-Transport-CrossTenantHeadersStamped: BN6PR11MB1730 On Oct 12, 2016, Peter LeFanu Lumsdaine wrote: > 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! I'm not sure if this is what you are looking for, but Exercise 11 in Chapter 0 of Hatcher's "Algebraic Topology" says: Show that f : X -> Y is a homotopy equivalence if there exist maps g, h : Y -> X such that fg =E2=89=83 1 and hf =E2=89=83 1. More generall= y, show that f is a homotopy equivalence if fg and hf are homotopy equivalences. I'm pretty sure this was already there in the original 2002 edition. Of course, this is an easy categorical fact that was well-known, but this is at least an explicit mention of this in the case of homotopy equivalences. Dan