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-ed1-x537.google.com (mail-ed1-x537.google.com [IPv6:2a00:1450:4864:20::537]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0d037f82 for ; Wed, 18 Sep 2019 16:15:22 +0000 (UTC) Received: by mail-ed1-x537.google.com with SMTP id s3sf93677edr.15 for ; Wed, 18 Sep 2019 09:15:22 -0700 (PDT) ARC-Seal: i=3; a=rsa-sha256; t=1568823322; cv=pass; d=google.com; s=arc-20160816; b=E9P3mmF32PPdokE34hVNlesJrjQupj4XxqfsDiVxJRyeDghCgtZ1lEGMYd0p4QRxZT zDKh0k/f9wNRAtNFo1NsO+XGZdSlIuSdqG10ZFZdDx7SDFITiKSlTYZILjSGa6bVnbAp OYuIsxaM6GdvYyG5tm/8q6qDW+j2BPeDFOvBzPyc0/7zuG8qWJe++OKcbWYzBTy5d0RO KydfTkJ59gmwmbazHQAO9JMVbMU4LiKbj1UxZ9ucn9uYgaLgfIwhhz3uwYWctC5owpBc Lv/jNK472ppq5vATIra150/D5bCRApCBoxGsZ4qX6pwbcASbTe7HDRyA/jAqe0KAzo+P T62Q== ARC-Message-Signature: i=3; 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:mime-version:content-transfer-encoding :content-id:content-language:accept-language:in-reply-to:references :message-id:date:thread-index:thread-topic:subject:cc:to:from:sender :dkim-signature; bh=Pyt6tuRyXx+E1jiYzK0rXz0+hsryOMu+rhjk+r4wGsY=; b=nZowKSbaRSNeSM6KKntalvO3js3BUqpw0RMxaw/Q5HwS600XGRg8ed4TvPG4/J0/N9 T8qd3qiydW7brBQgb+BcSo6Zq3Q+ERbZYqZYYJdz/n1QSh2DaROytRwbyzY0XEY0Nc5V MK336B0lNsCzDHcJYgZ/IXWUYL5kbzLJP/X8a6WBFKvUqsb0Wo7n7uBVU/pDZHJr+/yv A+dmdYUyjzolwe7U43z1IuerO/4rdNXLv9xXGHrIVyUPAEquXlOA97YSEq2t8swxhzOe DD6rXYkvCxK6rdIEi6lMPy7blRnrPBInahhtPeVS+K8zO37CAwzVqhKc5qFaP6YN8J3x yIdg== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector2 header.b=PUSxE3cd; arc=pass (i=1 spf=pass spfdomain=wesleyan.edu dkim=pass dkdomain=wesleyan.edu dmarc=pass fromdomain=wesleyan.edu); spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.70.121 as permitted sender) smtp.mailfrom=dlicata@wesleyan.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:cc:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language:content-id :content-transfer-encoding:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=Pyt6tuRyXx+E1jiYzK0rXz0+hsryOMu+rhjk+r4wGsY=; b=Feo8eSCYbLGY8rJhCQsZjlkKcESxfl/sEcfIB3JzvngY21PZAhTWVeVgqUXzfMDGO+ AhChpuG+Tf1JUiw7LDIYpuCPiLGpq9mFTYgYT7+wmDpPD/YB3Vlbn1JClcY8+E0wtg0u ztJGg77XCdLuRqvSgabpwiX5upp0WLWhpJstPxtSu77KMFuwP3TUPw3qD4jpfkLjamJM fJnlKi9pgSOAFJZhnneQBcZTOwWcbM3ysUos90Bc/DG9J3ZfVH6/JRy4rFmPmgPW10v6 UdPaahl5ffo/wxFKH/0smfsTovLmZAxjFMW+3J3B5UH5SRgWNh1U/tO9a5guoPH+TcZo XC2g== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:cc:subject:thread-topic :thread-index:date:message-id:references:in-reply-to:accept-language :content-language:content-id:content-transfer-encoding:mime-version :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=Pyt6tuRyXx+E1jiYzK0rXz0+hsryOMu+rhjk+r4wGsY=; b=Cpas7856azH+xWHNwyfGnv1rm9vaOILUnpNUCMZ6WWubG7buGC4Iq7Bbg8bQIMsn/r w0yu4yGzXLw75F6tlPMnWdCRB82Qnike7jJOwFVamMyPkUI/6P8jpJL3o68dvYdh95x3 h3DPHWN4QPvOiG+CpumWiBuAvanOtZthPM8u+oc7/52oCVFUXAqCDM/9kvNYzIxBUw5M 1mXwSSGTjB8lsojedqEGmD4hN5FwiPUNhAqHAqi/due6LKumRx+FDTD3CQJN2w/nu1ON BVSvWvnh8S6hcirABLfB8wEIYb2UXUW+RKx8Ld3c1jaOa/t+JId1t1rl3/G7EWS1t5qq 2ttw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUgv/dBE9K9jUIRlhkmC3JP6Me7LWN7lkChNhXRLvkbd95eaxdj exbEsCRWIx93R1lPWdZNTCU= X-Google-Smtp-Source: APXvYqye/69PXhMyWU3CC5hoPFtEnASt2khEkdCc8cT6rkJm2jNrBLHELtddpX9Qh39sZ+ovV7wbcw== X-Received: by 2002:aa7:df14:: with SMTP id c20mr11304383edy.133.1568823322609; Wed, 18 Sep 2019 09:15:22 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6402:1a24:: with SMTP id be4ls134038edb.1.gmail; Wed, 18 Sep 2019 09:15:22 -0700 (PDT) X-Received: by 2002:a05:6402:290:: with SMTP id l16mr8800195edv.178.1568823322127; Wed, 18 Sep 2019 09:15:22 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1568823322; cv=pass; d=google.com; s=arc-20160816; b=GZFnXFq6XAjbqzpuiowwCuJjqEGSmMoZ8M1nvLRzLRqHd85S24j5fuShTjca3K22nV 0ldzO2POreMyOF4malRl8HMiH9t135ob5w0mz9K/dRgesrNM+OJ1pxtrxsP+M0UvMUlK rOE/u/+eixdQmxxpubZ92/F04ZzRcxCknJL69dITc6dEkKBkNskJWOJto2vN0yL7SCLg n78gW753fJRTKbIatba8o8ETZo87GcysARw8QXhCZB5cCkSlV+XIBEEM4jRFRsCVIQvm rwEW7BplCfMATV4yUculyRQJKKcJL8DyIULqdf7KSiMY8I7LyEsTRZTwp6SNEA6UyQ7W wqmw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-id:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:dkim-signature; bh=iLuzzGQw6TS5C/8HbIUX0eXpiG69h8WZb+17snd2OJE=; b=eDjAOEpAjYg00xJoRGTGBmCzcnoo3Mu8qKe/bB95W4UJZ5DHzSZW+K/qVYtU7sTd5X 7zepKCRj815xDSoLdhpazBZAhMsaAv56f70OgwRa51pMZ0lSv5ZYewIwhgo6RMPGTKLx Z1mHHXbo5G5ileqnmA8ooWzOHFdIj5R/3YsuzUeB5hnfQB8UywPgQyiawnYBHIKXVnJ6 p1RrfqoenzENCTcgZ/hqZDk/OIsZ3MXLnbdNS9PLQuVbgP451mZ78qOALQWO3zVaRyzD Ra8EkId3aDT6YKnQH/TBJNQnFwiXnnDpZGmPp/921KktehTg+HZl47W5OZbNGQHzb2nG Csdg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector2 header.b=PUSxE3cd; arc=pass (i=1 spf=pass spfdomain=wesleyan.edu dkim=pass dkdomain=wesleyan.edu dmarc=pass fromdomain=wesleyan.edu); spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.70.121 as permitted sender) smtp.mailfrom=dlicata@wesleyan.edu Received: from NAM04-SN1-obe.outbound.protection.outlook.com (mail-eopbgr700121.outbound.protection.outlook.com. [40.107.70.121]) by gmr-mx.google.com with ESMTPS id d27si814071ejt.1.2019.09.18.09.15.21 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 18 Sep 2019 09:15:22 -0700 (PDT) Received-SPF: pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.70.121 as permitted sender) client-ip=40.107.70.121; ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=X+31ThfG3CjzuYxWme4ueY35HpLRT/mOPytWnAs6Okq2EApeda/UF6XRg8g2lQTRb5CC5eIFJSnssl8FjdHBQWuRur85rcJb1la2qDpRvcbEJjJ13QCp5b36Hqx6d4RYHG4qMxwtWTAmlnYtGUynxYogL5ePB5RoQPrDOX7I6yW5T1UGpux0Z0mozTTfkji5IIVSKXwrqyITiIhm8Irs6IgbOxFKJypwF/lcgdgzeJTqzWFoT3suikMVHDKoJPBiLjBNA+4mZoYPhkUq5TbvZSqFFMP//z6oE/Pj/HKH4973vM/L1v2CTFYDOm4FAPggTCaxVoWv/DVMoL67wfcN0Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=iLuzzGQw6TS5C/8HbIUX0eXpiG69h8WZb+17snd2OJE=; b=XKjwntynR6cLxYzYMJivGMoIRlFx9okd+hjNf8G1TwoR/NXGUtd+tHQeojT2RNVGgAWxghns0QPSLgM21WejrNISeDwXIMePpAV+29EfTazwgC6tHIdd+z5HYN9R5vNkV3Mp9fRFOL/ZA31A3L2DmOskrkzoh3rHYRRSKq9Z+5Krj5GR+qrKz41IFM53OBCA612cPl7IEBJ/aSVELWNhKarEhh+Iyb5385Z+xijFfqYX+VflWhREART7eIiyVvvgn7mkGZS7GCEurkY+dpX81gvT/PWD+8gdBkAmdYsShEJnE0A1/f1GwoqRqvW2YiQ0aHsOZlwQ8wh/yO43S+PmAQ== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=wesleyan.edu; dmarc=pass action=none header.from=wesleyan.edu; dkim=pass header.d=wesleyan.edu; arc=none Received: from BYAPR04MB4597.namprd04.prod.outlook.com (52.135.237.151) by BYAPR04MB3798.namprd04.prod.outlook.com (52.135.216.33) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2284.18; Wed, 18 Sep 2019 16:15:19 +0000 Received: from BYAPR04MB4597.namprd04.prod.outlook.com ([fe80::a123:d7dd:1dd1:a5d4]) by BYAPR04MB4597.namprd04.prod.outlook.com ([fe80::a123:d7dd:1dd1:a5d4%7]) with mapi id 15.20.2263.023; Wed, 18 Sep 2019 16:15:19 +0000 From: "Licata, Dan" To: Michael Shulman CC: "HomotopyTypeTheory@googlegroups.com" Subject: Re: [HoTT] Recovering an equivalence from univalence in cubical type theory Thread-Topic: [HoTT] Recovering an equivalence from univalence in cubical type theory Thread-Index: AQHVbjfAjEAJhbMjOUCQgzXqM4cD66cxnBeA Date: Wed, 18 Sep 2019 16:15:19 +0000 Message-ID: <1DF8E802-2959-4BEF-A85A-3C6E5E7B9595@wesleyan.edu> References: In-Reply-To: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [24.60.108.192] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: c77db3cd-35b0-4e02-7f72-08d73c536659 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600167)(711020)(4605104)(1401327)(2017052603328)(7193020);SRVR:BYAPR04MB3798; x-ms-traffictypediagnostic: BYAPR04MB3798: x-ms-exchange-purlcount: 1 x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:9508; x-forefront-prvs: 01644DCF4A x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(4636009)(366004)(396003)(39850400004)(346002)(376002)(136003)(189003)(199004)(75432002)(229853002)(11346002)(102836004)(446003)(99286004)(6116002)(4326008)(3846002)(14454004)(8676002)(966005)(186003)(66066001)(8936002)(316002)(66946007)(66476007)(66556008)(64756008)(66446008)(91956017)(76116006)(25786009)(476003)(2616005)(26005)(81166006)(81156014)(486006)(786003)(86362001)(36756003)(88552002)(33656002)(2171002)(6436002)(71190400001)(76176011)(71200400001)(6512007)(2906002)(6916009)(256004)(6306002)(5660300002)(53546011)(6506007)(478600001)(6246003)(7736002)(6486002)(305945005);DIR:OUT;SFP:1102;SCL:1;SRVR:BYAPR04MB3798;H:BYAPR04MB4597.namprd04.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;MX:1;A:1; received-spf: None (protection.outlook.com: wesleyan.edu does not designate permitted sender hosts) x-ms-exchange-senderadcheck: 1 x-microsoft-antispam-message-info: CtcvXlT4+AYqohNjmMJZprDk3VqRswZGHBRM6D7nszqelKdwflYYzZ93p+3mkzIUBa2Q6fKViFBnW2wzYmLz50fYWHDi0qGJx3BtUt3Ak7/E4nXyi51ZDUfh8MIBiiT1obj+JzlyVLvbWcsFLy/M4QUmwbTxkIB0XBokzyF3j51Up+K/Z16HYbaJOHA2zbvf9LFgx8dk3Z32659rZ0CDSfvSrXWz2zNROF6pBLqewGiEYnO6mqyNIgMkEmR+q9akOOPW3Wt7pSIMXmmvG4rr8D9rV8tKVxqrFaBmEuHMHVudWJyR9P4eKDRR4Xr54xcqUpT++xW/3ZCJBUmGWtPW2PoT+4sPN25jSBM0rx3qkijerwev5VPna7F+8vgzyn8d2B+uneX+QUejwUcjDEfTEiBWSSFrOz91heJxp6qL5Nc= x-ms-exchange-transport-forked: True Content-Type: text/plain; charset="UTF-8" Content-ID: <0165EA241FAB9F42AD12819D1DA58D54@namprd04.prod.outlook.com> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-OriginatorOrg: wesleyan.edu X-MS-Exchange-CrossTenant-Network-Message-Id: c77db3cd-35b0-4e02-7f72-08d73c536659 X-MS-Exchange-CrossTenant-originalarrivaltime: 18 Sep 2019 16:15:19.1559 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: a9fd6c79-6d71-49f3-9111-0c8e591dc3d1 X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: maiKU0O/IX+YQTd/IERTGt8VSmLlEwIi0+lTVTkLUlwoLQglUeXwcNQ8oH0jEbxyy0YLvOceoe2YgZ+UzbTttg== X-MS-Exchange-Transport-CrossTenantHeadersStamped: BYAPR04MB3798 X-Original-Sender: dlicata@wesleyan.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector2 header.b=PUSxE3cd; arc=pass (i=1 spf=pass spfdomain=wesleyan.edu dkim=pass dkdomain=wesleyan.edu dmarc=pass fromdomain=wesleyan.edu); spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.70.121 as permitted sender) smtp.mailfrom=dlicata@wesleyan.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: , 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 in = the Glue type that you use to implement ua doesn=E2=80=99t judgementally gi= ve you f; instead there is some morally-the-identity-composition (that wou= ld cancel with regularity) that gets stuck in. This is because the general= algorithm for composition in the glue type has to coerce in the =E2=80=9Cb= ase=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. =20 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 been = explored well enough to say for sure. > On Sep 18, 2019, at 11:42 AM, Michael Shulman wrot= e: >=20 > 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. >=20 > 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.) >=20 > --=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= email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/CAOvivQzzSXNHs%2BzbPQTyHEuU53aHXJ0sPe4pr%2Byf0ahLGvUpV= A%40mail.gmail.com. --=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/1DF8E802-2959-4BEF-A85A-3C6E5E7B9595%40wesleyan.edu.