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.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,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 13462 invoked from network); 14 Apr 2022 08:33:02 -0000 Received: from mail-wr1-x439.google.com (2a00:1450:4864:20::439) by inbox.vuxu.org with ESMTPUTF8; 14 Apr 2022 08:33:02 -0000 Received: by mail-wr1-x439.google.com with SMTP id z16-20020adff1d0000000b001ef7dc78b23sf722293wro.12 for ; Thu, 14 Apr 2022 01:33:01 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=from:to:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language :mime-version:x-original-sender:x-original-authentication-results :reply-to:precedence:mailing-list:list-id:list-post:list-help :list-archive:list-subscribe:list-unsubscribe; bh=jyLElrFD3Nz8wfy9M92BVT/fe+q8JCjzllIF6YCLfiA=; b=KJie5XGeGeKvrVILOLXMbpKlKOQxniUuwCKjQUmCLsXR8LxI/casp9tCFD5B+0rajB xjdnnCZdLDRk8hV9LrBzemABmPvAGHVnCQRinacg2usRksGRtsiVD+Rxq9WPUuaf8GXp IT8JcuqYhGeu1pFIeHirUDVGBZkziPiTnAGje3PDWd0xuqVgPC+uV/BusHmLF1DPxDhW tS/SkknTbembkqyaWdZJxclckGNgT/x4+8cCkHlRM1V2DeEEC7427blZHbe8pTxouYN8 pgrMZMt4ZXjexbUvVQ9FWQtMgZYeTvWUna5EUbanDYi7zV/1TCd3jfDSvRaCPE4Ng9op 19Dg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:from:to:subject:thread-topic:thread-index:date :message-id:references:in-reply-to:accept-language:content-language :mime-version:x-original-sender:x-original-authentication-results :reply-to:precedence:mailing-list:list-id:x-spam-checked-in-group :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=jyLElrFD3Nz8wfy9M92BVT/fe+q8JCjzllIF6YCLfiA=; b=z/CH5+iRB/tyyyv+fKcZk65iziO9A5sj5cxamdqlYtR0bJL5Xvo5j1I3z9rT/7zEQB ZcS2lYzo/olKI5lMivYI3gAudoez0655tJT/cusjWRjTVFQMsM/kImdw4Qw55ivko35C Nkq6SiMyktD2Wn8dkSvzMNikPGasJe7S2nDb9IGB529tAzAgxt7n/KX5XZx3lGdDHKO3 pvMXuIhPZXt/ZwFwVBkL6o8EfG13DrJZuvKmI/lpfRcySwuPj1ZzJHOpVfoM3VuUWd9u MzWxGdtPsHierhjRzwskQ2kMrwVTPO9A9vItbmCRfxZazajNWVO9bqlm4THBsXnVZUTK xABQ== X-Gm-Message-State: AOAM53205smNuDZHwHdLsmtQYPatml8Cxq+4KF54+GZV6ZIcVR6kti0O BpnX4SCTmBYcpinpgVLyihI= X-Google-Smtp-Source: ABdhPJz7BVRSjCEwZfJtqIwErv8/N36Gg0oOhcqAz175PIK/ban5H1Y9y4PEmNvb/7hWZ+F+OVgV0A== X-Received: by 2002:adf:8122:0:b0:1e7:b111:3b92 with SMTP id 31-20020adf8122000000b001e7b1113b92mr1233691wrm.695.1649925179512; Thu, 14 Apr 2022 01:32:59 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6000:1d8c:b0:207:aa22:e989 with SMTP id bk12-20020a0560001d8c00b00207aa22e989ls1331947wrb.1.gmail; Thu, 14 Apr 2022 01:32:57 -0700 (PDT) X-Received: by 2002:a05:6000:18cb:b0:207:8c65:3fd4 with SMTP id w11-20020a05600018cb00b002078c653fd4mr1218719wrq.131.1649925177533; Thu, 14 Apr 2022 01:32:57 -0700 (PDT) Received: from uidappmx02.nottingham.ac.uk (uidappmx02.nottingham.ac.uk. [128.243.43.125]) by gmr-mx.google.com with ESMTPS id l20-20020a05600c1d1400b0038e5649eef4si79700wms.2.2022.04.14.01.32.57 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Thu, 14 Apr 2022 01:32:57 -0700 (PDT) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 as permitted sender) client-ip=128.243.43.125; Received: from uidappmx02.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 23FC62E851B_257DC39B; Thu, 14 Apr 2022 08:32:57 +0000 (GMT) Received: from smtp3.nottingham.ac.uk (smtp3.nottingham.ac.uk [128.243.44.55]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by uidappmx02.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id 143CB2EDDCF_257DC38F; Thu, 14 Apr 2022 08:32:56 +0000 (GMT) Received: from uiwexedg02.ad.nottingham.ac.uk ([10.159.172.14]) by smtp3.nottingham.ac.uk with esmtp (Exim 4.94.2) (envelope-from ) id 1neuuN-0000HO-QY; Thu, 14 Apr 2022 09:32:55 +0100 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) by mail.nottingham.ac.uk (10.159.172.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.2375.17; Thu, 14 Apr 2022 09:32:55 +0100 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) by UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.2375.17; Thu, 14 Apr 2022 09:32:55 +0100 Received: from UiWexEDG01.ad.nottingham.ac.uk (10.159.172.13) by UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256) id 15.1.2375.17 via Frontend Transport; Thu, 14 Apr 2022 09:32:55 +0100 Received: from EUR05-AM6-obe.outbound.protection.outlook.com (128.243.226.54) by mail.nottingham.ac.uk (10.159.172.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.2375.17; Thu, 14 Apr 2022 09:32:55 +0100 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=V4k/KPEymJjAgVjXm0HVeYxvhWMa4boI87VS0sIZYwqCRAkva8yx6Ri36873UdEzyZ0gm7wLZVQCVqE4+QsRE3zaEWjYiuLwLqUVNfsQZluVDIIZDCHWIt3vAj287/+7rSGCw37Hq/5qIG47RcnAdUgFYFNgXTgGbmXEWdxrSdb9Gtm8GGrBl5TYN6aeEBaWDDmG/u02ZFby+CJOLppU9Ci3HW0IMPuA5gnA5M0Vm7m1ylI39jgi25T3/+k8A+uh4vL5Ji9p8cSY7EBzCExweiaDNbr2XjVKgFGWvj7ZqmqV0pz9LNMXr93XfHhkjKdVNCnxvAPCEzM2tVQbSWYUfg== 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=TdcpbZBOcw86YxHXPotC2cO4BhV0zArLOMf9sVzP2/Q=; b=Hib8NmAvdh1jMhfQiiZ6DxndzjgMlK3o4iAeAriYFMhsS2BOy9uTlBH3zlGI8Fuv8/BLUso/jjJLEE8T3Y2teLJZNGvtkNbdIu4FVFIziGQ2RiwBSqMWik3IRddOMCLdQ+Iuevdb7c1cSCV1zJcIt7K4HkHx8I4gly2b7Kk0Fj1Mf25md44OdRqTTNFjpwBsk9bzk/L8SHBMGR2arbPHgHZgcZ+XRe7z/M4tbOS0WpIjshx5Ci/3GA7wUn6c6VJpJYg9ia2UJIYZwBDdFmftLD7mE1g5agZM3E7A9N4ZeXmuBXxhD3ChRZg9nYv02ZQvHgE9faLXDoQKOK8tutvnJw== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=exmail.nottingham.ac.uk; dmarc=pass action=none header.from=exmail.nottingham.ac.uk; dkim=pass header.d=exmail.nottingham.ac.uk; arc=none Received: from PAXPR06MB7869.eurprd06.prod.outlook.com (2603:10a6:102:1a0::20) by HE1PR06MB4060.eurprd06.prod.outlook.com (2603:10a6:7:9d::21) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.5144.29; Thu, 14 Apr 2022 08:32:52 +0000 Received: from PAXPR06MB7869.eurprd06.prod.outlook.com ([fe80::19a2:5206:ca9c:f1c7]) by PAXPR06MB7869.eurprd06.prod.outlook.com ([fe80::19a2:5206:ca9c:f1c7%7]) with mapi id 15.20.5164.020; Thu, 14 Apr 2022 08:32:52 +0000 From: "'Thorsten Altenkirch' via Homotopy Type Theory" To: Chris Kapulkin , HoTT Electronic Seminar Talks , Homotopy Type Theory , "categories@mta.ca" Subject: Re: [HoTT] Re: M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series Thread-Topic: [HoTT] Re: M. Shulman, Towards Third-Generation HOTT, April 14, 21, and 28 - HoTTEST Distinguished Lecture Series Thread-Index: AQHYT578aNOwiGmZu0+T/N8mELZjBqzvFRST Date: Thu, 14 Apr 2022 08:32:52 +0000 Message-ID: References: In-Reply-To: Accept-Language: en-GB, en-US Content-Language: en-GB X-MS-Has-Attach: X-MS-TNEF-Correlator: x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: c382be3c-d11d-4ec5-08de-08da1df15e00 x-ms-traffictypediagnostic: HE1PR06MB4060: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: oW9TnGJ0MM1wier7qfXDyvMCIyAxruAFILgL/5py6JYj3oEcqV5GOieZCB7CrA6Imf1ug3U8wwx5hkG+r3VXI9iBiF+fgpSaRHVPOapF1pw2o2jpsErilrxtf/amuldqOzlxEkKDjFMPVUBGKhlJvYxdMmiLF7rHPspX5mwx0cZccQgAeVT0mTAmuxM25ufEP8e3l8/uwzf7h5yMwzD1lBCsuF08U1JNZ4I9CMT8N73A3djkmIsf7KsF9Ylct/hHDpUKEYSxJczf6w+zcRWUPLKpdttUIf5ildzWTuvphnc35II9cVeTgN5anWGwlVtxbjXHobIWeRPJAMxExn4N2P1XurXNcJYXhV6mLpmm47c230jJokbNJzbEDohPJ2jbTZ0VFwmt3mbM3VtzEDV8hLO6BdnBl4IXEmprukybVIwglYqjJSkhugsKSQ3fGS0PWhgkJT5y8jsQgrj6yfwvahs6fobioHb2j1o8aF3kYU6B/66zXKUsAIkNPn/1YNhD4PDxv/kg95ofeDG5Orxt8piCH+ZpxlvkSvijgMu9zrhOVVfUU07HLZLNKQmp7S54oEvWW2tMBpKLTPClUfgyzJHw+ic0K0sBB05vItc4uBVgxL5wt4u8LrawoNtATfdaumgkAx3XHQ6JdHNFQIoeapPrmdoQON2tFKLhOc5oLfLQc4+ycqW7PdQynGzvYcLT+p5mrRzFl/PLJqg5LYEmH6c5yqI57IVIjhKZiamu6xNVA/Dsc5kPUi0KCUbSnvqrG++Z3CmnxBfdB9rDmwErmog/2Uz795daWvS9lMejTVWEYSmyUJ80wwNLWKHB8UZe x-forefront-antispam-report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:PAXPR06MB7869.eurprd06.prod.outlook.com;PTR:;CAT:NONE;SFS:(13230001)(366004)(9686003)(508600001)(21615005)(9326002)(8936002)(86362001)(166002)(53546011)(2906002)(966005)(7696005)(6506007)(122000001)(55016003)(38100700002)(52536014)(33656002)(5660300002)(26005)(186003)(83380400001)(91956017)(66946007)(66476007)(76116006)(38070700005)(110136005)(786003)(66446008)(66556008)(8676002)(64756008)(71200400001)(316002)(10090945011);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata-chunkcount: 2 x-ms-exchange-antispam-messagedata-0: =?iso-2022-jp?B?TmNGSG5uZmdEUjJuZW1DeTZkaXk2RVA0OEVrd0dvdUxDc2p6YUJBTGhR?= =?iso-2022-jp?B?c2V5a3NqR0FvK3pDK3VURnVWNGtTRWtuMDRTWTNLSDZnQ3JydWhJdm1U?= =?iso-2022-jp?B?elprWVVmdWlGRys3RnlPMVlvL1FFbjE1TjZ1ekU3Um5LejJ2V0Rmd2lq?= =?iso-2022-jp?B?TnFxcEtDS3FnSTY5c1Q4bXZHc0Z1VmVNNHBWaDFDMmlIMXNhZExvaW5B?= =?iso-2022-jp?B?TXhnVER2RGQ0RmhFVzdjZ1VFTEh1M0JCbk9yUzhKelZxMWRaT2VkNjh3?= =?iso-2022-jp?B?MFg2U2dDWm1BM3J5MHFKalc1amdGZkttUFN5T0ZVNVVteDFJWXZ1RVM1?= =?iso-2022-jp?B?djlDdWFaMjlYU3ZhNm9jSnkxdEdKOE5VdEtiRkIzNHVHLytWbFhBZnhs?= =?iso-2022-jp?B?K0w3M0UyWFRpV29OcDVKWWZnQkFodmd4ZG9BTE1rbXd1ZmxCQVVLalFL?= =?iso-2022-jp?B?Q1NONTFhaUNCOHgxTWJTOG5lWXEwZFRPRHJOcWdscStXVUYvditpajB2?= =?iso-2022-jp?B?aEcvZ0JCU05COVgxNW1ybFNFbnRNWnBLT2lZZEE0dVNiNUUyMFpjd21C?= =?iso-2022-jp?B?RmtnNlU2U0VqbHgrWG5nVUIzSFRWUmp3eWVMWjIxNlhUTytsRWpIN2hV?= =?iso-2022-jp?B?UDBMWHdpT0t5U2tZSkkzKy84ekExeUo5NmFhYldOTWdaQ1k0SjN3OGlM?= =?iso-2022-jp?B?enUxU2RqZWlBTTVXaDVxS3FEbThyY1prTnJTd2tHL095SElsaUFNTEwv?= =?iso-2022-jp?B?Z2NyR3FOb1pzNmdROWR1VzJGcjRiRkIrY3lCT1plTk9WNnYzcHpwREF5?= =?iso-2022-jp?B?MDByNldqVk9TY3FzS2s5cnJKSllwdm5HSHlTdXFEUGNPNmo3ZXdxdmVN?= =?iso-2022-jp?B?alRSS0ZIWnBUNlQ2c3hjZjdwOU1tM3kvYnVBeEwra2tOQTZmdmk2eVFC?= =?iso-2022-jp?B?c2t1UE1pUGFOZHErTVRoQUgzQWpZaGo3elc0VFd5MVNyVURsUExrMHl6?= =?iso-2022-jp?B?RFV1TWEvb0JzT3JmRTVhRTk5aE4xOWRxV2laZ1h1NHVCY1FJUHBsZjgz?= =?iso-2022-jp?B?R0hWV1h1ZEloWkxMTm1QY05CRmpJYnVldXM4aVVUZUJmOWU2bWs0SWpt?= =?iso-2022-jp?B?VXZPN244aTdjUk9JOEJjaVRONTJKTTBHbEhOZHdmSE9PMGJHYUJsVmt2?= =?iso-2022-jp?B?VUdVWU14ZDVGUVNpejMxV2I2TXNGTXFpZGZEN2l4cGFROHo2Zk5DQ0dJ?= =?iso-2022-jp?B?YVRsOWhKdWZQM2dCWHVmZ1IveExVY0UxUzlUS1c0a09qRVJuSlZnRXlV?= =?iso-2022-jp?B?a1J5YlREam9OMWZyL1A1Z1ZFckpGbHpZd1lpN3BFY1JscUlRSWFzY1pq?= =?iso-2022-jp?B?aGFkTXR4bGd4TkdBOEJsNGlzZW1td1AvZkNVdWU2TVNjODdQM1YrTS8w?= =?iso-2022-jp?B?VDJCQm43N2cvS3orRjdrL2Z3NEhHb0pnVWFWcC9EbnlhUTRZTVFaNUFC?= =?iso-2022-jp?B?NGJiOXVQd3g3QUVCR0pIeVJFWTRMNDhxV3NyNGpranV3Mys3dXZEUWpx?= =?iso-2022-jp?B?dDZ6UlNCM3dpSlJLSzRnclFEUUJIV0tkSFA0N2VzRSt6b2VlOEViazhU?= =?iso-2022-jp?B?QytLdEUveVMxWlB5OEY0ZFl2M1NZdHdsZGU1QnhCcGdiUzNpaU1SMUdu?= =?iso-2022-jp?B?VzN2b2o2ZnFqVmlIM3R6THI0TEhVeDhWY3dsYVhwcFVwbHFmaDZlY0dL?= =?iso-2022-jp?B?NkNOVVhxRlV2SEV4MzM0UW1YaUQ4VFZrcUx0UU1Hb3VtZlRuMVNTbXF2?= =?iso-2022-jp?B?dnMra3ZtajRqU09JM1Z4QWgxTC9SQ1JVUFcyYkU3SjMyWE0xejMrdHFn?= =?iso-2022-jp?B?SEU2SzIrTUJ3Ynk3YVUyQmtmdjZ0YU5Tay9wZXJuVDl1REdRRG9RYWpH?= =?iso-2022-jp?B?UjJ1ZkJZNFlGUlQ4WUgyc3pqenJVTFI1TlpGSEhNV29CNjA3UTBnMzlx?= =?iso-2022-jp?B?YU4wLzE0Q1h3SXZEZDVSMkVMdDA3d0taVHJlOXRoVWtWVHhQWWprODFj?= =?iso-2022-jp?B?M055ekxWUDFiRGxOT3dNZGQvaWU3U3RLcE9NZkhiNnJOVU50RUFQRkww?= =?iso-2022-jp?B?VEd3UGQ5L3Juc0ZnLzR1bldiNXQvb3hqSkoyVmVvY2lnQzFrMnFpcmM5?= =?iso-2022-jp?B?NklOUFRVYStTZjgwNUhjTW8zbExxcWtGemJ2eUFqUjlQSG4zU2c5Ukp4?= =?iso-2022-jp?B?VFFNTnJLS1YrbjBUU2hOSnduNmRJelFJYWpHWG1ZWXRGNXlKbGpwM1Fs?= =?iso-2022-jp?B?S2dSRmt2aExEUCtPNVhqTGRrbE43dlE0b2QzTGp0cjRURG5oNXBTWXRh?= =?iso-2022-jp?B?cEtvNG1iUFFtVFVMUzJpT1N4WmpFREJQeDUzTkZiU25ySlNaWlJqcWpa?= =?iso-2022-jp?B?UExyc1pnekRsYmVmSVdDOWtLUy9rdStGbHpHckRxdkc1US8vTnlrQy9D?= =?iso-2022-jp?B?dnZEamszaElZbGxVQmxLR2x1NmFWV3hnaUdBeENsOGVxS1YzUkN2SFU0?= =?iso-2022-jp?B?dkxYRHJVaVFrYUpGYTdRR0t6R1FJN0syQU1BQkYwVjF5TUp5?= x-ms-exchange-antispam-messagedata-1: dPpF+HdkVJvL/A== Content-Type: multipart/alternative; boundary="_000_PAXPR06MB78693E007AE2B907EE128D6ACDEF9PAXPR06MB7869eurp_" MIME-Version: 1.0 X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-AuthSource: PAXPR06MB7869.eurprd06.prod.outlook.com X-MS-Exchange-CrossTenant-Network-Message-Id: c382be3c-d11d-4ec5-08de-08da1df15e00 X-MS-Exchange-CrossTenant-originalarrivaltime: 14 Apr 2022 08:32:52.3668 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: qAmSKMQCfWNreGdV11wPxhacesoH3rUlkRilMDyKHXV+Fb/e06QHVISgudmUKtH7BW7MIiWEjFSDaO7nz7gmz9pNaRKYoSlFe0roPhN70nZye4eZlfLrTPg/8WUKTcw6 X-MS-Exchange-Transport-CrossTenantHeadersStamped: HE1PR06MB4060 X-OriginatorOrg: exmail.nottingham.ac.uk X-SASI-RCODE: 200 X-Original-Sender: thorsten.altenkirch@nottingham.ac.uk X-Original-Authentication-Results: gmr-mx.google.com; arc=fail (body hash mismatch); spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=QUARANTINE sp=NONE dis=NONE) header.from=nottingham.ac.uk X-Original-From: Thorsten Altenkirch Reply-To: Thorsten Altenkirch 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_PAXPR06MB78693E007AE2B907EE128D6ACDEF9PAXPR06MB7869eurp_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi, Was this necessary? I don=E2=80=99t agree with Mike=E2=80=99s views on tran= sgender issues but this has nothing to do with the topic of the seminar. Ma= ybe he should have refrained on expressing them in the context of the HoTT = book but maybe it is not good if people can=E2=80=99t say what they think e= ven if we don=E2=80=99t agree with it. In the end cancelling the seminar is water on the mills of certain right wi= ng people who will see this as yet another example of =E2=80=9Ccancel cultu= re=E2=80=9D. Maybe you felt that you needed to cancel it to avoid it to get= hijacked to discuss topics which have nothing to do with the topic but the= n you should have said this. Cheers, Thorsten From: homotopytypetheory@googlegroups.com on behalf of Chris Kapulkin Date: Thursday, 14 April 2022 at 02:28 To: HoTT Electronic Seminar Talks , Homotopy Type Theory , catego= ries@mta.ca Subject: [HoTT] Re: M. Shulman, Towards Third-Generation HOTT, April 14, 21= , and 28 - HoTTEST Distinguished Lecture Series The organizers of the HoTT Electronic Seminar Talks are committed to the diversity and growth of homotopy type theory, and want everybody to feel comfortable and welcome in our community. We believe the speaker=E2=80=99s recent statements in the context of the Ho= TT Book stand in opposition to these values, and have made the difficult decision not to hold the upcoming HoTTEST Distinguished Lecture Series. Carlo Angiuli Dan Christensen Chris Kapulkin On Mon, Apr 11, 2022 at 9:32 AM Chris Kapulkin wrote= : > > 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 h= ave > 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/CAEXhy3Pjt4%3Dwi5ikinGTqkKXyQKQ6iWOCtyTjz%3DBc1zufLz-AQ%= 40mail.gmail.com. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment.=20 Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored=20 where permitted by law. --=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/PAXPR06MB78693E007AE2B907EE128D6ACDEF9%40PAXPR06MB7869.e= urprd06.prod.outlook.com. --_000_PAXPR06MB78693E007AE2B907EE128D6ACDEF9PAXPR06MB7869eurp_ Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

