BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Synthetic Fibered (∞\,1)-Category Theory
DTSTART:20211130T141500
DTEND:20211130T151500
DTSTAMP:20260916T064837Z
UID:325dc4bafe59a25f38b88f6d72a317e693b4a8e6406a5c59361c3361
CATEGORIES:Conferences - Seminars
DESCRIPTION:Jonathan Weinberger\, University of Birmingham\nAs an alterna
 tive to set-theoretic foundations\, homotopy type theory is a logical syst
 em which allows for reasoning about homotopical structures in an invariant
  and more intrinsic way.\n\nSpecifically\, for the case of higher categori
 es there exists an extended framework\, due to Riehl-Shulman\, to develop 
 (∞\,1)-category theory synthetically. The idea is to work internally to 
 simplicial spaces\, where one can define predicates witnessing that a type
  is (complete) Segal. This had also independently been suggested by Joyal.
 \n\nGeneralizing Riehl-Shulman’s previous work on synthetic discrete fib
 rations\, we discuss the case of synthetic cartesian fibrations in this se
 tting\, leading up to a 2-Yoneda Lemma. In developing this theory\, we are
  led by Riehl–Verity’s model-independent higher category theory\, ther
 efore adapting results from ∞-cosmos theory to the type-theoretic settin
 g. Time permits\, we’ll briefly point out generalizations to the two-sid
 ed case.\n\nIn fact\, by Shulman’s recent work on strict universes\, the
  theory at hand has semantics in Reedy fibrant diagrams in an arbitrary (
 ∞\,1)-topos\, so all type-theoretically formulated results semantically
  translate to statements about internal (∞\,1)-categories. \n\nThis is 
 based on joint work with Ulrik Buchholtz (https://arxiv.org/abs/2105.01724
 ) and the speaker's recent PhD thesis.
LOCATION:MA A1 12 https://plan.epfl.ch/?room==MA%20A1%2012
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR