If you have registered in time, you will receive an email in the morning of Sunday, 5 July 2020, with a link to a Zoom meeting.
If you have not received such a link, request it by sending an email to the organizers.
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.
Click here for registration for the main conferences FSCD and IJCAR.
Invited speakers
Carlo Angiuli (Carnegie Mellon University)
From raw terms to recollement In this two-part talk, I will start with an overview of the standard syntactic metatheorems of type theory, the proof techniques we have historically used to establish these properties, and how these properties are leveraged by proof assistants. In the second part, I present joint work with Jonathan Sterling and Daniel Gratzer on a synthetic method of computability for proving canonicity and normalization purely in the internal language of a glued topos. In particular, the "syntactic" and "semantic" aspects of computability families are projected via complementary open and closed modalities.
Video of the talk (YouTube)
Liron Cohen (Ben-Gurion University)
Building Effectful Realizability Models, Uniformly Constructive foundations have for decades been built upon
realizability models for higher-order logic and type theory. These
models, however, have a rather limited notion of realizability that
only supports non-termination while avoiding many other effects that
can (and should) be considered. In this talk we will present several
extensions to the standard realizability models, incorporating
non-deterministic and stateful computations, and explore their impact
on the resulting theories. Furthermore, we will introduce a new
model-theoretic tool for building such effectful realizability models
uniformly.
Video of the talk (YouTube)
Pierre-Louis Curien (Université de Paris)
A syntactic approach to opetopes, opetopic sets and opetopic categories Opetopes are shapes that were introduced by Baez and Dolan for an approach to a definition of higher categories. They can be concisely defined in the language of polynomial monads as trees whose nodes are themselves trees whose nodes etc. But opetopes are difficult combinatorial objects. I shall discuss one approach to a careful description of opetopes and, on the top of it, of two variants of opetopic sets, based on two different categories of opetopes, in which degeneracies are embodied in the objects (resp. in the morphisms). I’ll touch briefly and tentatively on the (tricky) axiomatics for higher categories via universality suggested by Eric Finster. The talk will reflect my own take on this subject, but will rely very much on joint work or continued conversations with Eric Finster, Amar Hadzihasanović, Cédric Ho Thanh and Samuel Mimram.
Video of the talk (YouTube)
