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: deprecated: topos theory

Topic: Monoidal topos

Callan McGill (Nov 10 2022 at 03:22):

The nlab defines a monoidal topos as a topos equipped with a monoidal structure. This definition seems quite unsatisfying to me since I think monoidal topos should be something where you can interpret some form of linear type theory / linear higher order logic and as such it should be closed under some form of self-indexing (and so satisfy some analogous result to the fundamental theorem of topos theory that every slice category is also a topos). Are there some proposed alternatives for how to combine the monoidal and cartesian structure over a topos that is more promising on this front?

Notification Bot (Nov 10 2022 at 09:36):

This topic was moved here from #theory: category theory > Monoidal topos by Morgan Rogers (he/him).

Morgan Rogers (he/him) (Nov 10 2022 at 09:53):

The motivation for considering monoidal toposes with that definition is that they arise naturally from monoidal categories: if I take presheaves on a small category with a monoidal product, the topos of presheaves inherits a monoidal structure via [[Day convolution]] which extends the monoidal product on the original category. This tensor product interacts well with colimits, so one might refer to a monoidal topos constructed in this way as a "Day topos", but I think it will fail to be stable under slicing if the monoidal product didn't lift to slices in the original category.
Do you have an example in mind of a topos with a monoidal product (which is not cartesian or cocartesian, say) where stronger properties hold? To me, the Day convolution construction is pretty good justification for keeping a fairly open definition.

Matteo Capucci (he/him) (Nov 10 2022 at 10:48):

Callan McGill said:

The nlab defines a monoidal topos as a topos equipped with a monoidal structure. This definition seems quite unsatisfying to me since I think monoidal topos should be something where you can interpret some form of linear type theory / linear higher order logic and as such it should be closed under some form of self-indexing (and so satisfy some analogous result to the fundamental theorem of topos theory that every slice category is also a topos). Are there some proposed alternatives for how to combine the monoidal and cartesian structure over a topos that is more promising on this front?

I think the 'fundamental theorem' still holds but it requires a bit of care to state: ${\cal E}/X$ is a monoidal topos if $\cal E$ is and $X$ is a either a monoid or a comonoid wrt to that.
Indeed you can define

$$(Y \to X) \boxtimes (Z \to X) = Y \otimes Z \to X \otimes X \overset{*}\to X$$

where $* :X \otimes X \to X$ is the multiplication, or

$$(Y \to X) \odot (Z \to X) = \delta^*(Y \otimes Z) \to X$$

where $\delta : X \to X \otimes X$ is the comultiplication

Mitchell Riley (Nov 10 2022 at 10:52):

I don't have a replacement for the notion of monoidal topos, but this seems like a good place to share an idea. The type theory I describe in my thesis works for a particular kind of monoidal topos; one which is infinitesimally cohesive over the base. That is, the global sections functor has a left and right adjoint that are equal, and fully faithful.

I think we could cook up a type theory for a general monodial topos by mashing the theory in my thesis with the theory for a general geometric morphism, as in Section 3 of @Colin Zwanziger's paper here. Briefly, the idea is to have a context of shape $\Delta \mid \Gamma \,\,\mathsf{ctx}$ where $\Delta$ is a set and $\Gamma$ is a morphism $\Gamma \to \mathrm{Disc} \Delta$. The $\otimes$-type would take as inputs two types $\Delta \mid \cdot \vdash A \,\,\mathsf{type}$ and $\Delta \mid \cdot \vdash B \,\,\mathsf{type}$, and give $\Delta \mid \Gamma \vdash A \otimes B \,\,\mathsf{type}$. This would be interpreted as a fibred tensor product: the objects $A$ and $B$ decompose into the $\Delta$-indexed coproduct of $A_i$ and $B_i$, which then have the monoidal product applied pointwise. The actual linearity restrictions on the variables in $\Gamma$ would be tracked as in my thesis, using an auxillary 'palette' idea.

Alternatively, we could keep everything in the same topos and use '$\flat$' as in spatial type theory, but the rules would need to be adjusted to make $\flat$ non-idempotent. This has the advantage of allowing a nice 'dependent external tensor product' as mentioned here, by allowing the context of $B$ above to be $\Delta, x : A \mid \cdot \vdash B \,\,\mathsf{type}$.

Callan McGill (Nov 10 2022 at 19:00):

@Morgan Rogers (he/him) I don’t view slice categories as fundamental in themselves. The importance seems to be that the fundamental fibration gives a self indexing of a topos indexed in toposes. That relies on Cartesian morphisms being pullbacks and gets structure from a topos being LCCC. So I would view slices as related to Cartesian structure. What I would hope for I some sort of naturally equipped monoidal self-indexing.