From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-vk1-xa38.google.com (mail-vk1-xa38.google.com [IPv6:2607:f8b0:4864:20::a38]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 546f51ea for ; Wed, 18 Sep 2019 19:23:32 +0000 (UTC) Received: by mail-vk1-xa38.google.com with SMTP id f199sf252567vka.17 for ; Wed, 18 Sep 2019 12:23:32 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1568834611; cv=pass; d=google.com; s=arc-20160816; b=oillJdOgjJqlz/4r/LOA9ie8lll1TJU17omHTHvmvzDglgGYtgssZSzs5tBvZM+MSE 922YOyO++SaPsc3Wx2YAw+jBQZt9o/zpKQNnVCX5STm0HKBWEUJediKRziilkh7RyLB8 fTQ9qkRghuONXAzhh0C0H3nssr8rs3oRiNvW7C448to51rRxgijzZ0wJKHT41KzcnnKU oEX5IEY3gT9lAaxthMrWVmMIh/51YLI7CSWVTi4fV9dufRXjc8ED1e5oAQk6mdO7CKRA Y9ByAP8tOOvtUl8LvUjMJerLk9Uh4n3RozasN+dctwkkaK7UVF0fdxEsXhYmma3S04uO 03lw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=SXavO+j5xbGwVeHwtnqmGqgj7woVfxYbZxng908S2fw=; b=V2nOH/0gOzduU9s7ZMG+lgZf+Mtom5klybWkibF3d3Rki/YnQxcJ+oTUGA4UfBi27c lcoF1tWL7rK9zu7fEQdzEXPjPVAPEkR5H+1bO2kL8s5mFbvaffG7uQqVUUqxOa4bVoNA 0ZbGT+vAJRduCSGPpX7epVF8yIlRrtQvFF2eeJi3m3MvIin8bQk1Z7Sfuu1XMxjkV9FD SMwEZHEzTQwtacEps6Ylja/LDx/yGQMLG8aS9zEmmH9E6kZDNv4KVW5LomG/tV1rNbRl 3pahNiQqATlwH85ck75LdH1DrhokpIq1HVqKRnJ0NxBfXQK6UcdPq0x2CZoB6gA8no44 u2Fg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=kT1LXGWj; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c31 as permitted sender) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=SXavO+j5xbGwVeHwtnqmGqgj7woVfxYbZxng908S2fw=; b=bPg3PELFs0jut/VTA/kVgDezEtE6/uxM8Z5WEs833H97toz2edkUQX8+719tAkuEOY mN97izgyEfW/dxlHtCfLSLzMtAzocmjvfVUDaxd6JpkW5xZMLBsKW2SpE34UT140pl3Z Db0z9+TJtRTkYRvlL+g4jpkCpxPbpP9wAiT6MjoikBkrGhuitUFUOzCoWpldj6BT3XLB sh5V2pBB20ST1QeZpB1XbFG8uaes/+wjWFEKuahDgTbXj54zHQIljkqL6QqogL4Nrbn1 vy+QFIT2symGDd/Nqe00mpUyOVgNhEy6ENU1iWbc8D+BJ3H3KZY/xAjbBKh+5NhKhCQK rTSA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=SXavO+j5xbGwVeHwtnqmGqgj7woVfxYbZxng908S2fw=; b=KqckkWvGnrFZv6hTJF6B9I0heYNQUbSZyyaHKwrAVUfYld2gq8I+fi9+xdWVlEW17H qK0Z3jBM44P3vpPCw6f2BEqvLrnW+naHS1Srlt1YDRspwphfgeBOlf4e4otizD7VmcAK BnKOVqtSfWsGxgWZsNwnfI/ppVqeNDZzX3E9vrONZfv10Lg/JjBjrPlbALlNgnmAqn0Y WJxbYg91eiXvzJ10qKYvzTXW+ShghtaPPUXVKbwiMSD5KGBcQOgv3DQUgXD2T9RfE2cV vUCR4FZ/cyuX/4eEUW4YpTmTVANpb8QhXgACx/rfOf/BF8PLoBiIJLt9UsZOzFs5nkJf qirA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXfTbL7cIVArG8ho87+HAKrbLePm/vIHGa9rU2wmrMXfRw/EE/Y KN7bILM5+Oqih8O0UVP7mLM= X-Google-Smtp-Source: APXvYqy7ao8wdXrthQ7c4plncGOjHyHIqqB3vS9jm4zsfQwCfbMnWj9OWzaUOhRYm6QR4FR2pAlK9Q== X-Received: by 2002:a1f:1897:: with SMTP id 145mr2879717vky.53.1568834611231; Wed, 18 Sep 2019 12:23:31 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9f:2475:: with SMTP id 108ls36394uaq.13.gmail; Wed, 18 Sep 2019 12:23:30 -0700 (PDT) X-Received: by 2002:ab0:5589:: with SMTP id v9mr3452641uaa.3.1568834610820; Wed, 18 Sep 2019 12:23:30 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1568834610; cv=none; d=google.com; s=arc-20160816; b=qwcldwDI5XGE83LmHtBTdbBcuSVjY50zWMeE5GdDU8iPba5agrYuPe5Si9oTrBTA2z cs4dv71Y65L3tOVsCdu6SQPec9HCKf2xOcPwwPhQK139aBPqY2y1M1LHwJJzZORJPqyD iWYyK3rE/OVBd43P0D2/LH2gjpTCINUfA6Gigm/0rNuVY5zryb8XauOyhA2Wllg7i57R 2Gev5hWdLtEU4pmOPfpgw39vVtgNSRnrjupg8nqOWgHou/djmg0BbDabomyoFM9on9tz iXpU5l/Mt4a3EkIAXRvaAPSTnPe2QvA3cAH6YAR9QjT9107zQGdavp8ubjdPmKetMIHw w6+w== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=TPRl0ffQekJ8FMR9E9LA2ii8KPYT6/CM6mKmkC7FgSk=; b=tZ1OgjdDMFkNqX1L/eA9HX149xxTuQRSZ5HpEmKRuEAyHJgu1u+zeHmDCE35WFswSS fDhYYhsZHwuyhNQu0+QlI/O2SUIkoy9By17GbtmmFB9kWGYjb7c2wlxA30lkZmm0CarE jD0Xo62qK/0p3PFt9aW3z25jyRFLHIDLH65deZJF/atv4UwG1W6+CLXYg/iBHPz+EuMj 80OAhbYjV97JAfhdFoK6IktujK6QqnBzJ5IzTcwy03QBN7I9ZLN4/fwrIHQGx+sK1AFS wICSLmgsTGYeiTloELL6X0gTYBLtpp/tW5yymURoRxidv8MWHkPKqKIGbyRunh9Afjvt FAhQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=kT1LXGWj; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c31 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc31.google.com (mail-yw1-xc31.google.com. [2607:f8b0:4864:20::c31]) by gmr-mx.google.com with ESMTPS id a128si747188vkh.1.2019.09.18.12.23.30 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 18 Sep 2019 12:23:30 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c31 as permitted sender) client-ip=2607:f8b0:4864:20::c31; Received: by mail-yw1-xc31.google.com with SMTP id x64so377855ywg.3 for ; Wed, 18 Sep 2019 12:23:30 -0700 (PDT) X-Received: by 2002:a81:a24f:: with SMTP id z15mr4859757ywg.55.1568834610188; Wed, 18 Sep 2019 12:23:30 -0700 (PDT) Received: from mail-yb1-f182.google.com (mail-yb1-f182.google.com. [209.85.219.182]) by smtp.gmail.com with ESMTPSA id v143sm1336586ywa.57.2019.09.18.12.23.29 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 18 Sep 2019 12:23:30 -0700 (PDT) Received: by mail-yb1-f182.google.com with SMTP id z7so439408ybg.0 for ; Wed, 18 Sep 2019 12:23:29 -0700 (PDT) X-Received: by 2002:a25:aa26:: with SMTP id s35mr3733412ybi.223.1568834609089; Wed, 18 Sep 2019 12:23:29 -0700 (PDT) MIME-Version: 1.0 References: <1DF8E802-2959-4BEF-A85A-3C6E5E7B9595@wesleyan.edu> In-Reply-To: <1DF8E802-2959-4BEF-A85A-3C6E5E7B9595@wesleyan.edu> From: Michael Shulman Date: Wed, 18 Sep 2019 12:23:17 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Recovering an equivalence from univalence in cubical type theory To: "Licata, Dan" Cc: "HomotopyTypeTheory@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=kT1LXGWj; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c31 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , Thanks, that's very interesting! The reason I ask is that I was wondering to what extent the type "A=3DB" can be regarded as "a coherent definition of equivalence" alongside half-adjoint equivalences, maps with contractible fibers, etc. Of course in some sense it is (even in Book HoTT), since it's equivalent to Equiv(A,B); but the question is how practical it is -- for instance, is it reasonable when doing synthetic homotopy theory to state all equivalences as equalities? In practice, the way we often construct equivalences is to make them out of a quasi-inverse pair, and all the standard definitions of equivalence have the nice property that they remember the two functions in the quasi-inverse pair judgmentally. My experience with the HoTT/Coq library is that this property is very useful, which is one reason we state equivalences as equivalences rather than making use of univalence to state them as equalities (another reason is that it avoids "univalence-redexes" all over the theory). Half-adjoint equivalences have the additional nice property that they remember one of the homotopies judgmentally, and if you're willing to prove the coherence 2-path by hand then they can be made to remember both of the homotopies; this seems to be much less useful than I thought it would be when we made the choice to use half-adjoint equivalences in the HoTT/Coq library, but it has proven useful at least once. So I was wondering to what extent equality of types in cubical type theory has properties like this. It sounds from what you say like the answer is "not much". This makes the lack of regularity seem like a rather more serious problem than I had previously thought. On Wed, Sep 18, 2019 at 9:15 AM Licata, Dan wrote: > > In ABCFHL, even the function fst(coe(ua(e))) : A -> B is only path-equal = to fst(e) : A -> B. If I recall correctly, the issue is that composition i= n the Glue type that you use to implement ua doesn=E2=80=99t judgementally = give you f; instead there is some morally-the-identity-composition (that w= ould cancel with regularity) that gets stuck in. This is because the gener= al algorithm for composition in the glue type has to coerce in the =E2=80= =9Cbase=E2=80=9D of the glue type (B in Glue [alpha -> T] B), which in the = case of ua(e) =3D Glue [x =3D 0 -> (A,e), x=3D1 -> (B,id)] B is degenerate = in x, but in general might not be. > > I don=E2=80=99t recall any cubical type theories solving this, but I don= =E2=80=99t remember the details of all of the other variations that have be= en explored well enough to say for sure. > > > On Sep 18, 2019, at 11:42 AM, Michael Shulman wr= ote: > > > > Let Equiv(A,B) denote the type of half-adjoint equivalences, so that > > an e:Equiv(A,B) consists of five data: a function A -> B, a function B > > -> A, two homotopies, and a coherence 2-path. Using univalence, we > > can make e into an identification ua(e) : A=3DB, and then back into an > > equivalence coe(ua(e)) : Equiv(A,B), which is typally equal to e. > > > > Now we might wonder whether coe(ua(e)) might be in fact *judgmentally* > > equal to e; or at least whether this might be true of some, if not > > all, of its five components. In Book HoTT this is clearly not the > > case, since univalence is posited as an axiom about which we know > > nothing else. But what about cubical type theories? Can any of the > > components of an equivalence e be recovered, up to judgmental > > equality, from coe(ua(e))? (My guess would be that at least the > > function A -> B, and probably also the function B -> A, can be > > recovered, but perhaps not more.) > > > > -- > > You received this message because you are subscribed to the Google Grou= ps "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, send = an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > > To view this discussion on the web visit https://groups.google.com/d/ms= gid/HomotopyTypeTheory/CAOvivQzzSXNHs%2BzbPQTyHEuU53aHXJ0sPe4pr%2Byf0ahLGvU= pVA%40mail.gmail.com. > > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/1DF8E802-2959-4BEF-A85A-3C6E5E7B9595%40wesleyan.edu. --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAOvivQz_wY2CVp9Y5caEehVotR7w7D%3DoP6jpoUxm463pNdNHuA%40= mail.gmail.com.