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,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 7958 invoked from network); 27 Mar 2022 16:28:33 -0000 Received: from mail-ot1-x340.google.com (2607:f8b0:4864:20::340) by inbox.vuxu.org with ESMTPUTF8; 27 Mar 2022 16:28:33 -0000 Received: by mail-ot1-x340.google.com with SMTP id m12-20020a9d7acc000000b005b21f450ed2sf7132622otn.20 for ; Sun, 27 Mar 2022 09:28:33 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1648398511; cv=pass; d=google.com; s=arc-20160816; b=of7p7w/JoxIKQ+DsFsXEGDzvaEp24zQ1bzMDY2NmiLb3etESlOGD0scO5Ur3SV2lIO 7Rqgr5nl7ghN/i3Fi97hJX7LeBh+6xSbOD9XvEaqzAXIP+8i5lBBjW3KwIZPtXAlsVhk hjYwfkoL1FkVBKutHCFXO13/vo8Cp/Rg7dRaqK+fz0cWXPqMH2k0hAZFOWOnIExeLhYL kR9Re+Z60QvwxS7qOYttFX3GdsxBd/90hmjxfLb0Orf3ZNfxJmz8MZA/V8yqRD9DQ7sb G7r27F4Ig1JJUmfK7526mk4+siLzsOE4yWN6wX09VRgC0LBAj2ENI0vdsOrzx3f4Z56x AaeA== 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:to:subject:message-id:date:from :mime-version:sender:dkim-signature:dkim-signature; bh=Zti1+R2F1Rl04UsXEJYtCCRwbQ7aAd1HB+v6FRzA+n8=; b=NoQBHtr42SKroQlBAwnIp6JJkExg7elNcPmmVyRI9Vx/ooG4wnPWcC5rxXLAkzcsmu w662kq6bBDYEHOxZ5fnorfIKi92mkirEAA/TBiM2XEPUOdvAMmLd6hInD1tT6VrXP9jz UbWTTVgwpupA8FFr2AswVXfeyfxrCDjQvufwPCuA1IxMCMJ8ioC2GxhAUjy3fGIiQfTq pqRezTzgeFtqN9v9nCaHjf4DB6SLesWmE7XfdegMQpC51Z2DNFstxgLSgV8RoBNzyHG9 /6qpc+U/tbu9lUtVuVRQZ4fyln+xxbdvF81tO3utjwsGE5Mzh9DgF4lzfFxH9q64vA2S zHzg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=LvchOmsJ; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::a2b as permitted sender) smtp.mailfrom=andersmortberg@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:mime-version:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-subscribe:list-unsubscribe; bh=Zti1+R2F1Rl04UsXEJYtCCRwbQ7aAd1HB+v6FRzA+n8=; b=I4gDviRMObu1UwYcOmrHpzqVgxGSDF4zRvpTzIZ6h2DzN4qC32DVwWeDFGGIZ1TPJj gohr0BfdJuiPrMkpqUTQ0v0dUlNlpIQAuxyBb57Fg4KX/OkMQZA4hTnIjjCeiX9BHlf1 buLWu9Arpj75yCrguxg7WPdDXbQbFSVg50TODbu4X5SAWnXkC+/jlhZdlDhLA1FVjC9W s2Qzeq1eUWUuqHmKZuYDq/pg2/vqIc+FZLzCjkD/FAOuJ98X9G6YmQ2DOQLWlnU5biJx Cfe+wiDsUWwBoO/wxRlK/56mxaATYvqHQsW+k4u5LAqASzN/QvcxSxecP6WSs14chueU 4hLg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:from:date:message-id:subject:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=Zti1+R2F1Rl04UsXEJYtCCRwbQ7aAd1HB+v6FRzA+n8=; b=ff/BpzX04UbRXH/YAyjeojauUTVGR/9gpU1rRxuiSweJbydHJDuMd2wnbWz5rpHydW BOe93lCFA14XFGeRWu2W0OcClKVBL8zLaVxuoQ1PfWCiJAQPS3l2jKC4hiv57P4+J5wD BVQj3G0olOZFomyM101TM1A3ThTZ2vK/+ZOEGA/dRQRqklqxfyIAXxwdVWGyi6KNFkmp 4nzs+aovLiQntgVOXiqwsQbAfG7cwZEW9cQr6VAlLLCm4eLQlyaJQewwlIitXTZIJ8g8 1SpJlBsXFlMBZaMtCvUoYVxxm2SPlX768Ubm8EEZyZxk43+CJTfIZzPDdQq4E3i+xxRT St2A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:mime-version:from:date:message-id:subject :to: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=Zti1+R2F1Rl04UsXEJYtCCRwbQ7aAd1HB+v6FRzA+n8=; b=1PlIgsxf0YMTlYnvHQD4EcBG/POBpzxTB5QMPYkPU3JkUUXb+7NXKZtL+pP8eDjAb4 qM1ZDg035H6snNFE7DWX7doJsxzmFupCAqBO76PujqYslekbwf6le7MN1v1KjIV4r0Sc dxE5edLA9uUcPWNw9mUGqZmy6qdOUlcSfJT/88FKyf4p0z14IRHaNIQcCdoCqn3JbpE3 Tvbi7vWFQAiI9EbRb/aCgBHBV3zTI4vybLo5Y00SxKT1KECbadNIk8JzrrLz7iTR7aTO wpr65UNYyRaZu21LU030ESbw7BOc7mleSWGNI0xRPh8GvER3xkEOmDU6B8fDu3iYYOYn +PMQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM530jomAtsqwYJiRLu4UC2JIIoLdPDTfvuMUFP3LwtMB/svm4jLLY 5c9K96/hj74dH6LmDjAR5LQ= X-Google-Smtp-Source: ABdhPJzy8LdAts53aynvTBLDMdkeWTOMkxxPhlN5Guwggj1zj6ANGHjqy/gy4n8ynnojVpX9j1r5/A== X-Received: by 2002:a05:6808:28b:b0:2ee:36b8:8619 with SMTP id z11-20020a056808028b00b002ee36b88619mr14688252oic.275.1648398511485; Sun, 27 Mar 2022 09:28:31 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6808:1918:b0:2da:5caf:d28 with SMTP id bf24-20020a056808191800b002da5caf0d28ls4290152oib.4.gmail; Sun, 27 Mar 2022 09:28:30 -0700 (PDT) X-Received: by 2002:a54:4714:0:b0:2ec:f566:8da5 with SMTP id k20-20020a544714000000b002ecf5668da5mr13968013oik.97.1648398510631; Sun, 27 Mar 2022 09:28:30 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1648398510; cv=none; d=google.com; s=arc-20160816; b=LfDas+H+MHV+NX1EFt/2mN2BmwDRlfABThKWBqU+e5L5PtzsI3+l9VUz3eACaFGkaC ccOW5K3g1YLrlVKTfcA+BwKNDmpmqFB6LiGBy/ElouUpWU0olSt0PB6rqYCyj7gpt0tA a/+EYSt2b9MVznOLU13hE2TY3klKTKY9BZ826fogH0DpGQNM6ECZV4FC9LryAIAgkRWf J+mFXMhpileszzN87jFnhNp+/SA5mALuawaucQAkYa7oEJ9yMuhrM20JRX+aH1WoPiTE 9632zALskwO7nbd1wS2CC2SCb6wRGgF0ROqlUo1PXbKyMvWJYccS6zA18BaeIiG+kvMq aD0Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=MzovqzoCOb1acLtqL2FcAMwxCjj/GCw7Z8wYesTITwk=; b=YdPWPg8uZQ6zGzi0qeDRJgbSro5bOWIaL1qZQNt2Hd8G28nn5iP6vJleBQ3csveN33 zzOaZbFuMH/cmXkJt6r7U0nHygsWYAQ8eOwhvlE4F77aSMzFtRApVEt9nWioqU/FaSow QkTZRPa6Le3ZdUK6oeoWYDnwFO8WmMff2zV+JYq/tv2Pkt9qiH5+JX34C0G2Sv3Vjw4h b33ryLnwkPuPheP4WuDSNxwjLI4ctpWx0kaxjM2ik1n3YWavo9mHyYBSim9TyP65lmP/ XqP6K/Ily9CjVfH2E95RTIih57R8tRyN1z96RPeW76LynqeQ0HsEg99e22JrYita3nX0 Ai4g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=LvchOmsJ; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::a2b as permitted sender) smtp.mailfrom=andersmortberg@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-vk1-xa2b.google.com (mail-vk1-xa2b.google.com. [2607:f8b0:4864:20::a2b]) by gmr-mx.google.com with ESMTPS id bh40-20020a056808182800b002ecaaa0ac09si773817oib.2.2022.03.27.09.28.30 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 27 Mar 2022 09:28:30 -0700 (PDT) Received-SPF: pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::a2b as permitted sender) client-ip=2607:f8b0:4864:20::a2b; Received: by mail-vk1-xa2b.google.com with SMTP id d7so6748869vkd.11 for ; Sun, 27 Mar 2022 09:28:30 -0700 (PDT) X-Received: by 2002:a05:6122:546:b0:342:f3e6:4214 with SMTP id y6-20020a056122054600b00342f3e64214mr2271219vko.26.1648398510112; Sun, 27 Mar 2022 09:28:30 -0700 (PDT) MIME-Version: 1.0 From: Anders Mortberg Date: Sun, 27 Mar 2022 18:27:53 +0200 Message-ID: Subject: [HoTT] Workshop on Syntax and Semantics of Type Theories in Stockholm, Sweden, on May 20-21, 2022 To: types-announce@lists.seas.upenn.edu, Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000a4c45f05db35af13" X-Original-Sender: andersmortberg@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=LvchOmsJ; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::a2b as permitted sender) smtp.mailfrom=andersmortberg@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: , --000000000000a4c45f05db35af13 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable We are organizing a workshop on Syntax and Semantics of Type Theories in Stockholm, Sweden, on May 20-21, 2022: https://europroofnet.github.io/wg6-kickoff-stockholm/ The event is intended as a kick-off meeting for working group 6 on type theory of the EuroProofNet EU Cost Action: https://europroofnet.github.io/wg6/ The programme will consist primarily of short talks, with plenty of time for discussion to share recent results, and co-ordinate future research, including collaboration towards deliverables. On the Sunday after the workshop, there will be an informal social excursion =E2=80=94 details TBA.= The meeting will be in-person. # Confirmed speakers (more TBA) * Andr=C3=A1s Kovacs * Andrej Bauer * Anja Petkovic Komel * Ivan Di Liberti * Jonathan Sterling * Taichi Uemura * Th=C3=A9o Winterhalter # Deadlines Contributed talks deadline: *Monday 11 April* Funding request deadline: *Monday 11 April* Participation registration deadline: *Friday 13 May* To register please fill out the form linked to on the event webpage. # Organisers * Benedikt Ahrens (TU Delft & University of Birmingham) * Peter LeFanu Lumsdaine (Stockholm University) * Anders M=C3=B6rtberg (Stockholm University) --=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/CAMWCpp%3De5gMPKPYtgbXvzXB%3Df_7Wd_xM5krpVuXYdGY87%3D6gK= w%40mail.gmail.com. --000000000000a4c45f05db35af13 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
We are organizing a workshop on Syntax and Semantics = of Type Theories in Stockholm, Sweden, on May 20-21, 2022:

