Skip to main content

Meeting 29

Thursday December 15, 2022

 

Hosted by the University of Manchester
Supported by the London Mathematical Society

Registration (closed)

Please complete the registration form by 17:00 GMT on Friday 9th December, 2022.

Schedule:

  • 13:00-13:45: Ivan Di Liberti (University of Stockholm)
  • 13:45-14:30: Luca Mesiti (University of Leeds)
  • 14:30-15:00: Coffee break
  • 15:00-15:45: Lyne Moser (University of Regensburg)
  • 15:45-16:30: Joshua Chen (University of Nottingham)

Location:

The meeting will be held in hybrid form, it is possible to participate over Zoom or meet in person in Frank Adams 1, Department of Mathematics, Alan Turing Building, University of Manchester, Oxford Road, Manchester M13 9PL. Registration is required for both in person and remote participants.

Titles and Abstracts:

Speaker: Ivan Di Liberti
Title: The geometry of coherent topoi and ultrastructures
Abstract: It is know that for T a first order theory we can construct ultraproducts of models along ultrafilters. From a topos theoretic point of view, this property of first order logic should correspond to a geometric property of coherent topoi. We discover such geometric property and we see how that impacts the behavior of coherent topoi. We show that coherent topoi are right Kan injective with respect to flat embeddings of topoi. We recover the ultrastructure on their category of points as a consequence of this result. We speculate on possible notions of ultracategory in various arenas of formal model theory.

References.
Di Liberti, The geometry of coherent topoi and ultrastructures. arXiv:2211.03104
Makkai, Stone duality for first order logic. Advances in Mathematics.
Lurie, Ultracategories.

Slides: here

Speaker: Luca Mesiti
Title: Lax normal conical 2-limits and the Grothendieck construction
Abstract: As it is usually understood, when one moves to dimension 2, or in general to an enriched setting, there is the need to consider weighted limits, as conical limits do not suffice anymore. However, for 2-categories, weighted 2-limits are not the only solution to the problem. There is indeed another idea that might come up: relaxing the concept of cone to admit coherent 2-cells inside. After briefly recalling the definition of weighted enriched limit, we will describe the problem of conicalizing weighted 2-limits. Such problem has, strictly speaking, no solution. But we will search for some essential solution to it, accepting the cones to have 2-cells inside.

Our wish to find an essential solution to the problem of conicalizing weighted 2-limits will simultaneously create an extension of the Grothendieck construction and the relaxed notion of conical 2-limit that we need. We call the latter lax normal conical 2-limit, and show that every weighted 2-limit can be reduced to one of this form. The process itself will justify the Grothendieck construction and reveal its bond with the laxness.We will then study the extended Grothendieck construction and the corresponding extended notion of fibration from a more abstract point of view. But the laxness that permeates the Grothendieck construction will force us to move out of 2-CAT , in order to consider lax natural transformations.

We will see that the pointwise Kan extensions are the key to the meaning of the Grothendieck construction. But there is no known definition of pointwise Kan extension in this weaker version of 2-CAT , and so we will firstly propose one. A generalized lax but not too lax version of the parametrized Yoneda lemma will help us with this, along with offering a better understanding of what it means to be lax normal.

Slides: here

Speaker: Lyne Moser
Title: Representation theorem for enriched categories
Abstract: Universal properties play an important role in mathematics, as they allow us to make many constructions such as (co)limits, Kan extensions, adjunctions, etc. In particular, a universal property is often formulated by requiring that a certain presheaf is representable. The representation theorem gives a useful characterization of these representable presheaves in terms of initial objects in their category of elements. Going one dimension up and considering 2-categories, with tslil clingman we showed that the same results is true for Cat-valued presheaves if one considers their ``double category of elements’’. In this talk, I will explain how to generalize the representation theorem to the more general framework of V-enriched categories, where V is a cartesian closed category. This is joint work with Maru Sarazola, and Paula Verdugo.

Slides: here

Speaker: Joshua Chen
Title: On internal models of type theory and constructions of Reedy fibrant diagrams
Abstract: A current major obstruction to the use of standard homotopy type theory as a language for ∞-category theory is the longstanding open problem of constructing semisimplicial objects in the universe of types. Numerous attempts and a number of clever proposals have all eventually run up against essentially the same wall: we have not yet found a way of internalizing the tower of coherence conditions required for a correct definition of the [n]-matching type for arbitrary n.

Seemingly distinct is the open problem of whether or not the universe type of HoTT models HoTT itself, or, phrased alternatively, if one may find a suitable notion of "model of type theory" that classes both the syntactic model and the so-called "standard model" of the universe as examples.

In joint work with Nicolai Kraus we suggest the following line of investigation: taking HoTT as our ambient metatheory, we consider internal models of type theory and construct semisimplicial types (and more general Reedy fibrant diagrams) in them. The case when the internal model is set-truncated may be viewed as an inversion of the two-level type theoretic setting, and already here the construction of diagrams requires somewhat more work than in 2LTT. One aim of this program is to later relax the truncation levels in order to yield higher internal models of type theory with proof-relevant judgmental equality, and to move our constructions into these new settings. Along the way, we prove half of an equivalence between the two open problems mentioned previously: HoTT models its own metatheory only if semisimplicial types are constructible; and also speculate on possible formulations of the coherence problem for semisimplicial types.

Slides: here