From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBC7777WA24CBBUWL5XOQKGQE6CM4HXI@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE,T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-pg1-x53d.google.com (mail-pg1-x53d.google.com [IPv6:2607:f8b0:4864:20::53d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2a0509ba for ; Mon, 8 Oct 2018 14:12:36 +0000 (UTC) Received: by mail-pg1-x53d.google.com with SMTP id s141-v6sf2265954pgs.23 for ; Mon, 08 Oct 2018 07:12:36 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1539007954; cv=pass; d=google.com; s=arc-20160816; b=tV5/zVluJloBfkaYEEMz9pVZhg84my5vTukWJIaPP7oruWoLYP8Z5M18JMkVBd3vMd 2GfU1bZ3gxnBOX1XleSVRiM4dyCd1XQprvBeUBUQ7JZjtWkgXz9UMYPZCd/xD0hLER0y 3IzlNVEeFWlUOdneJYWJr7QbzSj8G0LksQevTgC24IBDL3aDo40pFePzNx6f+2uZEbW0 g/Vwd4w3uI7+bXbkOT9vLzAg2LGD9yCx03u6KFx7wgHCjdfkw8v33zBZzzGMDr9U5bWl Pby6F4/E00gEnsKDbXHJ3gErRblZb1iILQsLtMrMMtgky2YeKIVMy3O4yvP7JSC8drtP eLcQ== 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:mime-version:spamdiagnosticmetadata :spamdiagnosticoutput:content-language:accept-language:message-id :date:thread-index:thread-topic:subject:to:from:ironport-phdr:sender :dkim-signature; bh=H4cGM3Puj6oMKuCKLAIFgqdxhhZOU8B4Op+9WgFfiq4=; b=DjIy6Mv8stPKNJ4zqR4EoHR96Q5aGwVV0oHVf98xbBDhoRhKHasO7RwaaQgOlA5loM 6+FZcKTvW8PqDmvW0VMiQWZsjc7EzqP66e2oDjl772N2ga0dopDH7H7hKGtMK2QfqPOG CkhLVFgPdKXV6xUx8neBKaZews6lftwpXUJfU7AGIeJq0baZnIxRebDALk3KWxyKgtse eU23WGsOJVlnyX3N3959tYqr7IIGcuPbJz/sJyiOcCHb4hW2LucBaqVtKpycvV3tyUlC w3yZN3jtRRUjzyRkZv+oLWmH24Cq1+s8M1fzOGZ6iY+3MWs6YZeFUYMJ/mmqXxQ+M2/+ vHfQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@jhu.edu header.s=jhuiron header.b=RvbggOeJ; dkim=pass header.i=@livejohnshopkins.onmicrosoft.com header.s=selector1-jhu-edu header.b=sT3JGAdQ; spf=pass (google.com: domain of prvs=81287200b=tslil@jhu.edu designates 162.129.199.180 as permitted sender) smtp.mailfrom="prvs=81287200b=tslil@jhu.edu"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=jhu.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:ironport-phdr:from:to:subject:thread-topic:thread-index:date :message-id:accept-language:content-language:spamdiagnosticoutput :spamdiagnosticmetadata:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=H4cGM3Puj6oMKuCKLAIFgqdxhhZOU8B4Op+9WgFfiq4=; b=msN79Co80OU0IqxobW/rpRP7rpgriV7HBXGHOjV7uaOwecs+bhntVWgnWrb+GSrhQE bockDXPeJvuUuZP6uE0NH00ELje+TOI9QEfg81vNm8nE2hKskuMj/HOw8hqf5nNjRsb5 pxFUzsNRxlQNtrcXgsH1w7T5F5/pW4ZoqliT6iLWTUlkEr/xEGq34SlKKLAJMpsM8o0g FMVHmgVTnWA8Bk07Ho1KPnWszgrzr8IKgLI81x6k8zp0jM9z8zOaSYM4/KRO8DvWC5W1 +Mzj1vZiDe8xGpIIrioTCx1Kq7rX8ZklCtYSe1DF+chUZ6kj16Q52enw6j596+G57NXJ gM7Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:ironport-phdr:from:to:subject :thread-topic:thread-index:date:message-id:accept-language :content-language:spamdiagnosticoutput:spamdiagnosticmetadata :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=H4cGM3Puj6oMKuCKLAIFgqdxhhZOU8B4Op+9WgFfiq4=; b=Y2UBwxOTv0LbVg6c3XW6MdjTOGItoIjWh8TRTX0D3v/Dl2gbwmNIfGRdpmDXhuxG9Q Yr993hX4gH1CivkZ8gbWxtVTEnjJ7n/8qTKi4JtsbND8EknYr9Mfcm+3b/JP51Wf+CuM v20sOStB+xBlWiT3gvxEUe9ESmUzACgbkfogB6LV7wfZ+4x87464gfUu3hKfQsda1QzN 7tbCMyLvb709Ut9Pl4jArc47HgpvlT0k9TBLBnJJBoQydyqTL6V8ByDQI3ti748DLuLx Rko2T7syG/77+YWry4FAL7D8frrbOf5NjE3AJYl1uK3zGG0H55wpMOqSFHgpv6Nrxcxr 9sYw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfoiHlfDEZclbjmrDCyMGvAD6J6Ohc6OV2UAIqbHKcUhLJYBrrYd9 trCyq9jTcRGxJKf44P/KvqY= X-Google-Smtp-Source: ACcGV60z9KX2Hdtw0gbWvvBH5ixTGTSO0zTQDJN7cZwc849fkbzMf/0QbXqI3qoNpXeWQNd6Tob5EQ== X-Received: by 2002:a62:f704:: with SMTP id h4-v6mr89357pfi.4.1539007954378; Mon, 08 Oct 2018 07:12:34 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a65:63cd:: with SMTP id n13-v6ls150533pgv.17.gmail; Mon, 08 Oct 2018 07:12:33 -0700 (PDT) X-Received: by 2002:a63:fd0b:: with SMTP id d11-v6mr9109855pgh.38.1539007953730; Mon, 08 Oct 2018 07:12:33 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1539007953; cv=none; d=google.com; s=arc-20160816; b=c2SzEXtH8ntUX169fR0IQKXhI4mUsYW9awUSiHkO2Z2QPetTYHTEGqk5SWOhthVWxs YBlAqM7JCf1s+kB7RiyO2g+9fx4H7SszAiu/yWsOqsdmKAO8pjTTERfZu1J8TvX0F80o EQEnOVRnU/YiLDwYBeu1WhAFVlY4hYa/VFOckwGLYxZZI2LpYCjBcxPLUPxOWJmjLU58 ygqGLq0eK7inzS5/uUXvV7AE7Duim4bJSxpqqR7Dd5PIE4tdDzwk42fv16x3bRwf3dGr /O9SBcTxAAFNfBCLXrNiZAs+04vvLMmxIXk5ypoLOf+FHo9Bvujvuu8P9ySAWFrvqM0O x2Gw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:spamdiagnosticmetadata:spamdiagnosticoutput :content-language:accept-language:message-id:date:thread-index :thread-topic:subject:to:from:dkim-signature:ironport-phdr :dkim-signature; bh=DEmr2Vokx4+HJiMD4uCEH6WM9C2rf0TnJCHUpf/AvlE=; b=pcfN8jdzuhntnoYsRCnWx+6x/jkLs8Rx3WjdOGIDOvTRsCTSlZhRHpuDZMVVA4H+3S EvPn71Ki5STk6WXglZP02dj2cc+pApnf2cOOvO7F1OdEGXJ3RZP1uRhvqBRZkU5B9KhE iPzAJlHzejnZqlYlw14WwVSeV/yqurG/K0am3a9T4qQRxu3yvhJEG2/jTbYTGxmvfM4Q QyjN9NBkBErH5WkvqJI0YzkJxvbZPWZBNzQ6vdwh1xze3824Ib0a208fkx5YBuj59Lax xmEn8Ur1Dae4ej6s5wRatH+W5Ix8D+4uR5VtCcKijMx6NDAIvG8PccOfSbA4R8aj8uRr t55w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@jhu.edu header.s=jhuiron header.b=RvbggOeJ; dkim=pass header.i=@livejohnshopkins.onmicrosoft.com header.s=selector1-jhu-edu header.b=sT3JGAdQ; spf=pass (google.com: domain of prvs=81287200b=tslil@jhu.edu designates 162.129.199.180 as permitted sender) smtp.mailfrom="prvs=81287200b=tslil@jhu.edu"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=jhu.edu Received: from IronEB8.johnshopkins.edu (ironeb8.johnshopkins.edu. [162.129.199.180]) by gmr-mx.google.com with ESMTPS id k8-v6si507352plt.5.2018.10.08.07.12.33 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 08 Oct 2018 07:12:33 -0700 (PDT) Received-SPF: pass (google.com: domain of prvs=81287200b=tslil@jhu.edu designates 162.129.199.180 as permitted sender) client-ip=162.129.199.180; IronPort-PHdr: =?us-ascii?q?9a23=3A/XeHRxxp1RnmvOfXCy+N+z0EezQntrPoPwUc9p?= =?us-ascii?q?sgjfdUf7+++4j5YRCN/u1j2VnOW4iTq+lJjebbqejBYSQB+t7A+GsHbIQKUh?= =?us-ascii?q?YEjcsMmAl1HNWBCEnTLv73KSE2AZcKWQ=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: X-IPAS-Result: X-Amp-Result: SKIPPED(no attachment in message) X-Amp-File-Uploaded: False Received: from esgmwexec3.win.ad.jhu.edu ([10.181.25.233]) by IronEB8.johnshopkins.edu with ESMTP/TLS/AES256-SHA; 08 Oct 2018 10:12:32 -0400 Received: from ESGMTWEX16.win.ad.jhu.edu (10.181.25.246) by ESGMWEXEC3.win.ad.jhu.edu (10.181.25.233) with Microsoft SMTP Server (TLS) id 15.0.1395.4; Mon, 8 Oct 2018 10:12:31 -0400 Received: from NAM03-BY2-obe.outbound.protection.outlook.com (10.173.97.194) by ESGMTWEX16.win.ad.jhu.edu (10.181.25.246) with Microsoft SMTP Server (TLS) id 15.0.1395.4 via Frontend Transport; Mon, 8 Oct 2018 10:12:31 -0400 Received: from BLUPR01MB306.prod.exchangelabs.com (10.242.202.14) by BLUPR01MB1732.prod.exchangelabs.com (10.162.212.150) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384) id 15.20.1207.21; Mon, 8 Oct 2018 14:12:30 +0000 Received: from BLUPR01MB306.prod.exchangelabs.com ([fe80::1d32:5435:f1d7:6df1]) by BLUPR01MB306.prod.exchangelabs.com ([fe80::1d32:5435:f1d7:6df1%18]) with mapi id 15.20.1207.024; Mon, 8 Oct 2018 14:12:29 +0000 From: Tslil Clingman To: "HomotopyTypeTheory@googlegroups.com" Subject: [HoTT] A proof that univalence implies function extensionality Thread-Topic: A proof that univalence implies function extensionality Thread-Index: AQHUXw+abOVrUxnWMECy57DnSApw1w== Date: Mon, 8 Oct 2018 14:12:29 +0000 Message-ID: Accept-Language: en-GB, en-US Content-Language: en-GB X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [128.220.159.4] x-ms-publictraffictype: Email x-microsoft-exchange-diagnostics: 1;BLUPR01MB1732;6:ZbqwAPCHqX3vENCJqhulppAP70yd55gU7mRWIRSFE68rcCgal6EREK09A8y96bo2Qyjfq6jgDfYbpW4zCm5v11SdNa+03/dtHtm+J7N6X+gcJcHoGgkGTsxelogrNjTmCE5OfaAHXrW3h6iwnXeM2yyiuld61O/1cxIC6QZp3v1MopujvJLWkb5qbuCVTHPXOZpR8T9BgjUBu5tHh8akpJNcMRa7gC8lGQUdh3KHDoolg0x3zA07m6ownLMIimbuVrKprWq49Swwc+Gr34PPeQAeJ7OSXXgmZK8ikS1oTh0VSGhJ9XPhFJ0PoFM2ullVqlUp8ByJBuozGSmjnTQonhx4Y9kwcX2FhP4McBY5t3osQFeo+DNHCgDa0YG+tDROaK2yJFcGq6PRcbJf3EXchOf95cuyANSMjGCLjQI2AeSLqK64jPq/ihCKJsZFF3m75m8YBG/QEh212MHrwylrqQ==;5:7TmAiXrm4hfVOT4mOIsfPXTuYMmBgjcAeMJpUwKJfs+zyyWcIT6xz+oFF5GpKk61BYUcK5vV+c90AXc4q9tDEY1EzAQNuR5t99YrwjkB89T55k+GUPMHGMs5gGxdIl+J+f2klen+xa2Z0l41icwLWIJYeYfPmD+dTO9yhvp1Ne8=;7:W3R2hdN4jzHcIfUeBd/LMsOtLeloK9xAsMIDcZSoSVwTwPne8obDprdldH36gtzv3JgS/Kf6JlN1xiDY9o2Ul7q9hXLepTYBmH+YFnZrE9Cv1BC+2zV6zLpK6f63qClZH/V1SQPKtONUwEtiC+AY35qTBjikb+fSEKDFo796kVgEfZ8zPVIySEmekg5KR46X4zsjKNrI/4BhC1at3qeYwzBLkw2HH4Dgy4I08VMbCNXhMXTjof6PAbTbYC+jR4GE x-ms-exchange-antispam-srfa-diagnostics: SOS; x-ms-office365-filtering-correlation-id: e4d4f2f8-445d-4b41-a246-08d62d281550 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600074)(711020)(2017052603328)(7153060)(7193020);SRVR:BLUPR01MB1732; x-ms-traffictypediagnostic: BLUPR01MB1732: x-microsoft-antispam-prvs: x-exchange-antispam-report-test: UriScan:(4782527817362); x-ms-exchange-senderadcheck: 1 x-exchange-antispam-report-cfa-test: BCL:0;PCL:0;RULEID:(8211001083)(6040522)(2401047)(8121501046)(5005006)(3231355)(944501410)(52105095)(3002001)(10201501046)(93006095)(93001095)(149066)(150057)(6041310)(20161123564045)(20161123560045)(20161123562045)(201703131423095)(201702281529075)(201702281528075)(20161123555045)(201703061421075)(20161123558120)(201708071742011)(7699051)(76991055);SRVR:BLUPR01MB1732;BCL:0;PCL:0;RULEID:;SRVR:BLUPR01MB1732; x-forefront-prvs: 081904387B x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(366004)(396003)(39860400002)(136003)(376002)(346002)(189003)(199004)(8936002)(19627405001)(55016002)(86362001)(6606003)(6436002)(81156014)(105586002)(81166006)(106356001)(5640700003)(68736007)(2501003)(33656002)(2351001)(8676002)(2900100001)(476003)(5250100002)(99286004)(6506007)(74316002)(1015004)(53936002)(75432002)(102836004)(486006)(7736002)(316002)(66066001)(236005)(786003)(186003)(88552002)(26005)(606006)(966005)(6916009)(6306002)(54896002)(14454004)(3846002)(6116002)(7696005)(9686003)(508600001)(256004)(71190400001)(2906002)(97736004)(25786009)(5660300001)(71200400001);DIR:OUT;SFP:1102;SCL:1;SRVR:BLUPR01MB1732;H:BLUPR01MB306.prod.exchangelabs.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;MX:1;A:1; x-microsoft-antispam-message-info: slv4+1IhOeKdNIFtf7QOvxVgyMg+otyjI6qdQp0cE7PVx9hcZiytPEhkleOtfs59++y3VnnLGGcqNXUndAKSlbpE7xxJLjt770CmQxQE/Bv/s8AhW6x29Dsd9fqrq0b2wM1fHZixCbanV2x3M2cB3FAu622MCc8XGRhqriu3snZb6TnRHoBIezF/J3Rq6YUeUT5Z29pQK9v8PKHCW5DudRvTfmrfphD5ke2WFB2GiJB2dIPUjomTCSy75KECQPbM8P7zm+Jedp1bC0EQ7SEIjFIWoZLz/uPHhn7Zhpi6h687IngOaYM5eFbBL1DWgi7i20tJn2QGF9FjkIfTkg8QB77+mLVXMOjzdhJudw96UqQ= spamdiagnosticoutput: 1:99 spamdiagnosticmetadata: NSPM Content-Type: multipart/alternative; boundary="_000_BLUPR01MB306371DDFC7A5B774BE88A4B9E60BLUPR01MB306prodex_" MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: e4d4f2f8-445d-4b41-a246-08d62d281550 X-MS-Exchange-CrossTenant-originalarrivaltime: 08 Oct 2018 14:12:29.8114 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 9fa4f438-b1e6-473b-803f-86f8aedf0dec X-MS-Exchange-Transport-CrossTenantHeadersStamped: BLUPR01MB1732 X-OriginatorOrg: jhu.edu X-Original-Sender: tslil@jhu.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@jhu.edu header.s=jhuiron header.b=RvbggOeJ; dkim=pass header.i=@livejohnshopkins.onmicrosoft.com header.s=selector1-jhu-edu header.b=sT3JGAdQ; spf=pass (google.com: domain of prvs=81287200b=tslil@jhu.edu designates 162.129.199.180 as permitted sender) smtp.mailfrom="prvs=81287200b=tslil@jhu.edu"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=jhu.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: , --_000_BLUPR01MB306371DDFC7A5B774BE88A4B9E60BLUPR01MB306prodex_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable All, I hope this email finds you well. I'm writing to you today as i have formal= ised a proof that univalence implies function extensonality and i think thi= s might be of at least positive interest here. This proof is unlike the `st= andard' one, as i discovered afterwards, in that it does not (obviously, an= yway) factor through `weak function extensionality' and instead rather dire= ctly derives a witness for is-equiv(happly). My hope is that, either manife= stly or through the write-up, this also feels like an `obvious' proof of th= e matter. The Agda code and a short write-up can be found here https://gitlab.com/tslil/univalence-to-funext This small exercise arose on my part for two reasons: 1) I was not, at the time, aware of the details of such a proof and a good = way to understand is to try for oneself. 2) I had not ever formalised anything before, and this felt like a foundati= onal enough result that formalisation would be within grasp. I expect that the second reason above readily shows in my code. I had had s= ome difficulty in understanding the structure of the HoTT-Agda library and = so i'm quite certain that i've duplicated work and taken unnecessary detour= s -- i would be very glad to hear feedback about the implementation too! Thanks for your time and consideration, yours &c., tslil --=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. For more options, visit https://groups.google.com/d/optout. --_000_BLUPR01MB306371DDFC7A5B774BE88A4B9E60BLUPR01MB306prodex_ Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

All,


I hope this email finds you well.= I'm writing to you today as i have formalised a proof that univalence impl= ies function extensonality and i think this might be of at least positive i= nterest here. This proof is unlike the `standard' one, as i discovered afterwards, in that it does not (obvio= usly, anyway) factor through `weak function extensionality' and instead rat= her directly derives a witness for is-equiv(happly). My hope is that, eithe= r manifestly or through the write-up, this also feels like an `obvious' proof of the matter.


The Agda code and a short write-u= p can be found here


https://gitlab.com/tslil/univalence-to-funext


This small exercise arose on my p= art for two reasons:


1) I was not, at the time, aware = of the details of such a proof and a good way to understand is to try for o= neself.

2) I had not ever formalised anyt= hing before, and this felt like a foundational enough result that formalisa= tion would be within grasp.


I expect that the second reason a= bove readily shows in my code. I had had some difficulty in understanding t= he structure of the HoTT-Agda library and so i'm quite certain that i've du= plicated work and taken unnecessary detours -- i would be very glad to hear feedback about the implementation = too!


Thanks for your time and consider= ation,

yours &c.,

tslil

--
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 = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
--_000_BLUPR01MB306371DDFC7A5B774BE88A4B9E60BLUPR01MB306prodex_--