CAUTION: The Sender of this email is not from within Dalhousie. 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ć 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/ ]