From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.194.119.196 with SMTP id kw4mr1732472wjb.1.1473960922981; Thu, 15 Sep 2016 10:35:22 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.197.136 with SMTP id v130ls382848wmf.14.canary; Thu, 15 Sep 2016 10:35:22 -0700 (PDT) X-Received: by 10.28.0.216 with SMTP id 207mr737054wma.3.1473960922313; Thu, 15 Sep 2016 10:35:22 -0700 (PDT) Return-Path: Received: from mail-lf0-x236.google.com (mail-lf0-x236.google.com. [2a00:1450:4010:c07::236]) by gmr-mx.google.com with ESMTPS id 82si284966wmg.3.2016.09.15.10.35.22 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 15 Sep 2016 10:35:22 -0700 (PDT) Received-SPF: pass (google.com: domain of andersm...@gmail.com designates 2a00:1450:4010:c07::236 as permitted sender) client-ip=2a00:1450:4010:c07::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of andersm...@gmail.com designates 2a00:1450:4010:c07::236 as permitted sender) smtp.mailfrom=andersm...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-lf0-x236.google.com with SMTP id l131so44290699lfl.2 for ; Thu, 15 Sep 2016 10:35:22 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=IMQCVbdWDgFGiZg8fz/j/kcQ3n2ZN/EOa+lENC9UTEA=; b=c4Huj55PX57dT288h4xldIb7iWpjWrcj/lgQFvVijvbzjDsksvQOXcUJ+goZjHovWN sgfj496O2BTyIeh9D/7waSpgcgrZpfkvoFi4jioKMoOm9I+moGE8iH5lJ1rrgA6KeGL+ 4w1EmxMT4G0i2HqFK89t13sOVXcFFongwZm/UOVeu4XuPZM7aCcY+6vb6f8eHYaOP3XA CMcAART6qb26Dh4SU/gTY3D5d3CVj3HFu7r6Foi1I2+NnhN6zQudwF2qecZxu1o04Pef +MnHiAbNsjv98h0XoMsOUX6ikC8nsvTw6kejmrgGtQcgSw9zMNgevE2Zoz5RWGcsDc1O 5+Iw== X-Gm-Message-State: AE9vXwO8wrpuAx0a4RLJESCOfbpTthLQqsCO8LY0N0N4gQARUBBHULnsTZp0eIB8vykyjJMKkjJHd1aeXq7EMw== X-Received: by 10.28.48.71 with SMTP id w68mr4305277wmw.4.1473960919154; Thu, 15 Sep 2016 10:35:19 -0700 (PDT) MIME-Version: 1.0 Received: by 10.80.175.4 with HTTP; Thu, 15 Sep 2016 10:35:18 -0700 (PDT) In-Reply-To: <9F0041A0-328D-4C4F-8152-3E42305D372E@cs.cmu.edu> References: <9F0041A0-328D-4C4F-8152-3E42305D372E@cs.cmu.edu> From: Anders Date: Thu, 15 Sep 2016 13:35:18 -0400 Message-ID: Subject: Re: [HoTT] weak univalence with "beta" implies full univalence To: Dan Licata Cc: Homotopy Type Theory Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Hi, I've formalized this in cubicaltt now, a self-contained formalization can be found here: https://github.com/mortberg/cubicaltt/blob/master/experiments/univalence_da= n.ctt#L123 The proof is a little different from Dan's and follows a sketch that I got from Thierry: We have that ua + uabeta implies that Equiv A B is a retract of Path U A B. Hence (X:U) x Equiv A X is a retract of (X:U) x Path U A X But (X:U) x Path U A X is contractible (contractibility of singletons). So (X:U) x Equiv A X is contractible as it is a retraction of a contractible type. This is an alternative formulation of the univalence axiom as noted by Mart=C3=ADn: https://groups.google.com/forum/#!msg/homotopytypetheory/HfCB_b-PNEU/Ibb48L= vUMeUJ One difference with Dan's proof is that this is not using the "grad lemma" (if f has a quasi-inverse then it is an equivalence (called "improve" in Dan's code)). It also shows that not having the computation rule for J definitionally doesn't get in the way, however having it would have made the proof of uabeta trivial (I now have to do some work by hand as two transports don't disappear). -- Anders On Wed, Sep 7, 2016 at 11:10 AM, Dan Licata wrote: > Hi, > > 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. > > 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. > > Here is a self-contained Agda file that checks this: > https://github.com/dlicata335/hott-agda/blob/master/misc/UABetaOnly-SelfC= ontained.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 univa= lence.) > > Unless the absence of definitional beta reduction for J somehow gets in t= he way, I think this gives another arugment why the Glue type in the Cohen,= Coquand,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 book HoTT. This is a small simplification/rearrangement of the argument= in Appendix B of their paper, essentially saying that condition (3) of Lem= ma 25 can be replaced by the retraction lemma. > > -Dan > > -- > You received this message because you are subscribed to the Google Groups= "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an= email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.