Workshop on Homotopy Type Theory / Univalent Foundations
Leuven, Belgium, April 2–4, 2024
Co-located with
the WG6 meeting of
the EuroProofNet COST
action.
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 with support for remote
participation. We encourage online participation for those who do not wish
to or cannot travel.
Invited speakers
Contributed talks
- Thorsten Altenkirch
Quotient inductive types as categorified containers
[video]
- Raymond Baker
Eckmann-Hilton and the Hopf Fibration
[slides]
[video]
- Benno van den Berg
Recent progress in the theory of effective Kan fibrations in simplicial sets
[slides]
[video]
- Ulrik Buchholtz and Johannes Schipp von Branitz
Primitive Recursive (Homotopy) Type Theory
[slides]
[video]
- Ulrik Buchholtz, J. Daniel Christensen, David Jaz Myers and Egbert Rijke
Tangent bundles and Euler classes
[slides]
[video]
- Stefania Damato and Thorsten Altenkirch
Coherences for the Container Model of Type Theory
[slides]
[video]
- Christopher Dean
Two-sided Fibration Categories
[slides]
- Jonas Frey
Factorizations on clans and monadicity
[slides]
[video]
- Sina Hazratpour and Emily Riehl
Structured Frobenius for Fibrations Defined from a Generic Point
[slides]
[video]
- Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu
Ordinal exponentiation in homotopy type theory
[slides]
[video]
- Axel Ljungström, Anders Mörtberg and Loïc Pujet
Cellular Homology and the Cellular Approximation Theorem
[slides]
[video]
- Axel Ljungström and David Wärn
The Steenrod Squares in HoTT Revisited
[slides]
[video]
- Owen Milner
Connected Covers in Cubical Agda
[slides]
[video]
- Hugo Moeneclaey
Differential Geometry in Synthetic Algebraic Geometry
[slides]
[video]
- Antoine Van Muylder, Andreas Nuyts and Dominique Devriese
Internal and Observational Parametricity for Cubical Agda
[slides]
[video]
- Jacob Neumann
A sampling of synthetic 1-category theory
[slides]
[video]
- Daniël Otten and Matteo Spadetto
Models for Axiomatic Type Theory
[slides]
[video]
- Pietro Sabelli
A topological reading of (co)inductive definitions in Dependent Type Theories
[slides]
[video]
- Andrew Swan
Towards computable homotopy theory
[slides]
[video]
- Niels Van Der Weide, Nima Rasekh, Benedikt Ahrens and Paige Randall North
Univalent Double Categories
[slides]
[video]
- Wind Wong, Vikraman Choudhury and Simon Gay
On commutativity, total orders, and sorting
[slides]
[video]
- Kobe Wullaert
A formal framework for univalent completions
[slides]
[video]
Schedule
Program committee
- Pierre Cagne (Appalachian State University)
- Evan Cavallo (University of Gothenburg)
- Felix Cherubini (Chalmers University of Technology/University of Gothenburg)
- Tom de Jong (University of Nottingham)
- Eric Finster (University of Birmingham)
- Daniel Gratzer (Aarhus University)
- Mitchell Riley (NYU Abu Dhabi)
- Michael Shulman (University of San Diego)
- Kristina Sojakova (INRIA Paris)
- Jon Sterling (University of Cambridge)
- Andrew Swan (University of Ljubljana)
- Jonathan Weinberger (Johns Hopkins University)
Organizers
- Evan Cavallo,
evan.cavallo@gu.se
(University of Gothenburg)
- Tom de Jong,
tom.dejong@nottingham.ac.uk
(University of Nottingham)
- Mitchell Riley,
mitchell.v.riley@nyu.edu
(NYU Abu Dhabi)
- Jonathan Weinberger,
jweinb20@jhu.edu
(Johns Hopkins University)
Local information
Venue
KU Leuven
Department of Computer Science
Celestijnenlaan 200A
3001 Heverlee
Leuven
Belgium
Talks: Auditorium Erik Duval, 200A.00.225
Collaborative room: Seminar room 200A.00.144
How to get
there (map).
Local information about
Leuven (and how to get there).
Code of Conduct
At the HoTT/UF Workshop we strive to ensure that participants enjoy a
welcoming environment. We seek to foster an atmosphere that encourages the
free expression and exchange of ideas. We support equality of opportunity
and treatment for all participants, regardless of gender, gender identity or
expression, race, color, national or ethnic origin, religion or religious
belief, age, marital status, sexual orientation, or disabilities.
Harassment is a form of misconduct that undermines the integrity of
HoTT/UF Workshop activities and mission. You can read more about how to
understand harassment here.
Violations may be reported confidentially to the organizers of the
workshop.
(Adapted from the AMS Policy Statement on Anti-Harassment.)
Previous HoTT/UF Workshops