From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.237.49.36 with SMTP id 33mr39805843qtg.15.1473261012127; Wed, 07 Sep 2016 08:10:12 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.214.81 with SMTP id o78ls891350itg.22.gmail; Wed, 07 Sep 2016 08:10:06 -0700 (PDT) X-Received: by 10.66.227.167 with SMTP id sb7mr39624652pac.19.1473261006029; Wed, 07 Sep 2016 08:10:06 -0700 (PDT) Return-Path: Received: from smtp01.srv.cs.cmu.edu (smtp01.srv.cs.cmu.edu. [128.2.217.200]) by gmr-mx.google.com with ESMTPS id c75si2158389ywh.0.2016.09.07.08.10.05 for (version=TLS1 cipher=AES128-SHA bits=128/128); Wed, 07 Sep 2016 08:10:05 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of d...@cs.cmu.edu designates 128.2.217.200 as permitted sender) client-ip=128.2.217.200; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of d...@cs.cmu.edu designates 128.2.217.200 as permitted sender) smtp.mailfrom=d...@cs.cmu.edu; dmarc=fail (p=NONE dis=NONE) header.from=cmu.edu Received-SPF: none (cs.cmu.edu: No applicable sender policy available) receiver=smtp01.srv.cs.cmu.edu; identity=mailfrom; envelope-from="d...@cs.cmu.edu"; helo="[192.168.144.101]"; client-ip=73.142.151.116 Received: from [192.168.144.101] (c-73-142-151-116.hsd1.ct.comcast.net [73.142.151.116]) (authenticated bits=0) by smtp01.srv.cs.cmu.edu (8.13.6/8.13.6) with ESMTP id u87FA3A7013871 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Wed, 7 Sep 2016 11:10:04 -0400 (EDT) From: Dan Licata Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Subject: weak univalence with "beta" implies full univalence Message-Id: <9F0041A0-328D-4C4F-8152-3E42305D372E@cs.cmu.edu> Date: Wed, 7 Sep 2016 11:10:03 -0400 To: Homotopy Type Theory Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) X-Mailer: Apple Mail (2.3124) X-Scanned-By: mimedefang-cmuscs on 128.2.217.200 Hi, What I=E2=80=99m about to say is a trivial consequence of an observation th= at Egbert/Martin made a couple of years ago (https://github.com/HoTT/book/i= ssues/718), so maybe other people have already realized this, but it was su= rprising to me. In particular, based on Martin=E2=80=99s observation https://github.com/HoT= T/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 S= et} =E2=86=92=20 (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)=20 =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 fac= t that transporting along such a path is the equivalence:=20 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 argu= ment. =20 Here is a self-contained Agda file that checks this: https://github.com/dlicata335/hott-agda/blob/master/misc/UABetaOnly-SelfCon= tained.agda (Almost all of the file is boilerplate, but I wanted to make sure I wasn=E2= =80=99t accidentally using anything from my library that relies on univalen= ce.)=20 Unless the absence of definitional beta reduction for J somehow gets in the= way, I think this gives another arugment why the Glue type in the Cohen,Co= quand,Huber,Mortberg cubical type theory gives full univalence: the only th= ing 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= book HoTT. This is a small simplification/rearrangement of the argument i= n Appendix B of their paper, essentially saying that condition (3) of Lemma= 25 can be replaced by the retraction lemma. -Dan