![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > Synthetic fibered (∞,1)-category theory
Synthetic fibered (∞,1)-category theoryAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Benedikt Ahrens. As an alternative to set-theoretic foundations, homotopy type theory is a logical system which allows for reasoning about homotopical structures in an invariant and more intrinsic way. Specifically, for the case of higher categories 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. Generalizing Riehl—Shulman’s previous work on synthetic discrete fibrations, we discuss the case of synthetic cartesian fibrations in this setting, leading up to a 2-Yoneda Lemma. In developing this theory, we are led by Riehl—Verity’s model-independent higher category theory, therefore adapting results from ∞-cosmos theory to the type-theoretic setting. If time permits, we’ll briefly point out generalizations to the two-sided case. In 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. This is based on joint work with Ulrik Buchholtz https://arxiv.org/abs/2105.01724 and the speaker’s recent PhD thesis. This talk is part of the Theoretical computer science seminar series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsMet and Mat Seminar Series Condensed Matter Group Meetings Artificial Intelligence and Natural Computation seminarsOther talksThe development of an optically pumped magnetometer based MEG system Hodge Theory: Connecting Algebra and Analysis Modelling uncertainty in image analysis. TBC Sensing and metrology activities at NPL, India Geometry of alternating projections in metric spaces with bounded curvature |