Skip to main content

Meeting 38

Meeting #38 of YaMCATS will happen:

23th June 2025 (University of Manchester)

This edition of YaMCATS will also be include a LMS Hardy Lectureship 2025.

Schedule

  • 13:00 -- 14:00: Daniel Gratzer
  • 14:00 -- 14:30: Coffee break
  • 14:30 -- 15:30: David Jaz Myers
  • 15:30 -- 16:00 Coffee break
  • 16:00 -- 17:00 Emily Riehl (Hardy Lecture).

Everyone is welcome to attend. However, we ask you to register by using this link, by 17:00 on Weds 18th June 2025. This will help the local organisers plan the coffee breaks, and will also facilitate the completion of the report forms required by the funders.

Venue: Alan Turing Building, University of Manchester
Room G.107.

Oxford Road train station is ~10 minutes walk, Piccadilly train station is ~25 minutes walk. Manchester Victoria train station ~40 minutes walk.

Titles and abstracts:

  • Daniel Gratzer (Aarhus University).
    • Title: On Directed Univalence in Simplicial Type Theory.
    • Abstract: In 2017, Riehl and Shulman introduced Simplicial Type Theory (STT), a type
      theory designed to axiomatize the salient features of simplicial spaces and thereby allow one to reason about $(\infty,1)$-categories. In this talk, I report on my work with Jonathan Weinberger and Ulrik Buchholtz to construct ordinary $(\infty,1)$-category theory inside STT. The first obstruction to any such development is the lack of concrete categories in STT. We rectify this state of affairs by adding a handful of additional axioms to STT which allow us to construct the category of $(\infty)$-groupoids $S$. Subsequent work by myself, Weinberger, and Buchholtz has used this category to develop a number of results concerning presheaf categories and the Yoneda embedding, but in this talk we focus on $S$ itself. Concretely, we (1) show how $S$ is defined as a particular subtype of the ordinary universe of types (2) discuss the universal property of $S$ (a version of the straightening--unstraightening correspondence) and the "directed" version of univalence it entails and (3) gloss a few consequences of $S$'s existence.

      Along the way, we observe that the definition of $S$ requires us to extend STT with several *modalities*---non-standard type formers distinguished by their comparatively poor behavior. We highlight that, in spite of the technical challenges they cause, these modalities arise naturally as we try to better capture the behavior of simplicial presheaves in type theory.

      Details on these results are contained in https://arxiv.org/abs/2407.09146 [arxiv.org].

  • David Jaz Myers Topos Institute (Oxford).
    • Title: A modal proof of the nerve theorem
      (joint work with Mitchel Riley)
    • Abstract: The nerve theorem is a classical result in homotopy theory, usually attributed to Borsuk, which computes the homotopy type of a (paracompact) topological space from a "good" open cover of it. An open cover is "good" when finite intersections of opens in the cover are contractible whenever they contain a point; the nerve of a good open cover is the simplicial complex with a point for each open in the cover, and an $n$-simplex for each inhabited intersection of opens in the cover. The nerve theorem states that the homotopy type of $X$ is the same as the nerve of any good open cover of it.

      In this talk, we'll prove the nerve theorem in the setting of modal homotopy type theory. The key concepts in the nerve theorem --- the homotopy type of a space, the homotopy type presented by a simplicial set, and even the Čech nerve itself --- may all be understood as "modalities" which act on simplicial, spatial homotopy types (that is, simplicial stacks on a suitably topological site). Once we understand the idea of modalities, we'll see that the nerve theorem is a completely modal statement concerning the commutation of two sorts of "cohesion" possible for types (in Lawvere's sense): the combinatorial cohesion of simplices, and the continuous cohesion of topology. As a result, we'll actually be proving a nerve theorem for all spatial stacks in a direct, conceptual way.

  • Emily Riehl Johns Hopkins University.
    • Title: Contractibility as uniqueness
    • Abstract: What does it mean for something to exist uniquely? Classically, to say that a set $A$ has a unique element means that there is an element $x$ of $A$ and any other element $y$ of $A$ equals $x$. When this assertion is applied to a space $A$, instead of a mere set, and interpreted in a continuous fashion, it encodes the statement that the space $A$ is contractible, i.e., that $A$ is continuously deformable to a point. This talk will explore this notion of contractibility as uniqueness and its role in generalizing from ordinary categories to infinite-dimensional categories.