Genoa, Italy, 15–16 April 2025
Co-located with the WG6 meeting (17–18 April) of the EuroProofNet COST action.
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.
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.
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.
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.
felix.cherubini@posteo.de
(Chalmers University of Technology/University of Gothenburg)tom.dejong@nottingham.ac.uk
(University of Nottingham)gratzer@cs.au.dk
(Aarhus University)mitchell.v.riley@nyu.edu
(NYU Abu Dhabi)
Villa Giustiniani-Cambiaso
Scuola Politecnica, Università di Genova
via Montallegro 1, Genova 16145
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.)