From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.66.246.197 with SMTP id xy5mr40388154pac.47.1473286839542; Wed, 07 Sep 2016 15:20:39 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.121.132 with SMTP id z126ls5631878itc.5.canary; Wed, 07 Sep 2016 15:20:37 -0700 (PDT) X-Received: by 10.66.12.195 with SMTP id a3mr30192563pac.46.1473286837655; Wed, 07 Sep 2016 15:20:37 -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 w132si2754615ywg.1.2016.09.07.15.20.37 for (version=TLS1 cipher=AES128-SHA bits=128/128); Wed, 07 Sep 2016 15:20:37 -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 u87MKRDY028478 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO); Wed, 7 Sep 2016 18:20:29 -0400 (EDT) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) Subject: Re: [HoTT] weak univalence with "beta" implies full univalence From: Dan Licata In-Reply-To: Date: Wed, 7 Sep 2016 18:20:28 -0400 Cc: Homotopy Type Theory Content-Transfer-Encoding: quoted-printable Message-Id: <227407CD-EB5C-4F5A-8D3E-B49C583D2CFE@cs.cmu.edu> References: <9F0041A0-328D-4C4F-8152-3E42305D372E@cs.cmu.edu> To: Andrew Pitts X-Mailer: Apple Mail (2.3124) X-Scanned-By: mimedefang-cmuscs on 128.2.217.200 Hi Andy, Thanks for the interesting comments! A few replies below. =20 >> In particular, based on Martin=E2=80=99s observation https://github.com/= HoTT/book/issues/718#issuecomment-65378867 >> that any retraction of an identity type is an equivalence: >>=20 >> 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}) >>=20 >> it is enough to assert =E2=80=9Cua=E2=80=9D (equivalence to path) and th= e =E2=80=9Cbeta=E2=80=9D direction of the full univalence axiom, i.e. the f= act 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 >>=20 >> The =E2=80=9Ceta=E2=80=9D direction comes for free by Martin=E2=80=99s a= rgument. >=20 > You are stating this for the usual inductively defined Martin-Lof > identity type =3D=3D, right? =20 Yes.=20 > Also I think you need to assume the identity types, > whatever they are, satisfy function extensionality don't you? I didn=E2=80=99t, but I stated ua=CE=B2 as an equation at function type. I= f it were pointwise, then I would have needed it. For an identity type wit= h definitional J-on-refl reduction, this suffices to get the usual statemen= t of univalence (I updated the file a little to remove a use a funext to ma= ke sure). Maybe this depends on having definitional J-on-refl though. =20 -Dan