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, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 11325 invoked from network); 11 May 2022 14:37:16 -0000 Received: from mail-lf1-x13b.google.com (2a00:1450:4864:20::13b) by inbox.vuxu.org with ESMTPUTF8; 11 May 2022 14:37:16 -0000 Received: by mail-lf1-x13b.google.com with SMTP id l19-20020ac24313000000b004739dbba717sf891853lfh.5 for ; Wed, 11 May 2022 07:37:16 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1652279834; cv=pass; d=google.com; s=arc-20160816; b=eSrPjbgyNkq7dskDR+PpEqg/fbGLxjNkNQi6Z9leY3Yo2UEUv51/XtPfUBob8lZfZh 6zcSIus20HQdcPGJDfRjczxkXM5x4vZN3gMjq+OtZ2280oO6IpuVvEYgDp3+ixJSJWCt yaAZxg262Vzh21N/LoyDjXtIk5xP60VidUK+4phPbFh4bXOjysMbI7UanVVvk6M2bbb7 NU/XzKoIdjtdJ0VvGG6v2YHmzt9U/DHT2elfnCHUUWVrTwsCmoNHB+Ji8es8UoEDx7Gb o+t0LOAs68WIDYpDHqvHCrgm4nfNUbtQFvbbp+ZoA6DUfKe0aJM/3aMRAbqbNZXzqiPs GsJg== 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=4uZUZZ92ChpgBVn3lFWxaxF40iIWTr6TFepFm6HKW1I=; b=LFuuLbaW45ZCDsSW0doDvVMjLrJemcbl7T+Se6I1/Q7jefooX2h/QFM9SgYYGir5wL 7sEL3unHJrjvcgozaWdzmNg8nhxrq1pMBDziHMBho7CBiSJ58hYUrpwoL8lNB9nYMzyK ZyyztDp59Kd+yTinIiB9eVE4F+8niFfv0H967U0Ha+9jYN/FLkc1/zdiFAoLb8UsmpCw WCVBASWpn+52i1JFbCl+ghWaz2l6JDCbRYDSsWvBa4TeELqgIZ0ptTjaxCr4nhDE9hFE 062ZmR177qb4yYI3z8yQYN+2yM4eJZDtDMLkQ7g0pu1VUWFL7H1TV+WEGvnu3TuLDRZK FIAA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=K+3wJzSM; spf=pass (google.com: domain of evancavallo@gmail.com designates 2a00:1450:4864:20::135 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=4uZUZZ92ChpgBVn3lFWxaxF40iIWTr6TFepFm6HKW1I=; b=XiwOoRW03FKtC5CpP+7rmVSdALFDMS6nB9t9uZyeSCpf4at+PvnGn6STIimT4MWLY8 FcNakIYfhL0Lv1QF0gbAIjNrDAur/4nnsaJeU6jkwmJN/QVlEr6zz7bHM6TVBcMc+0x8 Get4v9FesZtoNv6QETCzepKj0np1l6Ljv371/hktdnqzWLCS2m5MsmwBY8V1i8a4u+kA OpVpA3zP2pmaokuLbmxFkect4vOPbUaaoblzatSK8Bwdekd/ZhxN39kdywYI1O2kATao 0sbdsXXzI1wS0gvLKVm9mNxfN5C80c5yt9IepYQMKM/suVVDPu4JXV8AbAd4ysagOyZM AMCg== 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=4uZUZZ92ChpgBVn3lFWxaxF40iIWTr6TFepFm6HKW1I=; b=a8rRDAfyN8TJm+NwweFWJ/7l2esa32tfj5oJrwyjj3Os0/kyfkZeJQCK5YxZ2Lzchk l0bcuH8+SNPcTAt9jR7a87X+Z2WboeVnMjHUCCsK/cYOlQgTurvcRz56HYLZ9n5Wjx1s ug+8HKbx9CZUzr77jN1kQu7UBEaCiAwcg/hWSEPx7iS78dePm8Zs15KqfgFO5h2PXlif kn5b2YoLOAvbTtC1RNIso+mJ02Kh1TiifMthrWp9Tz2+jy/80aNwH9C4yOyFddDHXI/k C9KxVoumIyltPanMTLGkuxj+7eJ4vFnDjEQGVphTiNDdUODr9LEUIAA1p0M+eA8s9T3z rfCA== 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=4uZUZZ92ChpgBVn3lFWxaxF40iIWTr6TFepFm6HKW1I=; b=UeAV5BSuwQaLjtcBGEbIo4B/vXhjLlKl6R5mv7BQY7ugdOYZUBMvNQ3eF1z3VyM3fY EWv6sTAc0BMwciIVCntMNxK3Go2PpF2k3AD2P1kTch9rBboeV7Z91vdjT+Rw7dKEl6hk qmskJzR7rcZ3tPVTbDiuLQzDgkDU/qz1TjDDGHQaK0tL29GwUNiWopPo3p0lWL+4FItT EQ1Q8TXEGQmYRSsszD6dfL6DS7N1kCe2qBPHCztWXorWvyJBXn9SXpABllBiPTd+ZThg sqcRG14gCfXMspwc74ap7FX/fVb9ZfLqaqCxwQ6n7fDd2z7N2c0eQfjY7rqR2L8mwKm3 6MmA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM531QdGue9K61PYbXeQ1XtVbpKg+nI5VebPyjVJ/an8h1d1xW9IEk MDXWu1vQ+Bg9E5m+UELSKVw= X-Google-Smtp-Source: ABdhPJy1+WbSE14oZkJ2g6yx8UufDLdSn1V4zXSZMWwxcHCsUSOTTqVOwUuu+auG8ofLyUh9y/xn1A== X-Received: by 2002:a05:6512:3096:b0:473:b43c:1678 with SMTP id z22-20020a056512309600b00473b43c1678mr20575780lfd.289.1652279834580; Wed, 11 May 2022 07:37:14 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:b888:0:b0:250:638a:caae with SMTP id r8-20020a2eb888000000b00250638acaaels425280ljp.2.gmail; Wed, 11 May 2022 07:37:12 -0700 (PDT) X-Received: by 2002:a05:651c:1a23:b0:24f:4f94:2cf2 with SMTP id by35-20020a05651c1a2300b0024f4f942cf2mr17727582ljb.249.1652279832232; Wed, 11 May 2022 07:37:12 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1652279832; cv=none; d=google.com; s=arc-20160816; b=KOh20ZRQzdIqIC62kgowOqT2boXCP+XGzxYNCZppYVChktxmkp0DTLcob9NkV9oen2 9cmvs0W8MEM3uWBC2sYHT0wcs5i/veJXP0WQSzyTEaTTpPmeZiEyB5EMjAjti4g6wIrn WqAz2KILKEKA4+3ylQszjlxVm2WCJBN1A3mcKUG/jV5QEYCIWHwoSl4sL2Yo8KAdRgVf hNmyB35FokfX1c003q94ZOXViwLCWItFf3yUpe2niRs0m9EwDrvwZ8iHGXbhVfbwQjrB 9RYePwIMgFkJEom8mL70EYtVP999CRBW2ZzJ0jsiJkRLlHx0jDutQmz7jh5Krd3LNxjf DVdA== 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=sZfzRVxERBocWSpFgELq0gHSwVF/8J6oTygKvEDM6J0=; b=ZxV6ebOY6MahsRrXxHhvz81n4DIXuCy7HBakxXGmwGQbo6vAy8x5Z9j3hscEwJ+mhN 0H+APV6RO+6PRp6V8UZb2LdB+BuEylTwj4+Gu3j+xOo/0GwOZbXQ68qu2urhtSavOf0C J/s3jna+89frCiDZDImvTxnEe/b3VDr/pUJb2LLgRWLGQ+iMxwIPd+UMta217Q7EggIT T84obUfM9vKrsMxUUSpTGLgiQoqP97+kyYFxb36MPdcJiho2YompJy9jmC5A4cMMwyjH vlk9eA7WHnLT2m+OGc9dFwf/TwtOY6daqElZERd4E+yxmb67sgjBYMaa3gkpu3fFo3WG H5bw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=K+3wJzSM; spf=pass (google.com: domain of evancavallo@gmail.com designates 2a00:1450:4864:20::135 as permitted sender) smtp.mailfrom=evancavallo@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lf1-x135.google.com (mail-lf1-x135.google.com. [2a00:1450:4864:20::135]) by gmr-mx.google.com with ESMTPS id q20-20020a056512211400b00471902f5be2si126289lfr.3.2022.05.11.07.37.12 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 11 May 2022 07:37:12 -0700 (PDT) Received-SPF: pass (google.com: domain of evancavallo@gmail.com designates 2a00:1450:4864:20::135 as permitted sender) client-ip=2a00:1450:4864:20::135; Received: by mail-lf1-x135.google.com with SMTP id i10so3888375lfg.13; Wed, 11 May 2022 07:37:12 -0700 (PDT) X-Received: by 2002:a05:6512:3f07:b0:464:f20b:a160 with SMTP id y7-20020a0565123f0700b00464f20ba160mr20350494lfa.653.1652279831504; Wed, 11 May 2022 07:37:11 -0700 (PDT) Received: from [10.200.25.66] (wlan-eduroam-130-237-240-189.su.se. [130.237.240.189]) by smtp.gmail.com with ESMTPSA id m12-20020a19434c000000b0047255d21136sm314570lfj.101.2022.05.11.07.37.10 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 11 May 2022 07:37:10 -0700 (PDT) Message-ID: <1f912b06-0428-032e-fa2b-d2c516dfbdec@gmail.com> Date: Wed, 11 May 2022 16:37:10 +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] Extended Deadline for HoTT/UF 2022: 15 May 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=K+3wJzSM; spf=pass (google.com: domain of evancavallo@gmail.com designates 2a00:1450:4864:20::135 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: , We have extended the submission deadline for HoTT/UF abstracts to 15 May. Note that we will support remote speakers and participation. =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 EXTENDED CALL FOR CONTRIBUTIONS 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: **15 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: **15 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 (TU Wien) * 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 (TU Wien) * 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/1f912b06-0428-032e-fa2b-d2c516dfbdec%40gmail.com.