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.