Workshop on Homotopy Type Theory / Univalent Foundations 2025 (original) (raw)
Genoa, Italy, 15–16 April 2025
Co-located with the WG6 meeting (17–18 April) 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
- Reid Barton (Carnegie Mellon University, USA)
Geometric homotopy theory via simplicial sets
[slides] [video]
Classical algebraic topology connects what we might today regard as two distinct subjects: “pure” homotopy theory, of the sort that has been extensively developed in homotopy type theory, and the geometry of spaces like manifolds and the classical Lie groups. This connection has been very fruitful in both directions. One famous application of geometric topology to “pure” homotopy theory is the proof of the Hopf invariant one theorem by Adams and Atiyah using topological K-theory and the Adams operations.
Currently, we don't know whether it's possible to construct the homotopy types of (say) the unitary groups and their classifying spaces within ordinary homotopy type theory. An extension of type theory called real-cohesion is designed to give a synthetic account of exactly these kinds of geometric constructions. But what happens in extensions of type theory intended for other purposes, such as higher category theory or condensed mathematics? Perhaps these other extensions also enable such geometric constructions (even if not by design)?
In this talk, I will propose a few simple axioms on a distinguished “interval” type along with a distinguished subuniverse of types called “shapes”. Using these axioms, I'll explain how to associate shapes to certain geometric objects defined by polynomial equations, by adapting methods from traditional algebraic topology and model theory. As an application, I will outline some first steps towards the construction of topological K-theory. However, the main purpose of the talk is to give an account of the relationship between a simplicial set and the ∞-groupoid it represents from within homotopy type theory. - Bastiaan Cnossen (University of Regensburg, Germany)
Axiomatization of ∞-categories
[slides] [video]
I'll discuss our proposed axiomatization of synthetic categories that allows us to develop most of (∞-)category theory from first principles, without relying on explicit set-theoretic models. We expect that such a synthetic theory can make it easier to practice (∞-)category theory for non-experts and teach it to beginners; moreover, it allows for type theoretic interpretation and thus lends itself to formalization in proof assistants. This talk is based on ongoing collaborative work with D.-C. Cisinski, K. Nguyen and T. Walde. - Ambrus Kaposi (Eötvös Loránd University, Hungary)
Strictification of categories with families
[slides] [video]
The syntax of type theory can be viewed as the initial model, e.g. the initial category with families (CwF) with certain type formers. This is a fruitful viewpoint: the initial model does not need to be constructed by hand, it is just a quotient inductive-inductive type; ad-hoc syntactic details don't hide the forest from the trees; normalisation is proven by a concise gluing argument. However, implementing normalisation for the initial model in a proof assistant was so far out of reach. The main reason for this is the so-called “transport hell”: conversion rules (equality constructors) are required to make some operations well-typed, then transports appear on these operations which have to be manipulated by hand. In contrast, lots of these equations are definitional in a raw term presentation of the syntax (because e.g. substitution is defined recursively on raw terms), making transports unnecessary.
In this talk I will explain a technique which strictifies a contextual CwF with extra structure, making all substitution rules (and more) definitional. By strictification we do not mean turning isomorphisms into equalities, but turning propositional equalities into definitional ones. We do not turn beta/eta rules for type formers definitional, only the CwF equations and the substitution rules for each type former. The technique is based on the presheaf interpretation of higher-order abstract syntax and uses prefascist sets by Pédrot. I will demonstrate the practical usability of the technique by an Agda formalisation of the CwF-based syntax together with a canonicity construction.
This is joint work with Loïc Pujet.
Contributed talks
- Gianluca Amato, Matteo Calosci, Marco Maggesi and Cosimo Perini Brogi
Introducing Displayed Universal Algebra in UniMath
[slides] [video] - Fredrik Bakke
The Cantor–Schröder–Bernstein Theorem in ∞-topoi
[slides] [video] - Evan Cavallo and Christian Sattler
The algebraic small object argument as a saturation
[slides] [video] - Thierry Coquand, Jonas Höfer and Christian Sattler
Progress report on constructive higher presheaf models of HoTT
[slides] [video] - Daniel Gratzer, Jonathan Weinberger and Ulrik Buchholtz
The Yoneda embedding in simplicial type theory
[slides] [video] - Perry Hart and Kuen-Bang Hou Favonia
A note on left adjoints preserving colimits in HoTT
[slides] [video] - Hugo Herbelin and Ramkumar Ramachandra
About the construction of simplicial and cubical sets in indexed form: the case of degeneracies
[slides] [video] - Tom Jack and Axel Ljungström
Towards computing the second stable homotopy group of spheres in HoTT
[slides] [video] - Philipp Joram and Niccolò Veltri
Data Types with Symmetries via Action Containers
[slides] [video] - Krzysztof Kapulkin and Yufeng Li
Extensional concepts in intensional type theory, revisited
[slides] - Louise Leclerc
Towards a type theory for (∞, ω)-categories
[slides] [video] - Titouan Leclercq and Andrew Swan
Oracle modalities for higher dimensional types
[slides] [video] - Axel Ljungström and Loïc Pujet
Hurewicz and Brouwer
[slides] [video] - Axel Ljungström
Some properties of Whitehead products
[slides] [video] - Jem Lord
Easy Parametricity
[slides] [video] - Hugo Moeneclaey and Thierry Coquand
Chatelet's Theorem in Synthetic Algebraic Geometry
[slides] [video] - Andreas Nuyts
Transpension for Cubes without Diagonals
[slides] [video] - Vojtěch Štěpančík
Towards a formalization of Wärn's zigzag construction
[slides] [video] - Fedor Part, Valery Isaev and Sergey Sinchuk
The Arend theorem prover
[slides] [video] - Johannes Schipp von Branitz and Ulrik Buchholtz
Propositional Geometric Type Theory
[slides] [video] - Andrew Swan
Computable and non-computable 2-groups in HoTT
[slides] [video] - Mark Williams
Projective Presentations of Lex Modalities
[slides] [video]
Schedule
Program committee
- Ulrik Buchholtz (University of Nottingham)
- Pierre Cagne (Applachian State University)
- Dan Christensen (The University of Western Ontario)
- Felix Cherubini (Chalmers University of Technology/University of Gothenburg)
- Tom de Jong (University of Nottingham)
- Jonas Frey (Université Sorbonne Paris Nord)
- Daniel Gratzer (Aarhus University)
- Philipp Haselwarter (Aarhus University)
- András Kovács (University of Gothenburg)
- Anja Petković Komel (TU Wien)
- Loïc Pujet (University of Stockholm)
- Mitchell Riley (NYU Abu Dhabi)
Organizers
- Felix Cherubini,
felix.cherubini@posteo.de(Chalmers University of Technology/University of Gothenburg) - Tom de Jong,
tom.dejong@nottingham.ac.uk(University of Nottingham) - Daniel Gratzer,
gratzer@cs.au.dk(Aarhus University) - Mitchell Riley,
mitchell.v.riley@nyu.edu(NYU Abu Dhabi)
Local information
Venue
Villa Giustiniani-Cambiaso
Scuola Politecnica, Università di Genova
via Montallegro 1, Genova 16145
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.)