Meetings

Meeting 2:

8-9 September 2026, University of Aberdeen

Invited speakers:

Ioannis Markakis (University of Cambridge)

Paige North (Utrecht University)

Tashi Walde (University of Regensburg)

Here is the free registration form  where you have the option to submit an abstract for a contributed talk. The dealine for abstract submission is 31 August 2026.

PROGRAMME

Location: All talks are in Meston 1, in the Old Aberdeen campus. The welcome, coffee breaks and lunches are in the maths common room in Fraser Noble (first floor). The Old Aberdeen campus map can be downloaded here.

TUESDAY 8 SEPTEMBER 2026

9:00-9:30      Welcome.

9:30-10:30    Paige North (Utrecht University).

                    Title: Higher structures via homotopy type theory, part I.

10:30-11:15 Coffee break.

11:15-12:15 Tashi Walde (University of Regensburg).

                    Title: Invertibility in (∞,∞)-categories.

12:15-12:25 Group photo.

12:25-14:30 Lunch.

14:30-15:00 Matteo Spadetto (University of Nottingham).

                    Title: A conservativity proof via 2-category theory.

15:00-15:30 Ludovico Dziecielski (University of Aberdeen).

                   Title: 2.9 ways to prove a conjecture.

15:30-16:15 Coffee break.

16:15-16:45 Nicola Gambino (University of Manchester).

                   Title: Operadic 2-rigs.

18:30-- Conference dinner at Mi Amore, 80-82 Huntly St, Aberdeen AB101TD.

WEDNESDAY 9 SEPTEMBER 2026

9:30-10:30   Ioannis Markakis (University of Cambridge).

                    Title: Coinductive invertibility in higher categories.

10:30-11:15 Coffee break.

11:15-12:15 Paige North (Utrecht University).

                    Title: Higher structures via homotopy type theory, part II

12:15-14:15 Lunch.

14:15-14:45  Oumaima El Aouny (ENC Casablanca , Hassan II University Morocco).

                    Title : Derived Kan extensions and higher differentials.

14:45-15:15 Nicolai Kraus (University of Nottingham).

                    Title: Quasi-unitality, global and local.

 15:15-15:45  Owen Chan (University of Manchester).

                     Title: Hyperimaginaries and Exactness of the Pro-Completion.

15:45-16:30  Coffee break.

16:30-17:00  Aref Mohammadzadeh (University of Nottingham).

                     Title: Local and Fiberwise Classes of Maps in HoTT.

17:00-17:30 Giacomo Tendas (University of Manchester).

                    Title: Isoregular theories, accessible 2-categories, and free constructions.

ABSTRACTS

Paige North (Utrecht University) Title: Higher structures via homotopy type theory. The Equivalence Principle [1] is an informal principle asserting that equivalent mathematical objects have the same properties. For example, group theory has been developed so that isomorphic groups have the same group-theoretic properties, and category theory has been developed so that equivalent categories have the same category-theoretic properties (though sometimes other, ‘evil’ properties are considered). Vladimir Voevodsky established Univalent Foundations (also known as homotopy type theory [2]) as a foundation of mathematics (based on dependent type theory) in which the Univalence Principle, and thus the Equivalence Principle, for types (the basic objects of type theory) is a theorem. Later, versions of the Equivalence Principle for set-based structures such as groups and categories were shown to be theorems in Univalent Foundations.

In joint work with Ahrens, Shulman, and Tsementzis [3], we formulate and prove versions of the Equivalence Principle for a large class of categorical and higher categorical structures in Univalent Foundations. Our work encompasses (higher) categorical structures such as bicategories, dagger categories, opetopic categories, and more.

The Equivalence Principle in Univalent Foundations relies on the fact that the basic objects -- the types -- can be regarded as spaces. That is, Univalent Foundations can be viewed as an axiomatization of homotopy theory and as such is closely related to Quillen model category theory [4]. Univalent Foundations can also be viewed as a foundation of mathematics based not on sets, but on spaces. It is the homotopical content of this foundation of mathematics that allows us to prove something like the Equivalence Principle, something which is not possible in set-based foundations of mathematics, such as ZFC.

I will begin the lecture series with a whirlwind introduction to Univalent Foundations, and then continue on to explain how we can prove the equivalence principle in it for various structures.

References:

[1] Univalent foundations and the equivalence principle (2019), Benedikt Ahrens, Paige Randall North. https://arxiv.org/abs/2202.01892

[2] Homotopy Type Theory: Univalent Foundations of Mathematics (2013), The Univalent Foundations Program. https://homotopytypetheory.org/book/

[3] The Univalence Principle (2021), Benedikt Ahrens, Paige Randall North, Michael Shulman, Dimitris Tsementzis. https://arxiv.org/abs/2102.06275

