Workshop on Homotopy Type Theory/ Univalent Foundations
The Internet, July 5-7, 2020
Co-located with
FSCD 2020, The Internet
How to join the workshop
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.
Videos of the talks
Available on the HoTT/UF 2020 YouTube channel.
Overview
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.
Registration
Registration is free of charge, but mandatory.
- Click here to register for HoTT/UF 2020.
- 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)
Contributed talks
Program
Program committee
- Benedikt Ahrens (University of Birmingham)
- Paolo Capriotti (Technische Universität Darmstadt)
- Chris Kapulkin (University of Western Ontario)
- Nicolai Kraus (University of Birmingham)
- Peter LeFanu Lumsdaine (Stockholm University)
- Anders Mörtberg (Stockholm University)
- Paige Randall North (Ohio State University)
- Nicolas Tabareau (Inria Nantes)
Organizers
- Benedikt Ahrens,
B.Ahrens@cs.bham.ac.uk
(University of Birmingham)
- Chris Kapulkin,
kkapulki@uwo.ca
(Western University)
Previous HoTT/UF Workshops