https://europroofnet.github.io/wg6-kickoff-stockholm/

The event is intended as a kick-off meeting for working group 6 on typ= e theory of the EuroProofNet EU Cost Action:

https://e= uroproofnet.github.io/wg6/

The programme will consist primarily of short talks, with plenty of=20 time for discussion to share recent results, and co-ordinate future=20 research, including collaboration towards deliverables. On the Sunday=20 after the workshop, there will be an informal social excursion =E2=80=94 details TBA. The meeting will be in-person.

# Confirmed speakers (more TBA)

* Andr=C3=A1s Kovacs
* Andrej Bauer
* Anja Petkovic Komel
* Ivan Di Liberti
* Jonathan Sterling
* Taichi Uemura
* Th=C3=A9o Winterhalter

# Deadlines

Contributed talks deadline: Monday 11 April
Funding request deadline: Monday 11 April
Participation registration deadline: Friday 13 May

To register please fill out the form linked to on the event webpage.

# Organisers

* Benedikt Ahrens (TU Delft & University of Birmingham)
* Peter LeFanu Lumsdaine (Stockholm University)
* Anders M=C3=B6rtberg (Stockholm University)

--
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/CAMWCpp%3De5gMPKPYtgbXvzXB%= 3Df_7Wd_xM5krpVuXYdGY87%3D6gKw%40mail.gmail.com.
--000000000000a4c45f05db35af13--