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.
Marco Vianello (Jun 25 2026 at 14:59):Recently I've been familiarizing myself with the theory of smooth sets as presented in arxiv:2312.16301, arxiv:2512.22816 (in the following, fthg1 and 2) as well as in Urs Schreiber's online textbook. My motivation mainly comes from the desire to explore a rigorous formulation for classical field theory.
I plan to spend the next few months learning the abstract theory of cohesive toposes. I started from the relevant section of Prof. Schreiber's book, and my ultimate goal is to gain some familiarity with the "convenient" homotopical generalization of arxiv:1310.7930 (henceforth, dcct).
Would anybody be interested in joining me? I've found that my energies alone are not enough to learn this material thoroughly, and I think a small study group would make the process much more enjoyable.
I already sketched an preliminary study plan in my head, but I'm quite flexible.
For example[1], I'm becoming increasingly intrigued by the "synthetic" side of the story as developed in arxiv:1408.0054 and (in particular) arxiv:1509.07584. If others here are more drawn to this perspective, I'd be happy to orient our efforts in that direction.
Let me know:)
[1] Indeed, this is what prompted me to post here.
fosco (Jun 25 2026 at 17:23):Urs isn't here, but he would be an amazing study buddy!
Marco Vianello (Jun 25 2026 at 18:28):Ideally I was hoping to find one at roughly my own level, but hey, if someone is willing to do advisor work I will not refuse! (Basically this is the kind of work that in an ideal world could converge into a thesis.)
Alonso Perez-Lona (Jun 29 2026 at 16:53):Marco Vianello said:
For example[1], I'm becoming increasingly intrigued by the "synthetic" side of the story as developed in arxiv:1408.0054 and (in particular) arxiv:1509.07584. If others here are more drawn to this perspective, I'd be happy to orient our efforts in that direction.
Hi Marco,
Coincidentally, this is something that has caught my eye recently too. It would be great to find others intersted, and I am happy to discuss further regardless.
Marco Vianello (Jun 30 2026 at 09:17):Hi Alonso, I'm planning to set up a quick call soon with the other two people who contacted me, to get a sense of our backgrounds and goals and such. You're invited!
I think at this point everybody who contacted me would be quite happy to go down this road at least for while.
I lack a type theory background and I'm unable to judge whether, say, arxiv:1509.07584 is the right place where to start. But we will figure it out in some way or another I guess.
John Baez (Jun 30 2026 at 09:29):It really depends on whether you want to learn homotopy type theory as well as cohesive geometry. You don't need to study them together, though they do fit together rather nicely - you can roughly think of cohesive homotopy type theory as a way to formalize cohesive geometry which relies on the new foundation of mathematics called homotopy type theory. I believe your initial list of references didn't mention homotopy type theory, so they would provide a way to learn some cohesive geometry that doesn't bring in that other subject.
You might consider trying to get a feel for cohesive geometry before adding type theory to the mix. If one of you decides you love type theory, maybe it could help you move faster. There are certainly type theorists who would take that approach.
Marco Vianello (Jun 30 2026 at 15:23):I jotted down a few ideas on what I would like to get from the reading group before posting, but until now I just sent them privately to those who reached me out hoping to "keep the doors open" as much as possible. As you can see, there is no super precise plan on what to learn up to now.
As I said above, one thing I'm looking to become comfortable with is the theory of smooth sets. This has not much to do with abstract cohesive geometry in general, but it's probably a model worth familiarizing with even if one does not care about field theory. So one goal for the reading group that comes to my mind could be
I haven't had the time/energy to get too far up to now (enough to understand, say, the notion of differential form/Lagrangian density in this context plus some analytical subtleties).
Another cool resource on this material is an online textbook by Urs. In particular, there's a section with quite a bit of material on cohesive (1,1)-toposes, and another one on modal operators that is worth reading. So, one more humble goal could be
Urs' arxiv:1310.7930 (dcct) also contains a lot of material on cohesive toposes. While not still driven by the desire to learn more about the physics myself at this point, I find very tempting the idea of learning the "convenient" homotopy generalization of the theory to Sh_\infty(Man) as surveyed, say, here on yt. I admittedly don't know much homotopy theory at the moment, so, if participants are more attracted to dcct than the other resources I suggested, I my proposal is to
If we decide to tackle the abstract theory of cohesion as it appears on dcct and we are serious about building the required foundations in homotopy theory, I wounder whether taking the "synthetic" path to (\infty,1)-cats would bring somewhere. There are those lectures by Cnossen et al. that are quite popular nowadays.
In the same vein, as I anticipated above, depending on participants tastes there's also the possibility to dig a bit into the flavors of HoTT designed to be the "synthetic" side of this story. I come from a math/physics background and while I do have some passing familiarity with HoTT in cubical Agda this is still terra incognita for me. Nevertheless I would be glad to
if someone's interested.
Marco Vianello (Jun 30 2026 at 15:31):It also look like one the participants will be a type theorist so we will probably be taking this path (who knows, maybe this is the time I finally learn some type theory after having been a bit "conservative" (?) up to now)
Marco Vianello (Jun 30 2026 at 15:38):One thing that gives me pause is the fact that the quest for the "right" type theory of cohesive spaces seems to be far from settled (the theories available up to now have not been implemented in a proof assistant, am I right?). This is one point I'd really like to learn more about.
Benjamin Le (Jul 07 2026 at 14:56):I suspect modalities are the structural backbone of pretty much many things - they carve out discrete, cohesive, differential, and supergeometric layers of quantum physics (from Urs's book). Adjunctions are the engine inside every modality. And the natural language for adjunctions is string diagrams (it seems we have papers on that). Urs once mentioned that adjunctions are the "meat" of category theory.
I'm pursuing a "semantics-first" approach: learn the visual, diagrammatic calculus before the formal syntax, so the meaning is grounded in spatial intuition (I hope so). This is the path I'm walking, and I'd love to connect with others who see mathematics this way or are curious to explore it.
(This is a personal vision, not a textbook truth. I'm an independent learner, not an academic. But the pieces fit beautifully, and I think the diagrammatic route is worth mapping.)
Marco Vianello (Jul 07 2026 at 16:36):Here is the link to a DIscord group I made to keep in touch for the moment: https://discord.gg/vVNeCAQtz. Feel free to join.
Mike Shulman (Jul 25 2026 at 19:19):Marco Vianello said:
the theories available up to now have not been implemented in a proof assistant, am I right?
I believe this was true when you wrote it, but not any more! The experimental proof assistant Narya now implements generic multimodal type theory, which can be specialized to any modal type theory desired. The mode theory has to be built into the proof assistant at compile-time, but it's relatively easy to implement new mode theories (especially with AI assistance), so if the one you want isn't available yet, just let me know! Right now the available theory most relevant to cohesion is "spatial type theory" with as in my original paper on real-cohesive HoTT; there's also a two-mode version of it representing a local geometric morphism with .