It is clear that if A is a gws, then the tuple ($|A|$, $\text{pol}_A$, $\downarrow\uparrow$-Plays(A)) forms a simple game in the sense of Definition 3.1.1. To obtain an AJM game, it remains to define:

**Definition 7.1.14.** Let A be a gws and s, t ∈ $\downarrow\uparrow$-Plays(A).

We say s and t are **symmetric**, written $s \cong_A t$, if s and t have the same length, and

$$ \theta_{s,t}^j = \{(s_i, t_i) \mid 1 \le i \le j\} : \{s_1, \dots, s_j\} \cong_A \{t_1, \dots, t_j\} $$

is a symmetry in $\mathcal{S}(A)$ for all $1 \le j \le n$; writing $s = s_1 \dots s_n$ and $t = t_1 \dots t_n$.

As expected, we then have the AJM “unfolding” of a game with symmetry:

**Proposition 7.1.15.** For any gws A, ($|A|$, $\text{pol}_A$, $\downarrow\uparrow$-Plays(A), $\cong_A$) is an AJM game.

*Proof.* That $\cong_A$ is an equivalence relation follows directly from the groupoid condition on event structures with symmetry. There are three more conditions to check.

For (1), consider $s_1 \dots s_n \cong_A t_1 \dots t_p$. By definition, $n = p$ and

$$ \theta_{s,t}^n = \{(s_i, t_i) \mid 1 \le i \le n\} : \{s_1, \dots, s_n\} \cong_A \{t_1, \dots, t_n\} $$

is a symmetry in $\mathcal{S}(A)$. So for all $1 \le i \le n$, $\text{pol}_A(s_i) = \text{pol}_A(\theta_{s,t}^n(s_i)) = \text{pol}_A(t_i)$.

Likewise, (2) is immediate from the definition.

For (3), consider $s = s_1 \dots s_n \cong t_1 \dots t_n = t$ with $sa \in \downarrow\uparrow$-Plays(A). By definition,

$$ \theta_{s,t}^n = \{(s_i, t_i) \mid 1 \le i \le n\} : \{s_1, \dots, s_n\} \cong_A \{t_1, \dots, t_n\} $$

is a symmetry in $\mathcal{S}(A)$. By hypothesis, $x = \{s_1, \dots, s_n\} \in \mathcal{C}(A)$ extends to $x' = x \uplus \{a\} \in \mathcal{C}(A)$. Therefore, by condition extension, writing $y = \{t_1, \dots, t_n\}$, there is some $y' \subseteq y \in \mathcal{C}(A)$ and an extension $\theta_{s,t}^n \subseteq \theta' \in \mathcal{S}(A)$ such that $\theta' : x' \cong_A y'$. But $\theta'$ is a bijection, so we must have $y' = y \uplus \{\theta'(a)\}$, which we write $b = \theta'(a)$. It is then immediate that $tb \in \downarrow\uparrow$-Plays(A) with $sa \cong_A tb$ as required. $\square$

For the expert reader, we mention that this unfolding does not respect the usual AJM game constructions as an alternating play on a parallel composition $A \parallel B$ (though we have not yet defined this in the presence of symmetry) might not be locally alternating on A and B – this is analogous to the situation in Hyland-Ong games.

**Saturated strategies.** Following the same motto as before, a concurrent prestrategy with symmetry on gws A should simply add symmetry to Definition 6.1.5, i.e. should consist in a tuple $\sigma = (|\sigma|, \le_\sigma, \#_\sigma, \mathcal{S}(\sigma), \partial_\sigma)$ where $(|\sigma|, \le_\sigma, \#_\sigma, \mathcal{S}(\sigma))$ is an ess, and

$$ \partial_\sigma : \sigma \to A $$

preserves symmetry. But while a good first step, this is not yet a working notion of (pre)strategy with symmetry: for instance, it accepts a prestrategy as in Figure 7.1, playing on $!N$, and which simply outputs the copy index used by Opponent to interrogate the natural number<fnref n="1" />. This breaks uniformity: as in AJM games (see Section 3.4), in

<footnote n="1">¹Though the $q^-$ are to be symmetric in the game, nothing forces them to be symmetric in $\sigma$.</footnote>
<figure><img src="image_85.png" /><figcaption>Figure 7.1: An invalid prestrategy with symmetry on $!N$</figcaption></figure>

order to satisfy the expected laws of a model of linear logic we must ensure that the
behaviour of strategies should not depend on Opponent's choice of copy indices.

In saturated concurrent games, uniformity is achieved by an enforcing isofibration:

**Definition 7.1.16.** Consider A a gws. A **saturated prestrategy** on A is a tuple $\sigma = (|\sigma|, \le_\sigma, \#_\sigma, \partial_\sigma)$ where $(|\sigma|, \le_\sigma, \#_\sigma)$ is an ess, $\partial_\sigma : \sigma \to A$ is a map of ess, and s.t.:

isofibration: for all $x^\sigma \in \mathscr{C}(\sigma)$, for all $\theta : y_A \cong_A \partial_\sigma x^\sigma$,
there is a unique $\varphi : y^\sigma \cong_\sigma x^\sigma$ such that $\partial_\sigma \varphi = \theta$.

This removes the behaviour of Figure 7.1 – or rather, it forces there to also be

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

a countable non-deterministic choice letting the strategy pick a random natural number
in reaction to any copy index (although the diagram only displays conflicts between
contiguous numbers, it is meant that all natural numbers are pairwise conflicting). In
effect, *isofibration* enforces uniformity by ensuring that the behaviour of a strategy is
invariant under the addition of *noise*, non-deterministically scrambling all copy indices.

**The impact of saturation.** *Isofibration* is a rather neat condition mathematically speaking, but it is computationally more debatable. To see the issue, consider

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

a typical configuration of the *copycat* strategy on $!U$, anticipating on some definitions
to come. As in AJM games, in symmetry-free concurrent games, copycat is a simple
deterministic strategy merely copying Opponent moves from one side to the other.

But, it does not satisfy *isofibration*: indeed, that would force copycat to also include
configurations featuring reindexing, as in Figure 7.2 but with all choices of copy indices.
This “saturated copycat” would be a non-deterministic strategy, as illustrated by Figure
<figure><img src="image_88.png" /><figcaption>Figure 7.2: Reindexing</figcaption></figure>

<caption>Figure 7.3: Local conflict</caption>

<caption>Figure 7.4: Non-local conflict</caption>

7.3, as a copy index can be propagated to any copy index on the other side but must be propagated only once. The emerging patterns of conflict can be quite complex: for instance, Figure 7.4 illustrates that by *local injectivity*, two threads independently coming up with the same index must conflict, even though they should be computationally independent if the strategies are to satisfy something like single-threadedness.

Saturated concurrent games ensure uniformity by adding non-deterministic noise. All the non-deterministic choices arising in saturated copycat yield symmetric moves, so it is in principle possible to express that the saturated copycat is deterministic “up to symmetry”, but it is quite technical and the model loses part of the concrete appeal of CG. We now explore an alternative: *thin concurrent games*.

### 7.1.3 Thin Concurrent Games

We wish to construct an alternative setting for strategies with symmetry, that avoids *isofibration* and instead recognizes the old – deterministic – copycat as uniform. In what sense is the deterministic copycat uniform? Well, as in AJM games: in the diagram

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

if Opponent reindexes their move to $q_0^-$, there is a *unique* matching Player reindexing of $q_0^+$ to $q_0^+$ so that we get a configuration symmetric to the original. It is this unique Player reindexing that must be captured for *thin* games. The solution is dual to saturation: in saturated games, all reindexings are allowed, giving rise to a non-deterministic choice. In contrast in thin games, only *one canonical* reindexing is allowed; conflicts are actual, computationally meaningful non-deterministic choices and not artifacts from symmetry.

But what is an “Opponent reindexing”, and a “Player reindexing”? Our first step will be to refine games with symmetry to include chosen symmetries that capture this.

**Thin Concurrent Games.** We start with the definition:

**Definition 7.1.17.** A *thin concurrent game (tcg)* is a gws $A = (|A|, \le_A, #_A, \text{pol}_A, \mathcal{S}(A))$
<figure><img src="image_90.png" /><figcaption>Figure 7.5: Positive and negative symmetries</figcaption></figure>

with isomorphism families $\mathcal{S}_+(A)$, $\mathcal{S}_-(A)$ s.t. $\mathcal{S}_+(A) \subseteq \mathcal{S}(A)$, $\mathcal{S}_-(A) \subseteq \mathcal{S}(A)$, s.t.

orthogonality: for all $\theta \in \mathcal{S}(A)$, if $\theta \in \mathcal{S}_+(A) \cap \mathcal{S}_-(A)$, then $\theta = \text{id}_x$ for $x \in \mathcal{C}(A)$,

--receptivity: if $\theta \in \mathcal{S}_-(A)$ and $\theta \subseteq \theta' \in \mathcal{S}(A)$, then $\theta' \in \mathcal{S}_-(A)$,

+-receptivity: if $\theta \in \mathcal{S}_+(A)$ and $\theta \supseteq \theta' \in \mathcal{S}(A)$, then $\theta' \in \mathcal{S}_+(A)$,

where $\theta \subseteq^p \theta'$ means that $\theta \subseteq \theta'$ adding only (pairs of) events of polarity $p$.

Symmetries in $\mathcal{S}_+(A)$ are called **positive symmetries**, and intuitively correspond to reindexing only positive events. If $\theta : x \cong_A y$ is positive, we also write $\theta : x \stackrel{+}{\cong} y$. Likewise, symmetries in $\mathcal{S}_-(A)$ are the **negative symmetries**, corresponding to reindexing only negative events, and we write $\theta : x \cong_A^- y$ if $\theta$ is negative.

**Orthogonality** means that if a symmetry reindexes *only* Player moves and *only* Option moves, it must be an identity symmetry. A negative symmetry that extends in $\mathcal{S}(A)$ with negative events must remain negative, and symmetrically.

We show in Figure 7.5 examples of positive and negative symmetries. It looks like the first should not be negative, as we rename $\checkmark_0^+$ to $\checkmark_0^+$. However, this index is only a repetition of $0$ in $\mathbf{q}_0^-$: it originates in the ! on the rhs of $\vdash$, which is attached to $\mathbf{q}_0^-$.

This split of symmetries between *positive* and *negative* symmetries is the core of thin concurrent games. This simple definition has the following pleasant consequence:

**Lemma 7.1.18.** *Consider A a tcg, and $\theta : x \cong_A y$ a symmetry.*

Then there are unique $z \in \mathcal{C}(A)$, $\theta^- : x \cong_A^- z$ and $\theta^+ : z \cong_A^+ y$ s.t. $\theta = \theta^+ \circ \theta^-$.

*Proof. Existence.* By induction on the size (i.e. cardinality) of $\theta$. If $\theta = \emptyset$, it is clear. Take $\theta : x \cong_A y$ factoring as $\theta = \theta^+ \circ \theta^- \text{ for } \theta^- : x \cong_A^- z$, $\theta^+ : z \cong_A^+ y$, and assume

$$ \theta \upharpoonright \{(a, b)\} : x \upharpoonright \{a\} \cong_A y \upharpoonright \{b\}. $$

Since symmetries preserve polarity, $\text{pol}_A(a) = \text{pol}_A(b)$ – say w.l.o.g. it is positive, the other case is symmetric. Then, by *extension* on $\mathcal{S}_-(A)$, there is some extension

$$ \theta^- \upharpoonright \{(a, c)\} : x \upharpoonright \{a\} \cong_A^- z \upharpoonright \{c\} $$

for some $c$ a negative event. But then, by *groupoid* laws for $\mathcal{S}(A)$ we have

$$ (\theta \upharpoonright \{(a, b)\}) \circ (\theta^- \upharpoonright \{(a, c)\})^{-1} : z \upharpoonright \{c\} \cong_A y \upharpoonright \{b\} $$
which extends $\theta^+$ with $\{(c, b)\}$, so by $+\text{-receptivity}$, $\theta^+ \uplus \{(c, b)\} \in \mathcal{S}_+(A)$ as required. Uniqueness. Now, assume there is an alternative factorization $\theta = \varphi^+ \circ \varphi^-$ for

$$ \varphi^- : x \cong_A z' \qquad \varphi^+ : z' \cong_A y, $$

then we have $\varphi^- \circ (\theta^-)^{-1} = (\varphi^+)^{-1} \circ \theta^+ : z \cong_A z$; but the former is negative and the latter positive, so those compositions must be the identity by orthogonality. $\square$

This is illustrated in Figure 7.5. Intuitively, any reindexing may be obtained by first reindexing Opponent moves, then reindexing Player moves, in a unique way. Obviously, by groupoid laws we can deduce the dual positive-negative factorization.

**Thin concurrent strategies.** Now, we define *thin concurrent strategies* on a tcg A.

As before, we give the definition in two stages. First, we define *prestrategies*:

**Definition 7.1.19.** A *prestrategy* on tcg A comprises an *ess* ($|\sigma|, \leq_{\sigma}, \#_{\sigma}, \mathcal{S}(\sigma)$) with

$$ \partial : \sigma \to A $$

a map of event structures with symmetry called the **display map**, subject to:

~~~-receptive: for $\theta : x \cong_{\sigma} y$, and extensions $x \vdash_{\sigma} s_1^-$, $\partial(\theta) \vdash_{\mathcal{S}(A)} (\partial(s_1^-), a_2^-)$, there is a unique $s_2^- \in \sigma$ s.t. $\theta \vdash_{\mathcal{S}(\sigma)} (s_1^-, s_2^-)$ and $\partial(s_2^-) = a_2^-$,~~~
thin: for $\theta \in \mathcal{S}(\sigma)$, if $\partial_{\sigma}\theta \in \mathcal{S}_+(A)$, then $\theta = \text{id}_x$ for some $x \in \mathcal{C}(\sigma)$.

where for $\psi \in \mathcal{S}(A)$, $\psi \vdash_{\mathcal{S}(A)} (a_1, a_2)$ iff $(a_1, a_2) \notin \psi$ and $\psi \uplus \{(a_1, a_2)\} \in \mathcal{S}(A)$.

We call this a *prestrategy*, keeping the same terminology as without symmetry – this should not cause confusion: if the tcg is merely a game (meaning, its symmetries are all identities), these additional conditions vacuously hold. We may still sometimes say *thin* (*pre*)strategy, to insist on the presence of these additional conditions.

As without symmetry, prestrategies are not yet adequate as strategies, but they do capture uniformity with respect to symmetry. In particular, $\sim$-receptivity forces $\sigma$ to internally consider as symmetric any negative moves symmetric in the game, e.g.

$$ \{\mathbf{q}_0^-\} \cong_{\mathcal{I}B} \{\mathbf{q}_1^-\} \quad \Rightarrow \quad \{\mathbf{q}_0^-\} \cong_{\sigma} \{\mathbf{q}_1^-\} $$

for $\sigma : \mathcal{I}B$ (provided $\sigma$ has unique events matching $\mathbf{q}_0^-$, $\mathbf{q}_1^-$ referred to here by the same name). Then, the extension axiom of isomorphism families on $\mathcal{S}(\sigma)$ ensure there is

$$ \begin{array}{ccc} \{\mathbf{q}_0^-\} & \cong_{\sigma} & \{\mathbf{q}_1^-\} \\ \mathcal{I} \cap_+ & \Rightarrow & \mathcal{I} \cap_+ \\ x & & x \cong_{\sigma} y \end{array} $$

then *thin* ensures that this extension is unique; another such extension $y'$ yields

$$ \theta : y \cong_{\sigma} y' $$
<figure><img src="image_91.png" /><figcaption>Figure 7.6: Two thin concurrent strategies</figcaption></figure>

obtained by going back and forth via $x$. But then, displaying to the game yields

$$ \mathrm{id}_{\{q^{-}\}} \subseteq^{+} \partial_{\sigma}\theta $$

but $\mathrm{id}_{\{q^{-}\}} \in \mathcal{S}_{+}(!B)$ by groupoid laws, so that $\partial_{\sigma}\theta \in \mathcal{S}_{+}(!B)$ by $\text{+-receptivity}$ of positive symmetries. But then by *thin*, $\theta$ must be an identity bijection. Together, those conditions $\text{+-receptivity}, \text{extension}, \text{thin}$ are a powerful way to ensure uniformity of $\sigma$.

Strategies are obtained by adding the same conditions as in Definition 6.1.6:

**Definition 7.1.20.** A prestrategy $\sigma$ on tcg A is a strategy if it satisfies:

courteous: for all $s_1 \to_{\sigma} s_2$, if $\mathrm{pol}(s_1) = +$ or $\mathrm{pol}(s_2) = -$ then $\partial_{\sigma}(s_1) \to_A \partial_{\sigma}(s_2)$,

receptive: for all $x \in \mathcal{C}(\sigma)$, for all $\partial_{\sigma}(x) \vdash_A a^{-}$, there is a unique $x \vdash_{\sigma} s^{-}$ such that $\partial_{\sigma}(s) = a$,

We write $\sigma: A$ to mean that $\sigma$ is a strategy on game A.

As an illustration, we show in Figure 7.6 two examples of concurrent strategies. On the left hand side, the strategy is displayed exhaustively – its symmetries are all reduced to identities. On the right hand side, the representation is symbolic: Opponent may ask arbitrarily many times the moves $q_{0,i}^{-}$, $q_{1,j}^{-}$ and $q_{1,k}^{-}$. Symmetries are not represented in the diagram, but would be all bijections between configurations preserving and reflecting $\to$, and only changing copy indices $i, j$ and $k$. This strategy is that for the term

$$ \lambda f^{\mathbb{B} \to \mathbb{B}}. \mathbf{if} (f \mathbf{tt}) (\mathbf{if} (f \mathbf{tt}) \perp \mathbf{tt}) (\mathbf{if} (f \mathbf{ff}) \mathbf{tt} \perp) $$

with respect to the interpretation given in Section 9.1. The left hand side strategy is the affine version of one definable with state, as shall be seen in Section 9.1.

### 7.1.4 Constructions on Thin Concurrent Games

We start with the basic tcgs from which all others will be defined. The empty tcg, written **1**, has no events. The tcgs matching *ground types* are U, B and N respectively
<figure><img src="image_92.png" /><figcaption>Figure 7.7: U</figcaption></figure>

<figure><img src="image_93.png" /><figcaption>Figure 7.8: B</figcaption></figure>

<figure><img src="image_94.png" /><figcaption>Figure 7.9: N</figcaption></figure>

displayed in Figures 7.7, 7.8 and 7.9 – in all three cases, all symmetries are identities.

**Basic constructions.** First, we introduce the simple parallel composition. In this con-
structions, tcgs $A_1$ and $A_2$ are simply put side by side with all components inherited:

**Definition 7.1.21.** Consider two tcgs $A_1$ and $A_2$.
Then, we define their simple parallel composition $A_1 \parallel A_2$ as:

$$
\begin{align*}
\text{events:} \quad & |A_1 \parallel A_2| &&= |A_1| + |A_2| \\
\text{causality:} \quad &(i, a) \le_{A_1 \parallel A_2} (j, a') &&\Leftrightarrow i = j \ \& \ a \le_{A_i} a' \\
\text{conflict:} \quad &(i, a) \#_{A_1 \parallel A_2} (j, a') &&\Leftrightarrow i = j \ \& \ a \#_{A_i} a', \\
\text{symmetry:} \quad & \theta \in \mathcal{S}(A_1 \parallel A_2) &&\Leftrightarrow \exists \theta_i \in \mathcal{S}(A_i), \theta = \theta_1 \parallel \theta_2, \\
\text{polarities:} \quad & \operatorname{pol}_{A_1 \parallel A_2}(i, a) &&= \operatorname{pol}_{A_i}(a) \\
\text{pos. symmetries:} \quad & \theta_1 \parallel \theta_2 \in \mathcal{S}_+(A_1 \parallel A_2) &&\Leftrightarrow \theta_1 \in \mathcal{S}_+(A_1) \ \& \ \theta_2 \in \mathcal{S}_+(A_2) \\
\text{neg. symmetries:} \quad & \theta_1 \parallel \theta_2 \in \mathcal{S}_-(A_1 \parallel A_2) &&\Leftrightarrow \theta_1 \in \mathcal{S}_-(A_1) \ \& \ \theta_2 \in \mathcal{S}_-(A_2).
\end{align*}
$$

where, if $\theta_i : x_i \cong_{A_i} y_i$ for $i \in \{1, 2\}$, we set $(\theta_1 \parallel \theta_2)(i, e) = (i, \theta_i(e))$.

It is direct by construction that all conditions of tcgs are satisfied. Note that only
taking the first four components into account, this definition also applies to plain ess.

Recall that Section 6.1.3 that configurations $x \in \mathcal{C}(A \parallel B)$ are exactly those of the form $x = x_A \parallel x_B = x_A + x_B$ where $x_A \in \mathcal{C}(A)$ and $x_B \in \mathcal{C}(B)$. We now have additional analogous decompositions for *symmetries*:

**Lemma 7.1.22.** Consider *A* and *B* ess. Then, there are order-isomorphisms

$$
\begin{align*}
(- \parallel -) : \quad & \mathcal{C}(A) \times \mathcal{C}(B) & \cong \mathcal{C}(A \parallel B) \\
(- \parallel -) : \quad & \mathcal{S}(A) \times \mathcal{S}(B) & \cong \mathcal{S}(A \parallel B) \\
(- \parallel -) : \quad & \mathcal{S}_-(A) \times \mathcal{S}_-(B) & \cong \mathcal{S}_-(A \parallel B) \\
(- \parallel -) : \quad & \mathcal{S}_+(A) \times \mathcal{S}_+(B) & \cong \mathcal{S}_+(A \parallel B)
\end{align*}
$$

which commute with dom and cod, in the sense that for all $\theta_A \in \mathcal{S}(A)$ and $\theta_B \in \mathcal{S}(B)$,

$$
\begin{align*}
\operatorname{dom}(\theta_A \parallel \theta_B) &= \operatorname{dom}(\theta_A) \parallel \operatorname{dom}(\theta_B), \\
\operatorname{cod}(\theta_A \parallel \theta_B) &= \operatorname{cod}(\theta_A) \parallel \operatorname{cod}(\theta_B).
\end{align*}
$$

*Proof.* Straightforward with $\theta_A \parallel \theta_B$ comprising all ((1, a), (1, a')) for $(a, a') \in \theta_A$ and
((2, b), (2, b')) for $(b, b') \in \theta_B$; and all sets ordered by componentwise inclusion. $\square$
From now on, we shall routinely decompose symmetries as above. Next, we introduce the other elementary operation on tcgs, the dual:

**Definition 7.1.23.** Consider A a tcg. Its dual $A^{\perp}$ has all components as for A except:

$$ \begin{align*} \mathrm{pol}_{A^{\perp}}(a) &= -\mathrm{pol}_{A}(a), && (a \in A) \\ \mathcal{S}_{+}(A^{\perp}) &= \mathcal{S}_{-}(A), \\ \mathcal{S}_{-}(A^{\perp}) &= \mathcal{S}_{+}(A). \end{align*} $$

It is clear by construction that if A is a tcg, then so is $A^{\perp}$. As for plain games, if A and B are tcgs then we set $A \vdash B$ to be $A^{\perp} \parallel B$. Clearly, the order-isomorphisms of Lemma 7.1.22 adapt smoothly to this construction, and let us e.g. write any symmetry on $A \vdash B$ as $\theta_A \vdash \theta_B : x_A \vdash x_B \cong_{A \vdash B} y_A \vdash y_B$ for $\theta_A : x_A \cong_A y_A$ and $\theta_B : x_B \cong_B y_B$.

**Constructions for PCF types.** In this chapter, we shall not yet detail the interpretation of programming languages. Nevertheless, we introduce here the two additional constructions required to interpret PCF types, so that as to make precise the games in the examples appearing so far. For the remaining constructions on tcgs, see Chapter 8.

The first construction is the *linear arrow* applied to tcgs with a structural constraint:

**Definition 7.1.24.** We define the following conditions on a thin concurrent game A:

negative: for all $a \in \min(A)$, we have $\mathrm{pol}_A(a) = -$,
well-opened: A is negative, and there is exactly one $a \in \min(A)$.

where $\min(A)$ is the set of minimal events in A.

As it turns out, the interpretation of PCF types only yields well-opened tcgs, whose unique minimal events is the *initial* move by Opponent, prompting computation.

To interpret the arrow type, we first define the *linear arrow*. Intuitively, in game semantics, strategies from A to B are defined to play on A and B simultaneously, with however the polarity on A reversed to reflect its contravariance. This suggests using $A \vdash B$ as arrow type – and we shall see indeed that strategies from A to B do play on this compound game. But as in the traditional games introduced in Part I, types should yield *negative* games (at least as long as we are considering call-by-name languages); while $A \vdash B$ is not negative unless A is empty. So we set:

**Definition 7.1.25.** Consider A a negative tcg, and B a well-opened tcg.

Their *linear arrow* $A \sim B$ has all components set as $A \vdash B$ except for:

$$ \text{causality: } \le_{A \sim B} = \le_{A \vdash B} \upharpoonright \{(2, b_0), (1, a) \mid a \in A\} $$

writing $\min(B) = \{b_0\}$, yielding a well-opened tcg.

This corrects the non-negativity of $A \vdash B$, by forcing the missing dependency.

Finally, as for AJM games, the last missing component of the arrow tcg is the *exponential* operation from linear logic; which finally has a non-trivial action on symmetry:
**Definition 7.1.26.** Consider A a negative tcg. Then, we define the **bang** !A with:

$$
\begin{align*}
\text{events:} \qquad |!A| &= \mathbb{N} \times |A| \\
\text{causality:} \quad (i, a_1) \preceq_A! (j, a_2) &\Leftrightarrow i = j \land a_1 \preceq_A a_2 \\
\text{conflict:} \quad (i, a_1) \#_A! (j, a_2) &\Leftrightarrow i = j \land a_1 \#_A a_2 \\
\text{symmetries:} \quad \theta \in \mathcal{S}(!A) &\Leftrightarrow \exists \pi : \mathbb{N} \simeq \mathbb{N}, \exists (\theta_n)_{n \in \mathbb{N}} \in \mathcal{S}(A)^{\mathbb{N}} \\
&\phantom{\Leftrightarrow} \forall (i, a) \in \operatorname{dom}(\theta), \theta(i, a) = (\pi(i), \theta_i(a)) \\
\text{polarities:} \qquad \operatorname{pol}_A(i, a) &= \operatorname{pol}_A(a) \\
\text{pos. symmetries:} \quad \theta \in \mathcal{S}_+(!A) &\Leftrightarrow \exists (\theta_n)_{n \in \mathbb{N}} \in \mathcal{S}_+(A)^{\mathbb{N}}, \\
&\phantom{\Leftrightarrow} \forall (i, a) \in \operatorname{dom}(\theta), \theta(i, a) = (i, \theta_i(a)) \\
\text{neg. symmetries:} \quad \theta \in \mathcal{S}_-(!A) &\Leftrightarrow \exists \pi : \mathbb{N} \simeq \mathbb{N}, \exists (\theta_n)_{n \in \mathbb{N}} \in \mathcal{S}_-(A)^{\mathbb{N}}, \\
&\phantom{\Leftrightarrow} \forall (i, a) \in \operatorname{dom}(\theta), \theta(i, a) = (\pi(i), \theta_i(a))
\end{align*}
$$

This yields a negative tcg !A.

Positive and negative symmetries for the bang were illustrated in Figure 7.5. We skip the routine verification that this defines a tcg, but it is worth observing that this depends on *negative*. If $\ominus \oplus$ is a game with two independent events with the indicated polarities, then $!(\ominus \oplus)$ is *not* a tcg: the positive symmetry $\oplus_0 \cong^+ \oplus_1$ extends with $(\oplus_1, \oplus_2)$ to a valid symmetry, so by *+$receptivity$ it should be a positive symmetry – but it is not$^2$.

Here, we keep our convention to write copy indices in grey. With only the first four clauses, this also applies to define the bang !E of a plain ess E – notice then the similarity between the definition of symmetries and Definition 3.4.3. But for a tcg, the definitions of positive and negative symmetries are asymmetric: as the bang applies to negative tcgs, the permutation $\pi$ must be understood as reindexing Opponent moves – accordingly, it is arbitrary for $\mathcal{S}_-(!A)$ but restricted to the identity for $\mathcal{S}_+(!A)$.

Altogether, this lets us interpret any PCF type as a well-opened tcg, with $[[U]] = U$, $[[B]] = B$, $[[\mathbb{N}]] = \mathbb{N}$, and $[[A \to B]] = ![[A]] \dashv [[B]]$ – we stop there for now.

## 7.2 Mediating Between Strategies

In Chapter 6, we have seen that (plain) concurrent games and strategies naturally organized themselves into a *bicategory*, where strategies are related by certain *morphisms* (Definition 6.1.7) – the corresponding *isomorphisms* provide an adequate equivalence on strategies. As in **CG**, strategies on thin concurrent games are to be compared via adequate notions of morphisms. But unlike in **CG**, there are quite a few candidates for those morphisms and generated equivalences; hence we start by exploring the options.

### 7.2.1 A Zoology of Morphisms and Equivalences

**Morphisms between strategies.** It is natural to first relate strategies with the same morphisms, importing Definition 6.1.7, simply replacing morphisms of event structures

<footnote n="2">²The bang in thin concurrent games behaves well only in situations where one deals with *polarized* games, i.e. all games are either positive or negative: no games have minimal events of mixed polarity. In the rare situations where one needs a bang on non-polarized games [Baillot et al., 1997a, Melliès, 2019b], saturated concurrent games should be used instead – in that case the reader is referred to [Castellan et al., 2014].</footnote>
with morphisms of event structures with symmetry – we call those strong morphisms.

**Definition 7.2.1.** Consider $\sigma$ and $\tau$ two (pre)strategies on a tcg A.

A strong morphism from $\sigma$ to $\tau$, is a map of ess $f : \sigma \to \tau$ satisfying:

compatibility with display maps: $\partial_{\tau} \circ f = \partial_{\sigma}$,

rigidity: for all $s \leq_{\sigma} t$, we have $fs \leq_{\tau} ft$.

The associated **strong isomorphism** between (pre)strategies, is written $f : \sigma \cong \tau$. The induced equivalence relation is a useful equivalence between strategies, understood as $\sigma$ and $\tau$ behaving in exactly the same way – including the choice of copy indices – up to renaming of internal events. With this definition, one can replay Chapter 6 based on tcgs and obtain a bicategory of tcgs, strategies, and strong morphisms.

However, strong morphisms miss the point of symmetry, which is to identify strategies that only differ in their choice of copy indices. For instance, we wish to identify

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

and

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

which are two candidates for the *dereliction* strategy on $U$. The dereliction must choose a copy index, but it should not matter at all which one is selected – being able to perform such identifications is vital in order to get the expected laws for the exponential (!).

To address that, we weaken the commutation property, using Definition 7.1.10:

**Definition 7.2.2.** Consider $\sigma, \tau : A$ two (pre)strategies.

A weak morphism from $\sigma$ to $\tau$ is a map of ess $f : \sigma \to \tau$ such that

weak commutation: $\partial_{\tau} \circ f \sim \partial_{\sigma}$,

rigidity: for all $s \leq_{\sigma} t$, we have $fs \leq_{\tau} ft$.

As announced, this authorizes reindexings, of both Player and Opponent moves. But intuitively, we wish to relate strategies by *only letting Player change their indices*. In tcgs, this might be achieved by appealing to the two *positive* and *negative* sub-symmetries. This is done by first considering a refinement of Definition 7.1.10:

**Definition 7.2.3.** Consider $E$ an ess, $A$ a tcg, and $f, g : E \to A$ maps of ess. Then $f, g$ are **positively symmetric**, written $f \sim^{+} g$, iff $\forall x \in \mathcal{C}(E), \langle f, g \rangle_x \in \mathcal{S}_+(A)$.

Intuitively, two parallel maps that target a tcg are positively symmetric if they only differ by a reindexing of Player moves. This induces a final notion of morphism:

**Definition 7.2.4.** Consider $\sigma, \tau : A$ two (pre)strategies.

A positive morphism from $\sigma$ to $\tau$, written $f : \sigma \to \tau$, is a map $f : \sigma \to \tau$ s.t.:

positive commutation: $\partial_{\tau} \circ f \sim^{+} \partial_{\sigma}$,

rigidity: for all $s \leq_{\sigma} t$, we have $fs \leq_{\tau} ft$.
Altogether we have three notions of mediating maps between (pre)strategies: strong morphisms, weak morphisms and positive morphisms. In the end, positive morphisms will turn out to be the most important; but they will all play a role in the development.

**Equivalences.** This zoology gets even more abundant when looking at the induced equivalences (ignoring strong isomorphism, as it does not support reindexing). Indeed, considering $f: \sigma \to \tau$ and $g: \tau \to \sigma$, we can require them to be inverses on the nose; or up to symmetry, i.e. $g \circ f \sim \text{id}_\sigma$ and $f \circ g \sim \text{id}_\tau$. This means we have four options:

$$
\begin{align*}
\text{weak equivalence:} \quad & \partial_{\tau} \circ f \sim \partial_{\sigma} \qquad \partial_{\sigma} \circ g \sim \partial_{\tau} \qquad g \circ f \sim \text{id}_{\sigma} \qquad f \circ g \sim \text{id}_{\tau} \\
\text{positive equivalence:} \quad & \partial_{\tau} \circ f \sim \partial_{\sigma} \qquad \partial_{\sigma} \circ g \sim \partial_{\tau} \qquad g \circ f \sim \text{id}_{\sigma} \qquad f \circ g \sim \text{id}_{\tau} \\
\text{weak isomorphism:} \quad & \partial_{\tau} \circ f \sim \partial_{\sigma} \qquad \partial_{\sigma} \circ g \sim \partial_{\tau} \qquad g \circ f = \text{id}_{\sigma} \qquad f \circ g = \text{id}_{\tau} \\
\text{positive isomorphism:} \quad & \partial_{\tau} \circ f \sim \partial_{\sigma} \qquad \partial_{\sigma} \circ g \sim \partial_{\tau} \qquad g \circ f = \text{id}_{\sigma} \qquad f \circ g = \text{id}_{\tau}.
\end{align*}
$$

Fortunately, we shall see that they all end up inducing the same equivalence relation on (pre)strategies, which we call **thin equivalence** and write $\sigma \approx \tau$. This is thanks to some important properties of positive morphisms, that we explore now.

### 7.2.2 A Study of Positive Morphisms

We aim to prove that these equivalences actually coincide. On our way there, we shall develop a few properties of thin concurrent strategies that have proved crucial.

**Strictification of positive equivalence.** Our first step here is an easy consequence of *thin* that illustrates very well what that condition achieves: the observation that a positive equivalence actually *already* is an isomorphism.

**Lemma 7.2.5.** Consider $\sigma, \tau: A$ (pre)strategies on $tcg A$.

Any positive equivalence $(f: \sigma \Rightarrow \tau, g: \tau \Rightarrow \sigma)$ is a positive isomorphism.

*Proof.* From the hypotheses, we get $g \circ f \sim \text{id}_\sigma$, meaning

$$ \langle g \circ f, \text{id}_\sigma \rangle_x = \{(g(f_s), s) \mid s \in x\} \in \mathcal{S}(\sigma) $$

for all $x \in \mathcal{C}(\sigma)$. But we also get $\partial_\sigma \circ g \circ f \sim^+ \partial_\sigma$, meaning

$$ \langle \partial_\sigma \circ g \circ f, \partial_\sigma \rangle_x = \partial_\sigma \langle g \circ f, \text{id}_\sigma \rangle_x \in \mathcal{S}_+(A) $$

for all $x \in \mathcal{C}(\sigma)$ – but so by *thin*, $\theta_x = \text{id}_x$ for all $x \in \mathcal{C}(\sigma)$. So for all $x \in \mathcal{C}(\sigma)$ and $s \in x$, $g(f(s)) = s$. But any event $s \in \sigma$ appears in at least one configuration $[s] \in \mathcal{C}(\sigma)$, so $g \circ f = \text{id}_\sigma$. Symmetrically, $f \circ g = \text{id}_\tau$. $\square$

Going back and forth around a positive equivalence yields a map $g \circ f \sim \text{id}_\sigma$. But as the symmetries witnessing this display to positive symmetries in $A$, they must be identities as $\sigma$ is thin. This property will be very important in the forthcoming development: the horizontal composition of positive isomorphisms will only yield a positive equivalence, and it is only via this lemma that it will turn out to be an isomorphism.

This strictification only holds for *positive* equivalences. To generalize it further, we shall prove that any mediating map between (pre)strategies can be made positive.
**A fibration-like property.** Let us investigate this *positivisation* process, and see how its crux is a fundamental *fibration-like* property of thin strategies.

Intuitively, the idea is simple: for $\sigma$ and $\tau$ thin (pre)strategies, a weak morphism

$$f : \sigma \to \tau$$

changes copy indices for both Player and Opponent. The idea is, for each $s^- \in \sigma$, to set $f^+(s^-)$ as the unique event symmetric to $f(s)$ with the same copy index as $s$. By uniformity, we expect that the assignment $f^+$ should be completable to Player moves. But this would be intractable to formalize directly on events, so instead we reason on configurations. That $f$ is only a weak morphism means that for $x \in \mathscr{C}(\sigma)$,

$$\langle \partial_{\sigma}, \partial_{\tau} \circ f \rangle_x : \partial_{\sigma} x \cong_A \partial_{\tau} f(x)$$

may not be in $\mathscr{S}_+(A)$. However, by Lemma 7.1.18 it factors uniquely as

$$\partial_{\sigma} x \xrightarrow{\theta^{+}} y \xrightarrow{\theta^{-}} \partial_{\tau} f(x);$$

where $y$ is understood as $\partial_{\tau} f(x)$ with negative copy indices “set back” to those of $\partial_{\sigma}(x)$. Now, we would like to set $f^+(x)$ by transporting $f(x)$ along this symmetry $\theta^-$. In the presence of the condition *isofibration* of saturated strategies (Definition 7.1.16), this would be straightforward, but our thin strategies do not satisfy *isofibration*.

Instead, we shall prove and exploit an alternative fibration-like property for thin strategies: we shall find $z \in \mathscr{C}(\tau)$ such that $\partial_{\tau}(z)$ is not equal to $y$, but positively symmetric to $y$. This is best first illustrated on an example. Consider

$$ (!U \to U) \to U $$

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

a symbolic representation of the strategy $\sigma: A$ (with $A = !(!B \to B) \to B$) obtained for instance by interpreting $\lambda f \uparrow \to \downarrow$. $f(f \perp); \perp$. So $\sigma$ admits as configuration:

$$ (!U \to U) \to U $$

<figure><img src="image_98.png" /></figure>
Now, assume we have the negative symmetry reindexing the bottom move:

$$x = \underset{\substack{\mathbf{q}_0 \\ \mathbf{q}_{0,4}}} {\mathbf{q}_0^+} \underset{\cong_A}{=} \underset{\substack{\mathbf{q}_0 \\ \mathbf{q}_{0,8}}} {\mathbf{q}_0^+} \underset{\cong_A}{=} y$$

Clearly, $\sigma$ cannot match $y$, but it can match it up to positive symmetry, with

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

positively isomorphic to $y$: Player can adapt to the change of Opponent copy indices by performing his own reindexing. This can be done systematically by exploiting uniformity of $\sigma$; or more precisely by a straightforward successive application of $\sim$-receptivity and extension. Finally, the process results in a unique configuration via thin. Altogether:

**Lemma 7.2.6.** Consider A a tcg, $\sigma : A$ a (pre)strategy, $x \in \mathscr{C}(\sigma)$, $\theta^- : \partial_\sigma x \cong_A^- y$. Then, there are unique $\varphi : x \cong_\sigma z$ and $\theta^+ : y \cong_A^+ \partial_\sigma z$ such that

$$\partial_\sigma \varphi = \vartheta^+ \circ \theta^- : \partial_\sigma x \cong_A \partial_\sigma z.$$

*Proof. Existence.* By induction on (the size of) $x$. If $x$ is empty, this is clear. Otherwise, $x = x' \uplus \{s_1\}$ with $s_1$ maximal in $x$. By restriction, $\theta^-$ restricts to $\vartheta^- : \partial_\sigma x' \cong_A^- y'$. By induction hypothesis, there are $\varphi' : x' \cong_\sigma z'$ and $\vartheta^+ : y' \cong_A^+ \partial_\sigma z'$ such that

$$\partial_\sigma \varphi' = \vartheta^+ \circ \theta^- : \partial_\sigma x' \cong_A \partial_\sigma z'$$

Furthermore, let us write $\theta^- = \vartheta^- \uplus \{(\partial_\sigma s_1, a_1)\} : \partial_\sigma x \cong_A^- y$ with $y = y' \uplus \{a_1\}$, by construction of $\vartheta^-$. Now there are two cases, depending on the polarity of $s_1$. If $s_1, a_1$ are negative, then by extension for $\mathscr{S}_+(A)$, there is an extension $\vartheta^+ \uplus \{(a_1^-, a_2^-)\} \in \mathscr{S}_+(A)$, set $\vartheta^+ = \vartheta^+ \uplus \{(a_1^-, a_2^-)\} : y \cong_A^+ \partial_\sigma z' \uplus \{a_2^-\}$. To sum up,

$$\varphi' : x' \cong_\sigma z', \quad x' \vdash_\sigma s_1^-, \quad \partial_\sigma \varphi' \vdash (\partial_\sigma(s_1^-), a_2^-),$$

so by $\sim$-receptivity there is a unique $z' \vdash_\sigma s_2^-$ such that $\varphi' \vdash_{\mathscr{S}(\sigma)} (s_1^-, s_2^-)$ and $\partial_\sigma(s_2^-) = a_2^-$. Setting $\varphi = \varphi' \uplus \{(s_1^-, s_2^-)\}$ provides the extension of $\varphi'$ as required.

Now, if $s_1$ is positive, then by extension on $\mathscr{S}(\sigma)$ there is $\varphi = \varphi' \uplus \{(s_1^+, s_2^+)\} \in \mathscr{S}(\sigma)$ with $z = z' \uplus \{s_2^+\} \in \mathscr{C}(\sigma)$. But writing $a_2^+ = \partial_\sigma s_2^+$, this means that we may set

$$\theta^+ = y' \uplus \{a_1^+\} \stackrel{(\theta^-)^{-1}}{\cong_A} \partial_\sigma x \stackrel{\partial_\sigma \varphi}{\cong_A} \partial_\sigma z' \uplus \{a_2^+\}$$
in $\mathcal{S}(A)$ by groupoid and which extends $\vartheta^+ : y' \cong_A^+ \partial_\sigma z'$ with $(a_1^+, a_2^+)$, so also $\theta^+ \in \mathcal{S}_+(A)$ by +-receptivity. By construction, we have $\partial_\sigma \varphi = \theta^+ \circ \theta^-$ as required.

**Uniqueness.** Consider alternative $\varphi : x \cong_\sigma w$ and $\vartheta^+ : y \cong_A^+ \partial_\sigma w$ such that $\partial_\sigma \varphi = \vartheta^+ \circ \vartheta^- : \partial_\sigma x \cong_A \partial_\sigma w$. Then we have the following commuting diagram

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

in $\mathcal{S}(A)$, showing that $\partial_\sigma(\varphi \circ \varphi^{-1}) \in \mathcal{S}_+(A)$, so $z = w$ and $\varphi \circ \varphi^{-1} = \mathrm{id}_z$ by thin. It follows that $\varphi = \varphi$, and then that $\vartheta^+ = \vartheta^+$, as required. $\square$

This is reminiscent of Melliès' notion of uniformity by bi-invariance [Melliès, 2003].

Via this fundamental lemma, we can mimic the consequences of the isofibration of saturated strategies, without saturation. We also mention the following generalization, which gives a similar fibration-like property without assuming that the symmetry along which the reindexing happens is negative – it is an easy consequence of the above.

**Lemma 7.2.7.** Consider A a tcg, $\sigma : A$ a (pre)strategy, $x \in \mathcal{C}(\sigma)$, $\theta : \partial_\sigma x \cong_A y$. Then, there are unique $\varphi : x \cong_\sigma z$ and $\vartheta^+ : y \cong_A^+ \partial_\sigma z$ such that

$$ \partial_\sigma \varphi = \vartheta^+ \circ \vartheta : \partial_\sigma x \cong_A \partial_\sigma z. $$

*Proof. Existence.* First, we factor $\theta = \theta^+ \circ \theta^-$ for some $\theta^- : \partial_\sigma x \cong_A^- w$ and $\theta^+ : w \cong_A^+ y$ as prescribed by Lemma 7.1.18. By Lemma 7.2.6, there are $\varphi : x \cong_\sigma z$ and $\psi^+ : w \cong_A^+ \partial_\sigma z$ such that $\psi^+ \circ \theta^- = \partial_\sigma \varphi$. But then, setting $\vartheta^+ = \psi^+ \circ (\theta^+)^{-1} : y \cong_A^+ \partial_\sigma z$, we have $\vartheta^+ \circ \vartheta = \psi^+ \circ \theta^- = \partial_\sigma \varphi$ as required.

**Uniqueness.** As in Lemma 7.2.6, for alternative $\varphi : x \cong_\sigma w$ and $\psi^+ : y \cong_A^+ \partial_\sigma w$ such that $\partial_\sigma \varphi = \psi^+ \circ \vartheta : \partial_\sigma x \cong_A \partial_\sigma w$, we have the following commuting diagram

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

in $\mathcal{S}(A)$, showing $\partial_\sigma(\varphi \circ \varphi^{-1}) \in \mathcal{S}_+(A)$, which entails uniqueness by thin. $\square$

### 7.2.3 All Equivalences Coincide

**Positivization of mediating maps.** We deduce the desired positivization property:

**Proposition 7.2.8.** Consider $\sigma, \tau : A$ (pre)strategy, $f : \sigma \to \tau$ a weak morphism. Then, there is a unique positive morphism $f^+ : \sigma \Rightarrow \tau$ such that $f \sim f^+$. $\square$
*Proof. Existence.* Consider $x \in \mathscr{C}(\boldsymbol{\sigma})$. By definition of weak morphisms we have

$$ \langle \partial_{\sigma}, \partial_{\tau} \circ f \rangle_x = \{ (\partial_{\sigma}(s), \partial_{\tau}(f(s))) \mid s \in x \} : \partial_{\sigma} x \cong_A \partial_{\tau}(f(x)), $$

and by Lemma 7.2.7, there are unique $\varphi_x : f(x) \cong_{\tau} z_x$ and $\theta_x^+ : \partial_{\sigma} x \cong_A \partial_{\tau} z_x$ s.t.

$$ \partial_{\tau} \varphi_x = \theta_x^+ \circ \langle \partial_{\sigma}, \partial_{\tau} \circ f \rangle_x^{-1}, $$

let us call all that a *solution for x*. We set $f^+(x) = z_x$. This defines an action on configurations; we aim to induce a map by Lemma 7.1.9. Clearly, $f^+$ preserves cardinality as $x \cong f(x)$ by local injectivity of $f$ and $f(x) \cong_{\tau} z$; we show that $f^+$ preserves unions.

Consider $x, y \in \mathscr{C}(\boldsymbol{\sigma})$ such that $x \cup y \in \mathscr{C}(\boldsymbol{\sigma})$. As above, we have

$$ \varphi_{x \cup y} : f(x \cup y) \cong_{\tau} z_{x \cup y}, \qquad \theta_{x \cup y}^+ : \partial_{\sigma}(x \cup y) \cong_A^+ \partial_{\tau} z_{x \cup y} $$

such that $\partial_{\tau} \varphi_{x \cup y} = \theta_{x \cup y}^+ \circ \langle \partial_{\sigma}, \partial_{\tau} \circ f \rangle_{x \cup y}^{-1}$, i.e. a solution for $x \cup y$. But as $f(x \cup y) = f(x) \cup f(y)$, $\partial_{\sigma}(x \cup y) = \partial_{\sigma}(x) \cup \partial_{\sigma}(y)$ and $\langle \partial_{\sigma}, \partial_{\tau} \circ f \rangle_{x \cup y} = \langle \partial_{\sigma}, \partial_{\tau} \circ f \rangle_x \cup \langle \partial_{\sigma}, \partial_{\tau} \circ f \rangle_y$, by the *restriction* axiom it restricts to solutions for $x$ and $y$, and must hence be their componentwise union. In particular, $f^+(x \cup y) = f^+(x) \cup f^+(y)$ as needed.

For the action on symmetries, for $\omega : x \cong_{\sigma} x'$ we set as $\tilde{f}^+(\omega)$ the composite

$$ f^+(x) \stackrel{\varphi_x^{-1}}{\cong_{\tau}} f(x) \stackrel{f(\omega)}{\cong_{\tau}} f(x') \stackrel{\varphi_{x'}}{\cong_{\tau}} f^+(x'), $$

clearly commuting with domain and codomain, so that by Lemma 7.1.9 there is a unique map of ess $f^+ : \boldsymbol{\sigma} \to \boldsymbol{\tau}$ extending the action of $f^+$ on configurations. For all $x \in \mathscr{C}(\boldsymbol{\sigma})$,

$$ \langle \partial_{\sigma}, \partial_{\tau} \circ f^{+} \rangle_{x} = \{ (\partial_{\sigma}s, \partial_{\tau}(f^{+}(s))) \mid s \in x \} = \partial_{\tau}(\varphi_{x}) \circ \langle \partial_{\sigma}, \partial_{\tau} \circ f \rangle_{x} = \theta_{x}^{+} \in \mathcal{S}_{+}(A) $$

so that $f^+ : \boldsymbol{\sigma} \Rightarrow \boldsymbol{\tau}$ is a positive morphism as required.

*Uniqueness.* Consider $f_1^+, f_2^+ : \boldsymbol{\sigma} \Rightarrow \boldsymbol{\tau}$ two symmetric positive morphisms. This means for all $x \in \mathscr{C}(\boldsymbol{\sigma})$ we have $\langle f_1^+, f_2^+ \rangle_x \in \mathcal{S}(\boldsymbol{\tau})$, together with

$$ \langle \partial_{\sigma}, \partial_{\tau} \circ f_1^+ \rangle_x : \partial_{\sigma}(x) \cong_A^+ \partial_{\tau}(f_1^+(x)), $$

$$ \langle \partial_{\sigma}, \partial_{\tau} \circ f_2^+ \rangle_x : \partial_{\sigma}(x) \cong_A^+ \partial_{\tau}(f_2^+(x)), $$

but $\langle \partial_{\sigma}, \partial_{\tau} \circ f_2^+ \rangle_x \circ \langle \partial_{\sigma}, \partial_{\tau} \circ f_1^+ \rangle_x^{-1} = \partial_{\tau}(f_1^+, f_2^+)_{x}$, so $\partial_{\tau}(f_1^+, f_2^+)_{x} \in \mathcal{S}_{+}(A)$, so that $\langle f_1^+, f_2^+ \rangle_x$ identity by *thin*. Thus $f_1^+(x) = f_2^+(x)$ and $f_1^+ = f_2^+$ by Lemma 6.1.12. $\square$

From this, we may finally deduce the following:

**Corollary 7.2.9.** For $\boldsymbol{\sigma}, \boldsymbol{\tau} : A$ (pre)strategies on $tcg A$, the following are equivalent:

(1) $\boldsymbol{\sigma}$ and $\boldsymbol{\tau}$ are weakly equivalent,

(2) $\boldsymbol{\sigma}$ and $\boldsymbol{\tau}$ are positively equivalent,

(3) $\boldsymbol{\sigma}$ and $\boldsymbol{\tau}$ are weakly isomorphic,

(4) $\boldsymbol{\sigma}$ and $\boldsymbol{\tau}$ are positively isomorphic,

and we write $\boldsymbol{\sigma} \approx \boldsymbol{\tau}$ if that is the case.
Proof. (1) ⇒ (2) by Proposition 7.2.8; (2) ⇒ (4) by Lemma 7.2.5; (4) ⇒ (3) by definition; and (3) ⇒ (1) by definition. □

These four variants induce the same equivalence relation on (pre)strategies, but the equivalences themselves (with the mediating maps) are not the same! In particular, going from weak equivalence to positive equivalence requires changing the maps.

From all this, it should be clear why we adopt positive morphisms and positive iso-morphisms as the canonical device to compare (pre)strategies, used throughout this monograph. The developments in this section will be used often, and notably to ensure that positive morphisms are preserved by forthcoming operations on strategies.

### 7.2.4 Constructing Positive Morphisms

In plain concurrent games, we have argued that working with morphisms of strategies following their concrete definition – that is, as functions acting on the sets of events – is often impractical. For this purpose we introduced Lemma 6.3.4, which shows that in order to build a morphism between strategies, one can ignore trailing Opponent events: it suffices to define the action of a morphism on +-covered configurations only. In the presence of symmetry, this need for tools to help construct morphisms is strengthened, so we need a similar lemma. As with Lemma 6.3.4, positive morphisms will act on +-covered configurations; but also on +-covered symmetries:

**Definition 7.2.10.** Consider A a tcg, and $\sigma$ a (pre)strategy on A.

A symmetry $\theta \in \mathcal{S}(\sigma)$ is **+-covered** if its domain (equivalently, its codomain) is. We write $\mathcal{S}^+(\sigma)$ for the set of **+-covered** symmetries of $\sigma$.

The reader should take particular care not to confuse the set of **+-covered** symmetries of a thin prestrategy $\sigma: A$, written $\mathcal{S}^+(\sigma)$, with the set of positive symmetries of a tcg $A$, written $\mathcal{S}_+(A)$. The former asks that maximal events are positive, relying on the fact that symmetries are order-isomorphisms and so preserve maximal events; while the latter is part of the data of a tcg, intuitively capturing those symmetries only reindexing Player moves. Note that only a tcg has positive and negative symmetries, not a (pre)strategy.

With this notion, we prove the following generalization of Lemma 6.3.4:

**Lemma 7.2.11.** Consider $\sigma, \tau: A$ two strategies. Assume there is a function $f: \mathcal{C}^+(\sigma) \to \mathcal{C}^+(\tau)$ preserving unions, and monotone functions

$$ \tilde{f}: \mathcal{S}^+(\sigma) \to \mathcal{S}^+(\tau), \quad \tilde{f}: \mathcal{C}^+(\sigma) \to \mathcal{S}^+(A), $$

compatible with dom and cod as in Lemma 7.1.9, such that for all $x \in \mathcal{C}^+(\sigma)$,

$$ \tilde{f}(x) : \partial_{\sigma} x \cong_{A}^{+} \partial_{\tau} f(x), $$

and such that for all $\theta: x \cong_{\sigma} y \in \mathcal{S}^+(\sigma)$, we have $\partial_{\tau}(\tilde{f}(\theta)) = \tilde{f}(y) \circ (\partial_{\sigma} \theta) \circ \tilde{f}(x)^{-1}$.

Then, there is a unique positive $\hat{f}: \sigma \Rightarrow \tau$ such that for all $x \in \mathcal{C}^+(\sigma)$, $\hat{f}x = fx$.
*Proof. Existence.* We first extend $f$ to all configurations, via the following elaboration of the reasoning in Lemma 6.3.4. Consider $x \in \mathscr{C}(\boldsymbol{\sigma})$. There is a unique $y \in \mathscr{C}^{+}(\boldsymbol{\sigma})$ such that $y \subseteq^{-} x$, obtained by removing trailing events. Now, by hypothesis we have

$$ \tilde{f}(y) : \partial_{\sigma} y \cong_{A}^{+} \partial_{\tau} f(y), $$

and $\partial_{\sigma} y \subseteq^{-} \partial_{\sigma} x$, thus by extension, there is $\tilde{f}(y) \subseteq^{-} \theta : \partial_{\sigma} x \cong_{A}^{+} z$; it is actually unique because if we also have $\tilde{f}(y) \subseteq^{-} \theta' : \partial_{\sigma} x \cong_{A}^{+} z'$, then $\theta' \circ \theta^{-1} : z \cong_{A}^{+} z'$ is a negative extension of $\text{id}_{\partial_{\sigma} x}$ hence is also a negative symmetry, and thus must be an identity by orthogonality. Now that $\theta : \partial_{\sigma} x \cong_{A}^{+} z$ is uniquely determined, we note that $\partial_{\tau} f(y) \subseteq^{-} z$ inducing a unique $f(y) \subseteq^{-} u \in \mathscr{C}(\tau)$ so that $\partial_{\tau} u = z$ by $\text{--discrete opfibration}$; we set $f(x) = u$ and $\tilde{f}(x) = \theta$. From the uniqueness properties of $z, \theta, u$ it is straightforward that $f$, extended in this way, preserves unions.

We must similarly extend $\tilde{f}$ to all symmetries. If $\theta : x \cong_{\sigma} x'$, then as above there is a unique $\varphi \subseteq^{-} \theta$ such that $\varphi \in \mathscr{S}^{+}(\boldsymbol{\sigma})$, write $\varphi : y \cong_{\sigma} y'$, obtained by removing trailing (pairs of) negative moves. We have then $\tilde{f}(\varphi) : f(y) \cong_{\tau} f(y')$. Then

$$ \psi = \partial_{\tau} f(x) \cong_{A}^{+} \partial_{\sigma} x \cong_{A}^{+} \partial_{\sigma} x' \cong_{A}^{+} \partial_{\tau} f(x') $$

is a negative extension of $\tilde{f}(y') \circ (\partial_{\sigma} \varphi) \circ \tilde{f}(y)^{-1}$, which by hypothesis is $\partial_{\tau}(\tilde{f}(\theta))$. Thus by $\sim$-receptivity of $\tau$, there is a unique $\tilde{f}(\theta) \subseteq^{-} \theta'$ s.t. $\partial_{\tau} \theta' = \psi$, and we set $\tilde{f}(\theta) = \theta'$.

Clearly, this assignment is compatible with the extension of $f$ with respect to domain and codomain, and thus by Lemma 7.1.9, there is a unique map of ess $\hat{f} : \boldsymbol{\sigma} \to \tau$ extending $f$. We must show that $\partial_{\sigma} \sim^{+} \partial_{\tau} \circ f$, which amounts to showing

$$ \tilde{f}(x) = \langle \partial_{\sigma}, \partial_{\tau} \circ f \rangle_{x} \qquad (7.2) $$

for all $x \in \mathscr{C}(\boldsymbol{\sigma})$, which we prove by induction on $x$. If $x$ is empty, there is nothing to prove. If $x$ is not $\text{+-covered}$, then there is unique $y \in \mathscr{C}^{+}(\boldsymbol{\sigma})$ such that $y \subseteq^{-} x$. By induction hypothesis, $\tilde{f}(y) = \langle \partial_{\sigma}, \partial_{\tau} \circ f \rangle_{y}$, and there is a covering chain

$$ y \subset \dots \subset \tilde{s}_{1}^{-} \subset \dots \subset \tilde{s}_{n}^{-} \subset x $$

by induction on which it is immediate that (7.2) holds for $x$ as well by definition of the extension of $\tilde{f}$. Now if $x$ is $\text{+-covered}$, it has a maximal positive event $s$. Setting $y = x \setminus \{s\}$, by induction hypothesis (7.2) holds for $y \in \mathscr{C}(\boldsymbol{\sigma})$, but then it holds for $x$ by monotonicity of $\tilde{f}$. Thus we have $\partial_{\sigma} \sim^{+} \partial_{\tau} \circ \hat{f}$ as required.

**Rigidity.** Similar to the reasoning in Lemma 6.3.4.

**Uniqueness.** Consider $g$ another such extension. We first show by induction on $x$ that for all $x \in \mathscr{C}(\boldsymbol{\sigma})$, we have $f(x) = g(x)$ and $\tilde{f}(x) = \langle \partial_{\sigma}, \partial_{\tau} \circ g \rangle_{x}$. If $x$ is empty there is nothing to prove. If $x$ is not $\text{+-covered}$, there is $y \in \mathscr{C}^{+}(\boldsymbol{\sigma})$ such that $y \subseteq^{-} x$. By induction hypothesis, we have $f(y) = g(y)$ and $\tilde{f}(y) = \langle \partial_{\sigma}, \partial_{\tau} \circ g \rangle_{y}$. Now we have

$$ \langle \partial_{\sigma}, \partial_{\tau} \circ g \rangle_{y} \subseteq^{-} \langle \partial_{\sigma}, \partial_{\tau} \circ g \rangle_{x} \in \mathscr{S}^{+}(A), $$

forcing $g(x)$ to coincide with the construction of $f(x)$ above; that $\tilde{f}(x) = \langle \partial_{\sigma}, \partial_{\tau} \circ g \rangle_{x}$ is immediate from the construction of $\tilde{f}(x)$ following a covering chain of $y \subseteq^{-} x$. Finally, if $x$ is $\text{+-covered}$, the result follows by $f(x) = g(x)$ and monotonicity of $\tilde{f}$. $\square$
As before, when using this lemma we will not always explicitly spell out the action on +-covered symmetries when it is transparent from that on +-covered configurations, similarly we will detail $\tilde{f}$ only when it is non-trivial. Though unlike for Lemma 7.1.9, it remains unclear if $\tilde{f}$ and $\tilde{f}$ are necessarily unique here.

We mention in passing two direct consequences of the above. First, we have:

**Corollary 7.2.12.** Consider $f, g : \sigma \Rightarrow \tau$ two positive morphisms between strategies. If for all $x^\sigma \in \mathcal{C}^+(\sigma)$, we have $f(x^\sigma) = g(x^\sigma)$, then $f = g$.

*Proof.* By uniqueness in Lemma 7.2.11. □

And then, the following is sometimes useful to construct strong isomorphisms:

**Corollary 7.2.13.** Consider $\sigma, \tau : A$ strategies on tcg A. Assume there are

$$f : \mathcal{C}^+(\sigma) \simeq \mathcal{C}^+(\tau) \qquad \tilde{f} : \mathcal{S}^+(\sigma) \simeq \mathcal{S}^+(\tau)$$

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

Then, there is a strong isomorphism $\tilde{f} : \sigma \cong \tau$ s.t. for all $x \in \mathcal{C}^+(\sigma)$, $\tilde{f}(x) = f(x)$.

## 7.3 Composition and Copycat

Now that we have introduced thin strategies and the required tools to mediate between them, we are in position to compose them and introduce copycat. For both, the idea is to keep the structure developed in Chapter 6, only enriching it with symmetry.

For composition, the symmetries will exactly be pairs of causally compatible symmetries, as summarized by the following extension of Proposition 6.2.1:

**Proposition 7.3.1.** Consider A, B, C tcgs, and $\sigma : A \vdash B$ and $\tau : B \vdash C$ strategies.

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

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

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

order-isomorphisms commuting with dom, cod, and such that we have

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

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

As without symmetry, this proposition packages almost all the “working concurrent game semanticist” needs to know about the composition of thin strategies. We shall gradually work our way towards its proof, and the concrete construction of composition.

In the statement, we have used for the display of symmetries the same notation as for the display of configurations in Chapter 6, that is to say, we typically write $\theta^\sigma \in \mathcal{S}(\sigma)$ for symmetries in $\sigma$ for $\sigma$ a (pre)strategy, and we write its display as $\partial_\sigma \theta^\sigma = \theta_A^\sigma \vdash \theta_B^\sigma$. We have also used the notion of causal compatibility for symmetries:
**Definition 7.3.2.** Take $\sigma : A \vdash C$, $\tau : B \vdash C$ prestrategies, $\theta^\sigma \in \mathcal{S}(\sigma)$, $\theta^\tau \in \mathcal{S}(\tau)$.

We say that $\theta^\sigma$ and $\theta^\tau$ are matching if $\theta_B^\sigma = \theta_B^\tau$; and causally compatible if the domains $\text{dom}(\theta^\sigma)$, $\text{dom}(\theta^\tau)$ are (equivalently, if the codomains $\text{cod}(\theta^\sigma)$, $\text{cod}(\theta^\tau)$ are).

### 7.3.1 Interactions with Symmetry

We now set to construct concretely the composition of thin (pre)strategies. The first step is simply to enrich Definition 6.2.3 with symmetry, for A, B and C tcgs.

**Definition 7.3.3.** An interaction on A, B, C is an ess $\mu = (|\mu|, \leq_\mu, \#_\mu, \mathcal{S}(\mu))$ with

$$ \partial : |\mu| \to |A \parallel B \parallel C| $$

a display map subject to the following conditions:

rule-abiding: for all $x \in \mathcal{C}(\mu)$, $\partial(x) \in \mathcal{C}(A \parallel B \parallel C)$,

locally injective: for all $s_1, s_2 \in x \in \mathcal{C}(\mu)$, if $\partial(s_1) = \partial(s_2)$ then $s_1 = s_2$,

$\sim$-preserving: for all $\theta \in \mathcal{S}(\mu)$, $\partial(\theta) \in \mathcal{S}(A \parallel B \parallel C)$,

thin: for all $\theta \in \mathcal{S}(\mu)$, writing $\partial(\theta) \in \theta_A \parallel \theta_B \parallel \theta_C$, if $\theta_A \in \mathcal{S}_-(A)$ and $\theta_C \in \mathcal{S}_+(C)$, then $\theta = \text{id}_x$ for some $x \in \mathcal{C}(\mu)$.

i.e. $\partial : \mu \to A \parallel B \parallel C$ is a map of event structures with symmetry; and is thin.

Fix for now prestrategies $\sigma : A \vdash B$ and $\tau : B \vdash C$. Following the developments in Chapter 6, we have already constructed an interaction $\tau \otimes \sigma$ in the sense of Definition 6.2.3, that we need to enrich with symmetry. This relies on the following observation, letting us “zip” causally compatible symmetries into a bijection in $\tau \otimes \sigma$:

**Lemma 7.3.4.** Consider $\theta^\sigma : x^\sigma \cong_\sigma y^\sigma$ and $\theta^\tau : x^\tau \cong_\tau y^\tau$ causally compatible.

Then, there exists a unique bijection $\theta^\tau \otimes \theta^\sigma : x^\tau \otimes x^\sigma \cong y^\tau \otimes y^\sigma$ such that

$$ \begin{array}{ccc} x^\sigma \parallel x_C^\tau & \xleftarrow{\Pi_\sigma} & x^\tau \otimes x^\sigma \xrightarrow{\Pi_\tau} x_A^\sigma \parallel x^\tau \\ \theta^\sigma \parallel \theta_C^\tau & \downarrow & \theta^\tau \otimes \theta^\sigma \\ y^\sigma \parallel y_C^\tau & \xleftarrow{\Pi_\sigma} & y^\tau \otimes y^\sigma \xrightarrow{\Pi_\tau} y_A^\sigma \parallel y^\tau \end{array} \qquad (7.3) $$

commutes in the category of finite sets and bijections.

*Proof. Existence.* As $\theta^\sigma$ and $\theta^\tau$ are matching, the outer diagram commutes by Lemma 6.2.12. This lets us define the bijection $\theta^\tau \otimes \theta^\sigma : x^\tau \otimes x^\sigma \cong y^\tau \otimes y^\sigma$ as either path along the diagram above. The condition holds by construction.

*Uniqueness.* Clearly, $\theta^\tau \otimes \theta^\sigma$ is uniquely determined by the diagram. $\square$

This invites us to set $\mathcal{S}(\tau \otimes \sigma)$ as including all $\theta^\tau \otimes \theta^\sigma$ for $\theta^\sigma \in \mathcal{S}(\sigma)$ and $\theta^\tau \in \mathcal{S}(\tau)$ causally compatible. It remains to prove that this satisfies the required conditions.
**Lemma 7.3.5.** *Setting $\mathcal{S}(\tau \oplus \sigma)$ to comprise all $\theta^\tau \oplus \theta^\sigma$ for $\theta^\sigma \in \mathcal{S}(\sigma)$ and $\theta^\tau \in \mathcal{S}(\tau)$ causally compatible defines an ess (|$\tau$ $\oplus$ $\sigma$|, $\leq_{\tau \oplus \sigma}$, $\#_{\tau \oplus \sigma}$, $\mathcal{S}(\tau \oplus \sigma)$), yielding*

$$ \begin{tikzcd}[column sep=2.8em, row sep=2.8em]
    \sigma \arrow[r, "\tau \oplus \sigma"] & C \arrow[r, "\sigma"] & A \arrow[r, "\tau"] & \sigma \arrow[l, "\tau \oplus \sigma"]
    \arrow[d, "\partial_\sigma "] \\
    \multicolumn{4}{c}{\text{in the category of ess and their maps.}}
  \end{tikzcd} \quad (7.4) $$

a pullback in the category of ess and their maps.

*Proof.* We verify the axioms of isomorphism families. First, groupoid axioms follow from the definition. For restriction, by definition of $\theta^\sigma$ and $\theta^\tau$ matching we have

$$ \begin{tikzcd}[column sep=2.8em, row sep=2.8em]
    x^\sigma \arrow[r, "x^\tau"] \arrow[d, "\mathrm{dom}", "\varphi[x^\sigma, x^\tau]"'] & C \arrow[r, "\mathrm{cod}", "x_A^\sigma"] & A \arrow[r, "x^\tau"] & \sigma \arrow[l, "\mathrm{dom}", "\varphi[x^\sigma, x^\tau]"'] \\
    \vartheta^\sigma \arrow[r, "\vartheta^\tau"] \arrow[d, "\mathrm{dom}", "\varphi[y^\sigma, y^\tau]"'] & C \arrow[r, "\mathrm{cod}", "y_A^\sigma"] & A \arrow[r, "y^\tau"] & \sigma \arrow[l, "\mathrm{dom}", "\varphi[y^\sigma, y^\tau]"']
  \end{tikzcd} \quad (7.5) $$

commuting; assume now that $u^\sigma \oplus u^\tau \subseteq x^\tau \oplus x^\sigma$; i.e. we have $u^\sigma \subseteq x^\sigma$ and $u^\tau \subseteq x^\tau$ causally compatible. But then by restriction for $\sigma$ and $\tau$, we have

$$ \begin{tikzcd}[column sep=2.8em, row sep=2.8em]
    u^\sigma \arrow[r, "u^\tau"] \arrow[d, "\mathrm{dom}", "\varphi[u^\sigma, u^\tau]"'] & C \arrow[r, "\mathrm{cod}", "u_A^\sigma"] & A \arrow[r, "u^\tau"] & \sigma \arrow[l, "\mathrm{dom}", "\varphi[u^\sigma, u^\tau]"'] \\
    \vartheta^\sigma \arrow[r, "\vartheta^\tau"] \arrow[d, "\mathrm{dom}", "\varphi[v^\sigma, v^\tau]"'] & C \arrow[r, "\mathrm{cod}", "v_A^\sigma"] & A \arrow[r, "v^\tau"] & \sigma \arrow[l, "\mathrm{dom}", "\varphi[v^\sigma, v^\tau]"']
  \end{tikzcd} $$

with $\vartheta^\sigma \subseteq \theta^\sigma$ and $\vartheta^\tau \subseteq \theta^\tau$; in particular the diagram still commutes. Restriction follows by definition and Lemma 6.2.12.

For extension, consider again the diagram (7.5). It suffices to deal with one-step extensions, the general case follows by induction. Furthermore, we focus on an extension

$$ \varphi[x^\sigma, x^\tau] \xrightarrow{((1,s),(2,t))} \varphi[u^\sigma, u^\tau], $$

with $x^\sigma \subsetneq u^\sigma$ and $x^\tau \subsetneq u^\tau$, i.e. a synchronized event between $\sigma$ and $\tau$ – where $\partial_\sigma s$ and $\partial_\tau t$ occur in $B$ – the other cases are simpler. Moreover, we assume $\mathrm{pol}_\sigma(s) = +$, the other case is symmetric. Now, by extension for $\sigma$, there is $\theta^\sigma \subsetneq \vartheta^\sigma : u^\sigma \cong_\sigma v^\tau$. By ~-preserving for $\sigma$, $\partial_\sigma \vartheta^\sigma = \theta_A^\sigma \parallel \vartheta_B^\sigma$ with $\theta_B^\sigma \subsetneq \vartheta_B^\sigma : u_B^\sigma \cong_B v_B^\sigma$. But then, ~-receptivity of $\tau$ exactly gives us a matching extension $\theta^\tau \subseteq \vartheta^\tau$ such that

$$ \begin{tikzcd}[column sep=2.8em, row sep=2.8em]
    u^\sigma \arrow[r, "x_C^\tau"] \arrow[d, "\mathrm{dom}", "\varphi[u^\sigma, u^\tau]"'] & C \arrow[r, "\mathrm{cod}", "x_A^\sigma"] & A \arrow[r, "u^\tau"] & \sigma \arrow[l, "\mathrm{dom}", "\varphi[u^\sigma, u^\tau]"'] \\
    \vartheta^\sigma \arrow[r, "\vartheta_C^\tau"] \arrow[d, "\mathrm{dom}", "\varphi[v^\sigma, v^\tau]"'] & C \arrow[r, "\mathrm{cod}", "v_A^\sigma"] & A \arrow[r, "v^\tau"] & \sigma \arrow[l, "\mathrm{dom}", "\varphi[v^\sigma, v^\tau]"']
  \end{tikzcd} $$
commutes, which provides us with the required extension by Lemma 6.2.12.

It is clear by definition (see the diagram of Lemma 7.3.4) that $\Pi_{\sigma}$ and $\Pi_{\tau}$ preserve symmetry. We skip the universal property, straightforward via Lemma 7.1.9. $\square$

At last, this provides us with the ingredients for the interaction.

**Proposition 7.3.6.** *There is an interaction $\tau \oplus \sigma$, unique up to iso, s.t. there are*

$$(- \otimes -) : \{ (x^{\tau}, x^{\sigma}) \in \mathscr{C}(\tau) \times \mathscr{C}(\sigma) \mid x^{\sigma}, x^{\tau} \text{ causally compatible} \} \approx \mathscr{C}(\tau \oplus \sigma)$$

$$(- \otimes -) : \{ (\theta^{\tau}, \theta^{\sigma}) \in \mathscr{S}(\tau) \times \mathscr{S}(\sigma) \mid \theta^{\sigma}, \theta^{\tau} \text{ causally compatible} \} \approx \mathscr{S}(\tau \oplus \sigma)$$

order-isomorphisms commuting with dom and cod, and satisfying

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

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

*Proof. Existence.* The ess $\tau \oplus \sigma$ is defined in Lemma 7.3.5, with display map $\partial_{\tau \oplus \sigma} : \tau \oplus \sigma \to A \parallel B \parallel C$ defined as either way around (7.4). The order-iso for configurations comes from Proposition 6.2.8, while for symmetries it is follows from Lemma 7.3.4 (it is immediate from (7.3) that $\theta^{\sigma}$ and $\theta^{\tau}$ can be recovered from $\theta^{\tau} \oplus \theta^{\sigma}$).

For *thin*, take $\theta^{\tau} \oplus \theta^{\sigma} \in \mathscr{S}(\tau \oplus \sigma)$ s.t. $\theta_{A}^{\sigma} \in \mathscr{S}_{-}(A)$ and $\theta_{C}^{\tau} \in \mathscr{S}_{+}(A)$. Consider:

$$\begin{array}{ccc}
x^{\sigma} \parallel x_{C}^{\tau} & \xleftarrow{\text{dom}} & \varphi[x^{\sigma}, x^{\tau}] \xrightarrow{\text{cod}} x_{A}^{\sigma} \parallel x^{\tau} \\
\theta^{\sigma} \parallel \theta_{C}^{\tau} & \downarrow & \\
y^{\sigma} \parallel y_{C}^{\tau} & \xleftarrow{\text{dom}} & \varphi[y^{\sigma}, y^{\tau}] \xrightarrow{\text{cod}} y_{A}^{\sigma} \parallel y^{\tau}
\end{array}$$

and seeking a contradiction, assume the induced $\psi : \varphi[x^{\sigma}, x^{\tau}] \simeq \varphi[y^{\sigma}, y^{\tau}]$ is not an identity. By *restriction*, we may assume *w.l.o.g.* that there is exactly one non-identity $((m, m'), (n, n')) \in \psi$. Several cases arise. If $m = (2, c)$, $n = (2, t)$ with $m' = (2, c')$ and $n' = (2, t')$, then $\partial_{\tau} \theta^{\tau} = \theta_{B} \parallel \theta_{C}^{\tau}$ with $\theta_{B} \in \mathscr{S}_{-}(B)$ as an identity symmetry and $\theta_{C}^{\tau} \in \mathscr{S}_{+}(C)$ by hypothesis, so $\theta^{\tau}$ is an identity as $\tau$ is *thin*, contradiction. The case $m = (1, s)$, $n = (1, a)$, $m' = (1, s')$ and $n' = (1, a')$ is symmetric. The last case has $m = (1, s)$, $n = (2, t)$, $m' = (1, s')$ and $n' = (2, t')$. If $\text{pol}_{\sigma}(s) = \text{pol}_{\sigma}(s') = +$, then

$$\partial_{\sigma} \theta^{\sigma} = \theta_{A}^{\sigma} \parallel \theta_{B}^{\sigma} = \text{id}_{x_{A}^{\sigma}} \parallel (\text{id}_{x_{B}^{\sigma}} \uplus \{(b, b')\})$$

with $\partial_{\sigma}(s) = (2, b)$ and $\partial_{\sigma}(s') = (2, b')$. Then, $\text{pol}_{B}(b) = \text{pol}_{B}(b') = +$, so $\theta_{B}^{\sigma} \in \mathscr{S}_{+}(B)$ by $+-\text{receptivity}$. Of course, $\theta_{A}^{\sigma} \in \mathscr{S}_{-}(A)$ by hypothesis, so $\theta^{\sigma}$ is an identity by *thin*, contradiction. The final case, with $\text{pol}_{\tau}(t) = \text{pol}_{\tau}(t') = +$, is symmetric.

*Uniqueness.* Immediate from the order-isos, by Lemma 7.1.9. $\square$

Here, an isomorphism of interactions simply means an iso of ess commuting with the display maps on the nose. We may now give the concrete definition of composition.
### 7.3.2 Composition with Symmetry

To defined composition, we simply add symmetry to Definition 6.2.16:

**Definition 7.3.7.** The composition of $\sigma : A \vdash B$ and $\tau : B \vdash C$ comprises the components of Definition 6.2.16, enriched with a set of symmetries, defined as:

$$ \theta : x \cong_{\tau \odot \sigma} y \Leftrightarrow \exists \theta' \subseteq \theta' : x' \cong_{\tau \otimes \sigma} y'. $$

We have yet to show that composition yields a (pre)strategy; and first of all, while the axioms of event structures are immediate, it is not obvious at all that $\mathcal{S}(\tau \odot \sigma)$ is an isomorphism family: we need a tighter characterization of symmetries:

**Lemma 7.3.8.** Consider $x, y \in \mathcal{C}(\tau \odot \sigma)$, and a symmetry $\theta : x \cong_{\tau \odot \sigma} y$.

There exists a unique $[\theta]_{\tau \otimes \sigma}$, the interaction witness of $\theta$, s.t. $\theta \subseteq [\theta]_{\tau \otimes \sigma}$, and:

$$ [\theta]_{\tau \otimes \sigma} : [x]_{\tau \otimes \sigma} \cong_{\tau \otimes \sigma} [y]_{\tau \otimes \sigma}. $$

*Proof. Existence.* By definition, there is $\theta \subseteq \theta' : x' \cong_{\tau \otimes \sigma} y'$. But $[x]_{\tau \otimes \sigma} \subseteq x'$, so by restriction we have $\theta'' : [x]_{\tau \otimes \sigma} \cong_{\tau \otimes \sigma} y''$ – note $\theta''$ still contains $\theta$ as $\mathrm{dom}(\theta) = x \subseteq [x]_{\tau \otimes \sigma}$. Now, by Lemma 7.1.6 $\theta''$ is an order-isomorphism. From this, it is easy to show that maximal events of $y''$ are in $y$, i.e. $y'' = [y]_{\tau \otimes \sigma}$.

*Uniqueness.* Assume $\vartheta, \vartheta' : [x]_{\tau \otimes \sigma} \cong_{\tau \otimes \sigma} [y]_{\tau \otimes \sigma}$ such that $\vartheta \subseteq \vartheta, \vartheta'$. Then

$$ \partial_{\tau \otimes \sigma} \vartheta = \theta_A \parallel \vartheta_B \parallel \theta_C $$

$$ \partial_{\tau \otimes \sigma} \vartheta' = \theta_A \parallel \vartheta'_B \parallel \theta_C $$

only differ on $B$ as $\theta \subseteq \vartheta, \vartheta'$ only adding (pairs of) synchronized events. But then,

$$ \partial_{\tau \otimes \sigma}(\vartheta' \circ \vartheta^{-1}) = \mathrm{id}_{[\vartheta]_{\tau \otimes \sigma}} \parallel (\vartheta'_B \circ \vartheta^{-1}_B) \parallel \mathrm{id}_{[x]_{\tau \otimes \sigma}} $$

so $\vartheta' \circ \vartheta^{-1}$ is an identity since $\tau \otimes \sigma$ is thin; therefore $\vartheta = \vartheta'$.

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

We can now conclude that the composition yields an event structure with symmetry:

**Proposition 7.3.9.** We have $\tau \odot \sigma = (|\tau \odot \sigma|, \leq_{\tau \odot \sigma}, \#_{\tau \odot \sigma}, \mathcal{S}(\tau \odot \sigma))$, an ess.

Moreover, we have order-isomorphisms commuting with dom and cod:

$$ (- \odot -) : \{(x^\tau, x^\sigma) \in \mathcal{C}(\tau) \times \mathcal{C}(\sigma) \mid x^\sigma, x^\tau \text{ minimal caus. comp.}\} \cong \mathcal{C}(\tau \odot \sigma) $$

$$ (- \odot -) : \{(\theta^\tau, \theta^\sigma) \in \mathcal{S}(\tau) \times \mathcal{S}(\sigma) \mid \theta^\sigma, \theta^\tau \text{ minimal caus. comp.}\} \cong \mathcal{S}(\tau \odot \sigma), $$

where $\theta^\sigma, \theta^\tau$ minimal means $\mathrm{dom}(\theta^\sigma), \mathrm{dom}(\theta^\tau)$ (or $\mathrm{cod}(\theta^\sigma), \mathrm{cod}(\theta^\tau)$) minimal.

*Proof.* The definition of the event structure and order-isomorphism on configurations are developed in Proposition 6.2.18, which we only need to extend with symmetries. The conditions for isomorphism families follow directly from those for $\mathcal{S}(\tau \otimes \sigma)$ in combination with Lemma 7.3.8. For the order-isomorphism on symmetries, first we note that the isomorphism of Proposition 7.3.6 refine to an order-isomorphism:

$$ (- \otimes -) : \{(\theta^\tau, \theta^\sigma) \in \mathcal{S}(\tau) \times \mathcal{S}(\sigma) \mid \theta^\sigma, \theta^\tau \text{ min. caus. comp.}\} \cong \mathcal{S}^\nu(\tau \otimes \sigma) $$
where $\mathcal{S}^v(\tau \oplus \sigma)$ refers to symmetries whose maximal (pairs of) events are visible. This is clear by Lemma 6.2.12. Next, we have an order-isomorphism formed with:

$$ \begin{array}{rcl} \mathcal{S}^v(\tau \oplus \sigma) & \rightarrow & \mathcal{S}(\tau \odot \sigma) \\ \theta & \mapsto & \theta \cap V^2 \end{array} \qquad \begin{array}{rcl} \mathcal{S}(\tau \odot \sigma) & \rightarrow & \mathcal{S}^v(\tau \oplus \sigma) \\ \theta & \mapsto & [\theta]_{\tau \oplus \sigma} \end{array} $$

where $V$ is the set of visible events – it is easy that this defines an order-isomorphism. □

This defines the composition of $\sigma$ and $\tau$ as an ess, to which we may adjoin a display map specified via Lemma 7.1.9 by completing $\partial_{\tau \odot \sigma}$ with $\partial_{\tau \odot \sigma}(\theta^{\tau} \odot \theta^{\sigma}) = \theta_A^{\sigma} \vdash \theta_C^{\tau}$.

**Preservation of prestrategies.** We still have not accounted for a few of the additional conditions on (pre)strategies. Before wrapping up the composition of strategies, it is sometimes technically convenient to be able to compose prestrategies. This holds only modulo an additional condition on $\sigma$ and $\tau$, called *span-courteous*:

**Definition 7.3.10.** Consider $\sigma : A \vdash B$. We define the following condition:

span-courteous: for all $s_1 \to_A s_2$, if $\mathrm{pol}_\sigma(s_1) = +$ or $\mathrm{pol}_\sigma(s_2) = -$, then writing $\partial_\sigma(s_i) = (k_i, c_i)$, we have $k_1 = k_2$.

This tames failures of courtesy, expressing that they cannot span across the components $A, B$ – without it, composition of prestrategies may fail ~-receptivity.

Now, we have the ingredients to prove the following defining property:

**Proposition 7.3.11.** Take $\sigma : A \vdash B$ and $\tau : B \vdash C$ span-courteous prestrategies. Then, there is a prestrategy $\tau \odot \sigma$, unique up to strong iso, s.t. there are order-isos:

$$ (- \odot -) : \{(x^{\tau}, x^{\sigma}) \in \mathcal{C}(\tau) \times \mathcal{C}(\sigma) \mid x^{\sigma}, x^{\tau} \text{ min. caus. comp.}\} \simeq \mathcal{C}(\tau \odot \sigma) $$

$$ (- \odot -) : \{(\theta^{\tau}, \theta^{\sigma}) \in \mathcal{S}(\tau) \times \mathcal{S}(\sigma) \mid \theta^{\sigma}, \theta^{\tau} \text{ min. caus. comp.}\} \simeq \mathcal{S}(\tau \odot \sigma) $$

commuting with dom and cod; such that for $\theta^{\sigma} \in \mathcal{S}(\sigma)$, $\theta^{\tau} \in \mathcal{S}(\tau)$ minimal causally compatible, $\partial_{\tau \odot \sigma}(\theta^{\tau} \odot \theta^{\sigma}) = \theta_A^{\sigma} \parallel \theta_C^{\tau}$. Moreover, $\tau \odot \sigma$ is span-courteous.

**Proof. Existence.** The ess $\tau \odot \sigma$ is defined in Proposition 7.3.9, and the display map as above. *Thin* is immediate from *thin* for interactions, and Proposition 7.3.6.

For ~-receptive, consider $\theta^{\tau} \odot \theta^{\sigma} : x^{\tau} \odot x^{\sigma} \cong_{\tau \odot \sigma} y^{\tau} \odot y^{\sigma}$ with extensions

$$ x^{\tau} \odot x^{\sigma} \vdash_{\tau \odot \sigma} p_{1}^{-}, \quad \partial_{\tau \odot \sigma}(\theta^{\tau} \odot \theta^{\sigma}) \vdash_{\tau \odot \sigma} (\partial_{\tau \odot \sigma}(p_{1}^{-}), (2, c_{2}^{-})), $$

assuming w.l.o.g. that $\partial_{\tau \odot \sigma}(p_1) = (2, c_1)$ occurs in $C$, witnessed in the interaction by

$$ x^{\tau} \oplus x^{\sigma} \subseteq y^{\tau} \oplus y^{\sigma} \vdash_{\tau \oplus \sigma} p_{1}^{-}, $$

where the inclusion only adds synchronized events, which w.l.o.g. we may assume to be causal dependencies of the extension $p_1$. In fact, then, $x^{\tau} \oplus x^{\sigma} = y^{\tau} \oplus y^{\sigma}$. Indeed, taking $p_0 \in y^{\tau} \oplus y^{\sigma}$ such that $p_0 \to_{\tau \oplus \sigma} p_1$, by Lemma 6.2.15 this entails that $(p_0)_\tau$
is defined and $(p_0)_\tau \dashv_\tau (p_1)_\tau$. But as $\tau$ is *span-courteous*, $\partial_\tau(p_0)_\tau = (2, c_0)$, so $p_0$ is
visible. Thus $p_0 \in x^\tau \oplus x^\sigma$ necessarily. So in fact, we have:

$$
x^{\tau} \otimes x^{\sigma} \vdash_{\tau \oplus \sigma} p_{1}^{-}, \quad \partial_{\tau \oplus \sigma}(\theta^{\tau} \otimes \theta^{\sigma}) \vdash_{\tau \oplus \sigma} ((3, c_{1}), (3, c_{2}))
$$

which projects to $x^\tau \vdash_\tau (p_1)_\tau$ and $\partial_\tau(\theta_\tau) \vdash_\tau (\partial_\tau((p_1)_\tau), (2, c_2))$, and by $\sim$-receptive for $\tau$, there is a unique $\theta^\tau \vdash_\tau ((p_1)_\tau, t_2)$ such that $\partial_\tau(t_2) = c_2$. Now, by Proposition 7.3.9 we have $y^\tau \odot y^\sigma \not\subset (y^\tau \bowtie \{t_2\}) \odot y^\sigma$ – those being easily seen minimal causally compatible – write $p_2 \in \tau \odot \sigma$ the added move. Likewise, we have

$$
\theta^{\tau} \odot \theta^{\sigma} \xrightarrow{\substack{(p_1, p_2) \\ \leftarrow}} (\theta^{\tau} \bowtie \{((p_1)_{\tau}, t_2)\}) \odot \theta^{\sigma}
$$

which fits the requirements; uniqueness is direct from uniqueness of $t_2$.

For *span-courteous*, take $p_1 \dashv_{\tau \odot \sigma} p_2$ s.t. $\text{pol}(p_1) = +$ or $\text{pol}(p_2) = -$, say first
$\text{pol}(p_2) = -$, and *w.l.o.g.* $p_2$ occurs in $C$, i.e. $\partial_{\tau \odot \sigma}(p_2) = (2, c_2^-)$. By Lemma 6.2.21,

$$
p_1 \dashv_{\tau \oplus \sigma} q_1 \dashv_{\tau \oplus \sigma} \dots \dashv_{\tau \oplus \sigma} q_n \dashv_{\tau \oplus \sigma} p_2
$$

with all $q_i$ synchronized, if any. But by Lemma 6.2.15, $(q_n)_\tau$ exists and $(q_n)_\tau \dashv_\tau (p_2)_\tau$.
But as $\tau$ is *span-courteous*, this implies $\partial_\tau((q_n)_\tau) = (2, c)$, so is $q_n$ visible – this entails
$p_1 = q_n$, so $\partial_{\tau \odot \sigma} = (2, c)$ as required. The case where $\text{pol}(p_1) = +$ is analogous.

Uniqueness up to strong iso is straightforward by Lemma 7.1.9.

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

Without *span-courtesy*, $\sim$-receptivity may fail to be preserved under composition – a
counter-example is not terribly hard to find; we omit it for the economy of presentation.

**Composition of strategies.** We may finally prove our main proposition:

**Proposition 7.3.1.** Consider A, B, C tcgs, and $\sigma: A \vdash B$ and $\tau: B \vdash C$ strategies.

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

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

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

order-isomorphisms commuting with dom, cod, and such that we have

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

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

*Proof. Existence.* Being *courteous*, strategies are in particular *span-courteous*, which applies to show that $\tau \odot \sigma$ is a prestrategy. It is a strategy by Proposition 6.3.1, as the additional conditions do not involve symmetry. The order-isomorphisms follow from Proposition 7.3.11 specialized to $+$-covered configurations – Lemmas 6.3.5, 6.3.6 and 6.3.7 directly extend to symmetries as they are order-isomorphisms.

Uniqueness. By Corollary 7.2.13.

<figure><img src="image_104.png" /></figure>
### 7.3.3 Copycat

Now, we introduce the copycat thin strategy. As for composition, copycat will simply be the copycat strategy of Chapter 6, adequately enriched with symmetry.

Recall from Lemma 6.4.2 that for a plain game A, the configurations of $\mathcal{C}_A$ are those $x \vdash y \in \mathcal{C}(A \vdash A)$ such that $x \supseteq^+ x \cap y \subseteq^- y$; here the intuition is that y comprises positive events imported from x, negative events already propagated to x, but also negative events that have yet to be forwarded to x – and the situation is symmetric for x.

So what should be a symmetry

$$ \theta : x_1 \vdash x_2 \cong_{\mathcal{C}_A} y_1 \vdash y_2? $$

As it should display to a symmetry on $A \vdash A$, we know it should have the form $\theta_1 \vdash \theta_2$ for $\theta_1 : x_1 \cong_A y_1$ and $\theta_2 : x_2 \cong_A y_2$. But that is not all: additionally, $\theta_1$ and $\theta_2$ must agree on events that have already been propagated. We formalize this as:

**Definition 7.3.12.** For any tcg A, $\mathcal{C}_A : A \vdash A$ is defined with Definition 6.4.1, with:

$$ \text{symmetry: } \mathcal{S}(\mathcal{C}_A) = \{\theta_1 \vdash \theta_2 \in \mathcal{S}(A \vdash A) \mid \\ \phantom{\text{symmetry: } \mathcal{S}(\mathcal{C}_A) = \{\theta_1 \vdash \theta_2 \in \mathcal{S}(A \vdash A) \mid } \mathrm{dom}(\theta_1 \vdash \theta_2) \in \mathcal{C}(\mathcal{C}_A), \mathrm{cod}(\theta_1 \vdash \theta_2) \in \mathcal{C}(\mathcal{C}_A), \\ \phantom{\text{symmetry: } \mathcal{S}(\mathcal{C}_A) = \{\theta_1 \vdash \theta_2 \in \mathcal{S}(A \vdash A) \mid } \forall a \in \mathrm{dom}(\theta_1) \cap \mathrm{dom}(\theta_2), \theta_1(a) = \theta_2(a) \}. $$

Note that though we have required $\theta_1(a) = \theta_2(a)$ on any element of the common domain. This looks asymmetric, but it will follow from the next lemma that we could have equivalently asked $\theta_1^{-1}(a) = \theta_2^{-1}(a)$ for any a in the common codomain.

Now we show that this gives a well-formed ess, and characterize its symmetries:

**Lemma 7.3.13.** Consider A a tcg. Then, $(|\mathcal{C}_A|, \le_A, \#_A, \mathcal{S}(\mathcal{C}_A))$ is an ess.
Moreover, $\mathcal{S}(\mathcal{C}_A) = \{\theta_1 \vdash \theta_2 \mid \theta_1, \theta_2 \in \mathcal{S}(A), \theta_1 \cap \theta_2 \supseteq \theta_1 \text{ & } \theta_1 \cap \theta_2 \subseteq \theta_2\}$.

*Proof.* We first prove the characterization of symmetries. For $\subseteq$, clearly $\theta_1 \cap \theta_2 \subseteq \theta_1$ and take $(a, a') \in \theta_1$ with $\mathrm{pol}_A(a) = -$. Since $\theta_1 \vdash \theta_2 \in \mathcal{S}(\mathcal{C}_A)$, in particular $\mathrm{dom}(\theta_1 \vdash \theta_2) \in \mathcal{C}(\mathcal{C}_A)$. So by Lemma 6.4.2, $a \in \mathrm{dom}(\theta_2)$. Now, by definition of $\mathcal{S}(\mathcal{C}_A)$ again, $\theta_1(a) = \theta_2(a)$, so $(a, a') \in \theta_1 \cap \theta_2$. The proof that $\theta_1 \cap \theta_2 \subseteq \theta_2$ is symmetric.

For $\supseteq$, consider $a \in \mathrm{dom}(\theta_1) \cap \mathrm{dom}(\theta_2)$ and w.l.o.g. assume $\mathrm{pol}_A(a) = +$; the other case is symmetric. Since $a \in \mathrm{dom}(\theta_2)$, there is $(a, a') \in \theta_2$. But since $\theta_1 \cap \theta_2 \subseteq \theta_2$, it follows that $(a, a') \in \theta_1$ as well, so $\theta_1(a) = \theta_2(a)$ as required. Next, we show $\mathrm{dom}(\theta_1 \vdash \theta_2) \in \mathcal{C}(\mathcal{C}_A)$ – let us write $\theta_1 : x_1 \cong_A y_1$ and $\theta_2 : x_2 \cong_A y_2$ and reason via Lemma 6.4.2. Consider $a^+ \in x_2$; we must show $a^+ \in x_1$ as well. But there is some $(a^+, b^+) \in \theta_2$, so by hypothesis $(a^+, b^+) \in \theta_1$ as well, so $a^+ \in x_1$. Symmetrically, any $a^- \in x_1$ must be in $x_2$; so $x_1 \vdash x_2 \in \mathcal{C}(\mathcal{C}_A)$. Symmetrically, $y_1 \vdash y_2 \in \mathcal{C}(\mathcal{C}_A)$.

Next come the axioms for isomorphism families. Groupoid and restriction follow directly from the characterization of symmetries and Lemma 6.4.2. However, extension is subtle – to keep the development focused we postpone it to Lemma 7.3.17. □

*Extension* is really subtle. Indeed, the first significant surprise when starting the design of concurrent games with symmetry, was that copycat failed *extension* with games
plain ess with polarities (see Section A.4 in [Castellan et al., 2019]); this is a large part of what first steered us towards saturation in [Castellan et al., 2014], and of what later prompted us to look for what would eventually become the definition of tcgs. Here we opt to keep going with the development of copycat which is largely independent of the proof of extension, and come back to extension later on.

We mention the property on symmetries reflecting Lemma 6.4.4:

**Lemma 7.3.14.** Consider A a tcg. Then, $\mathcal{S}^+(\mathcal{c}_A) = \{\theta \vdash \theta \mid \theta \in \mathcal{S}(A)\}$.

If $\theta \in \mathcal{S}(A)$, we write $\mathcal{c}_\theta = \theta \vdash \theta \in \mathcal{S}^+(\mathcal{c}_A)$ for this +-covered symmetry.

*Proof.* Immediate from Lemmas 7.3.13 and 6.4.4. □

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

Finally, we show that copycat indeed is a well-formed strategy.

**Proposition 7.3.15.** For any tcg A, we have $\mathcal{c}_A : A \vdash A$ a strategy.

*Proof.* By Lemma 7.3.13, $\mathcal{c}_A$ is an ess. We first check the conditions for a prestrategy (i.e. Definition 7.1.19). *Rule-abiding, locally injective, ~-preserving, and ~-receptive* are direct. For *thin*, consider $\theta_1 \vdash \theta_2 : x_1 \vdash x_2 \cong_{\mathcal{c}_A} y_1 \vdash y_2$ such that $\theta_1 \in \mathcal{S}_-(A)$ and $\theta_2 \in \mathcal{S}_+(A)$. By *restriction*, this means that $\theta_1 \cap \theta_1 \in \mathcal{S}_-(A) \cap \mathcal{S}_+(A)$. By *orthogonality*, this means that $\theta_1 \cap \theta_2 = \text{id}_X$ for some $X \in \mathcal{C}(A)$. But then, by Lemma 7.3.13, $\text{id}_X \subseteq \neg \theta_2$, so by *--receptive*, $\theta_2 \in \mathcal{S}_-(A)$. So again, $\theta_2 \in \mathcal{S}_-(A) \cap \mathcal{S}_+(A)$ must be an identity by *orthogonality* – the symmetric argument shows that $\theta_1$ is an identity.

Finally, we show the conditions of Definition 7.1.20: *courteous* follows from Lemma 6.4.3, while *receptive* is direct from Lemma 6.4.2. □

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

In the sequel, we shall mostly reason on copycat via the characterizations of its +-covered configurations and symmetries in Lemmas 6.4.2 and 7.3.13.

**The extension property.** Now, we set towards completing the proof of Lemma 7.3.13 and proving the *extension property* for $\mathcal{S}(\mathcal{c}_A)$. This is a bit technical, but this development will not be referred to later on in this monograph, so skipping to Section 7.4 should not impede understanding of the rest of the text.

First, we find it interesting to start with a counter-example, to see where is the tension and how *close* extension is to fail. Consider $!(\Theta \oplus)$ obtained via the clauses of Definition 7.1.26, ignoring the negativity assumption and the positive and negative symmetries (recall that we noted below Definition 7.1.26 that those do *not* form a tcg). We may define $\mathcal{c}_{!(\Theta \oplus)}$ exactly as in Definition 7.3.12, but it does *not* form an event structure with symmetry, as it fails *extension!* To see the problem, consider the symmetry

$$ \begin{array}{ccc} \oplus_1 & \vdash & \ominus_1 \\ \theta_1 \cong & & \cong \theta_2 \\ \oplus_1 & \vdash & \ominus_2 \end{array} $$

linking configurations of $\mathcal{c}_{!(\Theta \oplus)}$, where no event has been forwarded. The issue is that $\theta_1$ and $\theta_2$ have made irreconciliable choices regarding copy indices. It causes no issue
yet as they live in separated components, but the upper configuration may move to

$$ \Theta_1 \oplus_1 \Theta_1 \quad \vdash \quad \Theta_1 $$

which, by extension, should trigger a corresponding extension of the bottom configuration, and of the symmetry. But the bottom configuration may only extend to $\Theta_1 \oplus_1 \Theta_2$ (by propagating to the left hand side the event $\Theta_2$ from the right hand side), and $\Theta_1 \oplus_1 \Theta_1 \not\cong_!(\Theta_1 \oplus_1 \Theta_2)$, because a symmetry in $!(\Theta_1 \oplus_1 \Theta_2)$ must follow a permutation of copy indices! Thus, extension fails. Fortunately for tcgs this cannot happen, due to:

**Lemma 7.3.16.** Consider A a tcg, $\theta, \theta_1, \theta_2 \in \mathcal{S}(A)$ such that $\theta \subseteq^+ \theta_1$ and $\theta \subseteq^- \theta_2$. If $\text{dom}(\theta_1)$ and $\text{dom}(\theta_2)$ are compatible, then so are $\theta_1$ and $\theta_2$.

*Proof.* First, we prove this property for the positive symmetries, thus assume we have $\theta, \theta_1, \theta_2 \in \mathcal{S}_+(A)$ such that $\theta \subseteq^+ \theta_1$ and $\theta \subseteq^- \theta_2$. By extension for $\mathcal{S}_+(A)$, we have

$$ \begin{array}{ccc} \theta_1' : x_1 \cup x_2 \cong_A^+ y_1' & \theta_2' : x_1 \cup x_2 \cong_A^+ y_2' & \\ \mathop{\cup}_1 & \mathop{\cup}_1 & \\ \theta_1 : x_1 \cong_A^+ y_1 & \theta_2 : x_2 \cong_A^+ y_2 & \\ \times \mathcal{S} & \mathcal{S} & \\ \theta : x \cong_A^+ y & & \end{array} $$

so by groupoid, we can form $\varphi = \theta_2' \circ \theta_1'^{-1} : y_1' \cong_A^+ y_2'$. As both $\theta_1'$ and $\theta_2'$ contain $\theta$, it follows that $\text{id}_y \subseteq \varphi$. Now, by restriction, consider $\psi : x_1' \cong_A^+ y_2$ obtained by restricting $\varphi$ to $y_2$ on the right. Since $y \subseteq y_2$, we still have $\text{id}_y \subseteq \psi$. But actually that inclusion is negative, which – as $\text{id}_y \in \mathcal{S}_-(A)$ – entails that $\psi \in \mathcal{S}_-(A)$ as well. Thus by orthogonality, $x_1' = y_2$ and $\psi = \text{id}_{y_2}$. Summing up, if $(a, a') \in \theta_2$, then $(a, a') \in \theta_2'$, and there is $(a'', a') \in \varphi$ for some $(a'', a) \in \theta_1'^{-1}$. But then $(a'', a') \in \psi$ also, hence $a'' = a'$ and $(a, a') \in \theta_1'$; so we have proved $\theta_2 \subseteq \theta_1'$, establishing compatibility of $\theta_1$ and $\theta_2$. Symmetrically, the same property holds for $\mathcal{S}_-(A)$.

Now, from this we must conclude that the property holds for $\mathcal{S}(A)$, so take $\theta, \theta_1, \theta_2 \in \mathcal{S}(A)$ such that $\theta \subseteq^+ \theta_1$ and $\theta \subseteq^+ \theta_2$. By Lemma 7.1.18, we have unique factorizations

$$ \theta = \theta^+ \circ \theta^-, \quad \theta_1 = \theta_1^+ \circ \theta_1^-, \quad \theta_2 = \theta_2^+ \circ \theta_2^- $$

By uniqueness in Lemma 7.1.18, it is immediate that this factorization is monotone, i.e. $\theta^+ \subseteq \theta_1^+$ and $\theta^+ \subseteq \theta_2^+$, so by the reasoning above we have $\theta_1^+$ and $\theta_2^+$ compatible in $\mathcal{S}_+(A)$, i.e. $\theta_1^+ \cup \theta_2^+ \in \mathcal{S}_+(A)$. Likewise, $\theta_1^- \cup \theta_2^- \in \mathcal{S}_-(A)$. Now it is immediate that $\theta_1^- \cup \theta_2^-$ and $\theta_1^+$ and $\theta_2^+$ are composable, and that we have

$$ (\theta_1^+ \cup \theta_2^+) \circ (\theta_1^- \cup \theta_2^-) = (\theta_1^+ \circ \theta_1^-) \cup (\theta_2^+ \circ \theta_2^-) = \theta_1 \cup \theta_2 $$

which must hence be a valid symmetry, concluding that $\theta_1$ and $\theta_2$ are compatible. $\square$

With the key lemma above, it is straightforward to finally deduce:

**Lemma 7.3.17.** Consider A a tcg. Then, $\mathcal{S}(\mathcal{C}_A)$ satisfies extension.
*Proof.* Consider a symmetry on copycat, which may be written as

$$ \begin{array}{ccc} x_1 & \vdash & x_2 \\ \theta_1 \downarrow & & \downarrow \theta_2 \\ y_1 & \vdash & y_2 \end{array} $$

and consider an extension of $x_1 \vdash x_2$. Without loss of generality, we can consider that only $x_2$ is extended, and with moves of the same polarity – this leaves two cases, for $x_2 \subseteq^- x'_2$ and $x_2 \subseteq^+ x'_2$. In the former case, then by extension we have $\theta_2 \subseteq \theta'_2$: $x'_2 \cong_A y'_2$, and $\theta_1 \subseteq^+ \theta_1 \cap \theta_2 \subseteq^- \theta_2 \subseteq^+ \theta'_2$, so $\theta_1 \vdash \theta'_2 \in \mathcal{S}(\mathfrak{c}_A)$ by Lemma 7.3.13.

In the latter case, writing $x'_1 = x_1 \cap x'_2$, and considering the restriction $\theta'_1$ of $\theta_1$ to $x'_1$,

$$ \theta'_1 \supseteq \theta_1 \cap \theta_2 \subseteq \theta_2, $$

so that $\theta'_2 = \theta'_1 \cup \theta_2 \in \mathcal{S}(A)$ by Lemma 7.3.16; and $\theta_1 \vdash \theta'_2$ is the desired extension. $\square$

At last, this concludes the construction of the thin copycat strategy.

## 7.4 The Bicategory TCG

We have most of the ingredients for our bicategory **TCG**: a notion of objects (thin concurrent games), morphisms (thin strategies), 2-cells (positive morphisms). We have the data for identities (copycat strategies) and composition.

**Structural 2-cells.** We must still extend from **CG** the 2-cells for associativity and unity laws, which is direct from the developments above. For associators, we have:

**Proposition 7.4.1.** Consider thin prestrategies $\sigma : A \vdash B$, $\tau : B \vdash C$ and $\delta : C \vdash D$. Then, there is a strong isomorphism of strategies, the **associator**

$$ a_{\sigma, \tau, \delta} : (\delta \odot \tau) \odot \sigma \cong \delta \odot (\tau \odot \sigma), $$

such that for all $(x^\delta \odot x^\tau) \odot x^\sigma \in \mathcal{C}((\delta \odot \tau) \odot \sigma)$ and $(\theta^\delta \odot \theta^\tau) \odot \theta^\sigma \in \mathcal{S}((\delta \odot \tau) \odot \sigma)$,

$$ a_{\sigma, \tau, \delta}((x^\delta \odot x^\tau) \odot x^\sigma) = x^\delta \odot (x^\tau \odot x^\sigma) $$

$$ a_{\sigma, \tau, \delta}((\theta^\delta \odot \theta^\tau) \odot \theta^\sigma) = \theta^\delta \odot (\theta^\tau \odot \theta^\sigma). $$

*Proof.* To apply Lemma 7.1.9 we show the associator preserves symmetry, which is clear by the description of the symmetries in the composition in Proposition 7.3.9. $\square$

Likewise, the developments above make it easy to define the **unitors**:

**Proposition 7.4.2.** Consider $\sigma : A \vdash B$ a thin strategy.

Then there are strong isomorphisms, the **unitors**:

$$ l_\sigma : \mathfrak{c}_B \odot \sigma \cong \sigma $$

$$ r_\sigma : \sigma \odot \mathfrak{c}_A \cong \sigma $$
### 7.4.1 Synchronization up to Symmetry

Fix $\sigma : A \vdash B$ and $\tau : B \vdash C$ two (pre)strategies.

First, we must specify under which conditions we expect to be able to synchronize two configurations up to symmetry. As without symmetry, there needs to be some causal compatibility condition – accordingly, we first generalize the definition of *causally compatible pairs* (Definition 6.2.2) to account for a mediating symmetry:

**Definition 7.4.3.** Consider $x^\sigma \in \mathcal{C}(\sigma)$, $x^\tau \in \mathcal{C}(\tau)$ and $\theta : x_B^\sigma \cong_B x_B^\tau$. We say that the triple $(x^\sigma, \theta, x^\tau)$ is *causally compatible* if the composite bijection

$$ \varphi[x^\sigma, \theta, x^\tau] : x^\sigma \parallel x_C^\tau \cong x_A^\sigma \parallel x_B^\sigma \parallel x_C^\tau \cong x_A^\sigma \parallel x_B^\tau \parallel x_C^\tau \cong x_A^\sigma \parallel x^\tau $$

is secured, in the sense that the relation

$$ (m, n) \triangleleft (m', n') \quad \Leftrightarrow \quad m <_{\sigma \parallel C} m' \lor n <_{A \parallel \tau} n' $$

defined on (the graph of) $\varphi[x^\sigma, \theta, x^\tau]$ from the causal constraints of $\sigma$ and $\tau$, is acyclic.

In that case, the reflexive transitive closure of $\triangleleft$ is a partial order $\leq_{\varphi[x^\sigma, \theta, x^\tau]}$, and $(x^\sigma, \theta, x^\tau)$ is **minimal** if the maximal elements of $\varphi[x^\sigma, \theta, x^\tau]$ occur in A or C.

At the core of TCG is the following property, stating that any causally compatible triple can be massaged to produce a unique equivalent causally compatible pair:

**Proposition 7.4.4.** Consider $(x^\sigma, \theta, x^\tau)$ a *causally compatible triple*. Then, there are unique $y^\sigma \in \mathcal{C}(\sigma)$ and $y^\tau \in \mathcal{C}(\tau)$ *causally compatible*, and

$$ \varphi^\sigma : x^\sigma \cong_\sigma y^\sigma, \qquad \varphi^\tau : x^\tau \cong_\tau y^\tau, $$

such that we have $\varphi_A^\sigma \in \mathcal{S}_-(A)$, $\varphi_C^\tau \in \mathcal{S}_+(C)$, and the following diagram commutes:

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

(in particular, the middle triangle commutes – the squares come for free).

*Proof.* Securedness follows the obvious generalization of Definition 6.2.2.

*Existence.* For a secured bijection $\phi$ (top of the diagram) as above, assume adequate $\varphi^\sigma : x^\sigma \cong_\sigma y^\sigma$ and $\varphi^\tau : x^\tau \cong_\tau y^\tau$ are provided by induction hypothesis. Consider:

$$ \phi \stackrel{(m,n)}{\rightleftharpoons} \phi' $$

with $\phi'$ a composite bijection. We first consider the key case, with $m = (1, s)$ for $x^\sigma \vdash_\sigma s^+$, and $n = (2, t)$ for $x^\tau \vdash_\tau t^-$ synchronized. Let us write their displays as

$$ \partial_\sigma(x^\sigma \triangleright \{s\}) = x_A^\sigma \vdash (x_B^\sigma \triangleright \{b_1\}), \quad \partial_\tau(x^\tau \triangleright \{t\}) = (x_B^\tau \triangleright \{b_2\}) \vdash x_C^\tau $$
synchronizing through $\theta \uplus \{(b_1, b_2)\} \in \mathcal{S}(B)$.

By extension for $\sigma$, we may propagate this extension through $\varphi^\sigma$ to obtain:

$$ \psi^{\sigma} = \varphi^{\sigma} \uplus \{(s, s')\} : x^{\sigma} \uplus \{s\} \cong_{\sigma} y^{\sigma} \uplus \{s'\} $$

displaying to $\partial_{\sigma}(\psi^{\sigma}) = \varphi_{A}^{\sigma} \vdash (\varphi_{B}^{\sigma} \uplus \{(b_1, b')\}) \in \mathcal{S}(A \vdash B)$. But then:

$$ \varphi_{B}^{\tau} \uplus \{(b_2, b')\} \in \mathcal{S}(B) $$

as it may be obtained as the composition $(\varphi_B^\sigma \uplus \{(b_1, b')\}) \circ (\theta \uplus \{(b_1, b_2)\})^{-1}$ of known symmetries in $B$. Then $\sim$-receptivity directly applies to provide $\psi^\tau = \varphi^\tau \uplus \{(t, t')\}$ matching this extension, concluding this case – missing verifications are immediate.

The case with $s$ negative and $t$ positive is symmetric. Next, consider the case $m = (2, c)$ and $n = (2, t)$ with $x^\tau \vdash_{\tau} t^-$, i.e. a visible, negative move in $C$. Its display is

$$ \partial_{\tau}(x^{\tau} \uplus \{t\}) = x_{B}^{\tau} \vdash (x_{C}^{\tau} \uplus \{c\}), $$

but then extension of $\mathcal{S}_+(C)$ applies to provide an extension $\varphi_C^\tau \uplus \{(c, c')\} \in \mathcal{S}_+(C)$. By $\sim$-receptivity of $\tau$, there is an (unique) matching extension $\psi^\tau = \varphi^\tau \uplus \{(t, t')\} \in \mathcal{S}(\tau)$, concluding this case – other components are unchanged.

Consider then the case $m = (2, c)$ and $n = (2, t)$ with $x^\tau \vdash_{\tau} t^+$. In that case,

$$ \psi^{\tau} = \varphi^{\tau} \uplus \{(t, t')\} \in \mathcal{S}(\tau) $$

is provided by extension for $\tau$. Considering its display $\partial_{\tau}(\psi^{\tau}) = \varphi_B^\tau \vdash (\varphi_C^\tau \uplus \{(c, c')\})$, we do have $\psi_C^\tau \in \mathcal{S}_+(C)$ as $\varphi_C^\tau \in \mathcal{S}_+(C)$ and by $\sim$-receptivity of tcgs. This concludes this case – other components are unchanged. All missing cases are symmetric. Finally, securedness follows from the diagram and securedness of $(x^\sigma, \theta, x^\tau)$, as all vertical morphisms in the diagram are order-isomorphisms.

**Uniqueness.** Consider now $\psi^\sigma : x^\sigma \cong_\sigma z^\sigma$ and $\psi^\tau : x^\tau \cong_\tau z^\tau$ also satisfying the hypotheses. But then, by composition of symmetries we also have

$$ \omega^{\sigma} = \psi^{\sigma} \circ (\varphi^{\sigma})^{-1} : y^{\sigma} \cong_{\sigma} z^{\sigma}, \qquad \omega^{\tau} = \psi^{\tau} \circ (\varphi^{\tau})^{-1} : y^{\tau} \cong_{\tau} z^{\tau}, $$

but additionally these symmetries are causally compatible, since

$$ \begin{aligned} \omega_B^\sigma &= \psi_B^\sigma \circ (\varphi_B^\sigma)^{-1} \\ &= \psi_B^\tau \circ \theta \circ (\varphi^\tau \circ \theta)^{-1} \\ &= \omega_B^\tau \end{aligned} $$

hence we have $\omega^\tau \otimes \omega^\sigma : y^\tau \otimes y^\sigma \cong_{\tau \otimes \sigma} z^\tau \otimes z^\sigma$ by Proposition 7.3.6. But additionally,

$$ (\omega^\tau \otimes \omega^\sigma)_A = \psi_A^\sigma \circ (\varphi_A^\sigma)^{-1} \in \mathcal{S}_-(A), $$

and likewise $(\omega^\tau \otimes \omega^\sigma)_C \in \mathcal{S}_+(C)$, so by thin for $\tau \otimes \sigma$, $\omega^\tau \otimes \omega^\sigma = \mathrm{id}_{y^\tau \otimes y^\sigma}$. It follows from Proposition 7.3.6 that $\omega^\sigma$ and $\omega^\tau$ are identities, so $\varphi^\sigma = \psi^\sigma$ and $\varphi^\tau = \psi^\tau$. $\square$

The above may be applied to compose configurations up to symmetry:
**Corollary 7.4.5.** Consider $(x^\sigma, \theta, x^\tau)$ a minimal causally compatible triple.
Then, the pair $(y^\sigma, y^\tau)$ given by Proposition 7.4.4 is minimal causally compatible.

*Proof.* By Proposition 7.4.4, we have $\varphi^\sigma : x^\sigma \cong_\sigma y^\sigma$ and $\varphi^\tau : x^\tau \cong_\tau y^\tau$ making

$$ \begin{array}{ccc} x^{\sigma} \parallel x_{C}^{\tau} & \xrightarrow{\varphi[x^{\sigma}, \theta, x^{\tau}]} & x_{A}^{\sigma} \parallel x^{\tau} \\ \varphi^{\sigma} \parallel \varphi_{C}^{\tau} & \downarrow & \downarrow \varphi_{A}^{\sigma} \parallel \varphi^{\tau} \\ y^{\sigma} \parallel y_{C}^{\tau} & \xrightarrow{\varphi[y^{\sigma}, y^{\tau}]} & y_{A}^{\sigma} \parallel y^{\tau} \end{array} $$

commute. But the vertical morphisms are order-isomorphisms, inducing an order-isoto between the (graphs of) $\varphi[x^\sigma, \theta, x^\tau]$ and $\varphi[y^\sigma, y^\tau]$. In particular it preserves maximal elements, so that the minimality of $(y^\sigma, y^\tau)$ follows from that of $(x^\sigma, \theta, x^\tau)$. $\square$

This finally lets us define the composition of configurations up to symmetry:

**Definition 7.4.6.** Consider $(x^\sigma, \theta, x^\tau)$ a minimal *causally compatible triple*. We set

$$ x^{\tau} \odot_{\theta} x^{\sigma} = y^{\tau} \odot y^{\sigma} \in \mathscr{C}(\tau \odot \sigma) $$

for $y^\sigma, y^\tau$ the minimal *causally compatible pair* given by Corollary 7.4.5.

It will be useful later on that this construction preserves unions:

**Lemma 7.4.7.** Consider $(x_1^\sigma, \theta_1, x_1^\tau)$, $(x_2^\sigma, \theta_2, x_2^\tau)$ minimal *causally compatible triples*, also compatible which each other in the sense that $(x_1^\sigma \cup x_2^\sigma, \theta_1 \cup \theta_2, x_2^\tau \cup x_2^\sigma)$ is a minimal *causally compatible triple*. Then, $x_1^\tau \odot_{\theta_1} x_1^\sigma$ and $x_2^\tau \odot_{\theta_2} x_2^\sigma$ are compatible, and

$$ (x_1^\tau \cup x_2^\tau) \odot_{\theta_1 \cup \theta_2} (x_1^\sigma \cup x_2^\sigma) = (x_1^\tau \odot_{\theta_1} x_2^\sigma) \cup (x_2^\tau \odot_{\theta_2} x_2^\sigma) $$

*Proof.* Applying Proposition 7.4.4 to $(x^\sigma, \theta, x^\tau) = (x_1^\sigma \cup x_2^\sigma, \theta_1 \cup \theta_2, x_2^\tau \cup x_2^\sigma)$, we get

$$ \begin{array}{ccc} x^{\sigma} \parallel x_{C}^{\tau} & \xrightarrow{\partial_{\sigma} \parallel x_{C}^{\tau}} & x_{A}^{\sigma} \parallel x_{B}^{\sigma} \parallel x_{C}^{\tau} \xrightarrow{x_{A}^{\sigma} \parallel \theta_{\sigma} \parallel x_{C}^{\tau}} x_{A}^{\sigma} \parallel x_{B}^{\tau} \parallel x_{C}^{\tau} \xrightarrow{x_{A}^{\sigma} \parallel \partial_{\tau}^{-1}} x_{A}^{\sigma} \parallel x^{\tau} \\ \varphi^{\sigma} \parallel \varphi_{C}^{\tau} & \xrightarrow{\varphi_{A}^{\sigma} \parallel \varphi_{B}^{\sigma} \parallel \varphi_{C}^{\tau}} & \xrightarrow{\varphi_{A}^{\sigma} \parallel \varphi_{B}^{\tau} \parallel \varphi_{C}^{\tau}} \\ y^{\sigma} \parallel y_{C} & \xrightarrow{\partial_{\sigma} \parallel y_{C}} & y_{A} \parallel y_{B} \parallel y_{C} \xrightarrow{y_{A} \parallel \partial_{\tau}^{-1}} y_{A} \parallel y^{\tau} \end{array} $$

with similar diagrams for $(x_1^\sigma, \theta_1, x_1^\tau)$ and $(x_2^\sigma, \theta_2, x_2^\tau)$ yielding causally compatible pairs $(y_1^\sigma, y_1^\tau)$ and $(y_2^\sigma, y_2^\tau)$. But the diagram above restricts to diagrams for $(x_1^\sigma, \theta_1, x_1^\tau)$ and $(x_2^\sigma, \theta_2, x_2^\tau)$, so by the uniqueness clause of Proposition 7.4.4 it must be the componentwise union of the diagrams for $(x_1^\sigma, \theta_1, x_1^\tau)$ and $(x_2^\sigma, \theta_2, x_2^\tau)$. Thus, we have

$$ \varphi[y^{\sigma}, y^{\tau}] = \varphi[y_{1}^{\sigma}, y_{1}^{\tau}] \cup \varphi[y_{2}^{\sigma}, y_{2}^{\tau}] $$

which, restricting to prime sub-secured bijections with visible top, yields

$$ x^{\tau} \odot_{\theta} x^{\sigma} = (x_{1}^{\tau} \odot_{\theta_{1}} x_{1}^{\sigma}) \cup (x_{2}^{\tau} \odot_{\theta_{2}} x_{2}^{\sigma}) $$

as required, implying also their compatibility. $\square$
## 7.4.2 Horizontal Composition

We can now use this to define horizontal composition of positive morphisms:

**Proposition 7.4.8.** Consider $\sigma, \sigma' : A \vdash B$ and $\tau, \tau' : B \vdash C$ (pre)strategies, along with $f : \sigma \Rightarrow \sigma'$ and $g : \tau \Rightarrow \tau'$ positive morphisms.

Then, there is a unique positive morphism $g \odot f : \tau \odot \sigma \rightarrow \tau' \odot \sigma'$ such that

$$ (g \odot f)(x^{\tau} \odot x^{\sigma}) = g(x^{\tau}) \odot_{g[x^{\tau}]_{B} \circ f[x^{\sigma}]_{B}^{-1}} f(x^{\sigma}) $$

for all $x^{\tau} \odot x^{\sigma} \in \mathscr{C}(\tau \odot \sigma)$ where $f[x^{\sigma}]_{B}$ and $g[x^{\tau}]_{B}$ arise as below (7.6).

*Proof. Existence.* Unfortunately, we cannot directly apply Lemma 7.2.11, because we want this proposition to handle positive morphisms between *prestrategies*. Thus, we construct $g \odot f$ via Lemma 7.1.9. Its action on configurations is given by definition – in particular, it follows immediately from *rigidity* that if $(x^{\sigma}, x^{\tau})$ is minimal causally compatible, then $(f(x^{\sigma}), g[x^{\tau}]_{B} \circ f[x^{\sigma}]_{B}^{-1}, g(x^{\tau}))$ is minimal causally compatible. Preservation of unions follows from Lemma 7.4.7 and the fact that

$$ g[x^{\tau}]_{B} \circ f[x^{\sigma}]_{B}^{-1} = (g[x_{1}^{\tau}]_{B} \circ f[x_{1}^{\sigma}]_{B}^{-1}) \cup (g[x_{2}^{\tau}]_{B} \circ f[x_{2}^{\sigma}]_{B}^{-1}) $$

whenever $x^{\sigma} = x_{1}^{\sigma} \cup x_{2}^{\sigma}$ and $x^{\tau} = x_{1}^{\tau} \cup x_{2}^{\tau}$. Preservation of cardinality follows from the preservation of the display to the game (see *positivity* below).

We must show that this action extends to symmetries. Consider

$$ \psi^{\tau} \odot \psi^{\sigma} : x^{\tau} \odot x^{\sigma} \cong_{\tau \odot \sigma} y^{\tau} \odot y^{\sigma} $$

a symmetry in $\tau \odot \sigma$; so $\psi^{\sigma} : x^{\sigma} \cong_{\sigma} y^{\sigma}$, $\psi^{\tau} : x^{\tau} \cong_{\tau} y^{\tau}$ with $\psi_{B}^{\sigma} = \psi_{B}^{\tau}$. We name:

$$ \begin{array}{ccc} f(x^{\sigma})_{B} & \xleftarrow{(\varphi_{B}^{\sigma})^{-1}} & x_{B}^{\sigma} = x_{B}^{\tau} \xrightarrow{g[x^{\tau}]_{B}} g(x^{\tau})_{B} \\ \xrightarrow{(\nu_{B}^{\tau})^{-1}} & \xrightarrow{\varphi_{B}^{\tau}} & z_{B}^{\sigma'} = z_{B}^{\tau'} \end{array} \qquad \begin{array}{ccc} f(y^{\sigma})_{B} & \xleftarrow{f[y^{\sigma}]_{B}} & y_{B}^{\sigma} = y_{B}^{\tau} \xrightarrow{g[y^{\tau}]_{B}} g(y^{\tau})_{B} \\ \xrightarrow{\nu_{B}^{\sigma}} & & u_{B}^{\sigma'} = u_{B}^{\tau'} \end{array} $$

writing $z^{\tau'} \odot z^{\sigma'} = g(x^{\tau}) \odot_{\theta} f(x^{\sigma})$ for $\theta = g[x^{\tau}]_{B} \circ f[x^{\sigma}]_{B}^{-1}$, and $u^{\tau} \odot u^{\sigma} = g(y^{\tau}) \odot_{\vartheta} f(y^{\sigma})$ for $\vartheta = g[y^{\tau}]_{B} \circ f[y^{\sigma}]_{B}^{-1}$. Next we note that the diagram below commutes

$$ \begin{array}{ccc} f(x^{\sigma})_{B} & \xleftarrow{f[x^{\sigma}]_{B}} & x_{B}^{\sigma} = x_{B}^{\tau} \xrightarrow{g[x^{\tau}]_{B}} g(x^{\tau})_{B} \\ \xrightarrow{f(\psi^{\sigma})_{B}} & & \psi_{B}^{\sigma} = \psi_{B}^{\tau} \\ \xrightarrow{f(y^{\sigma})_{B}} & \xleftarrow{f[y^{\sigma}]_{B}} & y_{B}^{\sigma} = y_{B}^{\tau} \xrightarrow{g[y^{\tau}]_{B}} g(y^{\tau})_{B} \end{array} $$
by definition of the components involved. But this means that the following diagram

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

commutes as well; so we may set the image $(g \odot f)(\psi^\tau \odot \psi^\sigma)$ of $\psi^\tau \odot \psi^\sigma$ as

$$(v^\sigma \circ f(\psi^\sigma) \circ (\varphi^\sigma)^{-1}) \circ (v^\tau \circ g(\psi^\tau) \circ (\varphi^\tau)^{-1}) : (g \odot f)(x^\tau \odot x^\sigma) \cong_{\tau' \circ \sigma'} (g \odot f)(y^\tau \odot y^\sigma)$$

and as Proposition 7.4.4 entails that $\varphi^\sigma$ is uniquely determined by $f(\psi^\sigma)$ and similarly for $\varphi^\tau$, $v^\sigma$ and $v^\tau$, it follows that this construction is monotone.

*Positivity.* Write $y^{\tau'} \odot y^{\sigma'} = (g \odot f)(x^{\tau} \odot x^{\sigma})$. We have

$$ \begin{tikzcd} x^{\sigma} \arrow[r, "f"] \arrow[d, "\partial_{\sigma}"] & f(x^{\sigma}) \arrow[r, "\varphi^{\sigma'}"] \arrow[d, "\partial_{\sigma'}"] & y^{\sigma'} \arrow[d, "\partial_{\sigma'}"] \\ \frac{f[x^{\sigma}]_{A} \vdash f[x^{\sigma}]_{B}}{\vdash} \arrow[r, "\varphi^{\sigma'} \vdash \varphi^{\sigma'}"] & \frac{\vdash}{\varphi^{\sigma'} \vdash \varphi^{\sigma'} \vdash} & \frac{\vdash}{\varphi^{\sigma'} \vdash \varphi^{\sigma'} \vdash} \arrow[r, "f(x^{\tau})"] \arrow[d, "\partial_{\tau}"] \arrow[d, "\partial_{\tau}"] & g(x^{\tau}) \arrow[r, "\varphi^{\tau'}"] \arrow[d, "\partial_{\tau'}"] & y^{\tau'} \arrow[d, "\partial_{\tau'}"] \arrow[r, "f(x^{\tau}) \vdash f(x^{\tau})_{B}"] \arrow[d, "\varphi^{\tau'} \vdash \varphi^{\tau'} "] \arrow[d, "\varphi^{\tau'} \vdash \varphi^{\tau'} \vdash"] \end{tikzcd} $$

$$ \begin{tikzcd} x^{\tau} \arrow[r, "f"] \arrow[d, "\partial_{\tau}"] & g(x^{\tau}) \arrow[r, "\varphi^{\tau'}"] \arrow[d, "\partial_{\tau'}"] & y^{\tau'} \arrow[d, "\partial_{\tau'}"] \\ \frac{f[x^{\tau}]_{A} \vdash f[x^{\tau}]_{B}}{\vdash} \arrow[r, "\varphi^{\tau'} \vdash \varphi^{\tau'} \vdash} & \frac{\vdash}{\varphi^{\tau'} \vdash \varphi^{\tau'} \vdash} & \frac{\vdash}{\varphi^{\tau'} \vdash \varphi^{\tau'} \vdash \vdash} \arrow[r, "f(x^{\tau}) \vdash f(x^{\tau})_{B}"] \arrow[d, "\varphi^{\tau'} \vdash \varphi^{\tau'} "] \arrow[d, "\varphi^{\tau'} \vdash \varphi^{\tau'} \vdash"] \end{tikzcd} $$

where in each case the left hand square commutes by definition of positive morphisms, and $\varphi^\sigma$, $\varphi^\tau$ provided by Proposition 7.4.4 – which also ensure that $\varphi_A^{\sigma'} \in S_-(A)$ and $\varphi_C^{\tau'} \in S_+(C)$. Now from the above, by definition and monotonicity of the constructions,

$$ \begin{tikzcd} x^{\tau} \odot x^{\sigma} \arrow[r, "g \odot f"] \arrow[d, "\partial_{\sigma}"] & (g \odot f)(x^{\tau} \odot x^{\sigma}) \arrow[d, "\partial_{\tau'}"] \\ \frac{\varphi_{A}^{\sigma'} \circ f[x^{\sigma}]_{A} \vdash \varphi_{C}^{\tau'} \circ g[x^{\tau}]_{C}}{\vdash} \arrow[r, "\varphi_{A}^{\sigma'} \vdash \varphi_{C}^{\tau'} \vdash \varphi_{C}^{\tau'} \vdash g[x^{\tau}]_{C}"] \arrow[d, "\varphi_{C}^{\tau'} \vdash \varphi_{C}^{\tau'} "] & \frac{\vdash}{\varphi_{C}^{\tau'} \vdash \varphi_{C}^{\tau'} \vdash \varphi_{C}^{\tau'} \vdash g[x^{\tau}]_{C}} \arrow[r, "f(x^{\tau})"] \arrow[d, "\varphi_{C}^{\tau'} \vdash \varphi_{C}^{\tau'} "] \arrow[d, "\varphi_{C}^{\tau'} \vdash \varphi_{C}^{\tau'} \vdash"] \end{tikzcd} \quad (7.7) $$

commutes as well, and $\varphi_A^{\sigma'} \circ f[x^\sigma]_A \in S_-(A)$ and $\varphi_C^{\tau'} \circ g[x^\tau]_C \in S_+(C)$ as required.

*Uniqueness.* Direct consequence of Lemma 6.1.12. $\square$

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

In particular, this entails that thin equivalence is a congruence, i.e. if $\sigma \approx \sigma' : A \vdash B$ and $\tau \approx \tau' : B \vdash C$, then $\tau \odot \sigma \approx \tau' \odot \sigma' : A \vdash C$. This will be useful when, later on, we truncate our bicategory **TCG** into a *~-category* – see Section 7.4.4.

We prove one final lemma on horizontal composition:

**Lemma 7.4.9.** Consider $f : \sigma \to \sigma'$ and $g : \tau \to \tau'$ positive morphisms.

Then, for all minimal causally compatible triple $(x^\sigma, \theta, x^\tau)$, we have:

$$ (g \odot f)(x^{\tau} \odot \theta x^{\sigma}) = g(x^{\tau}) \odot_{g[x^{\tau}]_{B} \circ \theta \circ f[x^{\sigma}]_{B}^{-1}} f(x^{\sigma}). $$
*Proof.* Let us write $y^\tau \odot y^\sigma = x^\tau \odot_\theta x^\sigma$ and $z^\tau \odot z^\sigma = (g \odot f)(y^\tau \odot y^\sigma)$; by definition of $x^\tau \odot_\theta x^\sigma$ and of $(g \odot f)(y^\tau \odot y^\sigma)$, we have symmetries $\varphi^\sigma : x^\sigma \cong_\sigma y^\sigma$, $\varphi^\tau : x^\tau \cong_\tau y^\tau$, $\nu^\sigma' : f(y^\sigma) \cong_\sigma z^\sigma'$ and $\nu^\tau' : g(y^\tau) \cong_\tau z^\tau'$, satisfying the triangles:

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

It follows that the following diagram commutes as well:

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

which proves our equality by uniqueness of Proposition 7.4.4. □

### 7.4.3 Bicategorical Laws

Proving the bicategorical laws requires one final technical development, establishing an associativity property of synchronization up to symmetry.

**Ternary synchronization up to symmetry.** Fix three strategies

$$ \sigma : A \vdash B, \quad \tau : B \vdash C, \quad \delta : C \vdash D $$

with configurations $x^\sigma \in \mathscr{C}(\sigma)$, $x^\tau \in \mathscr{C}(\tau)$, $x^\delta \in \mathscr{C}(\delta)$, and mediating symmetries

$$ \theta : x_B^\sigma \cong_B x_B^\tau, \quad \omega : x_C^\tau \cong_C x_C^\delta. $$

What can we say about their synchronizations up to symmetry? Assuming $(x^\sigma, \theta, x^\tau)$ is minimal causally compatible, by Proposition 7.4.4 there are unique

$$ \varphi^\sigma : x^\sigma \cong_\sigma y^\sigma, \quad \varphi^\tau : x^\tau \cong_\tau y^\tau $$

such that $\varphi_A^\sigma \in \mathscr{S}_-(A)$, $\varphi_C^\tau \in \mathscr{S}_+(C)$ and the following diagram commutes

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

and by Corollary 7.4.5, $y^\sigma$, $y^\tau$ are minimal causally compatible. With these notations:

**Lemma 7.4.10.** Assume $(x^\sigma, \theta, x^\tau)$ and $(x^\tau \odot_\theta x^\sigma, \omega \odot (\varphi_C^\tau)^{-1}, x^\delta)$ are min. caus. comp.
Then, so is $(x^\tau, \omega, x^\delta)$.
*Proof.* In that case, then by Proposition 7.4.4 there are unique

$$ \Psi^{\sigma, \tau} : y^{\tau} \odot y^{\sigma} \cong_{\tau \odot \sigma} u^{\tau} \odot u^{\sigma}, \quad \Psi^{\delta} : x^{\delta} \cong_{\delta} u^{\delta} $$

such that $\Psi_{A}^{\sigma, \tau} \in \mathcal{S}_{-}(A)$, $\Psi_{D}^{\delta} \in \mathcal{S}_{+}(D)$ and the following diagram commutes:

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

recalling that $\Psi^{\sigma, \tau} : y^{\tau} \odot x^{\sigma} \cong_{\tau \odot \sigma} u^{\tau} \odot u^{\sigma}$ consists in $\Psi^{\sigma} : x^{\sigma} \cong_{\sigma} u^{\sigma}$ and $\Psi^{\tau} : x^{\tau} \cong_{\tau} u^{\tau}$ matching on $B$. By Corollary 7.4.5, $u^{\tau} \odot u^{\sigma}$ and $u^{\delta}$ are minimal causally compatible. By Lemma 6.2.24, it follows that $u^{\tau}, u^{\delta}$ are minimal causally compatible. But then

$$ \Psi^{\tau \circ \varphi^{\tau}} : x^{\tau} \cong_{\tau} u^{\tau}, \quad \Psi^{\delta} : x^{\delta} \cong_{\delta} u^{\delta} $$

are order-isomorphisms such that the following triangle commutes:

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

Following these isomorphisms, it is a direct verification to establish causal compatibility of $(x^{\tau}, \omega, x^{\delta})$ from that of $(u^{\tau}, u^{\delta})$. $\square$

Now, assuming that the conditions of this lemma are satisfied, we know that $(x^{\tau}, \omega, x^{\delta})$ are causally compatible. This means, again by Proposition 7.4.4, that there are

$$ \psi^{\tau} : x^{\tau} \cong_{\tau} z^{\tau}, \quad \psi^{\delta} : x^{\delta} \cong_{\delta} z^{\delta} $$

such that the following triangle commutes:

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

Using these notations, we can then prove the following lemma:

**Lemma 7.4.11.** Assume $(x^{\sigma}, \theta, x^{\tau})$ and $(x^{\tau} \odot_{\theta} x^{\sigma}, \omega \circ (\varphi_{C}^{\tau})^{-1}, x^{\delta})$ are min. caus. comp. Then, so is $(x^{\sigma}, \psi_{B}^{\tau} \circ \theta, x^{\delta} \odot_{\omega} x^{\tau})$.

*Proof.* By Corollary 7.4.5, $u^{\sigma}$ and $u^{\delta} \odot u^{\tau}$ are minimal causally compatible. As for the previous lemma, the idea is to provide symmetries making minimal causal compatibility of $(x^{\sigma}, \psi_{B}^{\tau} \circ \theta, x^{\delta} \odot_{\omega} x^{\tau})$ boil down to that of $(u^{\sigma}, u^{\delta} \odot u^{\tau})$. First there is:

$$ \Psi^{\sigma \circ \varphi^{\sigma}} : x^{\sigma} \cong_{\sigma} u^{\sigma}, $$
and likewise we have two symmetries

$$ \Psi^{\tau \circ \varphi^{\tau} \circ (\psi^{\tau})^{-1}} : z^{\tau} \cong_{\tau} u^{\tau}, \quad \Psi^{\delta \circ (\psi^{\delta})^{-1}} : z^{\delta} \cong_{\delta} u^{\delta} $$

which can be checked to have the same projection on $C$. So their synchronization yields

$$ \Phi = (\Psi^{\delta \circ (\psi^{\delta})^{-1}}) \odot (\Psi^{\tau \circ \varphi^{\tau} \circ (\psi^{\tau})^{-1}}) : x^{\delta} \odot_{\omega} x^{\tau} \cong_{\delta \odot \tau} u^{\delta} \odot u^{\tau}. $$

Finally, a direct verification shows that the triangle below commutes:

$$ \begin{tikzcd} & & x_B^{\sigma} \arrow[r, "\psi_B^{\tau \circ \theta}"] \arrow[d, "\psi^{\sigma \circ \varphi^{\sigma}}"] & (x^{\delta} \odot_{\omega} x^{\tau})_B \arrow[d, "\Phi_B"'] \arrow[r, "\psi_B^{\tau \circ \theta}"] \\ u_B & & & \end{tikzcd} \qquad (7.8) $$

via which the announced min. caus. comp. boils down to that of $(u^{\sigma}, u^{\delta} \odot u^{\tau})$. $\square$

At this point we are equipped to state the seeked associativity property:

**Lemma 7.4.12.** If $(x^{\sigma}, \theta, x^{\tau})$ and $(x^{\tau} \odot_{\theta} x^{\sigma}, \omega \circ (\varphi_{C}^{\tau})^{-1}, x^{\delta})$ are min. caus. comp.,

$$ x^{\delta} \odot_{\omega \circ (\varphi_{C}^{\tau})^{-1}} (x^{\tau} \odot_{\theta} x^{\sigma}) = a_{\sigma, \tau, \delta}((x^{\delta} \odot_{\omega} x^{\tau}) \odot_{\psi_{B}^{\tau} \circ \theta} x^{\sigma}). $$

*Proof.* Keeping the notations above, $x^{\delta} \odot_{\omega \circ (\varphi_{C}^{\tau})^{-1}} (x^{\tau} \odot_{\theta} x^{\sigma}) = u^{\delta} \odot (u^{\tau} \odot u^{\sigma})$. Now,

$$ \Psi : x^{\delta} \odot_{\omega} x^{\tau} \cong_{\delta \odot \tau} u^{\delta} \odot u^{\tau}, \quad \Psi^{\sigma} \circ \varphi^{\sigma} : x^{\sigma} \cong_{\sigma} u^{\sigma} $$

are symmetries satisfying (7.8); and it is direct from the definition that $\Psi_A \in \mathcal{S}_-(A)$ and $(\Psi^{\sigma} \circ \varphi^{\sigma})_C \in \mathcal{S}_+(C)$. Consequently, by the uniqueness clause of Proposition 7.4.4,

$$ (x^{\delta} \odot_{\omega} x^{\tau}) \odot_{\psi_{B}^{\tau} \circ \theta} x^{\sigma} = (u^{\delta} \odot u^{\tau}) \odot u^{\sigma} $$

and $a_{\sigma, \tau, \delta}((u^{\delta} \odot u^{\tau}) \odot u^{\sigma}) = u^{\delta} \odot (u^{\tau} \odot u^{\sigma})$ as required. $\square$

**A bicategory.** At last, we have the ingredients to conclude:

**Theorem 7.4.13.** There is a bicategory TCG with games as objects, strategies as morphisms, and positive morphisms as 2-cells.

*Proof.* Identities are defined in Proposition 7.3.15, and composition in Proposition 7.3.1. Each strategy has an identity 2-cell (the identity positive isomorphism). Vertical composition of positive morphisms is composition in ESS, and horizontal composition is Proposition 7.4.8. Associators are defined in Proposition 7.4.1 and unitors in Proposition 7.4.2. It remains to prove the following laws:
**Functoriality of horizontal composition.** For functoriality, we compute

$$
\begin{align*}
& (g' \odot f') \circ (g \odot f)(x^\tau \odot x^\sigma) \\
&= (g' \odot f')(g(x^\tau) \odot_{g[x^\tau]_B \circ f[x^\sigma]_B^{-1}} f(x^\sigma)) \\
&= g'(g(x^\tau)) \odot_{g'[g(x^\tau)]_B \odot g[x^\tau]_B \circ f[x^\sigma]_B^{-1}} f'[f(x^\sigma)]_B^{-1} f'(f(x^\sigma)) \\
&= (g' \circ g)(x^\tau) \odot_{(g' \circ g)[x^\tau]_B \circ (f' \circ f)[x^\sigma]_B^{-1}} (f' \circ f)(x^\sigma) \\
&= ((g' \circ g) \odot (f' \circ f))(x^\tau \odot x^\sigma)
\end{align*}
$$

using definition of $g \odot f$, Lemma 7.4.9, definition of the preservation of symmetry of $g' \circ g$ and $f' \circ f$, and definition of $(g' \circ g) \odot (f' \circ f)$. By Lemma 6.1.12, we conclude that $(g' \circ f') \circ (g \circ f) = (g' \circ g) \circ (f' \circ f)$ as required. Likewise, it is straightforward using the same lemmas that horizontal composition preserves identity positive morphisms.

*Naturality of unitors.* We first show the naturality of $l_\sigma : \mathcal{C}_B \odot \sigma \cong \sigma$ in $\sigma$, i.e. that for all $\sigma, \sigma' : A \vdash B$ and $f : \sigma \Rightarrow \sigma'$ a positive morphism, we have $f \circ l_\sigma = l_{\sigma'} \circ (\mathcal{C}_B \odot f)$, and by Corollary 7.2.12 it suffices to prove the equality for $+-$covered configurations. By Lemma 6.4.4, $+-$covered configurations in $\mathcal{C}_B \odot \sigma$ have form $\mathcal{C}_{\chi_B^\sigma} \odot x^\sigma \in \mathcal{C}^+(\mathcal{C}_B \odot \sigma)$, and by definition of horizontal composition (in Proposition 7.4.8),

$$ (\mathcal{C}_B \odot f)(\mathcal{C}_{\chi_B^\sigma} \odot x^\sigma) = \mathcal{C}_{\chi_B^\sigma} \odot_{f[x^\sigma]_B^{-1}} f(x^\sigma), $$

but that must be $\mathcal{C}_{f(x^\sigma)_B} \odot f(x^\sigma) \in \mathcal{C}^+(\mathcal{C}_B \odot \sigma')$ as it is easily proved to satisfy the properties in Proposition 7.4.4 defining it uniquely.

Now, from the characterization of the action of unitors in Proposition 7.4.2,

$$ l_{\sigma'}(\mathcal{C}_{f(x^\sigma)_B} \odot f(x^\sigma)) = f(x^\sigma) $$

which is also $f(l_\sigma(\mathcal{C}_{\chi_B^\sigma} \odot x^\sigma)) = f(x^\sigma)$. The proof for $r_\sigma$ is symmetric.

*Naturality of associators.* Consider now $f : \sigma \Rightarrow \sigma' : A \vdash B$, $g : \tau \Rightarrow \tau' : B \vdash C$ and $h : \delta \Rightarrow \delta' : C \vdash D$ positive morphisms, and calculate:

$$
\begin{align*}
& (h \odot (g \odot f)) \circledast a_{\sigma, \tau, \delta}((x^{\delta} \odot x^{\tau}) \odot x^{\sigma}) \\
&= (h \odot (g \odot f))(x^{\delta} \odot (x^{\tau} \odot x^{\sigma})) \\
&= h(x^{\delta}) \odot_{h[x^{\delta}]_C \circ (g \odot f)[x^{\tau} \circ x^{\sigma}]_C^{-1}} (g \odot f)(x^{\tau} \odot x^{\sigma}) \\
&= h(x^{\delta}) \odot_{h[x^{\delta}]_C \circ (g \odot f)[x^{\tau} \circ x^{\sigma}]_C^{-1}} (g(x^{\tau}) \odot_{g[x^{\tau}]_B \circ h[x^{\sigma}]_B^{-1}} f(x^{\sigma})) \\
&= h(x^{\delta}) \odot_{h[x^{\delta}]_C \circ g[x^{\tau}]_C^{-1} \circ (\varphi_C^{\tau'})^{-1}} (g(x^{\tau}) \odot_{g[x^{\tau}]_B \circ f[x^{\sigma}]_B^{-1}} f(x^{\sigma})) \\
&= a_{\sigma', \tau', \delta'}((h(x^{\delta}) \odot_{h[x^{\delta}]_C \circ g[x^{\tau}]_C^{-1}} g(x^{\tau})) \odot_{\psi_B^{\tau} \circ g[x^{\tau}]_B \circ f[x^{\sigma}]_B^{-1}} f(x^{\sigma})) \\
&= a_{\sigma', \tau', \delta'}((h(x^{\delta}) \odot_{h[x^{\delta}]_C \circ g[x^{\tau}]_C^{-1}} g(x^{\tau})) \odot_{(h \circ g)[x^{\delta} \circ x^{\tau}]_B \circ f[x^{\sigma}]_B^{-1}} f(x^{\sigma})) \\
&= a_{\sigma', \tau', \delta'}((h \circ g)(x^{\tau} \odot x^{\sigma}) \odot_{(h \circ g)[x^{\delta} \circ x^{\tau}]_B \circ f[x^{\sigma}]_B^{-1}} f(x^{\sigma})) \\
&= a_{\sigma', \tau', \delta'}(((h \circ g) \odot f)((x^{\delta} \odot x^{\tau}) \odot x^{\sigma}))
\end{align*}
$$

using Lemma 7.4.9 twice, then the witness exposed in (7.7) for the fact that $g \odot f$ is a positive morphism, then Lemma 7.4.12 (using the same notations for $\varphi$ and $\psi$), then
again the witness in (7.7) for the fact that $h \circ g$ is a positive morphism, concluding with two applications of Lemma 7.4.9 – which finally ends the proof. $\square$

Though we have constructed a bicategory **TCG**, most of this monograph relies on a simpler structure ignoring coherence laws, sufficient for many semantic purposes.

### 7.4.4 A ~-category

To wrap up this chapter, we introduce a simplified higher-dimensional structure.

In order to use **TCG** for semantic purposes, we need much additional categorical structure: in particular, we must at least have a cartesian closed structure in order to interpret the simply-typed $\lambda$-calculus. Following Theorem 7.4.13, the reader may naturally expect us to aim towards constructing the *bicategorical* version of this structure. Such a construction is described by Paquet in [Paquet, 2020]. But ultimately, the explicit managing of 2-cells does not appear particularly useful for the semantic purposes of this monograph so we opted to not develop this higher-dimensional structure further.

Alternatively, we could quotient **TCG** to a category having as morphisms equivalence classes of strategies with respect to positive isomorphism (as done for instance in AJM games [Abramsky et al., 2000]). But this is actually harmful: it is methodologically better for the interpretation to yield actual concrete strategies, rather than equivalence classes (for instance, recursion is obtained via completeness properties of an ordering on strategies that does not seem to lift to equivalence classes). We also want to avoid the vagueness often encountered in switching implicitly between equivalence classes and representatives.

So we shall work neither with categories nor bicategories but with ~-categories:

**Definition 7.4.14.** A (small) ~-category $C$ consists in a set of objects $C_0$; for each $A, B$, a set of morphisms $C(A, B)$ with an equivalence relation $\sim$; a composition operation

$$(- \circ -) : C(B, C) \times C(A, B) \to C(A, C)$$

for all $A, B, C \in C_0$; an identity morphism $\mathrm{id}_A \in C(A, A)$ for all $A \in C_0$, subject to:

associativity: for all $f \in C(A, B)$, $g \in C(B, C)$, $h \in C(C, D)$, $(h \circ g) \circ f \sim h \circ (g \circ f)$,

identity: for all $f \in C(A, B)$, $\mathrm{id}_B \circ f \sim f \circ \mathrm{id}_A \sim f$,

congruence: for all $f \sim f' \in C(A, B)$, $g \sim g' \in C(B, C)$, $g' \circ f' \sim g \circ f$.

In other words, a ~-category is a special case of a bicategory where any two morphisms are related by at most one (invertible) 2-cell. Any bicategory yields a ~-category where $f \sim g$ iff $f$ and $g$ are related by an isomorphism.

Using ~-categories avoids quotienting morphisms, while making all coherence laws hold vacuously. All categorical notions extend transparently to ~-categories, with equations holding up to ~ rather than equality. For instance, functors between ~-categories respect ~, and preservation of identities and composition only holds up to ~. In the
sequel, we shall use several standard categorical notions in the ~-categorical world
without explicitly spelling them out – hopefully this causes no confusion.

From now on, we regard TCG as a ~-category:

**Proposition 7.4.15.** *There is TCG, a ~-category with tcgs as objects, strategies as morphisms, and equivalence relation ≈ the thin equivalence, from Corollary 7.2.9.*

**7.5 History and Related Work**

**Genesis of TCG.** I arrived as a postdoc with Glynn Winskel in Cambridge in September 2011. After participating in a first project to enrich concurrent games with winning conditions [Clairambault et al., 2012], my main task was the supposedly simple objective to extend **CG** with *symmetry* [Winskel, 2007], in particular so that concurrent games could handle replication as in AJM games [Abramsky et al., 2000]. What was initially expected to be relatively straightforward proved to be an endeavour full of surprises, for which we were soon joined by a research intern, Simon Castellan.

As discussed ealier, there are two ways to handle uniformity in (copy indices-based)
game semantics. The *fat* way, and the *thin* way. The fat approach to uniformity consists
in forcing strategies to be saturated: if a strategy can play one copy index, it must play
non-deterministically *all* copy indices. In contrast, in the thin approach, a strategy in a
given state will play *one canonically chosen* copy index. Uniformity then becomes an
interactive property: any change in Opponent's copy indices causes a subsequent change
in Player's copy indices. This *thin/fat* distinction is not about concurrent games at all,
but present as soon as there are strategies with copy indices: the original AJM games
are thin [Abramsky et al., 2000], but they can be made fat – the very first fat model
is [Baillot et al., 1997a]. The fat approach is simpler; however, it conflates uniformity
with non-determinism and also is not a compatible extension of the symmetry-free layer
as the basic mechanisms (identity and composition) must be changed.

In developing concurrent games with symmetry, we found that we could not make
the thin approach work as we lacked a good way to describe the interactive reindexing
process involved in uniformity. So the first published version of concurrent games with
symmetry is fat<sup>3</sup> [Castellan et al., 2014]<sup>4</sup>. However, saturation made the model difficult
to use, and I kept looking for a thin version, whose maturing was a long process.

*Thin concurrent games* first appeared in [Castellan et al., 2015] (the paper was mainly
about parallel innocence – see Chapter 10. The core of this setting is the one presented in
this chapter, though with many crucial changes and simplifications. Many significant
improvements (including the very definition of a tcg!) are due to Simon Castellan,
developed during his PhD thesis; others came while writing the journal version detailing
thin concurrent games [Castellan et al., 2019], and others still appeared since.

<footnote n="3"><sup>3</sup>In fact, the very first version of concurrent games with symmetry is thin, and only appears in Simon Castellan's (unpublished) internship report – however, we could only make this work adopting a coarse bisimulation-like equivalence relation on strategies, whereas we wanted an isomorphism.</footnote>

<footnote n="4"><sup>4</sup>Not very well-known is the fact that this paper also contains the very first non-deterministic generalization of Hyland-Ong innocence!</footnote>
**Further comments.** This chapter mainly presents constructions first introduced in [Castellan et al., 2015] and improved in [Castellan et al., 2019]. However, the latter uses results from [Castellan et al., 2017a], making for a somewhat intimidating chain of dependencies. In contrast, the present chapter is entirely self-contained and constructs thin concurrent games from the ground, with full details.

Finally, this chapter builds a bicategory, whereas the papers cited above only con-
struct a category up to positive isomorphisms. This is not a new result: in his PhD
thesis, Paquet proves that thin concurrent games form a bicategory (actually a symmet-
ric monoidal closed bicategory [Paquet, 2020]). However, Paquet does not detail the
naturality of unitors and associators; so our proof complements his.

It seems fair to say that **TCG** is the most expressive and fine-grained intensional
model on the market. Much of our further work builds on it, and there is a lot left to
explore. I consider this to be one of the main contributions in this line of work.

**Related work.** The core idea behind TCG is splitting symmetries into *positive* and *negative* symmetries: it is thanks to this separation that we are able to factor out Opponent’s reindexings when expressing uniformity and when comparing strategies. As mentioned earlier, this idea was first developed by Melliès as his approach to uniformity in asynchronous games [Melliès, 2003]. There, he considers an *asynchronous game* with two groups acting on plays, one for Player reindexings and one for Opponent reindexings; uniformity is there specified as a *bi-invariance* property with respect to these group actions, analogous in spirit to Lemma 7.2.6 – note that recently, Paquet showed that Melliès’ mechanism could also be applied in the setting of concurrent games [Paquet, 2023], obtaining a different, more global, notion of uniformity which differs from the present one for subtle reasons.

In any case, this polarized decomposition of symmetry is clearly a fundamental struc-
ture that deserves further exploration. One such recent exploration is a joint work with
Simon Forest, in which we build a bicategory of *thin spans of groupoids* sharing much
of the structure of **TCG**, but completely statically [Clairambault and Forest, 2023], i.e.
without time or causality. There, an *object* is a groupoid with two sub-groupoids,
the *positive* and the *negative* ones. Morphisms are spans of groupoids selected by a
biorthogonality relation ensuring that their composition satisfies a universal property
analogous to Proposition 7.3.1, but without causal compatibility. Overall, we get a
proof-relevant relational model sharing much of the flavour of **TCG**, but avoiding the
combinatorics of concurrent strategies and their composition.
# Chapter 8

## Constructing Games and Strategies

The previous chapter describes the bare bones of thin concurrent games: namely, the composition mechanism and the tools to handle symmetry. In the present chapter, we describe the constructions on games and strategies that will be exploited throughout this monograph, aiming to establish categorical structures useful for semantics.

In practice, we will build from **TCG** two radically different categorical structures.

**TCG per se** is an *unpolarized* category of games, in that games have no assigned polarity: in a game *A*, both players may be able to start. This is in contrast with most notions of games used in game semantics, which focus on *negative* games where only Opponent starts (for call-by-name languages), or on *positive* games where only Player starts (for call-by-value languages). A widespread urban legend has it that such non-polarized game settings suffer from a lack of associativity, due to the infamous *Blass problem* [Abramsky, 2003]. In fact, this phenomenon is very specific to Blass games, and Proposition 6.2.25 ensures that composition in **TCG** is indeed associative up to iso. But **TCG** is certainly not the first unpolarized category of games, the pioneering example is Joyal’s category of Conway games [Joyal, 1977]. As pioneered by Joyal, the expected categorical structure of such an unpolarized category of games is that of a *compact closed category*, i.e. a degenerate model of MLL where $\otimes = \mathcal{N}$. Our first objective in this chapter will be to show that **TCG** is a compact closed $\sim$-category.

To prepare the ground for semantics, we must then switch to *polarized games* – *negative*, since the languages considered here are call-by-name. We shall equip the negative sub-$\sim$-category of **TCG** with (a variation of) the structure of a *Seely category* [Melliès, 2009]. Seely categories are a standard model of ILL, and thus of the simply-typed $\lambda$-calculus; and we shall use this structure as the basis for our interpretations.
## 8.1 A Compact closed ~-Category

Compact closed categories are amongst the simplest categorical structures that exhibit higher-order behaviour. They are essentially those degenerated models of multiplicative linear logic where the ⊗ and its dual ℛ coincide – intuitively, they resemble proof nets without the correctness criterion. Like Conway games [Joyal, 1977], categories of unpolarized games are often compact closed, and this structure underlies much of the additional structure appearing in polarized categories of games, as explored by Melliès [Melliès, 2004b]. It is thus natural to start there.

Recall that a compact closed category is a symmetric monoidal category C where each object A has a (necessarily unique up to iso) dual object A*. This means we have

$$ \begin{aligned} \text{the unit, } \eta_A & : I \to A \otimes A^* \\ \text{the co-unit, } \epsilon_A & : A^* \otimes A \to I \end{aligned} $$

two morphisms for all A, respectively akin to the axiom and cut of proof nets, satisfying two coherence axioms [Kelly and Laplaza, 1980]. A compact closed ~-category is defined likewise, with all laws holding up to ~ instead of equality.

### 8.1.1 A bifunctor

For thin concurrent games we start with the first component, a ~-bifunctor:

$$ (- \parallel -) : \mathbf{TCG} \times \mathbf{TCG} \to \mathbf{TCG}. $$

Notice that we use $\parallel$ for the tensor of the compact closed structure, as we shall reserve $\otimes$ for a later construction in the context of negative games.

**Definition.** On tcgs, the construction $\parallel$ is defined in Section 7.1.4. If A and B are tcgs, then $A \parallel B$ is thought of as the game formed of A and B played in parallel. Note that though the games are independent, a strategy on $A \parallel B$ may very well impose crossed immediate causal links between the two components!

On strategies, the action of $\parallel$ is given by the following:

**Proposition 8.1.1.** Consider A, B, C, D tcgs, and $\sigma : A \vdash B$, $\tau : C \vdash D$ strategies. Then, there is a strategy $\sigma \parallel \tau : A \parallel C \vdash B \parallel D$, unique up to iso, s.t. there are

$$ \begin{aligned} (- \parallel -) & : \mathcal{C}^{+}(\sigma) \times \mathcal{C}^{+}(\tau) \approx \mathcal{C}^{+}(\sigma \parallel \tau) \\ (- \parallel -) & : \mathcal{S}^{+}(\sigma) \times \mathcal{S}^{+}(\tau) \approx \mathcal{S}^{+}(\sigma \parallel \tau) \end{aligned} $$

order-isos commuting with dom, cod, and s.t. for all $\theta^\sigma \in \mathcal{S}^+(\sigma)$ and $\theta^\tau \in \mathcal{S}^+(\tau)$,

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

Moreover, $(- \parallel -)$ preserves $\approx$ (a property we call congruence).
**Proof. Existence.** As the notation suggests, $\sigma \parallel \tau$ has the simple parallel composition of $\sigma$ and $\tau$. Its display map is set as:

$$ \partial_{\sigma \parallel \tau}(1, s) = \begin{cases} (1, (1, a)) & \text{if } \partial_{\sigma}(s) = (1, a) \\ (2, (1, b)) & \text{if } \partial_{\sigma}(s) = (2, b) \\ (1, (2, c)) & \text{if } \partial_{\tau}(t) = (1, c) \\ (2, (2, d)) & \text{if } \partial_{\tau}(t) = (2, d), \end{cases} $$
$$ \partial_{\sigma \parallel \tau}(2, t) = \begin{cases} (1, (1, a)) & \text{if } \partial_{\sigma}(s) = (1, a) \\ (2, (1, b)) & \text{if } \partial_{\sigma}(s) = (2, b) \\ (1, (2, c)) & \text{if } \partial_{\tau}(t) = (1, c) \\ (2, (2, d)) & \text{if } \partial_{\tau}(t) = (2, d), \end{cases} $$

we omit the routine verification that this yields a strategy. All additional conditions follow as in Lemma 7.1.22 along with routine verifications.

*Uniqueness.* Straightforward consequence of Corollary 7.2.13.

*Congruence.* Immediate from the definition. $\square$

**Functoriality.** Proposition 8.1.1 makes functoriality easy. First:

**Lemma 8.1.2.** For any tcgs A and B, we have $\mathfrak{c}_{A\parallel B} \approx \mathfrak{c}_A \parallel \mathfrak{c}_B$.

*Proof.* We calculate:

$$ \begin{align*} \mathcal{C}^+(\mathfrak{c}_A \parallel \mathfrak{c}_B) &\cong \mathcal{C}^+(\mathfrak{c}_A) \times \mathcal{C}^+(\mathfrak{c}_B) \\ &= \{x_A \parallel x_A \mid x_A \in \mathcal{C}(A)\} \times \{x_B \parallel x_B \mid x_B \in \mathcal{C}(B)\} \\ &\cong \{(x_A \parallel x_B) \parallel (x_A \parallel x_B) \mid x_A \parallel x_B \in \mathcal{C}(A \parallel B)\} \\ &= \mathcal{C}^+(\mathfrak{c}_{A\parallel B}) \end{align*} $$

using Proposition 8.1.1, then Lemma 6.4.4, then the obvious bijection, then Lemma 6.4.4 again – all these are order-isos, which preserve display maps in the obvious sense.

The same reasoning applies to symmetries compatibly, using Proposition 8.1.1 and Lemma 7.3.14. Finally, the seeked isomorphism follows from Corollary 7.2.13. $\square$

For preservation of composition, consider four strategies:

$$ \sigma_1 : A_1 \vdash B_1, \quad \sigma_2 : A_2 \vdash B_2, \quad \tau_1 : B_1 \vdash C_1, \quad \tau_2 : B_2 \vdash C_2. $$

The only additional ingredient needed is the following lemma:

**Lemma 8.1.3.** Take $x^{\sigma_1} \in \mathcal{C}^+(\sigma_1)$, $x^{\sigma_2} \in \mathcal{C}^+(\sigma_2)$, $x^{\tau_1} \in \mathcal{C}^+(\tau_1)$ and $x^{\tau_2} \in \mathcal{C}^+(\tau_2)$.

Then, $x^{\sigma_1} \parallel x^{\sigma_2} \in \mathcal{C}^+(\sigma_1 \parallel \sigma_2)$ and $x^{\tau_1} \parallel x^{\tau_2} \in \mathcal{C}^+(\tau_1 \parallel \tau_2)$ are causally compatible iff (1) $x^{\sigma_1}$ and $x^{\tau_1}$ are causally compatible; and (2) $x^{\sigma_2}$ and $x^{\tau_2}$ likewise.

*Proof.* A routine verification, left to the reader. $\square$

Now, we can finally conclude:

**Proposition 8.1.4.** Parallel composition extends to a $\sim$-bifunctor:

$$ (- \parallel -) : \mathbf{TCG} \times \mathbf{TCG} \to \mathbf{TCG}. $$
*Proof.* Preservation of copycat is by Lemma 8.1.2. For composition, we calculate:

$$ \begin{align*} & \mathcal{C}^+((\tau_1 \parallel \tau_2) \odot (\sigma_1 \parallel \sigma_2)) \\ & \cong \{(x^{\tau_1} \parallel x^{\tau_2}, x^{\sigma_1} \parallel x^{\sigma_2}) \in \mathcal{C}^+(\tau_1 \parallel \tau_2) \times \mathcal{C}^+(\sigma_1 \parallel \sigma_2) | \text{caus. comp.}\} \\ & \cong \{(x^{\tau_1}, x^{\sigma_1}) \in \mathcal{C}^+(\tau_1) \times \mathcal{C}^+(\sigma_1) | \text{caus. comp.}\} \times \\ & \qquad \{(x^{\tau_2}, x^{\sigma_2}) \in \mathcal{C}^+(\tau_2) \times \mathcal{C}^+(\sigma_2) | \text{caus. comp.}\} \\ & \cong \mathcal{C}^+(\tau_1 \odot \sigma_1) \times \mathcal{C}^+(\tau_2 \odot \sigma_2) \end{align*} $$

using Proposition 7.3.1, then Proposition 8.1.1 along with Lemma 8.1.3, then Proposition 7.3.1 again. All these are order-isos, preserve display maps, and the same reasoning applies to symmetries – so the desired isomorphism follows from Corollary 7.2.13. □

## 8.1.2 Lifting Maps to Strategies

Besides this bifunctor, we need structural morphisms for the monoidal structure.

We introduce a method to construct them systematically. The idea is that all these morphisms are direct variations of copycat: they play copycat following a certain isomorphism of games. Accordingly, we show how to lift certain maps to strategies.

**Renamings.** We shall lift more than just isos: “liftable” maps are called renamings:

**Definition 8.1.5.** A renaming from game A to B is a function $f: |A| \to |B|$ satisfying:

validity: $\forall x \in \mathcal{C}(A), f(x \in \mathcal{C}(B))$

local injectivity: $\forall a_1, a_2 \in x \in \mathcal{C}(A), f a_1 = f a_2 \Rightarrow a_1 = a_2$

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

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

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

courtesy: $\forall a_1 \to_A a_2, (\text{pol}_A(a_1) = + \vee \text{pol}_A(a_2) = -) \Rightarrow f a_1 \to_B f a_2$.

We write **Ren** for the category of renamings, and $f: A \to B$ for a renaming.

Any isomorphism of games (i.e. an isomorphism preserving all structure) is a renaming. Renamings let us change the display of events of strategies, via the operation:

**Definition 8.1.6.** Consider $\sigma: A \vdash B$, with renamings $f: A^{\perp} \to A'^{\perp}, g: B \to B'$. Then, the redisplayed strategy $g \cdot \sigma \cdot f$ has components the same as $\sigma$, except:

$$ \partial_{g \cdot \sigma, f} = (f \parallel g) \circ \partial_{\sigma}. $$

This is still a strategy – note the strategy itself is not really changed, only its display. Here, $f \parallel g$ refers to the monoidal structure of ESS, defined with $(f \parallel g)(1, a) = (1, f(a))$ and $(f \parallel g)(2, b) = (2, g(b))$. Note also that we can redisplay on one side of a strategy only, as in $g \cdot \sigma$: this means $g \cdot \sigma \cdot \text{id}_A$ – likewise, $\sigma \cdot f$ means $\text{id}_B \cdot \sigma \cdot f$.
**Lifting.** We motivated renamings by the *lifting* operation, which is:

**Definition 8.1.7.** Consider $f : A \to B$ a renaming.

Its forward lifting $\mathfrak{c}_f : A \vdash B$ is defined as $\mathfrak{c}_f = f \cdot \mathfrak{c}_A$.

Its backward lifting $\mathfrak{d}_f : B^{\perp} \vdash A^{\perp}$ is defined as $\mathfrak{d}_f = \mathfrak{c}_{A^{\perp}} \cdot f$.

This gives a simple definition of a strategy playing copycat alongside a certain map. This is a nice feature of concurrent games: such a construction is ubiquitous also in more traditional game semantics settings, but it is very rarely made explicit.

The fundamental property enjoyed by this construction is the **lifting lemma**:

**Lemma 8.1.8.** Consider $\sigma : A \vdash B$, and renamings $f : A^{\perp} \to A'^{\perp}$, $g : B \to B'$.

Then, $g \cdot \sigma \cdot f \approx \mathfrak{c}_g \odot \sigma \odot \mathfrak{d}_f$.

*Proof.* We show $g \cdot \sigma \approx \mathfrak{c}_g \odot \sigma$ – note $\sigma \cdot f \approx \sigma \odot \mathfrak{d}_f$ is symmetric, and the general case follows since $g \cdot \sigma \cdot f = g \cdot (\sigma \cdot f) = (g \cdot \sigma) \cdot f$ and $\odot$ is associative up to $\approx$.

By definition, $\mathfrak{C}^+(\mathfrak{c}_f) = \mathfrak{C}^+(\mathfrak{c}_B) = \{x_B \parallel x_B \mid x_B \in \mathfrak{C}(B)\}$ (Lemma 6.4.4), with

$$ \partial_{\mathfrak{c}_g}(x_B \parallel x_B) = x_B \parallel g(x_B). $$

Thus a pair $(x^{\sigma}, x_B \parallel x_B)$ is causally compatible for $\sigma$ and $\mathfrak{c}_f$ iff it is causally compatible for $\sigma$ and $\mathfrak{c}_B$. We may then reuse the unitor of Proposition 6.4.9 which yields $r_{\sigma} : \mathfrak{C}^+(\sigma \odot \mathfrak{c}_f) \cong \mathfrak{C}^+(\sigma)$. Computing the display maps, we have

$$ \partial_{g \cdot \sigma}(x^{\sigma}) = g(x_B^{\sigma}) = g(x_B), \quad \partial_{\mathfrak{c}_g \odot \sigma}((x_B \parallel x_B) \odot x^{\sigma}) = g(x_B) $$

where $x_B^{\sigma} = x_B$ as the pair $(x^{\sigma}, x_B \parallel x_B)$ is matching. The same reasoning applies to symmetries using Lemma 7.3.14. By Corollary 7.2.13, we deduce the desired iso. $\square$

We deduce one last convenient property of lifting:

**Proposition 8.1.9.** There are two $\sim$-functors:

$\mathfrak{c}_- : \mathrm{Ren} \to \mathrm{TCG}$,

$\mathfrak{d}_- : \mathrm{Ren}^{\mathrm{OP}} \to \mathrm{TCG}$,

such that if $f : A \to B$ is an iso, then $\mathfrak{c}_f$ and $\mathfrak{d}_{f^{\perp}}$ are inverses, and $\mathfrak{c}_{f^{-1}} \approx \mathfrak{d}_{f^{\perp}}$.

*Proof.* By Lemma 8.1.8 and a direct verification via Corollary 7.2.13. $\square$

Above, we write $f^{\perp} : A^{\perp} \to B^{\perp}$ for $f : A \to B$ defined as the same map as $f$. Note that if $f : A \to B$ is an iso, then $f^{\perp} : A^{\perp} \to B^{\perp}$ is an iso hence a renaming.

### 8.1.3 Compact Closed Structure

We may now directly apply this for the symmetric monoidal structure.
**Symmetric monoidal structure.** We need structural isomorphisms for TCG.

First, notice that Ren is a symmetric monoidal category. Indeed, for $f : A \to B$ and $f' : A' \to B'$ renamings, then $f \parallel f' : A \parallel A' \to B \parallel B'$ is a renaming. Furthermore, there are obvious isomorphisms of tcgs, so invertible renamings

$$
\begin{align*}
\rho_A & : \quad A \parallel \mathbf{1} \to A \\
\lambda_A & : \quad \mathbf{1} \parallel A \to A \\
\alpha_{A,B,C} & : \quad (A \parallel B) \parallel C \to A \parallel (B \parallel C) \\
s_{A,B} & : \quad A \parallel B \to B \parallel A
\end{align*}
$$

natural in A, B, C and satisfying the coherence laws of a symmetric monoidal category.

From this and the lifting operation introduced above, we prove:

**Proposition 8.1.10.** Consider the $\sim$-bifunctor $(- \parallel -)$ along with the empty tcg **1**, and

$$
\begin{align*}
\rho_A & : \quad A \parallel \mathbf{1} \to A \\
\lambda_A & : \quad \mathbf{1} \parallel A \to A \\
\alpha_{A,B,C} & : \quad (A \parallel B) \parallel C \to A \parallel (B \parallel C) \\
s_{A,B} & : \quad A \parallel B \to B \parallel A
\end{align*}
$$

defined with $\rho_A = \mathfrak{c}_{\rho_A}$, $\lambda_A = \mathfrak{c}_{\lambda_A}$, $\alpha_{A,B,C} = \mathfrak{c}_{\alpha_{A,B,C}}$ and $s_{A,B} = \mathfrak{c}_{s_{A,B}}$.

This data makes TCG a symmetric monoidal $\sim$-category.

*Proof.* The bifunctor is constructed in Proposition 8.1.4. The coherence laws follow from the symmetric monoidal structure of Ren along with Proposition 8.1.9.

It remains to establish naturality, which is now relatively direct. We detail naturality of $s_{A,B}$ for illustration purposes: take $\sigma : A \vdash A'$ and $\tau : B \vdash B'$. Observe

$$
s_{A',B'} \cdot (\boldsymbol{\sigma} \parallel \boldsymbol{\tau}) \approx (\boldsymbol{\tau} \parallel \boldsymbol{\sigma}) \cdot s_{A,B}^{\perp} \quad (8.1)
$$

as follows directly by Corollary 7.2.13 applied to the obvious isomorphisms $\mathscr{C}^+(\boldsymbol{\sigma} \parallel \boldsymbol{\tau}) \cong \mathscr{C}^+(\boldsymbol{\tau} \parallel \boldsymbol{\sigma})$ and $\mathscr{S}^+(\boldsymbol{\sigma} \parallel \boldsymbol{\tau}) \cong \mathscr{S}^+(\boldsymbol{\tau} \parallel \boldsymbol{\sigma})$. From that we calculate:

$$
\begin{align*}
s_{A',B'} \odot (\boldsymbol{\sigma} \parallel \boldsymbol{\tau}) &\approx s_{A',B'} \cdot (\boldsymbol{\sigma} \parallel \boldsymbol{\tau}) \\
&\approx (\boldsymbol{\tau} \parallel \boldsymbol{\sigma}) \cdot s_{A,B}^{\perp} \\
&\approx (\boldsymbol{\tau} \parallel \boldsymbol{\sigma}) \odot \mathfrak{a}_{s_{A,B}^{\perp}} \\
&\approx (\boldsymbol{\tau} \parallel \boldsymbol{\sigma}) \odot \mathfrak{c}_{s_{B,A}} \\
&\approx (\boldsymbol{\tau} \parallel \boldsymbol{\sigma}) \odot s_{B,A}
\end{align*}
$$

using Lemma 8.1.8, equation (8.1), Lemma 8.1.8 again, Proposition 8.1.9, and definition of $s_{A,B}$. All other naturality squares follow using the same route. $\square$

**Compact closed structure.** Briefly recall that a compact closed category *C* is a symmetric monoidal category where each object comes with a dual *A*\* and two morphisms

$$
\epsilon_A : A^* \otimes A \to 1 \qquad \eta_A : 1 \to A \otimes A^*,
$$
the *unit* and the *co-unit*, satisfying two equations (see Theorem 8.1.12). A compact closed category is automatically symmetric monoidal closed: the monoidal closure can be defined as $A \to B = A^* \otimes B$. While this structure is not adequate to directly interpret a programming language, it is the fundamental structure expected of an unpolarized category of games, and it will be helpful for further constructions.

In **TCG**, the dual of a game *A* is as expected $A^\perp$. The unit and co-unit are:

**Definition 8.1.11.** Consider *A* a tcg. The co-unit $\epsilon_A : A^\perp \parallel A \vdash 1$ and unit $\eta_A : 1 \vdash A \parallel A^\perp$, formed with ess respectively $\mathfrak{c}_{A^\perp}$ and $\mathfrak{c}_A$ with display maps respectively

$$ \partial_{\epsilon_A} : \begin{array}{rcl} |\mathfrak{c}_{A^\perp}| & \to & |A^\perp| \parallel A \vdash 1| \\ (1, a) & \mapsto & (1, (1, a)) \\ (2, a) & \mapsto & (1, (2, a)), \end{array} $$

$$ \partial_{\eta_A} : \begin{array}{rcl} |\mathfrak{c}_A| & \to & |1 \vdash A| \parallel A^\perp| \\ (1, a) & \mapsto & (2, (1, a)) \\ (2, a) & \mapsto & (2, (2, a)) \end{array} $$

are valid strategies.

Altogether, this provides the data for the following theorem:

**Theorem 8.1.12.** TCG is a compact closed $\sim$-category.

*Proof.* It remains to prove the two duality conditions:

$$ \begin{align*} \mathfrak{c}_A &\approx \rho_A \odot (\mathfrak{c}_A \parallel \epsilon_A) \odot \alpha_{A,A^\perp,A} \odot (\eta_A \parallel \mathfrak{c}_A) \odot \lambda_A^{-1} \\ \mathfrak{c}_{A^\perp} &\approx \lambda_{A^\perp} \odot (\epsilon_A \parallel \mathfrak{c}_{A^\perp}) \odot \alpha_{A^\perp,A^\perp,A^\perp}^{-1} \odot (\mathfrak{c}_{A^\perp} \parallel \eta_{A^\perp}) \odot \rho_A^{-1} \end{align*} $$

which follow from Corollary 7.2.13 using Proposition 7.3.1, Lemmas 6.4.4 and 7.3.14 and the direct verification that all matching pairs involved are causally compatible. $\square$

As a compact closed $\sim$-category, **TCG** is a model of MLL and hence of the linear $\lambda$-calculus. But not more: like Conway games, **TCG** has neither products nor coproducts (as analysed by Melliès [Melliès, 2004b]). It also does not support the resource modality ! of Definition 7.1.26, which was defined on *negative* tcgs.

This missing structure may be recovered by switching to a *polarized* category of games: here *negative* games, where Opponent always starts (see Definition 7.1.24).

## 8.2 Negative Winning Games

As mentioned earlier, in order to obtain the categorical structure required to interpret programming language, one must commit to either *negative* games (which have products but no coproducts); or *positive* games (which have coproducts but no products). A pleasant feature of game semantics is that this choice reflects the evaluation order that one wishes to represent: call-by-name languages are naturally interpreted in categories of negative games, while call-by-value languages are interpreted in categories of positive games [Honda and Yoshida, 1999]. Here, we focus on negative games.
**Winning games.** We also introduce another condition: winning games and strategies. This mechanism, adapted from [Melliès, 2005, Melliès and Tabareau, 2007], has two purposes: (1) it compensates the inherently affine nature of game semantics, tightening the connections with relational-like semantics (see Section 10.4); and (2) it replaces the traditional but often bulky notion of *well-bracketing* in banning control operators like call/cc. We wire this into our ambient game semantics. We call this *winning* as it sets as common objective for both players to reach a winning position with as many Player as Opponent moves – and where intuitively speaking, all questions have an answer.

**Relative Seely categories.** Here, a reader familiar with categorical models of linear logic might expect us to construct a *Seely category*, a categorical model of intuitionistic linear logic [Melliès, 2009]. One can indeed construct a Seely category of thin concurrent games [Castellan and Clairambault, 2021]. But that construction is slightly unpleasant due to types such as $o \to (o \otimes o)$, i.e. tensors appearing on the right hand side of an arrow, which do not appear in our languages<fnref n="1" />. Worse, this construction breaks the clean connection with the relational model. So we shall aim for a slightly weaker categorical structure called a *relative Seely category*, which slightly restricts the monoidal closure, banning in particular tensors on the right of an arrow. Like Seely categories, relative Seely categories still enjoy that the Kleisli category for ! is cartesian closed.

### 8.2.1 Relative Seely categories

Though that is a detour in our game-theoretic narrative, we must first define what we mean by relative Seely categories. Relative Seely categories model the fragment of intuitionistic linear logic with formulas those generated by the grammar

$$S, T ::= \top | S \& T | A \to S$$

$$A, B ::= 1 | A \otimes B | S | !S$$

splitting formulas into *strict* $S, T$ and *general* $A, B$ formulas. Note that this covers all formulas involved in Girard's call-by-name translation for types.

In the following definition, we make use of the standard notions of relative adjunctions and relative comonads. For the reader unfamiliar with these, the definition also contains explicit data. For full details, see Appendix A.

**Definition 8.2.1.** *A relative Seely category is a symmetric monoidal category (C, ⊗, 1) equipped with a full subcategory C<sub>s</sub> together with the following data and axioms:*

* $C_s$ has finite products ($\&$, $\top$) preserved by the inclusion functor $J : C_s \hookrightarrow C$.

* For every $B \in C$ there is a functor $B \to - : C_s \to C_s$, such that there is

$$\Lambda(-) : C(A \otimes B, S) \cong C(A, B \to S).$$

a bijection natural in $A \in C$ and $S \in C_s$.

<footnote n="1">¹This triggers a duplication of the $o$ on the left with conflict between the two copies. Monoidal closure works, but with a cumbersome technical overhead that we prefer to avoid here. Note that *products* on the right hand side of an arrow are fine; indeed we shall eventually form a cartesian closed Kleisli category.</footnote>
* There is a J-relative comonad $! : C_s \to C$ : we have, for every $S \in C_s$, an object $!S \in C$ and a dereliction morphism $\text{der}_S : !S \to S$, and for every $\sigma : !S \to T$, a promotion $\sigma' : !S \to !T$, subject to three axioms [Altenkirch et al., 2010]:

$$
\begin{align*}
\text{der}_T \circ \sigma' &= \sigma && (\sigma : !S \to T) \\
\text{der}_S' &= \text{id}_{S} && (S \in C_s) \\
(\tau \circ \sigma')' &= \tau' \circ \sigma' && (\sigma : !S \to T, \tau : T \to U),
\end{align*}
$$

which make $! : C_s \to C$ a functor, via $!\sigma = (\sigma \circ \text{der}_S)'$ for $\sigma : S \to T$.

* The functor $! : C_s \to C$ is symmetric strong monoidal $(C_s, \& , \top) \to (C, \otimes , 1)$, so

$$
m_0 : 1 \to !\top \qquad m_{S,T} : !S \otimes !T \to !(S\&T)
$$

are natural isos, additional compatible with promotion: the diagram

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

commutes for all $\Gamma$, $S$, $T \in C_s$, $f \in C(\Gamma, S)$, $g \in C(\Gamma, T)$.

Note any Seely category is canonically a relative Seely category with $C = C_s$. For any
relative Seely category, the Kleisli category associated with $!$, denoted $C_!$, is cartesian
closed: it has objects those of $C_s$, and $C_!(S, T) = C(!S, T)$.

**Lemma 8.2.2.** For a relative Seely category *C*, the Kleisli category *C*₁ is cartesian closed with finite products given as in *C*₅, and function space *S* ⇒ *T* = !*S* → ∞*T*.

*Proof.* The proof is essentially as for Seely categories; see Appendix A.1. $\square$

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

For **TCG** these definitions must of course be taken in $\sim$-categorical form: as before this means that all operations preserve $\sim$, and all conditions hold up to $\sim$; yielding a notion of **relative Seely $\sim$-category**. We omit the straightforward adaptation.

We now start building the concrete relative Seely $\sim$-category NTCG.

**8.2.2 Playing Board Games**

Objects of **NTCG** are certain negative tcgs, equipped with an additional component $\kappa$, a
so-called *payoff function* expressing the *winning conditions*. More precisely, $\kappa$ records
which configurations are complete and assigns responsibility of non-completeness to
one of the players otherwise. The resulting object will be the main notion of game used
in the rest of this monograph, so we need a distinctive name that remains “gamey”:
**Boards.** We now give the full definition of the objects of NTCG:

**Definition 8.2.3.** A board is a tcg A along with $\kappa_A : \mathscr{C}(A) \to \{-1, 0, +1\}$ a payoff function, such that this data satisfies the following conditions:

invariant: for all $\theta: x \cong_A y$, we have $\kappa_A(x) = \kappa_A(y)$,

race-free: for all $a \sim_A a'$, we have $\text{pol}_A(a) = \text{pol}_A(a')$.

forestial: for all $a_1, a_2, a \in A$, if $a_1, a_2 \le_A a$, then $a_1 \le_A a_2$ or $a_2 \le_A a_1$,

alternating: for all $a_1, a_2 \in A$, if $a_1 \to_A a_2$, then $\text{pol}_A(a_1) \neq \text{pol}_A(a_2)$,

A **--board** is additionally negative, and must also satisfy:

$$ \text{initialized: } \kappa_A(\emptyset) \ge 0. $$

Finally, a **--board** A is **strict** if $\kappa_A(\emptyset) = 1$ and all its initial moves are in pairwise conflict. It is **well-opened** if it is strict with exactly one initial move.

The payoff function $\kappa_A$ assigns a value to each configuration. Configurations with payoff 0 are called complete: they correspond to terminated executions, which have reached an adequate stopping point where in particular all calls have adequately returned. Otherwise, $\kappa_A$ assigns a responsibility for why a configuration is non-complete. If $\kappa_A(x) = -1$ then Player is responsible, otherwise it is Opponent.

**Basic --boards.** It seems natural to introduce first the boards for PCF base types.

Recall that in Figures 7.7, 7.8 and 7.9 we introduced tcgs U, B and N respectively for the unit type, booleans and natural numbers. These three tcgs are turned into boards by adjoining them a payoff function which, for all three, is defined similarly by

$$ \begin{align*} \kappa(\emptyset) &= 1 \\ \kappa(\{\mathbf{q}^{-}\}) &= -1 \\ \kappa(\{\mathbf{q}^{-}, a^{+}\}) &= 0 \end{align*} $$

which is exhaustive as maximal configurations have only two elements.

We keep the notations U, B and N for these boards. They are *strict*: the payoff function essentially *forces* Opponent to ask the initial question. In these three basic boards, maximal configurations have null payoff – as mentioned earlier, we call those *complete*:

**Definition 8.2.4.** Consider A a board, and $x \in \mathscr{C}(A)$.

We say that $x$ is **complete** iff $\kappa_A(x) = 0$, and write $x \in \mathscr{C}^0(A)$.

*Complete* configurations are intuitively those where every call is answered, in that they reflect the complete plays of traditional game semantics (see Definition 3.3.6). They shall also inform the link with relational semantics: this will be detailed in Section 10.4, but note already that $\mathscr{C}^0(\text{U})$, $\mathscr{C}^0(\text{B})$ and $\mathscr{C}^0(\text{N})$ are in bijection with the usual relational model interpretation of the corresponding types.

The other basic **--boards** are the units. In the presence of the payoff function the empty tcg **1** splits into two units, reflecting the units of multiplicative and additive con-junctions in linear logic: the **top** $\vdash$ has $\kappa_\vdash(\emptyset) = 1$, while the **one** **1** has $\kappa_1(\emptyset) = 0$ – we overload the notation for the empty tcg **1**, which should not cause any confusion.
<table><caption>Figure 8.1: Payoff for $\otimes$ and $\#\mathfrak{A}$</caption><thead><tr><th>&otimes;</th><th>-1</th><th>0</th><th>+1</th></tr></thead><tbody><tr><th>-1</th><td>-1</td><td>-1</td><td>-1</td></tr><tr><th>0</th><td>-1</td><td>0</td><td>+1</td></tr><tr><th>+1</th><td>-1</td><td>+1</td><td>+1</td></tr></tbody></table><table><thead><tr><th>&#x2610;</th><th>-1</th><th>0</th><th>+1</th></tr></thead><tbody><tr><th>-1</th><td>-1</td><td>-1</td><td>+1</td></tr><tr><th>0</th><td>-1</td><td>0</td><td>+1</td></tr><tr><th>+1</th><td>+1</td><td>+1</td><td>+1</td></tr></tbody></table>

**Dual, tensor and par.** First, the **dual** (Definition 7.1.23) extends with payoff via $\kappa_{A^{\perp}}(x) = -\kappa_{A}(x)$ as expected. Of course, the dual does not preserve $\neg$-boards.

Like the units, *parallel composition* splits into two:

**Definition 8.2.5.** Consider A and B two boards.

Their tensor $A \otimes B$ and their par $A \# B$ are $A \parallel B$ enriched with:

$$ \kappa_{A \otimes B}(x_A \parallel x_B) = \kappa_A(x_A) \otimes \kappa_B(x_B), \quad \kappa_{A \# B}(x_A \parallel x_B) = \kappa_A(x_A) \# \kappa_B(x_B) $$

with the operations $\otimes$ and $\#\mathfrak{A}$ defined on $\{-1, 0, +1\}$ in Figure 8.1.

The tensor of two $\neg$-boards is still a $\neg$-board, though tensor does not preserve *strict* $\neg$-boards. The par also preserves $\neg$-boards, but we shall not use it on $\neg$-boards: if $A$ and $B$ are $\neg$-boards, let us use $A \vdash B$ to denote the board $A^{\perp} \#\mathfrak{A} B$ used to define the strategies from $A$ to $B$. Observe that even if $A$ and $B$ are $\neg$-boards, $A \vdash B$ is not.

**The with.** We only consider the additive conjunction of linear logic: the with. But in order to define it, we must first define a new operation of ess and tcgs.

**Definition 8.2.6.** Let $A_1$ and $A_2$ be two tcgs.

Then, we define their **sum** $A_1 + A_2$ as comprising the components:

$$ \begin{array}{l@{\qquad}l} \text{events:} & |A_1 \parallel A_2| = |A_1| + |A_2| \\ \text{causality:} & (i, a) \le_{A_1 \parallel A_2} (j, a') \Leftrightarrow i = j \ \& \ a \le_{A_1} a' \\ \text{conflict:} & (i, a) \#_{A_1 \parallel A_2} (j, a') \Leftrightarrow i \neq j \ \& \ a \#_{E_i} a', \\ \text{symmetry:} & \theta \in \mathcal{S}(A_1 \parallel A_2) \Leftrightarrow \exists \theta_i \in \mathcal{S}(A_i), \theta = \theta_1 \parallel \theta_2, \\ \text{positive symmetries:} & \theta_1 \parallel \theta_2 \in \mathcal{S}_+(A_1 + A_2) \Leftrightarrow \theta_1 \in \mathcal{S}_+(A_1) \ \& \ \theta_2 \in \mathcal{S}_+(A_2) \\ \text{negative symmetries:} & \theta_1 \parallel \theta_2 \in \mathcal{S}_-(A_1 + A_2) \Leftrightarrow \theta_1 \in \mathcal{S}_-(A_1) \ \& \ \theta_2 \in \mathcal{S}_-(A_2). \end{array} $$

where, necessarily, one of $\theta_1$ or $\theta_2$ must be empty.

Ignoring the positive and negative symmetries, this also yields an operation $+$ on plain event structures with symmetry that we shall use later on.

If $A, B$ are tcgs and $x_A \in \mathcal{C}(A)$, we write $(1, x_A) \in \mathcal{C}(A + B)$ as a shorthand for $\{1\} \times x_A$ and likewise for $(2, x_B) = \{2\} \times x_B \in \mathcal{C}(A + B)$ for $x_B \in \mathcal{C}(B)$. Note that all configurations of $A+B$ have the form $(1, x_A)$ for $x_A \in \mathcal{C}(A)$ or $(2, x_B)$ for $x_B \in \mathcal{C}(B)$. For non-empty configurations, this decomposition is *unique*. We shall also use the corresponding notations for symmetries, with e.g. $(1, \theta_A) : (1, x_A) \cong_{A+B} (1, y_A)$ for $\theta_A : x_A \cong_A y_A$ comprising all $((1, a), (1, a'))$ for $(a, a') \in \theta_A$.
This sum operation yields the with operation on strict boards:

**Definition 8.2.7.** Consider A and B two strict --boards.
Then, their with A&B is the strict --board with tcg the sum A + B and

$$ \kappa_{A\&B}(1, x_A) = \kappa_A(x_A), \quad \kappa_{A\&B}(2, x_B) = \kappa_B(x_B), $$

for non-empty configurations and $\kappa_{A\&B}(\emptyset) = 1$.

As we will see, this construction will give a cartesian product in the subcategory of strict --boards. It can also be applied to non-strict --boards, but then it is not a product: if one of the $A_i$ is not strict then the corresponding projection does not respect payoff (in the sense of Definition 8.2.14), because we have set $\kappa_{A_1\&A_2}(\emptyset) = 1$. On the other hand having $\kappa_{A_1\&A_2}(\emptyset) = 0$ breaks the correspondence with the relational model, since the empty configuration does not correspond in a canonical way to one of the components.

In the sequel, we should use the obvious n-ary generalization of the product, with respect to which any strict --board decomposes into a with of well-opened --boards:

**Lemma 8.2.8.** Consider A a strict --board. Then there is a family $(A_i)_{i \in I}$ of well-opened --boards, unique up to isomorphism, such that $A \cong \&_{i \in I} A_i$.

*Proof.* Straightforward. $\square$

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

We need notations for configurations of this board. Writing $\mathcal{C}^{\neq\emptyset}(A)$ (resp. $\mathcal{S}^{\neq\emptyset}(A)$) for the set of non-empty configurations (resp. symmetries) of A, we observe:

**Lemma 8.2.9.** Consider $(A_i)_{i \in I}$ a family of well-opened --boards. Then there are

$$ \begin{align*} \mathcal{C}^{\neq\emptyset}(\&_{i \in I} A_i) &\cong \sum_{i \in I} \mathcal{C}^{\neq\emptyset}(A_i) \\ \mathcal{S}^{\neq\emptyset}(\&_{i \in I} A_i) &\cong \sum_{i \in I} \mathcal{S}^{\neq\emptyset}(A_i) \\ \mathcal{S}_{-}^{\neq\emptyset}(\&_{i \in I} A_i) &\cong \sum_{i \in I} \mathcal{S}_{-}^{\neq\emptyset}(A_i) \\ \mathcal{S}_{+}^{\neq\emptyset}(\&_{i \in I} A_i) &\cong \sum_{i \in I} \mathcal{S}_{+}^{\neq\emptyset}(A_i) \end{align*} $$

order-isos commuting with dom and cod.

*Proof.* Straightforward. $\square$

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

For $x \in \mathcal{C}^{\neq\emptyset}(A_i)$ (resp. $\theta \in \mathcal{S}^{\neq\emptyset}(A_i)$) we write $(i, x) \in \mathcal{C}^{\neq\emptyset}(\&_{i \in I} A_i)$ (resp. $(i, \theta) \in \mathcal{S}^{\neq\emptyset}(\&_{i \in I} A_i)$). The final linear connective we shall consider is the linear arrow:

**Linear arrow.** First, we define it in the case the rhs board is well-opened:

**Definition 8.2.10.** Consider A a --board and B a well-opened --board.
Then, $A \to B$ has tcg as defined in Definition 7.1.25, and payoff function:

$$ \kappa_{A \to B}(x_A \parallel x_B) = \kappa_{A \to B}(x_A \parallel x_B) = \kappa_{A \perp}(x_A) \mathcal{Y} \kappa_B(x_B). $$
<figure><img src="image_120.png" /><figcaption>Figure 8.2: The board $U \to (U\&U)$</figcaption></figure>

The definition of relative Seely categories requires us to define $A \to B$ not only when $B$ is well-opened (which has no particular status in the definition of relative Seely categories), but when it is strict. In that case, $A \to B$ may be defined directly via the decomposition of Lemma 8.2.8, as done in the following definition:

**Definition 8.2.11.** Consider $A$ a $--board$, and $B$ a strict $--board$, with $B \cong \&_{i \in I} B_i$. Then, we define $A \to B = \&_{i \in I} A \to B_i$.

The construction is illustrated in Figure 8.2.2, in which we omit payoff. The construction duplicates the argument arena, with one copy for each initial move of $B$. In that, the reader familiar with Hyland-Ong games – or the attentive reader of Part I) will recognize its arrow arena construction (modulo the conflict, see e.g. Figure 4.1).

It will be useful to have the analogue of Lemma 8.2.9 for the linear arrow:

**Lemma 8.2.12.** Consider $A, B$ $--boards$ with $B$ strict. Then, there are:

$$ \begin{align*} \mathscr{C}^{\neq\emptyset}(A \to B) &\cong \mathscr{C}(A) \times \mathscr{C}^{\neq\emptyset}(B) \\ \mathscr{S}^{\neq\emptyset}(A \to B) &\cong \mathscr{S}(A) \times \mathscr{S}^{\neq\emptyset}(B) \\ \mathscr{S}^{\neq\emptyset}(A \to B) &\cong \mathscr{S}_+(A) \times \mathscr{S}^{\neq\emptyset}(B) \\ \mathscr{S}_+^{\neq\emptyset}(A \to B) &\cong \mathscr{S}_-(A) \times \mathscr{S}_+^{\neq\emptyset}(B) \end{align*} $$

order-isos commuting with dom and cod.

*Proof.* If $B$ is well-opened, then $\mathscr{C}^{\neq\emptyset}(A \to B) \cong \mathscr{C}(A) \times \mathscr{C}^{\neq\emptyset}(B)$ is obvious. Now if $B \cong \sum_{i \in I} B_i$ via Lemma 8.2.8, we compose bijections:

$$ \begin{align*} \mathscr{C}^{\neq\emptyset}(A \to B) &\cong \sum_{i \in I} \mathscr{C}^{\neq\emptyset}(A \to B_i) \\ &\cong \sum_{i \in I} \mathscr{C}(A) \times \mathscr{C}^{\neq\emptyset}(B_i) \\ &\cong \mathscr{C}(A) \times (\sum_{i \in I} \mathscr{C}^{\neq\emptyset}(B_i)) \\ &\cong \mathscr{C}(A) \times \mathscr{C}^{\neq\emptyset}(B) \end{align*} $$

using Lemma 8.2.9, the well-opened case, distributivity, followed by Lemma 8.2.9 again. The same construction applies to symmetries in a compatible way. $\square$
Following this lemma, we adopt the convention that for each $x_A \in \mathscr{C}(A)$ and $x_B \in \mathscr{C}^\neq\emptyset(B)$, $x_A \rightsquigarrow x_B \in \mathscr{C}^\neq\emptyset(A \rightsquigarrow B)$ denotes the corresponding configuration.

**Bang.** The next definition enriches Definition 7.1.26 with payoff:

**Definition 8.2.13.** Consider A a --board.

Then, !A has tcg as in Definition 7.1.26 enriched with:

$$ \kappa_{!A}(\|_{i \in I} x_i) = \bigotimes_{i \in I} \kappa_A(x_i) \quad (I \subseteq \mathbb{N}, \forall i \in I, x_i \neq \emptyset) \\ \kappa_{!A}(\emptyset) = 0 $$

$$ \text{where } \|_{i \in I} x_i = \bigcup_{i \in I} (\{i\} \times x_i). $$

So the payoff for the bang acts as a *n*-ary tensor for the non-empty components, while the empty configuration gets assigned payoff zero. This means that it is considered *complete*: a complete execution might not initiate any of the copies; but a copy initiated must be brought to a complete state if the whole computation is to be complete.

A pleasing consequence of this definition is that if A is strict, then the symmetry classes of complete configurations of !A are in one-to-one correspondence with finite multisets of symmetry classes of complete configurations of A, informing the link with the relational model – again, see Section 10.4 for more details.

## 8.2.3 Negative Winning Strategies

**Winning strategies.** First, we define what it means for a strategy to be well-behaved with respect to payoff. Recall that this has two effects: it compensates for the inherently affine nature of strategies, and it also replaces the traditional well-bracketing condition.

Intuitively, a strategy is *winning* when its stopping points are complete, or the incompleteness can be attributed – via the payoff function – to Opponent:

**Definition 8.2.14.** Consider A a board, and $\sigma$: A a strategy. We define conditions:

negative: for all $s \in \sigma$ minimal for $\leq_{\sigma}$, we have $\text{pol}_A(\partial_{\sigma} s) = -$,

winning: for all $x^{\sigma} \in \mathscr{C}^{+}(\sigma)$, $\kappa_A(\partial_{\sigma} x^{\sigma}) \geq 0$.

Negative means that Opponent always starts, also in strategies. Winning forces $\sigma$ to be strictly linear rather than affine, i.e. it must investigate arguments not marked with a !. For instance, the strategy displayed in Figure 8.3 is non-winning: as U is strict, the fact that the strategy does not investigate its argument is punished by a payoff of -1 on the left, yielding a global payoff of -1 $\mathfrak{P} 0 = -1$ for the maximal configuration.

This definition also ensures a measure of well-bracketing, though it may not be obvious to the reader. Conceptually, Melliès and Tabareau's insight is that well-bracketing is a linearity constraint [Melliès and Tabareau, 2007]: in a well-bracketed completed (in the sense that the initial question receives an answer) execution, each question receives exactly one answer. Still, it might be helpful to examine a concrete example of how typically non-well-bracketed behaviour in the traditional sense is banned. Such an
<figure><img src="image_121.png" /><figcaption>Figure 8.3: An affine non-winning strategy</figcaption></figure>

<figure><img src="image_122.png" /><figcaption>Figure 8.4: A non-winning strategy</figcaption></figure>

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

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

example appears in Figure 8.4: the configuration without the gray event is +-covered. Its payoff is $(-1 \otimes +1) \mathfrak{N} 0 = -1$, where the $-1$ is the price of Player omitting to answer the “pending” left-most question. But this is actually quite subtle and one should not attempt to match this notion of well-bracketing with the traditional ones. In particular, the same causal pattern may very well appear in a winning strategy: for instance, we invite the reader to verify that the strategy in Figure 7.6 (on the left) is winning.

We obtain a ~-category of --boards and negative winning strategies:

**Proposition 8.2.15.** There is NTCG, a ~-category with --boards as objects, negative winning strategies on $A \vdash B$ as morphisms from $A$ to $B$, and $\approx$ as equivalence.

*Proof.* Copycat. Negative is immediate by inspection of Definition 6.4.1. For winning, consider $x_A \parallel x_A \in \mathscr{C}^+(w_A)$ exploiting Lemma 6.4.4. Then, $\kappa_{A \vdash A}(x_A \parallel x_A) = -p \mathfrak{N} p$ for $p = \kappa_A(x_A)$, and for all $p \in \{-1, 0, +1\}$, $-p \mathfrak{N} p \ge 0$ as required.

*Composition.* For negative, assume w.l.o.g. that there is $p \in \tau \odot \sigma$ minimal positive. In particular, $x^\tau \odot x^\sigma = \{p\} \in \mathscr{C}^+(\tau \odot \sigma)$. Now $p$ cannot occur in $C$, as minimal events in $C$ are negative, so it must occur in $A$. That means $x^\sigma \in \mathscr{C}^+(\sigma)$ is non-empty. As $\sigma$ is negative, there is a minimal (necessarily) negative event in $x^\sigma$, which must occur in $B$. As $x^\sigma$ and $x^\tau$ are matching, $x^\tau$ is non-empty as well. By negative, there is a minimal (necessarily) negative event in $x^\tau$, which must occur in $C$. But as $\partial_{\tau \odot \sigma}(x^\tau \odot x^\sigma) = x_A^\sigma \parallel x_C^\tau$, $x^\tau \odot x^\sigma$ must have an event occurring in $C$, absurd.

For winning, consider $x^\tau \odot x^\sigma \in \mathscr{C}^+(\tau \odot \sigma)$, with $\partial_{\tau \odot \sigma}(x^\tau \odot x^\sigma) = x_A^\sigma \parallel x_C^\tau$. If $\kappa_A(x_A^\sigma) = -1$, then $\kappa_{A \vdash C}(x_A^\sigma \parallel x_C^\tau) = 1$ and we are done. Likewise if $\kappa_C(x_C^\tau) = 1$, we are done, so assume neither. Now if $\kappa_A(x_A^\sigma) = 1$, as $\sigma$ is winning we must have $\kappa_B(x_B^\sigma) = \kappa_B(x_B^\tau) = 1$ as well; and as $\tau$ is winning this entails $\kappa_C(x_C^\tau) = 1$, absurd. Symmetrically, $\kappa_C(x_C^\tau) = -1$ entails $\kappa_A(x_A^\sigma) = -1$, absurd. The only case left has $\kappa_A(x_A^\sigma) = \kappa_C(x_C^\tau) = 0$, so that $\kappa_{A \vdash C}(x_A^\sigma \parallel x_C^\tau) = 0 \ge 0$ as required. $\square$

The properties of the equivalence relation $\approx$ packaged in Proposition 7.4.15 are undis-
turbed by these now conditions and apply transparently.

**8.2.4 Symmetric Monoidal Structure**

We now extend the symmetric monoidal structure.
**Tensor.** First, we extend the tensor of strategies:

**Proposition 8.2.16.** *The tensor operation of Definition 8.2.5 yields a $\sim$-bifunctor:*

$$(- \otimes -) : \mathbf{NTCG} \times \mathbf{NTCG} \to \mathbf{NTCG}.$$

*Proof.* Consider $\sigma : A \vdash B$, $\tau : C \vdash D$, their tensor $\sigma \otimes \tau$ is defined on strategies as in Proposition 8.1.1. We must check that this preserves *negative* and *winning*.

*Negative.* Consider $m \in \sigma \parallel \tau$ minimal. Seeking a contradiction, assume $m$ is positive, so $\{m\}$ is $+-$covered. By Proposition 8.1.1, $\{m\}$ may be written as $x^\sigma \parallel x^\tau \in \mathscr{C}^+(\sigma \otimes \tau)$. As $\partial_{\sigma \otimes \tau}(m) \in A \otimes C \vdash B \otimes D$, $m$ occurs in one of the four components. Say w.l.o.g. that it is in $A$ or $B$, then $x^\sigma$ must be a singleton. But as $\sigma$ is negative, $\partial_\sigma x^\sigma$ is a singleton whose only event is negative in $A \vdash B$. By the constraints on display maps given by Proposition 8.1.1, it follows that $m$ is negative, contradiction.

*Winning.* Consider $x^\sigma \parallel x^\tau \in \mathscr{C}^+(\sigma \otimes \tau)$. If $\kappa_A(x_A^\sigma) = -1$ or $\kappa_C(x_C^\tau) = -1$, then we are done. As $\sigma$ and $\tau$ are winning, this directly entails that we cannot have $\kappa_B(x_B^\sigma) = -1$ or $\kappa_D(x_D^\tau) = -1$ either, so $\kappa_B(x_B^\sigma)$, $\kappa_D(x_D^\tau) \ge 0$. Now, assume $\kappa_{A \otimes C}(x_A^\sigma \parallel x_C^\tau) = 1$. If $\kappa_A(x_A^\sigma) = 1$, then as $\sigma$ is winning we have $\kappa_B(x_B^\sigma) = 1$. But as $\kappa_D(x_D^\tau) \ge 0$, $\kappa_{B \otimes D}(x_B^\sigma \parallel x_D^\tau) = 1$ and we are done. Likewise if $\kappa_C(x_C^\tau) = 1$, we may conclude. $\square$

**Lifting.** The monoidal structure shall be obtained following Section 8.1.2, by lifting maps. However, we must first define those renamings that yield winning strategies.

**Definition 8.2.17.** *Consider A, B two boards, and $f : A \to B$ a renaming.*

*We say that $f$ is winning if for all $x_A \in \mathscr{C}(A)$, $\kappa_B(f(x_A)) \ge \kappa_A(x_A)$.*

As expected, winning renamings preserve winning strategies:

**Lemma 8.2.18.** *Consider winning renamings $f : A^\perp \to A'^\perp$ and $g : B \to B'$. Then, $g \cdot \sigma \cdot f : A' \vdash B'$ is winning.*

*Proof.* Consider $x^\sigma \in \mathscr{C}^+(\sigma)$. If $\kappa_{A'}(f(x_A^\sigma)) = -1$ or $\kappa_{B'}(g(x_B^\sigma)) = 1$ then we are done, so assume otherwise. If $\kappa_{A'}(f(x_A^\sigma)) = 1$, then $\kappa_{A'\perp}(f(x_A^\sigma)) = -1$, but since $f$ is winning, we have $\kappa_{A'\perp}(f(x_A^\sigma)) \ge \kappa_{A\perp}(x_A^\sigma)$ so $\kappa_{A\perp}(x_A^\sigma) = -1$ as well. Now since $\sigma$ is winning, this entails $\kappa_B(x_B^\sigma) = 1$. But then $\kappa_{B'}(g(x_B^\sigma)) \ge \kappa_B(x_B^\sigma)$ as $g$ is winning, so $\kappa_{B'}(g(x_B^\sigma)) = 1$, contradiction. Symmetrically, if $\kappa_{B'}(g(x_B^\sigma)) = -1$, this entails $\kappa_{A'}(f(x_A^\sigma)) = -1$ as $f$, $\sigma$ and $g$ are winning, contradiction. $\square$

It follows directly that we may lift winning renamings to strategies:

**Corollary 8.2.19.** *Consider $f : A \to B$ a winning renaming. Then,*

(1) $\mathfrak{c}_f : A \vdash B$ is a negative, winning strategy,

(2) $\mathfrak{d}_f : B^\perp \vdash A^\perp$ is a negative, winning strategy.

*Proof.* Immediate by Lemma 8.2.18. $\square$

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

And finally, we deduce the symmetric monoidal structure:
**Proposition 8.2.20.** *Proposition 8.2.16 along with the data of Proposition 8.1.10 makes NTCG a symmetric monoidal ~-category.*

*Proof.* Direct from Propositions 8.2.16, 8.1.10 and Corollary 8.2.19. □

## 8.2.5 Cartesian Product of Strict --Boards

Next, we must define the cartesian structure. Recall from the definition of relative Seely categories (Definition 8.2.1) that the cartesian product is not required to be defined on the whole category, but only on a full subcategory $C_s$. Here, we will consider the full $\sim$-subcategory $NTCG_s$ with as objects the strict --boards.

**Projections.** First, we define the projections. First we need renamings:

**Lemma 8.2.21.** *Consider A, B strict --boards. The injections $\iota_A : A^{\perp} \to (A\&B)^{\perp}$, $\iota_B : B^{\perp} \to (A\&B)^{\perp}$ are winning renamings.*

*Proof.* Immediate verification. □

The above lets us define the projections via lifting:

$$ \pi_A = \mathfrak{a}_{\iota_A} : A \& B \vdash A, \quad \pi_B = \mathfrak{a}_{\iota_B} : A \& B \vdash B $$

winning negative strategies by Corollary 8.2.19.

**Pairing.** As for earlier constructions, we build pairing via a universal construction:

**Proposition 8.2.22.** *For --boards $\Gamma$, A, B, with A, B strict, and negative winning strategies $\sigma : \Gamma \vdash A, \tau : \Gamma \vdash B$, there is a negative winning strategy $\langle \sigma, \tau \rangle : \Gamma \vdash A \& B$, unique up to iso, s.t. there are order-isos:*

$$ \mathcal{C}^{+}(\sigma) + \mathcal{C}^{+}(\tau) \approx \mathcal{C}^{+}(\langle \sigma, \tau \rangle) $$

$$ \mathcal{S}^{+}(\sigma) + \mathcal{S}^{+}(\tau) \approx \mathcal{S}^{+}(\langle \sigma, \tau \rangle) $$

commuting with dom, cod, and such that for all $\theta^\sigma \in \mathcal{S}^+(\sigma)$ and $\theta^\tau \in \mathcal{S}^+(\tau)$, we have

$$ \partial_{\langle\sigma, \tau\rangle}(\iota_{\sigma}(\theta^{\sigma})) = \theta_{\Gamma}^{\sigma} \parallel (\theta_{A}^{\sigma} \parallel \emptyset), \quad \partial_{\langle\sigma, \tau\rangle}(\iota_{\tau}(\theta^{\tau})) = \theta_{\Gamma}^{\tau} \parallel (\emptyset \parallel \theta_{B}^{\tau}) $$

with $\iota_\sigma : \mathcal{C}^+(\sigma) \to \mathcal{C}^+((\sigma, \tau))$ and $\iota_\tau : \mathcal{C}^+(\tau) \to \mathcal{C}^+((\sigma, \tau))$ the induced injections. Moreover, $\langle -, - \rangle$ preserves $\approx$.

*Proof. Existence.* We set $\langle \sigma, \tau \rangle$ as having as ess $\sigma + \tau$, with display maps given by

$$ \partial_{\langle\sigma, \tau\rangle}(\iota_{\sigma}(x^{\sigma})) = x_{\Gamma}^{\sigma} \vdash (1, x_{A}^{\sigma}) $$

$$ \partial_{\langle\sigma, \tau\rangle}(\iota_{\tau}(x^{\tau})) = x_{\Gamma}^{\tau} \vdash (2, x_{B}^{\tau}) $$

where $\partial_\sigma(x^\sigma) = x_\Gamma^\sigma \vdash x_A^\sigma$ and $\partial_\tau(x^\tau) = x_\Gamma^\tau \vdash x_B^\tau$; and likewise for symmetries. All required verifications are immediate, and this yields a negative winning strategy.

**Uniqueness.** Direct consequence of Corollary 7.2.13.

**Congruence.** Direct from the definition. □
We need one last lemma to conclude with the cartesian product:

**Lemma 8.2.23.** Consider $\Gamma$, $A$, $B$ --boards with $A$, $B$ strict, and $\alpha : \Gamma \vdash A \& B$. Then,

$$ \mathscr{C}^+(\pi_A \odot \alpha) \cong \{x^\alpha \in \mathscr{C}^+(\alpha) \mid \partial_\alpha x^\alpha = x_\Gamma^\alpha \vdash (1, x_A^\alpha)\} $$

$$ \mathscr{S}^+(\pi_A \odot \alpha) \cong \{\theta^\alpha \in \mathscr{S}^+(\alpha) \mid \partial_\alpha \theta^\alpha = \theta_\Gamma^\alpha \vdash (1, \theta_A^\alpha)\} $$

are order-isomorphisms compatible with display maps – and likewise for $\pi_B$.

*Proof.* A direct adaptation of the proof of Proposition 6.4.9. $\square$

**Proposition 8.2.24.** For any two strict --boards $A$ and $B$, $A \& B$ is a cartesian product of $A$ and $B$ in NTCG. Moreover, $\top$ is terminal.

*Proof.* We prove the universal property of cartesian products.

*Existence.* For $\sigma : \Gamma \vdash A$, $\tau : \Gamma \vdash B$ we form $\langle\sigma, \tau\rangle$ via Proposition 8.2.22. Then:

$$ \mathscr{C}^+(\pi_A \odot \langle\sigma, \tau\rangle) \cong \{x \in \mathscr{C}^+(\langle\sigma, \tau\rangle) \mid \partial x = x_\Gamma \vdash (1, x_A)\} $$

$$ \cong \mathscr{C}^+(\sigma) $$

using Lemma 8.2.23 followed by Proposition 8.2.22, and those order-isos preserve display maps. The same reasoning applies to symmetries, so that $\pi_A \odot \langle\sigma, \tau\rangle \approx \sigma$ by Corollary 7.2.13. Symmetrically, we have $\pi_B \odot \langle\sigma, \tau\rangle \approx \tau$ as well.

*Uniqueness.* Consider $\alpha : \Gamma \vdash A \& B$ such that $\pi_A \odot \alpha \approx \sigma$ and $\pi_B \odot \alpha \approx \tau$. First,

$$ \alpha \cong \langle \pi_A \odot \alpha, \pi_B \odot \alpha \rangle $$

follows from Lemma 8.2.23, uniqueness of Proposition 8.2.22 and immediate verifications. Finally, we have $\langle\pi_A \odot \alpha, \pi_B \odot \alpha\rangle \approx \langle\sigma, \tau\rangle$ as $\langle-, -\rangle$ preserves $\approx$.

*Terminal.* For any --board $\Gamma$, it is immediate that the empty strategy $\epsilon : \Gamma \vdash \top$ is a winning negative strategy. Moreover, given any $\alpha : \Gamma \vdash \top$ negative, any minimal event in $\alpha$ must be negative and hence map to an event in $\top$ – but there are none. $\square$

This concludes the investigation of cartesian products in NTCG.

## 8.2.6 Relative Closure

The final piece of the linear structure is the relative closure (see Definition 8.2.1). The main operation we must define is **currying** – as for the other operations, we characterize it uniquely up to isomorphism via its configurations.

**Proposition 8.2.25.** Consider $\Gamma$, $A$, $B$ --boards with $B$ strict.

For $\sigma : \Gamma \otimes A \vdash B$, there is $\Lambda(\sigma) : \Gamma \vdash A \dashv B$, unique up to iso, s.t. there are

$$ \Lambda(-) : \mathscr{C}^+(\sigma) \cong \mathscr{C}^+(\Lambda(\sigma)) $$

$$ \Lambda(-) : \mathscr{S}^+(\sigma) \cong \mathscr{S}^+(\Lambda(\sigma)) $$

order-isos commuting with dom, cod, and such that for all $\theta^\sigma$ non-empty,

$$ \partial_{\Lambda(\sigma)}(\Lambda(\theta^\sigma)) = \theta_\Gamma^\sigma \vdash \theta_A^\sigma \dashv \theta_B^\sigma \qquad (8.2) $$

$$ \text{whenever } \partial_\sigma(\theta^\sigma) = \theta_\Gamma^\sigma \parallel \theta_A^\sigma \vdash \theta_B^\sigma. $$

Moreover, $\Lambda(-)$ preserves $\approx$.
As usual, evaluation $ev_{A,B} : (A \to B) \otimes A \vdash B$ may be defined as

$$ev_{A,B} = \Lambda^{-1}(\mathfrak{c}_{A \to B})$$

the uncurrying of the identity, for A, B --boards with B strict. We have:

**Lemma 8.2.27.** Consider A, B --boards with B strict. Then,

$$\mathscr{C}^{\neq \emptyset, +}(ev_{A,B}) = \{\mathfrak{c}_{x_A \to x_B} | x_A \in \mathscr{C}(A), x_B \in \mathscr{C}^{\neq \emptyset}(A)\},$$

$$\mathscr{S}^{\neq \emptyset, +}(ev_{A,B}) = \{\mathfrak{c}_{\theta_A \to \theta_B} | \theta_A \in \mathscr{S}(A), \theta_B \in \mathscr{S}^{\neq \emptyset}(B)\}$$

with $\partial_{ev_{A,B}}(\mathfrak{c}_{x_A \to x_B}) = (x_A \to x_B) \parallel x_A \vdash x_B$ and idem for symmetries.

*Proof.* Direct from Lemmas 6.4.4, 7.3.14 and the definition of $\Lambda^{-1}(-)$. $\square$

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

Finally, uncurrying may be equivalently computed by composing with evaluation:

**Lemma 8.2.28.** Consider $\sigma : \Gamma \vdash A \to B$ a negative winning strategy.

$$\textit{Then, } \Lambda^{-1}(\sigma) \approx ev_{A,B} \odot (\sigma \otimes \mathfrak{c}_A).$$

*Proof.* We calculate:

$$\begin{align*}
& \mathscr{C}^{+}(ev_{A,B} \odot (\sigma \otimes \mathfrak{c}_A)) \\
& \cong \{(\mathfrak{c}_{x_A \to x_B}, (x^\sigma \parallel \mathfrak{c}_{y_A})) | \text{matching, c.c.}\} \\
& = \{(\mathfrak{c}_{x_A \to x_B}, (x^\sigma \parallel \mathfrak{c}_{y_A})) | \text{matching}\} \\
& = \{(\mathfrak{c}_{x_A^\sigma \to x_B^\sigma}, (x^\sigma \parallel \mathfrak{c}_{x_A^\sigma})) | x^\sigma \in \mathscr{C}^{+}(\sigma)\} \\
& \cong \mathscr{C}^{+}(\sigma)
\end{align*}$$

using Propositions 7.3.1 and 8.1.1, Lemmas 6.4.4 and 8.2.27; a direct verification to ensure that no causal loop arises; and resolving the constraints due to matching by definition of the display maps. All order-isomorphisms involved are compatible with display maps, and the same reasoning compatibly applies to symmetries, so altogether we get a strong isomorphism by Corollary 7.2.13. $\square$

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

Finally, we may conclude the universal property of relative closure for NTCG:

**Proposition 8.2.29.** Consider $\Gamma, A, B$ --arenas with B strict.

For any $\sigma : \Gamma \otimes A \vdash B$ negative and winning, there is a unique (up to $\approx$) $\Lambda(\sigma) : \Gamma \vdash A \to B$ such that $ev_{A,B} \odot (\Lambda(\sigma) \otimes \mathfrak{c}_A) \approx \sigma$.

*Proof. Existence.* First, $\Lambda(\sigma)$ is obtained by Proposition 8.2.25. Now we have

$$ev_{A,B} \odot (\Lambda(\sigma) \otimes \mathfrak{c}_A) \approx \Lambda^{-1}(\Lambda(\sigma)) \approx \sigma$$

by Lemma 8.2.28 followed by Lemma 8.2.26.

*Uniqueness.* If $\tau : \Gamma \vdash A \to B$ satisfies the desired property, then $\Lambda^{-1}(\tau) \approx \sigma$ by Lemma 8.2.28, so $\tau \approx \Lambda(\sigma)$ since $\Lambda(-)$ preserves $\approx$ and by Lemma 8.2.26. $\square$

<figure><img src="image_128.png" /></figure>
## 8.3 Non-Linear Structure

Next, we describe the non-linear structure in boards.

### 8.3.1 The Resource Modality

Last but not least, we must define $!$, the resource modality. This is where all the somewhat heavy handling of symmetries up to now finally strikes in.

**Functorial action.** On a strict $--board A$, the (non-strict) $--board !A$ was defined in Definition 8.2.13. We must extend it to a functor, thus first define the functorial action.

As observed below Definition 7.1.26, the construction $!(-)$ applies to plain ess, so we may form the ess $!\sigma$ which we must equip with a display map. For that, we use:

**Lemma 8.3.1.** For E an ess, there is an order-isomorphism

$$[-] : \mathrm{Fam}(\mathcal{C}^{\neq\emptyset}(E)) \simeq \mathcal{C}(!E)$$

with $\mathrm{Fam}(X)$ the set of families of elements of $X$ indexed by finite subsets of $\mathbb{N}$.

*Proof.* If $(x_i)_{i \in I}$ is a family of non-empty configurations of $E$, we write

$$[(x_i)_{i \in I}] = \|_{i \in I} x_i = \bigcup_{i \in I} \{i\} \times x_i \in \mathcal{C}(!E),$$

and this decomposition is clearly unique if we insist that all $x_i$s are non-empty. $\square$

This order-iso for configurations of $!E$ is very much like similar isomorphisms we encountered for other constructions, see e.g. Lemma 7.1.22 for parallel composition / tensor, Lemma 8.2.9 with &, and Lemma 8.2.12 for $\to$. However, unlike those, it does not extend to symmetries. This is because symmetries of $!E$ do not restrict componentwise, on the contrary, their role is precisely to span across components. However:

**Lemma 8.3.2.** Consider A a strict $--board$. Then, there is an order-isomorphism

$$[-] : \mathrm{Fam}(\mathcal{S}_+^{\neq\emptyset}(A)) \cong \mathcal{S}_+(!A)$$

compatible with dom and cod.

*Proof.* Direct from the definition. $\square$

In order to define the strategy $!\sigma$, it suffices to assign a display map:

**Proposition 8.3.3.** Consider A, B strict $--boards$, and $\sigma : A \vdash B$ negative winning. Then, the ess $!\sigma$ may be equipped with a display map $\partial_{!\sigma}$ such that

$$\partial_{!\sigma}([x^i | i \in I]) = [x_A^i | i \in I] \vdash [x_B^i | i \in I]$$

where $\partial_{!\sigma}(x^i) = x_A^i \vdash x_B^i$ for $i \in I$; making $!\sigma : !A \vdash !B$ negative winning. Moreover, $!(-)$ preserves $\approx$.
*Proof. Strategy.* The display map defined above on configurations preserves unions and cardinal; moreover it is straightforward to extend it to symmetries. This gives a map of ess by Lemma 7.1.9, we omit the verifications that this yields a strategy.

*Negative, winning.* A *n*-ary analogue of the tensor (see Proposition 8.2.16).

*Congruence.* Consider $f : \sigma \approx \tau$. We construct $!f : !\sigma \approx !\tau$ simply component-wise. Clearly, it is an isomorphism, we must show that it commutes with the display to the board up to a positive symmetry. For that, consider $[x^i | i \in I] \in \mathscr{C}(!\sigma)$. For $i \in I$

$$ \begin{tikzcd} x^i \arrow[r, "f"] \arrow[d, "\partial_\sigma"] & f(x^i) \arrow[d, "\partial_\tau"'] \\ x_A^i \vdash x_B^i \arrow[r, "\theta_A^i \vdash \theta_B^i"] & y_A^i \vdash y_B^i \end{tikzcd} $$

where $\theta_A^i \in \mathscr{S}_-(A)$ and $\theta_B^i \in \mathscr{S}_+(B)$. It follows by Lemma 8.3.2 that the diagram

$$ \begin{tikzcd} [x^i | i \in I] \arrow[r, "!f", "\partial_\sigma"] & [f(x^i) | i \in I] \arrow[d, "\partial_\tau"] \\ [x_A^i | i \in I] \vdash [x_B^i | i \in I] \arrow[r, "[\theta_A^i | i \in I] \vdash [\theta_B^i | i \in I]"'] & [y_A^i | i \in I] \vdash [y_B^i | i \in I] \end{tikzcd} $$

typechecks, where $[\theta_A^i | i \in I] \in \mathscr{S}_-(!A)$ and $[\theta_B^i | i \in I] \in \mathscr{S}_+(!A)$. It also commutes as it typechecks for all sub-configurations of $[x^i | i \in I]$, all as constructions involved are monotone and preserve cardinal, by Lemma 6.1.12 this implies commutation. $\square$

It remains to prove that $!(\neg)$ is a $\neg$-functor:

**Proposition 8.3.4.** We have a $\neg$-functor $!(\neg) : \text{NTCG} \to \text{NTCG}$.

*Proof. Preservation of copycat.* We build an isomorphism $!(\mathscr{c}_A) \approx \mathscr{c}_{!A}$. This is done via Corollary 7.2.13, by constructing an order-isomorphism between $\mathscr{S}^+(!(\mathscr{c}_A))$ and $\mathscr{S}^+(\mathscr{c}_{!A})$ compatible with dom and cod and with display maps. First, notice that

$$ \mathscr{S}^+(\mathscr{c}_{!A}) \cong \mathscr{S}!(A) \qquad (8.5) $$

by Lemma 7.3.14. From the definition and Lemma 7.3.14, $\mathscr{S}!(\mathscr{c}_A)$ comprises

$$ \theta : [x_A^i \parallel x_A^i | i \in I] \cong [y_A^j \parallel y_A^j | j \in J] $$

given by some bijection $\pi : I \cong J$ and $\theta^i \parallel \theta^i : x_A^i \parallel x_A^i \cong \mathscr{c}_A y_A^j \parallel j_A^j$ – but this is clearly isomorphic to the data of $\pi : I \cong J$ and a family of symmetries $\theta^i : x_A^i \cong_A y_A^j$, i.e. to $\mathscr{S}!(A)$. Together with (8.5), this yields a bijection $\mathscr{S}^+(\mathscr{c}_{!A}) \cong \mathscr{S}^+(!\mathscr{c}_A)$ which is easily checked to be an order-isomorphism preserving display maps as required.

*Preservation of composition.* We build an iso $\mathscr{S}^+((\tau \odot \sigma)) \cong \mathscr{S}^+((\tau) \odot (\sigma))$.

By definition and Proposition 7.3.1, symmetries in $\mathscr{S}^+((\tau \odot \sigma))$ are given by a bijection $\pi : I \cong J$, and for each $i \in I$, a symmetry

$$ \theta_i^\tau \odot \theta_i^\sigma : x_i^\tau \odot x_i^\sigma \cong \tau \odot \sigma y_{\pi(i)}^\tau \odot y_{\pi(i)}^\sigma $$
in $S^+(\tau \odot \sigma)$. Then $\pi : I \cong J$ together with the family of $\theta_i^\tau : x_i^\tau \cong_\tau y_{\pi(i)}^\tau$ yields

$$ \theta^{!\tau} : [x_i^\tau | i \in I] \cong_{!\tau} [y_j^\tau | j \in J]. $$

Likewise, set $I' = \{i \in I | \theta_i^\sigma \neq \emptyset\}$, and $\pi' : I' \cong J'$ as the restriction of $\pi$. Then, $\pi' : I' \cong J'$ together with the family of $\theta_i^\sigma : x_i^\sigma \cong_\sigma y_{\pi'(i)}^\sigma$ for $i \in I'$ yields

$$ \theta^{!\sigma} : [x_i^\sigma | i \in I'] \cong_{!\sigma} [y_j^\sigma | j \in J'], $$

It is direct that $\theta^{!\sigma}$ and $\theta^{!\tau}$ are causally compatible, forming $\theta^{!\tau} \odot \theta^{!\sigma} \in S^+(!\tau \odot !\sigma)$, and that the construction preserves unions and display maps.

Reciprocally, symmetries in $S^+(!\tau \odot !\sigma)$ are given by causally compatible

$$ \theta^{!\sigma} : x^{!\sigma} \cong_{!\sigma} y^{!\sigma}, \qquad \theta^{!\tau} : x^{!\tau} \cong_{!\tau} y^{!\tau} $$

respectively given by $\pi^\sigma : I \cong J$ and $\theta_i^\sigma : x_i^\sigma \cong_\sigma y_{\pi(i)}^\sigma$ for $i \in I$; and by $\pi^\tau : I' \cong J'$ and $\theta_i^\tau : x_i^\tau \cong_\tau y_{\pi'(i)}^\tau$ for $i \in I'$. Now, for $i \in I$, $\theta_i^\sigma$ is non-empty. Since $\sigma$ is negative, $(\theta_i^\sigma)_B$ is non-empty. So as $\theta^{!\sigma}$ and $\theta^{!\tau}$ are matching, we must have $i \in I'$ as well with $\theta_i^\tau$ non-empty. This also entails that $\pi(i) = \pi'(i)$, so that $I \subseteq I'$, $J \subseteq J'$ and $\pi \subseteq \pi'$. For $i \in I' \setminus I$, set $x_i^\sigma = \emptyset$, $y_i^\sigma = \emptyset$, and $\theta_i^\sigma = \emptyset$. Now it is direct that for any $i \in I$, the symmetries $\theta_i^\sigma$ and $\theta_i^\tau$ are matching causally compatible, so that $\theta_i^\tau \odot \theta_i^\sigma \in S^+(\tau \odot \sigma)$. So altogether we have a bijection $\pi : I \cong J$, and for all $i \in I$ a symmetry

$$ \theta_i^\tau \odot \theta_i^\sigma : x_i^\tau \odot x_i^\sigma \cong_{\tau \odot \sigma} y_i^\tau \odot y_i^\sigma, $$

that is, the data for a symmetry in $!(\tau \odot \sigma)$. It is a direct verification that this transformation preserves unions and display maps.

These operations are defined on symmetries but the same applies to configurations compatibly, informing an isomorphism $!(\tau \odot \sigma) \approx !\tau \odot !\sigma$ by Corollary 7.2.13. $\square$

Notice that we formulated the latter isomorphism directly on symmetries, whereas in many earlier proofs, we worked on configurations and only remarked that the same applies to symmetries. In most cases (e.g. tensor, with, composition), the construction applies to configurations and symmetries in exactly the same way. But the situation is really different for $!(-)$: this is the only construction that introduces new, non-trivial symmetries, and so treats the two levels genuinely differently.

**A** ~-**comonad**. It remains to equip $!(-)$ with adequate structural morphisms, which as before will be obtained by lifting appropriate renamings:

**Lemma 8.3.5.** Consider A a --board. Then, we have winning renamings:

$$ \begin{aligned} \mathrm{der}_A &: A^{\perp} \to (!A)^{\perp} \\ a &\mapsto (0, a) \end{aligned} $$

$$ \begin{aligned} \mathrm{dig}_A &: (!A)^{\perp} \to (!A)^{\perp} \\ (i, (j, a)) &\mapsto ((i, j), a) \end{aligned} $$

with $\langle -, - \rangle : \mathbb{N} \times \mathbb{N} \cong \mathbb{N}$ a fixed bijection.

*Proof.* Direct verification. $\square$