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=DKIM_SIGNED,DKIM_VALID, FREEMAIL_FROM,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 28828 invoked from network); 21 Mar 2023 13:51:12 -0000 Received: from mail-qk1-x73d.google.com (2607:f8b0:4864:20::73d) by inbox.vuxu.org with ESMTPUTF8; 21 Mar 2023 13:51:12 -0000 Received: by mail-qk1-x73d.google.com with SMTP id c80-20020ae9ed53000000b007468c560e1bsf2438056qkg.2 for ; Tue, 21 Mar 2023 06:51:12 -0700 (PDT) ARC-Seal: i=3; a=rsa-sha256; t=1679406670; cv=pass; d=google.com; s=arc-20160816; b=MOaXmfaUHCV+jP1Zrr1oSrmwvAvOAHSQhQKlXhH9Hbptl4mur1aQeBYFFXZc0IiuUg A7uvCfNrVrgleFTgHFhNmuY5H+PcmeB9/chlUwMSlI6nkIoixjrcWtHpbbS8wZj2WgU+ 4YP3Dp/Seo1LKEm2/LsX7x3xM2O/I1vEn5J3U1LBpdP1j8mRHR3QSnFK6a8gSwI8ldq7 fj3f/6XJmt1KCQyFXB6ykrA90MY3mE2CAFI/soVrmQMxurvV5QKu4c9td632fRdM+qe8 w314HxxXoTmRUWIAQ6IvA6Bpt1RVL4tYkQH2NoOJxTwOdixcWbib57sl/ar24fqv9NTF 6I8w== 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 :content-transfer-encoding:msip_labels:content-language :accept-language:message-id:date:thread-index:thread-topic:subject :to:from:sender:dkim-signature; bh=WCe+lu2ZsiLGQqFH1iuV4JsMHNGfu8NuGuo870iJjQQ=; b=ZAO/JB4ZygvV2AkUGz3szfZwkmwXsS1Ja2zepRx9l4uvRSqvvY+qnor06lq92TsPT/ I5eWipsE73ekAeaF9TIXdR4S6+G72tZ4sUmn5KtC0AZUxo3G3mmiBJAaaD75tS7I2utS ur+qZP59NpMVh92+P9IXY7sLcNivj9y4NBzfvO0uk5KKhQwS3ijQcyJHXDbDzl7NVIMg Mb7VaiMnjCrdpuQVQOgJaA0kRITEfMtptoRqu6oRUCHkuNm1Au7mVs8ZDQ+YylJGZ1L4 upkbiR2HL9IURCP/hVmx1Hnno6RNHw+/maFEa7nQ5lxPPqCV4G9HAGRWCaCDPg5SbLfe P/Xg== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@AnthropLOGIC.onmicrosoft.com header.s=selector1-AnthropLOGIC-onmicrosoft-com header.b=HzUnGXa0; 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:f400:7eaa::60c as permitted sender) smtp.mailfrom=admin@anthroplogic.onmicrosoft.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; t=1679406670; h=list-unsubscribe:list-subscribe: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=WCe+lu2ZsiLGQqFH1iuV4JsMHNGfu8NuGuo870iJjQQ=; b=fg5vLptISFxT8TLZPIddDbbg55fzkj5mCsJiGUmuuuJ5yQ04MSf3rzX8vfxiTG7TGd 8VK63sHm6+rbvb/Hzr26kBWxPLtZl5zWkL3PGxv7zpPGEAmf5MFScfQdgY6Yu+foItui tAdxloXT/Ekppgjebpy0E1M6HbRyqAqQ32c93fO6t43/g3iF/8ukBXDxl+SS8P3Lorz5 VnrR5S5J1wr44uHNx5CHLT5+IDF3XExFCJVuSnfGdNyGIzavLzgmBvxbaA4YY+0Uu6hi Di/6CEFV7HMZGNp4zyNFuWxaOux1/uwluS+ABKPerGFXyHxlRVaYFl440Ty5pNAR5018 I0jw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; t=1679406670; h=list-unsubscribe:list-subscribe: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-gm-message-state:sender :from:to:cc:subject:date:message-id:reply-to; bh=WCe+lu2ZsiLGQqFH1iuV4JsMHNGfu8NuGuo870iJjQQ=; b=2TUHkDHhV9M5pvBSBmoDNZb0qUEF3Pqdm4B62gQMDedhFO7d6S+rjV2GY1zFeKwuTc i4xt/kyeiXoGpk6I8ZZNznPQxJ2oMHd+UyIl8T41zfEbSLHECzjtQllfX7F6Saj4LaXy wRaKfBSkpZuhm1tk2gZ/pjYkcbbFrBUEtUPT78vv9CTwVj5Yo9p4mHjKKW1nqKPA5hfH NBM0QetHj8XLv6iwt0Q/HX7YMxmJEo0ZarpnXPkLLmqyVRV7l3hRLBKa50Us9/f9CfAL LAerI2P3ei+5XYIXsT71EuWV5qK1t54KavfM18f7F5MOlLs+MIC4jgLC/vOlVAhKuZC8 xFFQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AO0yUKWT5afN7Adjtnab4QufrFnPE1LWDYSkWhhoGTTgVVJECrtJm4Oe ouVXkouiJejv5Nf+EYz48xw= X-Google-Smtp-Source: AK7set/wdUoJw87M1YB8/rTTtVyB600lxD+2W0JMMItWwLRQfchno10MpX1O6DrLWaev4LmPHATp/w== X-Received: by 2002:a05:6214:9a4:b0:56f:52da:1d2c with SMTP id du4-20020a05621409a400b0056f52da1d2cmr467540qvb.7.1679406669697; Tue, 21 Mar 2023 06:51:09 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:622a:4ccc:b0:3e3:7e10:9748 with SMTP id fa12-20020a05622a4ccc00b003e37e109748ls2968691qtb.3.-pod-prod-gmail; Tue, 21 Mar 2023 06:51:08 -0700 (PDT) X-Received: by 2002:a05:622a:1353:b0:3e3:8587:21f8 with SMTP id w19-20020a05622a135300b003e3858721f8mr473877qtk.8.1679406668699; Tue, 21 Mar 2023 06:51:08 -0700 (PDT) Received: by 2002:a05:620a:45a1:b0:745:881b:d804 with SMTP id af79cd13be357-7469b419c7ams85a; Tue, 21 Mar 2023 04:37:15 -0700 (PDT) X-Received: by 2002:aa7:d7d4:0:b0:501:d43e:d1dd with SMTP id e20-20020aa7d7d4000000b00501d43ed1ddmr2609834eds.33.1679398634349; Tue, 21 Mar 2023 04:37:14 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1679398634; cv=pass; d=google.com; s=arc-20160816; b=FvkzbNUbeBpkJaq2wwZJWrpK8ZArtn0msLu/N0eBv3Woxfw0mnALDwfMktbjy3V6+a iwWP5x/Tc+GttmV/6oFQmLtTCTrTx372YcrFGLt0FSHbG7gQ8DJXhfQ/ycrTqwQCwFvr /l/6cTQt/pw8tds87bqBS9bwbILmjsFyTmaZrasNJ9gjq98S5lN3VuIHxwSEZG7DM3PF GhLSGKmyhcZ1QyghEyrLL/9WmKyzfR6cUk1/7G9sLF1AWmwEGPaGtHLgsjAM8xGWKltl FRhAMXTVglcJz6594nDdAoHKfky/z0XZsI482FDCdDwsjenBbabyoqsQw/MDa9RNeXLY znEg== 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=iAunG5GjPxKgVBSw3PfCJ3V9EUb4UyZIQkx7CGPGXRk=; b=wzaTghXZSXSn2FUqKdc4bglSvwJMyESCpDrkpBRzT1PIGF27dBsESa/D4jiGPb21sN xsN+QL50+MnRRGUF1OTxmE75mOqOYEp+VU43l/nbHhdfWYPMk6z6QGQ6EcpzqEVUsetr 7d/CZpKgUyFiCTGpQw4Z+E4H6JOyisOMmSWkUWAPwebM2t4FaPJJAtl6qzsQdOPQptUA 0cD51uIa4PvAJrdJdVWnYiC/p7dFHi5MNa1FcRoIInOvDkgAVKbL3u4hJKwPMAQPEK+W Y8zpfEqnlc4hOhDKq93OBZVYIJSJ9mI5OMbrZNBF/97OwyJorr50aKYM38qO9v2jAK4M hbTA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@AnthropLOGIC.onmicrosoft.com header.s=selector1-AnthropLOGIC-onmicrosoft-com header.b=HzUnGXa0; 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:f400:7eaa::60c as permitted sender) smtp.mailfrom=admin@anthroplogic.onmicrosoft.com Received: from NAM11-DM6-obe.outbound.protection.outlook.com (mail-dm6nam11on2060c.outbound.protection.outlook.com. [2a01:111:f400:7eaa::60c]) by gmr-mx.google.com with ESMTPS id f20-20020a0564021e9400b00501da628407si66950edf.4.2023.03.21.04.37.14 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Tue, 21 Mar 2023 04:37:14 -0700 (PDT) Received-SPF: pass (google.com: domain of admin@anthroplogic.onmicrosoft.com designates 2a01:111:f400:7eaa::60c as permitted sender) client-ip=2a01:111:f400:7eaa::60c; ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=amTEg3l7SMGE7d0seISdaFikLH2ZDxLuqYIUtdi3t6w+pEqkh1vGQWSBR5OXhzf3AuSgLrJOYjYUUh5rm9snbLlAVeYDdZXfVV9HiDpYGmzsPiGfmVvdTZyoWBR8MpKCt1+9PTyxehKWc1zdz3qafggEyuZz1mVRNU5JpiatxN+2wzom8Xh44LI7xqDtkJE4oXt5KLQU5vrPk5KyBnLXBy2YxNrO656bsdSe6CYkX0vlcbOIH1FgL0H/9GV+hbd6hLbCo1vPI+3FqxR+dnY/gcWT1XXKAE6iWOvlsSuyPP3dZZ3AolfhjowkpTYB8eJLRAtL3TQZd0+GJWc9+AQ/RA== 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=iAunG5GjPxKgVBSw3PfCJ3V9EUb4UyZIQkx7CGPGXRk=; b=aDu9yDMuBcrerzuuw8ZdzhFKEonRaUXHluLS2NxUwclYRicSuZ0M3/P9iSzFCsDIripQO8nyyaAutS9sEqtMpdz5gRAJwdpcWJ/1uOTyBDvuyJmVzKhTNGtyWrG1WGuQ2D0r27G6XMXMJYX2Jx0S6F1VuATNKYdqgUW1zRX8glRVXsiBJ9cEwUO76/B2sMveSdxib579GqMGzHR6pIyR8D0Ps2kvOl1X/y5oEGYms6sVQ++DfZQ6xu5OKlKJP6d+VoGPFKiXiDKtovtP5XZW1maahFSW28/FHNfhOpmg7m5C50kDQll95UX7t4eh6jxpTQRrFFiKE7l7M6LZkyBazw== 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 BYAPR20MB2790.namprd20.prod.outlook.com (2603:10b6:a03:b5::31) by BN0PR20MB3847.namprd20.prod.outlook.com (2603:10b6:408:127::17) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.6222.8; Tue, 21 Mar 2023 11:37:10 +0000 Received: from BYAPR20MB2790.namprd20.prod.outlook.com ([fe80::439e:3e13:d73f:2164]) by BYAPR20MB2790.namprd20.prod.outlook.com ([fe80::439e:3e13:d73f:2164%4]) with mapi id 15.20.6222.010; Tue, 21 Mar 2023 11:37:09 +0000 From: admin To: "mathieu.anel@gmail.com" , "homotopytypetheory@googlegroups.com" , "denis-charles.cisinski@ur.de" , "coq-club@inria.fr" Subject: =?UTF-8?Q?=5BHoTT=5D_Re=3A_=5BCMU=2DHoTT=5D_Special_lectures_Directed_Type?= =?UTF-8?Q?_Theory_=E2=80=94_via_dependent_profunctor=2Dtypes_following_Kosta_D?= =?UTF-8?Q?osen?= Thread-Topic: =?utf-8?B?W0NNVS1Ib1RUXSBTcGVjaWFsIGxlY3R1cmVzIERpcmVjdGVkIFR5cGUgVGhl?= =?utf-8?B?b3J5IOKAlCB2aWEgZGVwZW5kZW50IHByb2Z1bmN0b3ItdHlwZXMgZm9sbG93?= =?utf-8?Q?ing_Kosta_Dosen?= Thread-Index: AQHZW88TquQ0/PUXz0WLEFCq7fppbg== Date: Tue, 21 Mar 2023 09:54:05 +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: BYAPR20MB2790:EE_|BN0PR20MB3847:EE_ x-ms-office365-filtering-correlation-id: 00fb6476-a6d8-4679-e462-08db2a009b56 x-ms-exchange-senderadcheck: 1 x-ms-exchange-antispam-relay: 0 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: 7ZJScMcH9g1/G9RueSqbUOJX/q2EH14HmJFNhg0o7ASzoWFXS0yDnaQBo6LDjsxbKgPqUQOpXrAZcMNdW2IuhtZYdSG0uVJABKeH+YHm+v5dsjvvKqtgfceWHhkA4t1Dj0dqFJx0+mpRHMufXBoQTsLPkdys57dTAj9KwM9g9SdUeQ+8jCmxO9DGsZhxNuUzo44ZpQ49ntWSHVX/O28tNfk4FYVl01NsbsiWffb30k/Tk+6RAz2nVOWD6s9VGNI/VbE2z1H4Bj6NcRfQQq2xFeM3qUC99j+dGEFJ/PP84gGd3od6VNv0IkB7Z5DgrwE0MkWd8aEkL+Q30bjMQCqoW2HNLjsX4w2uHV/wqNA4+ohtHLw7IbteR9WQBBHa5BaIvSHKzvH+pPlLQcok/y3td7/ZOWTv5NmOf0/VVvZxPYkZ8Ggm/3jg1kYdaI+iq2zh1Nf6t9+J30Pg/KX+X29OkhW6XRNjb0rZTqrtb5wqURyelZed9D44O3mJgGCgPYrMdYajBcVnQpsx33FRw5zIlQJCtNuTgPCCJqwFnRVD8zEgn/mh0/UpxpgJracgco7lQqSZWM92NKIDxhbIAFmkYXzomrhb5R72uzwG2IOAQBnjomS9mcm1cqEdxiNMsJMzVXblIEb5/tBFvG7MpZMN74BrAQJj3FtS9FTLmf7djdqI4zIl7ER/0SgezLHw9DO3n2B8DQELSBUvMlcn77/fxg== x-forefront-antispam-report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:BYAPR20MB2790.namprd20.prod.outlook.com;PTR:;CAT:NONE;SFS:(13230025)(39830400003)(376002)(136003)(396003)(366004)(346002)(451199018)(110136005)(76116006)(478600001)(64756008)(66556008)(66946007)(66446008)(66476007)(91956017)(316002)(52536014)(66574015)(41300700001)(5660300002)(7406005)(7416002)(8936002)(83380400001)(86362001)(55016003)(38070700005)(33656002)(26005)(71200400001)(186003)(9686003)(6666004)(6506007)(2906002)(38100700002)(966005)(7696005)(122000001)(90356010);DIR:OUT;SFP:1101; x-ms-exchange-antispam-messagedata-chunkcount: 1 x-ms-exchange-antispam-messagedata-0: =?utf-8?B?UWxHZW9VSnc2WmJrRytpamh6UlpBaHF0MVgrMjlka1M3R0JINitSV3JuODhN?= =?utf-8?B?MXpVbnZNUnJjcjYxSkM2MDY2MnhpVHduRVpyYWhMeXFaUjVvWlgrZHBqN1dF?= =?utf-8?B?WXZKRHQ2Um5DeFBlc2NrdXExclZ0dmxFZUZqMFdVYWRubEZwdXBiY0VpakZW?= =?utf-8?B?aUJGSXh1OVpOb2twTTZCUi9SMk5hWWFJcHg3RjFsZmNFS0dpSHNZRXNWcVBE?= =?utf-8?B?eWQ3eXp1bHRDWE03SlY1WjZIbnZRRkVaVCtKQ3ZzZVlPNnluNzVpaE5CbUh1?= =?utf-8?B?TmMvOWZvTGpGMHdTWlJQdkk1Q0xvVmZiVmpiUWJXOVJtM2FRMVE5NE9SVnZ5?= =?utf-8?B?N3RRWldicVR6N0I1eURCS3RxQ1h5WDJvOTU5d0RlWk5wV2xrRFRlUXZKZEtP?= =?utf-8?B?aVpXRW94bTV1b3JFYUh5Umt3ZkhRbVArbTJSWU5PaEYvdWhEbGY4YTFDZFk4?= =?utf-8?B?L1NOaW9uSXZmcXEyMThpMHNlUmloc3VWUzdRS01XRVduVWdEWWZETUplalBW?= =?utf-8?B?ZFBmeXRTb1N5QVdhMzMzUVpXYXpIMGpOMGZkQjg4NU4yTjlEekpnWHlBbUxJ?= =?utf-8?B?a1V5Kzlxa2ovMWUxZzZJMnZVa24xbzJFWlplSXdoV2NWT1ZMcUFqTTlsUkU5?= =?utf-8?B?dXZ2ZThpRFhQN1FXb3NLTE5EcW9rMGMvNGxOY1JGOU9IOUNJTWtXNVpueTlP?= =?utf-8?B?TnhwTWozN2FDWnkrRlhJcG5ab01MWUs0MXRDWXdKYk9rV2hINFBOVUVzSHZX?= =?utf-8?B?ZENIaTlla2dHaHVqbVZDVFpZanZsSDNaR3ZTV1JOZWhPWjRhNDBZWjF5RSs2?= =?utf-8?B?MCtnTVQ2U21Hb0xXS2lZdVVoeFFOaEZwM0NHRUlJRXppUytabnJoY015Mktx?= =?utf-8?B?MzdoRUQ4eDk1NmQ4aDl1YmdOMDA2R1VmREdlK2VFRG9yK2JDOFBuSnphU2tY?= =?utf-8?B?UitwM280Tms1SHI3cnhFVlpLYmg2MjV0a0RiVjlzUnU4QlhOYk9VL2VOVGRG?= =?utf-8?B?NW1meXdUL1JobGtmMXB1MFRNaEZKSjB1OVNON2haWkZCUFVFV0NRQmE0MFAz?= =?utf-8?B?TTN2QjZWZU5Va1JLTTN5czUyY09CRkg3bGViM1MwdWtST3FXc20rSGhybGRM?= =?utf-8?B?djJva3NoT0h1R3dOWi9yY3dnRlByOEJVVmkxaVAyQlh3UW54dEF5UWJHU2M2?= =?utf-8?B?R3BnNnREazBScWYwRG1wM003bkhIaFlmSjZuR2RHZXNLeUI4TkptcjBpU1hP?= =?utf-8?B?WDVoc2Q5TXZXQ0ZkVytac2R1UXpqV2xISWlnejQweFpWMXhJbjJBbFhiM1pL?= =?utf-8?B?RTVDTUVQQnpwTHVGd21TQXhlenZpWnlIRHBSeWNLY1BQdjRSeENyaytKRU9j?= =?utf-8?B?S0Q3ZDhJMEpwcllQZGM0YXRubzVKYVloK1lkTHg0d1RlUTNXUlN1T3hxL09u?= =?utf-8?B?QXZsOHR1SkFDTitwa283QXQ4NkMyTEpVbFV0U0MwNnp4SEMzMnFSVzFZSVRP?= =?utf-8?B?S1JEbGFkUmxpelA2bjRyQ3JsM1RoRXpkYkMybUFwV3RRRUdMWWVza1F2VGxI?= =?utf-8?B?Um5sZnRzZm16OWZqMzQwRmVoRU1oYklEUGJjcWVOOFVsMVl5dks1NkNUTHM4?= =?utf-8?B?WFVuNEJaREZja0RyMXl3d0tyYlphM2RYcjlHZkVsNFhpN0h0Z0NxK29QMTJI?= =?utf-8?B?R2lVcC9QanpJaTRNVThFSW5YK2xNTWdjdmxBZzgxSXZDcHFBdzMvbFNtandy?= =?utf-8?B?dlVXaU5kejVuV1g4OHZjb0ZqRFJaTzRuSkVzbk0rQVU1NTFzNzZwdzNaZWZN?= =?utf-8?B?OGZnL0FIRU1BTjlTNFlGbmRQWTIyTXQ3OHFOSFVERTRBYkFyYWtiUG45TUNu?= =?utf-8?B?WmUzam1VRjRJWjFXQThaNElqelNmMU53b0M3U0psanI1UFU0OTE4TWZWa1Qv?= =?utf-8?B?ZHBZb3FWTzZ4RlB6aFpFeTJHRXFWSkNaVXVVNmt6VFRnaEJLZGVEWm0yNjZT?= =?utf-8?B?NzZ3M1BOd2xYU3B5QzljZ2x3dk5yOTdmRDlxdGNQOW9LK200bE85bFB6ZWJZ?= =?utf-8?B?UzJQbk1TbUdwRVdRSHdMRWorc0ZnMnVrZ3c1NDIvc2hNbGp6V1ZHeGEzOElW?= =?utf-8?B?ajJxUno3d3ZmT3FSNGtLSFRLdTJ1Y0VjT1Y2UDdWbmZwM3VrNFlvMzBROFlI?= =?utf-8?Q?h4tTNDS9RjQbCMJHI/iX/F4=3D?= 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: BYAPR20MB2790.namprd20.prod.outlook.com X-MS-Exchange-CrossTenant-Network-Message-Id: 00fb6476-a6d8-4679-e462-08db2a009b56 X-MS-Exchange-CrossTenant-originalarrivaltime: 21 Mar 2023 11:37:08.5934 (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: HJRhYtZlAy9+dWXcWIGG7/0tmKLclBqou35DKzdB5QOai/Ygr0MrlsbYIRRokxJGdXzeDY/bUeOk/8AbeG5oClZsNem16tmxruFEJ5C33qMm/lRseB4+6Yc9bW6Lc2T6 X-MS-Exchange-Transport-CrossTenantHeadersStamped: BN0PR20MB3847 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=HzUnGXa0; 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:f400:7eaa::60c 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: , List-Unsubscribe: , Salut DCC, ton 2=C3=A8me cours s=C3=A9mantique m'ennuyait alors en attente = du 3=C3=A8me cours syntaxique voici une response at yesterday's Joyal hint = towards hes alternative presentation via barrels (profunctors): https://ncatlab.org/joyalscatlab/published/Distributors+and+barrels implemented as cut-elimination in the double category of dependent-profunct= ors with J-rule-eliminated adjunctions: https://github.com/1337777/cartier/blob/master/cartierSolution12.lp Here, a covering (co)sieve is implemented simply as a fibration of profunct= ors, which covers some base (unit-hom) profunctor at some fixed covariant v= ariable (the contravariant piece is understood as some codomain fibration o= f categories). This was hinted also in Joyal's page. Now this failure of sieves being monomorphisms is the motivation for the ne= w =E2=80=9Cgrammatical sheaf cohomology=E2=80=9D, where the redundant stora= ge space for functions defined over the topology is what allows possibly-in= compatible functions to be glued: gluing: F(U0)=E2=8A=95F(U1)=E2=8A=95F(U01) =E2=86=92 F(U) ((f0,f01),(g1,g01),(h01)) =E2=86=A6 (f0,g1,f01+g01-h01) Another alternative from =E2=80=9Ctype theory=E2=80=9D and its types with (= global) elements, is instead Kosta Dosen-style =E2=80=9Ccategorial programm= ing=E2=80=9D which is about morphisms (generalized elements) between profun= ctor-types (of arrows data). This new functorial lambda calculus evaluation= has been implemented as: =E2=80=9C=CF=B5_(B,O)=E2=88=98 B=E2=8A=97(g)=E2=80=9D =E2=88=98 (x=E2=8A= =97f) =3D =E2=80=9C=CF=B5_(A,O)=E2=88=98 A=E2=8A=97((x=E2=87=92O) =E2=88=98 (g = =E2=88=98 f))=E2=80=9D , for x:A=E2=86=92B where the input argument x is simply accumulated using the implication _=E2= =87=92_ bifunctor. And the new =E2=80=9CJ-rule=E2=80=9D has been implemente= d as simply the construction that, given some global element of some profun= ctor datatype, it generates the morphism (transformation) from the unit-hom= -profunctor towards this profunctor datatype (semantically by covariant/con= travariant action/composition): | Unit_con_transf : =CE=A0 [I A B J : cat] [F : func I A] [R : mod A B] [= G : func I B], =CE=A0 (M : func J A), hom F R G =E2=86=92 transf (Unit_mod = M F) Id_func (M =E2=88=98>> R) G Therefore, this general setup has facilitated the implementation of cut-eli= mination (J-rule elimination) for any adjunctions of functors and of their = decidability of equations between data (arrows inside categories). Also thi= s implementation has expressed and proved computationally that any right ad= joint functor preserves the profunctor-weighted limits of other functors: assert [B J J' A I : cat] (F : func J B) (W : mod J' J) (F_=E2=87=90_W : = func J' B) (isl : isLimit F W F_=E2=87=90_W) (R : func B A) (L : func A B) = (isa : isAdj L R) (M : func I A) =E2=8A=A2 ((((M)_'=E2=88=98> (Adj_cov_hom isa F)) =E2=87=902 (Id_transf W)) ''=E2=88=98 (limit_intro_transf isl (M =E2=88=98> L))) ''=E2=88=98 ((Adj_con_hom isa M) =E2=88=98>'_(F_=E2=87=90_W)) : transf ((Unit_mod M (R <=E2=88=98 F)) =E2=87=90 W) Id_func (Unit_mod M = (R <=E2=88=98 F_=E2=87=90_W)) Id_func This implementation moreover would enable new executable applications to th= e study of graphs transformations understood as categorial rewriting in a d= ouble category, where the objects are graphs, the vertical monomorphisms ar= e pattern-matching subterms inside contexts and the horizontal morphisms ar= e congruent/contextual rewriting steps. Finally, the core difficulty at implementing Kosta Dosen (ref [1], [2], [3]= , [4], [5]) would be the long-term synchronized industrial labor and the ne= w format for reviewers-productive-output, which requires tools such as: [CfP] WorkSchool 365 is a new marketing format for authors/brands to disq= ualify reviewers/customers, sign-in at https://WorkSchool365.com=20 [1] Dosen-Petric: Cut Elimination in Categories 1999; [2] Proof-Theoretical Coherence 2004;=20 [3] Proof-Net Categories 2005;=20 [4] Coherence in Linear Predicate Logic 2007;=20 [5] Coherence for closed categories with biproducts 2022 [6] Pierre Cartier --=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/BYAPR20MB2790C743D51D7ADF7AFA077291819%40BYAPR20MB2790.n= amprd20.prod.outlook.com.