[4] Homotopy theoretic models of identity types (2007), Steve Awodey, Michael A. Warren. https://arxiv.org/abs/0709.0248

Ioannis Markakis (University of Cambridge) Title: Coinductive invertibility in higher categories. Invertibility is a crucial notion in category theory, providing the correct notion of sameness for objects within a category and equivalences of categories. This notion readily generalises to finite-dimensional higher categories inductively by replacing equalities with higher dimensional isomorphisms. The situation becomes more subtle with infinite-dimensional categories where there are different notions of invertibility [1,2,3]. In this talk, we will give an introduction to weak ω-categories and we will study coinductively invertible cells within them [4]. We will then describe computads with invertible generators as data for freely generating ω-categories. The talk is based on a series of papers [5,6]

References:

[1] Viktoriya Ozornova, Martina Rovelli, Tashi Walde. Cores and localizations of (∞,∞)-categories. 2026

[2] Simon Henry, Felix Loubaton. An inductive model structure for strict ∞-categories. 2025

[3] David Gepner, Hadrian Heine. Homotopy Posets, Postnikov Towers, and Hypercompletions of ∞-Categories. 2026

[4] Eugenia Cheng. An ω-category with all Duals is an ω-groupoid. 2007. Applied Categorical Structures, 15(4), 439–453

[5] Christopher J. Dean, Eric Finster, Ioannis Markakis, David Reutter, Jamie Vicary. Computads for weak ω-categories as an inductive type. 2024. Advances in Mathematics (450)

[6] Thibaut Benjamin, Camil Champin, Ioannis Markakis. Computads with invertible generators for weak ω-categories. 2026

Tashi Walde (University of Regensburg) Title: Invertibility in (∞,∞)-categories. There are various ways to study (∞,d)-categories in the limit d —> ∞  and hence various kinds of objects that all deserve the name “(∞,∞)-category” in one form or another. In this talk I present joint work with V.Ozornova and M.Rovelli, where we establish and investigate some of the resulting hierarchies. In particular, we disentangle different notions of invertibility that only appear at infinity, both between (∞,∞)-categories and within any given one.

Matteo Spadetto (University of Nottingham)  Title: A conservativity proof via 2-category theory. The general theme of this talk is the relationship between the homotopical and the higher-categorical approaches to the model theory of dependent type theory. Starting from path categories and the main ideas around this notion, we focus on the 1-truncated setting and present a 2-categorical characterisation of the model theory of axiomatic type theory (that is dependent type theory with propositional computation rules) which is concrete, avoids syntax based presentations, and is suitable for explicit constructions. As an application, we consider the conservativity problem: to what extent ordinary intensional dependent type theory is stronger than its axiomatic counterpart. The 2-categorical characterisation of the semantics of the latter allows us to bypass the syntactic intricacies and visualise the construction required to transform a model of 1-truncated axiomatic type theory into a model of 1-truncated intensional type theory, producing a proof of the conservativity of the latter over the former. This is an example of how sometimes category theory can simplify arguments that are syntactically involved.

Ludovico Dziecielski, (University of Aberdeen)  Title: 2.9 ways to prove a conjecture. In this talk, I will present my recent work on the compatibility of three different solutions of Franke’s algebraicity conjecture. I will briefly explain the general ideas and methods behind the different proofs. With a focus on the most recent solution by I. Patchkoria and P. Pstrągowski, where we will see that the higher categorical approach yields to a much cleaner and more intuitive solution of the conjecture.

