You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Astra Kolomatskaia (Dec 01 2023 at 02:51):A new paper of mine, joint with @Mike Shulman, just went live on the arxiv!
It may be accessed here: https://arxiv.org/abs/2311.18781
We construct a new type theory in which it is possible to coinductively construct semi-simplicial types in full semantic generality. In particular, the discrete mode of our theory has semantics in any CwF with pi-types, universes, and ω-limits; any ∞-topos model will satisfy these properties. We accomplish this through a syntactic primitive called display, which is, in semantics, the fibrant counterpart of décalage on augmented semi-simplicial diagrams.
I am opening this thread to start a discussion on our results! :smile:
Chris Grossack (they/them) (Dec 01 2023 at 04:48):Congrats! ^_^
Christian Williams (Dec 08 2023 at 00:29):Wow, this is amazing! I need to read the whole paper soon; the intro is extremely clear and insightful.