From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,HTML_MESSAGE,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 6619 invoked from network); 8 Feb 2022 23:24:38 -0000 Received: from mail-lj1-x23b.google.com (2a00:1450:4864:20::23b) by inbox.vuxu.org with ESMTPUTF8; 8 Feb 2022 23:24:38 -0000 Received: by mail-lj1-x23b.google.com with SMTP id m13-20020a2e97cd000000b0023e09d49ce4sf272917ljj.6 for ; Tue, 08 Feb 2022 15:24:38 -0800 (PST) ARC-Seal: i=3; a=rsa-sha256; t=1644362677; cv=pass; d=google.com; s=arc-20160816; b=btSn55Lp/CeeSP0lvJO5RPbdDkyOXpYz9P01Em/ImPGwVxZJwUN/E/dnwOQjCYlf1u b+pU8rc/kgT7PLE++KCiOYAIGHef+0taCE/ki3NSRtJdldxzVJmaIxc2j7E6Bez9GbJ4 5XpDMRo7ZhU/psK4ssteZcs0dc7F4skn/6TTG1+Xy5NSiREdXJGRrr3CvjirnK1CAEbE hh/oeR4XhrNbfh7bEEg6zkgz9tCrf0qGmY3ZeP0gHI5K014i0NRg7UTF/AHD/D7/0gK2 dd8RhezaV4IJ8QuxNvnQIoZCxtY8B9kQC5KI6Grk/HyBZfuTsmQHVF+lmhUcwXaCo3uQ SwqA== ARC-Message-Signature: i=3; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:mime-version :suggested_attachment_session_id:content-language:accept-language :in-reply-to:references:message-id:date:thread-index:thread-topic :subject:to:from:sender:dkim-signature; bh=JbwrR5curbcGSgwO3yoau8KwoE+8sB5TwrYmFki8iDM=; b=K8Cfu+1/kgIqbIeANCnpKxqFRY1R59GwPHcx52eAFkgHDEE6oBk8iVuAFlV8eANwhc Qb6DnDoFU8NPS5NV0AmDdPKKhiLUZAD+uQANyma2ksBDIkaA78VXV52LgdsPQi18tGN6 McctHFQ+3KomzgUjxT7L8BT8oYM4AHv8C3bUJniI4Rd5lMlfHcDhMRv/WRFaVsuD43gF 6YIQQqqi9+8tsBmqtckRASkdEKzhRqb4cejxUitcj9U0IWKdLxV3geNIVbEIZc3HDs/H RD6gPxLhBKmCNkIP8SARE+tAutL4pXJJcnisCKobEy9fa4QBBt3hx4vPCtg3PBxLAo1C iEWw== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@UQAM.onmicrosoft.com header.s=selector2-UQAM-onmicrosoft-com header.b=fXld16ji; arc=pass (i=1); spf=pass (google.com: domain of joyal.andre@uqam.ca designates 2a01:111:f400:fe5c::626 as permitted sender) smtp.mailfrom=joyal.andre@uqam.ca DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=sender:from:to:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language :suggested_attachment_session_id:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=JbwrR5curbcGSgwO3yoau8KwoE+8sB5TwrYmFki8iDM=; b=RnDBlbvx1cEvXXMwk4zgKEd6V5bY8Ss3om/0sMeytcVH3IPB6EtFCj1h/6ZixMsk02 vheP3yBqdItHk9JftDfpV5D/zN4NV9qw9xFnhEC0SWGt7G4D7S2bD1Zox58D2PwfdhTx o/X9ZJewB7ZYvIOGJJVNEGj1dzQsADvSGEe23gDVx6m+glS4KxZDUoR+NGM1yMNrhrO9 exXuQsDWaMUAiUu2WHMJEYHoHWNaTOMKT045Z5cyZXcDJx7A6uV0qrjLiftfvYsQ71wU 4Z70gQlpKFaDEEvfBnwFPKxPLwo7f0k1jtPbW2W3imZvHLo4xJlYWlDhM3KPSevyAjid 0bzQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:from:to:subject:thread-topic:thread-index :date:message-id:references:in-reply-to:accept-language :content-language:suggested_attachment_session_id: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-subscribe:list-unsubscribe; bh=JbwrR5curbcGSgwO3yoau8KwoE+8sB5TwrYmFki8iDM=; b=YvqFEFDWORjWwpQHRZeyM5sXfJNr9EkSfcETTeVBrdY6kl55/LDUHuZsPFfRgQzfAe OJaY/rqn2srNPN61RrMJumvYcSa+zP+Kf5lHRLai/SpPJj7uc5NKzNcHzYY0iVS6zMqv DUlJyzGmy5D18bQi+Lpxneiu5itCss9kk8FTkZ/Q+6m7DbcuM1a12JBpDv5BJW45167t 1dVOX1yuO1a6iNwuqGq3FhQWGhS9Ep23O1Ankpz9obweKbzevRp0ZPy/ZrxovW1YNY6R FXTSX0tOjM8FONy0UA3YzSQBHOBgF+sN07iFQN6M8jCSJfdvvwycOQRJZOJWa33MdGn7 Avbw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM531gdEHONv9J6SI2Icjynrbn1MiQAYJPeo/wWkIE/6DPFfvTb4eh AyshXK/e2W4gRMlu/Sd13oc= X-Google-Smtp-Source: ABdhPJwUtVyJ7IGvIh3geNuyedWRmtAAsbO21oiY00Gh3zXnSxvcXoP4jiZ7icYlG8BvCYoD+hBcWg== X-Received: by 2002:a05:651c:503:: with SMTP id o3mr4322590ljp.70.1644362677089; Tue, 08 Feb 2022 15:24:37 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac2:4e11:: with SMTP id e17ls210316lfr.1.gmail; Tue, 08 Feb 2022 15:24:35 -0800 (PST) X-Received: by 2002:a05:6512:3ba0:: with SMTP id g32mr1585296lfv.355.1644362675117; Tue, 08 Feb 2022 15:24:35 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1644362675; cv=pass; d=google.com; s=arc-20160816; b=JUimpF80QIPfqApPnKg06BrMabJfvTz2ytAXlfbxX/j1weqKVY3lCupbRkD2RDstf8 u7Lcwk3DCCUz9UnvyqF9h0dZvGOSOqJ5S0DT37+qJ5sfBJUhUCauNYTTLTQ+RFkHIbY9 /sNOvZ9Dc7ZCtGHm5tDnyv1Z/Nmqkv3X/oB5paNqnb980w8qJWYqoY56wgXbTtjt/NGX ODh6XnsrIreLTdaOFSUo0ifei3eM0YpOgatUJIYVRXT2nsGn1OBBzkReJzonyR7i7RxJ f/lHFRqkCxoQIsnEAnrb/HthhnaBy/d5pBKbMjrAjHRmclmF1UIMJJ4Ps9ZU+JAEsusK nIcQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:suggested_attachment_session_id:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:to:from:dkim-signature; bh=L1QJ/ZOAq07P2UTOgUeN8lCDOKxJWDX/rGZHODFq9Nk=; b=kKimZX5f86UyB0rzH4JXBeI4jf5li+OjDU6QvBMLSKAgCnYX0HOtv2kpoWghP5B/uf IiuBRd12m4uEcehYkRdLouHDkD8Mi8jJODY3n25vOKsCxmftXs8u6vY4EvTGi36CScGn 1MtiQuRsd/XuyZCPYQbnnAi82y0wokbV2/ozqPq7jVgGjnyQRNHQBYWiJ8GGwO9GOOVt bHAQb5da/RVV92JwWJ+dgaYrXsKZvNddKdS3h5xaUKKLtGkrAH5lxVCcGBHngWJSTCxi SFqCsPC26hHecHN+1xznMY2AHl2S77E4ZTz2LDS0JYttldsEpOluvG0lkpGySAxHImOu WufQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@UQAM.onmicrosoft.com header.s=selector2-UQAM-onmicrosoft-com header.b=fXld16ji; arc=pass (i=1); spf=pass (google.com: domain of joyal.andre@uqam.ca designates 2a01:111:f400:fe5c::626 as permitted sender) smtp.mailfrom=joyal.andre@uqam.ca Received: from CAN01-QB1-obe.outbound.protection.outlook.com (mail-qb1can01on0626.outbound.protection.outlook.com. [2a01:111:f400:fe5c::626]) by gmr-mx.google.com with ESMTPS id o24si848839lfb.1.2022.02.08.15.24.34 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Tue, 08 Feb 2022 15:24:34 -0800 (PST) Received-SPF: pass (google.com: domain of joyal.andre@uqam.ca designates 2a01:111:f400:fe5c::626 as permitted sender) client-ip=2a01:111:f400:fe5c::626; ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=m3xFns4lqepr13HRXHb5/b248z9DLHko0OWoMN25vWDpCZOz2oaaSuBy3wRIuidsdcr7IgcAGWcNpUbdVxbzuQXhhiyXF6+ndF29uY84nZ0FJUg6wQjFarbJjdNrquOZdo0yZOAMctq8f9Uea0V8e2RqkO/pnEj0JtZvMqo4Ye/NMWxAgfyTd0skZv22sgnjCX7yAjbuCQ5bDKcC8NQQ2ABLDIAMKLBBJHf2+OArkGoZSvZDoZUUUhAbaIGpfxOl2T71qTeEGmB3zhqXTJBvncBcn5gAILgIs/nEp+LW3gEIcALWt17lGKISm/9uKBAB6gP6ACDWLPH13vEfqsxmiA== 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-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=L1QJ/ZOAq07P2UTOgUeN8lCDOKxJWDX/rGZHODFq9Nk=; b=WKd6DY1VKMTIgxjs013u4A8bL4zhYmhUwAztMe9lxE4v+nj3+q4UDeTl29kclSz7jpySzGACzPL/nIPd2SYEZL2R2S1k3gcA99kCy6ysIcUdbRL0zR0p1SBbH9xYfB1saEwEx6hnP7gEl1Ph0U99nEZuDHKvSMqavqxbLFZfxHqwY+DAxAW7I2raiwVxFanD9SmVonl4ARDvf4H/dR4fkoEZxgroI0yAI5iO5QWNIQ6CMSRZhDIiWMix/uDw5t2fhWSMmF7wvvcKcLMOwxCFbUB7i41SPEL/YOTvUWyaM5NG50sHHwfRnNSuJmPuAFLW5NZwJVIB5UqpAgZ90HdzqA== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=none; dmarc=none; dkim=none; arc=none Received: from QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.COM (2603:10b6:c00:38::33) by YT1PR01MB4486.CANPRD01.PROD.OUTLOOK.COM (2603:10b6:b01:41::17) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.4951.12; Tue, 8 Feb 2022 23:24:32 +0000 Received: from QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.COM ([fe80::b4c8:2681:cf16:e2e6]) by QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.COM ([fe80::b4c8:2681:cf16:e2e6%7]) with mapi id 15.20.4975.011; Tue, 8 Feb 2022 23:24:32 +0000 From: =?utf-8?B?Sm95YWwsIEFuZHLDqQ==?= To: Anders Mortberg , Homotopy Type Theory Subject: =?UTF-8?B?UmU6IFtIb1RUXSBGb3JtYWxpemF0aW9uIG9mIM+A4oKEKFPCsyniiYXihKQvMuKEpCBpbg==?= =?UTF-8?B?IEN1YmljYWwgQWdkYSBjb21wbGV0ZWQ=?= Thread-Topic: =?utf-8?B?W0hvVFRdIEZvcm1hbGl6YXRpb24gb2Ygz4DigoQoU8KzKeKJheKEpC8y4oSk?= =?utf-8?Q?_in_Cubical_Agda_completed?= Thread-Index: AQHYHSlR9RjQV+dUf0KGQyswj7WG1qyKSCuF Date: Tue, 8 Feb 2022 23:24:32 +0000 Message-ID: References: In-Reply-To: Accept-Language: fr-CA, en-US Content-Language: fr-CA X-MS-Has-Attach: X-MS-TNEF-Correlator: suggested_attachment_session_id: 48870002-031c-3fb3-b1db-af2efb2e9a5e x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: a32c65ca-b92f-48b8-9642-08d9eb5a293f x-ms-traffictypediagnostic: YT1PR01MB4486:EE_ x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:10000; x-ms-exchange-senderadcheck: 1 x-ms-exchange-antispam-relay: 0 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: jZBCtzOq7Pw54v3wsgmPYCKYqAYLcQiobuzVXgtN6r0y6LA3RnXXkdE0R1dlT2l7XMcivGlRM92ebvzPzk6V1R9dmCZMWKa9TyKjmfSsluc5sAAkdvDsv285nWWOPPkyOTiCaJJBkhRcegeynFkh/UeWi4yOWAxL9yHdnMqOCM3w7DP/Izmb1xuGfY21c+pG+JIk8AiVn/9lfAHsARrLYDGMcQ4CcOAspSTZuE+Ydyvg86JHeLC4a6kryttbNYRxQlXgewYL5Hzwyb1RMMQJzYIFUnLcetUU4NkC7KUiX0hTgtKYZGbVfsl+tlI1AFZf+Pum1hWE43dm+nG18JqlgOZApSBzJjfHQItvcOzsGhONrlwd5X2uFLctYQKwGOHKIrelA0Qy3Xcqb/xypgydcJdC2yPpkz502lFubXFm6lpz/lej69q9EhwzRfODyJRMhvolcAZITJRIahYSgSYJIbBOC2fqbO6PJpcLNAOrS8+NavA5QH098Ov8YssyUdCmECqIkwhcjx4ux0Dr+QneuswI9ccgVk78B8RPXWG+3WQW51Ua8l8KPOinymJ6LZt6bBWXj2IL81xFVGepoE5wlEL1iX2dcV6P++YLcIytU7zvp7fBQnKmNTqhvZu84eI1fSFUJWOEM46qEmQrjWm8JThJpmUbFW72Uhc91sQ9+dN4kUx4sZNtgZErPIqqUPW8eTjp9glctSw0YTArKjbdosnYwmLifjgYxHpDrE1X5yqroCeODGdhy2xKaBbzvV+4bLqoTCsAHXhstuK+uDtMkktENGtJYoyTp3B6alTuC7PMMqUe7hHhxAnLqjVBPfTqkALTU6pMXPemxEKRBg6IzA== x-forefront-antispam-report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.COM;PTR:;CAT:NONE;SFS:(13230001)(4636009)(366004)(5660300002)(19627405001)(508600001)(66574015)(52536014)(966005)(91956017)(76116006)(66476007)(7696005)(66946007)(38070700005)(66556008)(186003)(2906002)(26005)(83380400001)(8936002)(224303003)(33656002)(122000001)(85182001)(55016003)(66446008)(316002)(38100700002)(166002)(71200400001)(9686003)(86362001)(786003)(110136005)(6506007)(64756008);DIR:OUT;SFP:1101; x-ms-exchange-antispam-messagedata-chunkcount: 1 x-ms-exchange-antispam-messagedata-0: =?utf-8?B?RDkyRllSRVJzZXlMQVNpYk5jZDMycTBRc0xXb3U2MTMwNkJxbjlHdkt3Sm9n?= =?utf-8?B?UVI0NmdsTmlIb2xOT010SlczVEQra3Voa083RjhSVU5GRkl5cGZSSXVlcldX?= =?utf-8?B?cVFrQ1I5R3FMVDl3cDl0L0xTdTVCMFNRRmU1Rk9pMU5qTzQ4YjF6VC82SVdo?= =?utf-8?B?cncySkFlU21aZ2VQSFkyampDTnVWTHVaN1ZJeWNjanY5YTJSUjkwTHdpaEtQ?= =?utf-8?B?VEVEYm9BUEl3YndOQWhTZ013N0gwRVduTlpTdzUyNkZvTWlFL3l5RWtUWUk4?= =?utf-8?B?dVR5WEowMi9OazVkeTZkKzU1S3B4d0lNOTVsNVZVQ3Z0azZaMFZKaGc1b0xS?= =?utf-8?B?a1A2N0V4WlhtalRvYTRmbVFLTFRsRktEUjhkcVRMNjkyMnlPRnhnZ1gwYzcz?= =?utf-8?B?QWx0K2NWdUdrWktXMlREdkpTUmpOeHFhOWNGcWVIZFVlTk53c3dhUGJISmI2?= =?utf-8?B?cWpwdmRNSzhpK0dYQ29UaDVFcDFoem1ka0JCR1YwK1JhUFJWOUFrNVRWNU53?= =?utf-8?B?eHJrMGtnZWxid0dtRCtvaVRBUjlSY3NueWgrelhjSDUvbWVoL2VkS1J3Rmk2?= =?utf-8?B?cHR3K0V1U09WRGd3dm80a2JiRHgvNm85TlBUamxJS0QwbnVIUGV2Rk1nWmpU?= =?utf-8?B?WENjN25HbWVhYisya05PcjVHS0ZxT1BLczZ2T2pKVlVXRWl0TWVSbEVRRUZJ?= =?utf-8?B?cG55UnVVM3dvYWd0RzhveW1pY0RvcTdyUFFGL0R3ZU41TVB6blU3UXgxdHNm?= =?utf-8?B?dXcyOHlqOEhpUTQ1SEFGdWNEeWRNTUlQQ2gwWDRUS3E5RUNHV2t2T2NjelMz?= =?utf-8?B?cDZrRCs5Q2xicUpWMjNBeUpFcVpPUXJacjlkK0RBOFpDWUdWelIwMUZ2Ymxn?= =?utf-8?B?bkZ1NWpteWZkd3U1TzdjM3hkMzZTY1RDbTF3VDdkak4wSE5IY1IvWHRDUndH?= =?utf-8?B?T1NVeGpXa3ZYbTdkc1N4bXo1b2dMTis4eU9Sc3o4R29kcUZoSjhHUm1pUEty?= =?utf-8?B?VGlKd0lFNnUzMjYxTlpHQlptNk8waDR0UElJczRUWDhuWURTRUd5dmF1Zkdu?= =?utf-8?B?eFYrOFFJS21RdGVSWFF0L1BneW80cDJUUzlabnVLNDBmWnZXTFRRVHd1RzVM?= =?utf-8?B?MWR5RmI1QmV0ZlNFbGI0dDl6U3U4U004WUQxeWpzV1pOdWlqK1RXZnkydWs1?= =?utf-8?B?TFZ2cHlrYkROUUJ4VnRCL2V1czRrV1VmNVJWZi9QajJiWEdaMW5JSzUyVzRT?= =?utf-8?B?Mll2Yys3QlIySkU2L1c4T3FoWDNuSFU5SWVZdmozY3RqZUlWTGRkcExtZVJD?= =?utf-8?B?dEQwQVNpY1RnenRneWNXWFRBSnA2Z0l0VHpFQWJRaEt0cmE2NDBEOStFYmdz?= =?utf-8?B?R0h1TzJwVnJJVnhpL0ZIK0RZQ2YrQndOYXE1RmZCNGNCUFVQMVYzYzFOakJL?= =?utf-8?B?MEJHS3ljbzMzRjBnTmNVWVhuaTdoQkRXZmxLUEtVWHB0Ull6V0RyZEVrRTgw?= =?utf-8?B?QU05VGNEeGxQWTFKWlBKbVhiODlSUE9CQWFRdW5WSjN0Tis2OXVZS05mWEFD?= =?utf-8?B?NmJVYTZZM1ZFY2JVYWQ0UzJBcHVvSVdKWjg2ZnVPTG1tbllycm5SRmdoejVL?= =?utf-8?B?U3g4N2dxWnJQb2l5QWI3VTdjQlN2M2RCMllFNzVqQk5oaGZXcnE0WGtkRGlI?= =?utf-8?B?SHlQR21ubkJYamN3S2JTS2xtaFg3a2lHMlRpa0QzQ2U5Vm5Yc3VEK2lIdmFt?= =?utf-8?B?WWlUS3cxVzhkdVJBQmVPZFZHTXdQeUNYczFDL0JSaUFSM0F3cnkzVzZucjVF?= =?utf-8?B?TDlXeVNFWmhEVXJQcWw1Z2Zvbk1qNGhwTzF5NmtJNHcrTU9rcithWGY2U2Z1?= =?utf-8?B?UEpNV21MMUVIMHU1WnpXYmhEVWVvZUo1MjkyV1NJcllQMFN6Rk9jbXlENDNI?= =?utf-8?B?eENKZDErNmJMK0dkTWxVazh3NThRYnQ1VGVkbVFNWmJnb0NaOXA4YzJtMVU5?= =?utf-8?B?dTJXSmdWckI2bjdyYzlvTVVsLzh3WEROTnJOSTJZZnF0SUQrYjFETlVtR3hV?= =?utf-8?B?eEk2ZkpMNGZ3R3MvMG5OTjM3M1dENUg0aEtSWldSN29laERCcXI5VjJzbWNi?= =?utf-8?B?RFNRWlZ5ZVdYSGRIbGl5bXpwWnRMWjgyT3Y3OFcwcTRWYldOQWJqanN3OXFH?= =?utf-8?B?Ymc9PQ==?= Content-Type: multipart/alternative; boundary="_000_QB1PR01MB29481886234F6ECEB3006C31FD2D9QB1PR01MB2948CANP_" MIME-Version: 1.0 X-OriginatorOrg: uqam.ca X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-AuthSource: QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.COM X-MS-Exchange-CrossTenant-Network-Message-Id: a32c65ca-b92f-48b8-9642-08d9eb5a293f X-MS-Exchange-CrossTenant-originalarrivaltime: 08 Feb 2022 23:24:32.0627 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 12cb4e1a-42da-491c-90e1-7a7a9753506f X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: ETSYa3XcbBIMkuskaeRLfjT0jJvQWArePPusphIAWJ6PuUYfr6oD+QhLXuqbvUnxR5Ue8t/a/VySjrQW3lxWwg== X-MS-Exchange-Transport-CrossTenantHeadersStamped: YT1PR01MB4486 X-Original-Sender: joyal.andre@uqam.ca X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@UQAM.onmicrosoft.com header.s=selector2-UQAM-onmicrosoft-com header.b=fXld16ji; arc=pass (i=1); spf=pass (google.com: domain of joyal.andre@uqam.ca designates 2a01:111:f400:fe5c::626 as permitted sender) smtp.mailfrom=joyal.andre@uqam.ca 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: , List-Unsubscribe: , --_000_QB1PR01MB29481886234F6ECEB3006C31FD2D9QB1PR01MB2948CANP_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Dear Anders, Congratulation to you and Axel for doing this! It was a problem for many years! We can now honestly say that cubical Agda is a serious tool in homotopy the= ory! It is an amazing piece of work. Thanks to all, starting with Guillaume. Best wishes, Andre ________________________________ De : homotopytypetheory@googlegroups.com de la part de Anders Mortberg Envoy=C3=A9 : 8 f=C3=A9vrier 2022 15:19 =C3=80 : Homotopy Type Theory Objet : [HoTT] Formalization of =CF=80=E2=82=84(S=C2=B3)=E2=89=85=E2=84=A4/= 2=E2=84=A4 in Cubical Agda completed We are happy to announce that we have finished a formalization of =CF=80= =E2=82=84(S=C2=B3)=E2=89=85=E2=84=A4/2=E2=84=A4 in Cubical Agda. Most of t= he code has been written by my PhD student Axel Ljungstr=C3=B6m and the pro= of largely follows Guillaume Brunerie's PhD thesis. For details and a summa= ry see: https://github.com/agda/cubical/blob/master/Cubical/Homotopy/Group/Pi4S3/Su= mmary.agda The proof involves a lot of synthetic homotopy theory: LES of homotopy grou= ps, Hopf fibration, Freudenthal suspension theorem, Blakers-Massey, Z-cohom= ology (with graded commutative ring structure), Gysin sequence, the Hopf in= variant, Whitehead product... Most of this was written by Axel under my sup= ervision, but some results are due to other contributors to the library, in= particular Lo=C3=AFc Pujet (3x3 lemma for pushouts, total space of Hopf fi= bration), KANG Rongji (Blakers-Massey), Evan Cavallo (Freudenthal and lots = of clever cubical tricks). Our proof also deviates from the one in Guillaume's thesis in two major way= s: 1. We found a direct encode-decode proof of a special case of corollary 3.2= .3 and proposition 3.2.11 which is needed for =CF=80=E2=82=84(S=C2=B3). Thi= s allows us to completely avoid the use of the James construction of Sectio= n 3 in the thesis (shortening the pen-and-paper proof by ~15 pages), but th= e price we pay is a less general final result. 2. With Guillaume we have developed a new approach to Z-cohomology in HoTT,= in particular to the cup product and cohomology ring (see https://drops.da= gstuhl.de/opus/volltexte/2022/15731/). This allows us to give fairly direct= construction of the graded commutative ring H*(X;Z), completely avoiding t= he smash product which has proved very hard to work with formally (and also= informally on pen-and-paper as can be seen by the remark in Guillaume's th= esis on page 90 just above prop. 4.1.2). This simplification allows us to s= kip Section 4 of the thesis as well, shortening the pen-and-paper proof by = another ~15 pages. This then leads to various further simplifications in Se= ction 5 (Cohomology) and 6 (Gysin sequence). With these mathematical simplifications the proof got a lot more formalizat= ion friendly, allowing us to establish an equivalence of groups by a mix of= formal proof and computer computations. In particular, Cubical Agda makes = it possible to discharge several small steps in the proof involving univale= nce and HITs purely by computation. This even reduces some gnarly path alge= bra in the Book HoTT pen-and-paper proof to "refl". Regardless of this, we = have not been able to reduce the whole proof to a computation as originally= conjectured by Guillaume. However, if someone would be able to do this and= compute that the Brunerie number is indeed 2 purely by computer computatio= n there would still be the question what this has to do with =CF=80=E2=82= =84(S=C2=B3). Establishing this connection formally would then most likely = involve formalizing (large) parts of what we have managed to do here. Furth= ermore, having a lot of general theory formalized will enable us to prove m= ore results quite easily which would not be possible from just having a ver= y optimized computation of a specific result. Best regards, Anders and Axel -- 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/CAMWCppmb%2BAt_Bwp_2USKH9dAigFGx0GBrcG3XQQaqZmkr-kHog%40= mail.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/QB1PR01MB29481886234F6ECEB3006C31FD2D9%40QB1PR01MB2948.C= ANPRD01.PROD.OUTLOOK.COM. --_000_QB1PR01MB29481886234F6ECEB3006C31FD2D9QB1PR01MB2948CANP_ Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear Anders,

Congratulation to you and Axel for doing this!
It was a problem for many years!
We can now honestly say that cubical Agda is a serious tool in homotopy the= ory!
It is an amazing piece of work.
Thanks to all, starting with Guillaume.

Best wishes,
Andre

De : homotopytypetheory@goo= glegroups.com <homotopytypetheory@googlegroups.com> de la part de And= ers Mortberg <andersmortberg@gmail.com>
Envoy=C3=A9 : 8 f=C3=A9vrier 2022 15:19
=C3=80 : Homotopy Type Theory <homotopytypetheory@googlegroups.co= m>
Objet : [HoTT] Formalization of =CF=80=E2=82=84(S=C2=B3)=E2=89=85=E2= =84=A4/2=E2=84=A4 in Cubical Agda completed
 
We are happy to announce that we have finished a formaliza= tion of  =CF=80=E2=82=84(S=C2=B3)=E2=89=85=E2=84=A4/2=E2=84=A4  i= n Cubical Agda. Most of the code has been written by my PhD student Axel Lj= ungstr=C3=B6m and the proof largely follows Guillaume Brunerie's PhD thesis= . For details and a summary see:

https://github.com/agda/cubical/bl= ob/master/Cubical/Homotopy/Group/Pi4S3/Summary.agda

The proof involves a lot of synthetic homotopy theory: LES of homotopy= groups, Hopf fibration, Freudenthal suspension theorem, Blakers-Massey, Z-= cohomology (with graded commutative ring structure), Gysin sequence, the Ho= pf invariant, Whitehead product... Most of this was written by Axel under my supervision, but some results ar= e due to other contributors to the library, in particular Lo=C3=AFc Pujet (= 3x3 lemma for pushouts, total space of Hopf fibration), KANG Rongji (Blaker= s-Massey), Evan Cavallo (Freudenthal and lots of clever cubical tricks).

Our proof also deviates from the one in Guillaume's thesis in two majo= r ways:

1. We found a direct encode-decode proof of a special case of corollary 3.2= .3 and proposition 3.2.11 which is needed for =CF=80=E2=82=84(S=C2=B3). Thi= s allows us to completely avoid the use of the James construction of Sectio= n 3 in the thesis (shortening the pen-and-paper proof by ~15 pages), but the price we pay is a less general final result.

2. With Guillaume we have developed a new approach to Z-cohomology in HoTT,= in particular to the cup product and cohomology ring (see https://drops.dagstuhl.de/opus/volltexte/2022/15731/). This all= ows us to give fairly direct construction of the graded commutative ring H*= (X;Z), completely avoiding the smash product which has proved very hard to work with formally (and also informa= lly on pen-and-paper as can be seen by the remark in Guillaume's thesis on = page 90 just above prop. 4.1.2). This simplification allows us to skip Sect= ion 4 of the thesis as well, shortening the pen-and-paper proof by another ~15 pages. This then leads to various f= urther simplifications in Section 5 (Cohomology) and 6 (Gysin sequence).

With these mathematical simplifications the proof got a lot more formalizat= ion friendly, allowing us to establish an equivalence of groups by a mix of= formal proof and computer computations. In particular, Cubical Agda makes = it possible to discharge several small steps in the proof involving univalence and HITs purely by computati= on. This even reduces some gnarly path algebra in the Book HoTT pen-and-pap= er proof to "refl". Regardless of this, we have not been able to = reduce the whole proof to a computation as originally conjectured by Guillaume. However, if someone would be able to = do this and compute that the Brunerie number is indeed 2 purely by computer= computation there would still be the question what this has to do with =CF= =80=E2=82=84(S=C2=B3). Establishing this connection formally would then most likely involve formalizing (large) parts of what = we have managed to do here. Furthermore, having a lot of general theory for= malized will enable us to prove more results quite easily which would not b= e possible from just having a very optimized computation of a specific result.

Best regards,
Anders and Axel

--
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 Homotopy= TypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppmb%2BAt_Bwp_2US= KH9dAigFGx0GBrcG3XQQaqZmkr-kHog%40mail.gmail.com.

--
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/QB1PR01MB29481886234F= 6ECEB3006C31FD2D9%40QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.COM.
--_000_QB1PR01MB29481886234F6ECEB3006C31FD2D9QB1PR01MB2948CANP_--