This week the #HoTTEST seminar presents:
Jonathan Weinberger
Directed univalence and the Yoneda embedding for synthetic ∞-categories
The talk is at 11:30am EST (16:30 UTC) on Thursday, March 6. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html for the Zoom link, the abstract, and a list of all upcoming talks.
All are welcome!
#HoTT @carloangiuli @emilyriehl
Abstract:
In this talk, I'll present recent results in synthetic ∞-category theory in an extension of homotopy type theory. An ∞-category is analogous to a 1-category, but with composition defined only up to homotopy. To reason about them in HoTT, Riehl and Shulman proposed simplicial HoTT, an extension by a directed interval, generating the shapes that model arrows and their composition.
To account for fundamental constructions like the opposite category or the maximal subgroupoid, we add further type formers as modalities using Gratzer-Kavvos-Nuyts-Birkedal's framework of multimodal dependent type theory (MTT).
I'll present the construction of the universe 𝒮 of small ∞-groupoids in that setting which we can show to be an ∞-category satisfying directed univalence. As an application, we can define various ∞-categories of interest in higher algebra such as ∞-monoids and ∞-groups. Furthermore, I'll show the construction of the fully functorial Yoneda embedding w.r.t. 𝒮 as well as the Yoneda lemma (which is hard to establish in set-theoretic foundations). [truncated due to space considerations]
The material is joint work with Daniel Gratzer und Ulrik Buchholtz (https://arxiv.org/abs/2407.09146, https://arxiv.org/abs/2501.13229).
