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.
Please register by filling out this form. Registration is mandatory (also if you're attending online only). Registration deadline: 28 March 2025 (AoE).
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.)