From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.165.14 with SMTP id c14mr1758292ywh.48.1473264655370; Wed, 07 Sep 2016 09:10:55 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.54.178 with SMTP id h47ls566020otc.37.gmail; Wed, 07 Sep 2016 09:10:54 -0700 (PDT) X-Received: by 10.237.44.38 with SMTP id f35mr39938243qtd.18.1473264654664; Wed, 07 Sep 2016 09:10:54 -0700 (PDT) Return-Path: Received: from mail-oi0-x231.google.com (mail-oi0-x231.google.com. [2607:f8b0:4003:c06::231]) by gmr-mx.google.com with ESMTPS id q204si1034787itq.0.2016.09.07.09.10.54 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Sep 2016 09:10:54 -0700 (PDT) Received-SPF: pass (google.com: domain of andrew....@gmail.com designates 2607:f8b0:4003:c06::231 as permitted sender) client-ip=2607:f8b0:4003:c06::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of andrew....@gmail.com designates 2607:f8b0:4003:c06::231 as permitted sender) smtp.mailfrom=andrew....@gmail.com Received: by mail-oi0-x231.google.com with SMTP id m11so32789622oif.1 for ; Wed, 07 Sep 2016 09:10:54 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:in-reply-to:references:from:date:message-id :subject:to:cc:content-transfer-encoding; bh=wBLDeEVUb4KIg8N5xOaOrkwjP0o0OXB4MUrVfQASEOY=; b=ztgYmlYzFjzfOhha3SvSGGI5H13b5dMHaQjjzldt6z42AuFM92jajnx/6TX0KHv7qe 2+YUnuac1ChgQqtkbbs3aWrcebQDdpOTTrsUbyp6US1nGUFtoX92C6phZna9Px/0cqFL 3cSC+RcDgw4UHH5KvjwhDeMnZpm1mA6lU/LrQM9n7Jsa/vedWANFtO2Ss7lQsyWhqrMZ 35XPHM+8nZc9vbOIbps2Pq5U5ntee0xB1bZnwh+D1+bLY/WgCiF3PrChMmqNfou8kIy6 yRX2BP7ccRarLzGERtdkOKG2a6TwyqsNiEoZHa+t+N3+F0O6bGBTuKYb530lfDPrO0zK 1wSQ== X-Gm-Message-State: AE9vXwPvZff4Twll1m+2FI6R5LJTEoJ9Gh9PaHnb+V6rAB2LXvHFycpwa5gOVFLs90tn/2v3JbDmExp6mTYd3g== X-Received: by 10.157.4.200 with SMTP id 66mr37950461otm.171.1473264654411; Wed, 07 Sep 2016 09:10:54 -0700 (PDT) MIME-Version: 1.0 Sender: andrew....@gmail.com Received: by 10.202.218.130 with HTTP; Wed, 7 Sep 2016 09:10:33 -0700 (PDT) In-Reply-To: <9F0041A0-328D-4C4F-8152-3E42305D372E@cs.cmu.edu> References: <9F0041A0-328D-4C4F-8152-3E42305D372E@cs.cmu.edu> From: Andrew Pitts Date: Wed, 7 Sep 2016 17:10:33 +0100 Message-ID: Subject: Re: [HoTT] weak univalence with "beta" implies full univalence To: Dan Licata Cc: Homotopy Type Theory , "Prof. Andrew M Pitts" Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On 7 September 2016 at 16:10, Dan Licata wrote: > What I=E2=80=99m about to say is a trivial consequence of an observation = that Egbert/Martin made a couple of years ago (https://github.com/HoTT/book= /issues/718), so maybe other people have already realized this, but it was = surprising to me. Very spooky: I recently noticed this for myself (though not via the observation you mention) and was just about to ask this list whether it was "well known". > In particular, based on Martin=E2=80=99s observation https://github.com/H= oTT/book/issues/718#issuecomment-65378867 > that any retraction of an identity type is an equivalence: > > retract-of-Id-is-Id : =E2=88=80 {A : Set} {R : A =E2=86=92 A =E2=86=92= Set} =E2=86=92 > (r : {x y : A} =E2=86=92 x =3D=3D y -> R x y) > (s : {x y : A} =E2=86=92 R x y =E2=86=92 x =3D=3D = y) > (comp1 : {x y : A} (c : R x y) =E2=86=92 r (s c) = =3D=3D c) > =E2=86=92 {x y : A} =E2=86=92 IsEquiv {x =3D=3D y}= {R x y} (r {x}{y}) > > it is enough to assert =E2=80=9Cua=E2=80=9D (equivalence to path) and the= =E2=80=9Cbeta=E2=80=9D direction of the full univalence axiom, i.e. the fa= ct that transporting along such a path is the equivalence: > > ua : =E2=88=80 {A B} =E2=86=92 Equiv A B =E2=86=92 A =3D=3D B > ua=CE=B2 : =E2=88=80 {A B} (e : Equiv A B) =E2=86=92 transport (\ X ->= X) (ua e) =3D=3D fst e > > The =E2=80=9Ceta=E2=80=9D direction comes for free by Martin=E2=80=99s ar= gument. You are stating this for the usual inductively defined Martin-Lof identity type =3D=3D, right? Actually I believe it holds with respect to any notion of propositional identity type (by which I mean any model of the Coquand-Danielsson axioms), such as the path types that occur in the CCHM model. Also I think you need to assume the identity types, whatever they are, satisfy function extensionality don't you? > Unless the absence of definitional beta reduction for J somehow gets in t= he way, I don't think it does get in the way. > I think this gives another arugment why the Glue type in the Cohen,Coquan= d,Huber,Mortberg cubical type theory gives full univalence: the only thing = specifc to cubical type theory that you need to check is that ua and ua=CE= =B2 can be derived from Glue, and the rest of the argument can happen in bo= ok HoTT. This is a small simplification/rearrangement of the argument in A= ppendix B of their paper, essentially saying that condition (3) of Lemma 25= can be replaced by the retraction lemma. Yes indeed. This certainly seems a pleasantly minimal condition to have to check for univalence and, as you say, applies to the model of Cohen,Coquand,Huber & Mortberg [CCHM]. (Ian Orton and I are trying to apply it to a different model we are developing.) Andy