From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) 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,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE, URIBL_BLACK autolearn=no autolearn_force=no version=3.4.4 Received: from mail-oa1-x3f.google.com (mail-oa1-x3f.google.com [IPv6:2001:4860:4864:20::3f]) by inbox.vuxu.org (Postfix) with ESMTP id 192E52600E for ; Tue, 25 Jun 2024 08:40:34 +0200 (CEST) Received: by mail-oa1-x3f.google.com with SMTP id 586e51a60fabf-25caef89679sf9338713fac.3 for ; Mon, 24 Jun 2024 23:40:34 -0700 (PDT) ARC-Seal: i=3; a=rsa-sha256; t=1719297633; cv=pass; d=google.com; s=arc-20160816; b=fYLXmAzyrUaJ4Rbk3qaS3jrix+S/Nyt/hcZKBRugggYNctMRRvI8pwlYP3Jlday8Fe tzasiBSATMyMtaXGTHr3yMJkYH9JMWpXZpSZcC5dWTWdIO980gyrcq//ZtQ3X7nhMVZU hv1EJN3ewk+kyRLamxxKJzZ3xz5SxH6aC3iApjk3qYcMF5AhXlgaf6V5rhMSpiwDNVAZ yupAhwC6kVbo/DloLyky2U9tA9BPxpxtusGgqcQekEGcVXnK+lJKU/sapbje0LiYpMwM JF3W7GE3W4t8wv8A7nws+yFMnnophGOZoNb9vhR1w03qDhZ/qWtQSP3E+OJLnErrEDBk MKDA== 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 :msip_labels:content-language:accept-language:message-id:date :thread-index:thread-topic:subject:to:from:sender:dkim-signature; bh=pLdjVBx7FXiQTlOkhQMuGtNJDtB3soR55rgrreQR5HU=; fh=tyfXlvX+ghXq3Ut3t71XgndI++SMq7V61lYsRIrvhXU=; b=Adc/HeBqthrcnHK7DJR6HnCMIWPk1Q+MHtKoCajZITlvpJUYOBsbgUUlYs+jLHFatm J7Li1kztiI9cySvQtRCeYqlbzMVIxHF+ab94UyE/qszUAyjMsk9l9w1auwMhxB6aXnUm qIdaz6Tar0X4/or07Zh8V+2NxuBne4qU6c+hP2aqUL0H+4HjsfQwqG6uHl9C0UQ2lZ2q gCjQkqCv/bw6OvcDOq/kEODF0Tnshzzeo/lWPYWl5iVaKc97B83FgsC4Ta70ADV7Cw62 /3gyMaFewIDpgvjKaDyd8oe117GL7SnBI4drIhIudncu/ZatW5d0g4eB/7YTHGDd5mgq 72sg==; darn=inbox.vuxu.org ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@AnthropLOGIC.onmicrosoft.com header.s=selector1-AnthropLOGIC-onmicrosoft-com header.b=EXkufdrD; arc=pass (i=1 spf=pass spfdomain=anthroplogic.onmicrosoft.com dkim=pass dkdomain=anthroplogic.onmicrosoft.com dmarc=pass fromdomain=anthroplogic.onmicrosoft.com); spf=pass (google.com: domain of admin@anthroplogic.onmicrosoft.com designates 2a01:111:f403:2414::707 as permitted sender) smtp.mailfrom=admin@anthroplogic.onmicrosoft.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20230601; t=1719297633; x=1719902433; darn=inbox.vuxu.org; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:x-original-authentication-results :x-original-sender:mime-version:content-transfer-encoding :msip_labels:content-language:accept-language:message-id:date :thread-index:thread-topic:subject:to:from:sender:from:to:cc:subject :date:message-id:reply-to; bh=pLdjVBx7FXiQTlOkhQMuGtNJDtB3soR55rgrreQR5HU=; b=wW2w3Gx8vMfO9Znpqjcdygsa7T6aMFNzt53i5dzhhF8Fv+MDJbuY9pWZUiQ4gAasSI ZqmQt7jHahozc/TCLK6mEqZM61QmnRZ7iEa5wkQBAu2vc/qiEjy2cc1srE0N05kYrV9d UmwkjcMk6ZdLSTlpsn3Y9kwC4qwGPWSOOkYadqZqE8GiyBv23bsr9In6ueNhErUN8jVe hwTuFKu/RjiFv7jnlt4pWWsvGFb3bCkd5twy02Ml7rVUU88r8yYJCzX833al+PjPQo49 2EkaWwQ8Fa/HHSoTGA77v4eoZU5JevqKYi4qhXj3odHjTV73vnoT4RTZe2ARjwomBfDC 6v2A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1719297633; x=1719902433; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:x-original-authentication-results :x-original-sender:mime-version:content-transfer-encoding :msip_labels:content-language:accept-language:message-id:date :thread-index:thread-topic:subject:to:from:x-beenthere :x-gm-message-state:sender:from:to:cc:subject:date:message-id :reply-to; bh=pLdjVBx7FXiQTlOkhQMuGtNJDtB3soR55rgrreQR5HU=; b=KjHPlzeuYeGKWhVFeEb3YrV3mWv5gijX6yu+OEgentCiI0JXrPIqd8VYqnJLrqhUI6 whOqGxw6sXt8PfARKIqfo3g6w+t35xguiANGqwRivKCvUd3qJFx8ZQvbsFSojqIieXaA lMB559TXysUwmQSM5kUUKb23YvhEeTDdmsGwNEQ2y4AnOXWkXpj73azuohC9GlSJ4uQk /oCooKZKgfzQIEc2Iv+1UeFwLkdaIAsVHDEDDQv3XJBzXrcwm7VsZ3GOJynR6KmWFR3Q 1gwIp+HG7bwi6OHAlDB+o0wt+YaK9/64lyb+S+IzYebdMr20Imlm8Bm1CTqCaZZtkQoX +gTQ== Sender: homotopytypetheory@googlegroups.com X-Forwarded-Encrypted: i=3; AJvYcCVag/HSgKfIcMc1wl8uJhS8vNiVALJff2DqHRAK1ETD6DHYYPUjJVb0pbPl5OgMk7FXdfAhHeeQnpgSqzIRpiJg+Q== X-Gm-Message-State: AOJu0YzMtWlvw3OBqsvth3GVK8/3/IOnxsBR5/d+Gyl5VeMy1WnjNw4C nSl8lDsblDmv+kA6XbVMkjNLqCwwctDp0s5s9ni+LtzpQpKb77js X-Google-Smtp-Source: AGHT+IGuYeClIdboAQ+Jq+PhHxZLrVDNkzFCelcuXra05q0kaM8UfGb/Xa1n+FxTQqCZJ5B//xQbQw== X-Received: by 2002:a05:6871:5210:b0:250:7465:d221 with SMTP id 586e51a60fabf-25d06cdac07mr7138450fac.28.1719297633173; Mon, 24 Jun 2024 23:40:33 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6870:280d:b0:259:8ac8:a82b with SMTP id 586e51a60fabf-25cb5f24b5fls2621874fac.2.-pod-prod-07-us; Mon, 24 Jun 2024 23:40:32 -0700 (PDT) X-Forwarded-Encrypted: i=3; AJvYcCVeXGs4C2lhtpn4FQxFcJS46/EoTQSB/ksA/HR0Lpc43D2dN/sKseu0Ws4MUBP1HR+RHudEHtCMjxQj2j2tYPtCLhXhSFQJX6hiK4XeVjK5kWHIbQ== X-Received: by 2002:a05:6870:9216:b0:25d:b48:3651 with SMTP id 586e51a60fabf-25d0b489811mr899723fac.3.1719297631942; Mon, 24 Jun 2024 23:40:31 -0700 (PDT) Received: by 2002:a05:6808:1b23:b0:3d5:1c66:dfa4 with SMTP id 5614622812f47-3d53c32e780msb6e; Mon, 24 Jun 2024 18:37:16 -0700 (PDT) X-Forwarded-Encrypted: i=3; AJvYcCXDWho6sSsmkpwY5lP9yFuJtFEfRFKNXB98TUJXX1yFxaaZNcVABBmHeGrjWEYstCfiV7PgLS8u5r7l2Ux2P5zgbBO3EsOPfBU6w2ZCVd4HSDnHyA== X-Received: by 2002:a05:6602:3424:b0:7eb:caf2:98d5 with SMTP id ca18e2360f4ac-7f3a759275dmr892753439f.1.1719279435606; Mon, 24 Jun 2024 18:37:15 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1719279435; cv=pass; d=google.com; s=arc-20160816; b=lvcng9oJm5xLaMrLieRVseUQySuW8mqMwrqIgjQT7vbIATNUSp+aW6SFaL4HsbIUVp kmFUWVLGoBb5K5Kh6xEh2R8EghVAxZvLZ58hC2nXTqsTQ+6lWIeVRaaDE4MQfZ6B9ICv tsjiB6I4+VnagmGGPhJNFvucd27TutL3q7/rPYbkQg0Afvly952SvHwje974Nv1T7UbB inwdFgBFNnDvMhxx4363Jqhr/ZPUgQwKaTQYXnwY1L/AKeFqAzZrZUSvrzNgGVIFpGZs pKtBwajdHyc2ifSJD2Y5sdTcBVqH9AAyAWTZnLYeZsByhpnP0Fsrgul1lR53mvrJcbha Hwpw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:msip_labels:content-language :accept-language:message-id:date:thread-index:thread-topic:subject :to:from:dkim-signature; bh=ilxTjv1+Rk58M8w9ighVifEDk9h978xkiETi6ie72z8=; fh=h9bkAdw4gphqg3y5ZJTak3WBdYS20FzrMlQqjwn79Y4=; b=VjqPa3w53DC5IkNXGytJnU2r0nK6SZAeTM/TIwSraxURjIpBTdeY6TrEHSPneti9B1 CjsRiQo2uZ9WhVuifek2Ef+XWhm2KadzuS52ekIFsk4q25XMwrukr49PU0dWFWooa+1/ 8P9ezPYGA1IcuHy5aQXgt1Lgkc2SiS1YZSIv9VPADow1vlz/T3KW0+TlXvws1izXE/78 mUEYp/DTqisP5etaQrfAwHsMiUscS+DBn8rx6Zy3z555U/x9FHwc/QsBgGlRWl3grluI flWgafbqdikHOfJJkUK0wgivU2VewTTRT6URpPqG8evUsV+VDv9SSCsB1N2CHIqRGcmP 8TCA==; dara=google.com ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@AnthropLOGIC.onmicrosoft.com header.s=selector1-AnthropLOGIC-onmicrosoft-com header.b=EXkufdrD; arc=pass (i=1 spf=pass spfdomain=anthroplogic.onmicrosoft.com dkim=pass dkdomain=anthroplogic.onmicrosoft.com dmarc=pass fromdomain=anthroplogic.onmicrosoft.com); spf=pass (google.com: domain of admin@anthroplogic.onmicrosoft.com designates 2a01:111:f403:2414::707 as permitted sender) smtp.mailfrom=admin@anthroplogic.onmicrosoft.com Received: from NAM11-BN8-obe.outbound.protection.outlook.com (mail-bn8nam11on20707.outbound.protection.outlook.com. [2a01:111:f403:2414::707]) by gmr-mx.google.com with ESMTPS id 8926c6da1cb9f-4b9f98e81f4si149068173.7.2024.06.24.18.37.15 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 24 Jun 2024 18:37:15 -0700 (PDT) Received-SPF: pass (google.com: domain of admin@anthroplogic.onmicrosoft.com designates 2a01:111:f403:2414::707 as permitted sender) client-ip=2a01:111:f403:2414::707; ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=Xs7cYvmOIRqi3rC7e1YgarFS1XosWsi2KrvquUDrVvuGIxnop66obW1kjoeAnp+hudzb1ViFP5jCEyaG/1DLgPiqRiQ3Z0/zPbZw61qO4x08SadoxmYOIc4yHSPHQNg7/svXq7L0aNAlocZsfnhjX1huA3z2+OGRtWpQ+9DkvYptCSCbXup5qIyNj47w8VziwplosbYO+C8JUlcpn5GpYaJIEk1tcC7FbZWjVSqdllHQ87BinkiT8iPWHMyC8fPStw9a6XTF85bDLoEQukVANkjwGNnDgellUzhAOxaseA+zfbpLhjrypXmJ8s+kN/SjoqB59b6AAS2Kq/YlxoVezQ== 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=ilxTjv1+Rk58M8w9ighVifEDk9h978xkiETi6ie72z8=; b=eNtWBWRyXp8Jf9bV0Lhz+Tz/5HUNn3BNcNd+fNvNRdbvPyaqKFtqOaqXgcYQlau2IAJb4uD3buXLPwZG9RoQFzKaRLkeur8vkMFhPJJNdFko30Ds2bHIAQKzuHEd82cNfscM1y3vTIaX4DarEU9U2zWCpPM0+iazCRbn1nYgK064WN6QiMcJ+5Wg+mvZ4JdkuNjH1wuiSXyi08ig8u29H4Y55zKyuF5sjd2U7V+Taj0xTb7Prv4SmhHfgsMcKNKuynPgOti9rRDqTZX7huU844YyCvQbMP4e0htDrn/NKBw9VeyvZ0t+hOjg+qUj7iDw11mmBPJklRLDdeKNOUy1Tw== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anthroplogic.onmicrosoft.com; dmarc=pass action=none header.from=anthroplogic.onmicrosoft.com; dkim=pass header.d=anthroplogic.onmicrosoft.com; arc=none Received: from DS0PR20MB6232.namprd20.prod.outlook.com (2603:10b6:8:f1::19) by SA1PR20MB7190.namprd20.prod.outlook.com (2603:10b6:806:3ec::18) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.7677.31; Tue, 25 Jun 2024 01:37:11 +0000 Received: from DS0PR20MB6232.namprd20.prod.outlook.com ([fe80::74c:42bb:ef9e:fbaa]) by DS0PR20MB6232.namprd20.prod.outlook.com ([fe80::74c:42bb:ef9e:fbaa%3]) with mapi id 15.20.7698.025; Tue, 25 Jun 2024 01:37:10 +0000 From: admin To: Cyril Cohen , "fom@lists.ugent.be" , "coq-club@inria.fr" Subject: =?UTF-8?Q?=5BHoTT=5D_Re=3A_new_arxiv_calendar_overlay_=E2=80=94_=5BCoq=2DClub=5D?= =?UTF-8?Q?_Postdoc_Machine_Learning?= Thread-Topic: =?utf-8?B?bmV3IGFyeGl2IGNhbGVuZGFyIG92ZXJsYXkg4oCUIFtDb3EtQ2x1Yl0gUG9z?= =?utf-8?Q?tdoc_Machine_Learning?= Thread-Index: AQHaxpAa8x7eVRIrUE6hNtOMJ1hxaw== Date: Tue, 25 Jun 2024 01:37:00 +0000 Message-ID: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: msip_labels: x-ms-publictraffictype: Email x-ms-traffictypediagnostic: DS0PR20MB6232:EE_|SA1PR20MB7190:EE_ x-ms-office365-filtering-correlation-id: 2e3d2400-2a95-4730-02e1-08dc94b754e8 x-ms-exchange-senderadcheck: 1 x-ms-exchange-antispam-relay: 0 x-microsoft-antispam: BCL:0;ARA:13230037|7416011|1800799021|376011|366013|38070700015; x-microsoft-antispam-message-info: =?utf-8?B?dTJvNEpVSkZ3T1VQQ0wwVzhGaWtZdkdLK3B1Sm9ob3h0WGtjZUlldEVjMG5G?= =?utf-8?B?NE1FZU5KZmgzamR3M3VQTStjakZWbWU5d0Q3T2xvYUF5S3pRWFhxMlRxM2to?= =?utf-8?B?U1hLQ1c4SXRhR1pjeU9sWEFoNjMvRUI2ck52dXRjUEpmZWFyVWhnUW1YU0hC?= =?utf-8?B?bEV4eS8zV1VVTjN3UDlXa3k3QlE1UTc4U2l1cVNCR2E0WkdSVmxCZ3NONGFM?= =?utf-8?B?Y3cxdlZWM25NS1hpNVVCTVNIRDB0NGpXRG5BWE1UeldPbjMyS3VkMEtWUFRw?= =?utf-8?B?L2x2SEoxYmd1MjlHajBETjRHckdrUEhlRjZyTUxiQklaMGJuUk8wSVpINDNR?= =?utf-8?B?K0dUSDYxRGdMQklJR1dweUpwUFI3WTMvNW9OZkp3UUtXd2pIdTJucGgyWXFx?= =?utf-8?B?WHBlVktjT3BRYkc3dnk4VWtmZW10R3k0c1dzNmZHbVR6S0lybmVsNmNuTjJi?= =?utf-8?B?d2JCeS9aeUhBa1g4cDlKSTR2eWV6ZjBOcGxhU3Y3NlZkeVYrYkJ3WmNQY0Zz?= =?utf-8?B?elJpVDBDdVBIRlg3Wk9nenNkalBJNGY3N3RqeEkvRkpvYmhPOG9SV0hXQlhI?= =?utf-8?B?WWlJWmpIcjlTbHYzak1SWHhDUW1uVmNSN1JFalE2cEF2YjI0N2Q2V3FJWWlM?= =?utf-8?B?VkVmZDRyNTNzZ2FYTnlkL3lhQnFZZVJUZ3YyRHZsUGNLV3dGWjFFRk5NNm5k?= =?utf-8?B?dWF4K3lwbFpyUmFNUVJEVk1TNVlRcDR1R0J6aHFocjJINkh6WHZ4VEltRjYv?= =?utf-8?B?WDJuRzQ5NHFacG1abml3R1hGWTdLL0NMVTQxUmlSQzNjTkRON3JqYzgrYzRl?= =?utf-8?B?WWJPUTd0MFA0ZFhuRzJrWmh6WXoyd0dvbDlCU2tVd2NldVBVMmQxdjJKQXFt?= =?utf-8?B?aXNqK3JOc1p4ckxPOHY2Uk91dndwc3phNHBLTXd2U24xNjJ6d1RPdDl1ZGkv?= =?utf-8?B?akxUbGZwZTF1TDQ2cWFzdTZTcHR2TEVKUU45bzNNSXNVK2dUV21KS1ZlNjEv?= =?utf-8?B?OWlJTmx6aHR6VDJJdW1aQ1N4eGN6dXdUR1IrT25rVjducXEwUzdFdnpJdjNO?= =?utf-8?B?MG5MUTVxTmZBM2pyTzNNTWRsZ1BQME5YeG5BNlRXVndXc1RCalR3MTJUK0RD?= =?utf-8?B?Um55QUJWZmhqMUdtTWgxYmI5RkRVcWprelhPRmJrWkM4TkVueEw4Lzg4THJa?= =?utf-8?B?QmI3OUIxOTVJZnRBdXI3biticDBtUlVkcEp4MHBHZDZWKzRlTXZBV2FrZEZC?= =?utf-8?B?NmtzSnVxVUV1cUNERlR1Y0JvMWNDZ3VLdHBod3l3WXlhYlVRM0dKY243cGpa?= =?utf-8?B?WFA4Vld4ZHRoRDA2KzhxTzVXYktBS3N3b3RzdE4xb2tqZnQxalI5TEpnN1c5?= =?utf-8?B?N0prRXpOV2YwK3Y2Y0lweWgzZXRWS09RdDMrREk1MDE5UzFsK3FxV3FoeXVx?= =?utf-8?B?MHJVRmg0anBUVjRaU2tlWHdaZWRHYm5xL2VRTisxZ3VmL0I3NkFuSGtqVGo3?= =?utf-8?B?eHBSalhmL0pyakJRbkJOczFWRnJmTyszZmFMWTBFNklWaFRqdWNmYmppMDZy?= =?utf-8?B?SFl4QXluVE5KZG0yZ2t0d21SM1ZvQUQwbGlXanM5WFdrL3lQWUlkMzh0K2ow?= =?utf-8?B?THBJS3RJN3ZZL2o5UFJCcmxWTWl0QzRzRVZRS0ljOFVOUWswbSt3RE16OFV4?= =?utf-8?B?dEVzd1RNaGh6akplS0dLbmpqd0xhU0pqWnd5d2xmSUYvYytVQzJ2dGxuVXNU?= =?utf-8?Q?ek2dOgeBiPvg6mbppLv6gLFBaTNbwYWAjBZWXNB?= x-forefront-antispam-report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:DS0PR20MB6232.namprd20.prod.outlook.com;PTR:;CAT:NONE;SFS:(13230037)(7416011)(1800799021)(376011)(366013)(38070700015);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata-chunkcount: 1 x-ms-exchange-antispam-messagedata-0: =?utf-8?B?ajE3OWM1RkltY1VrbTdOa1AxQ1ZERHFVUXM5Zzd5YzdyK1RwaWhRSk1wMG5L?= =?utf-8?B?d29sZnBZdHU4dVNncFZBQXdHV2JaQkJBWEVucVBXVm0zT0RsM0JYd20vWFdr?= =?utf-8?B?MGVkdFJxYWpncTFTSlc4dkxURy9BMkNOS255UHljdGtpOEF6NFpuM09TVTc1?= =?utf-8?B?NktBY0UyQmY5SWtzRGhBZ2psOFhnR3IyZzVTRlRqU3RwdFpIU2hZUWRhdFZs?= =?utf-8?B?OGlad1FTMHZiZkdpaE15Rm1ibWoyaGNUejNPVGJRZ2lrMmtqK3RpY0YvTzVS?= =?utf-8?B?c0pKazRhblcwNkF1czdIUDV2d2NaTnJKVlpZaFN6eEUxTDZVYmMyTHMwbXd2?= =?utf-8?B?SXFnaFRQL2kwRzJMVmQ0M3p3K29HZE5Eb01Ha2RWK1lQcDc0RW9LVXBjRUoz?= =?utf-8?B?bWMxT2VYK2k5TERmZlF0ZWFjaUJ6ajlXdnB2SEl1Ky9UQUgvSVJRcjZyZGYr?= =?utf-8?B?bUUvR3RmdmtZeFlManFGUlhCd2FlUzJCZHBwQXF1VnJPd0dkcGFNaXk5cVlP?= =?utf-8?B?TUREZXVsbURkVTZ3Q0M2U1kwR1V1RVNXVTU0V0JDc1J0cE94NDcrNEdjSHJz?= =?utf-8?B?RUo4VE5seHV6eDhid3ZpSEpuUnJMN2Mza2lSTXl5SUhyM1FnM0RqMzdWL3hY?= =?utf-8?B?NXlQWGo0MTJuOXFZSnJsM0lNQllvMU01WUh0MWdZVGRweXAvNS83cWlwMld0?= =?utf-8?B?VzduTzhheENOSXJaZEFUVW1PVlVIOVlMVzVoSWhyTkRodmxFdlB4eVBGais5?= =?utf-8?B?WGFWMmgrSDl0UXJaWkYvbi9Rc1drQUtYNjJ5SmZmU3owekV2dEZoa3BKcTRR?= =?utf-8?B?a1pVN3NadEJBNzhsa2tYQTRmdXBSRUs4RFBXME9XN0ZvaExidk9YT1JkbGFP?= =?utf-8?B?VEFUd2k2RXdLSG1VWGJ6S2VlQ0RJV2RZM1Nqc3oyV2ZQK2dhV2swdjU0Z1di?= =?utf-8?B?emxjak1zaWxGMGJDclowWnUyc2JJMUxTbU00T3dNdVFoTjJtMzB2ZUppOG5y?= =?utf-8?B?V2JPdUhSVm1NMk4zOHNvRFE0OTlvZnZqQkxwb3FGdDJvcUU3Vkt5a1NLT3ZB?= =?utf-8?B?YlIxdnA5bUdUT01DS3pPSU1IblNmQlBXVEZqeWhNeUhiM1drQXR5ZGgvOTNK?= =?utf-8?B?NVVQczFvK2dRMi9GL0pDbEFvOFJyUEJoemV2VG5HNWxhczZjdlI5RVIyMmNy?= =?utf-8?B?cEdraWNmR1FkZE14R3FBL2FTSzNMRjcvektCLzBKYTluQjJVaG9xY0VKdldz?= =?utf-8?B?UFhSV2lKVUVjclVaRXpBUHNTa0EzamtqcUM0aGFZRDJZeVJKNFE1ZEsxT1VB?= =?utf-8?B?cjNPNk5uMysyb3l0c1BKYzJWVXJwVlNrbGdhOWdjclJ4Y0ZOUU9TbGRnamFr?= =?utf-8?B?eElpVlVIZm02YzVHamFSYnc4eitJQWtWMHg3MzNHR1pqTWJIS0g4K3lBRklD?= =?utf-8?B?WGJVYjBuSmRSWkxUNWlNdWVOSHFwR2xnWU4zc2dqZ2hQME8yMmp3Qk5HSVY4?= =?utf-8?B?UG1uTDJBbnhOakVLYWV6YVF6bjJIWVA5VDdUZ3l0Z2FNZDdZNmRGblkzWktq?= =?utf-8?B?UkQwd0NXdXdiZmtYRWhWSkpyRWFHdXpaZlZOM1QvY2hrL29UaHpSK0Q2MzBX?= =?utf-8?B?ZDhQRGdQTmZSRVFNTk5zRFluTkFKZi9xQnZRamNhWnlmQUtSZnJwT255MFpl?= =?utf-8?B?RitqM2pscEs3K2VjM000VXBnN3NUNHlxL3BsWGxURWxrQ012YW5YMjMxeU1G?= =?utf-8?B?ZjBmL0ZFcU9BbmtTU3NZcW4rWGVEMDV0RWU0ZENSZ25Gbjk4V1o1NTVVSkJB?= =?utf-8?B?RUh5SCt4TjdjT2dQY0NoekJGaEhpUUJBb1R5SVhVbk1WVnl3U21KZHdXcm9l?= =?utf-8?B?dlRRd1NYLzNJNjc0ZE9sUjhKam04RXJwa2thNTYrcjVzMVRXS1NoT1hKUkps?= =?utf-8?B?eHNEWjREYkVqcUFBMU9vbDZLRHhNKzQ1VDM5QmRua29LRWpIYzJSSkxXRHpr?= =?utf-8?B?QkM3RzRzaTVHd1AwenZ5NGVDZXVZbENlNWF6ck1ZVCtQZUFoQUJFYjJwOWlt?= =?utf-8?B?MXJrbzFqK0ZPNEorbnR0NE9pQytZY0lOQjdxQXFBUS92WldacEloYkpOcTRH?= =?utf-8?B?L3M2OHkxTFZublI1Y2VZR3NiYUhRWWxTYnFFamptZVVwN3Q5WkJsM0hNSHh2?= =?utf-8?B?Tmc9PQ==?= Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-OriginatorOrg: AnthropLOGIC.onmicrosoft.com X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-AuthSource: DS0PR20MB6232.namprd20.prod.outlook.com X-MS-Exchange-CrossTenant-Network-Message-Id: 2e3d2400-2a95-4730-02e1-08dc94b754e8 X-MS-Exchange-CrossTenant-originalarrivaltime: 25 Jun 2024 01:37:10.3879 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 92c6c2d0-5fb7-4778-af38-bb58423944dd X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: 1RK/OkhvZeRxeRX9bHNVgGdICGVdybLmo+OaUpbCG5NIx9ajAFrE5EmNcV7qjKsLop4Cm1jhUKEDce4aTGR6elzoLKLf8gn4mtfMdnEveDVXzxPFpHi2Mswc+qBN6T6u X-MS-Exchange-Transport-CrossTenantHeadersStamped: SA1PR20MB7190 X-Original-Sender: admin@anthroplogic.onmicrosoft.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@AnthropLOGIC.onmicrosoft.com header.s=selector1-AnthropLOGIC-onmicrosoft-com header.b=EXkufdrD; arc=pass (i=1 spf=pass spfdomain=anthroplogic.onmicrosoft.com dkim=pass dkdomain=anthroplogic.onmicrosoft.com dmarc=pass fromdomain=anthroplogic.onmicrosoft.com); spf=pass (google.com: domain of admin@anthroplogic.onmicrosoft.com designates 2a01:111:f403:2414::707 as permitted sender) smtp.mailfrom=admin@anthroplogic.onmicrosoft.com 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: , Salut Ciryl [updated]: https://github.com/1337777/cartier/blob/master/cartierSolution15= .lp Indeed your goal could be non-trivial if translation implies compilation vi= a machine learning, especially Kosta Dosen's normalization of functorial pr= ograms. Kosta Dosen=E2=80=99s book =C2=AB Cut-elimination in categories =C2=BB (199= 9) is how some good substructural formulation of the Yoneda lemma, via prof= unctors, allows for computation and automatic-decidability of categorial eq= uations. For example, the profunctor C[ F =E2=80=93 , _ ] is a distinct com= puter type than the hom-profunctor C[ =E2=80=93 , _ ] of the category C app= lied to outer objects of the form (F =E2=80=93) This new stricter typing discipline is still successful to compute with pol= ynomials (morphisms of polynomial-bicomodules along cofunctors of categorie= s, substitution of polynomials, and their prafunctor semantics) via their u= nderlying profunctors. It is conjectured that these computations can be ext= ended to analytic functors and their automatic differentiation (via linear-= logic's exponential comonad on the underlying profunctors) in reverse-mode = (differential categories) for gradient-based neural-learning... And now this updated implementation of fibred profunctors has a draft appli= cation to inductively-constructed covering sieves and sheaf topology: a sie= ve is a fibred profunctor dependent over the hom-profunctor; and the Yoneda= action and lemma (gluing) still holds when the hom-profunctor (the total s= ieve) is replaced by any covering sieve and the presheaf is replaced by a s= heaf. symbol _'=E2=88=98>yonedaTotalDep : =CE=A0 [X Y I: cat] [F : func I X] [R= : mod X Y] [G : func I Y] [r : hom F R G] [A : catd X] [B : catd Y] [II] [= FF : funcd II F A] [RR : modd A R B] [GG : funcd II G B], =CE=A0 [J: cat] [= M : func J X] [JJ : catd J] (MM : funcd JJ M A),=20 homd r FF RR GG =E2=86=92 transfd ((M)_'=E2=88=98>yonedaTotal r) (Unit_mo= dd MM FF) Id_funcd (MM =E2=88=98>>d RR) GG;=20 This is not yet another "categorical semantics of", but here the categories= are syntax which compute (in the Lambdapi proof assistant). For example, h= ere is my review of the folks at "categoricaldeeplearning.com" : it is most= ly categorical semantics fluff of structural-invariants (by permutation, by= translation, etc.) over the domain's metric (discrete, fully-connected, sh= ortest path, etc.) that are baked into each neural network architecture (De= ep Sets, Transformers, Graph Neural Networks, Convolutional Neural Networks= , etc)... nothing "deep", lol Unlike this bad faith's "blind expert peer reviewer" enT8 at ACT2024 who wr= ote about cartierSolution15.lp : =C2=AB This talk purports to prove that 1 = + 2 =3D 3 in multiple ways ... is full of comments saying "todo" ... =C2=BB= but aren't these cartierSolution13.lp cartierSolution14.lp done? [CfP] Wou= ld this reviewer kindly disclose hemself so that we settle 1 + 2 =3D 3 on a= blackboard at CT2024 or at re365.net: re365.net is a free open source Microsoft 365 app, developed by a community= (https://meetup.com/dubai-ai) of 2,000+ contributors, to Schedule reviews = with authors and businesses, with the end-goal to co-author or by-product a= n AI interface for their papers and apps API. And https://dailyReviews.link= is an instance of re365.net for the topics of math.CT/cs.LG/cs.LO; it is s= ome kind of tiktok-style calendar overlay of arxiv.org and producthunt.com = (and soon semanticscholar.org) for users (and editors/marketers) to schedul= e reviews with VIP authors/developers. Frankly, re365.net tries to answer this question: what does the usual pract= ice of citing an (arxiv) preprint paper mean, if it does not mean a "blind = expert peer review"? --=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/DS0PR20MB6232AB422CDB77864CEBEED191D42%40DS0PR20MB6232.n= amprd20.prod.outlook.com.