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: theory: type theory & logic

Topic: Substitution in spatial type theory

Dylan Braithwaite (Oct 17 2025 at 13:08):

I've been working through understanding the spatial type theory in Shulman's Brouwer's fixed-point theorem in real-cohesive homotopy type theory but I'm a bit confused about how substitution should work under the $\sharp$-modality.

The rule for introducing a term with the modality is

$$\frac{\Gamma, \Delta \mid \cdot \vdash e : A}{\Gamma \mid \Delta \vdash e^\sharp : \sharp A}$$

which moves the cohesive (right) context into the crisp (left) context. Now if I have a term $\Gamma \mid \Delta, x : B \vdash e_1^\sharp : \sharp A$ then I should be able to substitute an arbitrary term $\Gamma \mid \Delta \vdash e_2 : B$ into $e_1^\sharp$. But if substitution behaves the way I'd naively expect, like $e_1^\sharp [e_2/x] = (e_1[e_2/x])^\sharp$, then we get stuck because you can only substitute variables in the crisp context for crisp terms. i.e. in $\Gamma, \Delta, x : B \mid \cdot \vdash e_1 : A$, the target variable $x$ is now in the wrong context to be substituted for $e_2$.

Is there a way to get around this, or is it just the case that the semantics are supposed to be taken denotationally, and it makes sense in the intended model, even if it doesn't work out syntactically?

Nathanael Arkor (Oct 17 2025 at 14:42):

(It's worth actually mentioning @Mike Shulman, since he would be best placed to answer the question.)

Mike Shulman (Oct 17 2025 at 21:24):

The whole point of using split-contexts is to get a theory in which substitution does work syntactically. In the case you describe, the point is that since crisp variables can also be used as cohesive variables, you also have $\Gamma,\Delta \mid \cdot \vdash e_2 : B$, and so you can substitute it for $x$ in $e_1$ as in your $(e_1[e_2/x])^\sharp$.

Dylan Braithwaite (Oct 20 2025 at 09:56):

Mike Shulman said:

The whole point of using split-contexts is to get a theory in which substitution does work syntactically. In the case you describe, the point is that since crisp variables can also be used as cohesive variables, you also have $\Gamma,\Delta \mid \cdot \vdash e_2 : B$, and so you can substitute it for $x$ in $e_1$ as in your $(e_1[e_2/x])^\sharp$.

Aha. I missed that you could shift variables into the left context, but that makes perfect sense. I guess semantically its just precompositon with $\flat$’s counit. Thanks!