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,MSGID_FROM_MTA_HEADER,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 20972 invoked from network); 12 Jun 2020 16:05:02 -0000 Received: from mail-io1-xd3a.google.com (2607:f8b0:4864:20::d3a) by inbox.vuxu.org with ESMTPUTF8; 12 Jun 2020 16:05:02 -0000 Received: by mail-io1-xd3a.google.com with SMTP id c5sf6338407iok.18 for ; Fri, 12 Jun 2020 09:05:01 -0700 (PDT) ARC-Seal: i=3; a=rsa-sha256; t=1591977898; cv=pass; d=google.com; s=arc-20160816; b=D8bDPeU8crDs6gkHJBdCgpoIEejmwHuW4Fs2sUByikXcYHvq4X74PRqhlRpUVkXesu vWkK88uiafxW2U+waFDvBqBYOwgXKlqigGUacekMTK1H9WiB80uRxlYfmK7iMwG+sl4K 9Rv/qkNWFDGz9Wzt1rGxxBv/Ac5Fu9moekXwtpyewMuzue/QTixHUwAORT8ZiC1DP7Kp wu2RhQ5ta4qMNBfecz6T19+2sNG549zHHrL3591juKiznJ5Z+Y1PJpNhTJRL7WGlxIMf pgywqGlqeZTTnK/mPl6yPEO6FcOgu7lzFEUBeSJJ4Mr0WYVGQOBregbMiYCHnpBJv7Up bKnQ== 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 :message-id:date:user-agent:subject:to:from:sender:dkim-signature; bh=kdxeKry8qb9+oSVXTgkOGUmz69TLq1csctRPq2ZYeh0=; b=t8hEe6Rmlj3tQzhjvtIyY1xfxTLa9x13BqE8tKtrH8F1rZeqc9Ur0SCQxP5N1fLQd8 Y0Yw+2xy4/zee+xPm76zCaJwxwm++h3Mxyio4vCovgmYO8XT/6DzGBOKDQtCPKYI58aY WcSf2p+5MfJbe2+1kMzLU70D82RQy+vxhgqeBuZ1N+8hzgXMcMmgmMf8AuOzlQrarJGI mi644bU7XrzBd2SUbaqIcopPQTRYZ+YUCLMVaE7nibrreZmpWPoM7ZPnfF1XugAaacax N85QvfvUGeH8JPJBZACfqNv8+pHXWjGxhXI2b/TGk4LSf/EZKiI5JvHbTa54zlkklvS3 KX8w== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector2-uwoca-onmicrosoft-com header.b=JWEX0Fgd; 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.67.138 as permitted sender) smtp.mailfrom=jdc@uwo.ca DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:subject:user-agent:date:message-id :content-transfer-encoding:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=kdxeKry8qb9+oSVXTgkOGUmz69TLq1csctRPq2ZYeh0=; b=lzgqqfjm1+ZpE/pNmlo6oV/DJz2SvBB6KgksrKG/8mEFwc6emGj1BEkz5XZUFPbiMO OZK/TcYeEaa/LI0lBZmRMuof23b6fRSVNv6fjYvefG0Cv3lqBKT5UrOk7RGfsnx3cJRo nvupRmYGHteEsxuITZp0aeVE39t4ODbZrTEIBkHEBiqk9OMknoovlCH1yjFIwpcRsF+w 1Wc5RU2OsgsvJ6Vi7rwIwvDxJs2M4RhtNO7J0+0eNlFTjhCuDtT+csxMQ1/1us3MZWt3 BqNzzF5OxvDByfVes7M/JpPeB+xQ7cjx6gf6cmn/Kof7CbkcKlHla9R78GsB/ppeb08B i/VQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:subject:user-agent:date :message-id:content-transfer-encoding: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-unsubscribe; bh=kdxeKry8qb9+oSVXTgkOGUmz69TLq1csctRPq2ZYeh0=; b=JqWCO/Ajw/WiqmyjaS1hNlxrZ8uhvf1HjYswXwX37LatrO/9Kag7N2TCg9Qk9Lj+iV sWXF9MuNPlUbrFvhQQu6PIHPudH1uZsqpUjl9/ouYtAIHUAwqkoCslxnb6TkQeM9SvhT ky7DMdoJpvZsGuHvahrCliDR2NGQRPGxyRX/46CXgmAaBjADlBPYAhLkVI9pNpcs/EKw 3IXXq44nQv75d6WDK/iIAfoa2gqe872tHszEtAiQP0M5lbPD+SqeoegbSnQ8hFA9e6eG 5DjgZw9xUjW4yLgBLACeY2I1YOIDOA423WCFUuG6a9xlgDOxaltWSTxq+MzS677IkdLY XK3Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM533thwoW/sZAt5oszJ5hB1uyoosmbqwkXRm+ZqsfRbpBRdB3eBjd hBVZSbcGWeVbe8aOEVqqhVQ= X-Google-Smtp-Source: ABdhPJzhS21EVJzLjp3Mz2ewea9zYi5uQOlWqWQsa8ecsKlrkiH5ZMeZRtvL/nJ4GxLd4Z4OYF4zXQ== X-Received: by 2002:a5e:df49:: with SMTP id g9mr14359392ioq.153.1591977897673; Fri, 12 Jun 2020 09:04:57 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a6b:1453:: with SMTP id 80ls1250728iou.2.gmail; Fri, 12 Jun 2020 09:04:57 -0700 (PDT) X-Received: by 2002:a5e:8e47:: with SMTP id r7mr14316552ioo.204.1591977897237; Fri, 12 Jun 2020 09:04:57 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1591977897; cv=pass; d=google.com; s=arc-20160816; b=0HgIPcm/2o37ZFgbgmheCica/yOb7pz3vm/I0bojbu9Okx1kt1/pFz4t7xfRpprI8w EfDSIX7Rkbd+PsG3AdLt8+tiVSqvDXrqif9oyhzeYSlLacQqO2saZ2JpT+aMMyb5yOgR zYsZ6KRMn1h0GiEDrWIkn0jwfJiBbwmdlLB4o/lFturFGXD9FmnL0XOS7kQ/iUyv4j1y FyA2qx0KTIqGQ6oTWXWwyBL60dME4Vs3wXKwNwJCtnHaWAH/paSMhbTdXSeQvIwH8U1h BSiIQAFOx1u28avvGdpqI3haTfdkZUymDNCA5B028IMqIzrASVSlWVClM6D3+wYY4qS9 Hkeg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:message-id:date:user-agent :subject:to:from:dkim-signature; bh=Uxg1PiuzFjdb8bQN3w4b+djKESyChXPv5zG5UqfWvLI=; b=ISTqzSRvt+Jmj5Qj4is0iqwNh7VgcBHPq3r016G/NNxv2qesW60S4uCI3rW0rJLNuU 3ISjcPRbt4RYDpu9BMbBVmP4dtVvFvY93gpiC3qcN8VSl1JhnxIZTvery9xcNKJnbX3P Iujv1x8WBAfanE3eMBKgay9epxp6T/OmFj7jppgrgmtpzwunKon94x2dJsroB2pAtsIL vr7aaWx7xv9sjq76+2RARXrTFVyTh0zlYZSkT0BDSZNijSchUQ4h5CSlh2UBwsIB3C+S GU5+kfqErQsaZU3ODN25cgkzInkX4BO9M+ZXwqHGcrw0jbfzIenDMbTMwI9Sp+Dz9l8c RxcA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector2-uwoca-onmicrosoft-com header.b=JWEX0Fgd; 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.67.138 as permitted sender) smtp.mailfrom=jdc@uwo.ca Received: from CAN01-TO1-obe.outbound.protection.outlook.com (mail-eopbgr670138.outbound.protection.outlook.com. [40.107.67.138]) by gmr-mx.google.com with ESMTPS id z17si426270iod.1.2020.06.12.09.04.56 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Fri, 12 Jun 2020 09:04:56 -0700 (PDT) Received-SPF: pass (google.com: domain of jdc@uwo.ca designates 40.107.67.138 as permitted sender) client-ip=40.107.67.138; ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=kLuWqxTJ12/JLWXr1NyFaMdn/JAFe+cyP0LDaVPLJYS6ZK6DMiJThHqLfqvBm8PDgvRxXG1IJkO87QHyX4Qa4TTIPc38YULhi+65rAvlClsCDE4sPhupg7/YJcw2rWgo1w2uHaQCk0oUuH6m80qM/fFOq1nR6AHTBFM1HMtUxDySY4wSZAt3ydR1xtnTJspqc/c1Q9To0fXOl5tgfa9qeO+eFlv566HArJRildApb5WY05LsM1UGaOLyLuFrFj6gVuoM613Gm4qW/+0pvk5buqM6RNEXXBiAmXGhLWeALVvGOZgQ/ySqPZ59NVmRlVyrayHtY+aL9JZS9yPP/Fu+Jw== 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-SenderADCheck; bh=Uxg1PiuzFjdb8bQN3w4b+djKESyChXPv5zG5UqfWvLI=; b=bokQTE0FVDO/HXop68AgcTakCVUIT3uqxmrXn+sZF2QhtZez+YM/UorKHe/I7npOeRW4QJ7B/p2UyWLXTM/DM+ST251vVhvjw345E15y/AxnqRsDkhFdBQ89FCcefxLj8wj/AzP3jQyp3jBDpjFdGV8ASNf9votn82KCu4lieKYckAZlL1UhuA7Umv8HxprqPKwXuQbYKm+7HpFTL7avez+/CfT+1r8Ovj9FsjxK/5Ic1JJRxNuS4enlr9B7fGqDrIfc+iQLhAqFfscukznzNWKhwaEsebvIHalC/4Dan6bEKRepm6yGebJZcug84hdxiKNGi3iZWS6z6G3UAulnRA== 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 YTOPR0101MB2204.CANPRD01.PROD.OUTLOOK.COM (2603:10b6:b00:24::25) by YTOPR0101MB1756.CANPRD01.PROD.OUTLOOK.COM (2603:10b6:b00:18::10) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.3088.21; Fri, 12 Jun 2020 16:04:55 +0000 Received: from YTOPR0101MB2204.CANPRD01.PROD.OUTLOOK.COM ([fe80::c5b2:dac5:315e:74d5]) by YTOPR0101MB2204.CANPRD01.PROD.OUTLOOK.COM ([fe80::c5b2:dac5:315e:74d5%4]) with mapi id 15.20.3088.019; Fri, 12 Jun 2020 16:04:55 +0000 From: Dan Christensen To: HomotopyTypeTheory@googlegroups.com Subject: [HoTT] The HoTTEST Conference of 2020, June 15-19 (homotopy type theory) User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux) Date: Fri, 12 Jun 2020 12:04:54 -0400 Message-ID: <875zbw1d95.fsf@uwo.ca> Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-ClientProxiedBy: YQBPR01CA0026.CANPRD01.PROD.OUTLOOK.COM (2603:10b6:c01::34) To YTOPR0101MB2204.CANPRD01.PROD.OUTLOOK.COM (2603:10b6:b00:24::25) MIME-Version: 1.0 X-MS-Exchange-MessageSentRepresentingType: 1 Received: from speedy (99.244.22.253) by YQBPR01CA0026.CANPRD01.PROD.OUTLOOK.COM (2603:10b6:c01::34) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.3088.21 via Frontend Transport; Fri, 12 Jun 2020 16:04:55 +0000 Received: by speedy (Postfix, from userid 1000) id 7BA0C4C0105; Fri, 12 Jun 2020 12:04:54 -0400 (EDT) X-Originating-IP: [99.244.22.253] X-MS-PublicTrafficType: Email X-MS-Office365-Filtering-Correlation-Id: e2499038-0fc8-4fa4-acda-08d80eea591a X-MS-TrafficTypeDiagnostic: YTOPR0101MB1756: X-Microsoft-Antispam-PRVS: X-MS-Oob-TLC-OOBClassifiers: OLM:7219; X-Forefront-PRVS: 0432A04947 X-MS-Exchange-SenderADCheck: 1 X-Microsoft-Antispam: BCL:0; X-Microsoft-Antispam-Message-Info: ZI417k01CIXM+qs769aTNojhwClY+o0lkUwjeg4/71eccRCxn+9SoBxgGn7OQWhOqhqO9GHvh3/1J27IoJgUEDdinGc6RFXICpcL480hW6b6whCkKqcMhMhjCaKcRTH0RNv0Cqk4QNFl/sMwMEzeJDVKeOlHzFlES62WiZBcPditHHMn169psNd/9Zqo8ghOvJeq8/G7SCXGqknF+EN24x4YT3mH7jEjkY1R2q2+WBdKuaghVhED5QI9Nye3//shAM7u+H+kd4750OST1/ok3OkymtsqP8TIqcQ7QVhGTnkyxEDQrNVuJoLytlJGYpFl1B5QuTltdKhDqgJcJ4lNKPZCfA29ym5gS4s40kbHT5+8+S+f4ML6kkCiSxAifRG1M7LLCFzFl05BJxgs7fNSQg== X-Forefront-Antispam-Report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:YTOPR0101MB2204.CANPRD01.PROD.OUTLOOK.COM;PTR:;CAT:NONE;SFTY:;SFS:(4636009)(376002)(136003)(346002)(39860400002)(396003)(366004)(52116002)(316002)(42186006)(966005)(86362001)(2906002)(66946007)(83380400001)(8676002)(66476007)(478600001)(6266002)(66556008)(6916009)(186003)(26005)(36756003)(5660300002)(2616005)(786003)(8936002)(426003);DIR:OUT;SFP:1102; X-MS-Exchange-AntiSpam-MessageData: zozEuYOV4jaDqzOdGx8X7N+4qiWGLcEUBZiKLQFDI8CblGJWMiF2h0bykeD7IKOsteaVrVS/EWZ641Bc9rp7E4UAcYhIeJmglTbPu0f8+mjddvFFzfnU4nCAvYpXIEoWYGa3Htga8ZyePItAn5Wnmq09gmmEw+wDytvGk70qmEMKhsoAH3IaPfirevJBk80OpHCDXl+5umX4+l669w0W4udUgS4Bp5W6zNmUFzgegASjFAge0vRO7DZN+EmUXTJ8r5rsWTMQz/fhs2ZdeCbESeOwbTzhHTT40lOZzvUZHNL1M4PuoU49n6wEiYWPXH4g+sHqyj1TW50aOOvzZWmqWeIl2BXuu6+1TW/QDHLlbc5oisNMVTKc+NpiH2ipUfVU1ByiOa2cJLyYTk+OSoKygEmfq7NWOXVt/nFwuY1tiOa6g6FIxQGYxuitZ3oQuwVxM+r9iJUJCAGztNoh0RQb1bPTgvUDckbFans/j1o2JKU= X-OriginatorOrg: uwo.ca X-MS-Exchange-CrossTenant-Network-Message-Id: e2499038-0fc8-4fa4-acda-08d80eea591a X-MS-Exchange-CrossTenant-OriginalArrivalTime: 12 Jun 2020 16:04:55.3901 (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: mAhrUJNvPkyMmoOTjemOFzEcHSd8mh5fDZ9JibOba+fFIwEwyaZWnTQVM/6NnaI7 X-MS-Exchange-Transport-CrossTenantHeadersStamped: YTOPR0101MB1756 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=JWEX0Fgd; 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.67.138 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: , The HoTTEST Conference of 2020 is next week, from Monday to Friday, with two talks per day at 10:30am and 12pm EDT (UTC-4). The Zoom link is https://zoom.us/j/994874377 Speakers and titles Brandon Doherty (University of Western Ontario) Cubical models of (=E2=88=9E,1)-categories Eric Finster (University of Birmingham) Weak structures from strict ones Valery Isaev (JetBrains Research and Higher School of Economics) Indexed type theories Peter LeFanu Lumsdaine (Stockholm University) What are we thinking when we present a type theory? David Jaz Myers (Johns Hopkins University) Higher Schreier theory Paige Randall North (Ohio State University) A higher structure identity principle Anja Petkovi=C4=87 (University of Ljubljana) Equality checking for finitary type theories Mitchell Riley (Wesleyan University) Synthetic spectra via a monadic and comonadic modality Mike Shulman (University of San Diego) Type-theoretic model toposes Taichi Uemura (University of Amsterdam) Abstract type theories Further information, including abstracts and schedule, can be found at https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest_conference_2020= .html The talks are also listed at https://researchseminars.org/seminar/HoTTEST2020 On behalf of the organizers, Dan Christensen Chris Kapulkin --=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/875zbw1d95.fsf%40uwo.ca.