From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10527 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Chris Kapulkin Newsgroups: gmane.science.mathematics.categories Subject: Call for Participation: HoTT/UF 2021 - July 17-18 Date: Thu, 8 Jul 2021 08:50:09 -0400 Message-ID: Reply-To: Chris Kapulkin Mime-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="31747"; mail-complaints-to="usenet@ciao.gmane.io" To: categories@mta.ca Original-X-From: majordomo@rr.mta.ca Fri Jul 09 01:59:59 2021 Return-path: Envelope-to: gsmc-categories@m.gmane-mx.org Original-Received: from smtp2.mta.ca ([198.164.44.75]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1m1dvz-00084F-Jw for gsmc-categories@m.gmane-mx.org; Fri, 09 Jul 2021 01:59:59 +0200 Original-Received: from rr.mta.ca ([198.164.44.159]:37118) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1m1due-0007QE-4Z; Thu, 08 Jul 2021 20:58:36 -0300 Original-Received: from majordomo by rr.mta.ca with local (Exim 4.92.1) (envelope-from ) id 1m1duS-0000XR-Q4 for categories-list@rr.mta.ca; Thu, 08 Jul 2021 20:58:24 -0300 Precedence: bulk Xref: news.gmane.io gmane.science.mathematics.categories:10527 Archived-At: 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) [For admin and other information see: http://www.mta.ca/~cat-dist/ ]