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 4319 invoked from network); 14 Apr 2022 15:49:13 -0000 Received: from mail-wm1-x33c.google.com (2a00:1450:4864:20::33c) by inbox.vuxu.org with ESMTPUTF8; 14 Apr 2022 15:49:13 -0000 Received: by mail-wm1-x33c.google.com with SMTP id c125-20020a1c3583000000b0038e3f6e871asf2610850wma.8 for ; Thu, 14 Apr 2022 08:49:13 -0700 (PDT) ARC-Seal: i=3; a=rsa-sha256; t=1649951352; cv=pass; d=google.com; s=arc-20160816; b=iec3Z7Zhx+EB9Cunk+/WA5QFfdVMmvfHoRK4VkcjoZDg0cmMS03tENqur3AGwzKTW1 zlI4zofAxZnsjj/9HHf2edR6V8GMJMsT7U/8/7ygFDOvYxhkpmXN57Tnwao935sqTLlN Cp9lKCdKz/5B69EC2m6xvzYOz6KAk8OljcsG5T/c9daqv42yr9mRnkFRHiVSqVn+GhZD RLVbf9ntqhwtOt088lv+diphuRcWKzMcNq4WiyyQNumDtNGUtMaK0jdRfoJdWpFtd3ai rP/dGmn2eJpjx7B1GKykd9ymnqyq1iMyVItqxYuzyyHwFqzfTWPQz58+u4Iml0lNAcp/ skXA== 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:msip_labels :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:to:from:sender :dkim-signature; bh=M265GwaKcdHPRRnsL0pIoDYCCQljiNT0wKQI+/SKDlc=; b=duCnbcD+UtGGTSmP23fRRcMYKHOM43aAevr3U4ZwxRK1o7TJcXZYRLBGXV1yTXjLsx FrgA2rqPj2r2noB1Uv+OnArQCg4+jjD3VzCnbRUdPYivVr8Hol8i6CIVUSmjlw/K8ZTf Kr+a67RnmEubht3Nxmaq7YorVWCWFcQ4Ppw/lgZhddgQdlg1axwH4TY2kIvgArKqJ5qM hqo+58yrhQ07A7NmXxhuBMuCb+XehBlacCJkqznYAFFhDfSDlJ9B7UP5mG175j380lgu deymsob/qDSnhSvUMXbFuUylRIs8K6E+ny+7KKhEg9lxn9tub0myp3/RUKPs/KUW5EKN 8nXQ== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@UQAM.onmicrosoft.com header.s=selector2-UQAM-onmicrosoft-com header.b=XuE1nOj8; arc=pass (i=1 spf=pass spfdomain=uqam.ca dkim=pass dkdomain=uqam.ca dmarc=pass fromdomain=uqam.ca); spf=pass (google.com: domain of joyal.andre@uqam.ca designates 2a01:111:f400:fe5c::612 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:msip_labels :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=M265GwaKcdHPRRnsL0pIoDYCCQljiNT0wKQI+/SKDlc=; b=qKMtvEHVUnV/zfB/tU1h/x/X16FDQQsALHqcit7zEL5BoMwin4t1axAut9GGat0whk dx02FzPrGs543uvqmaI7Bl+RDSweMIlGlAL9iAop812AzmUqsYI33sK7q9Lj3DRnKC0g vMrGlU4k6IpWj9LB6u8MENxomoLOcNpcFaWu3q8t5SA/Sl2r5dk281/nifFzQB/CTM+b mTY9XZgLWkuysJ4mz+YZVyZDbtqmqSNlAzOZE70AWWgoaMBO0OulLOXcKZV35h9Z36VK rNSgbl1p3fHm97Q47Ba5V/pRj4/TntrOXuOryyZA2LuDsmokNXFRgqnyNRQaI1VQxAaN Sjxg== 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:msip_labels: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=M265GwaKcdHPRRnsL0pIoDYCCQljiNT0wKQI+/SKDlc=; b=7FQ7u0y/i+Rfu2REzS6vc4REkY8HbgNrC2tLU6blTy8DYC/pixJk3KOncpkXKoQjFC 4AovwvG/ePzfhJJNa6wdkED/eCEAdtKutCtq/1QWfdYLA7eyI31vmEC5AzGhkkOnDhSD lAS1KQAvmFzNBO6WzfAnPiN30NrWV8NfkPUNI0WtcJZ6Fi7PvA7Ul71nXiCayidvDDce 9SSgnwME/TxUHfz4ngxp/Kh8sjsB1awooP4RWKrOKcKRYR0E5Ggw2P2uXCN3PEq7pfdt b3zgxMbPEu2Zbld+gcpZc5wEPqKVZCA545iTpsKT0M+zeeubIL1WeLlXxkCWOK5umadQ 2X0A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM5300Oqb+nEd4lBWJnwQK0kA4mGKnEFEyrSZdqA84yZo7IMrw9h9s DY45rYrr/n9djYrf8viyrZA= X-Google-Smtp-Source: ABdhPJx1dh/8B310p/4jAyFts3lOF/qcbjFHTr97H+DOb2R811nWnhq3tM3paVlaTsYHNDuOGvAouA== X-Received: by 2002:a05:600c:21d1:b0:381:4fed:159a with SMTP id x17-20020a05600c21d100b003814fed159amr3783031wmj.143.1649951352566; Thu, 14 Apr 2022 08:49:12 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:600c:3ba1:b0:38e:b80d:4580 with SMTP id n33-20020a05600c3ba100b0038eb80d4580ls2769151wms.0.gmail; Thu, 14 Apr 2022 08:49:10 -0700 (PDT) X-Received: by 2002:a1c:7707:0:b0:38e:b8bc:f0a9 with SMTP id t7-20020a1c7707000000b0038eb8bcf0a9mr4227312wmi.125.1649951350894; Thu, 14 Apr 2022 08:49:10 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1649951350; cv=pass; d=google.com; s=arc-20160816; b=YwicwDK6yyg9nbeJ00C57ui1E/mGtkRWj4Xy8SmUlWOLne/cl2MwM+B3Z6tiHHAklp Mi9PFP6Vo4Rsr2YZLJv8+YFLBBWwxkIvT4g6dN3/Vq+gjvpa+Yz9qvWY4mHfKq8UZf/D j3UHUIq6MPnYvaiac2gSYRYcbxKnOR1vreeEO8ZXz7oSAGU/S0OQMppnbEJEnicuN5Gz jMKf2UzdJHtNpL2Hg32g43dALy3LmkixBV7Fk5kS6mq5VH31VFy7pJb5b+lmm1FdGOJP QVGTVGQ2BhQgGcfqKOu9CR10ywIILQpKFxGuAVyOl5kb7iEEZp2ONi+HfprFrxcAMLsB DCgQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:msip_labels:content-language:accept-language :in-reply-to:references:message-id:date:thread-index:thread-topic :subject:to:from:dkim-signature; bh=AEyWWBwfhVxX9v1gs+9dqMprLPJoihL+IifaYVTKzbQ=; b=id4ynZ2kl1h/iJDsEEzUSwfgqGbODzUmmnBO1JS64n6VWVVW216CLkWlJVRR+5LZSl wEdSWOBS6RQvc0KJJV1KG4Tau059YLdpnTS3NlNXTtmkPAFb8IVp+OySfV9Fs9Pnjx4P 5p6Lz24loq4cb3EuFFyqt3HZ9gvmo2lIkbHN27GwpVpxmQ9tyNJr4U1eKeNzxLLSK/xG xPJlTqjGUQxRkc7GskoN/jdkp5fKYRlbqnoKj9RarCVeExSiJtMXzUNAUXbECglWvmsl +qr0/JrbGEwwyy27D8HMu/M0Rq8u68MryT5IJO+SjkFiq1Cu7Tz3Grvf58MIb86Q3rhp UTTA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@UQAM.onmicrosoft.com header.s=selector2-UQAM-onmicrosoft-com header.b=XuE1nOj8; arc=pass (i=1 spf=pass spfdomain=uqam.ca dkim=pass dkdomain=uqam.ca dmarc=pass fromdomain=uqam.ca); spf=pass (google.com: domain of joyal.andre@uqam.ca designates 2a01:111:f400:fe5c::612 as permitted sender) smtp.mailfrom=joyal.andre@uqam.ca Received: from CAN01-QB1-obe.outbound.protection.outlook.com (mail-qb1can01on0612.outbound.protection.outlook.com. [2a01:111:f400:fe5c::612]) by gmr-mx.google.com with ESMTPS id a9-20020adfe5c9000000b002079112400asi674659wrn.2.2022.04.14.08.49.10 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Apr 2022 08:49:10 -0700 (PDT) Received-SPF: pass (google.com: domain of joyal.andre@uqam.ca designates 2a01:111:f400:fe5c::612 as permitted sender) client-ip=2a01:111:f400:fe5c::612; ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=azm7lU6oZIuOzDDAEvjgpWtDRpAeU5Dc1uqHSEpMOGdICKRqSK2f9XyKEoi4WYKEf4RrD21L4J3hZ+k6i1enPNeW5zQC2C3gbaCifFaxQ054xc+BEe1+Bv9FzvYlxxbeBmnfw38sjDOijoxOgfHKpigUTWLGbkXwnKCK7EBpSb3jSu4azBvBEtJkHk04OypNR8aTAag/cbSpB/uYCnKXtM3pxfc2FzwgZk3Bhr8Iaq+Y67PxNf5YKTFKjBnLYy4c/2yBznHJOF8pX2Ensrg/CDzrLIlKfFaRZyitjJm+uYT9WRNlvfaCz880ZJe7FG5aEONME17qlx7jBWCA9hNg9w== 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=AEyWWBwfhVxX9v1gs+9dqMprLPJoihL+IifaYVTKzbQ=; b=mCYG6VU0HQRoj2j2NaXZTVSmkwPzNuKTK43rNr5xNg1TdKJajWyAp/YD910M8dm7m9xWvri3coIKr0ZMdvpXuHIZFYRmNYnsVF/Z0zYTd8O5QQ0V0JHrQ3oHvWShf2MbDnd/aE9g3cI46f5iyCDONU2CBCqhuFTGr3zy3FAHFgaWMXPoIXRD+Vbqg2ThZ2yLYRguLXeX01foa0IMJcKGl1zVGJow7zXnKq4jNoofCPr7X0Gtvc8n3UUN1CEJLtWEVXlLJ53K5di5heY/qs1GWWJo5INpWr9/YhS/mzSr8BShHkPO5lq/n6Ex1xSsBlm9QOFQPymI1L2nyhk45W2Blg== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=uqam.ca; dmarc=pass action=none header.from=uqam.ca; dkim=pass header.d=uqam.ca; arc=none Received: from QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.COM (2603:10b6:c00:38::33) by YTBPR01MB2845.CANPRD01.PROD.OUTLOOK.COM (2603:10b6:b01:26::28) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.5164.20; Thu, 14 Apr 2022 15:49:08 +0000 Received: from QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.COM ([fe80::d1f1:a9d4:8055:73b]) by QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.COM ([fe80::d1f1:a9d4:8055:73b%6]) with mapi id 15.20.5144.030; Thu, 14 Apr 2022 15:49:08 +0000 From: =?utf-8?B?Sm95YWwsIEFuZHLDqQ==?= To: Chris Kapulkin , HoTT Electronic Seminar Talks , Homotopy Type Theory , "categories@mta.ca" Subject: Re: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series Thread-Topic: [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series Thread-Index: AQHYTaitXJ7chRA+e0u2XHfF/ZpE3azvjwxq Date: Thu, 14 Apr 2022 15:49:08 +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: msip_labels: x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: 6ad07166-0376-4d6c-5651-08da1e2e4fd0 x-ms-traffictypediagnostic: YTBPR01MB2845:EE_ x-microsoft-antispam-prvs: x-ms-exchange-senderadcheck: 1 x-ms-exchange-antispam-relay: 0 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: enIFjsnEz5uoH22dSNI+EUTUmXfc8norEx7O9InuIxxpfK0AWmlhFNoVwVSymyLzCI8nhRmp06qbS+9goUTfG/8rZJczbpTmpNFRVApTZ0Gb4aFgIODywtxdUlb1nv+QcQCPbEJTGL3wnloBxS56rbLUdNBqMR/6hI7nzT1Sbp7LB43j3rcia3jLG+kZYe/EbFUskrnbGXPksxJ2wcRTVok2rpA0qMX9gdz2H3slFJ8R6WfY51ihn9mwAKC6HzCDyVjwPIkTj4HqVeEesTD1IOFpzZ0Y31xluO9pwYpHRTXhoeINFAuvw9RM1TuoNTfHXJf37oOaj4cWqifHHaLHKs/AYFG7pwXiuzqRwQFjeBjA4Apr8oICZIrSXoa4nlDE4ZeuxA8EVr3TpiXYlKxh0lVbfdJzoETEBMxdx4zeB9rLZf/g8JR+puRCLLAFzctJof2R0T37D/DxI6iDbkf+WesFJBDDQAUpdCFJqow3BygJDXouP9ODnkAztK+xxCiRTmxtZH9lGyrlkrlpB62oGzxnV4suk4eFSec6DWWgx9ALc1k9BcJWLRfCIETWSgo/BWsIy+y/BllHQr/JvUqpBZV0iR06bhwog6K2mVELtCi+6OCyw0L1uqawnsFZczB3OV9Mf/OX/6LklYgZE8QPKK3MfYX5qmZeODmEfiZv0vvz/wny3gVUcgZZR9QpqGVDD4xA++WXZjxqiqBKq/5DPLV6DtefgPICIec5B59/nSz9atxRFk/QmgsGBnzlFLLHzUXDqcN82OQ09atRf0TcPf/D0h7rSndxJXFs9ZIwoWvuw2QytkiF2AztNKghWYh/ 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)(64756008)(8676002)(2906002)(66446008)(76116006)(21615005)(66946007)(66476007)(66556008)(5660300002)(966005)(55016003)(166002)(122000001)(83380400001)(38070700005)(52536014)(38100700002)(8936002)(186003)(19627405001)(508600001)(9686003)(71200400001)(26005)(110136005)(7696005)(6506007)(85182001)(33656002)(86362001)(786003)(316002)(10090945011);DIR:OUT;SFP:1101; x-ms-exchange-antispam-messagedata-chunkcount: 1 x-ms-exchange-antispam-messagedata-0: =?utf-8?B?dytoMDZmQlRUZmJvYWNLcDlGTzRKTHpxb2IxbmYwL1hXSVJmUmNzMWxiLzho?= =?utf-8?B?RWNTOUloaEdQVEl6Z25wTU5VNURWbjU4dEM1L3E5ZWNmeHpLSE5xSTk5ajB3?= =?utf-8?B?K3ZtZW1Tck5hUVZrUFZjcnRjbGl1N2NpbENUNVNYZm53QnJpaHNlT2c2QzF3?= =?utf-8?B?VTYzUHdYTE9XZ09yalkvZHRqdjdpUkhKb0pHNHRab0x3bHkvZS9obndiZXU1?= =?utf-8?B?ZXdPdHNZUjhZR1VXU2xrWmlpbUtOb3A1RVBIbEtxNTh2M0ZMOHVySW5XdkdC?= =?utf-8?B?czFFR0tZN3gzNmd5MGlwZnd2SHFHcXVNc2lXSmFxMFBXNmh0cUkvVlpxLzl5?= =?utf-8?B?bDVhRUpyWVA0SmVhRDRzSDh4bVlzOGtkUWR5ejhvSUFGbTRiZ2pQb21ucjU5?= =?utf-8?B?OG5DNnhQU2RJYlNlZUpCVTUwdWdIc0VicXAzRXZ6ZzBQNzZwUjVOa04zcGFn?= =?utf-8?B?Mkc1VWVsbU80clpneVBIZHFPRXVJT1lVdFNpMUlPbTlncFdTNzNkM0RqVEZz?= =?utf-8?B?dHcxaHBPMERNZ25nVklGVnQ0SVJzL1JSVHBVb29YUWR0MEdYbnBoc1lLdkdk?= =?utf-8?B?Q1lzaTdhREx4cHMxOXhtUmxwdUVzbjFsamJ1UjJXQXNKWFpQUFNUOVBRajRo?= =?utf-8?B?dHY5M254a3htYjNvMlNJYmpxbUQxanNiQVJUWm9hM2ZuK1c5c1RlWStDSmxH?= =?utf-8?B?cVVUd002MThWSjc3dGo1VVU2emZ5R0NpSkY2dGN0M2NsSzRYWDBSTmlzWFR2?= =?utf-8?B?VVAyUXQ5RGtLaWEvT0NHS0xwUGoxTEwrZWc2SnQyOXhDaUxhK0Z5RGZIR2hZ?= =?utf-8?B?VFFyLzgxRGxJOFdNOXFETk5wVW10QmJlMlVZdk1iM095Nm8zcmlpK2E0d3Z3?= =?utf-8?B?RitDRWQ1MWhRNXlxMi84UlBiajg5Z0RKZ0oyZDVqczRSRjJIRzhjMFhXaUhJ?= =?utf-8?B?OWhSVnV6RjdNVWUyejNhaVIrYUdMTnhtRUlmOVRvNFZpUCtpNDgxMVZDUDZa?= =?utf-8?B?QXZnUU5UMStRbnVoYm8yY3EvYVpidjJjMTZtOENGclowN1NqVGJuZFArV2M2?= =?utf-8?B?RisvTm11Yk1HdEpVZ1BFVFAwQ05lSC9mcjRvSnFUZHk3NzlrSUlHOWxKSUt2?= =?utf-8?B?Q1owajlFbjZ4bkRneFgyTHdQQmljSHdMYWFuek40TVdnbUpIK2d1WHZxeVM4?= =?utf-8?B?c1JOc05TWTNEcUJZeUZtVnJZUVZnLzFnb0pxWC9OS3pXODRHSWtWSFh3Z3Jk?= =?utf-8?B?U1VqU0dXRXpyQXlZUWJFRjZJMU9OUnBzOXlsNndWelBUc1JtMk9zTUU2MDk2?= =?utf-8?B?bDRqdnRBckZvMEtLVGNUWGREK3NsbERtd0gxaTJlK2VucUd3TitjTGllQkIz?= =?utf-8?B?UDFvOVlqVkNvWERzVGR5QXFRd2Q4OHkyTVpPZncxcHlPR3lFWWRMRXhNNUVO?= =?utf-8?B?NHRtMzN3d0xVT0wxSlhsbHBUSVNVM2VFeHg2dEdDTVBaQjdFWEhUYVFaWTJw?= =?utf-8?B?WGNyd3hxV0I5WmsrZSt2dW9uVlZWMml3YVpsK203YVJHWVoxdE00TDNYenpO?= =?utf-8?B?M3lyWk5kOVdnbmxWcTRXWU43cHdySUpOSkU2dXE5a0RnOFgvejZma2x4cjNI?= =?utf-8?B?dkRTSXBIVE1qbXJXY3loZ1F0QWZ2dFZaTUJLWjVtU3ovQWVNdU5xcTZrYVhs?= =?utf-8?B?S3VrMy9zOFQyRU9nRWZpTkwyaEM3YUIwdkN0NklJcnozMHBqZHRQajhaRTU0?= =?utf-8?B?N0x4dUcvbDBTaWl0VHQ3UENLS2RId1E1WmgxOUllWExzKzVnTWhLWXlicjRS?= =?utf-8?B?R0NhaUg2K0JWaGVWd1V1ek5GemZlRld2ai9rVENwek1RdVlPMGovbzNGNXVt?= =?utf-8?B?NFFVeVkyNHljc0Uvd0dXN3JZcW90ajNKRjRqRk8wbnc3ekJ1Y2xNd05SZkxN?= =?utf-8?B?OFVibEVRTDNIdlpzRGlBak55by96RlQzMHBQbHRaeEdoZkk2dVV3VWpkc1Nn?= =?utf-8?B?czk1dG5SK2o5azA5RUx1dnVYZlR0TndWa3NZZUdTWkgwQjRYSHRveDJrZVZR?= =?utf-8?B?SzlYOEEyck1jakRIdXpQU1hRZmxiMnhMcC9CbWY5U3o5bjg4MnFkMkdZS2hr?= =?utf-8?B?WEdFLzU3VUFmcVZ4TWVaSFJIbXdTZEtVOUx1ekFSNG9FTzFVaTVXbDFDMmNw?= =?utf-8?B?RG83UVZLR2UyejQ4bGJHV0ZXamoyNWNlUDRhMktMRVg5cE5XTWFQNklUd0dL?= =?utf-8?B?VVcyS1RnUmtLUHV6MEJhdVpldDF6U1RkWHdLZC9rNkxOM1NkODVPbHYwWTFU?= =?utf-8?B?QWZ1SWJ2NlhENnhWdnpTT0FMRi9HQmdteWRIVXZZR0JydVJzM2RIdz09?= Content-Type: multipart/alternative; boundary="_000_QB1PR01MB2948B2FA84E4733851CA50F4FDEF9QB1PR01MB2948CANP_" 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: 6ad07166-0376-4d6c-5651-08da1e2e4fd0 X-MS-Exchange-CrossTenant-originalarrivaltime: 14 Apr 2022 15:49:08.2260 (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: B+WeuSsAVIXij3g6/gxRsqpNOXQe3W3Hpa4oHW8ARndBjnI7JsVUIwUpMHy4EtHMPSmpd1o3MaDFEw3qEWTksA== X-MS-Exchange-Transport-CrossTenantHeadersStamped: YTBPR01MB2845 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=XuE1nOj8; arc=pass (i=1 spf=pass spfdomain=uqam.ca dkim=pass dkdomain=uqam.ca dmarc=pass fromdomain=uqam.ca); spf=pass (google.com: domain of joyal.andre@uqam.ca designates 2a01:111:f400:fe5c::612 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_QB1PR01MB2948B2FA84E4733851CA50F4FDEF9QB1PR01MB2948CANP_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable To the organisers of the HoTTEST Distinguished Lecture Series: Carlo Angiuli, Dan Christensen Chris Kapulkin I am very disappointed you have cancelled the lectures by Mike Shulman. I respectfully ask you to reconsider your decision, irrespective of Mike's= opinion. Best wishes, Andr=C3=A9 Joyal ________________________________ De : homotopytypetheory@googlegroups.com de la part de Chris Kapulkin Envoy=C3=A9 : 11 avril 2022 09:32 =C3=80 : HoTT Electronic Seminar Talks ; Homotopy Type Theory ; c= ategories@mta.ca Objet : [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, 21, and= 28 - HoTTEST Distinguished Lecture Series We are delighted to announce the inaugural HoTTEST Distinguished Lecture Series to be given by Mike Shulman (University of San Diego). The series consists of three lectures which will take place on April 14, 21, and 28 at 11:30 AM Eastern time. The Eastern time zone is now observing daylight saving time, making it UTC-04:00. Each lecture will be one-hour long and will be followed by a 30-minute discussion. The title and abstract are below. The Zoom link is https://zoom.us/j/994874377 Further information, including our Google Calendar and Youtube channel, is available at http://uwo.ca/math/faculty/kapulkin/seminars/hottest.html We are looking forward to seeing many of you there! Best wishes, Carlo Angiuli Dan Christensen Chris Kapulkin * Mike Shulman University of San Diego Towards Third-Generation HOTT In Book HoTT, identity is defined uniformly by the principle of "indiscernibility of identicals". This automatically gives rise to higher structure; but many desired equalities are not definitional, and univalence must be asserted by a non-computational axiom. Cubical type theories also define identity uniformly, but using paths instead. This makes more equalities definitional, and enables a form of univalence that computes; but requires inserting all the higher structure by hand with Kan operations. I will present work in progress towards a third kind of homotopy type theory, which we call Higher Observational Type Theory (HOTT). In this system, identity is not defined uniformly across all types, but recursively for each type former: identifications of pairs are pairs of identifications, identifications of functions are pointwise identifications, and so on. Univalence is then just the instance of this principle for the universe. The resulting theory has many useful definitional equalities like cubical type theories, but also gives rise to higher structure automatically like Book HoTT. Also like Book HoTT, it can be interpreted in a class of model categories that suffice to present all Grothendieck-Lurie (=E2=88=9E,1)-toposes; and we hav= e high hopes that, like cubical type theories, some version of it will satisfy canonicity and normalization. This is joint work with Thorsten Altenkirch and Ambrus Kaposi. -- 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/CAEXhy3MVeK4auqO3MTkjn0JBO0XoqV8k-5RnS%3DOfi%3DVDQv15DA%= 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/QB1PR01MB2948B2FA84E4733851CA50F4FDEF9%40QB1PR01MB2948.C= ANPRD01.PROD.OUTLOOK.COM. --_000_QB1PR01MB2948B2FA84E4733851CA50F4FDEF9QB1PR01MB2948CANP_ Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
To the organisers of the HoTT= EST Distinguished Lecture Series:
= Carlo Angiuli,
Dan Christensen
Chris Kapulkin


I am very disappointed you have cancelled the lectures by Mike Shulman.
I respectfully ask you to reconsider your decision, irrespective of  M= ike's opinion.

Best wishes,
Andr=C3=A9 Joyal
De : homotopytypetheory@goo= glegroups.com <homotopytypetheory@googlegroups.com> de la part de Chr= is Kapulkin <k.kapulkin@gmail.com>
Envoy=C3=A9 : 11 avril 2022 09:32
=C3=80 : HoTT Electronic Seminar Talks <hott-electronic-seminar-t= alks@googlegroups.com>; Homotopy Type Theory <homotopytypetheory@goog= legroups.com>; categories@mta.ca <categories@mta.ca>
Objet : [HoTT] M. Shulman, Towards Third-Generation HOTT, April 14, = 21, and 28 - HoTTEST Distinguished Lecture Series
 
We are delighted to announce the inaugural HoTTEST= Distinguished
Lecture Series to be given by Mike Shulman (University of San Diego).
The series consists of three lectures which will take place on April
14, 21, and 28 at 11:30 AM Eastern time. The Eastern time zone is now
observing daylight saving time, making it UTC-04:00.

Each lecture will be one-hour long and will be followed by a 30-minute
discussion. The title and abstract are below.

The Zoom link is

  https://zoom.us/j/994874377<= /a>

Further information, including our Google Calendar and Youtube
channel, is available at

  http://uwo.ca/math/faculty/kapulkin/seminars/hottest.html

We are looking forward to seeing many of you there!

Best wishes,
Carlo Angiuli
Dan Christensen
Chris Kapulkin

*

Mike Shulman
University of San Diego

Towards Third-Generation HOTT

In Book HoTT, identity is defined uniformly by the principle of
"indiscernibility of identicals". This automatically gives rise t= o
higher structure; but many desired equalities are not definitional,
and univalence must be asserted by a non-computational axiom. Cubical
type theories also define identity uniformly, but using paths instead.
This makes more equalities definitional, and enables a form of
univalence that computes; but requires inserting all the higher
structure by hand with Kan operations.

I will present work in progress towards a third kind of homotopy type
theory, which we call Higher Observational Type Theory (HOTT). In this
system, identity is not defined uniformly across all types, but
recursively for each type former: identifications of pairs are pairs
of identifications, identifications of functions are pointwise
identifications, and so on. Univalence is then just the instance of
this principle for the universe. The resulting theory has many useful
definitional equalities like cubical type theories, but also gives
rise to higher structure automatically like Book HoTT. Also like Book
HoTT, it can be interpreted in a class of model categories that
suffice to present all Grothendieck-Lurie (=E2=88=9E,1)-toposes; and we hav= e
high hopes that, like cubical type theories, some version of it will
satisfy canonicity and normalization.

This is joint work with Thorsten Altenkirch and Ambrus Kaposi.

--
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/CAEXhy3MVeK4auqO3MTkjn= 0JBO0XoqV8k-5RnS%3DOfi%3DVDQv15DA%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/QB1PR01MB2948B2FA84E4= 733851CA50F4FDEF9%40QB1PR01MB2948.CANPRD01.PROD.OUTLOOK.COM.
--_000_QB1PR01MB2948B2FA84E4733851CA50F4FDEF9QB1PR01MB2948CANP_--