Meetings

Meeting 1:

19 November 2025, University of Nottingham 

The meeting is open to everybody. Participants from the four nodes may be offered travel reimbursement. We hope to be able to reimburse all staff and PhD students from the nodes, but if (depending on participants numbers) any budget issues arise priority will be given to PhD students and early career researchers.

Here is the Registration form, where you have the option to submit an abstract for a contributed talk.

The deadline for abstract submission is 5 November 2025.

Invited speakers:

Leonard Guetta (Utrecht University)

Nima Rasekh (University of Greifswald)

Programme 

To be announced.

Titles and Abstracts:

Leonard Guetta:

Title: Lax Functoriality of the higher Grothendieck construction and Gray ω-categories

Abstract: In this talk, I will present recent joint work with Dimitri Ara on extending the Grothendieck construction to ω-categories, with a focus on its functorial properties. I will explain how this extension naturally leads us to consider lax Gray ω-categories—a variant of ω-categories in which the interchange law holds only up to a non-invertible cell. This opens up an unexplored and exciting new direction in higher category theory. Reference: arXiv:2503.08832

Nima Rasekh:

Title: Filter Quotient Models in Homotopy Type Theory

Abstract: Since the early days of homotopy type theory (HoTT), a central goal has been to identify and classify its models, thereby clarifying the correspondence between homotopical syntax and semantics. This commenced with the simplicial model and expanded through numerous subsequent constructions, ultimately culminating in the result that every Grothendieck ∞-topos provides a model of HoTT. While this has been a significant achievement, it has long been anticipated that many potential models remain unexplored.

In this talk, I introduce a new approach to constructing models of HoTT via the filter quotient construction. Filter quotients were first introduced in category-theoretic foundations as a systematic way to construct new models, analogous to the set-theoretic forcing method. Recently, I have extended these concepts to the ∞-categorical setting, leading to the construction of filter quotient ∞-categories. I will explain how the ∞-categorical filter quotient construction preserves models of HoTT, thereby yielding an entirely new class of models. Time permitting, I will also explore how this framework can be used to produce models with tailored properties, thereby yielding new independence results.