From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.193.198 with SMTP id r189mr827863wmf.7.1473270652041; Wed, 07 Sep 2016 10:50:52 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.29.133 with SMTP id d127ls2393445wmd.27.canary; Wed, 07 Sep 2016 10:50:50 -0700 (PDT) X-Received: by 10.28.207.131 with SMTP id f125mr1018201wmg.4.1473270650910; Wed, 07 Sep 2016 10:50:50 -0700 (PDT) Return-Path: Received: from mail-lf0-x233.google.com (mail-lf0-x233.google.com. [2a00:1450:4010:c07::233]) by gmr-mx.google.com with ESMTPS id r137si261851wmf.0.2016.09.07.10.50.50 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Sep 2016 10:50:50 -0700 (PDT) Received-SPF: neutral (google.com: 2a00:1450:4010:c07::233 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2a00:1450:4010:c07::233; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2a00:1450:4010:c07::233 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-lf0-x233.google.com with SMTP id u14so4015800lfd.1 for ; Wed, 07 Sep 2016 10:50:50 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=PYFune4ieMwBy6gluWSn+oHhSULN9Q1IAl5FpsUuG0U=; b=DvP+C81j6bL88CygDwdACSkELmbxqbjLJFAEIq24+H23AEQEJn7SkJEzXpMmqnqdqW msKgKDytIahB0rgCA4lcOUWPq2j15Rzx6EaYk1S/HRoevUTtYTsCaqkC+Fzl4VocEiQm p8bUIHUC2FmONg0ALY26nHPepHzCzTPOfgOnSU+9HK2NLacGO5IWmCS7IKY4RVJEt+ub ZD989ujq/L9ycGEuGiIIGJfXe2QwWRqplxYIilsG7Vlqxwv/Kpy+Gc6rMGfISMll8nB7 z3JcreTmnQXHJokhEzrpLjgIQQVnnHTZBjM5j+9bFMish2D9Qv1ikX5uS38A/29rThn2 R8wg== X-Gm-Message-State: AE9vXwN2adWG/OwYPhelKX/IXQkZNqRYCyCAnOlQTysr8Kje2TFHXLVz0DNzCxiN9oTXyZck X-Received: by 10.25.76.198 with SMTP id z189mr305237lfa.74.1473270650269; Wed, 07 Sep 2016 10:50:50 -0700 (PDT) Return-Path: Received: from mail-lf0-f48.google.com (mail-lf0-f48.google.com. [209.85.215.48]) by smtp.gmail.com with ESMTPSA id 73sm3675106ljf.9.2016.09.07.10.50.49 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Sep 2016 10:50:49 -0700 (PDT) Received: by mail-lf0-f48.google.com with SMTP id g62so3969743lfe.3 for ; Wed, 07 Sep 2016 10:50:49 -0700 (PDT) X-Received: by 10.46.32.136 with SMTP id g8mr107359lji.54.1473270649111; Wed, 07 Sep 2016 10:50:49 -0700 (PDT) MIME-Version: 1.0 Received: by 10.25.149.14 with HTTP; Wed, 7 Sep 2016 10:50:28 -0700 (PDT) In-Reply-To: <9F0041A0-328D-4C4F-8152-3E42305D372E@cs.cmu.edu> References: <9F0041A0-328D-4C4F-8152-3E42305D372E@cs.cmu.edu> From: Michael Shulman Date: Wed, 7 Sep 2016 10:50:28 -0700 X-Gmail-Original-Message-ID: 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 I feel like we sort of knew this, but I'm not sure it was written down exactly. Essentially the same argument did come up a couple of years ago in discussing higher inductive-recursive universes: https://homotopytypetheory.org/2014/06/08/hiru-tdd/ On Wed, Sep 7, 2016 at 8: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.