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,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 14414 invoked from network); 3 Oct 2022 20:14:57 -0000 Received: from mail-wr1-x43a.google.com (2a00:1450:4864:20::43a) by inbox.vuxu.org with ESMTPUTF8; 3 Oct 2022 20:14:57 -0000 Received: by mail-wr1-x43a.google.com with SMTP id m3-20020adfc583000000b0022cd60175bbsf3332856wrg.6 for ; Mon, 03 Oct 2022 13:14:57 -0700 (PDT) ARC-Seal: i=3; a=rsa-sha256; t=1664828096; cv=pass; d=google.com; s=arc-20160816; b=WLXayQXH8cKgVkWHdLpi7XdKpNvvExwlsUwTBfpO9MYVc5IksljtmECHEplzwsru1W iXOBK71MbFsAv/vII3C1cnytfFEyNbPFRCmS9zzMBOluFfWNcV+IWUz+sqJYpFFdXjbu +hAaQ6fSy/VRAySdxVpMz6DN+9fB3zCv305WYYJl3wiZw83mr9XyuDhiWxxitEnZQHE0 6rrC0Lk74k9LnyFr5mZ+F3sxMiTwviUP2CflmVoOMBCeEUSyL0EINQe82CdpMFmA9Jk9 /b+XCkBVErlC29g60ej+cVAuQiNXds/BRYf3pHftLpTMfICAZ9oaQzjaSAGyhpxk0/H9 7I+Q== 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:content-id:user-agent:content-language :accept-language:references:message-id:date:thread-index :thread-topic:subject:to:from:sender:dkim-signature; bh=aMdpLBYDtg1lieBvsuI9q/Yr2JjgHV5B0IjnNwaZcWw=; b=NJz30Y7dlQGvbuWJnr3cp46xI3vmvoGXYDm0HdC7vNdxRp9oF8+fkJd/Dcjh7cFLc+ SeNARbmrw2ni9znYPkSuCiL/fcuJpaJ+ANQQiMjIbwd6s2D3BrQKFXtDjrP4UaheF7B8 9C/VOo4IoeM+NoS8j3JEQNSkVzmvRjObVqThRpzWGk7e7h45rbfKa09bWn1Yis0XRSzB b3GhN/OtlcHJjdzkXXeJUM9ULDK+KFArSEAAa1IHR638wfEOtvIKJyeELqb1iOLs7MsD ST35KPCO52JYNXLM070oRysb1BnOO6thfCUKB2lFbdPyhBHpwI2RDMe/UEEwXknVubJc EpVg== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector2-uwoca-onmicrosoft-com header.b=fLOLqoQa; arc=pass (i=1 spf=pass spfdomain=uwo.ca dkim=pass dkdomain=uwo.ca dmarc=pass fromdomain=uwo.ca); spf=pass (google.com: domain of jdc@uwo.ca designates 40.107.115.100 as permitted sender) smtp.mailfrom=jdc@uwo.ca DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; 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:content-id :user-agent:content-language:accept-language:references:message-id :date:thread-index:thread-topic:subject:to:from:sender:from:to:cc :subject:date; bh=aMdpLBYDtg1lieBvsuI9q/Yr2JjgHV5B0IjnNwaZcWw=; b=XH5fPx/fEi7iF9mC64sjxegvG/9E/qE0c2SXLlzimRzVwcbW14MOVWB2zh6hR11932 zBaPBM/AOiHfwFakGFlXdxxC1Ln4xCkbDeXlRl0E0BhtduhWc6M8/dgX0TNbNlx7fbOa Ph5gb7d92gqAwAnVcflsO4FBju4FHR1XpmvqfaOSAvWKm3y9am5UExzX71nWnmaM6+IX ubmu4TR5ynZoAk8u7b0VaLG/tzfJmbmYznc/PZDX2Xhd8qleo1uA1AGJCdII4/XAz+yL xyp20za8g6WUesNlbF+0Uxf/mkBreJlHt3kEsyY5yfyBV6z4Q9BFtPY2JjKZWERH/n9E GEcA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:mime-version :content-transfer-encoding:content-id:user-agent:content-language :accept-language:references:message-id:date:thread-index :thread-topic:subject:to:from:x-gm-message-state:sender:from:to:cc :subject:date; bh=aMdpLBYDtg1lieBvsuI9q/Yr2JjgHV5B0IjnNwaZcWw=; b=XwNfJ/UhS0ZfVruN37QDkzXG2/e0Hhi+pzYbsdGVMMsCoDC8NsvLYJuCX1v3mur+sp JmWXNKRqYCQSybICnTiaTvYjC0IpLUcs0RynmQnEhOGfoeOfzSIR6ASfA01K3CZyL7lx IIpMP4XsGc2YASFJ1Q/GxZv/hZgfeSX13hJE8zQITsN1pBSfB5g0VU/6Aup8aFSIanlc abStawkUoY3WeIhYABJxDKlIGgqAP3f+fUFxhgNMAjCnYKPtxKe7plw6Ydf6KSO2C363 t9n4uzffTWtLXQ2GdYU5VY675aJbHu/eeeRLWnxP4y7nIgfTi3HBSpSz+ZbKgTXu7fZc 2Jvw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ACrzQf3kxJsUUXUBkg8iykNFX74wUlwV/iwtRbHxwZpQ18Ej2B/xPN9R lJ3WQnYVQ1w+BxJ/WWHx+0Y= X-Google-Smtp-Source: AMsMyM4KUNE8p7pIShycSOJ60vs69Nhd8OYVNSTVd+K8B0aIUXl7ljH7OhjyDQLTjz+dp0GAeXx6QA== X-Received: by 2002:a05:600c:1906:b0:3b4:c979:e639 with SMTP id j6-20020a05600c190600b003b4c979e639mr7782690wmq.10.1664828096134; Mon, 03 Oct 2022 13:14:56 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:7714:0:b0:3b4:a307:9032 with SMTP id t20-20020a1c7714000000b003b4a3079032ls5993071wmi.2.-pod-control-gmail; Mon, 03 Oct 2022 13:14:54 -0700 (PDT) X-Received: by 2002:a05:600c:4e94:b0:3b4:b416:46c3 with SMTP id f20-20020a05600c4e9400b003b4b41646c3mr8164635wmq.149.1664828094174; Mon, 03 Oct 2022 13:14:54 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1664828094; cv=pass; d=google.com; s=arc-20160816; b=W8WjnHj2fs/TC7XnxB4NZXrae8scW5Y3kRwNdsVkI7OthAHmPnuKSB+nzbcQPy2aDj 3Qk5DIevq2GzYL35GCbxCb/ATJDwsxklntouLeSIFKa8y1HL2u8cCbqGxTsHJ7i8Y/iQ 6Bu7eNa5/tgg6Kt+QS9le1SOxngR+EHAXSv7BrCHwChwXXIky9ScB5PdjZxBMeIiGiHJ 6cJxO2ErIcbV+ZWMZNxycFMA7RBTXNTz7oI90HqCcg7PyHGz7XHj8rSEYfawCIrAhSsq BMfm1QoLnPMg2E4rTfKlt620hqlqq/JpnDGtbwAOcbnO4V2SpZvr8y5WCuHcwFTlzTNi MGzQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-id:user-agent :content-language:accept-language:references:message-id:date :thread-index:thread-topic:subject:to:from:dkim-signature; bh=twARHA1OcH002aEeahcxASbhlN482O0TbavYJa9SC0I=; b=pNeHHc9AXyvFzfjGL7AxDgdHbHoMWqvd5Pjp0D3oAOMR9xiTvKMNbL8WNXvrKXf8xT EV7i5NO/ejWFGB34l2eIHZick2DajScbk3Wzj81/sXW+DbmkYcLtZ93VJF/oPYwy9dP9 MwgwG1HMn325yhC5946MpRelnZgtbsW+5TLQvwGK2qjVI+xMluR2i5Rub2fGXWWVTJQH tvxyLK3bqSVwKq4EQugobfY3mWssd5bP+ptPzbDfGbDM5AZfWg2huTizFEwnQDWcA2Ib J2IvK0f6tYv2YcpQzhRAZ2Sos0HVv1lWePEH4RcdGLrdelBcTO2VwJ90C2jAB5SiHcEP XyjQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector2-uwoca-onmicrosoft-com header.b=fLOLqoQa; arc=pass (i=1 spf=pass spfdomain=uwo.ca dkim=pass dkdomain=uwo.ca dmarc=pass fromdomain=uwo.ca); spf=pass (google.com: domain of jdc@uwo.ca designates 40.107.115.100 as permitted sender) smtp.mailfrom=jdc@uwo.ca Received: from CAN01-YT3-obe.outbound.protection.outlook.com (mail-yt3can01on2100.outbound.protection.outlook.com. [40.107.115.100]) by gmr-mx.google.com with ESMTPS id y11-20020adffa4b000000b0022c8a1af685si219841wrr.4.2022.10.03.13.14.53 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 03 Oct 2022 13:14:54 -0700 (PDT) Received-SPF: pass (google.com: domain of jdc@uwo.ca designates 40.107.115.100 as permitted sender) client-ip=40.107.115.100; ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=UiOCLHMgM90YIHlr6MtKZPVc7PzZgYovFuy0ogdlcKZU8cH9DtWAkCXkTx2HopeX1Zwe2hiiiAKRSQCyw9VhKIzDyYvyn5AuYJBZYY524Nf9jQzuZH2ybM3YmuKFhlpYwZIhMNPp7/aozGaQIao5BGWClVShw3IDmW2/hCwG4wcPPTFKPJsu3PMzxpUmfr+0aSXgcjEKteoId5hHeUZX1xQ/mZw7CFnxADY05H/xBQ0HxS3arAUOjEpc7eBqGqlCqTSkNIdabqfmfYo8Fm7LQQ3VKjG06N47FsSoMZK/sjFw5N48R3wWmwaEcR6f5UW3PoGh5ig2DdCF+3zfOyYkuQ== 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=twARHA1OcH002aEeahcxASbhlN482O0TbavYJa9SC0I=; b=KBg2Q/RpFuw5hdVGZauVuRLXhKZxhUfPLuBVOzqgALa/Y4tiIP+TQtv50pr0uv4eTuNutPxSdbDH9gdfdjplxwdamNjBgiMn4VQbunmFYuhmIZjPPq7+QInsj4uGRg492nbwP1Jom0jqstedkIZiMVQJPFBw4P7udxPrOu5pmyKkugVgd2pckFSntDaH87iDxtkFk71OIyKl4wFrQmOL4vFoW9t72NrDShbdYgHKtnvg/zKAy+YMUH4cQymZ5Z1nr3EwjSzbaP/3VkScloXLMh//PU3qfl4Oz84kGsIOxHPduIOxXYw2H8u9wveN3gwwY3Iwhffx2XparGh6NB6dgw== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=uwo.ca; dmarc=pass action=none header.from=uwo.ca; dkim=pass header.d=uwo.ca; arc=none Received: from QB1PR01MB2753.CANPRD01.PROD.OUTLOOK.COM (2603:10b6:c00:30::22) by YQXPR01MB6366.CANPRD01.PROD.OUTLOOK.COM (2603:10b6:c01:4d::14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.5676.28; Mon, 3 Oct 2022 20:14:52 +0000 Received: from QB1PR01MB2753.CANPRD01.PROD.OUTLOOK.COM ([fe80::a10e:a9cb:6f51:abd2]) by QB1PR01MB2753.CANPRD01.PROD.OUTLOOK.COM ([fe80::a10e:a9cb:6f51:abd2%4]) with mapi id 15.20.5676.030; Mon, 3 Oct 2022 20:14:52 +0000 From: Dan Christensen To: Homotopy Type Theory , HoTT Electronic Seminar Talks Subject: [HoTT] HoTTEST Event for Junior Researchers starts this week Thread-Topic: HoTTEST Event for Junior Researchers starts this week Thread-Index: AQHY12TLUhnPSRfU/UKqcBCV9F8HtQ== Date: Mon, 3 Oct 2022 20:14:52 +0000 Message-ID: <87k05gaclf.fsf@uwo.ca> References: <87r12c0xdl.fsf@uwo.ca> Accept-Language: en-CA, en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Gnus/5.13 (Gnus v5.13) Emacs/27.1 (gnu/linux) x-ms-publictraffictype: Email x-ms-traffictypediagnostic: QB1PR01MB2753:EE_|YQXPR01MB6366:EE_ x-ms-office365-filtering-correlation-id: 30609011-0d37-4d68-d85a-08daa57bee69 x-ms-exchange-senderadcheck: 1 x-ms-exchange-antispam-relay: 0 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: /Z998u6TlTAEk+aM9450qPArc/VcLmfz6uZ70gc2AFzZOycntB60Bjo8WzMrO2H+wK362lznr9QHuoaSKy7ZivrlnNRXaMHSXs+UyLhr6JB8lfBJ3M5kvZagf+W/uvhEO9T3t2xdlVZzA6HHT8EYDLFLuxRVT/9wByMEroaeeaJ6Xe9uORQ0tkqa5MWtXhjJZBXe3+sdFdkaOXLFDIQnYIR3weFneEdG8fCCJQWGvce1hg1hElHigbuWn8oznQNR5FLu03vWt/AUzcaUVRyenD4pHFWf8YI710vhxYXG8UNot0RypQ6rySrTR89Lkrm+UTWwE4W72PaIZp8TXQGr5K8XXsElhgorAkk+ZKma9bRAMWMeQBLQca4qwZWTx3oH5fMhlbQKIvpgENPM+pGRZgUaXvOvAM/+l18hunm5/8B82BJ6hGn9F84O1IVj33jo44XpbYYzo/xLLa3DIUwcL7c35EatRda0UMP9TQIz1UXzap+v7HlQcnMZYBAK9X9WeuG4VHckk0BVuuhxsgKS21B1hgs99trejF/HRoafduFNDdM1XR9OrB23oRHGBiMSm0goAwqe+gWfGORA93WDjDsaq+6Tws/V6RViCxBDJBVcW105rHCpbSKjbYYavt5rM4OCF3MQ+aUORFD7oOyZcqaOsH5ghHdi8IhngAwzxmWEecBkcs++hnaqI2lUXIap0Ihs5RN9hH8qRYGUpB1RAlYCFoaNJFKUTKPd7YyjjgkN5YyNlAnm8xGVCYCE6uo2QDJKsEkBGIlwSsnwMHjFmDEkghK3lXxUkPmH5vdBhBxWIditJIY8ZM8wNhje7fIaJWiUq9RrMSLSM5jSbE0KuvaxbbyAnXtnf4O23huFgag= x-forefront-antispam-report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:QB1PR01MB2753.CANPRD01.PROD.OUTLOOK.COM;PTR:;CAT:NONE;SFS:(13230022)(4636009)(346002)(39860400002)(396003)(366004)(376002)(136003)(451199015)(41320700001)(5660300002)(86362001)(6506007)(8936002)(41300700001)(6512007)(26005)(38070700005)(38100700002)(122000001)(66574015)(186003)(2616005)(83380400001)(2906002)(316002)(786003)(36756003)(110136005)(71200400001)(478600001)(966005)(8676002)(6486002)(91956017)(450100002)(66476007)(76116006)(64756008)(66446008)(66946007)(66556008)(10090945012);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata-chunkcount: 1 x-ms-exchange-antispam-messagedata-0: =?utf-8?B?K3ByR08vMVFWVy81b0txMUlaSFBqTm51UHFnUVJ3SHBZMStLT1JibEdGemZV?= =?utf-8?B?WEthdk9QNnhJNkpDUkllR3ByMHc2RHM5ODlWajM5K0NOVy83OENTYzZaU0ps?= =?utf-8?B?dWQ5YWVuMWhqalF3RnNwbG9Qc3N3dDlKYm9hSjBkaEdWWUo2K1R6MEFJUHBq?= =?utf-8?B?ZVBpVzZzUHJ3cnFOZzRERFpSbVRCOXZtZEtvSVJSeWE4b2xJbmF4dnE2UytO?= =?utf-8?B?aTFZZXFQVFFRWFdyMmRmSXdvY1dINWoxdXVMa2w4QVcrMVI3VGVBT1JCV2xF?= =?utf-8?B?a1IyZzJiMFBUZW41ZDhCYUE4QVhsdzdXTkZRazNvcHVXM0ZwVXdqU2g1aWR6?= =?utf-8?B?bDRDZktURFZHZlFnTVRwaFVRRHNZUVpzU01vcTAzdHZSWmpRSlhkUE9Vdlh5?= =?utf-8?B?c0pWQk9qZnlTVm84b3JvbWpiSEZtUEFWRTJPY1Vxdk1CaXJKYndQSWtvc2xx?= =?utf-8?B?VDU2NElKQUoxOTQyNVFTRkNiZ1hTd1czUWZIbkNWdzJSREVnMXhyQnliU1dW?= =?utf-8?B?aXlLVW44TnJXU2s1OEtSTWtJU09aTitwbkZtdUp3NUg1T2FlQkQxeTRIYkJ3?= =?utf-8?B?NXR0aWZ1NFZFM29jM0dwV2FWRWJ4cTV3d2owQllmeDBocldJZENGS2JVdXVm?= =?utf-8?B?aE8zaGNPL3NJYlFDUWxxSmM1SC9rclNabGNvcStpN2ovZWJBRG1MRU9FS2xh?= =?utf-8?B?N3YzbWovcGs1N2h4cGF3T3VxcDFSWFVTNWVXZ3NhN2FnSzQ2TCtOYWQ0WnJj?= =?utf-8?B?SC9LdkpOMXdMTXJPcmpQQ3V6UVY0TjhpN1kwRGlzb3p2VXlNanNUUXNzNUFM?= =?utf-8?B?R3ZKeWo4WUxiRExUYk8zV2dIOWFUY0hUZnUwaUJia0Yxa0NMRzJUSHdZK0Nx?= =?utf-8?B?WWdWWFNadGpuSjc4MWk5NklleHB2T3o0WHIvK1BsTTNEdWhOcW9YeFIrNE82?= =?utf-8?B?NEI5dXA0NUxBV2V1d0l4V1F5eWswc3ZWNjJ5TlhwZG1oK0ZYM2ltY3owUjRI?= =?utf-8?B?Y3dSREVxK201dlhCTytNT2VXOXB5emxIVmJLTVJiVDhxdDRuVHpYdDJJVVky?= =?utf-8?B?dkhZdHlhRW4xdUVvYzY0RW9JckRMcDRpd1pyR2dyQlZRWkRUUmJwSUF0Wkh1?= =?utf-8?B?ZXM0eGg2T0VqS0JiTVN1QklaTmZvdEtpY0YwV3YzVW9RRkUwTi9ldXF6R3NN?= =?utf-8?B?OTk4MXJpMkpxNi90MzJEK2dTL3B4WHdweVc3cUNyZXgrZy8yblEvZDVmTW1H?= =?utf-8?B?bDdicHhHb3NwUmhBQTBBY0tFVlF3K1laRXFWeFJnazZzaktYY2x4U3VPVXF3?= =?utf-8?B?MnJXbzZsMjM0MXUrOFN0ZExtbk9ZS3kzQ01YVjZlWXBjaGNnZXRjcEloUEt6?= =?utf-8?B?S3l5bzNoTDZMZVc2SXVubC9zbEt4cGo4ZjBMeXZGWVRrZWgraWM2d3Z2WVFv?= =?utf-8?B?b0ZhamFRUkk3RkN6UGJjQWdvaS9GKzZwZFAwRTQ5R2dzcy9LWDZvRzFkRzNV?= =?utf-8?B?bjVvNEdlWmRxN2RhMUI5enRxYndnK1dnUXpEMzZ6ZnBsczBpblBFaHRFRGto?= =?utf-8?B?cmNzR09aeEdzdll1Zk5jSW5EbzRzRWptY0NuY3hoM1NPT0I3LzJRU2VmMXIw?= =?utf-8?B?ZS9pcmY1WTZSM1orc2RCS1lPMjJHVFlhZzlHS2h4VEZ3ZUtxa2lQTDFWNlRR?= =?utf-8?B?aTk5anlqRWc4R01Dc21zUGR0SVVXQjlnMXRDT0tjVHVqYk9GRHNqVUZYMXFR?= =?utf-8?B?Qk9xNVd4VUJKcVU5Z2ZqNzNHMzhmQjVoUTVod3prQ0Q2SmlLU3JQTExpOG5O?= =?utf-8?B?eWRhSEMrVHQzcU9kdVFJb3VseGNya2xTQzg3cE1jalZDZVFOWUc4TUZzcWUy?= =?utf-8?B?U0NCdENsa0NWT3ZKMWxXcVIvVG42a2xNZHVURFloNnNLeFlUMTBvSTN6ODgw?= =?utf-8?B?dnlBdG1FNU5WZ3llSGxYY3dzSVFoZ2hmYWZ1SDBKVUhoOGJNdHNBSkMwbmVy?= =?utf-8?B?UWtkSTQ1b1hOSmRxYXkxWXFTVnIxUm9GOGkyZ1g3VGlORjV5TnJsQklkZW1N?= =?utf-8?B?M2xXbHpZc2tOcUlPRHdaaVA0R3ZpTzlObEowanhxeWxpNGJzSGpSa3ZOZjlJ?= =?utf-8?Q?J0s3tnpFr5U5iX/8E5Se4rkUP?= Content-Type: text/plain; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-OriginatorOrg: uwo.ca X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-AuthSource: QB1PR01MB2753.CANPRD01.PROD.OUTLOOK.COM X-MS-Exchange-CrossTenant-Network-Message-Id: 30609011-0d37-4d68-d85a-08daa57bee69 X-MS-Exchange-CrossTenant-originalarrivaltime: 03 Oct 2022 20:14:52.5196 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: ad93a64d-ad0d-4ecd-b2fd-e53ce15965be X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: 1+a3t1FBgQmCsnj8/XGJ5Ay2wbG7tCvGUetnW3tvm6+24VD/jQzSYQXqpExbCSNb X-MS-Exchange-Transport-CrossTenantHeadersStamped: YQXPR01MB6366 X-Original-Sender: jdc@uwo.ca X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector2-uwoca-onmicrosoft-com header.b=fLOLqoQa; arc=pass (i=1 spf=pass spfdomain=uwo.ca dkim=pass dkdomain=uwo.ca dmarc=pass fromdomain=uwo.ca); spf=pass (google.com: domain of jdc@uwo.ca designates 40.107.115.100 as permitted sender) smtp.mailfrom=jdc@uwo.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: , The HoTTEST event for Junior Researchers begins this week, on Thursday, October 6 at 11:30am Eastern. Each day will have two 30-minute talks, followed by a discussion in Gather Town. The first two titles and abstracts are below. The Zoom link is https://zoom.us/j/994874377 Please subscribe to our mailing list at https://groups.google.com/forum/#!forum/hott-electronic-seminar-talks for future updates. Further information, including videos and slides from past talks, is at: http://uwo.ca/math/faculty/kapulkin/seminars/hottest.html Dan (On behalf of the HoTTEST organizers: Carlo Angiuli, Dan Christensen, Chris Kapulkin, and Emily Riehl.) --- October 6 11:30 Eastern Am=C3=A9lia Liao=09 Univalent Category Theory Category theory is the study of structure across mathematics. Being a mathematical subject itself, category theory should also encompass the study of its own structural aspects. A promising approach (Gray 1974; Di Liberti & Loregian 2019) is formal category theory: studying the properties of the bicategory of categories which make it possible to study category theory from a structural perspective. A different idea is to approach categories as groupoids with extra structure, something which finds itself naturally at home in HoTT, where "groupoids" are particular types. This approach lends itself particularly well to formalization in a proof assistant. In the context of Cubical Agda, we recap the basic theory of univalent categories (Ahrens, Kapulkin & Shulman 2013) and the move towards higher univalent category theory (Capriotti & Kraus 2017; Ahrens et all 2019), particularly the application of cubical syntax to fibred categories (following Sterling & Angiuli 2021; Ahrens & Lumsdaine 2017). --- October 6 12 Eastern Chris Grossack=09 Where are the open sets? Comparing HoTT with Classical Topology It's often said that Homotopy Type Theory is a synthetic description of homotopy theory, but how do we know that the theorems we prove in HoTT are true for mathematicians working classically? In this expository talk we will outline the relationship between HoTT and classical homotopy theory by first using the simplicial set semantics and then transporting along a certain equivalence between (the homotopy categories of) simplicial sets and topological spaces. We will assume no background besides some basic knowledge of HoTT and classical topology. --=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/87k05gaclf.fsf%40uwo.ca.