From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.106.213 with SMTP id f204mr6798870ywc.56.1476665906297; Sun, 16 Oct 2016 17:58:26 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.40.182 with SMTP id s51ls11909804ota.14.gmail; Sun, 16 Oct 2016 17:58:25 -0700 (PDT) X-Received: by 10.13.233.6 with SMTP id s6mr6815148ywe.63.1476665905761; Sun, 16 Oct 2016 17:58:25 -0700 (PDT) Return-Path: Received: from mail-it0-x236.google.com (mail-it0-x236.google.com. [2607:f8b0:4001:c0b::236]) by gmr-mx.google.com with ESMTPS id n126si395087ita.0.2016.10.16.17.58.25 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 16 Oct 2016 17:58:25 -0700 (PDT) Received-SPF: pass (google.com: domain of jason...@gmail.com designates 2607:f8b0:4001:c0b::236 as permitted sender) client-ip=2607:f8b0:4001:c0b::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of jason...@gmail.com designates 2607:f8b0:4001:c0b::236 as permitted sender) smtp.mailfrom=jason...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-it0-x236.google.com with SMTP id 4so37225914itv.0 for ; Sun, 16 Oct 2016 17:58:25 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:references:in-reply-to:from:date:message-id:subject:to; bh=smfgat+O6I1O5WFsxCpJ1LENK90qBjCc7uZVQVeiteM=; b=uF/RUMWsyIyBcrSXDy29gkWoui06D1Ticq/baeJnVfc3D6oUQci1RBQb9jsrsRermA ABpUxjXEiEuuhLnTD7+QSBTEvfVoXJ5NVvWJx0tTCdV8YoekNuH+AFxAzZN8SHVDdmlK FmQ/oQIOkJNqXK2Of19GdNq8S2k9VWSByuxoaa3Ap4/2SvmHX1YQ7WjaL/SodiBNJlmP TUfjgV8hfG/vNOagEi7KcUqJxhwDfBR1+W3qQ1RZGkv+ZQzkFhAPm/mbfpEAwUeXb7qN SzhvSKBy+eRqphiOjj61q7KzmP7GHER0ZNy1TSfRfx3pOwJdyCtPpCfpZTKIc0YaVYjm Ijiw== X-Gm-Message-State: AA6/9Rn8veaoVWufcUYxCLiapYDuJBanB07nsRiZ62kVYm1je4fC7qRwl89rWkDSfAjYPdyB2R3JD8iyfaR3ag== X-Received: by 10.36.20.9 with SMTP id 9mr7224317itg.24.1476665905434; Sun, 16 Oct 2016 17:58:25 -0700 (PDT) MIME-Version: 1.0 References: <9F0041A0-328D-4C4F-8152-3E42305D372E@cs.cmu.edu> In-Reply-To: From: Jason Gross Date: Mon, 17 Oct 2016 00:58:13 +0000 Message-ID: Subject: Re: [HoTT] weak univalence with "beta" implies full univalence To: Martin Escardo , Homotopy Type Theory Content-Type: multipart/alternative; boundary=001a11446af8bed89c053f05126d --001a11446af8bed89c053f05126d Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable To belatedly add a little bit to this discussion: > so maybe other people have already realized this, but it was surprising to me A way that I've found to make this seem more obvious is that too use the encode-decode method, you provide a proof of "forall x, Contr { y : A & code x y }" (using Coq notation for sigma types). With a bit of rearranging, giving your ua and ua=CE=B2 is the same as giving the data for "forall A (p q : { B : Type & A <~> B }), p =3D q", i.e., giving the hProp obligation for contractibility. There's some Coq code that implements this that I put here: https://github.com/HoTT/HoTT/issues/757#issuecomment-102128029, and in the following discussion, Mike and Vladimir and Steve pointed out that this had been seen before. -Jason On Thu, Sep 15, 2016 at 3:39 PM 'Martin Escardo' via Homotopy Type Theory < HomotopyT...@googlegroups.com> wrote: > Nice, Dan and Anders and Thierry. Martin > > On 15/09/16 18:35, Anders wrote: > > 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_= dan.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/Ibb4= 8LvUMeUJ > > > > > > 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 observati= on 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/HoTT/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 fact 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= argument. > >> > >> 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 > univalence.) > >> > >> Unless the absence of definitional beta reduction for J somehow gets i= n > the way, I think this gives another arugment why the Glue type in the > Cohen,Coquand,Huber,Mortberg cubical type theory gives full univalence: t= he > 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 h= appen > in book HoTT. This is a small simplification/rearrangement of the argume= nt > in Appendix B of their paper, essentially saying that condition (3) of > Lemma 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. > > > > -- > 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. > --001a11446af8bed89c053f05126d Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
To belatedly add a little bit to this discussion:

>=C2=A0so maybe other people= have already realized this, but it was surprising to me

=
A way that I've found to make this seem more obvio= us is that too use the encode-decode method, you provide a proof of "f= orall x, Contr { y : A & code x y }" (using Coq notation for sigma= types).=C2=A0 With a bit of rearranging, giving your ua and=C2=A0ua=CE=B2 = is the same as giving the data for "forall A (p q : { B : Type & A= <~> B }), p =3D q", i.e., giving the hProp obligation for=C2=A0= contractibility.=C2=A0 There's some Coq code that implements this that = I put here:=C2=A0https://github.com/HoTT/HoTT/issues/757#issuecommen= t-102128029, and in the following discussion, Mike and Vladimir and Ste= ve pointed out that this had been seen before.

-Ja= son

On Thu, Sep = 15, 2016 at 3:39 PM 'Martin Escardo' via Homotopy Type Theory <<= a href=3D"mailto:HomotopyT...@googlegroups.com">HomotopyT...@googlegroups.c= om> wrote:
Nice, Dan and And= ers and Thierry. Martin

On 15/09/16 18:35, Anders wrote:
> Hi,
>
> I've formalized this in cubicaltt now, a self-contained formalizat= ion
> can be found here:
>
> https://github.com/mortberg/cubicaltt/blob/master/experiments/u= nivalence_dan.ctt#L123
>
> The proof is a little different from Dan's and follows a sketch th= at I
> got from Thierry:
>
> We have that
>
>=C2=A0 ua + uabeta
>
> implies that Equiv A B is a retract of Path U A B. Hence
>
>=C2=A0 (X:U) x Equiv A X=C2=A0 =C2=A0 is a retract of=C2=A0 =C2=A0 (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<= br class=3D"gmail_msg"> > of the univalence axiom as noted by Mart=C3=ADn:
>
> https://groups.google.com/forum/#!msg/homotopytypetheory/HfCB_b-PNEU/= Ibb48LvUMeUJ
>
>
> One difference with Dan's proof is that this is not using the &quo= t;grad
> lemma" (if f has a quasi-inverse then it is an equivalence (calle= d
> "improve" in Dan's code)). It also shows that not having= the
> computation rule for J definitionally doesn't get in the way, howe= ver
> 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 <d...@cs.cmu.edu> = wrote:
>> Hi,
>>
>> What I=E2=80=99m about to say is a trivial consequence of an obser= vation that Egbert/Martin made a couple of years ago (https://github.com/HoTT/book/issues/718), so maybe other p= eople have already realized this, but it was surprising to me.
>>
>> In particular, based on Martin=E2=80=99s observation https://github.com/HoTT/book/iss= ues/718#issuecomment-65378867
>> that any retraction of an identity type is an equivalence:
>>
>>=C2=A0 =C2=A0 retract-of-Id-is-Id : =E2=88=80 {A : Set} {R : A =E2= =86=92 A =E2=86=92 Set} =E2=86=92
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 (r : {x y : A} =E2=86=92 x =3D=3D y -> R x y)
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 (s : {x y : A} =E2=86=92 R x y =E2=86=92 x =3D=3D y)
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 (comp1 : {x y : A} (c : R x y) =E2=86=92 r (s c) =3D=3D c= )
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 =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 fact that transporting along such a path is the equivalence:
>>
>>=C2=A0 =C2=A0 ua : =E2=88=80 {A B} =E2=86=92 Equiv A B =E2=86=92 A = =3D=3D B
>>=C2=A0 =C2=A0 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 argument.
>>
>> Here is a self-contained Agda file that checks this:
>> https://github.com/dlicata335/hott-agda/blob/master/misc/UAB= etaOnly-SelfContained.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= univalence.)
>>
>> Unless the absence of definitional beta reduction for J somehow ge= ts in the way, I think this gives another arugment why the Glue type in the= Cohen,Coquand,Huber,Mortberg cubical type theory gives full univalence: th= e 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.=C2=A0 This is a small simplification/rearrangement of = the argument in Appendix B of their paper, essentially saying that conditio= n (3) of Lemma 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://group= s.google.com/d/optout.
>

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google= .com/d/optout.
--001a11446af8bed89c053f05126d--