Aarhus, Denmark, 1–2 June 2026
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 conference will be held in INCUBA Katrinebjerg (Aabogade 15, 8200 Aarhus), just north of the city center. Specifically, it is located INCUBA Next, the conference room on the top floor of the building. To reach it, simply proceed to floor 18 using the elevators at ground level.
This location is easily accessible using the 2A and 5A bus lines which run frequently and cover most of Aarhus. If you are taking local transport, we recommend usising the Rejsekort app as it is not possible to purchase tickets within the bus itself.
Submissions should consist of a title and a 1-2 pages abstract not including references, in pdf format, via EasyChair. The intended speaker has to be picked on submission.
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.
Containers in homotopy type theory
Containers, also known as polynomial functors, act as a normal form of a wide class of strictly positive data types in terms of shapes and positions. The theory of containers provides semantics for simple inductive types and inductive families. The original development of containers took place in extensional Martin-Löf type theory, with the assumption of uniqueness of identity proofs (UIP).
In HoTT, data types are not only defined in terms of their elements, but also in terms of their equalities. Such data types are collectively referred to as higher inductive types (HITs). Our long-term goal is to extend the theory of containers to provide semantics for HITs. This necessitates adapting the current literature on containers to a non-UIP setting.
In this talk, we begin by surveying the current landscape of semantics for various classes of inductive types. We then look at the different kinds of containers that have been developed in the literature, and discuss their closure properties in a setting without UIP. As a first step towards semantics for HITs, we present ongoing work on using containers to provide semantics for strictly positive quotient inductive-inductive types (QIITs), which are set-truncated HITs with induction-induction. A prerequisite to our approach is being able to model type theory via containers. We investigate the container model of type theory and its current limitations, and conclude with directions for future work.
Cohomology in realizability models of HoTT
Cohomology is well known in homotopy theory as one of the main ways of assigning algebraic invariants to spaces, and more generally to objects in higher toposes. It also has a connection with logic first studied by Blass: non trivial cohomology groups detect failures of the axiom of choice. In particular, cohomology groups of the natural numbers can be used to measure failures of countable choice. I'll give two examples of this coming from realizability. The first is the original CCHM model, by using particular characteristics of the model including the role of decidability of degeneracies and the particular construction of HITs. The second is a more natural example of cohomology witnessing the failure of countable choice in Lifschitz realizability.
Sheaves in HoTT with applications to synthetic algebraic geometry
In this talk we will give an overview of the machinery which was developed during the quest for constructive models of Synthetic Algebraic Geometry. We will avoid technical semantic considerations, and focus on what this machinery can give us, i.e. models of HoTT satisfying various additional axioms. The main applications so far are to build constructive models for synthetic algebraic geometry and synthetic Stone duality, leading to the synthetic study of Zariski sheaves and light condensed sets. We expect more applications in the future.
We will start by explaining how results from Thierry Coquand, Jonas Höfer and Christian Sattler can be used to work internally in classifying higher presheaf topoi. Their machinery takes as input an algebraic theory (e.g. the theory of rings) and as output gives a presheaf model of HoTT with a generic model (e.g. a generic ring) satisfying 3 axioms.
From these axioms we can give an internal definition for topologies and their associated sheaves. Given such an internal topology satisfying mild conditions, we will explain how to build a sheaf model of HoTT satisfying a variant of the presheaf axioms. This relies crucially on sheafification being a lex modality internal to HoTT.
We will then use this machinery to build 4 models of HoTT: the presheaf topos classifying rings, the Zariski topos, the étale topos and the fppf topos. We will contrast the additional axioms satisfied by each of these models, giving a new perspective on the ubiquitous use of these sheaf topoi in algebraic geometry.
We will conclude with some considerations on synthetic Stone duality, as well as on future applications and extensions of this framework.
felix.cherubini@posteo.de
(University of Augsburg)axel.ljungstrom@nottingham.ac.uk
(University of Nottingham)gratzer@cs.au.dk
(Aarhus University)loic@pujet.fr
(University of Strasbourg)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.)