From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.32.230 with SMTP id g99mr481852lji.9.1475886099120; Fri, 07 Oct 2016 17:21:39 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.197.77 with SMTP id v74ls79637wmf.25.canary; Fri, 07 Oct 2016 17:21:38 -0700 (PDT) X-Received: by 10.28.154.147 with SMTP id c141mr55854wme.18.1475886098540; Fri, 07 Oct 2016 17:21:38 -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 u64si363854wmf.0.2016.10.07.17.21.38 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 07 Oct 2016 17:21:38 -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 1bsfOU-00075G-NW for HomotopyT...@googlegroups.com; Sat, 08 Oct 2016 01:21:38 +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 1bsfOU-00089d-Da for HomotopyT...@googlegroups.com using interface auth-smtp.bham.ac.uk; Sat, 08 Oct 2016 01:21:38 +0100 Subject: Re: [HoTT] Re: Joyal's version of the notion of equivalence To: "HomotopyT...@googlegroups.com" References: <963893a3-bfdf-d9bd-8961-19bab69e0f7c@googlemail.com> <25c7daf7-8c0f-97de-7d3d-34851bf50a98@googlemail.com> From: Martin Escardo Message-ID: Date: Sat, 8 Oct 2016 01:21:37 +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: <25c7daf7-8c0f-97de-7d3d-34851bf50a98@googlemail.com> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-BHAM-SendViaRouter: yes X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom) 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