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=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 8405 invoked from network); 5 May 2022 10:56:33 -0000 Received: from mail-ed1-x53e.google.com (2a00:1450:4864:20::53e) by inbox.vuxu.org with ESMTPUTF8; 5 May 2022 10:56:33 -0000 Received: by mail-ed1-x53e.google.com with SMTP id s29-20020a50ab1d000000b00427e495f00csf2105638edc.14 for ; Thu, 05 May 2022 03:56:33 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1651748192; cv=pass; d=google.com; s=arc-20160816; b=ero0skVeNoL1b1PR5+AWnDbSWfZY7VG2ON1bUYRdOrfsk1rFzimRXq/DKw4uej5TG9 XE+sMt6aH13Z7sePPiPy5aXqFsas/lEvmenPM2AYZDn+B/sxJZx4127kvkBX+HMJx3HR 4Tk0Rrc0odCL58FlQd+C6G3noQLPXFgqnTL94IZb6lrrRV6yJOYxim011SVy3/SIdNIW /GHO9cpIrzlpQLPnxmViT53kFrd5ofNSFG3em7SAlrl/N+St5tZgsLM6tAwPbmgWIRE3 XjpnQxEp+z/xxviOpjSXMPTW2b7Tk+giHFv/0xglIOex5LV/wNiGpYojBFm/GVS3GTt1 5lUQ== ARC-Message-Signature: i=2; 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:content-transfer-encoding:subject :from:to:content-language:user-agent:mime-version:date:message-id :sender:dkim-signature:dkim-signature; bh=21jphU4TqXqWaSJ4Oy19VXRkjX4YRSMGQUaK8YjcRHs=; b=mQSkvT8dVgeC87gcblD//N73+VSBOozotVsXWHi783rseX+YuapWRv7y75gGDhGLW9 /vgH8ZwebhRQAzsAIHmcs0DC6c0iICDbzqZbKBEDEOuy85BOHZEorEs6qAbocMUj1Grs UVFQizEtIM7yrF12ZWTh70hjoMLXQJ58FzPZRU0atgajD4vkmsqrERRsmKaOGARHsVk6 j43V38c1k51hsoXsE0/ScAoKECMwvaFwWBTtFBS6Bevxq+obBJ2RfwmpN8I6Yl4vYT7A 0b1ms4bxx321Ks7bI73U1ucLTKtlTT4qRjkjZV9aTx97kUyTIkphxzMiW0yhsaM40FhT +kwg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=jx4ZroJt; spf=pass (google.com: domain of evancavallo@gmail.com designates 2a00:1450:4864:20::22c as permitted sender) smtp.mailfrom=evancavallo@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=sender:message-id:date:mime-version:user-agent:content-language:to :from:subject:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=21jphU4TqXqWaSJ4Oy19VXRkjX4YRSMGQUaK8YjcRHs=; b=kqwAXDuTuF1Wy+IKALwULTh5B+dKrP7OfDolcYlVxaUMLF/QCP4OlLcXtKmEl/pbxB f84Kr74r95ww5rojqSoUEjltyebea9JmQ2ru6kkBhIoMuBOOvt6OyKahUS67Sj+moRWe 4NlLtN+jh5kBxA4Tq0WdmT4zxZlBXwAQ+4ndVBr7w1OHA5j2Ep5suI/5nyfICjRa3RY5 XsopKBqROCgo/LAt+ZQfFRHhgoYuKrEHtwa0O/T7hLTfmRDEWfbf/haalFHxm6ycngUo TrZ0Ag7wUldPGv+hem8MDRQDCb9F77JDEVXyMGCEITbMUvMW33UDgTw5/XLwO9d/1CqQ w2Dw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=message-id:date:mime-version:user-agent:content-language:to:from :subject:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=21jphU4TqXqWaSJ4Oy19VXRkjX4YRSMGQUaK8YjcRHs=; b=L04/i0WnBKruIOHqsV7hM9C3+MOr+6Pp4SiI/8HEEGuFHh7ccoFgG2Hd+OeL1ESk/g rsUEIKP21Trs0CEcw9WC0iTLeMZQwDAB1aoLHeaoYqYyRSdl0/26Im8HmGX5xzHixWe4 rgGCvO3RzREyRHYvHw3auu0PVTthA9Ni8mH8cYLGc9mMQsRdY6dxOVm4UGtPlxp1aXkt r2iDqSBwEEfv/nIiLwt9dVpuiZ3v5ad+xEDkgk8fXRNpZ8aJIiMRvoyEtS8uHsoCywuc UKFjagAumNl5LVhjGyZbsKvkEt/9aFVSDSCbYKzCCeJhsPWiG7aCNDPuoqo+88fcP8kD wDjw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:message-id:date:mime-version:user-agent :content-language:to:from:subject:content-transfer-encoding :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=21jphU4TqXqWaSJ4Oy19VXRkjX4YRSMGQUaK8YjcRHs=; b=Vd5MwCioscZIdOrp1qKCgJc0+Gu7YyZUT6PVV9rs7upiT6w0FYXMbuL2EGN6EHQokW vGptye6+lZYzjVleBjPNL7skspqR+d7cvM5rMTZmvfNK8msbW40wNjr9s1i827x4OvY5 yfTpanX4raW+Ef0VnBwADqr812Y71JGXR16hXsx2FC4z9oFT3mJR+bN5HeORTW2qPVbK o9B/VGsgmCfHpovlhzfZn0zXNniu9EYt225NK0L9w4VhUeHJ96bhtU9FgXpNj9dcNkvY DQ+k6C7TIcFH5I22XTItc5rowlrw88tXM1JbD3cxJ4O6LpffmqrTBQGExErHtW4Q5/lj RZtA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM530CYtv06+1T5B1IiptPAjcZTf2KbBqoSwsi/5bYaxcA+bYqfIlo B7btddBPUQII9qFxc2ZOwxE= X-Google-Smtp-Source: ABdhPJx8gIxXSwRpTD6iKeIAsbkRR61RkcRscssaebmyfcWuAwBP4CiFczlcv4+fH3YpyPu/+FgRYw== X-Received: by 2002:aa7:d610:0:b0:425:ccf8:c369 with SMTP id c16-20020aa7d610000000b00425ccf8c369mr29488755edr.368.1651748192087; Thu, 05 May 2022 03:56:32 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:907:7ea2:b0:6f4:dcbc:baa9 with SMTP id qb34-20020a1709077ea200b006f4dcbcbaa9ls1468361ejc.2.gmail; Thu, 05 May 2022 03:56:30 -0700 (PDT) X-Received: by 2002:a17:907:9726:b0:6f4:c0e:40ce with SMTP id jg38-20020a170907972600b006f40c0e40cemr24789332ejc.170.1651748190159; Thu, 05 May 2022 03:56:30 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1651748190; cv=none; d=google.com; s=arc-20160816; b=s6oZgu9Jmgu8UZRVO1gxKNriB2z80ZVWYhxCHflOt2OocWn/Efh9oW5U3XkArzIdCQ QFvy+bvSOoIJAmnIGZpLI6jTV1YO/hyEbDbGzDLgZbleHp4+DgSzlf284ZzEZnB/bcfX shVzqQIjS3/JxqtaLtt6DXdDcvU3KjZNbsOdzpnZP3ofsBbViU9YjK/Jkj1nEyNMRmmz JNGzkc7wlI/tfHva9xaygMMvl2nUBJWXLZAFc7WvoOtYc4l+DPiGlZT0+/qiK5LT5yD6 Ed8NYWHjAl523lFKVa6DiPFSATbN1nhTZOMBk0kBlp+B1mA723qmRHm2zRYpkLgexKto Wl/Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:subject:from:to:content-language :user-agent:mime-version:date:message-id:dkim-signature; bh=5wDkiFoMfkjzhe64XPHSvZVRL8Niw7bDf6fp16tvUWg=; b=u0oiHANUcd51l2cNPa1h4EYeOu4Tqt+D5V1cU83lAF8IifGW7oQU/AXa08p1fHvRHJ AuLPxMbL/ZVD2WJlIoP3kSPXx3Np+FWJWEkKLwkIjaNIwQ7dzJWPfe0dqcTwIOIipb/g arZi/2QbWh8viz/bGqyakVZcYvKj/R0J7SA20Y/tWCOH2z9eYLARChDAbLzZS2X++idR AISqhmAyd2HHup7fnO0sfJa19T4s+y8SDENmWA/dfaNEJn2Cy5mbwfkx0nmscPfUkOMf NCyloKZq6v1gaTNTqVjM1P5uHkVX0CaEd+RWihYc0yaXVSG992SB8/sfkwg60YqPitZo 1nYA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=jx4ZroJt; spf=pass (google.com: domain of evancavallo@gmail.com designates 2a00:1450:4864:20::22c as permitted sender) smtp.mailfrom=evancavallo@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lj1-x22c.google.com (mail-lj1-x22c.google.com. [2a00:1450:4864:20::22c]) by gmr-mx.google.com with ESMTPS id d4-20020a50e404000000b0041b5ea4060asi54770edm.5.2022.05.05.03.56.30 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 05 May 2022 03:56:30 -0700 (PDT) Received-SPF: pass (google.com: domain of evancavallo@gmail.com designates 2a00:1450:4864:20::22c as permitted sender) client-ip=2a00:1450:4864:20::22c; Received: by mail-lj1-x22c.google.com with SMTP id q130so5088668ljb.5; Thu, 05 May 2022 03:56:30 -0700 (PDT) X-Received: by 2002:a2e:93c8:0:b0:24e:eabd:bf6e with SMTP id p8-20020a2e93c8000000b0024eeabdbf6emr15204649ljh.347.1651748189107; Thu, 05 May 2022 03:56:29 -0700 (PDT) Received: from [192.168.1.189] (89-253-67-151.customers.ownit.se. [89.253.67.151]) by smtp.gmail.com with ESMTPSA id z4-20020a2e3504000000b0024f3d1dae93sm163007ljz.27.2022.05.05.03.56.27 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 05 May 2022 03:56:28 -0700 (PDT) Message-ID: Date: Thu, 5 May 2022 12:56:25 +0200 MIME-Version: 1.0 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:91.0) Gecko/20100101 Thunderbird/91.7.0 Content-Language: en-US To: homotopytypetheory@googlegroups.com, univalent-mathematics@googlegroups.com, lean-user@googlegroups.com From: Evan Cavallo Subject: [HoTT] HoTT/UF 2022: Second Call for Contributions Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable X-Original-Sender: evancavallo@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=jx4ZroJt; spf=pass (google.com: domain of evancavallo@gmail.com designates 2a00:1450:4864:20::22c as permitted sender) smtp.mailfrom=evancavallo@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.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: , =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D SECOND CALL FOR CONTRIBUTIONS AND PARTICIPATION Workshop on Homotopy Type Theory and Univalent Foundations (HoTT/UF 2022, co-located with FSCD 2022) =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D ------------------------------------------------------------------------ Workshop on Homotopy Type Theory and Univalent Foundations July 31 - August 1, 2022, Haifa, Israel https://hott-uf.github.io/2022/ Co-located with FSCD 2022 http://www.cs.tau.ac.il/~nachumd/FSCD/ Abstract submission deadline: 10 May 2022 ------------------------------------------------------------------------ Homotopy Type Theory is a young area of logic, combining ideas from several established fields: the use of dependent type theory as a foundation for mathematics, inspired by ideas and tools from abstract homotopy theory. Univalent Foundations are foundations of mathematics based on the homotopical interpretation of type theory. The goal of this workshop is to bring together researchers interested in all aspects of Homotopy Type Theory/Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. The workshop will be held in person, and remote participation will be supported. Specifically, talks will be streamed for remote viewers given speaker permission, and we will support streamed or recorded talks from remote speakers. =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D # Invited speakers * Eric Finster (University of Birmingham) * Kristina Sojakova (INRIA Paris) * Taichi Uemura (Stockholm University) =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D # Submissions * Abstract submission deadline: 10 May 2022 * Author notification: mid June 2022 Submissions should consist of a title and a 1-2 pages abstract, in pdf format, via https://easychair.org/conferences/?conf=3Dhottuf2022. Considering the broad background of the expected audience, we encourage authors to include information of pedagogical value in their abstract, such as motivation and context of their work. =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D # Financial support Limited financial support will be available to subsidize participation costs. Priority will be given to women and members of under-represented minorities, including representatives of developing countries. Please contact the organizers via evan.cavallo@math.su.se for more information. =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D # Program committee * Benedikt Ahrens (TU Delft and University of Birmingham) * Carlo Angiuli (Carnegie Mellon University) * Evan Cavallo (Stockholm University) * Chris Kapulkin (University of Western Ontario) * Nicolai Kraus (University of Nottingham) * Peter LeFanu Lumsdaine (Stockholm University) * Anja Petkovi=C4=87 Komel (Vienna University of Technology) * Paige Randall North (University of Pennsylvania) * Christian Sattler (Chalmers University of Technology) * Michael Shulman (University of San Diego) * Th=C3=A9o Winterhalter (Max Planck Institute, Bochum) =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D # Organizers * Benedikt Ahrens (University of Birmingham) * Evan Cavallo (Stockholm University) * Chris Kapulkin (Western University) * Anja Petkovi=C4=87 Komel (Vienna University of Technology) * Paige Randall North (University of Pennsylvania) --=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/a3666faa-5937-a253-41f0-94c62830630d%40gmail.com.