Hi,<= /o:p>

&nbs= p;

Was this = necessary? I don=E2=80=99t agree with Mike=E2=80=99s views on transgender i= ssues but this has nothing to do with the topic of the seminar. Maybe he sh= ould have refrained on expressing them in the context of the HoTT book but maybe it is not good if people can=E2=80=99t say what= they think even if we don=E2=80=99t agree with it.

&nbs= p;

In the en= d cancelling the seminar is water on the mills of certain right wing people= who will see this as yet another example of =E2=80=9Ccancel culture=E2=80= =9D. Maybe you felt that you needed to cancel it to avoid it to get hijacked to discuss topics which have nothing to do with the top= ic but then you should have said this.

&nbs= p;

Cheers,

Thorsten<= o:p>

&nbs= p;

&nbs= p;

&nbs= p;

From: homotopytypetheory@googlegroups.com <= homotopytypetheory@googlegroups.com> on behalf of Chris Kapulkin <k.k= apulkin@gmail.com>
Date: Thursday, 14 April 2022 at 02:28
To: HoTT Electronic Seminar Talks <hott-electronic-seminar-talks@= googlegroups.com>, Homotopy Type Theory <homotopytypetheory@googlegro= ups.com>, categories@mta.ca <categories@mta.ca>
Subject: [HoTT] Re: M. Shulman, Towards Third-Generation HOTT, April= 14, 21, and 28 - HoTTEST Distinguished Lecture Series

