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 7494 invoked from network); 8 Jul 2021 12:50:22 -0000 Received: from mail-wr1-x43a.google.com (2a00:1450:4864:20::43a) by inbox.vuxu.org with ESMTPUTF8; 8 Jul 2021 12:50:22 -0000 Received: by mail-wr1-x43a.google.com with SMTP id m10-20020a5d64aa0000b029013370949d6bsf1907370wrp.1 for ; Thu, 08 Jul 2021 05:50:22 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1625748621; cv=pass; d=google.com; s=arc-20160816; b=z06ZShYCJc1r7HIbDSS2Y4qBfwGz8dIb93v4rYyFnbul2oHk6wXUZmy7jH0Xk2sXY0 ll1qZUz0fFWkzUn7ixMFF+PltY6SOWS0MGof4KkiSgzgLKRGlQppOKudCXS6R9h0CwG5 VgZYf2jFyrmUhefYgu4p3ixy8MiKLBdUMiW/W11J3GWkjSgbPY18ChxxTqXyds7wjrUy Fvzd6EXb0ervPRC+Q5bn9MRIU2wjZ8nPgG/lfOMZRLjApUSJ3NKqjACz73jCM8e3endn peJTNTh3JmiSQs8E1adTHlmmfyfqoAbaDaLUjZ61Z06jXeT21kRojYrD+HP4COlLV8zn 7XQQ== ARC-Message-Signature: i=2; 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:content-transfer-encoding:to:subject :message-id:date:from:mime-version:sender:dkim-signature :dkim-signature; bh=8wdw62BSlcZXE+MIqdaEyUtCHgUNEFnpJarzyQkIYak=; b=JBMIKPVqwnC81teMCRZzbn2+wtKvIsSmDkmeukgLr+dyNx9t9rTKVofwdI0M5o2fE1 2j605xXbTDsj7TjMQobrzeF9KlAIPvmGP1iwGftK1uHQ+aPJfwofJyKozc/Gl+H+hYML +jUG9hrPTR1YlpttoCENBia8HMHDffny9p5FpKMjsZwUezJhEhRqjP9ppK89zfCuJ25V Dn1+yshw1AYTqOVauJLqIWYTM51x/N1wcVnyo/G3f7g3m0itIZbCnt6IX2fTr61FBkAf nHL0eYo+swgNJEX/pkVq4cPEh/zAziYznE1VVHXXiPpveR8PidIRt5WIEiQZTPpj3BKY dQWQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=GGdUdTT9; spf=pass (google.com: domain of k.kapulkin@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) smtp.mailfrom=k.kapulkin@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=20161025; h=sender:mime-version:from:date:message-id:subject:to :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=8wdw62BSlcZXE+MIqdaEyUtCHgUNEFnpJarzyQkIYak=; b=eru5PiPMyCSHbCTRRYVq5kkTVJkzsO7OQQNv3BsZ3AQS21GVAfSc6/b3ne/lDEQWOG NUKsbKnMCkMgqLvBJDyb7BCHctsG5aHEu5BSSGeoSy7zIQ2KGTzA1ZLwbLW16P/DoYul GkwoeUnf6OnlctsgXkuNU28DaFpjqTOe/hlSbyqewPKb9LZ4Zf9LYWXUEk7HWxSHED32 9o3CEWbOwwcHNGVdWgtZv4/lDDLTBc8XyTYgJh0Xiclf8tGXymIIt2B0ZZ09x3TBnNzj RvueCmv7Ff5N3VqTpfRoUWr1hjWZb7JLkFeD9BxRqNKa0Smh87xZR93UgRc30bbmPoFa N3pA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=8wdw62BSlcZXE+MIqdaEyUtCHgUNEFnpJarzyQkIYak=; b=OnHe/BkFs2yoQCL2ZUVVPgeWgRObd36YblZ90TfnfvfVz0azITc+/mx3CaZjjolEPo zj+yKz1S2z3nzjyV2i5AehcfvcsebMao0EUcq57K1GcICzsoNS31/i4Y3cAajCQ5OomC pshxdyx6TpqaM0zo5CLAXZjDRJEd+Ccvq4ePvWNzizg+Had9tVU0GJkL10dT3KIDC5gY Ukk0PO10KUyn1+MH0BZXdbXdN1zRp8fBwa2nsq6x8GE6wMGIVemSyyF7y+ImkloXitEO 07LESkNdPVLhpCs2eqiSyfZhBzg4Q9tpt/2HGq+h9EizvxkYirpJcqfsMCg2gd1KcHBR +Kvg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:from:date:message-id:subject :to: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-unsubscribe; bh=8wdw62BSlcZXE+MIqdaEyUtCHgUNEFnpJarzyQkIYak=; b=llsesqMgLvU3sn7f2xJl1gSwwhcqZ341nVkAOcg7lZ5KeG1/xv485Io6ZChH3kgn+Q 5ZRS5Tladpo8OMP/MAK+wbdCjoI52w5HbTZOXguDbwzY6OO9VnO4mlYwgOFZ8s1dn51W Kxdp1VAzBAr9rQZbTL5RxCuqTXrL5GUMgOCZryWOizPPY0nINXV9Qj49BRds3AM2nXsb JlsAgUdeXIW4wxq2OE6DhbTu1AcLHsP08L9RUFg3fST8zgwav4uVJFmJ9h+s04I5O/ij PRQ73l5hagMPtcUSKy4J3C5ZdPzlBnWC1ekgOoZwoHjAYKXoT1hESVvPzudTlPVyOrJw 064Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM53288QqsDk2rjR2xgUpAacvEtzfkgagPt/Fry/huWU9eG/HogobJ iTKKp9c1dM9ZaeqOZZf4GWs= X-Google-Smtp-Source: ABdhPJyzTztbJZcz/ZoUCdaeVLfqrLVeFdlJn3X6WlvPUrDfFO6iuFY6YG9emkUAtZZu4pehdA1jEg== X-Received: by 2002:a5d:4606:: with SMTP id t6mr35371438wrq.288.1625748621136; Thu, 08 Jul 2021 05:50:21 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:adf:dd86:: with SMTP id x6ls1155810wrl.1.gmail; Thu, 08 Jul 2021 05:50:20 -0700 (PDT) X-Received: by 2002:a5d:67cd:: with SMTP id n13mr34309473wrw.201.1625748620240; Thu, 08 Jul 2021 05:50:20 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1625748620; cv=none; d=google.com; s=arc-20160816; b=pRXxHy8bOoytlDJR2/BEJIniyjCpYF1/9DXTvJFQmMW4it4MFsqotRxTJAfIAfqQXC 6pgP/CZudJkpnE1/2rQnsQmyWeV7GwXBc/tGes2PgvEXK9qJu+UpBHI/aoo3KndsSEDW camdjrHzSrYjM7bvUZgPU38KjWCN+7nSBhw4HjLGZwo7OWGnG2cj4F0KeixKYxivfyXX DyAgzN5F4Xp8srfq32/zYKZkmE226M/bojNwTc21yhPGQjAy3zjjpNBoqMVe1kMkEgXW Pqnbz5xfDW3wz5UkzcSEpt0VCfSdHay3rDiIJfiov0GmtzE59zRS29szp7pl9P0PW+wv 6y7A== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :mime-version:dkim-signature; bh=FwSKeCfw4JH32ay570i1s1DJA9ia4vtO/U2W/a/Jilk=; b=aygOOGGi6jdKGxBgxDLnEjIkqgRw2SMFng63EXRgBqEMn2bXkpCWdkqB5VyuqIi3vq Si37f5UUVJvsy7IbwG2vcNGIPi49GUFgyJWP9P6yH3JZ83caeTK4bKflL3SzRRWPLukT RCq7C0/3a+TIebB8zvz38dLkZTfPBr8DjXXTEazwRi+0benr0FZTgHr8OcggIOVFWqau MCWrFBqka1NUcyeJW/H8RQPMU453ozgzTD75PavmXJMvUwvm0iUmhqgv+Y2DRzWiRDr8 jNRtIJvhvJQnMw9CxozBi9BJ741MSZjViyYzcBjQ77MAeagvvD3+owlK6DYDJjwRlsf2 V/WQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=GGdUdTT9; spf=pass (google.com: domain of k.kapulkin@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) smtp.mailfrom=k.kapulkin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm1-x32a.google.com (mail-wm1-x32a.google.com. [2a00:1450:4864:20::32a]) by gmr-mx.google.com with ESMTPS id b6si94199wro.3.2021.07.08.05.50.20 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 08 Jul 2021 05:50:20 -0700 (PDT) Received-SPF: pass (google.com: domain of k.kapulkin@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) client-ip=2a00:1450:4864:20::32a; Received: by mail-wm1-x32a.google.com with SMTP id g8-20020a1c9d080000b02901f13dd1672aso4863894wme.0; Thu, 08 Jul 2021 05:50:20 -0700 (PDT) X-Received: by 2002:a1c:7402:: with SMTP id p2mr5029875wmc.88.1625748619852; Thu, 08 Jul 2021 05:50:19 -0700 (PDT) MIME-Version: 1.0 From: Chris Kapulkin Date: Thu, 8 Jul 2021 08:50:09 -0400 Message-ID: Subject: [HoTT] Call for Participation: HoTT/UF 2021 - July 17-18 To: algtop-l@lists.lehigh.edu, categories@mta.ca, Homotopy Type Theory , HoTT Electronic Seminar Talks Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: k.kapulkin@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=GGdUdTT9; spf=pass (google.com: domain of k.kapulkin@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) smtp.mailfrom=k.kapulkin@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: , CALL FOR PARTICIPATION Workshop on Homotopy Type Theory and Univalent Foundations July 17-18, 2021, The Internet @ Buenos Aires, Argentina https://hott-uf.github.io/2021/ 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 and Univalent Foundations: from the study of syntax and semantics of type theory to practical formalization in proof assistants based on univalent type theory. # Registration Registration is free of charge, but required. Please see https://fscd2021.dc.uba.ar/registration.html # Invited talks * Evan Cavallo (Carnegie Mellon University) Cohesive Internal Parametricity for Cubical Type Theory * Peter LeFanu Lumsdaine (Stockholm University) Categories with attributes are not full split comprehension categories * Anja Petkovi=C4=87 Komel (University of Ljubljana) Towards an Elaboration Theorem * Matthew Weaver (Princeton University) ([Directed] Higher) Inductive Types in Bicubical Directed Type Theory # Contributed talks 12 talks were accepted by the Program Committee. Their titles and abstracts are available on the event website. # Schedule The event will take place from July 17-18, 2021. The talks are scheduled 2 PM and 8 PM CEST (UTC+2). Detailed schedule is now available on the website. # Organizers * Benedikt Ahrens (University of Birmingham) * Chris Kapulkin (University of Western Ontario) --=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/CAEXhy3M7Nkaz7f%2Bg0VkZkwPaJcYGPSj%2BXJFGXSB_DH8oPftF4g%= 40mail.gmail.com.