Nicola Gambino (University of Manchester) Title: Operadic 2-rigs. I will present joint work with M. Anel and M. Fiore (available at https://arxiv.org/abs/2607.12705), in which we show that the bicategory of operads and bimodules can be embedded into the bicategory of symmetric 2-rigs, a categorification of commutative rings. In order to do this, we introduce the notion of an operadic 2-rig and show that the full sub-bicategory of symmetric 2-rigs spanned by operadic 2-rigs has the universal property of being a completion under Eilenberg-Moore-Kleisli objects.

Oumaima El Aouny, (ENC Casablanca , Hassan II University Morocco) Title : Derived Kan extensions and higher differentials. Spectral sequences play a fundamental role in homotopy theory and derived algebra, providing powerful computational tools for extracting invariants from filtered objects and diagrams. In higher categorical settings, such as (∞,1) categories or homotopical model categories, the construction and interpretation of spectral sequence differentials require homotopy invariant methods. In this talk, we explore the role of derived Kan extensions in the construction and interpretation of higher differentials in spectral sequences arising from simplicial and cosimplicial objects. Derived Kan extensions provide a homotopically meaningful framework for extending diagrams and computing derived limits and colimits, which naturally appear in the formation of spectral sequences. We discuss how these constructions interact with homotopy limits, derived functors, and higher categorical structures. In particular, we illustrate how higher differentials can be understood through derived categorical mechanisms, highlighting their relationship with homotopy coherent diagrams and derived mapping spaces. These ideas contribute to a more conceptual understanding of spectral sequences in higher algebra and homotopical contexts, with potential applications to derived categories, higher homotopy structures, and modern homotopical algebra.

Nicolai Kraus, (University of Nottingham) Title: Quasi-unitality, global and local. A non-unital category object in a given ∞-category C with pullbacks is a semisimplicial object satisfying the Segal condition. Lurie, Harpaz and Haugseng proved, in three different but related settings, that "having identities" is a property rather than extra structure. If C is a higher topos (e.g. the topos of spaces), one can compare global and local formulations of quasi-unitality. Harpaz's formulation is local, but the comparison with Segal spaces requires completeness; Haugseng's formulation is global, and he expects that the local condition (without completeness) is strictly weaker due to missing continuity. In this talk, I will show that this is not the case provided that C is a higher topos, as continuity can be recovered. In particular, Segal spaces are equivalent to non-unital Segal spaces in which every object merely has a quasi-identity and maps preserve them. The tool that makes this work is the notion of idempotent equivalences, which I have used earlier in a type-theoretic framework and which Joachim Kock traced back to Saavedra's 1972 work.

Owen Chan, (University of Manchester) Title: Hyperimaginaries and Exactness of the Pro-Completion. An early result in categorical model theory due to Makkai connects elimination of imaginaries for a theory to the exactness of the syntactic category of said theory. Namely, a complete theory T eliminates imaginaries if and only if the category def(T) of definable sets and functions is exact. Building on Kamensky's work connecting projective limits and type-definable sets, we provide a categorical characterisation of elimination of hyperimaginaries in terms of the exactness of the pro-completion of def(T).

Aref Mohammadzadeh (University of Nottingham) Title: Local and Fiberwise Classes of Maps in HoTT.  Finitary and infinitary local classes of maps have been studied in [Lur], [GK] and [Ras]. Gepner and Kock prove that in a presentable, locally cartesian closed ∞-category the equivalence classes of univalent maps form a poset isomorphic to the poset of bounded infinitary local classes of maps. In HoTT we take, in place of infinitary locality, pullback-stability together with Σ-closedness: a class is Σ-closed when the total map of any family of its members, indexed by an arbitrary 𝒰-type, again lies in the class. The pullback-stable Σ-closed classes are exactly the fiberwise ones, those consisting of the maps whose fibers all satisfy a fixed property of types. They are therefore exactly the subuniverses. And a map is called univalent when for any two points of its base the canonical map from their identifications to the equivalences between their fibers is an equivalence. Univalence then implies that the poset of 𝒰-small univalent maps ordered by pullback is equivalent to the poset of fiberwise classes ordered by inclusion, and conversely this equivalence forces univalence of 𝒰.

Univalence also implies that every fiberwise class is local: pullback-stable and closed under gluing along pushouts. The question we ask is which maps can be built from the terminal maps of a subuniverse by pullback and pushout gluing. These are the members of the least local class whose fiberwise completion determines that subuniverse. We construct this least local class as a quotient inductive type. For a type V : 𝒰 there are then two such classes to compare: the one generated by the terminal map of V alone, and the one generated by all terminal maps in the universe. We prove that on V-bundle, the second class is no larger than the first, up to a double negation, and outright under excluded middle. We also determine the univalent maps inside the least local class generated by all terminal maps in the universe.

 References:

[GK] D. Gepner and J. Kock, Univalence in locally cartesian closed ∞-categories, Forum Math. 29 (2017), 617–652.

[Lur] J. Lurie, Higher Topos Theory, Annals of Mathematics Studies 170, Princeton University Press, 2009.

[Ras] N. Rasekh, A theory of elementary higher toposes. arXiv:1805.03805.

Giacomo Tendas (University of Manchester) Title: Isoregular theories, accessible 2-categories, and free constructions. The importance of free constructions in 2-category theory is widely recognised; think for instance about free completions under limits or colimits of some shape, as well as free regular and exact completions. A way to show that such free constructions exist is usually provided by an adjoint functor theorem. The purpose of this talk is to present a notion of 2-dimensional theory, in the sense of logic, whose 2-categories of models are good enough so that an adjoint functor theorem can actually be applied. We call the 2-dimensional theories in question isoregular. The idea being that, just like in ordinary cartesian logic one is allowed to express properties defined by unique existential quantification, within isoregular logic one can express properties defined by an existence which is unique up to (unique) isomorphism. Examples of 2-categories arising this way include those whose objects are: Categories with (co)limits of some shape, Grothendieck fibrations, Clans, Comprehension categories, and structures arising from categorical algebra. This is joint work with Nicola Gambino.

Participants:

Blackett Fiona (University of Strathclyde).

Borhani Amir (University of Aberdeen).

Chan Owen (University of Manchester).

Das Arnav (Caltech).

Du Kunhong (University of Nottingham).     

Dziecielski  Ludovico (University of Aberdeen).   

Edwards Cassia (University of Edinburgh).

El Aouny Oumaim (ENC Casablanca , Hassan II University Morocco).

Finster Eric (University of Birmingham).

Gambino Nicola (University of Manchester).

Hampl  Jakub (University of Aberdeen).       

Harington Elies (University of Nottingham) 

Hepworth-Young Richard (University of Aberdeen).

Kraus Nicolai (University of Nottingham)

Kuo-Gross Jules (University of Strathclyde).

Lemann Ezekiel (University of Aberdeen)              

Lewis Xander (University of Aberdeen).      

Markakis Ioannis (University of Cambridge).

Mohammadzadeh Aref (University of Nottingham). 

North Paige (Utrecht University).     

Paoli Simona (University of Aberdeen).

Price Ian (Swansea University).  

Raza Hassan (University of Aberdeen).     

Spadetto Matteo (University of Nottingham).

Tendas Giacomo (University of Manchester).

Toth Samuel (University of Nottingham).     

Walde Tashi (University of Regensburg).

Zhang Yuhe (University of Glasgow).   

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:

Léonard Guetta (Utrecht University)

Nima Rasekh (University of Greifswald)

Location

• Pre lunch session: Room B13 in the Xu Yafen Building, Jubilee Campus, Google Maps

• Post lunch sessions: Lecture Theatre LT1 in the Exchange Building, Jubilee Campus, Google Maps 

Travel from Nottingham train station to campus

• By taxi: exit the station at Queens Road entrance, then call a taxi

• By bus: exit at the main station entrance, then walk to Victoria Centre, then take bus 28 or 30 to Jubilee Campus.

Programme 

• 11:00 - 11:15   Welcome

• 11:15 - 12:30   Léonard Guetta: Lax Functoriality of the higher Grothendieck construction and  Gray ω-categories

• 12:30 - 14:00   Lunch break

• 14:00 - 15:15   Nima Rasekh: Filter Quotient Models in Homotopy Type Theory

• 15:15 - 16:00   Break

• 16:00 - 17:40   Introductions and speed talks by the four network  co-organizers (Eric Finster, Nicolai Kraus, Nicola Gambino, Simona Paoli) and by Calum Hughes, Giacomo Tendas, Michele Riva, Stiéphen Pradal.

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.

Participants

• Aref Mohammadzadeh (University of Nottingham )

• Axel Ljungström (University of Nottingham)

• Bruno Lindan (University of Manchester)

• Calum Hughes (University of Manchester)

• Cameron Kemp (University of Nottingham)

• Eric Finster (University of Birmingham)

• Fredrik Bakke (Norwegian University of Science and Technology (NTNU))

• Giacomo Tendas (University of Manchester)

• Ieke Moerdijk (University of Sheffield/Utrecht)

• Ishan Dasgupta Samarendra (King's College, University of Cambridge)

• Jonathan Davies (University of Nottingham)

• Kunhong Du (School of Computer Science, University of Nottingham)

• Leonard Guetta (Utrecht University)

• Mark Williams (University of Nottingham)

• Martin Ray (University of Nottingham)

• Michele Riva (University of Manchester)

• Nicola Gambino (University of Manchester)

• Nicolai Kraus (University of Nottingham)

• Nima Rasekh (University of Greiswald)

• Owen Chan (University of Manchester)

• Pouya Partow (University of Birmingham)

• Reuben Hillyard (University of Birmingham)

• Saheb Mohapatra (Durham University)

• Sam Speight (University of Birmingham )

• Samuel Toth (University of Nottingham)

• Sean Moss (University of Birmingham)

• Simona Paoli (University of Aberdeen)

• Stiéphen Pradal (University of Nottingham)

• Thorsten Altenkirch (University of Nottingham)

• Till Rampe (University of Birmingham)

• Ulrik Buckholtz (University of Nottingham)

• Zhili Tian (University of Nottingham)

Lunch Options

For the lunch break (12:30-14:00), there are several options on campus. We recommend:

• Spokes Cafe (most restaurant-like option; but please order at the till, then find a table)

• The Atrium (a canteen, basic food)

• Cafe Terrazzo (light food: loaded fries, paninis, etc)

• Aspire (just below the conference room; however, most likely extremely busy)

All options with menues can be found on this university website:

https://www.nottingham.ac.uk/hospitality/cafesbars/jubileecampus.aspx