Workshop on Homotopy Type Theory/ Univalent Foundations

Haifa, Israel, July 31 - August 1, 2022

Co-located with FSCD 2022, Haifa, Israel

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.

The workshop will be held in person, and remote participation will be supported. Any streamed material will be available at this Zoom room.

Submissions

Submissions should consist of a title and an abstract of no more than 2 pages in pdf format, via EasyChair.

Abstract submission deadline: ~~10 May 2022~~ 15 May 2022
Author notification: mid June 2022

Considering the broad background of the expected audience, we encourage authors to include information of pedagogical value in their abstract, such as motivation and context of their work.

Registration

Registration is mandatory. Please register on the registration site of FSCD.

Invited speakers

Sunday:

Kristina Sojakova (INRIA Paris): Towards Syllepsis for Syllepsis: Higher Coherences in Homotopy Type Theory
Taichi Uemura (Stockholm University): Internal languages of diagrams of ∞-toposes (Notes)

Monday:

Eric Finster (University of Birmingham): The (∞,1)-category of Types

Contributed talks

Sunday:

Maximilian Doré Elementary Simplicial Collapses in Cubical Agda
Felix Cherubini Towards computing cohomology of dependent abelian groups
Benedikt Ahrens, Ralph Matthes and Kobe Wullaert A Library of Monoidal Categories for Display and Univalence
Jarl G. Taxerås Flaten The internal AB axioms
Elif Uskuplu An Experiment with 2LTT Features in Agda

Monday:

Jonathan Weinberger, Benedikt Ahrens, Ulrik Buchholtz and Paige North Towards Normalization of Simplicial Type Theory via Synthetic Tait Computability
Jacob Neumann Towards Directed Higher Observational Type Theory
Michele Contente and Maria Emilia Maietti The Compatibility of MF with HoTT
Benedikt Ahrens, Paige North and Niels van der Weide Semantics for two-dimensional type theory
El Mehdi Cherradi Models of homotopy type theory from the Yoneda embedding
Evan Cavallo and Christian Sattler A type-theoretic model structure over cubes with one connection presenting spaces
Sam Speight Groupoidal Realizability: Formalizing the Topological BHK Interpretation

Program

See the FLoC 2022 program.

Program committee

Benedikt Ahrens (TU Delft and University of Birmingham)
Carlo Angiuli (Carnegie Mellon University)
Evan Cavallo (Stockholm University)
Chris Kapulkin (University of Western Ontario)
Nicolai Kraus (University of Nottingham)
Peter LeFanu Lumsdaine (Stockholm University)
Anja Petković Komel (TU Wien)
Paige Randall North (University of Pennsylvania)
Christian Sattler (Chalmers University of Technology)
Michael Shulman (University of San Diego)
Théo Winterhalter (Max Planck Institute, Bochum)

Organizers

Benedikt Ahrens, B.Ahrens@cs.bham.ac.uk (University of Birmingham)
Evan Cavallo, evan.cavallo@math.su.se (Stockholm University)
Chris Kapulkin, kkapulki@uwo.ca (Western University)
Anja Petković Komel, anja.komel@tuwien.ac.at (TU Wien)
Paige Randall North, pnorth@upenn.edu (University of Pennsylvania)