Modal Fibrations in Homotopy Type Theory
Event details
Date | 12.04.2021 |
Hour | 17:15 › 18:15 |
Speaker | David Jaz Myers, Johns Hopkins University |
Location | |
Category | Conferences - Seminars |
Spaces are not the same thing as homotopy types; after all, there is more than one function from R to R. Moreover, there are many different sorts of spaces --- topological spaces, condensed sets, smooth manifolds, schemes --- each with their own peculiar theory. We may extract a homotopy type from a space, usually by localizing at some family of ``contractible'' spaces, and use this homotopy type to study the space with algebraic methods.
Homotopy type theory is a logical system for working directly with sheaves of homotopy types as fundamental objects. Sheaves of homotopy types include spaces as representable sheaves, as well as higher spaces like orbifolds, Lie groupoids, and Deligne-Mumford stacks. The operation of taking the homotopy type forms a modality on the oo-topos of such sheaves.
In this talk, we will introduce a notion of modal fibration suitable for doing algebraic topology in modal homotopy type theory. In one sense, a modal fibration closely resembles the classical definition of a quasi-fibration --- its fibers are weakly equivalent to its homotopy fibers. This is a simple definition, but it is classically ill behaved. What we want from a fibration is the monodromy action of the homotopy type of the base on the homotopy types of the fibers, which is to say that the homotopy types of the fibers should form a local system over the base. With the magic of modal homotopy type theory, we will show that these two conditions are equivalent when both are interpreted in homotopy type theory. We will then see a trick for proving that a map is a modal fibration which may be summarized by saying that ``if it can be written as F --> E --> B, then it is a fibration''. This definition and trick work as well for higher stacks (including orbifolds) as for spaces.
Practical information
- Expert
- Free