From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.36.60.15 with SMTP id m15mr2840636ita.5.1476401226624; Thu, 13 Oct 2016 16:27:06 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.141.15 with SMTP id p15ls2621143iod.36.gmail; Thu, 13 Oct 2016 16:27:03 -0700 (PDT) X-Received: by 10.107.181.144 with SMTP id e138mr2746543iof.95.1476401223217; Thu, 13 Oct 2016 16:27:03 -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 p70si2109909vkd.0.2016.10.13.16.27.03 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 13 Oct 2016 16:27:03 -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 1bupOw-00073C-Mu for HomotopyT...@googlegroups.com; Fri, 14 Oct 2016 00:27:02 +0100 Received: from host86-137-209-253.range86-137.btcentralplus.com ([86.137.209.253] helo=[192.168.1.73]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1bupOv-0005QU-G4 for HomotopyT...@googlegroups.com using interface auth-smtp.bham.ac.uk; Fri, 14 Oct 2016 00:27:02 +0100 To: "HomotopyT...@googlegroups.com" From: Martin Escardo Subject: Joyal equivalence II Message-ID: <7377a68d-def8-6147-0310-a4347990e91b@googlemail.com> Date: Fri, 14 Oct 2016 00:26:55 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.3.0 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 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) Define (where "=" is the identity type) f:X->Y has a section := Sigma(s:Y->X), f.s = id. f:X->Y has a retraction := Sigma(r:Y->X), r.f = id. f:X->Y is a Joyal equivalence := f has a section * f has a retraction. We discussed that the type "f is a Joyal equivalence" is always a proposition, although the types "f has a section" and "f has a retraction" are not in general propositions, but rather structure or data on f, of course. For X:U and A:X->U, define there is a unique x:X s.t. A(x) := isContr(Sigma(x:X), A(x)), there is at most one x:X s.t. A(x) := isProp (Sigma(x:X), A(x)). These (are always propositions and hence) are not in general equivalent to the naive formulations copied from first-order mathematics in set theory to type theory. With this terminology, "f:X->Y is a Voevodsky equivalence" reads "for every y:Y there is a unique x:X such that f(x)=y". Now, it is easy to check that, for any A,B:U, isProp(A * B) <-> (A -> isProp B) * (B -> isProp A), where of course the logical equivalence can be replaced by an equivalence, by univalence, as the lhs and rhs types are propositions, but this is unimportant here. Because we know that the Joyal equivalence of f:X->Y is always a proposition, it follows that we always have f has a section -> f has at most one retraction, and f has a retraction -> f has at most one section. Hence we recover what is true in set theory, for types more general than sets, by considering the right notion of there-is-at-most-one. But surely homotopy theorists knew this too. Notice also that, in each implication, it is possible to change the Sigma in the premise to an existential quantifier (a -1-truncated Sigma), because the conclusion is a proposition, to get the same conclusion. And conversely if we had stated the result with the existential quantifier, we would recover the result with Sigma, as it is a stronger hypothesis (or has more data available). (What are the shortest proofs of each of these two implications in univalent type theory?) Martin