BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Modal Fibrations in Homotopy Type Theory
DTSTART:20210412T171500
DTEND:20210412T181500
DTSTAMP:20260929T053340Z
UID:0c432e2d6955ad57de92129f638d5a5f93e56ddf2458d9d2821cc3db
CATEGORIES:Conferences - Seminars
DESCRIPTION:David Jaz Myers\, Johns Hopkins University\nSpaces are not the
  same thing as homotopy types\; after all\, there is more than one functi
 on from R to R. Moreover\, there are many different sorts of spaces --- t
 opological spaces\, condensed sets\, smooth manifolds\, schemes --- each 
 with their own peculiar theory. We may extract a homotopy type from a spa
 ce\, usually by localizing at some family of ``contractible'' spaces\, an
 d use this homotopy type to study the space with algebraic methods.\n\nHo
 motopy type theory is a logical system for working directly with sheaves o
 f homotopy types as fundamental objects. Sheaves of homotopy types includ
 e spaces as representable sheaves\, as well as higher spaces like orbifol
 ds\, Lie groupoids\, and Deligne-Mumford stacks. The operation of taking 
 the homotopy type forms a modality on the oo-topos of such sheaves.\n\nIn
  this talk\, we will introduce a notion of modal fibration suitable for do
 ing algebraic topology in modal homotopy type theory. In one sense\, a mo
 dal fibration closely resembles the classical definition of a quasi-fibra
 tion --- its fibers are weakly equivalent to its homotopy fibers. This is
  a simple definition\, but it is classically ill behaved. What we want fr
 om a fibration is the monodromy action of the homotopy type of the base o
 n the homotopy types of the fibers\, which is to say that the homotopy ty
 pes of the fibers should form a local system over the base. With the magi
 c 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 b
 e summarized by saying that ``if it can be written as F --> E --> B\, the
 n it is a fibration''. This definition and trick work as well for higher 
 stacks (including orbifolds) as for spaces.
LOCATION:World Wide Web https://epfl.zoom.us/j/94351048760
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR