# APPENDIX A. CONCURRENT GAMES TOOLBOX

## A.1. Event Structures and Maps.
We start with recalling maps of event structures.

**Definition A.1.** Consider $E, F$ two es. A **map of event structures** from $E$ to $F$ is a function $f: |E| \to |F|$ satisfying the following two conditions:

*valid:* for all $x \in \mathscr{C}(E)$, we have $f x \in \mathscr{C}(F)$,

*local injectivity:* for all $e_1, e_2 \in x \in \mathscr{C}(E)$, if $fe_1 = fe_2$ then $e_1 = e_2$.

If $E$ and $F$ are esp s, a **map of esp s** is additionally required to preserve polarities.

**Lemma A.2.** Consider $f: E \to F$ a map of event structures, and $e_1, e_2 \in x \in \mathscr{C}(E)$.

If $f(e_1) \leq_f f(e_2)$, then $e_1 \leq_E e_2$.

*Proof.* Seeking a contradiction, assume we do not have $e_1 \leq_E e_2$. This means that $e_1 \notin [e_2]_E$. But $[e_2]_E \in \mathscr{C}(E)$, so $f[e_2]_E$ is down-closed. Moreover, $fe_2 \in f[e_2]_E$, so $fe_1 \in f[e_2]_E$. So there is $e'_1 \in [e_2]_E$ such that $fe'_1 = fe_1$. Finally, $[e_2]_E \subseteq x$, so $e_1, e'_1 \in x \in \mathscr{C}(E)$. Hence, by local injectivity, $e_1 = e'_1$. We deduce that $e_1 \in [e_2]_E$ after all, contradiction. $\square$

## A.2. Basic Properties of Strategies.
We gather some basic properties.

**Lemma A.3.** Consider A an arena, $\sigma$: A a causal strategy, and $m, n \in |\sigma|$.

If $m \to_{\sigma} n$, then $\mathrm{pol}(m) \neq \mathrm{pol}(n)$.

*Proof.* If $\mathrm{pol}(m) = \mathrm{pol}(n)$, then by *courteous* we have $\partial_{\sigma}(m) \to_A \partial_{\tau}(n)$ as well. But since arenas are alternating, this is absurd. $\square$

**Lemma A.4.** Consider A an arena, $\sigma$: A a causal strategy, and $m, n^- \in |\sigma|$ compatible.

Then, $m \to_{\sigma} n$ iff $\partial_{\sigma}(m) \to_A \partial_{\sigma}(n)$.

*Proof.* If. Assume $\partial_{\sigma}(m) \to_A \partial_{\sigma}(n)$. Since $[n]_{\sigma} \in \mathscr{C}(\sigma)$ and $\partial_{\sigma}$ is a map of event structures, $\partial_{\sigma}[n]_{\sigma} \in \mathscr{C}(A)$, so it is down-closed. Thus, there is $m' \in [n]_{\sigma}$ such that $\partial_{\sigma}(m') = \partial_{\sigma}(m)$. In particular, $n$ cannot be minimal, so there is $m'' \to_{\sigma} n$. By *courteous*, since $n$ is negative we have $\partial_{\sigma}(m'') \to_A \partial_{\sigma}(n)$. But $A$ is *forestial*, so $\partial_{\sigma}(m'') = \partial_{\sigma}(m)$. Now, since $m, n$ are compatible they appear in a configuration $x \in \mathscr{C}(\sigma)$, and in particular $m, m'' \in x$. Thus, $m = m''$ by local injectivity. Only if. If $m \to_{\sigma} n^-$, then $\partial_{\sigma}(m) \to_A \partial_{\sigma}(n)$ by *courteous*. $\square$

**Lemma A.5.** Consider A an arena, $\sigma$: A a causal strategy, and $m^- \in |\sigma|$ s.t. $\partial_{\sigma}m$ non-minimal. Then, there is a unique $n \to_{\sigma} m$.

*Proof.* Existence. Write $a \to \partial_{\sigma}(m)$, which is unique since $A$ is *forestial*. Since $[m]_{\sigma} \in \mathscr{C}(\sigma)$, we have $\partial_{\sigma}[m]_{\sigma} \in \mathscr{C}(A)$, therefore it is down-closed and must contain $a$. Therefore, there is $n \leq_{\sigma} m$ such that $\partial_{\sigma}(n) = a$. By Lemma A.4, we then have $n \to_{\sigma} m$ as required.

*Uniqueness.* If $n_1 \to_{\sigma} m$ and $n_2 \to_{\sigma} m$, by *courteous* $\partial_{\sigma}n_1 \to_A \partial_{\sigma}m$ and $\partial_{\sigma}n_2 \to_A \partial_{\sigma}m$.

But then, $\partial_{\sigma}n_1 = \partial_{\sigma}n_2$ as $A$ is *forestial*. So $n_1 = n_2$ as $\partial_{\sigma}$ is locally injective. $\square$

**Lemma A.6.** Consider A an arena, $\sigma$: A a causal strategy, and $m, n_1, n_2 \in |\sigma|$.

If $n_1 \to_{\sigma} m$ and $n_2 \to_{\sigma} m$ with $n_1, n_2$ distinct, then $\mathrm{pol}(m) = +$.

*Proof.* Seeking a contradiction, assume $\mathrm{pol}(m) = -$. Then, by *courteous*, we have $\partial_{\sigma}(n_1) \to_A \partial_{\sigma}(m)$ and $\partial_{\sigma}(n_2) \to_A \partial_{\sigma}(m)$. As $A$ is *forestial*, $\partial_{\sigma}(n_1) = \partial_{\sigma}(n_2)$. As $n_1, n_2 \in [m]_{\sigma} \in \mathscr{C}(\sigma)$, we have $n_1 = n_2$ by local injectivity, contradiction. $\square$
**Lemma A.7.** Consider A an arena, $\sigma$: A a causal strategy, and $m^+ \in x \in \mathscr{C}(\sigma)$.
Then, $m$ is maximal in $x$ iff $\partial_{\sigma}m$ is maximal in $\partial_{\sigma}x$.

*Proof.* If. Assume $\partial_{\sigma}m$ is maximal in $\partial_{\sigma}x$. Seeking a contradiction, assume that $m \to_{\sigma} n$. By Lemma A.3, $\text{pol}(n) = -$. Therefore, by *courteous*, $\partial_{\sigma}(m) \to_{A} \partial_{\sigma}(n)$, contradiction. *Only if.* Straightforward by Lemma A.2. $\square$

**Lemma A.8.** Consider A an arena, $\sigma$: A a causal strategy, and $m_1^-, m_2^- \in |\sigma|$. If $m_1$ and $m_2$ are in minimal conflict in $\sigma$, then $\partial_{\sigma}(m_1)$ and $\partial_{\sigma}(m_2)$ are in minimal conflict in A.

*Proof.* We first prove that $\partial_{\sigma}(m_1)$ and $\partial_{\sigma}(m_2)$ are in conflict. Seeking a contradiction, assume that it is not the case. Then, as $m_1$ and $m_2$ are in minimal conflict, we have $\partial_{\sigma}([m_1]_{\sigma} \cup [m_2]_{\sigma}) \in \mathscr{C}(A)$. Hence, by *receptive*, there is a unique $m'_2 \in |\sigma|$ such that

$[m_1]_{\sigma} \cup [m_2]_{\sigma} \vdash_{\sigma} m'_2$ with $\partial_{\sigma}(m'_2) = \partial_{\sigma}(m_2)$ - where $[m_2]_{\sigma} = \{n \in |\sigma| \mid n <_{\sigma} m_2\}$. But then, by Lemma A.4, $m_2$ is minimal in $\sigma$ iff $m'_2$ is minimal in $\sigma$, and so $m_2 = m'_2$ by *receptive*, contradicting that $m_1 \#_{\sigma} m_2$. Otherwise, consider $n \to_{\sigma} m_2$ and $n' \to_{\sigma} m'_2$. Then, by *courteous*,

$\partial_{\sigma}(n) \to_{A} \partial_{\sigma}(m_2), \quad \partial_{\sigma}(n') \to_{A} \partial_{\sigma}(m'_2)$, but then $\partial_{\sigma}(n) = \partial_{\sigma}(n')$ since A is *forestial*. But $n, n' \in [m_1]_{\sigma} \cup [m_2]_{\sigma} \in \mathscr{C}(\sigma)$, so we must have $n = n'$ by locally injectivity. By Lemma A.5, $n$ is the unique predecessor of $m_2$ and $m'_2$. So, $[n]_{\sigma} \vdash_{\sigma} m_2$ and $[n]_{\sigma} \vdash_{\sigma} m'_2$ with the same image. So $m_2 = m'_2$, contradiction. Finally, minimality of the conflict is obvious from that of $m_1$ and $m_2$. $\square$

## APPENDIX B. CONSTRUCTION OF ALTERNATING STRATEGIES

In this second section of the appendix, we give more details on the construction of $\downarrow\uparrow$-Strat.

First, a warning: quite a few superficial complications come from the general construction $A \dasharrow B$ for $B$ non-pointed, with morphisms from $A$ to $B$ being strategies on $A \dasharrow B$. An alternative is to only consider $A \dasharrow B$ for $B$ strict. Then we do not have a symmetric monoidal closed category, only an exponential ideal. This would be sufficient for the languages considered in this paper, however, we opted to link with traditional categorical models.

### B.1. Basic Categorical Structure.
We start by establishing the categorical structure.

#### B.1.1. *Arrow arena.*
First, we give postponed proofs on the construction of the arrow arena.

**Lemma B.1.** Consider A and B two $\dasharrow$-arenas.

Then, there is a unique $\#_{A \dasharrow B}$ making $A \dasharrow B$ a $\dasharrow$-arena such that for all down-closed finite $x \subseteq |A \dasharrow B|$, $x \in \mathscr{C}(A \dasharrow B)$ iff $\chi_{A,B} x \in \mathscr{C}(A^{\perp} \parallel B)$ with $\chi_{A,B}$ injective on $x$.

*Proof. Existence.* We set $\#_{A \dasharrow B}$ as the following relation:

$$ \begin{array}{lclcl} (2, b_1) \#_{A \dasharrow B} (2, b_2) & \Leftrightarrow & b_1 \#_B b_2 & & \\ (1, (b, a_1)) \#_{A \dasharrow B} (1, (b, a_2)) & \Leftrightarrow & a_1 \#_A a_2 & & \\ (2, b_1) \#_{A \dasharrow B} (1, (b_2, a)) & \Leftrightarrow & b_1 \#_B b_2 & & \\ (1, (b_1, a)) \#_{A \dasharrow B} (2, b_2) & \Leftrightarrow & b_1 \#_B b_2 & & \\ (1, (b_1, a_1)) \#_{A \dasharrow B} (1, (b_2, a_2)) & \Leftrightarrow & (b_1 \#_B b_2) \vee (\min(a_1) = \min(a_2)) \vee (a_1 \#_A a_2), & & \\ \end{array} $$
<figure><img src="image_101.png" /><figcaption>Figure 68: Restrictions of pre-interactions</figcaption></figure>

where $b_1, b_2$ are assumed distinct, all other pairs left consistent, and with $\min(a)$ the unique minimal antecedent of $a$. It is routine that this conflict makes $A \to B$ a $\to$-arena.

Now, we check the additional condition. Consider $x \subseteq |A \to B|$ down-closed, written as

$$x = (\|_{b \in I} x_{A,b}) \| x_B$$

where $I$ is a subset of the minimal events of $B$. Then, we show that $x \in \mathscr{C}(A \to B)$ iff

$$\chi_{A,B} x = (\cup_{b \in I} x_{A,b}) \| x_B \in \mathscr{C}(A \vdash B)$$

and $\chi_{A,B}$ is injective on $x$. Only if is a direct verification. For if, if $\chi_{A,B} x \in \mathscr{C}(A \to B)$ then the only possible conflict in $x$ is of the form, with $b_1 \#_B b_2$ or $\min(a_1) = \min(a_2)$:

$$(1, (b_1, a_1)) \#_{A \to B} (1, (b_2, a_2))$$

In the former case, by down-closure, $(2, b_1)$, $(2, b_2) \in x$, contradicting $\chi_{A,B} x \in \mathscr{C}(A \vdash B)$. In the latter case, by down-closure, $(1, (b_1, \min(a_1)))$, $(1, (b_2, \min(a_2))) \in x$ – but they have the same image through $\chi_{A,B}$, contradicting that it should be injective on $x$. Uniqueness follows as with fixed events, an event structure is determined by configurations. $\square$

### B.1.2. Composition.
Consider fixed $A, B$ and $C$ three $\to$-arenas, and $\sigma: A \to B, \tau: B \to C$ alternating prestrategies. Recall from the main text:

**Definition B.2.** A pre-interaction on $A, B, C$ is $u \in |(A \to B) \to C|^*$ satisfying:

$$\text{valid: } \forall 1 \le i \le n, \{s_1, \dots, s_i\} \in \mathscr{C}((A \to B) \to C)$$

Remember that in $A \to B$, events are either $(2, b)$ for $b \in |B|$, or $(1, (b, a))$ for $b \in \min(B)$ and $a \in |A|$. By convention, in this section, we write $[r, b]$ for $(2, b)$ and $[l, a]_b$ for $(1, (b, a))$. In that case, $[r, b]$ is the unique immediate predecessor of $[l, a]_b$, i.e. its *justifier*. Similarly, in $(A \to B) \to C$, events can be $(2, c)$ written $[r, c]$; $(1, (c, (2, b)))$ written $[m, b]_c$; and $(1, (c, (1, (b, a))))$ written $[l, a]_{b,c}$; we respectively say that they are **in C**, **in B**, or **in A**.

Using this, we define in Figure 68 three restrictions of a pre-interaction $u$, namely $u \uparrow A, B \in |A \to B|^*$, $u \uparrow B, C \in |B \to C|^*$, and $u \uparrow A, C \in |A \to C|^*$. Now we set:

**Definition B.3.** An interaction $u \in \tau \circledast \sigma$ between $\sigma$ and $\tau$ is a pre-interaction $u$ s.t.

$$u \uparrow A, B \in \sigma, \quad u \uparrow B, C \in \tau, \quad u \uparrow A, C \in \downarrow \uparrow \text{-Plays}(A \to C).$$

The composition of $\sigma$ and $\tau$ is $\tau \odot \sigma = \{u \uparrow A, C | u \in \tau \circledast \sigma\}$.

The first step is to ensure that $\tau \odot \sigma$ is a prestrategy, and that if $\sigma$ and $\tau$ are strategies, then so is $\tau \odot \sigma$. We start with the conditions of Definition 2.8, postponing uniformity. *Non-empty* and *prefix-closed* follow from those on $\sigma$ and $\tau$. For *deterministic*, we need more tools. The main tool to study the interaction of alternating strategies is the *state analysis* of plays and interactions. Recall from Section 6.1.3 that $s$ alternating is **in state O** if it has even length, and **in state P** otherwise. Then, we have the following property:
**Lemma B.4.** If $u \in \tau \circledast \sigma$, then we are in one of the following three cases:

(1) $u \uparrow A, B, u \uparrow B, C$ and $u \uparrow A, C$ are respectively in state O, O, O.

(2) $u \uparrow A, B, u \uparrow B, C$ and $u \uparrow A, C$ are respectively in state O, P, P.

(3) $u \uparrow A, B, u \uparrow B, C$ and $u \uparrow A, C$ are respectively in state P, O, P.

*Proof.* Standard argument, direct by induction on $u$. □

Next, we can prove the key property of the composition of alternating strategies.

**Lemma B.5.** Consider $s \in \tau \odot \sigma$ of even length.

Then, there is a unique witness $u \in \tau \circledast \sigma$ such that $u \uparrow A, C = s$.

*Proof. Existence* is obvious by definition.

*Uniqueness.* Seeking a contradiction, consider $u_1, u_2 \in \tau \circledast \sigma$ distinct such that $u_1 \uparrow A, C = u_2 \uparrow A, C = s$. First, since $s$ has even length, $u_i \uparrow A, C$ is in state O, so $u_1$ and $u_2$ must be in state (1) of Lemma B.4. It follows that their immediate prefix cannot be in state (1), from which it follows last move is visible (i.e. in A or C). So, $u_1$ and $u_2$ cannot be comparable for the prefix order. Therefore, there is $u'$ maximal such that $u' \subseteq u_1$ and $u' \subseteq u_2$, say we have $u'm_1 \subseteq u_1$ and $u'm_2 \subseteq u_2$ for $m_1, m_2$ distinct. By Lemma B.4, $u'$ is in one of the states (1), (2) or (3). If it is in state (1), then the next moves $m_1$ and $m_2$ are in $u \uparrow A, C = s$, so they cannot be distinct. Say $u'$ is in state (3) – the case (2) is similar but simpler. Necessarily, $m_1$ and $m_2$ are in A or B, so that

$$u'm_1 \uparrow A, B = (u' \uparrow A, B)n_1 \qquad u'm_2 \uparrow A, B = (u' \uparrow A, B)n_2$$

are two plays of $\sigma$ with even length – so that $n_1 = n_2$, by *determinism*. From the definition of restriction, the only case where $m_1 \neq m_2$ with $n_1 = n_2$ is if $m_1 = [l, a]_{b,c}$, $m_2 = [l, a]_{b,c'}$ with $c \neq c'$, so $n_1 = n_2 = [l, a]_b$. Then, as $u'$ satisfies condition *valid*, this entails that their immediate dependencies $[m, b]_c, [m, b]_{c'} \in |u'|$ as well – impossible since $[m, b]_c \# [m, b]_{c'}$. □

It is then straightforward to prove that $\tau \odot \sigma$ satisfies *deterministic*.

**Proposition B.6.** We have that $\tau \odot \sigma : A \to C$ is a prestrategy.

Moreover, if $\sigma$ and $\tau$ are strategies, then so is $\tau \odot \sigma$.

*Proof.* To obtain a prestrategy, it remains that $\tau \odot \sigma$ satisfies *deterministic*. Consider $sn_1^+, sn_2^+ \in \tau \odot \sigma$. Consider $u_1m_1, u_2m_2 \in \tau \circledast \sigma$ their unique witness as given by Lemma B.5. We reason as in Lemma B.5: if there is a diverging point between $u_1m_1$ and $u_2m_2$, by Lemma B.4 the divergence can be attributed to either $\sigma$ or $\tau$, contradicting determinism.

Now, assume that $\sigma$ and $\tau$ satisfy condition *receptive*. Consider $s \in \tau \odot \sigma$ such that $sm^- \in \downarrow\uparrow$-Plays($A \to C$). More precisely, assume that $m = [(l, a)]_c$ as the case in C is simpler. Consider now $u \in \tau \circledast \sigma$ such that $u \uparrow A, C = s$; necessarily $u$ is in state (1) of Lemma B.4. Now, as $m$ is negative its immediate predecessor of $m$ in $A \to C$ is some $[(l, a')]_c$ in $s$. Since $s = u \uparrow A, C$, it corresponds to some $[(l, a')]_{b,c}$ in $u$, for some $b \in \min(B)$. But then, it is a direct verification that $(u \uparrow A, B)[(l, a)]_b \in \downarrow\uparrow$-Plays($A \to B$), so $(u \uparrow A, B)[(l, a)]_b \in \sigma$ by *receptive*. Therefore, $u[(l, a)]_{b,c} \in \tau \circledast \sigma$ witnessing that $sm \in \tau \odot \sigma$ as required. □

Note that this argument and the prior state analysis of Lemma B.4 are also found in the proof of composition of sequentiality for causal strategies in Section 6.1.3.
B.1.3. *Associativity.* We now sketch associativity, which follows standard lines, see e.g. [Har04]. Let us fix $\sigma: A \to B$, $\tau: B \to C$ and $\delta: C \to D$ three alternating prestrategies.

The first step is to define a notion of interaction between three strategies. First:

**Definition B.7.** A 3-pre-interaction on $A, B, C, D$ is $w \in |((A \to B) \to C) \to D|*$ s.t.

$$ \textit{valid:} \quad \forall 1 \le i \le n, \{w_1, \dots, w_i\} \in \mathcal{C}((A \to B) \to C), $$

where $w = w_1 \dots w_n$.

For a 3-pre-interaction $w$, we define $w \uparrow A, B \in |A \to B|*$, $w \uparrow B, C \in |B \to C|*$, $w \uparrow C, D \in |C \to D|*$ and $w \uparrow A, D \in |A \to D|*$ with the obvious adaptation of Figure 68. An **interaction** of $\sigma, \tau$ and $\delta$ is a 3-pre-interaction $w$ s.t.

$$ w \uparrow A, B \in \sigma, \quad w \uparrow B, C \in \tau, \quad w \uparrow C, D \in \delta, \quad w \uparrow A, D \in \downarrow\uparrow\text{-Plays}(A \to D), $$

written $w \in \delta \circledast \tau \circledast \sigma$. We have four additional restrictions $w \uparrow A, B, C \in \tau \circledast \sigma$, $w \uparrow B, C, D \in \delta \circledast \tau$, $w \uparrow A, C, D \in \delta \circledast (\tau \odot \sigma)$ and $w \uparrow A, B, D \in (\delta \odot \tau) \circledast \sigma$, defined in the obvious way.

Then, the key argument of associativity is the so-called “zipping lemma”:

**Lemma B.8 (Zipping).** Consider $u \in \delta \circledast (\tau \odot \sigma)$ and $v \in \tau \circledast \sigma$ such that $u \uparrow A, C = v \uparrow A, C$.

Then, there is a unique $w \in \delta \circledast \tau \circledast \sigma$ such that $w \uparrow A, C, D = u$ and $w \uparrow A, B, C = v$.

*Proof.* By induction on $u$ – by Lemma B.4 the moves in $B$ from $v$ can be interleaved with those in $v$ in a unique way; likewise there is a unique way to set their dependency. $\square$

We also have the mirror image, zipping $u \in (\delta \odot \tau) \circledast \sigma$ with $v \in \delta \circledast \tau$. Altogether,

**Proposition B.9.** We have $(\delta \odot \tau) \odot \sigma = \delta \odot (\tau \odot \sigma)$.

*Proof.* Consider $s \in \delta \odot (\tau \odot \sigma)$. It has a (unique) witness $u \in \delta \circledast (\tau \odot \sigma)$. Then, $u \uparrow A, C \in \tau \odot \sigma$, thus there is again $v \in \tau \circledast \sigma$ s.t. $u \uparrow A, C = v \uparrow A, C$. By Lemma B.8, there is $w \in \delta \circledast \tau \circledast \sigma$ s.t. $w \uparrow A, C, D = u$ and $w \uparrow A, D, C = v$. But then we may restrict $w$ to $w \uparrow B, C, D \in \delta \circledast \tau$, so $w \uparrow B, D \in \delta \odot \tau$. Moreover $w \uparrow A, B \in \sigma$ so $w \uparrow A, B, D \in (\delta \odot \tau) \circledast \sigma$, from which $w \uparrow A, D \in (\delta \odot \tau) \odot \sigma$. The other direction is symmetric. $\square$

Note that associativity holds for prestrategies and does not depend on *receptive*.

B.1.4. *Identities.* Fix some --arena $A$. For $s \in \downarrow\uparrow\text{-Plays}(A \to A)$, we define its restrictions

$$ \begin{align*} \varepsilon \uparrow | &= \varepsilon & \varepsilon \uparrow \mathbf{r} &= \varepsilon \\ s[(l,a)]_{a'} \uparrow | &= (s \uparrow |)a & s[(l,a)]_{a'} \uparrow \mathbf{r} &= s \uparrow \mathbf{r} \\ s[(r,a)] \uparrow \mathbf{r} &= s \uparrow \mathbf{r} & s[(r,a)] \uparrow \mathbf{r} &= (s \uparrow \mathbf{r})a \end{align*} $$

using which we may define the identity for alternating strategies:

**Definition B.10.** The copycat $\mathfrak{c}_A: A \to A$ comprises all $s \in \downarrow\uparrow\text{-Plays}(A \to A)$ s.t.

(1) for all $s' \subseteq s$ of even length, $s' \uparrow | = s' \uparrow \mathbf{r}$,

(2) for all $[(l,a)]_{a'} \in |s|$, with $a \in \min(A)$, $a = a'$.

Condition (2) means that when playing a minimal event on the left hand side, copycat justifies it with the same move on the right. Such a condition is also required in Hyland-Ong games (though sometimes mistakenly omitted). Copycat strategies provide identities:

**Proposition B.11.** The --arenas and alternating strategies form a category $\downarrow\uparrow$-Strat.

*Proof.* It remains that for any $\sigma: A \to B$, $\sigma = \mathfrak{c}_B \odot \sigma \odot \mathfrak{c}_A$, which is elementary. $\square$
<figure><img src="image_102.png" /><figcaption>Figure 69: Partial restrictions for the tensor</figcaption></figure>

## B.2. Monoidal Closed Structure.
We now describe the monoidal structure.

### B.2.1. Tensor product.
On $\otimes$-arenas, we have defined $A \otimes B$ simply as $A \parallel B$.

For strategies, the critical step is a suitable notion of restriction. More precisely, for $A_1, A_2, B_1, B_2$ $\otimes$-arenas and $s \in \text{↓↑-Plays}(A_1 \otimes A_2 \to B_1 \otimes B_2)$, we give a partial definition

$$s \uparrow A_1, B_1 \in |A_1 \to B_1|^* \qquad s \uparrow A_2, B_2 \in |A_2 \to B_2|^*$$

in Figure 69 – partial, because e.g. $[(l, (1, a))]_{(2,b)} \uparrow A_1, B_1$ is left undefined. We then set:

**Definition B.12.** Consider $\sigma_1 : A_1 \to B_1$ and $\sigma_2 : A_2 \to B_2$ alternating strategies. Then:

$$\sigma_1 \otimes \sigma_2 = \{s \in \text{↓↑-Plays}(A_1 \otimes A_2 \to B_1 \otimes B_2) \mid \forall i \in \{1, 2\}, s \uparrow A_i, B_i \in \sigma_i\},$$

implying in particular that for each $s \in \sigma_1 \otimes \sigma_2$ and $i \in \{1, 2\}$, $s \uparrow A_i, B_i$ is defined.

By definition, $\sigma_1 \otimes \sigma_2$ satisfies non-empty and prefix-closed. As for composition, determinism involves performing a state analysis expressing that at each point, only one of $\sigma_1$ or $\sigma_2$ has control. We skip the details. See e.g. [Har04] for an analogous proof, also reflected in the proof in Section 6.1.4 that sequential causal strategies are stable under tensor.

**Proposition B.13.** Consider $\sigma_1 : A_1 \to B_1$ and $\sigma_2 : A_2 \to B_2$ alternating strategies.

Then, $\sigma_1 \otimes \sigma_2 : A_1 \otimes A_2 \to B_1 \otimes B_2$ is an alternating strategy.

Fix $\sigma_1 : A_1 \to B_1$, $\sigma_2 : A_2 \to B_2$, $\tau_1 : B_1 \to C_1$ and $\tau_2 : B_2 \to C_2$. For $w \in (\tau_1 \otimes \tau_2) \circledast (\sigma_1 \otimes \sigma_2)$, we first define partially $w \uparrow A_1, B_1, C_1$ and $w \uparrow A_2, B_2, C_2$ analogously to Figure 69 – it is direct to prove that $w \uparrow A_1, B_1, C_1 \in \tau_1 \circledast \sigma_1$ and $w \uparrow A_2, B_2, C_2 \in \tau_2 \circledast \sigma_2$.

Functoriality is analogous to associativity in that it relies on a zipping lemma:

**Lemma B.14.** Consider $u_1 \in \tau_1 \circledast \sigma_1$, $u_2 \in \tau_2 \circledast \sigma_2$, and $s \in \text{↓↑-Plays}(A_1 \otimes A_2 \to C_1 \otimes C_2)$ such that $s \uparrow A_1, C_1 = u \uparrow A_1, C_1$ and $s \uparrow A_2, C_2 = u \uparrow A_2, C_2$.

Then, there is a unique $w \in (\tau_1 \otimes \tau_2) \circledast (\sigma_1 \otimes \sigma_2)$ such that

$$s = w \uparrow A_1 \otimes A_2, C_1 \otimes C_2, \quad s \uparrow A_1, B_1, C_1 = u_1, \quad s \uparrow A_2, B_2, C_2 = u_2.$$

**Proposition B.15.** The construction $\otimes$ extends to a bifunctor

$$\otimes : \text{↓↑-Strat} \times \text{↓↑-Strat} \to \text{↓↑-Strat}.$$

*Proof.* Preservation of identities is direct. Factoriality follows by Lemma B.14 □

<figure><img src="image_103.png" /></figure>

Next, we complete the symmetric monoidal structure by providing the structural natural isomorphisms. We first introduce a few tools useful in giving a clean definition of such structural isomorphisms, which are variants of the copycat strategy. We shall make use of certain morphisms, called *renamings*, to act on strategies.
**Definition B.16.** A renaming from arena A to B is a function $f: |A| \to |B|$ satisfying:

validity: $\forall x \in \mathscr{C}(A), fx \in \mathscr{C}(B)$

local injectivity: $\forall a_1, a_2 \in x \in \mathscr{C}(A), fa_1 = fa_2 \implies a_1 = a_2$

polarity-preserving: $\forall a \in |A|, \text{pol}_B(fa) = \text{pol}_A(a)$

symmetry-preserving: $\forall \theta \in \mathscr{S}(A)(\text{resp. } \mathscr{S}_+(A), \mathscr{S}_-(A)), f\theta \in \mathscr{S}(B), (\text{resp. } \mathscr{S}_+(B), \mathscr{S}_-(B))$

strong-receptivity: for all $\theta \in \mathscr{S}(A)$, for all $f\theta \subseteq \varphi \in \mathscr{S}(B)$, $\exists!\theta \subseteq \theta' \in \mathscr{S}(A) f\theta' = \varphi$

courtesy: $\forall a_1 \to_A a_2, (\text{pol}_A(a_1) = + \lor \text{pol}_A(a_2) = -) \implies fa_1 \to_B fa_2$.

We write $f: A \to B$ to mean that $f$ is a renaming from $A$ to $B$.

This construction is imported from [CCW19]. Then we have:

**Definition B.17.** Consider $\sigma: A \to B$ and renamings $g: B \to B'$, $f: A^{\perp} \to A'^{\perp}$. We set

$$g \cdot \sigma \cdot f = \{g \cdot s \cdot f \mid s \in \sigma\} : A' \to B'$$

where $g \cdot s \cdot f$ acts on $s$ event-wise, sending $[(l, a)]_b$ to $[(l, f(a))]_{g(b)}$ and $[(r, b)]$ to $[(r, g(b))]$.

It is direct that $g \cdot \sigma \cdot f$ is a strategy. The structural isomorphisms that we aim to define are obtained by *lifting* renamings. Indeed if $f: A \to B$ is a renaming, we may define

$$\vec{f} = f \cdot \omega_A : A \to B.$$

a renaming from copycat. Likewise, from $f: B^{\perp} \to A^{\perp}$ we set $\overleftarrow{f} = \omega_B \cdot f: A \to B$.

The main property satisfied by these constructions is the following *lifting lemma*.

**Lemma B.18.** Consider $\sigma: A \to B$ a strategy, and $f: A^{\perp} \to A'^{\perp}$, $g: B \to B'$ two renamings. Then, we have $\vec{g} \odot \sigma \odot \overleftarrow{f} = g \cdot \sigma \cdot f$.

*Proof.* A direct adaptation of the neutrality of copycat under composition. $\square$

<figure><img src="image_104.png" /></figure>

Before we put these to use to construct the symmetric monoidal structure, we deduce a few properties of lifted strategies. In the statement below, for any renaming $f: A \to B$ which is additionally an isomorphism, then we write $f^{\perp}: B^{\perp} \to A^{\perp}$ for its inverse with polarities reversed – it is immediate that it still satisfies the conditions of a renaming.

**Proposition B.19.** *Lifting is a functor from the category of renamings to $\downarrow$-Strat.*

Moreover, if $f: A \to B$ is an iso, $\vec{f}$ is an iso; and we have $\vec{f}^{-1} = \overleftarrow{f}^{-1}$ and $\overleftarrow{f} = f^{\perp}$.

*Proof.* By Lemma B.18 and direct verifications. $\square$

<figure><img src="image_105.png" /></figure>

With this, we may now define the structural isomorphisms for the symmetric monoidal structure. We notice that for all arenas $A, B, C$, there are invertible renamings:

$$\rho_A : A \otimes 1 \to A$$

$$\lambda_A : 1 \otimes 1 \to A$$

$$\alpha_{A,B,C} : (A \otimes B) \otimes C \to A \otimes (B \otimes C)$$

$$s_{A,B} : A \otimes B \to B \otimes A$$

where 1 is the empty arena, satisfying the coherence laws of a symmetric monoidal category. The required structural isomorphisms are simply obtained by lifting those as $\vec{\rho}_A$, $\overleftarrow{\lambda}_A$, $\alpha_{A,B,C}$ and $\overleftarrow{s}_{A,B}$. By Proposition B.19, the required coherence diagrams are still satisfied.

**Proposition B.20.** *The category $\downarrow$-Strat is a symmetric monoidal category.*

*Proof.* It remains to prove naturality, easy from Proposition B.19 and direct verifications. $\square$

<figure><img src="image_106.png" /></figure>
### B.2.2. Cartesian products. 
$\downarrow\uparrow$-Strat has cartesian products, given by $\&$ on objects.

To perform the **pairing** of $\sigma_1: A \to B_1$ and $\sigma_2: A \to B_2$, we first build prestrategies

$$ \text{inj}_1(\sigma_1) : A \to B_1 \& B_2, \qquad \text{inj}_2(\sigma_2) : A \to B_1 \& B_2 $$

defined by applying event-wise $\text{inj}_i([[(r, b)])] = [(r, (i, b))], \text{inj}_j([[(l, a)]_b) = [(l, a)]_{(i,b)}$. We obtain $\langle\sigma_1, \sigma_2\rangle = \text{inj}_1(\sigma_1) \oplus \text{inj}_2(\sigma_2)$. It is direct that this yields a bijection:

$$ \langle-, -\rangle : \downarrow\uparrow\text{-Strat}(A, B_1) \times \downarrow\uparrow\text{-Strat}(A, B_2) \to \downarrow\uparrow\text{-Strat}(A, B_1 \& B_2) $$

The **projections** are $(\pi_1, \pi_2) = \langle-, -\rangle^{-1}(\text{id}_{B_1 \& B_2})$, and we can verify

$$ \pi_1 \odot \langle\sigma_1, \sigma_2\rangle = \sigma_1, \qquad \pi_2 \odot \langle\sigma_1, \sigma_2\rangle = \sigma_2 $$

which is enough to complete the cartesian structure of $\downarrow\uparrow$-Strat.

### B.2.3. Monoidal closure.
First, for $--$arenas $A, B$ and $C$, there is a clear isomorphism

$$ (A \otimes B) \to C \cong A \to (B \to C) $$

which, applied event-wise, yields $\Lambda(-) : \downarrow\uparrow\text{-Strat}(A \otimes B, C) \simeq \downarrow\uparrow\text{-Strat}(A, B \to C)$. Then,

$$ \text{ev}_{A,B} = \Lambda^{-1}(\text{id}_{A \to B}) : (A \to B) \otimes A \to B $$

is the **evaluation** strategy. It is a verification akin to the neutrality of copycat that for all $\sigma: A \to (B \to C)$, we have $\text{ev}_{A,C} \odot (\sigma \otimes B) = \Lambda^{-1}(\sigma)$.

**Proposition B.21.** *$\downarrow\uparrow$-Strat is a cartesian symmetric monoidal closed category.*

### B.3. Symmetry.
We now develop the structure pertaining to symmetry.

#### B.3.1. Basic structure.
The extension of the construction above with symmetry and uniformity unfolds essentially as in AJM games [AJM00]. We describe the main steps.

First of all, we ensure all structural morphisms are uniform. This is the purpose of:

**Lemma B.22.** For $A$ and $B$ $--$arenas and $f: A \to B$ a renaming, $\vec{f} \approx \overleftarrow{f}$.

*Proof.* Straightforward by symmetry-preserving and strong-receptivity of renamings. $\square$

<figure><img src="image_107.png" /></figure>

Next, we show operations on strategies are compatible with $\approx$. The delicate case is composition. Fix $A, B$ and $C$ $--$arenas, and write $I = (A \to B) \to C$. We shall give to events of $(A \to B) \to C$ a *polarity* corresponding to their role in an interaction: a move $m$ is *negative* if it is in $A$ or $C$ and is negative for $A \to C$, and has *polarity p* otherwise.

The main tool is the following lifting of Definition 2.13 to interactions:

**Definition B.23.** Consider $\sigma, \sigma' : A \to B$ and $\tau, \tau' : B \to C$. We write $\tau \circled{\sigma} \approx \tau' \circled{\sigma'}$ iff

*$\to$-simulation: $\forall u m^p \in \tau \circled{\sigma}, v \in \tau' \circled{\sigma'}, u \cong_I v \implies \exists n^p, vn \in \tau' \circled{\sigma'} \& um \cong_I vn$

*$\leftarrow$-simulation: $\forall u \in \tau \circled{\sigma}, vn^p \in \tau' \circled{\sigma'}, u \cong_I v \implies \exists m, um \in \tau \circled{\sigma} \& um \cong_I vn$

*$\to$-receptive: $\forall u m^- \in \tau \circled{\sigma}, v \in \tau' \circled{\sigma'}, um^- \cong_I vn^- \implies vn^- \in \tau' \circled{\sigma'}$

*$\leftarrow$-receptive: $\forall u \in \tau \circled{\sigma}, vn^- \in \tau' \circled{\sigma'}, um^- \cong_I vn^- \implies um^- \in \tau \circled{\sigma}$

**Lemma B.24.** Consider $\sigma, \sigma' : A \to B$ and $\tau, \tau' : B \to C$ such that $\sigma \approx \sigma'$ and $\tau \approx \tau'$.

Then, $\tau \circled{\sigma} \approx \tau' \circled{\sigma'}$.
$$
\begin{align*}
\varepsilon \upharpoonright i &= \varepsilon \\
s [(l, (i, a))]_{(i,b)} \upharpoonright i &= (s \upharpoonright i) [(l, a)]_b \\
s [(l, (j, a))]_{(k,b)} \upharpoonright i &= s \upharpoonright i \quad (i \neq j) \\
s [(r, (i, b))] \upharpoonright i &= (s \upharpoonright i) [(r, b)] \\
s [(r, (j, b))] \upharpoonright i &= s \upharpoonright i \quad (i \neq j)
\end{align*}
$$

<caption>Figure 70: Partial restrictions for !</caption>

Proof. $\rightarrow$-simulation. Consider $ump^p \in \tau \circled{\circ} \sigma$ and $v \in \tau' \circled{\circ} \sigma'$, s.t. $u \cong_v v$. Necessarily, $m$ is positive for $\sigma$ or $\tau$, w.l.o.g. say $\sigma$. Again, we distinguish cases whether $m$ is in $A$ or $B$. We consider $B$, which is the most interesting case – so that $m = [(m, b)]_c$ for some $c \in \min(C)$.

We project $u[(m,b)]_c \upharpoonright A, B = (u \upharpoonright A, B)[(r,b)]^+ \in \sigma$, $v \upharpoonright A, B \in \sigma'$ with $u \upharpoonright A, B \cong_{A \to B} v \upharpoonright A, B$. By $\rightarrow$-simulation for $\sigma$, there is $[(r,b')]$ s.t. $(v \upharpoonright A, B)[(r,b')] \in \sigma'$ and

$$
(u \upharpoonright A, B)[(r, b)] \cong_{A \to B} (v \upharpoonright A, B)[(r, b')]. \quad (B.1)
$$

However, we also have $(u \upharpoonright B, C)[(l, b)]_c^- \in \tau$, $v \upharpoonright B, C \in \tau'$. We also have $u \upharpoonright B, C \cong_{B \to C} v \upharpoonright B, C$. Necessarily, $(r, c) \in |u \upharpoonright B, C|$ and there is a symmetric $(r, c') \in |v \upharpoonright B, C|$. Then, from (B.1) and the definition of symmetry on $A \to B$ and $B \to C$,

$$
(u \upharpoonright B, C)[(l, b)]_c \cong_{B \to C} (v \upharpoonright B, C)[(l, b')]_{c'}
$$

so by receptivity, $(v \upharpoonright B, C)[(l, b')]_{c'} \in \tau'$. It follows that $v[(m, b')]_{c'} \in \tau' \circled{\circ} \sigma'$ with $u[(m, b)]_c \cong_I v[(m, b')]_{c'}$ as required. The condition $\leftarrow$-simulation is symmetric.

Finally, $\rightarrow$-receptive and $\leftarrow$-receptive are similar but simpler.

<figure><img src="image_108.png" /></figure>

Finally, we may deduce compatibility of $\approx$ with composition:

**Corollary B.25.** Consider $\sigma, \sigma' : A \to B$ and $\tau, \tau' : B \to C$ such that $\sigma \approx \sigma'$ and $\tau \approx \tau'$. Then, $\tau \odot \sigma \approx \tau' \odot \sigma'$.

Proof. Direct from Lemmas B.5 and B.24.

<figure><img src="image_109.png" /></figure>

Lemma B.5 is crucial: this fails if we do not have a unique witness. This is the main reason why this approach to uniformity does not extend to $\mathcal{C}$-Strat. Other operations on strategies are easily seen to be compatible with $\approx$. Therefore, considering $\downarrow\uparrow$-Strat as having as only morphisms the uniform strategies (i.e. self-equivalent for $\approx$), it is equipped with an additional equivalence relation $\approx$ with respect to which all operations are compatible.

B.4. **Seely category.** We now provide the last ingredients to the Seely category.

First, we need a functor ! : $\downarrow\uparrow$-Strat $\rightarrow$ $\downarrow\uparrow$-Strat. The construction is similar to the tensor and defined by a suitable restriction, given in Figure 70. Armed with this, we set:

**Definition B.26.** Consider $\sigma : A \to B$ an alternating strategy. Then, we set:

$$
!\sigma = \{s \in \downarrow\uparrow\text{-Plays}(!A \to !B \mid \forall i \in \mathbb{N}, s \upharpoonright i \in \sigma)\},
$$

implying in particular that for each $s \in !\sigma$ and $i \in \mathbb{N}$, $s \upharpoonright i$ is defined.

This is really an infinitary tensor of $\sigma$. That this yields $!\sigma : !A \to !B$ an alternating strategy, along with functoriality, are as for the tensor. We skip the details.

**Proposition B.27.** The construction ! extends to a functor ! : $\downarrow\uparrow$-Strat $\rightarrow$ $\downarrow\uparrow$-Strat.
$$ \eta_A : \begin{array}{rcl} A^{\perp} & \to & (!A)^{\perp} \\ a & \mapsto & (i, a) \end{array} $$

$$ \begin{array}{rcl} \text{see}_{A,B} & !A \otimes !B & \to ! (A \ \& \ B) \\ & (1, (i, a)) & \mapsto (2i, (1, a)) \\ & (2, (i, b)) & \mapsto (2i + 1, (2, a)) \end{array} $$

$$ \mu_A : \begin{array}{rcl} (!!A)^{\perp} & \to & (!A)^{\perp} \\ (i, (j, a)) & \mapsto & (\langle i, j \rangle, a) \end{array} $$

$$ \begin{array}{rcl} \text{see}_{A,B}^{\leftarrow} & ! (A \ \& \ B) & \to ! A \otimes ! B \\ & (i, (1, a)) & \mapsto (1, (i, a)) \\ & (i, (2, b)) & \mapsto (2, (i, b)) \end{array} $$

<caption>Figure 71: Comonad renamings</caption>

<caption>Figure 72: Seely renamings</caption>

The Seely structure also includes structural morphisms, all defined through lifting. We define renamings in Figures 71 and 72 (with $\langle -, - \rangle : \mathbb{N} \times \mathbb{N} \to \mathbb{N}$ any bijection), set

$$ \begin{array}{rcl} \text{der}_A & = & \overleftarrow{\eta}_A : \quad !A \quad \to \quad A \\ \text{dig}_A & = & \overleftarrow{\mu}_A : \quad !A \quad \to \quad !!A \\ \text{mon}_{A,B} & = & \overleftarrow{\text{see}}_{A,B} : \quad !A \otimes !B \quad \to \quad ! (A \ \& \ B) \\ \text{mon}_{A,B}^{-1} & = & \overleftarrow{\text{see}}_{A,B}^{-1} : \quad ! (A \ \& \ B) \quad \to \quad !A \otimes !B, \end{array} $$

and all coherence and naturality properties follow from Lemma B.18 with direct verifications. A number of those only hold up to $\approx$: for instance, $\text{mon}_{A,B}$ and $\text{mon}_{A,B}^{-1}$ are inverses up to $\approx$, but not up to equality. Finally, $\text{mon}^0: \mathbf{1} \to !\mathbf{1}$ is the empty strategy. Altogether:

**Proposition B.28.** *The category $\downarrow\uparrow$-Strat is a Seely category.*

## APPENDIX C. CONSTRUCTION OF NON-ALTERNATING STRATEGIES

Next, we construct the category $\mathcal{C}$-Strat of $\mathcal{C}$-arenas and non-alternating strategies.

### C.1. Basic Categorical Structure.
We first study composition and copycat. For composition, the development is essentially a simpler version of $\downarrow\uparrow$-Strat as there is no determinism requirement. On the other hand, copycat requires slightly more care.

#### C.1.1. Composition.
Consider fixed $A, B$ and $C$ three $\mathcal{C}$-arenas, and $\sigma: A \to B, \tau: B \to C$ non-alternating prestrategies. Re-using pre-interactions and restrictions from before, we set:

**Definition C.1.** An interaction $u \in \tau \circled{\otimes} \sigma$, is a pre-interaction $u$ such that

$$ u \upharpoonright A, B \in \sigma, \quad u \upharpoonright B, C \in \tau, $$

and we automatically have $u \upharpoonright A, C \in \mathcal{C}$-Plays($A \to C$).

The composition of $\sigma$ and $\tau$ is $\tau \odot \sigma = \{u \upharpoonright A, C \mid u \in \tau \circled{\otimes} \sigma\}$.

It is clear this yields a non-alternating prestrategy, which only requires non-empty and prefix-closed. In composing non-alternating (pre)strategies, there is no analogue of Lemma B.4: all players can move anytime. The unique witness property is lost: $s \in \tau \odot \sigma$ if there is a witness $u \in \tau \circled{\otimes} \sigma$ such that $s = u \upharpoonright A, C$, but $u$ is in general not unique$^{29}$.

That composition preserves strategies will follow from Propositions C.3 and C.5.

<footnote>$^{29}$Causal strategies in $\mathcal{C}$-Strat, with their explicit branching information, recover a unique witness property.</footnote>
### C.1.2. Associativity.
Fix $\sigma : A \to B$, $\tau : B \to C$ and $\delta : C \to D$ non-alternating prestrategies. As above, an **interaction** of $\sigma, \tau$ and $\delta$ is a 3-pre-interaction $w \in |((A \to B) \to C) \to D|^*$ such that

$$w \uparrow A, B \in \sigma, \quad w \uparrow B, C \in \tau, \quad w \uparrow C, D \in \delta,$$

from which it follows automatically that $w \uparrow A, D \in \mathcal{C}-\text{Plays}(A \to D)$.

Again, associativity relies on a “zipping lemma”.

**Lemma C.2 (Zipping).** Consider $u \in \delta \otimes (\tau \odot \sigma)$ and $v \in \tau \otimes \sigma$ such that $u \uparrow A, C = v \uparrow A, C$.

Then, there is $w \in \delta \otimes \tau \otimes \sigma$ such that $w \uparrow A, C, D = u$ and $w \uparrow A, B, C = v$.

Again, $w$ is not unique. The interactions $u$ and $v$ impose causal constraints on $|w|$, and $w$ may be chosen as any ternary interaction respecting those. As in the alternating case there is a mirror lemma, and associativity follows as in Proposition B.9.

**Proposition C.3.** We have $(\delta \odot \tau) \odot \sigma = \delta \odot (\tau \odot \sigma)$.

Associativity works for prestrategies, i.e. it does not rely on *receptive* and *courteous*.

### C.1.3. Copycat.
Non-alternating strategies are intended to model asynchronous concurrency – accordingly, the non-alternating copycat, still written $\omega_A : A \to A$, is an asynchronous forwarder. We first describe the configurations on $A \vdash A$ reached by copycat: those are $x \parallel y$ for $x, y \in \mathcal{C}(A)$, such that $y \subseteq x$, where $\subseteq$ is the “Scott order” [Win13] defined as

$$y \subseteq x \Leftrightarrow y \supseteq x \cap y \subseteq^+ x$$

with polarities taken on $A$. Whenever $\omega_A$ receives a negative event, it forwards it to the other side, but asynchronously: $y$ may contain negative events not yet forwarded to $x$, and $x$ may contain positive events (i.e. negative for $A \vdash A$) not yet forwarded to $y$.

But copycat plays on $A \to A$, not on $A \vdash A$. Remember from Section 2.1.3 that there is

$$\chi_{A,B} : (A \to B) \to (A \vdash B)$$

satisfying the axioms of a map of event structures. We may set:

**Definition C.4.** For $A$ any --arena, we set $\omega_A$ to comprise all $s \in \mathcal{C}-\text{Plays}(A \to A)$ s.t.:

*balanced*: for all $1 \le i \le n$, writing $\chi_{A,A}|_{s_1 \dots s_n} = x \parallel y$, we have $y \subseteq x$,

*well-linked*: for all $[(l, a)]_{a'}$, we have $a = a'$,

where $s = s_1 \dots s_n$.

It is direct that copycat is *receptive* and *courteous*. In fact, it turns out that *receptive* and *courteous* are *exactly* the required conditions for copycat to be neutral for composition:

**Proposition C.5.** Consider $A$ and $B$ two --arenas, and $\sigma : A \to B$ a prestrategy.

Then, $\sigma$ is a strategy if and only if $\omega_B \odot \sigma \odot \omega_A = \sigma$.

*Sketch.* If. It is direct that all non-alternating prestrategies $\omega_B \odot \sigma \odot \omega_A$ are *receptive* and *courteous*. Only if. Considering $w \in \omega_B \otimes \sigma \otimes \omega_A$, using that $\sigma$ is *receptive* and *courteous*, $w$ can be transformed by permuting into $w'$ with the same outer restriction, but where all moves are immediately forwarded by copycat. It follows that the outer restriction is in $\sigma$. $\square$

This was noticed in [GM08], and also holds for causal strategies [RW11]. We deduce:
**Corollary C.6.** The --arenas and non-alternating strategies form a category ⌜-Strat.

*Proof.* Follows from Propositions C.3 and C.5.

<figure><img src="image_110.png" /></figure>

C.1.4. *Further structure.* As for ↓↑-Strat, we have – with the same constructions:

**Proposition C.7.** ⌜-Strat is a cartesian symmetric monoidal closed category.

We could easily adapt the developments of Section 6.1 to show that there is a subcategory of sequential non-alternating strategies, which maps functorially to ↓↑-Strat (without uniformity). However, our attempts to endow ⌜-Strat with symmetry failed, because of the lack of unique witness in compositions. It seems it could be done by using a different approach to symmetry, namely Melliès' group-theoretic formulation of uniformity [Mel03]; this is however left for future work. We conclude this section with:

**Proposition C.8.** There is a symmetric monoidal closed category with products ⌜-Strat<sup>wb</sup>, with objects --arenas, and morphisms well-bracketed non-alternating strategies on A —→ B.

*Proof.* It remains to prove that copycat strategies are well-bracketed and that well-bracketing is preserved by operations on strategies, which is a routine verification.

<figure><img src="image_111.png" /></figure>

# APPENDIX D. THIN CONCURRENT GAMES

In this section, we give some proof for thin concurrent games. Notably, we detail the proofs for the characterisations of configurations of interaction and composition used in this paper: they do not appear in [CCW19], as they were elaborated more recently.

## D.1. Representable functions.
We investigate the functions between domains of configurations representable as maps of event structures.

### D.1.1. Representable functions between configurations.
We will be interested in those functions between configurations arising from maps of event structures:

**Definition D.1.** For A, B, es, a function $f : \mathscr{C}(A) \to \mathscr{C}(B)$ is **representable** if there is a (necessarily unique) map of event structure $\hat{f} : A \to B$ s.t. for all $x \in \mathscr{C}(A)$, $\hat{f}(x) = f(x)$.

*Proof.* For uniqueness, if $f_1, f_2 : A \to B$ have the same image for configurations, we have

$$f_1([a]_A) \stackrel{f_1(a)}{\subset} f_1([a]_A), \quad f_2([a]_A) \stackrel{f_2(a)}{\subset} f_2([a]_A),$$

where $[a]_A = \{a' \in |A| \mid a' <_A a\}$.

Since $f_1([a]_A) = f_2([a]_A)$ and $f_1([a]_A) = f_2([a]_A)$ this entails $f_1(a) = f_2(a)$.

<figure><img src="image_112.png" /></figure>

We shall use the following characterisation of representable functions:

**Lemma D.2.** For A, B, es, a function $f : \mathscr{C}(A) \to \mathscr{C}(B)$ is representable iff it:

preserves the empty set: $f(\emptyset) = \emptyset$

preserves covering: for $x, y \in \mathscr{C}(A)$, if $x \subsetneq y$, then $f(x) \subsetneq f(y)$

preserves unions: for $x, y \in \mathscr{C}(A)$, if $x \cup y \in \mathscr{C}(A)$ then $f(x \cup y) = f(x) \cup f(y)$.
i.e. $\hat{f}(\theta)$, for all $\theta \in \mathcal{S}(A)$. Indeed, consider a covering chain for $\theta$, i.e. a sequence in $\mathcal{S}(A)$:

$$ \emptyset = \theta_0 \stackrel{(a_1, a'_1)}{\subset} \theta_1 \stackrel{(a_2, a'_2)}{\subset} \dots \stackrel{(a_n, a'_n)}{\subset} \theta_n = \theta. $$

We show by induction on $0 \le i \le n$ that $\tilde{f}(\theta_i) = \hat{f}(\theta_i)$. First, $\mathrm{dom} \circ \tilde{f}(\emptyset) = f(\emptyset) = \emptyset$, so $\tilde{f}(\emptyset) = \emptyset = \hat{f}(\emptyset)$. For $0 \le i \le n$, by IH, $\tilde{f}(\theta_i) = \hat{f}(\theta_i)$. We then have:

$$ \begin{aligned} \mathrm{dom}(\tilde{f}(\theta_{i+1})) &= f(\mathrm{dom}(\theta_{i+1})) \\ &= f(\mathrm{dom}(\theta_i) \cup \{a_{i+1}\}) \\ &= f(\mathrm{dom}(\theta_i)) \cup \{\hat{f}(a_{i+1})\}, \end{aligned} $$

and the symmetric reasoning shows $\mathrm{cod}(\tilde{f}(\theta_{i+1})) = \mathrm{cod}(\hat{f}(\theta_i)) \cup \{\hat{f}(a'_{i+1})\}$ as well. But finally, we also have $\tilde{f}(\theta_i) \subseteq \hat{f}(\theta_{i+1})$ since $\tilde{f}$ is monotone. So we must have

$$ \begin{aligned} \tilde{f}(\theta_{i+1}) &= \tilde{f}(\theta_i) \cup \{(\hat{f}(a_{i+1}), \hat{f}(a'_{i+1}))\} \\ &= \hat{f}(\theta_i) \cup \{(\hat{f}(a_{i+1}), \hat{f}(a'_{i+1}))\} \\ &= \hat{f}(\theta_{i+1}), \end{aligned} $$

as required. Now this exactly means that for all $\theta \in \mathcal{S}(A)$ we have $\hat{f}(\theta) \in \mathcal{S}(B)$, and thus $\hat{f}$ is a map of event structures with symmetry. Only if. Obvious. $\square$

**D.2. Interaction and Composition.** Fix $\sigma : A \vdash B$ and $\tau : B \vdash C$ (pre)strategies.

**D.2.1. Interaction.** First, we characterise interaction in terms of its configurations.

We start by recalling that by Lemma 3.12 of [CCW19], there is a pullback

<figure><img src="image_113.png" /></figure>

in the category of event structures with symmetry, the interaction pullback. First, we have:

**Lemma D.5.** For any $x \in \mathcal{C}(\tau \circledast \sigma)$, writing

$$ \Pi_{\sigma} x = x^{\sigma} \parallel x_{C}^{\tau} \in \mathcal{C}(\sigma \parallel C) \qquad \Pi_{\tau} x = x_{A}^{\sigma} \parallel x^{\tau} \in \mathcal{C}(A \parallel \tau), $$

then we have $x^{\sigma} \in \mathcal{C}(\sigma)$ and $x^{\tau} \in \mathcal{C}(\tau)$ causally compatible.

**Proof.** First, $x^{\sigma}$ and $x^{\tau}$ are matching. For causal compatibility, we consider

$$ \varphi_{x^{\sigma}, x^{\tau}} : x^{\sigma} \parallel x_{C}^{\tau} \stackrel{\partial_{\sigma} \parallel x_{C}^{\tau}}{\approx} x_{A}^{\sigma} \parallel x_{B} \parallel x_{C}^{\tau} \stackrel{x_{A}^{\sigma} \parallel \partial_{\tau}^{-1}}{\approx} x_{A}^{\sigma} \parallel x^{\tau} $$

from Definition 4.5, with $(m, n) \lhd (m', n')$ iff $m <_{\sigma} C m'$ or $n <_{A} \tau n'$ which we must prove acyclic. Now, the function which to $c \in x$ associates $(\Pi_{\sigma}(c), \Pi_{\tau}(c))$ is a bijection

$$ \psi : x \approx \varphi_{x^{\sigma}, x^{\tau}}, $$

and we now claim that for all $c, c' \in x$, if $\psi(c) \lhd \psi(c')$, then $c <_{\tau \circledast \sigma} c'$. Indeed, say $c = (m, n)$ and $c' = (m', n')$, with w.l.o.g. $m <_{\sigma} C m'$. Of course then, $m = \Pi_{\sigma}(c)$ and $m' = \Pi_{\tau}(c')$.
Now, we use that $\Pi_{\sigma}$ is a map of event structures, and those always locally reflect causality (Lemma A.2). Therefore, we must have $c <_{\tau \otimes \sigma} c'$ as required.

Therefore a cycle for $\llcorner$ in $\varphi_{x^{\sigma}, x^{\tau}}$ would induce a cycle for $<_{\tau \otimes \sigma}$ in $x$, contradiction. $\square$

**Proposition D.6.** There is a pre-interaction $\tau \circled{\sigma}$, unique up to iso, such that there are

$$(- \circled{–}) : \{(x^{\tau}, x^{\sigma}) \in \mathcal{C}(\tau) \times \mathcal{C}(\sigma) \mid x^{\sigma}, x^{\tau} \text{ causally compatible}\} \cong \mathcal{C}(\tau \circled{\sigma})$$

$$(- \circled{–}) : \{(\theta^{\tau}, \theta^{\sigma}) \in \mathcal{S}(\tau) \times \mathcal{S}(\sigma) \mid \theta^{\sigma}, \theta^{\tau} \text{ causally compatible}\} \cong \mathcal{S}(\tau \circled{\sigma})$$

order-isomorphisms commuting with dom and cod, and satisfying

$$\partial_{\tau \circled{\sigma}}(\theta^{\tau} \circled{\theta^{\sigma}}) = \theta_{A}^{\sigma} \parallel \theta_{B} \parallel \theta_{C}^{\tau}$$

for all $\theta^{\sigma} \in \mathcal{S}(\sigma)$ and $\theta^{\tau} \in \mathcal{S}(\tau)$ causally compatible.

*Proof. Existence.* We must provide the two order-isomorphisms announced. Take $x^{\sigma} \in \mathcal{C}(\sigma)$ and $x^{\tau} \in \mathcal{C}(\tau)$ causally compatible. By Definition 4.5, the bijection

$$\varphi_{x^{\sigma}, x^{\tau}} : x^{\sigma} \parallel x_{C}^{\tau} \stackrel{\partial_{\sigma} \parallel x_{C}^{\tau}}{\cong} x_{A}^{\sigma} \parallel x_{B} \parallel x_{C}^{\tau} \stackrel{x_{A}^{\sigma} \parallel \partial_{\tau}^{-1}}{\cong} x_{A}^{\sigma} \parallel x^{\tau}$$

is secured, i.e. the relation $(m, n) \llcorner (m', n') \Leftrightarrow m \leq_{\sigma} C m' \lor n \leq_{A \parallel \tau} n'$ defined on the graph of $\varphi_{x^{\sigma}, x^{\tau}}$ is acyclic, so its reflexive transitive closure $\leq_{x^{\sigma}, x^{\tau}}$ is a partial order. This turns $\varphi_{x^{\sigma}, x^{\tau}}$ into an event structure, and in fact an ess with identity symmetries. Moreover, there are obvious maps of ess

$$\pi_{\sigma} : \varphi_{x^{\sigma}, x^{\tau}} \rightarrow \sigma \parallel C \qquad \pi_{\tau} : \varphi_{x^{\sigma}, x^{\tau}} \rightarrow A \parallel \tau$$

commuting with display maps, so by the universal property, $\langle \pi_{\sigma}, \pi_{\tau} \rangle : \varphi_{x^{\sigma}, x^{\tau}} \rightarrow \tau \circled{\sigma}$ and

$$x^{\tau} \circled{\ast} x^{\sigma} = \langle \pi_{\sigma}, \pi_{\tau} \rangle (|\varphi_{x^{\sigma}, x^{\tau}}|) \in \mathcal{C}(\tau \circled{\sigma})$$

concludes the definition of the action of $(- \circled{–})$ on causally compatible pairs. Reciprocally, if $x \in \mathcal{C}(\tau \circled{\sigma})$ then its projections yield $\Pi_{\sigma}(x) = x^{\sigma} \parallel x_{C}^{\tau}$ and $\Pi_{\tau}(x) = x_{A}^{\tau} \parallel x^{\tau}$, and by Lemma D.5, $x^{\sigma}$ and $x^{\tau}$ are causally compatible. Finally, for $x^{\sigma}$ and $x^{\tau}$ causally compatible,

$$\Pi_{\sigma}(x^{\tau} \circled{\ast} x^{\sigma}) = x^{\sigma} \parallel x_{C}^{\tau} \qquad \Pi_{\tau}(x^{\tau} \circled{\ast} x^{\sigma}) = x_{A}^{\sigma} \parallel x^{\tau}$$

by construction and if $x \in \mathcal{C}(\tau \circled{\sigma})$, $x = x^{\tau} \circled{\ast} x^{\sigma}$ by universal property of the pullback. The projections are monotone, and the monotonicity of $(- \circled{–})$ follows from the universal property. For symmetries, causal compatibility of $\theta^{\sigma} \in \mathcal{S}(\sigma)$ and $\theta^{\tau} \in \mathcal{S}(\tau)$ amounts to

$$\begin{gathered} x^{\sigma} \parallel x_{C}^{\tau} \stackrel{\Pi_{\sigma}^{-1}}{\cong} x^{\tau} \circled{\ast} x^{\sigma} \stackrel{\Pi_{\tau}}{\cong} x_{A}^{\sigma} \parallel x^{\tau} \\ \theta^{\sigma} \parallel \theta_{C}^{\tau} \parallel \lambda \parallel \theta_{A}^{\sigma} \parallel \theta^{\tau} \\ y^{\sigma} \parallel y_{C}^{\tau} \stackrel{\Pi_{\sigma}}{\cong} y^{\tau} \circled{\ast} y^{\sigma} \stackrel{\Pi_{\tau}}{\cong} y_{A}^{\sigma} \parallel y^{\tau} \end{gathered}$$

commuting, inducing $\theta^{\circled{\ast}} : x^{\tau} \circled{\ast} x^{\sigma} \cong y^{\tau} \circled{\ast} y^{\sigma}$. But symmetries on $\tau \circled{\ast} \sigma$ are precisely those bijections $x^{\tau} \circled{\ast} x^{\sigma} \cong y^{\tau} \circled{\ast} y^{\sigma}$ projecting to $\mathcal{S}(S \parallel C)$ and $\mathcal{S}(A \parallel T)$ as above, so $\theta^{\circled{\ast}} \in \mathcal{S}(\tau \circled{\ast} \sigma)$. Reciprocally, $\theta^{\circled{\ast}} \in \mathcal{S}(\tau \circled{\ast} \sigma)$ induces $\theta^{\sigma} \in \mathcal{S}(\sigma)$ and $\theta^{\tau} \in \mathcal{S}(\tau)$ by projections. That this yields an order-isoc compatible with dom and cod is direct.

*Uniqueness.* Two event structures with symmetry satisfying the hypotheses obviously have isomorphic domains of configurations (and isomorphic domains of symmetries, in a compatible manner). But such order-isomorphisms between domains of configurations and symmetries are automatically representable in the sense of Definition D.3. Therefore, by Lemma D.4 the isomorphisms are generated by isomorphisms of event structures with
symmetry, as required. Preservation of display maps holds for configurations by hypothesis; and by uniqueness in Lemma D.4, two maps of ess with the same action on configurations must be equal. Therefore, the isomorphism commutes with display maps and is an isomorphism of pre-interactions as required. □

### D.2.2. *Composition.*
We aim to prove Propositions 4.10 and 4.12, exploiting Proposition 4.8, along with a few extra lemmas. First, we notice a connection between *minimality* of causally compatible pairs and that maximal events of interactions are visible.

**Lemma D.7.** For $x^\sigma \in \mathscr{C}(\sigma)$ and $x^\tau \in \mathscr{C}(\tau)$ causally compatible, they are minimal causally compatible iff the maximal events of $x^\tau \circled{\tau} x^\sigma$ are visible, e.g. occur in A or C.

*Proof.* If. Consider $y^\sigma \in \mathscr{C}(\sigma)$ and $y^\tau \in \mathscr{C}(\tau)$ causally compatible such that $y^\sigma \subseteq x^\sigma$, $y^\tau \subseteq x^\tau$, while $x_A^\sigma = y_A^\sigma$ and $x_C^\tau = y_C^\tau$. Assume, seeking a contradiction, that we have $y_B \subset x_B$ a strict inclusion. Necessarily, we have $y^\tau \circled{\tau} y^\sigma \subset x^\tau \circled{\tau} x^\sigma$. Take $m \in (y^\tau \circled{\tau} y^\sigma) \setminus (x^\tau \circled{\tau} x^\sigma)$, w.l.o.g. we can assume that $m$ is maximal for $\leq_{\tau \circled{\tau} \sigma}$ in $x^\tau \circled{\tau} x^\sigma$. By hypothesis, $m$ occurs in A or C. But this immediately contradicts the hypothesis that $x_A^\sigma = y_A^\sigma$ and $x_C^\tau = y_C^\tau$.

*Only if.* Assume $x^\sigma, x^\tau$ are minimal causally compatible, and take $m \in x^\tau \circled{\tau} x^\sigma$ maximal. Seeking a contradiction, assume that $m$ occurs in B. So, projecting

$$ \Pi_{\sigma} (x^{\tau} \circled{\tau} x^{\sigma}) = x^{\sigma} \parallel x_{C}^{\tau}, \qquad \Pi_{\tau} (x^{\tau} \circled{\tau} x^{\sigma}) = x_{A}^{\sigma} \parallel x^{\tau}, $$

we have $\Pi_{\sigma} m = (1, s)$ with $s \in x^\sigma$ and $\Pi_{\tau} m = (2, t)$ with $t \in x^\tau$. As maps of event structures locally reflect causality (Lemma A.2), $s$ is maximal in $x^\sigma$ and $t$ is maximal in $x^\tau$. Hence, $y^\sigma = x^\sigma \setminus \{s\} \in \mathscr{C}(\sigma)$ and $y^\tau = x^\tau \setminus \{t\} \in \mathscr{C}(\tau)$. By construction they are causally compatible with the same projections to A and C, contradicting minimality of $x^\sigma$ and $x^\tau$. □

We write $\mathscr{C}^v(\tau \circled{\tau} \sigma)$ for the configurations whose maximal events are visible and likewise for symmetries. Then, the lemma above means that we can refine Proposition 4.8 to:

**Proposition D.8.** *The order-isomorphisms of Proposition 4.8 restrict to*

$$ (- \circled{\tau} -) : \{ (x^\tau, x^\sigma) \in \mathscr{C}(\tau) \times \mathscr{C}(\sigma) \mid x^\sigma \text{ and } x^\tau \text{ minimal causally compatible} \} \simeq \mathscr{C}^v(\tau \circled{\tau} \sigma) $$

$$ (- \circled{\tau} -) : \{ (\theta^\tau, \theta^\sigma) \in \mathscr{S}(\tau) \times \mathscr{S}(\sigma) \mid \theta^\sigma \text{ and } \theta^\tau \text{ minimal causally compatible} \} \simeq \mathscr{S}^v(\tau \circled{\tau} \sigma) $$

Now, it remains to link configurations of $\tau \odot \sigma$ with configurations of $\tau \circled{\tau} \sigma$ with visible maximal events, and likewise for symmetries. First, we fix a few notations. Any configuration $x \in \mathscr{C}(\tau \circled{\tau} \sigma)$ yields a configuration of the composition, its **hiding**, defined as $x_{\downarrow} = x \cap |\tau \odot \sigma| \in \mathscr{C}(\tau \odot \sigma)$. Reciprocally, if $x \in \mathscr{C}(\tau \odot \sigma)$ is a configuration of the composition, its **witness** is defined as

$$ [x]_{\tau \circled{\tau} \sigma} = \{m \in |\tau \circled{\tau} \sigma| \mid \exists n \in x, m \leq_{\tau \circled{\tau} \sigma} n\} \in \mathscr{C}(\tau \circled{\tau} \sigma). $$

The next point we make, is that interactions with visible maximal events are exactly those arising as witnesses of configurations of the composition. More precisely, we have:

**Lemma D.9.** *There are order-isomorphisms compatible with dom, cod and display maps:*

$$ (-)_{\downarrow} : \mathscr{C}^v(\tau \circled{\tau} \sigma) \simeq \mathscr{C}(\tau \odot \sigma) : [-]_{\tau \circled{\tau} \sigma} $$

$$ (-)_{\downarrow} : \mathscr{S}^v(\tau \circled{\tau} \sigma) \simeq \mathscr{S}(\tau \odot \sigma) : [-]_{\tau \circled{\tau} \sigma} $$
*Proof.* For configurations, to $x \in \mathscr{C}^v(\tau \circled{\sigma})$ we associate its hiding $x \downarrow \in \mathscr{C}(\tau \odot \sigma)$. Reciprocally, to $x \in \mathscr{C}(\tau \odot \sigma)$, we associate its witness $[x]_{\tau \circled{\sigma}} \in \mathscr{C}^v(\tau \circled{\sigma})$. Those operations preserve inclusion, and it is an elementary verification that they are inverses.

For symmetries, any $\theta : x \cong_{\tau \circled{\sigma}} y$ must preserve visible events, so it induces by *hiding*

$$ \theta \downarrow : x \downarrow \cong_{\tau \odot \sigma} y \downarrow $$

a symmetry on the composition; and hiding preserves inclusion. Reciprocally, if $\theta : x \cong_{\tau \odot \sigma} y$ then by definition there is $\theta \subseteq \theta' : x' \cong_{\tau \circled{\sigma}} y'$. Necessarily, $[x]_{\tau \circled{\sigma}} \subseteq x'$ and $[y]_{\tau \circled{\sigma}} \subseteq y'$. Since $\theta'$ is an order-iso, by *restriction* we may assume *w.l.o.g.* $\theta' : [x]_{\tau \circled{\sigma}} \cong_{\tau \circled{\sigma}} [y]_{\tau \circled{\sigma}}$.

But the witness $\theta'$ is *unique*: by Lemma 3.33 of [CCW19], if $\theta'' : [x]_{\tau \circled{\sigma}} \cong_{\tau \circled{\sigma}} [y]_{\tau \circled{\sigma}}$ is such that $\theta'' \downarrow = \theta' \downarrow = \theta$, then $\theta' = \theta''$. So to $\theta : x \cong_{\tau \odot \sigma} y$ we associate this unique $\theta' : [x]_{\tau \circled{\sigma}} \cong_{\tau \circled{\sigma}} [y]_{\tau \circled{\sigma}}$. Monotonicity and that these operations are inverses also follow immediately from uniqueness of the witness symmetry, *i.e.* Lemma 3.33 of [CCW19]. $\square$

Composing the order-isomorphisms of Proposition D.8 and Lemma D.9, we get:

**Proposition D.10.** Consider $\sigma : A \vdash B$, and $\tau : B \vdash C$ causal strategies.

There is a causal strategy $\tau \odot \sigma$, unique up to iso, s.t. there are order-isos:

$$ (- \odot -) : \{ (x^\tau, x^\sigma) \in \mathscr{C}(\tau) \times \mathscr{C}(\sigma) \mid x^\sigma, x^\tau \text{ minimal causally compatible} \} \cong \mathscr{C}(\tau \odot \sigma) $$

$$ (- \odot -) : \{ (\theta^\tau, \theta^\sigma) \in \mathscr{S}(\tau) \times \mathscr{S}(\sigma) \mid \theta^\sigma, \theta^\tau \text{ minimal causally compatible} \} \cong \mathscr{S}(\tau \odot \sigma) $$

commuting with dom and cod; s.t., for $\theta^\sigma \in \mathscr{S}(\sigma)$, $\theta^\tau \in \mathscr{S}(\tau)$ minimal causally compatible,

$$ \partial_{\tau \odot \sigma}(\theta^\tau \odot \theta^\sigma) = \theta_A^\sigma \parallel \theta_C^\tau. $$

*Proof. Existence.* Direct by Proposition D.8 and Lemma D.9.

*Uniqueness.* As in the proof of Proposition 4.8. $\square$

This means that any configuration $x \in \mathscr{C}(\tau \odot \sigma)$ may be written uniquely as $x^\tau \odot x^\sigma$ for $x^\sigma \in \mathscr{C}(\sigma)$ and $x^\tau \in \mathscr{C}(\tau)$ minimal causally compatible – note that from the construction of the order-isomorphism in the proposition above, we then have $x^\tau \circled{\sigma} x^\sigma = [x^\tau \odot x^\sigma]_{\tau \circled{\sigma}}$.

### D.2.3. +-covered case.
Finally, it remains to prove Proposition 4.12.

In essence, Proposition 4.12 is a specialization of Proposition 4.10 to strategies. Consider therefore from now on that $\sigma : A \vdash B$ and $\tau : B \vdash C$ are strategies. First of all, we show that for +-covered configurations we can omit the minimality assumption.

**Lemma D.11.** Consider $x^\sigma \in \mathscr{C}^+(\sigma)$ and $x^\tau \in \mathscr{C}^+(\tau)$ causally compatible +-covered.

Then, $x^\sigma$ and $x^\tau$ are minimal causally compatible.

*Proof.* Seeking a contradiction, assume $y^\sigma$ and $y^\tau$ are causally compatible such that $y^\tau \circled{\sigma} y^\sigma \subseteq x^\tau \circled{\sigma} x^\sigma$ with $x_A^\sigma = y_A^\sigma$ and $x_C^\tau = y_C^\tau$. Without loss of generality, consider $m \in (x^\tau \circled{\sigma} x^\sigma) \setminus (y^\tau \circled{\sigma} y^\sigma)$ maximal for $\leq_{\tau \circled{\sigma}}$. By hypothesis, $m$ occurs in $B$. Therefore, projecting

$$ \Pi_{\sigma}(m) = (1, s) \qquad \Pi_{\tau}(m) = (2, t), $$

maximality of $m$ in $x^\tau \circled{\sigma} x^\sigma$ entails via Lemma A.2 that $s$ is maximal in $x^\sigma$ and $t$ maximal in $x^\tau$. But necessarily, $s$ and $t$ has dual polarities: w.l.o.g. say that $\mathrm{pol}_\sigma(s) = +$ and $\mathrm{pol}_\tau(t) = -$. So, $t$ is negative maximal in $x^\tau$, contradicting that $x^\tau \in \mathscr{C}^+(\tau)$ is +-covered. $\square$

So in a synchronization between +-covered configurations, the maximal events are visible as if they are synchronized, they will be both maximal and negative for one of the two players. Resulting configurations of the composition are automatically +-covered:
**Lemma D.12.** For $x^{\sigma} \in \mathscr{C}^{+}(\boldsymbol{\sigma})$, $x^{\tau} \in \mathscr{C}^{+}(\boldsymbol{\tau})$ causally compatible, $x^{\tau} \odot x^{\sigma} \in \mathscr{C}^{+}(\boldsymbol{\tau} \odot \boldsymbol{\sigma})$.

*Proof.* Consider $m \in x^{\tau} \odot x^{\sigma}$ maximal. This means that $m$ is also maximal in $x^{\tau} \circled{\circ} x^{\sigma} = [x^{\tau} \circled{\circ} x^{\sigma}]_{\boldsymbol{\tau} \circled{\circ} \boldsymbol{\sigma}}$. Necessarily, $m$ occurs in $A$ or $C$, w.l.o.g. assume it occurs in $C$. Then, $\Pi_{\boldsymbol{\tau}}(m)$ has the form $(2,t)$ where using Lemma A.2, necessarily $t$ is maximal (for $\leq_{\boldsymbol{\tau}}$) in $x^{\tau}$. But then, since $x^{\tau}$ is $+-$covered, $t$ is positive – hence, $m$ is positive as well. $\square$

So causally compatible $+-$covered $x^{\sigma} \in \mathscr{C}^{+}(\boldsymbol{\sigma})$ and $x^{\tau} \in \mathscr{C}^{+}(\boldsymbol{\tau})$ are minimal, and their composition yields $x^{\tau} \odot x^{\sigma} \in \mathscr{C}^{+}(\boldsymbol{\tau} \odot \boldsymbol{\sigma})$ $+-$covered. We prove the converse:

**Lemma D.13.** Consider $x^{\sigma} \in \mathscr{C}(\boldsymbol{\sigma})$ and $x^{\tau} \in \mathscr{C}(\boldsymbol{\tau})$ minimal causally compatible.

If $x^{\tau} \odot x^{\sigma} \in \mathscr{C}^{+}(\boldsymbol{\tau} \odot \boldsymbol{\sigma})$ is $+-$covered, so are $x^{\sigma} \in \mathscr{C}^{+}(\boldsymbol{\sigma})$ and $x^{\tau} \in \mathscr{C}^{+}(\boldsymbol{\tau})$.

*Proof.* Consider $s \in x^{\sigma}$ maximal. Necessarily, there is a unique $m \in x^{\tau} \circled{\circ} x^{\sigma}$ such that $\Pi_{\sigma}(m) = (1, s)$. Assume first that $m$ is maximal in $x^{\tau} \circled{\circ} x^{\sigma}$. As $x^{\tau} \circled{\circ} x^{\sigma} = [x^{\tau} \odot x^{\sigma}]_{\boldsymbol{\tau} \circled{\circ} \boldsymbol{\sigma}}$, if $m$ is maximal it must be visible and maximal in $x^{\tau} \odot x^{\sigma}$. Therefore, it is positive by hypothesis, and $s$ is positive.

Otherwise, assume $m$ is not maximal, so there is some $m \to_{\boldsymbol{\tau} \circled{\circ} \boldsymbol{\sigma}} n$. By Lemma 4.21,

$$ \Pi_{\sigma}(m) \to_{\sigma \parallel C} \Pi_{\sigma}(n) \quad \text{or} \quad \Pi_{\tau}(m) \to_{A \parallel \tau} \Pi_{\tau}(n). $$

If this is the former, then there is $s \to_{\sigma} s'$ with $s' \in x^{\sigma}$, absurd by maximality of $s$. If this is the latter, then two cases arise. If $m$ occurs in $A$, then $\Pi_{\tau}(m) = (1, a)$ and $\Pi_{\tau}(n) = (1, a')$ with $a \to_{A} a'$. Likewise, $\Pi_{\sigma}(m) = (1, s)$ and $\Pi_{\sigma}(n) = (1, s')$. But then by Lemma A.2, we must have $s <_{\sigma} s'$ contradicting again the maximality of $s$. Finally, if $m$ occurs in $B$, then $\Pi_{\tau}(m) = (2, t)$ and $\Pi_{\tau}(n) = (2, t')$ with $t \to_{\tau} t'$. We split cases one last time, depending on the polarity of $t$ in $\boldsymbol{\tau}$. If $t$ is negative, then $s$ is positive in $\boldsymbol{\sigma}$ as required. Otherwise, by courtesy of $\boldsymbol{\tau}$ we must have $\partial_{\tau}(t) \to_{B \to C} \partial_{\tau}(t')$. In particular, $t'$ must also occur in $B$ and we must have $\Pi_{\sigma}(n) = (1, s')$ for $s' \in x^{\sigma}$, with moreover $\partial_{\sigma}(s) \to_{A \to B} \partial_{\sigma}(s')$. Therefore, again by Lemma A.2, we must have $s <_{\sigma} s'$ contradicting the maximality of $s$.

The symmetric reasoning shows that any $t \in x^{\tau}$ maximal in $x^{\tau}$ is positive. $\square$

We are almost in position to prove Proposition 4.12 – the only missing piece is *uniqueness*:

**Lemma D.14.** Consider $\boldsymbol{\sigma}, \boldsymbol{\tau} : A$ two causal strategies. Assume there are

$$ \psi : \mathscr{C}^{+}(\boldsymbol{\sigma}) \simeq \mathscr{C}^{+}(\boldsymbol{\tau}) \qquad \psi : \mathscr{S}^{+}(\boldsymbol{\sigma}) \simeq \mathscr{S}^{+}(\boldsymbol{\tau}) $$

order-isomorphisms compatible with dom, cod, and display maps.

Then, $\boldsymbol{\sigma}$ and $\boldsymbol{\tau}$ are isomorphic.

*Proof.* We extend $\psi$ to all configurations and all symmetries, and conclude via Lemma D.4.

Let $x \in \mathscr{C}(\boldsymbol{\sigma})$. Consider $x^{+} \in \mathscr{C}(\boldsymbol{\sigma})$ minimal such that $x^{+} \subseteq -x$. Necessarily, $x^{+} \in \mathscr{C}^{+}(\boldsymbol{\sigma})$, so we may take $\psi(x^{+}) \in \mathscr{C}^{+}(\boldsymbol{\tau})$. Now, since $\psi$ is compatible with display maps,

$$ \partial_{\tau}(\psi(x^{+})) \subseteq - \partial_{\sigma}(x), $$

therefore by receptivity and courtesy (see Lemma 3.13 from [CCRW17]), there is a unique $y \in \mathscr{C}(\boldsymbol{\tau})$ such that $\psi(x^{+}) \subseteq - y$ and $\partial_{\tau}(y) = \partial_{\sigma}(x)$; we set $\psi(x) = y$.

We must show this extended $\psi$ preserves inclusion; we show it preserves covering, and distinguish the positive and negative cases. First, consider configurations in $\mathscr{C}(\boldsymbol{\sigma})$:

$$ x \stackrel{s^{+}}{\rightleftharpoons} y, $$
which means $x^+ \subseteq -z \subset y^+$. Now, by hypothesis $\psi(x^+) \subseteq \psi(y^+)$, so $\psi(x^+) \subseteq \psi(y)$. Moreover, this inclusion must contain exactly one positive event, write it $t^+ \in \psi(y) \setminus \psi(x^+)$ – necessarily, $\partial_\tau(t) = \partial_\sigma(s)$. Now, notice $\partial_\tau(t)$ is maximal in $\partial_\tau(\psi(y))$: indeed,

$$ \partial_{\tau}(\psi(x)) = \partial_{\sigma}(x) \xrightarrow{\partial_{\sigma}(s)} \partial_{\sigma}(y) = \partial_{\tau}(\psi(y)) $$

by hypothesis. So, by courtesy, $t$ is maximal in $\psi(y)$ as well. So, we have $z = \psi(y) \setminus \{t\} \in \mathscr{C}(\tau)$. Moreover, $\partial_\tau(z) = \partial_\tau(\psi(y)) \setminus \{\partial_\tau(t)\} = \partial_\sigma(x)$. So, $\psi(x^+) \subseteq -z$ with $\partial_\tau(z) = \partial_\sigma(x)$, therefore $z = \psi(x)$; and $\psi(x) \subsetneq \psi(y)$ as required. Considering now a negative extension, i.e.

$$ x \xrightarrow{s} y, $$

it follows that $x^+ = y^+$ and $\psi(x) \subsetneq \psi(y)$ is immediate by receptivity. Altogether we have

$$ \psi : \mathscr{C}(\sigma) \to \mathscr{C}(\tau) $$

compatible with display maps and preserving inclusion. Likewise we construct $\psi^{-1} : \mathscr{C}(\tau) \to \mathscr{C}(\sigma)$ preserving inclusion from its action on $+\text{-covered configurations}$. That they are inverses is immediate from $\psi$ being a bijection between $+\text{-covered configurations}$, and receptivity.

Now, we consider the action of $\psi$ on symmetries. If $\theta \in \mathscr{S}(\sigma)$, consider $\theta^+ \in \mathscr{C}(\sigma)$ minimal s.t. $\theta^+ \subseteq -\theta$ – recall that as a symmetry, $\theta$ is an order-iso preserving polarities, so this is well-defined. Now, $\theta^+ \in \mathscr{S}^+(\sigma)$, so that we may take $\psi(\theta^+) \in \mathscr{S}^+(\tau)$ as for configurations. Again, since $\psi$ is compatible with display maps, we have

$$ \partial_{\tau}(\psi(\theta^{+})) \subseteq -\partial_{\sigma}(\theta). $$

By receptivity and courtesy of $\tau$, there are unique extensions of $\mathrm{dom}(\psi(\theta^+))$ and $\mathrm{cod}(\psi(\theta^+))$ to $\psi(\mathrm{dom}(\theta))$ and $\psi(\mathrm{cod}(\theta))$, projecting via $\partial_\tau$ to $\mathrm{dom}(\partial_\sigma(\theta))$ and $\mathrm{cod}(\partial_\sigma(\theta))$ respectively. We get $\psi(\theta^+) \subseteq -\Omega \in \mathscr{S}(\tau)$ by iterating $\sim$-receptivity for $\tau$, such that $\partial_\tau(\Omega) = \partial_\sigma(\theta)$ – which characterises $\Omega$ as the composition

$$ \psi(\mathrm{dom}(\theta)) \stackrel{\tau}{\cong} \mathrm{dom}(\partial_{\sigma}(\theta)) \stackrel{\partial_{\sigma}(\theta)}{\cong_A} \mathrm{cod}(\partial_{\sigma}(\theta)) \stackrel{\tau}{\cong} \psi(\mathrm{cod}(\theta)), $$

so a unique extension of $\psi(\theta^+)$ matching $\partial_\sigma(\theta)$ and compatible with display maps – we fix $\psi(\theta) = \Omega$. Monotonicity is immediate from compatibility with $\mathrm{dom}$ and $\mathrm{cod}$ and that $\psi$ preserves covering $\subsetneq$ on configurations. Likewise we extend $\psi^{-1}$ to all symmetries; that $\psi$ and $\psi^{-1}$ are inverses follows as they preserve covering and are inverses on configurations. $\square$

We may now conclude our final characterization of composition:

**Proposition D.15.** Consider $\sigma : A \vdash B$ and $\tau : B \vdash C$ causal strategies.

Then, there is a strategy $\tau \odot \sigma : A \vdash C$, unique up to iso, such that there are order-isos:

$$ (- \odot -) : \{ (x^\tau, x^\sigma) \in \mathscr{C}^+(\tau) \times \mathscr{C}^+(\sigma) \mid x^\sigma \text{ and } x^\tau \text{ causally compatible} \} \simeq \mathscr{C}^+(\tau \odot \sigma) $$

$$ (- \odot -) : \{ (\theta^\tau, \theta^\sigma) \in \mathscr{S}^+(\tau) \times \mathscr{S}^+(\sigma) \mid \theta^\sigma \text{ and } \theta^\tau \text{ causally compatible} \} \simeq \mathscr{S}^+(\tau \odot \sigma) $$

commuting with $\mathrm{dom}$ and $\mathrm{cod}$, and s.t., for $\theta^\sigma \in \mathscr{S}^+(\sigma)$ and $\theta^\tau \in \mathscr{S}^+(\tau)$ causally compatible,

$$ \partial_{\tau \odot \sigma}(\theta^\tau \odot \theta^\sigma) = \theta_A^\sigma \parallel \theta_C^\tau. $$

*Proof. Existence.* Simply a restriction of the isomorphisms of Proposition 4.10. By Lemma D.11, causally compatible $x^\sigma \in \mathscr{C}^+(\sigma)$ and $x^\tau \in \mathscr{C}^+(\tau)$ are automatically minimal, and by Lemma D.12, $x^\tau \odot x^\sigma \in \mathscr{C}^+(\tau \odot \sigma)$ is $+\text{-covered}$. Reciprocally, if $x^\tau \odot x^\sigma \in \mathscr{C}^+(\tau \odot \sigma)$ is $+\text{-covered}$, then by Lemma D.14, so are $x^\sigma \in \mathscr{C}^+(\sigma)$ and $x^\tau \in \mathscr{C}^+(\tau)$. Since the isomorphism
($\ominus$ -) is compatible with dom and cod and symmetries are order-isomorphisms, there observations apply to symmetries. *Uniqueness*. By Lemma D.14. □

### D.3. Charactering immediate causality.

**Lemma D.16.** For $\sigma: A \vdash B$, $\tau: B \vdash C$ causal prestrategies, for $m, m' \in |\tau \circled{\ast} \sigma|$, if $m \to_{\tau \circled{\ast} \sigma} m'$, then $m_{\sigma} \to_{\sigma} m'_{\sigma}$, or $m_{\tau} \to_{\tau} m'_{\tau}$, where $m_{\sigma}, m_{\tau}$ are defined whenever used.

*Proof.* If $m \to_{\tau \circled{\ast} \sigma} m'$, then $x = [m]_{\tau \circled{\ast} \sigma} \setminus \{m, m'\} \in \mathscr{C}(\tau \circled{\ast} \sigma)$. Then we have

$$x = x^{\tau} \circled{\ast} x^{\sigma} \stackrel{m}{\subset} y^{\tau} \circled{\ast} y^{\sigma} \stackrel{m'}{\subset} z^{\tau} \circled{\ast} z^{\sigma} = [m]_{\tau \circled{\ast} \sigma}$$

in $\mathscr{C}(\tau \circled{\ast} \sigma)$, inlining the order-isomorphism of Proposition 4.7. Let us focus first on

$$x^{\tau} \circled{\ast} x^{\sigma} \stackrel{m}{\subset} y^{\tau} \circled{\ast} y^{\sigma}.$$

Since $(- \circled{\ast} -)$ is an order-iso, this yields a covering in the partial order of causally compatible pairs, ordered by pairwise inclusion. By compatibility with display maps these inclusions add exactly one event in $A$, in $B$, or in $C$. This yields three cases: (a) $m$ occurs in $A$, $x^{\tau} = y^{\tau}$, and $x^{\sigma} \subsetneq y^{\sigma}$ adds one event $s \in |\sigma|$; (b) $m$ occurs in $C$, $x^{\sigma} = y^{\sigma}$ and $x^{\tau} \subsetneq y^{\tau}$ adds one event $t \in |\tau|$; or (c) $m$ occurs in $B$, $x^{\sigma} \subsetneq y^{\sigma}$ adds one event $s$ and $x^{\tau} \subsetneq y^{\tau}$ adds one event $t$ with $\partial_{\sigma}(s) = (2, b)$ and $\partial_{\tau}(t) = (1, b)$.

Now, back to considering $m$ and $m'$. If both occur in $C$, then we have

$$x^{\tau} \circled{\ast} x^{\sigma} \stackrel{m}{\subset} y^{\tau} \circled{\ast} x^{\sigma} \stackrel{m'}{\subset} z^{\tau} \circled{\ast} x^{\sigma},$$

with $x^{\tau} \stackrel{t}{\subset} y^{\tau} \stackrel{t'}{\subset} z^{\tau}$. If $t <_{\tau} t'$, then $t \to_{\tau} t'$ and we are done. Otherwise, we also have

$$x^{\tau} \stackrel{t'}{\subset} u^{\tau} \stackrel{t}{\subset} z^{\tau},$$

and as $t'$ occurs in $C$ we also have $x^{\sigma}$ and $u^{\tau}$ causally compatible. Therefore

$$x^{\tau} \circled{\ast} x^{\sigma} \stackrel{n'}{\subset} u^{\tau} \circled{\ast} x^{\sigma} \stackrel{n}{\subset} z^{\tau} \circled{\ast} x^{\sigma}$$

for some $n, n' \in |\tau \circled{\ast} \sigma|$ since $\circled{\ast}$ is an order-isomorphism, so $\{n, n'\} = \{m, m'\}$. But since $u^{\tau} \circled{\ast} x^{\sigma} \neq y^{\tau} \circled{\ast} x^{\sigma}$ we must have $n = m$ and $n' = m'$, contradicting $m <_{\tau \circled{\ast} \sigma} m'$.

The case where $m$ and $m'$ both occur in $A$ is symmetric. If $m$ occurs in $A$ and $m'$ in $C$,

$$x^{\tau} \circled{\ast} x^{\sigma} \stackrel{m}{\subset} x^{\tau} \circled{\ast} z^{\sigma} \stackrel{m'}{\subset} z^{\tau} \circled{\ast} z^{\sigma}$$

with $x^{\sigma} \stackrel{s}{\subset} z^{\sigma}$ and $x^{\tau} \stackrel{t}{\subset} z^{\tau}$. But then $x^{\sigma}$ and $z^{\tau}$ are also causally compatible, and

$$x^{\tau} \circled{\ast} x^{\sigma} \subsetneq z^{\tau} \circled{\ast} x^{\sigma} \subsetneq z^{\tau} \circled{\ast} z^{\sigma}$$

which as above contradicts $m <_{\tau \circled{\ast} \sigma} m'$. The case where $m$ occurs in $C$ and $m'$ occurs in $A$ is symmetric. Now, assume $m$ occurs in $A$ and $m'$ occurs in $B$. Then we have

$$x^{\tau} \circled{\ast} x^{\sigma} \stackrel{m}{\subset} x^{\tau} \circled{\ast} y^{\sigma} \stackrel{m'}{\subset} z^{\tau} \circled{\ast} z^{\sigma}$$

where $x^{\sigma} \stackrel{s}{\subset} y^{\sigma}$, $x^{\tau} \stackrel{t}{\subset} z^{\tau}$, and $y^{\sigma} \stackrel{s'}{\subset} z^{\sigma}$. If $s <_{\sigma} s'$, then $s \to_{\sigma} s'$ and we are done. Otherwise, we also have $x^{\sigma} \subsetneq u^{\sigma} \subsetneq z^{\sigma}$, $u^{\sigma}$ and $z^{\tau}$ are also causally compatible, and

$$x^{\tau} \circled{\ast} x^{\sigma} \subsetneq z^{\tau} \circled{\ast} u^{\sigma} \subsetneq z^{\tau} \circled{\ast} z^{\sigma},$$
contradiction. All cases with one event occurring in B and the other in A or C are symmetric. Finally, assume both m and m' occur in B. In that case, we have

$$x^{\sigma} \stackrel{s}{\subset} y^{\sigma} \stackrel{s'}{\subset} z^{\sigma}, \quad \text{and} \quad x^{\tau} \stackrel{t}{\subset} y^{\tau} \stackrel{t'}{\subset} z^{\tau}.$$

If we have $s <_{\sigma} s'$ then $s \to_{\sigma} s'$ and we are done, and likewise for $t \to_{\tau} t'$. Otherwise, $x^{\sigma} \subsetneq u^{\sigma} \subsetneq z^{\sigma}$ and $x^{\tau} \subsetneq u^{\tau} \subsetneq z^{\tau}$, and $x^{\tau} \circled{\tau} x^{\sigma} \subsetneq u^{\tau} \circled{\tau} u^{\sigma} \subsetneq z^{\tau} \circled{\tau} z^{\sigma}$, contradiction. $\square$

**Lemma D.17.** Consider $m, m' \in |\tau \circled{\sigma}|$ such that $m \to_{\tau \circled{\sigma}} m'$.

Then, if $m_{\sigma} <_{\sigma} m'_{\sigma}$ we have $m_{\sigma} \to_{\sigma} m'_{\sigma}$, and likewise for $\tau$.

*Proof.* If $m \to_{\tau \circled{\sigma}} m'$, then there is $x^{\tau} \circled{\tau} x^{\sigma}, y^{\tau} \circled{\tau} y^{\sigma}$ and $z^{\tau} \circled{\tau} z^{\sigma}$ in $\mathscr{C}(\tau \circled{\sigma})$ such that

$$x^{\tau} \circled{\tau} x^{\sigma} \stackrel{m}{\subset} y^{\tau} \circled{\tau} y^{\sigma} \stackrel{m'}{\subset} z^{\tau} \circled{\tau} z^{\sigma},$$

but if $m_{\sigma}$ and $m'_{\sigma}$ are defined then $x^{\sigma} \stackrel{m_{\sigma}}{\subset} y^{\sigma} \stackrel{m'_{\sigma}}{\subset} z^{\sigma}$. If $m_{\sigma} <_{\sigma} m'_{\sigma}$, $m_{\sigma} \to_{\sigma} m'_{\sigma}$. $\square$

**D.4. The Bang Lemma.** Now, we prove the *bang lemma* from AJM games [AJM00]. Fix A and B two concrete arenas with B pointed, and $\sigma : !A \vdash !B$ a causal strategy.

By *receptive*, for each $i \in \mathbb{N}$, there is a unique $q_i \in \min(\sigma)$ such that $\partial_{\sigma}(q_i) = (2, (i, b))$ the unique minimal move of B of copy index i. Let us write

$$|\sigma_i| = \{m \in |\sigma| \mid q_i \leq_{\sigma} m\}$$

for the set of events of $\sigma$ above $q_i$. Since $\sigma$ is pointed, it follows that for $i, j \in \mathbb{N}$ distinct, $|\sigma_i|$ and $|\sigma_j|$ are disjoint. Likewise, since arenas are concrete, moves in immediate conflict have the same predecessor – it follows that if $m \in |\sigma_i|$ and $n \in |\sigma_j|$, the negative dependencies of $m$ and $n$ are compatible, hence $m$ and $n$ are compatible by *determinism*. Therefore, we have $\sigma \cong_{||_{i \in \mathbb{N}}} \sigma_i$ where $\sigma_i$ has a structure of ess directly imported from $\sigma$. Furthermore, $\sigma_i : !A \vdash B$ with the display map $\partial_{\sigma_i}$ defined in the obvious way. The key argument is:

**Lemma D.18.** For any $i, j \in \mathbb{N}$, we have $\sigma_i \approx \sigma_j$.

*Proof.* We exploit Lemma D.2 and build a (necessarily representable) iso between the domains of configurations, compatible with symmetry. Consider $x_i \in \mathscr{C}(\sigma_i)$, with

$$\partial_{\sigma}(x_i) = x_A \parallel \{i\} \times x_B.$$

From Definition 7.19, $x_A \parallel \{i\} \times x_B \cong_{!A \vdash !B} x_A \parallel \{j\} \times x_B$ with the obvious symmetry $\theta_{i,j}$. We must transport $x_i$ along this negative symmetry $\theta_{i,j}$. By Lemma B.4 from [CCW19], there are unique $x_j \in \mathscr{C}(\sigma)$ and $\psi : x_i \cong_{\sigma} x_j$ s.t. $\partial_{\sigma} \psi = \theta^+ \circ \theta_{i,j}^-$ for some

$$\theta^+ : x_A \parallel \{j\} \times x_B \cong_{!A \parallel !B} y_A \parallel \{j\} \times y_B$$

where we know that $j$ is unchanged, because of condition $+-\text{transparent}$ of Definition 7.19. Therefore, $x_j \in \mathscr{C}(\sigma_j)$ as required. Monotonicity of this operation and the fact that it is a bijection between configurations follow from the *uniqueness* clause for Lemma B.4 of [CCW19]; compatibility with symmetry follows from composition with the symmetry $\psi$.

This induces an isomorphism of ess $\varphi : \sigma_i \approx \sigma_j$ which we must still check is a positive isomorphism. But for $x_i \in \mathscr{C}(\sigma_i)$, the symmetry $\theta^+$ above entails

$$\partial_{\sigma_i}(x_i) = x_A \parallel x_B \stackrel{\varphi^+}{\cong_{!A \vdash B}} y_A \parallel y_B = \partial_{\sigma_j}(x_j)$$

ensuring that the triangle commutes up to positive symmetry as required. $\square$
Next we lift a positive isomorphism on one copy index to the whole strategy:

**Lemma D.19.** Consider A and B concrete --arenas with B pointed, and $\sigma, \tau : !A \vdash !B$. If $\sigma_0 \approx \tau_0$, then $\sigma \approx \tau$.

*Proof.* By Lemma D.18, for $i \in \mathbb{N}$, $\sigma_i \approx \sigma_0 \approx \tau_0 \approx \tau_i$, we conclude by parallel composition. $\square$

<figure><img src="image_114.png" /></figure>

We may finally deduce the bang lemma:

**Lemma D.20.** For concrete arenas A, B with B pointed and $\sigma \in \rightarrow\text{-Strat}(!A, !B)$,

$$(\mathrm{der}_B \odot \sigma)^{\dagger} \approx \sigma.$$

*Proof.* By Proposition 4.12 and a reasoning analogous to Proposition 4.19, we have $\mathrm{der}_B \odot \sigma \approx \sigma_0$. Therefore, by Lemma D.19, for any two $\sigma, \tau : !A \vdash !B$, if $\mathrm{der}_B \odot \sigma \approx \mathrm{der}_B \odot \tau$, then $\sigma \approx \tau$. The lemma follows directly from that and the Seely category laws. $\square$

<figure><img src="image_115.png" /></figure>

**D.5. Expansion of Meager Strategies.** Consider $\sigma : A$ parallel innocent. We first observe that any move $m \in |\sigma|$ is determined by $\mathrm{mf}(m)$, along with the copy index of its negative dependencies. An exponential slice for $y \in \mathscr{C}(\mathrm{mf}(\sigma))$ normal is an assignment of copy indices for all negative questions of $y$ – or more precisely,

$$\alpha : y^{Q,-} \rightarrow \mathbb{N},$$

with $y^{Q,-}$ the negative questions of $y$. To any $x \in \mathscr{C}(\sigma)$ we have associated $\mathrm{mf}(x) \in \mathscr{C}(\mathrm{mf}(\sigma))$. To complete $\mathrm{mf}(x)$, we also associate to $x$ an exponential slice for $\mathrm{mf}(x):

$$\begin{array}{l} \mathrm{slice}(x) : (\mathrm{mf}(x))^{Q,-} \rightarrow \mathbb{N} \\ n^{-} \mapsto \mathrm{ind}(\partial_{\sigma}(\theta_{x}^{-1}(n))). \end{array}$$

We now show how to reconstruct events of $\sigma$ from $\mathrm{mf}(\sigma)$ and an exponential slice.

**Lemma D.21.** Consider A a concrete arena, $\sigma : A$ a causal strategy, and $y \in \mathscr{C}(\mathrm{mf}(\sigma))$.

For any $\alpha : y^{Q,-} \rightarrow \mathbb{N}$, there is a unique $x \in \mathscr{C}(\sigma)$ such that $y = \mathrm{mf}(x)$, $\alpha = \mathrm{slice}(x)$, and $x \cong_{\sigma} y$. Moreover, the symmetry $\varphi_y : y \cong_{\sigma} x$ is unique.

*Proof.* Same proof as for Lemma 7.24, setting up indices following $\alpha$ instead of 0. $\square$

<figure><img src="image_116.png" /></figure>

Just as Lemma 7.24, for $\sigma : A$ parallel innocent, Lemma D.21 can be used to assemble an event $m \in |\mathrm{mf}(\sigma)|$ and an exponential slice $\alpha : [m]^{Q,-} \rightarrow \mathbb{N}$ into $n \in |\sigma|$ s.t. $\mathrm{mf}(n) = m$ and $\mathrm{slice}([n]_{\sigma}) = \alpha$. So together, Lemmas 7.24 and D.21 establish a bijection between $|\sigma|$ and pairs $(m, \alpha)$ of $m \in |\mathrm{mf}(\sigma)|$ and an exponential slice $\alpha : [m]^{Q,-} \rightarrow \mathbb{N}$. From this it seems clear how to reconstruct $\sigma$ from $\mathrm{mf}(\sigma)$: first, we reconstruct a partial order.

**Proposition D.22.** For A a concrete arena and $\sigma : A^+$, we define a partial order $\exp(\sigma)$:

$$\begin{array}{l} |\exp(\sigma)| = \{(m, \alpha) \mid m \in |\sigma| \wedge \alpha : [m]^{Q,-} \rightarrow \mathbb{N}\} \\ (m_1, \alpha_1) \leq_{\exp(\sigma)} (m_2, \alpha_2) \iff m_1 \leq_{\sigma} m_2 \wedge \forall n^{-} \leq_{\sigma} m_1, \alpha_1(n) = \alpha_2(n). \end{array}$$

Then, for any $\sigma : A, \sigma$ and $\exp(\mathrm{mf}(\sigma))$ are isomorphic partial orders.

*Proof.* Direct consequence of Lemmas 7.24 and D.21. $\square$
It remains to complete $\exp(\boldsymbol{\sigma})$ into a causal strategy. The display map is determined by a choice of copy index for positive questions. Hence, for any $m^{Q,+} \in |\boldsymbol{\sigma}|$, assume fixed some

$$f_m : \mathbb{N}^{[m]} \xrightarrow{\boldsymbol{\sigma}, -} \mathbb{N}$$

specifying, for each Player question, its copy index depending on indices of Opponent questions in its causal dependency. For simplicity, we assume this choice is globally injective, i.e. $f_m, f_n$ have disjoint codomains for distinct $m, n \in |\boldsymbol{\sigma}|$. The resulting strategy will not depend on the choice of the family $(f_m)_{m \in |\boldsymbol{\sigma}|_{Q,+}}$ up to positive isomorphism.

**Proposition D.23.** Consider A a concrete arena, $\boldsymbol{\sigma} : A^+$ parallel innocent causally well-bracketed. We define a display map $\partial_{\exp(\boldsymbol{\sigma})}$ for $\exp(\boldsymbol{\sigma})$ by induction, with image

$$\begin{align*}
\partial_{\exp(\boldsymbol{\sigma})}(m^A, \alpha) &= a, \\
\partial_{\exp(\boldsymbol{\sigma})}(m^{Q,-}, \alpha) &= q \quad \text{s.t. } \text{ind}(q) = \alpha(m), \\
\partial_{\exp(\boldsymbol{\sigma})}(m^{Q,+}, \alpha) &= q \quad \text{s.t. } \text{ind}(q) = f_m(\alpha),
\end{align*}$$

where $a, q$ is the unique event of A with label $lbl(m)$, predecessor $\partial_{\exp(\boldsymbol{\sigma})}(\text{just}(m, \alpha))$ with just($m, \alpha$) defined as just($m$) with slice the restriction of $\alpha$, label $lbl(m)$; satisfying the additional constraint given. Further components are:

$$\begin{align*}
(m, \alpha) \#_{\exp(\boldsymbol{\sigma})} (n, \beta) &\Leftrightarrow m \#_{\boldsymbol{\sigma}} n, \text{ and } \alpha \text{ and } \beta \text{ coincide on their common domain} \\
\theta \in \mathcal{S}(\exp(\boldsymbol{\sigma})) &\Leftrightarrow \theta : x \cong y \text{ order-iso s.t. } \pi_1 = \pi_1 \circ \theta.
\end{align*}$$

Then, $\exp(\boldsymbol{\sigma}) : A$ is parallel innocent causally well-bracketed.

The only difficulty is in handling conflict. A positive iso $\varphi : \boldsymbol{\sigma}_1 \approx \boldsymbol{\sigma}_2$ directly lifts to $\exp(\boldsymbol{\sigma}_1) \approx \exp(\boldsymbol{\sigma}_2)$, applying $\varphi$ to moves while keeping copy indices unchanged. Finally:

**Corollary D.24.** For A a concrete arena, the operations $\text{mf}(-)$ and $\exp(-)$ yield a bijection between (positive isomorphism classes of) causally well-bracketed strategies on A and $A^+$.

*Proof.* For $\boldsymbol{\sigma} : A^+$, $\text{mf}(\exp(\boldsymbol{\sigma})) \approx \boldsymbol{\sigma}$ by construction. For $\boldsymbol{\sigma} : A$, $\exp(\text{mf}(\boldsymbol{\sigma})) \approx \boldsymbol{\sigma}$ is obtained from the iso of Proposition D.22 and a verification that this preserves further structure. $\square$