##### Hosted on Zoom by the
University of Birmingham

Supported by the London
Mathematical Society

**Zoom Link:**The meeting will be held online via Zoom. You can click here to join.

**Schedule (all GMT times):**

- 10:30-10:35 Welcome
- 10:35-11:20 Eric Finster (University of Birmingham)
- 11:20-12:05 Matteo Spadetto (University of Leeds)
- 12:05-13:30 Lunch break
- 13:30-14:15 Tomáš Jakl (University of Cambridge)
- 14:15-15:00 Zeinab Galal (Universiry of Leeds)

All talks are 30 minutes followed by 15 minutes of questions and discussion.

**Titles and Abstracts:**

**Speaker:**Eric Finster

**Title:**Infinitely Connected Objects

**Abstract:**One interesting aspect of ∞-topos theory which separates it from classical homotopy theory is the existence of objects which have trivial homotopy groups in every dimension, but which nonetheless are not contractible. We say such objects are

*∞-connected*. In this short talk, I will give a quick introduction to this notion and describe the main sources of examples.

**Speaker:**Matteo Spadetto

**Title:**Dialectica completion & dialectica logical principles

**Abstract:**The notion of dialectica construction associated to a finitely complete category, an attempt of providing a categorical version of Gödel's Dialectica interpretation, was introduced by de Paiva in her PhD thesis and then generalised by Hyland and Biering to an arbitrary fibration. In this talk we introduce the notion of Gödel fibration, which categorically embodies both the logical principles of traditional Skolemization and the existence of a prenex normal form presentation for every formula. A Gödel fibration is defined by a list of categorical properties, essentially saying that it has "enough" existential quantifier free and universal quantifier free predicates.

Taking advantage of Hofstra's recent work relating the generalised version of de Paiva's construction to the notions of existential and universal completion of a given fibration, we characterise the instances of the dialectica completion, showing that these are precisely the Gödel fibrations. Secondly we mention some principles and rules that are involved in the Dialectica interpretation and that these fibrations satisfy. Finally, we describe the categorical (logical) structures that behave well with respect to this construction, comparing the proof irrelevant setting to the proof relevant one. The talk is based on joint work with Davide Trotta (University of Pisa) and Valeria de Paiva (Topos Institute).

**Speaker:**Tomáš Jakl

**Title:**Game comonads and Courcelle's theorem

**Abstract:**In the recent years comonads encoding positions in model comparison

games have been successfully applied to study a range of imporatnt

notions in finite model theory and combinatorics.

I will give an overivew of the emerging theory of game comonads and

an ongoing work with Dan Marsden and Nihil Shah where we prove various

Feferman–Vaught-Mostowski-type theorems, which are behind Courcelle's

celebrated theorem.

**Speaker:**Zeinab Galal

**Title:**Finiteness species of structures

**Abstract:**Finiteness spaces were introduced by Ehrhard as a refinement of the relational model of linear logic. A finiteness space is a set equipped with a class of finitary subsets which can be thought of being subsets that behave like finite sets. A morphism between finiteness spaces is a relation that preserves the finitary structure. This model allows for a finer analysis of the computational aspects of the relational model and it provided a semantical motivation for differential linear logic and the syntactic notion of Taylor expansion. In this talk, I will present a bicategorical generalization of this construction where the relational model is replaced with the model of generalized species of structures introduced by Fiore, Gambino, Hyland and Winskel and the finiteness property now relies on finite presentability.