Bunched Type Theory and Monoidal Classifying Toposes

A monoidal topos is a topos equipped with an extra monoidal structure. I've seen these arise several times:

• The Schanuel topos, which has been suggested as a way to handle syntactic variables.
• Classifying toposes for noncommutative rings, as I am exploring.
• Possibly a categorified version of separation logic.

Ulrich Schöpp has described a type theory with builtin monoidal connectives. While it was designed to be interpreted into the Schanuel topos, it is more flexible than that. I noticed that there seems to be a simple syntactic condition on a geometric theory which suffices to interpret this type theory into the classifying topos.

We must have a symmetric binary relation \(\sim\) such that, for any \(x\), the subset \(\{a \in A \mid a \sim x\}\) is a (sub)model of the same theory.

For the Schanuel topos, which classifies infinite decidable objects, \(\sim\) is the apartness relation. For the classifying topos of rings, the relation is \(a \sim b \Leftrightarrow ab = ba\).

My proof nearly goes through, but there's a technical detail that isn't working. Even so, this is a good indicator of when you'd expect a classifying topos to support a useful monoidal structure.