The organizers of the H= oTT Electronic Seminar Talks are committed to
the diversity and growth of homotopy type theory, and want everybody
to feel comfortable and welcome in our community.

We believe the speaker=E2=80=99s recent statements in the context of the Ho= TT
Book stand in opposition to these values, and have made the difficult
decision not to hold the upcoming HoTTEST Distinguished Lecture
Series.

Carlo Angiuli
Dan Christensen
Chris Kapulkin

On Mon, Apr 11, 2022 at 9:32 AM Chris Kapulkin <k.kapulkin@gmail.com>= wrote:
>
> We are delighted to announce the inaugural HoTTEST Distinguished
> Lecture Series to be given by Mike Shulman (University of San Diego).<= br> > 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<= br> > 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 r= ise to
> higher structure; but many desired equalities are not definitional, > and univalence must be asserted by a non-computational axiom. Cubical<= br> > 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<= br> > 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<= br> > definitional equalities like cubical type theories, but also gives
> rise to higher structure automatically like Book HoTT. Also like Book<= br> > HoTT, it can be interpreted in a class of model categories that
> suffice to present all Grothendieck-Lurie (=E2=88=9E,1)-toposes; and w= e have
> 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/CAEXhy3Pjt4%3Dwi5ikinG= TqkKXyQKQ6iWOCtyTjz%3DBc1zufLz-AQ%40mail.gmail.com.


This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.=20

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored=20
where permitted by law.

--
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/PAXPR06MB78693E007AE2= B907EE128D6ACDEF9%40PAXPR06MB7869.eurprd06.prod.outlook.com.
--_000_PAXPR06MB78693E007AE2B907EE128D6ACDEF9PAXPR06MB7869eurp_--