Category Theory
Zulip Server
Archive

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.

Stream: learning: questions

Topic: Motivation for modal HoTT

Madeleine Birchfield (Mar 21 2025 at 17:12):

One of my motivations for learning modal HoTT is the ability to do $(\infty,1)$ -category theory without having to deal with model categories or simplicial enrichment or whatever. The hope here is that eventually the theory gets developed enough that I am able to define the $(\infty,1)$ -topos of $(\infty,1)$ -sheaves on the $(\infty,1)$ -site of Cartesian spaces and smooth functions $\mathrm{Sh}_{(\infty,1)}(\mathrm{CartSp}_\mathrm{smooth})$ , and use the resulting $(\infty,1)$ -topos as an environment in which to do physics.

Chris Grossack (she/they) (Mar 21 2025 at 17:13):

Sure, but where does the modality come in? I'm already sold on HoTT and special-purpose variants being useful as an internal logic for various (oo,1)-topoi, and this is hugely influential in how I think about oo-categories... I'm curious what exactly the modalities buy you, but maybe I should spend more time reading the nlab since the answer is probably in there somewhere

Madeleine Birchfield (Mar 21 2025 at 17:16):

Chris Grossack (she/they) said:

Sure, but where does the modality come in? I'm already sold on HoTT and special-purpose variants being useful as an internal logic for various (oo,1)-topoi, and this is hugely influential in how I think about oo-categories... I'm curious what exactly the modalities buy you, but maybe I should spend more time reading the nlab since the answer is probably in there somewhere

In simplicial / triangulated type theory, they need modalities to construct the opposite $(\infty,1)$ -category, the twisted arrow $(\infty,1)$ -category, and the amazing right adjoint, as well as the flat and shape modalities for the core $(\infty,1)$ -category and localisation at the directed interval. Those modalities are needed to prove the Yoneda embedding and to construct the directed univalent universe of $\infty$ -groupoids as an $(\infty,1)$ -category, as well as the type of higher algebraic objects such as the type of coherent $\infty$ -monoids and the type of spectra.

Madeleine Birchfield (Mar 21 2025 at 17:17):

See the two papers by Gratzer et al:

Madeleine Birchfield (Mar 21 2025 at 17:21):

I don't know how many of the modalities will actually be used in defining an $(\infty,1)$ -topos of $(\infty,1)$ -sheaves on some $(\infty,1)$ -site and constructing the differential cohesion adjoint quadruples.

Madeleine Birchfield (Mar 21 2025 at 17:34):

We are probably going to use at least every modality used to construct the directed univalent universe of $\infty$ -groupoids $\mathcal{U}$ as well as the opposite modality, since both are used in the definition of an $(\infty,1)$ -presheaf $F:S^\mathrm{op} \to \mathcal{U}$ .

Notification Bot (Mar 21 2025 at 19:53):

A message was moved here from #learning: questions > Why care about differential cohesive (oo-)topoi? by Madeleine Birchfield.

Notification Bot (Mar 21 2025 at 19:53):

6 messages were moved here from #learning: questions > Why care about differential cohesive (oo-)topoi? by Madeleine Birchfield.

Madeleine Birchfield (Mar 21 2025 at 19:57):

I moved the messages here because $\mathrm{Sp}_{(\infty,1)}(\mathrm{CartSp}_\mathrm{smooth})$ only has smooth cohesion rather than differential cohesion.

Madeleine Birchfield (Mar 21 2025 at 20:00):

Apparently, one needs $\mathrm{Sp}_{(\infty,1)}(\mathrm{CartSp}_\mathrm{synthdiff})$ for differential cohesion. The nLab says in [[CartSp]] that the site $\mathrm{CartSp}_\mathrm{synthdiff}$ is the

full subcategory of the category of smooth loci on those of the form $\mathbb{R}^n \times D$ for $D$ an infinitesimal space (the formal dual of a Weil algebra)