Skip to main content

Meeting 32

Thursday, 14th September

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

Schedule:

  • 13:00-14:00 Jack Romo (Leeds).
  • 14:00 -- 14:30: Coffee break.
  • 14:30—15:30 Stefania Damato (Nottingham).
  • 15:30 -- 16:00 Coffee break.
  • 16:00 -- 17:00 Kristina Sojakova (INRIA, Paris).

Location:

Talks will be in the Lecture Theatre 2 of the Computer Science department.

The department is a half hour walk from the centre of Cambridge, or a one hour walk from the train station. There are e-scooters available to hire, and Uber operates in the city. There is a bus from the station but it is not very frequent. If you are driving you can park in the free Park & Ride car park, which is a 5-minute walk from the department.

Titles and Abstracts:

Speaker: Jack Romo
Title: Homotopy Bicategories of Complete 2-fold Segal Spaces

Abstract:.Across the multitude of definitions for a higher category, a dividing line can be found between two major camps of model. On one side lives the ‘algebraic’ models, like Bénabou’s bicategories, tricategories following Gurski and the models of Batanin and Leinster, Trimble and Penon. On the other end, one finds the ‘non-algebraic’ models, including those of Tamsamani and Paoli, along with quasicategories, Segal n-categories, complete n-fold Segal spaces and more. The bridges between these models remain somewhat mysterious. Progress has been made in certain instances, as seen in the work of Tamsamani, Leinster, Lack and Paoli, Cottrell, Campbell, Nikolaus and others. Nonetheless, the correspondence remains incomplete; indeed, for instance, there is no fully verified means in the literature to take an `algebraic’ homotopy n-category of any known model of (∞, n)-category for general n.

In this talk, I will explore current work in the problem of taking homotopy bicategories of non-algebraic (∞, 2)-categories, including a construction of my own. If time permits, I will discuss some of the applications of this problem to topological quantum field theories.

 

Speaker: Stefania Damato
Title: A container model of type theory

Abstract: I will present ongoing work on a model of type theory via a category with families (CwF), whereby the category of contexts and substitutions is the category of set-containers (a.k.a. polynomial functors) and set-container morphisms. Unlike existing models which also make use of containers (by von Glehn, Atkey, and Kovács), in our model, types are generalised containers and terms are 'dependent' natural transformations (this approach was first proposed in a TYPES 2021 abstract by Altenkirch and Kaposi). This construction raises certain issues, such as the collection of objects in our category not being h-sets, therefore violating the definition of a CwF. I will discuss such issues and potential solutions we are considering. Our main motivation for this model is to provide semantics for (quotient) inductive-inductive types, via a process of 'containerification'.

 

Speaker:  Kristina Sojakova
Title: Syllepsis for Syllepsis: Higher Coherences in Martin-Loef Type Theory

Abstract: It is well-known that in homotopy type theory one can prove the Eckmann-Hilton theorem: any two loops p and q on reflexivity commute. If we go one dimension higher, that is, if p and q are loops on iterated reflexivity, a property known as syllepsis also holds: the Eckmann-Hilton proof for q and p is the inverse of the Eckmann-Hilton proof for p and q. We revisit the original HoTT proof of syllepsis and present it in a more conceptual way that avoids the explicit use of (too much) path algebra. This approach allows us to go further and prove higher coherences about the proof of syllepsis itself - ultimately leading to syllepsis for syllepsis.