Abstracts

We will start with a quick introduction to motivic homotopy theory, emphasizing the parallels to the homotopy theory of topological spaces.
We will then develop some basic motivic homotopy theory in an abstract setup: We replace the infinity category of motivic spaces by a presentable, cartesian closed infinity category (PCCC) and the multiplicative group scheme by a commutative group object G in this category. Starting from this, we will construct basic geometric objects like projective spaces, see a representation theorem for G-bundles, a Snaith type algebraic K-theory spectrum, Adams operations, rational splittings and a rational Eilenberg-MacLane spectrum.

(recording)

The results and constructions, at least the unstable ones, are closer to a formalization in homotopy type theory than usual presentations of motivic homotopy theory. Furthermore, there is an initial example of our setup, the classifying PCCC for commutative groups, which we hope to be a model for univalent homotopy type theory. Results and constructions carried out in this particular PCCC with its generic commutative group carry over to general PCCCs with commutative groups.

(recording)

I will survey the theory of gerbes and bands from the HoTT point of view and then discuss how modalities play a role in studying non-abelian cohomology.

(recording)

I will give concrete descriptions of the universes and selected subuniverses in a range of toy models of cohesion.

(recording)

Goodwillie's calculus of functors is an advanced technique in homotopy theory for interpolating between stable and unstable information. I will present the basics of the subject from the point of view of type theory, explaining its connection to the theory of lex modalities.

(recording I, recording II)

A cartesian bicategory is a bicategory B such that

1. all hom-categories have finite products, and
   
2. the full subcategory of left adjoints has finite products
   
3. which extend to a symmetric monoidal structure on B.
   

We call a cartesian bicategory closed if all pre- and postcomposition functors have right adjoints. The canonical example of a cartesian bicategory is the bicategory of categories and profunctors, where composition is given by a coends, and the closed structure by ends. I present a natural-deduction style language for cartesian bicategories which controls the "mixed variances" appearing in calculations with (co)ends via syntactic conditions on contexts and judgments.

In this talk we will synthesize the obvious presentation of the reduced suspension from "the book" and Kan's combinatorial treatment of spectra to produce a new presentation of the (∞,1)-category of spectra as weak Z-groupoids satisfying a local finiteness condition. We will follow a natural path beginning at the question of why the simplex category provides such a good nerve for categories and ending with spectra as the category of weak models for a sketch of the essentially algebraic theory of Z-groupoids; we will present a naive stable homotopy hypothesis.

(recording)

In his thesis, Penon introduced a logical topology carried by any type, and related it to infinitesimals in synthetic algebraic and differential geometry. In this talk, I will relate this intrinsic topology of types to the cohesion they gain through the modalities of cohesive type theory. We will see that a set is Liebnizian in the sense of Lawvere if and only if it is de Morgan, and that the set truncation of the shape of a type is its set of logical connected components.
(slides, screen reading version, slides, recording)

Naively, taking the degree of a polynomial should give a function from polynomials into the natural numbers. But in cohesion, most polynomial algebras of interested are connected, so this map would have to be constant. In this talk, I will discuss polynomials and vector spaces in HoTT, and the type of upper naturals in which their degrees and dimensions naturally land. We will then see that every crisp polynomial or vector space has a natural number degree or dimension.

(slides, screen reading version, slides, recording)

We introduce reflective subuniverses and modalities following the most basic example: truncations. This talk is introductory, and is aimed at familiarizing the audience with the basic concepts. We will prove the most basic properties, such as closure under pullbacks and dependent products, and we introduce the factorization system of connected maps and truncated maps.

(recording)

A type is said to be separated with respect to a reflective subuniverse if its identity types are local. The basic example is that (n+1)-truncated types are separated types for the reflective subuniverse of n-truncated types. We show that the subuniverse of separated types is again a reflective subuniverse.

(recording)

We introduce the reflective factorization system associated to a modality. Unlike the factorization system of connected and modal maps, the left class in the reflective factorization system is not stable under pullbacks. However, it satisfies the 3-for-2 property. In the basic example of the n-truncations, we show that a map is in the right class (i.e. an etale map) if and only if it is right orthogonal to the map 1 -> Sⁿ⁺¹. Using the reflective factorization system we prove a descent theorem for modalities.

(recording)

Adding systems of adjoint modal operators to homotopy(-)type(-)theory makes it an elegant and powerful formal language for reasoning about higher geometry, specifically and incrementally for a) differential topology, b) differential geometry, c) supergeometry.
The first two of these stages are discussed in other talks at this meeting.
In my talks I will:

1. describe higher supergeometry as intended categorical semantics for the full system of modalitites;
   
2. mention interesting theorems that should lend themselves to formalization in type theory;
   
3. indicate motivation from and application to the unofficial Millennium Problem of formulating M-theory (joint with Hisham Sati and Vincent Braunack-Mayer).
   

(slides, recording I, recording II)
For more see nlab-page for the talk.

While (idempotent) monadic modalities can be defined purely internally as in the HoTT book, the same is not true of comonadic modalities. The most convenient way to add comonadic modalities to to type theory is to modify the judgmental structure to reflect them, leading to a "modal type theory". I will introduce the ideas of modal type theories, and then explore in more detail the case of "cohesive type theory" which has one comonadic modality and two monadic ones in an adjoint string.

(recording)

Under the interpretation of type theory in categories and higher categories, modalities correspond to various kinds of reflective or coreflective subcategories and factorization systems, many of which arise naturally in geometric models. I will describe the categorical structures corresponding to the basic kinds of monadic and comonadic modalities, and how they arise from notions of topos-theoretic geometry such as subtoposes, concrete quasitoposes, local toposes, and cohesive toposes.

(recording)

(recording)