Concurrent Hyland-Ong games
Simon Castellan
Pierre Clairambault
Glynn Winskel
In this technical report, we build a cartesian closed category of non-deterministic concurrent strategies playing on arenas. We show that this CCC admits as a sub-CCC the standard category of arenas and Hyland-Ong innocent strategies. Our strategies, have much more possible behaviours than standard Hyland-Ong innocent strategies -- however the purpose of this technical report is to define our CCC, and we leave for later its use for semantics of programming languages.
appendix.tex
In this section, we recall some preliminaries on event structures. In particular
we introduce stable families, used in our proofs of the main development.

\subsection{Event structures and stable families}

Here we only give some basic definitions, notations and properties, but we will skip proofs. This
is intended as a reference only, a more comprehensive introduction to event structures and
stable families can be found in [cite:GamesFam].

\paragraph{Notation.} If $x\in \conf{E}$, $e\in E$ and $x\cup \{e\} \in \conf{E}$,
we write $x\longcov{e}$ or $x\cov$ -- this is the covering relation, \emph{i.e.} the
one-step extension of a configuration.

We write $\ES$ for the category of event structures and maps between them, and $\ESP$ for the category
of event structures with polarities and polarity-preserving maps.

\subsubsection{Products}

\begin{definition}
Let $E$ be a set of events equipped with a non-empty $\F_E \subseteq_f E$ (a set of finite subsets). For $X\subseteq \F_E$
we say that $X$ is \textbf{compatible}, written $X\uparrow$, iff there is $x\in \F_E$ such that $\cup X \subseteq x$.
We define a \textbf{stable family} as such a pair $(E, \F_E)$ satisfying the additional axioms:
\begin{itemize}
\item[(1)] \emph{Completeness:} For $X\subseteq \F_E$, if $X\uparrow$ then $\cup X \in \F_E$ as well.
\item[(2)] \emph{Stability:} For $X\subseteq \F_E$, if $X\uparrow$ then $\cup X \in \F_E$ as well.
\item[(3)] \emph{Coincidence-freeness:} For $e, e'\in x\in \F$ with $e\neq e'$, then there is $y\in \F_E$
with $y\subseteq x$ and $e\in y \Leftrightarrow e'\not \in y$.
\end{itemize}
A map $f: (E, \F_E) \to (F, \F_F)$ of stable families is a function $f:E\to F$ preserving configurations,
and locally injective in the sense that forall $e, e'\in x\in \F_E$, $f(e) = f(e') \implies e = e'$.
\end{definition}

When speaking about a stable family $(E, \F_E)$ we will sometimes leave $E$ implicit and refer to it as $\F_E$.

The product of stable families is easier to describe directly than that of event structures. 

\begin{definition}
For stable families $(A, \F_A)$ and $(B, \F_B)$ their product is $(A\times B, \F_{A\times B})$, where
$x\subseteq A\times B$ is in $\F_{A\times B}$ iff it satisfies:
\begin{itemize}
\item[(1)] Projections: $\pi_1 x \in \F_A$ and $\pi_2 x \in \F_B$
\item[(2)] Injectivity of projections: If $e, e' \in x$ with $\pi_i e = \pi_i e'$, then $e = e'$.
\item[(3)] Coincidence-freeness: If $e, e'\in x$ with $e\neq e'$, then there exists $y \subseteq x$ with
$\pi_1 y \in \F_A$ and $\pi_2 y \in \F_B$ as well, and $e\in y \Leftrightarrow e'\not \in y$.
\end{itemize}
\end{definition}

This definition yields a stable family, and actually gives a product in the category of stable families
and maps between them. This product can be transported to event structures as follows.

\subsubsection{Products in event structures}

We do not reiterate the definition of event structures or maps of event structures, which can be found in
the main text. Let us note though that for $E$ an event structure, $(E, \conf{E})$ is a stable family. Actually,
$\conf{-}$ is easily extended to a functor from event structures to stable families. 

There is an operation in the other direction, giving a right adjoint to $\conf{-}$.

\paragraph{Primes.} Let $(E, \F_E)$ be a stable family, and $x\in \F_E$. Then there is a partial order induced
on $x$ by, for $e, e'\in x$:
\[
e \leq_x e' \Leftrightarrow \forall y \subseteq x, y\in \F_E \& e'\in y \implies e \in y
\]
We also have the corresponding notion of immediate dependency $e \imc_x e'$.

Then for $e\in x\in \F_E$, we can define the \textbf{prime}:
\[
[e]_x = \{e'\in x \mid e'\leq_x e\}
\]
It is then easy to show that $[e]_x \in \F_E$.

\begin{definition}
For a stable family $(E, \F_E)$ we define an event structure $\Pr((E,\F_E))$ having:
\begin{itemize}
\item \emph{Events:} primes $[e]_x$.
\item \emph{Causality:} inclusion.
\item \emph{Consistency:} $X \in \Con_{\Pr((E, \F_E))}$ iff $\cup X \in \F_E$.
\end{itemize}
\end{definition}

Then one can check that $\Pr(-)$ extends to a functor from stable families to event structures, which is
right adjoint to $\conf{-}$. For event structures $A$ and $B$ we can now define:

\[
A\times B = \Pr(\conf{A}\times \conf{B})
\]

One can check that this defines a product of $A$ and $B$ in the category of event structures.

\subsubsection{Two constructions on event structures}

We introduce two constructions on event structures:

\paragraph{Restriction.} Let $E$ be an event structure, and $R\subseteq E$. The \emph{restriction} of $E$
to $R$ comprises events whose causal dependencies are all in $R$.

\begin{definition}
There is an event structure $E\restr R$, the \textbf{restriction} of $E$ to $R$, having:
\begin{itemize}
\item \emph{Events:} 
\[
\{e\in E \mid [e] \subseteq R\}
\]
\item \emph{Causality, consistency:} same as in $E$.
\end{itemize}
\end{definition}

For $(E, \F_E)$ a stable family one can also form its restriction to $R$ by restricting $\F_E$ to subseteq
of $R$. We can then check that $\conf{E\restr R} = \conf{E}\restr R$, and for all $(E, \F_E)$
stable family we have $\Pr((E, \F_E)\restr R) = \Pr((E, \F_E)) \restr \max^{-1}R$.


\paragraph{Projection.} Let $E$ be an event structure, and $V\subseteq E$. The \emph{projection} of $E$ to
$V$ hides the causal dependencies that are not in $V$.

\begin{definition}
For $E$ an event structure and $V\subseteq E$ there is an event structure $E\proj V$, the \textbf{projection}
of $E$ to $V$, having:
\begin{itemize}
\item \emph{Events:} Those of $V$,
\item \emph{Causality, consistency:} Induced by $E$.
\end{itemize}
\end{definition}

\subsubsection{Pullbacks in $\ES$}

We have seen how one can define products in $\ES$. Take now $f, g : E \to F$. Defining $R \subseteq E$ 
as $e\in R$ iff $f(e) = g(e)$, one can check that $E\restr R$ is an equalizer of $f$ and $g$. Together
with the product introduced above, this permits to construct pullbacks in $\ES$. 

Let $f: A \to C$ and $g: B \to C$. Form their pullback by expanding the definition above.

\[
\xymatrix@R=20pt@C=20pt{
& A\circledast B
	\ar[dl]_{\Pi_1}
	\ar[dr]^{\Pi_2}
	\pb{270}\\
A 	\ar[dr]_{f}&&
B
	\ar[dl]^{g}\\
&C
}
\]

Precisely, we first define $R \subseteq A\times B$ as the set of pairs $(a, b)$ such that $f(a) = g(b)$.
Then we set: 
\[
A \circledast B = \Pr(\conf{A} \times \conf{B} \restr R)
\]
and thereby obtain the pullback of $f$ and $g$. Unfolding the definitions, we can see that events of
$A \circledast B$ have the form:
\[
[(a, b)]_x
\]
where $x \in \conf{A}\times \conf{B} \restr R$ and $(a, b)\in x$.

\subsubsection{Technical lemmas on the pullback}

The pullback will be of key importance in our development. We will make use of the following technical lemmas,
for a pullback $A\circledast B$ of $f : A \to C$ and $g: B \to C$.

\begin{lemma}[Characterization of immediate causality]
Take $f: A\to C$ and $g: B \to C$, and take their pullback $A\circledast B$. Suppose moreover that in the
pullback, we have:
\[
[(a, b)]_x \imc [(a', b')]_x
\]
Then necessarily, $a\imc a'$ or $b\imc b'$.
\label{lem:imc_pullback}\label{causality_in_the_pullback}
\end{lemma}
\begin{proof}
Suppose first we have $a \leq a'$ or $b\leq b'$, say \emph{w.l.o.g.} $a < a'$. Suppose, looking for a 
contradiction, that this dependency is not immediate: there is $a''$ such that $a < a'' < a'$. But then
$[(a', b')]_x$ must contain some $(a'', b'')$. Then we have:
\[
[(a, b)]_x \subset [(a'', b'')]_x \subset [(a', b')]_x
\]
Contradicting the immediate causality $[(a, b)]_x \imc [(a', b')]_x$, so $a\imc a'$.

Suppose we have neither $a\leq a'$ nor $b \leq b'$. But then, setting $y = [(a', b')]_x$ we
have $y \setminus (a, b) \in \conf{A\circledast B}$. To prove that, the only non-trivial condition
to check is that its projections are still configurations. Suppose by contradiction that $\pi_1 (y\setminus (a,b)) 
\not \in \conf{A}$. This means that there is $a''\in y$ such that $a \leq a''$, so $y\setminus (a,b)$ is not 
down-closed anymore. But then there is $(a'', b'') \in y$ with:
\[
(a, b) \leq_x (a'', b'')
\]
But $(a'', b'') \leq_x (a', b')$ as well by definition of $y$, so that contradicts the hypothesis $[(a, b)]_x \imc [(a', b')]_x$.
\end{proof}

\begin{lemma}[Characterization of immediate conflict]
Take $f: A\to C$ and $g: B \to C$, and take their pullback $A\circledast B$. Suppose moreover that in the
pullback, we have $x\in \conf{A\circledast B}$ with $x \longcov{[(a, b)]_y}, x \longcov{[(a', b')_{y'}]}$
but $x \cup \{[(a, b)]_y, [(a', b')]_{y'}\} \not \in \conf{A\circledast B}$. Then either
$\Pi_1\,x \cup \{a, a'\} \not \in \conf{A}$, or $\Pi_2\,y\cup \{b, b'\} \not \in \conf{B}$.
\label{lem:conflict_pullback}\label{lemma:pbconflict}
\end{lemma}
\begin{proof}
If we had both $\Pi_1\,\cup \{a, a'\} \in \conf{A}$ and $\Pi_2\,\cup \{b, b'\}$, then 
$x \cup \{[(a, b)]_y, [(a', b')]_{y'}\}$ would have its two projections respectively in $\conf{A}$ and
$\conf{B}$. However it obviously satisfies the other conditions of configurations of the product, and
is in the restriction involved in the definition of the pullback; therefore it is a valid configuration
of $A\circledast B$, absurd.
\end{proof}


Very often, we will reason at the level of configurations of the pullback rather than events. Such configurations
can be presented a bit more simply:

\begin{proposition}
Configurations of $A\circledast B$ uniquely correspond to the composition bijections between $x\in \conf{A}$ and
$y\in \conf{B}$:
\[
x \stackrel{f}{\iso} f(x) = g(y) \stackrel{g}{\iso} y
\]
that are \textbf{secured}, in the sense that the transitive relation generated by
$(a, b) \leq (a', b')$ iff $a\leq a'$ or $b\leq b'$ is a partial order -- in other words there is no causal loop.
\label{prop:secured}
\label{secured1}
\end{proposition}
\begin{proof}
Simple verification.
\end{proof}


\subsubsection{Technical lemmas on event structures}

The two following technical lemmas will be useful in our development.

\begin{lemma}\label{lem:incmap}
Let $f: E \to F$ be a map of event structures, and let $x, y, z \in \conf{E}$ such that $x, y \subseteq z$ and
$f(x) \subseteq f(y)$, then $x \subseteq y$.
\end{lemma}
\begin{proof}
Suppose this is not the case, then there is $e\in x$ such that $e \not \in y$. But still $f(e) \in f(y)$ so there is
$e'\in y$ such that $f(e) = f(e')$. But since $x, y \subseteq z\in \conf{E}$, by local injectivity we have $e = e'$, absurd.
\end{proof}

\begin{lemma}[Mapification]
Suppose there is a total function $p: \conf{R} \to \conf{S}$ preserving $\cov$ and \emph{preserves bounded union} in the sense that for all
$x, y\in \conf{R}$ such that $x$ and $y$ are compatible, then $p(x\cup y) = p(x) \cup p(y)$. Then there is a unique total map of event structure
$\hat{p} : R \arrow S$ such that for all $x\in \conf{R}$, $\hat{p}(x) = p(x)$.
\label{lem:mapification}
\end{lemma}
\begin{proof}
For an event $r\in R$, we necessarily have $p([e)) ~ \cov ~ p([e])$, let us write $p([e]) = p([e)) \cup \{e'\}$. We set
$\hat{p}(e) = e'$. Now, suppose $x \longcov{e} y$ in $\conf{R}$. Necessarily,
\begin{eqnarray*}
p(y)    &=& p(x \cup [e])\\
        &=& p(x) \cup p([e])\\
        &=& p(x) \cup p([e)) \cup \{\hat{p}(e)\}\\
        &=& p(x) \cup \{\hat{p}(e)\}
\end{eqnarray*}
from which it follows by immediate induction that for any configuration $x\in \conf{R}$, $\hat{p}(x) = p(x)$.
Finally, $\hat{p}$ is a map of event structures since it evidently preserves configurations, and is locally injective since it preserves
$\cov$.
\end{proof}

\subsection{Symmetry}

The basic theory of event structures with symmetry is introduced and developped in \cite{glynn-symmetry}. In this
technical appendix, we recall some basic definitions, then give some lemmas used in our development.

\subsubsection{Event structures with symmetry}

\begin{definition}[Open maps]
  An map $f : A {\rightarrow} B$ between event structures is \emph{open} whenever
  it is rigid (preserves causal dependency) and for each configuration
  $x$ of $A$ and $y$ configuration of $B$ such that $fx \subseteq y$
  then $x$ can be extended to a configuration $x'$ of $A$ such that
  $fx' = y$.
\end{definition}
\begin{definition}[Event structure with symmetry]
  An event structure with symmetry $\A$ is a tuple $(A, \tilde A, l_A, r_A)$
  where $A$ and $\tilde{A}$ are event structures, and $l_A, r_A$ form a span:
  \[
  \xymatrix{
  A&\tilde{A}\ar[l]_{l_A} \ar[r]^{r_A}& A
  }
  \]
  such that $l_A, r_A$ are jointly monic (\emph{i.e.} their pairing $\tuple{l_A, r_A}$ is
  monic) and satisfy diagrams presenting categorically equivalence relations, see \emph{e.g.} \cite{glynn-symmetry}.
  Moreover, $l_A$ and $r_A$ are supposed to be open maps.
\end{definition}

We do not recall the diagrams expressing the fact that $l_A, r_A$ form an equivalence since they
are at the same time standard, and not used much in our development.


We use the notation $\A, \B, \C$ to range over event structures with symmetry whose underlying event structures will be denoted $A, B, C, {\ldots}$ and symmetries $\tilde A, \tilde B, \tilde C, {\ldots}$
An alternative definition of event structures with symmetry can be
given in terms of isomorphism families:
\begin{definition}[Isomorphism families]
  An \textbf{isomorphism family} on event structure $A$ is a set 
  $\mathbb S_A$ of
  bijections between onfigurations of $A$ containing the identities $x
  {\cong} y$, closed under composition and inverse, and satisfying two
  more properties:
  \begin{itemize}
  \item Whenever ${\theta}: x {\cong} y {\in} \mathbb S_A$ and $x'$ a
    sub-configuration of $x$ then ${\theta}\vert_{x'}$ the restriction
    of ${\theta}$ to $x'$ must belong to $\mathbb S_A$
  \item Whenever ${\theta} : x {\cong} y {\in} \mathbb S_A$ and $x \subseteq x' {\in} {\mathscr{C}}(A)$
    then there exists ${\theta}' \supseteq {\theta}$ in $\mathbb S_A$ such that the
    domain of ${\theta}'$ is $x'$.
  \end{itemize}
\end{definition}
Note that because of restriction, any bijection which belongs to $\mathbb S_A$ is also an order-isomorphism,
\emph{i.e.} it preserves and reflects causal order. 

Isomorphism families can be regarded as a more concrete presentation of symmetries on event structures. Any
symmetry $(\tilde{A}, l_A, r_A)$ on event structure $A$ generates an isomorphism family by setting:
\[
\mathbb{S}_A = \{\{(l_A \tilde{a}, r_A \tilde{a})\mid \tilde{a}\in x\} \mid x\in \conf{\tilde{A}}\}
\]
Likewise $\mathbb{S}_A$ is a stable family on the set of events $A\times A$, therefore one can redefine
the symmetry \emph{via} the primes construction, as $\Pr(\mathbb{S}_A)$. One can check that the event 
structure defined in this way along with the obvious projections is a symmetry isomorphic to the original,
This connection is worked out in all details in \cite{glynn-symmetry}. In our development, we will mostly work with the
isomorphism families and leave the symmetry implicit -- it can be, anyway, recovered uniquely up to
isomorphism.

If $\A$ is an event structure with symmetry, we will write:
\[
x \stackrel{\theta}{\iso_\A} y 
\]
if $\theta : x \iso y$ is in $\mathbb{S}_A$.


Event structures with symmetry can carry additional labels
(eg. polarity and question/answer labelling), that have to be preserved by isomorphisms.
Operations such as dual and parallel
composition extends clearly to event structures with symmetry.

\begin{definition}[Maps of event structures with symmetry]
  A map $f : \A {\rightarrow} \B$ of event structures with symmetry is a
  map $f : \A {\rightarrow} \B$ of event structures such that for each
  isomorphism $x \stackrel{\theta}{\iso_\A} y$, the bijection induced by $f$:
  \[
  f\,\theta = \{(f(a_1), f(a_2))\mid (a_1, a_2) \in \theta\}
  \]
  is in $\mathbb{S}_B$.

  Or equivalently, there exists a (necessarily
  unique) map $\tilde f : \tilde A{\rightarrow} \tilde B$ such that $l_B \circ \tilde{f}= f\circ l_A$,
  and $r_B \circ \tilde{f} = f \circ r_B$.
\end{definition}

There is a category $\ESS$ of event structures with symmetry and maps preserving symmery, and a 
category $\ESSP$ in the presence of polarities, which the isomorphisms and maps should preserve.

Symmetry allow us to identify maps that play symmetric events:
\begin{definition}[Symmetric maps]
  Let $f, g : \A {\rightarrow} \B$ be two parallel maps of event structures with
  symmetry. We say that $f$ and $g$ are symmetric (notation: $f\sim
  g$) when for any configuration $x$ in $A$, the induced bijection:
  \[
  \theta = \{(f(a), g(a))\mid a \in x\}
  \]
  is in $\mathbb{S}_B$.

  Or equivalently, there is a (necessarily unique) $h : A\to \tilde{B}$ such that 
  $l_B \circ h = f$ and $r_B \circ h = g$.
\end{definition}
This relation $\sim$ is preserved by composition,
which makes $\ESS$ and $\ESSP$ into a (rather degenerate) strict 2-categories.

%As an example of symmetry, one can endow $\oc A$ with a symmetry:
%\begin{lemma}[Symmetry on $\oc A$]
%  The set of isomorphisms of $\oc A$ consisting in the sets of all the order-isomorphisms:
%\[
%x \stackrel{\theta}{\iso} y
%\]
%such that $\lbl\circ \theta = \lbl$ is a symmetry on $!A$
%\end{lemma}
%\begin{proof}
%  Clearly this set contains the identity and is stable under
%  composition, inverse and restriction. If we have $x \stackrel{{\theta}} {\cong}
%  y$ and $x \longcov{{\alpha}:[a] {\rightarrow} {\omega}}$ then we must have $[a) \subseteq
%  \lbl(x)$ and thus we can define ${\alpha}'(a) = {\alpha}(a)$ and ${\alpha}'(b) =
%  \ind({\theta}(b))$. That gives ${\alpha}' : [a] {\rightarrow} {\omega}$ such that $y \longcov {\alpha'}$ and
%  ${\theta} \cup\{{\alpha}, {\alpha}'\}$ is a valid symmetry of $!A$.
%\end{proof}
\subsubsection{Higher symmetry}
\label{sec:highsymm}

%The category of event structures with symmetry does not have pullbacks
%in general but has pseudo-pullbacks. We have a similar characterisation
%of configurations of a pseudo pullback, similar to the one of Lemma
%\ref{secured1}:
%\begin{lemma}\label{secured2}
%  Let $f : \A {\rightarrow} \C, g : \B {\rightarrow} \C$ be maps between event structures with
%  symmetry. Configurations of the pseudo-pullback are triples $(x, {\theta},
%  y)$ such that $x {\in} {\mathscr{C}}(A)$, $y {\in} {\mathscr{C}}(B)$ and ${\theta} {\in} \mathbb S_C$ with $fx
%  \stackrel{{\theta}} {\cong} gy$. Isomorphisms between $(x, {\theta}, y)$ and $(x', {\theta},
%  y')$ in the symmetry of the pseudo-pullback are given by ${\varphi} : x {\cong} x'$ and ${\psi} : y {\cong} y'$ such that
%$$\xymatrix{
%\ar[d]_{f{\varphi}} fx \ar[r]^{{\theta}} & gy \ar[d]^{g{\psi}} \\
%fx' \ar[r]_{{\theta}'} & gy'
%}$$
%\end{lemma}
%
%
%If $\A$ is an event structure with symmetry, then $\tilde{\A}$ can be obtained, itself as an event structure
%with symmetry, via the pseudo-pullback:
%\[
%\xymatrix{
%&\tilde{\A}
%        \ar[dl]
%        \ar[dr]
%        \ar@{}[dd]|{\sim}
%        \pb{270}\\
%\A       \ar[dr]_{id_\A}&&
%\A       \ar[dl]^{id_\A}\\
%&\A
%}
%\]

If $\A$ is an event structure with symmetry, then its symmetry $\tilde{A}$ is itself canonically equipped with a 
symmetry. Although it can be described via a universal property (pseudopullbacks -- see \cite{CCW}), here
we define it instead through its isomorphism family. 

As we have seen above, configurations of $\tilde{A}$ correspond to isomorphisms $\theta \in \mathbb{S}_A$. By abuse of
notations, we will often silently go from one to the other. In particular, configurations on $\tilde{\tilde{A}}$ should
correspond to certain bijections between isomorphisms $\theta, \theta'\in \mathbb{S}_A$ (seen as subsets of $A\times A$).
We ask the isomorphism family of $\tilde{A}$ to comprise bijections between $\theta, \theta'$ corresponding to 
commuting squares: 
\[
\xymatrix@R=15pt@C=15pt{
x       \ar@{}[r]|{\stackrel{\phi}{\iso_\A}}&
x'\\
y       \ar@{}[u]|{\theta \rotatebox{-90}{$\iso$}_\A}
        \ar@{}[r]|{\stackrel{\phi'}{\iso_\A}}&
y'      \ar@{}[u]|{{\theta'}\rotatebox{-90}{$\iso$}_\A}
}
\]
According to this characterisation, $l_{\tilde{A}}$ sends this square to its left side and $r_{\tilde{A}}$ sends it
to its right side. However, there are now additional maps $u_{\tilde{A}}$ sending it to its upper side and $d_{\tilde{A}}$
sending it to its lower side. These additional projections satisfy the diagram:

\[
\xymatrix@R=0pt{
&\tilde{\tilde{S}}
        \ar[dl]_{l_{\tilde{S}}}
        \ar[dd]^{u_{\tilde{S}}}
        \ar[dr]^{r_{\tilde{S}}}&&&
\tilde{\tilde{S}}
        \ar[dl]_{l_{\tilde{S}}}
        \ar[dd]^{d_{\tilde{S}}}
        \ar[dr]^{r_{\tilde{S}}}\\
\tilde{S} \ar[dd]_{l_S}&&
\tilde{S} \ar[dd]^{r_S}&
\tilde{S} \ar[dd]_{r_S}&&
\tilde{S} \ar[dd]^{r_S}\\
&\tilde{S}\ar[dl]_{l_S}
        \ar[dr]^{r_S}&&&
\tilde{S} \ar[dl]_{l_S}
        \ar[dr]^{r_S}\\
S&&S&S&&S
}
\]

We write $\tilde{\A}$ for $\tilde{A}$ \emph{equipped with its symmetry} $\tilde{\tilde{A}}$.
We can now automatically lift some properties from maps $f: \A \to \B$ to $\tilde{f}:\tilde{\A}\to \tilde{\B}$:

\begin{lemma}
We have the following lifting properties.
\begin{enumerate}
\item If $f : \A \arrow \B$ is a morphism in $\ESS/\ESSP$, then $\tilde{f} : \tilde{\A} \arrow \tilde{\B}$ preserves symmetry as well.
\item If $f \sim g$, then $\tilde{f} \sim \tilde{g}$,
%\item If $\sigma : S \arrow A$ has a canonical extension, so does $\tilde{\sigma}$. Moreover, the canonical extension of $\tilde{S}$ coincides
%with that of $S$ in the sense that for all isomorphism $\theta_1 \iso_{\phi} \theta_2$ in $\tilde{\tilde{A}}$ such that $\theta_1 \subseteq \theta'_1$,
%we have:
%\begin{eqnarray*}
%u_{\tilde{A}}(\ext(\phi, \theta'_1)) &=& \ext(u_{\tilde{A}}(\phi), l_{\tilde{A}}(\theta'_1))\\
%d_{\tilde{A}}(\ext(\phi, \theta'_1)) &=& \ext(d_{\tilde{A}}(\phi), r_{\tilde{A}}(\theta'_1))
%\end{eqnarray*}
\end{enumerate}
\label{lem:lifting}
\end{lemma}
\begin{proof}
\emph{(1)} We need to check that $\tilde{f} : \tilde{A} \arrow \tilde{B}$ preserves symmetry. Take a isomorphism in $\tilde{\tilde{A}}$, corresponding
to a square:
\[
\xymatrix{
x       \ar@{}[d]|{\theta \rotatebox{270}{$\iso$}_{\A}}
        \ar@{}[r]|{\stackrel{\phi_1}{\iso_{\A}}}&
x'      \ar@{}[d]|{\theta' \rotatebox{270}{$\iso$}_{\A}}\\
y       \ar@{}[r]|{\stackrel{\phi_2}{\iso_{\A}}}&
y'
}
\]
The component-wise image of this isomorphism by $\tilde{f}$ corresponds to the commuting square:
\[
\xymatrix{
fx       \ar@{}[d]|{f\theta \rotatebox{270}{$\iso$}_{\B}}
        \ar@{}[r]|{\stackrel{f\phi_1}{\iso_{\B}}}&
fx'      \ar@{}[d]|{f\theta' \rotatebox{270}{$\iso$}_{\B}}\\
fy       \ar@{}[r]|{\stackrel{f \phi_2}{\iso_{\B}}}&
fy'
}
\]
which corresponds to a configuration of the isomorphism family of $\tilde{\B}$ by definition.

\emph{(2)} Suppose $f \sim g$, this means that for any $x\in \conf{A}$, the isomorphism $\theta_x = \{(fa, ga)\mid a\in x\}$ is in the isomorphism
family of $x$. Then it is clear that for any isomorphism $x \iso_\phi y$ in the isomorphism family of $A$, the following square commutes:
\[
\xymatrix{
fx       \ar@{}[d]|{\rotatebox{270}{$\iso$}_{f \phi}}
        \ar@{}[r]|{\iso_{\theta_x}}&
gx      \ar@{}[d]|{\rotatebox{270}{$\iso$}_{g \phi}}\\
fy       \ar@{}[r]|{\iso_{\theta_y}}&
gy
}
\]
Indeed take $(a, b)\in \phi$. Then we have $(fa, fb)\in f \phi$, $(ga, gb)\in g\phi$, $(fa, ga)\in \theta_x$ and $(fb, gb)\in \theta_y$.
But this square corresponds to an isomorphism between $\tilde{f}\phi$ and $\tilde{g}\phi$ in $\tilde{B}$, so we do have $\tilde{f} \sim \tilde{g}$.

\end{proof}

\subsubsection{Projections with symmetry}

In this small subsection, we introduce a few definitions and lemmas regarding the generalisation
of projection in the presence of symmetry.

\begin{definition}
Let $\A$ be an event structure with symmetry. A subset $V\subseteq A$ is \emph{closed under symmetry} iff, setting
\[
\tilde{V} = \{\tilde{a}\in \tilde{A} \mid l_A(\tilde{a}) \in V\}
\]
we have $\sigma_A(\tilde{V}) = \tilde{V}$ (where $\sigma_A : \tilde{A} \to \tilde{A}$ is the map expressing that as an equivalence relation, the
symmetry is symmetric).
\label{def:closed_symm}
\end{definition}

\begin{prop}
Let $\A$ be an event structure with symmetry, let $V$ be a subset of the events of $A$ closed under symmetry. Then the triple
$(\tilde{A} \proj \tilde{V}, l_A \restrict \tilde{V}, r_A \restrict \tilde{V})$ (where $\restrict$ denotes function restriction) is
a symmetry on $A\proj V$.

The event structure with symmetry $(A \proj V, \tilde{A} \proj \tilde{V})$ is called the \textbf{projection} of $A$ on $V$.
\label{prop:proj_symm}
\end{prop}
\begin{proof}
A subset $V$ is closed under symmetry if and only if it is the domain of a partial map of event structures preserving
symmetry. According to this, this proposition is a restatement of the partial-total factorisation result for event
structures with symmetry.
\end{proof}


ccccho.tex
We have built a $\sim$-bicategory $\CGS$, which has the structure of a compact closed category and
satisfies its laws up to weak equivalence. Using it as underlying linear category, we will construct
a sub-$\sim$-bicategory of strategies playing on (tcgs generated from) standard Hyland-Ong arenas,
and show how the usual ccc of innocent strategies arises as a subcategory.

\subsection{Arenas and expanded games}

First, we give (an alternative presentation of) the usual notion of arenas \cite{DBLP:journals/iandc/HylandO00}. For $A$ an event structure,
write $\min(A)$ for its set of minimal events.

\begin{definition}
An \textbf{arena} is a countable esp $A$ which is:
\begin{itemize}
\item A \textbf{forest}: for all $a, a'\leq a''$ we have either $a\leq a'$ or $a'\leq a$,
\item \textbf{conflict-free}: $\mathcal{P}_f(A) \subseteq \Con_A$,
\item \textbf{alternating}: for all $a\imc a'$, $\pol(a) \neq \pol(a')$.
\end{itemize}
An arena $A$ is \textbf{negative} iff $\pol(\min(A)) = \{-\}$.
We can also add a Questions/Answers labeling, but this is outside the scope of this paper.
\end{definition}


We will now be interested in $\sim$-strategies playing on a tcg $\oc A$ thought as "$A$ with replications", 
derived from an arena $A$. Its underlying set of events will be the set of \emph{index functions} on $A$:
functions $\alpha : [a] \to \omega$. For such an index function, we write $\lbl\,\alpha = a$ for the
maximal element of its domain, and $\ind\,\alpha = \alpha\,(\lbl\,\alpha)$ for the copy index of its domain.

\begin{lemma}
Let $A$ be an arena. There is an tcg $\oc A$ having:
\begin{itemize}
\item Events: indexing functions $\alpha : [a] \to \omega$.
\item Causality: $\alpha \leq \alpha'$ defined as $\lbl\,\alpha \leq \lbl\,\alpha'$ and $\alpha, \alpha'$
agree on their common domain,
\item Consistency: trivial -- there is no conflict.
\item Symmetry: comprises order-isomorphisms $\theta : x\iso y$ with $x, y \in \conf{\oc A}$ such that
$\theta$ preserves labels.
\end{itemize}
Events $\alpha \in \oc A$ also inherit polarities from $A$.
\end{lemma}
\begin{proof}
  Clearly this set contains the identity and is stable under
  composition, inverse and restriction. If we have $x \stackrel{{\theta}} {\cong}
  y$ and $x \longcov{{\alpha_1}:[a] {\rightarrow} {\omega}}$, then since $A$ is a forest
there is a unique $a' \imc a$, and necessarily $\alpha'_1 = \alpha_1 \restrict [a']$ satisfies
$\alpha'_1 \imc \alpha_2$. Take $\alpha'_2 = \theta(\theta'_1)$. Necessarily, since $y$ is finite,
there is $n \in \omega$ such that $\alpha_2 = \alpha'_2 \cup \{a \mapsto n\} \not \in y$, it is direct to check
that extending $\theta$ with $(\alpha_1, \alpha_2)$ gives an order-isomorphism preserving labels as required.

The essp $\oc A$ is race-preserving, since it is conflict-free. For receptive thin sub-symmetries, pick the
isomorphism families:
\begin{eqnarray*}
\tilde{\oc A}_+ &=& \{x \stackrel{\theta}{\iso_{\oc A}} y\mid \forall \alpha^+\in x,\,\,\ind\,\alpha = \ind\,(\theta(\alpha))\}\\
\tilde{\oc A}_- &=& \{x \stackrel{\theta}{\iso_{\oc A}} y\mid \forall \alpha^-\in x,\,\,\ind\,\alpha = \ind\,(\theta(\alpha))\}
\end{eqnarray*}
which obviously satisfy the requirements.
\end{proof}

Arenas are closed under parallel composition $A\parallel B$ -- sometimes written $A\times B$ for compatibility
with \cite{DBLP:journals/iandc/HylandO00} and since it will be the product of our cartesian closed category. They also support the
dual operation $(-)^\perp$, and include the empty arena $1$.

A $\sim$-strategy playing on an arena $A$ is a $\sim$-strategy
$\sigma : \S \to \oc A$, and a $\sim$-strategy from $\oc A$ to $\oc B$
is a $\sim$-strategy $\sigma : \S \to \oc A^\perp \parallel \oc B$. Restricting
$\CGS$ to objects of the form $\oc A$ gives a full sub-$\sim$-category of $\CGS$. We will
now restrict this sub-$\sim$-bicategory further to obtain one satisfying the laws
of a cartesian closed category up to weak equivalence.

\subsection{A sub-$\sim$-bicategory of $\CGS$}

To get a cartesian closed stucture, we will restrict to \emph{negative} arenas, and
only consider as morphisms $\sim$-strategies that are \emph{negative}, and \emph{single-threaded} in the following sense.

\begin{definition}
An esp $A$ is \textbf{single-threaded} iff it satisfies:
\begin{itemize}
\item[(1)] For any $a\in A$, $[a]$ has exactly one minimal event.
\item[(2)] For any $x\in \conf{A}$ such that $x\longcov{a_1}, x\longcov{a_2}$ and 
$x\cup \{a_1, a_2\} \not \in \conf{A}$, then $[a_1] \cap [a_2] \neq \emptyset$.
(alternatively, they share the same minimal event).
\end{itemize}
An essp $\A$ is single-threaded iff $A$ is.
For a $\sim$-strategy $\sigma : \S \to \A$, we say that it is single-threaded iff $\S$ is.
\end{definition}

The $\sim$-bicategory $\CHO$ has:
\begin{itemize}
\item \emph{Objects:} Negative arenas,
\item \emph{Morphisms from $A$ to $B$:} $\sim$-strategies
\[
\sigma : \S \to \oc A^\perp \parallel \oc B
\]
that are \textbf{negative} (\emph{i.e.} $S$ is negative), and \textbf{single-threaded}. We write
$\sigma : A \choto B$. Negative single-threaded strategies are called $\CHO$-strategies.
\item \emph{$2$-cells:} weak equivalences.
\end{itemize}

For that to typecheck, we need to check that copycat satisfies these conditions and that they
are stable under composition.

\begin{lemma}
For $\A, \B$ conflict-free single-threaded tcgs, the strategies obtained by lifting maps $f: \B^\perp \to A^\perp$ are
negative and single-threaded.
\label{lem:lifting_cho}
\end{lemma}
\begin{proof}
  We just have to check that $\CC_{\B}$ for any conflict-free tcg $\B$ is negative and 
  single-threaded. Clearly minimal events of $\CC_{B}$ are negative.
  Let us first check condition \emph{(1)}.
  Take a prime configuration $x\in \conf{\CC_{\B}}$, we need to check that $x$ has a unique minimal event.
  We know that $x$ must correspond to:
\[
x_1 \supseteq^+ x_2 \subseteq^- x_3
\]
Suppose first that the maximal event of $x$ corresponds to $b\in x_1$. Then we make two observations: firstly, $x_1 = [b]$ -- this
follows from a straightforward analysis of causal dependencies in $\CC_{\B}$. Secondly, necessarily $x_2 = x_3$ since by definition
of $\CC_{\B}$ no event in $x_3 \setminus x_2$ could be below $b$. Any minimal event of $x$ must correspond to a minimal (negative)
event in $x_3$ by negativity of $\CC_{\B}$. Therefore if there were two such $a_1, a_2 \in x_2 = x_3$ they would appear (and
be minimal) as well in $x_1$, which is absurd since $x_1 = [b]$ and $\B$ is single-threaded.

Suppose now that the maximal event of $x$ corresponds to $b\in x_3$. Then for the same reason as above $x_3 = [b]$. Since
minimal events of $x$ must be in $x_3$, there must be only one by single-threadedness of ${\B}$.

For condition \emph{(2)}, note that since $\B$ has no conflict, $\CC_\B$ has none either.
\end{proof}

In particular, from Lemma \ref{lem:lifting_cho} it follows that $\cc_{\oc A} : A \choto A$ is negative
and single-threaded. We now show that $\CHO$-strategies are stable under composition.

\begin{lemma}
  Let $\sigma : \S \to \A^\perp \parallel \B$ and $\tau : \T \to
  \B^\perp \parallel \C$ be negative single-threaded $\sim$-strategies with
  $\A, \B, \C$ negative tcgs.
  Then, $\tau \odot \sigma : \T \odot \S \to \A^\perp \parallel \C$ is negative and single-threaded.
\label{lem:comp_wt}
\end{lemma}
\begin{proof}
  Note first that this is independent from symmetry, so we shall just reason
  on strategies $\sigma : S \to A^\perp \parallel B$
  and $\tau : T \to B^\perp \parallel C$.

   Let $P = (S\parallel {
    C})\circledast ({A}\parallel T)$ be the pullback (in $\ES$)
  of $\sigma \parallel {C}$ and ${A}\parallel \tau$, with
  projections $\Pi_1$ and $\Pi_2$. By construction we have $P =
  \Pr(\F)$ with $\F$ the stable family:
\[
\F = \conf{S \parallel {C}} \times \conf{{A} \parallel T} \restrict R
\]
where $R = \{(e_1,e_2)\mid (\sigma \parallel {C})(e_1) = ({A}\parallel \tau)(e_2)\}$. 

%First, by a straightforward analysis it follows that minimal events of $P$ must have the form
%$[((2, c), (2, t))]_z$ with $t\in \min(T)$, projecting to $C$ hence visible, and with $\tau(t)$ negative -- so $T\odot S$
%is negative. 
%

In order to prove condition \emph{(1)} of single-threadedness,
we are going to prove by induction on $<_P$ that for all $p\in P$, there exists a unique $p'\in \min(P)$, necessarily
of the shape $[((2, c), (2, t))]_z$, such that $p'\leq p$.
If $p\in P$ is minimal it has the form $[((2, c), (2, t))]_z$ for some $z\in \F$, indeed any other case would contradict
negativity of either $S$ or $T$.
Otherwise $p$ is not minimal, \ie~ it has an immediate
cause $q_1 \imc p$. By induction hypothesis, there is a unique $q'_1$ minimal such that $q'_1 \leq q_1 \leq p$. So if there is another
$q'_2 \leq p$ minimal, there must be another $q_2 \imc p$ such that $q'_2 \leq q_2$. We now distinguish cases, depending on the
form of $p$.
\begin{itemize}
\item If $p$ has the form $[((1, s), (1, a))]_z$. Then, by Lemma \ref{lem:imc_pullback} it is straightforward to show that
$q_i$ must have the form $[(1, s_i), -)]_z$. Necessarily, this implies that $s_i \imc s$ as well, and in particular $s_i \leq s$.
By single-threadedness of $S$ it follows that there is a unique $s'\in \min(S)$ such that $s'\leq s_1$ and $s'\leq s_2$. By definition of the pullback
it follows that there is $t\in T$ such that $((1, s'), (2, t))\in z$, and we have:
\begin{eqnarray*}
[((1, s'), (2, t))]_z &\leq& q_i
\end{eqnarray*}
By induction hypothesis, the unique minimal cause of $q_1$ and $q_2$ must be the same as for $[((1, s'), (2, t))]_z$, so we must
have $q'_1 = q'_2$.
\item If $p$ has the form $[((1, s), (2, t))]_z$ where $\pol(s) = +$, then by Lemma \ref{lem:imc_pullback} it is 
straightforward to show that 
$q_i$ must have the form $[((1, s_i), e)]_z$. Then we argue that, as above, we must have $s_i \leq s$. Indeed from
Lemma \ref{lem:imc_pullback} we also know that 
we have either $s_i \imc s$, or $e$ has the shape $(2, t_i)$ with $t_i \imc t$. But by courtesy the latter would
imply that $\tau t_i \imc \tau t$, so $s_i \leq s$ as well since $\sigma$ is a map of event structures. Then the same reasoning as in the previous case applies.
\item If $p$ has the form $[((1, s), (2, t))]_z$ where $\pol(s) = -$, then for the same reason as above, $q_i$ must have the form
$[(-, (2, t_i))]_z$. The reasoning is dual to the previous case.
\item If $p$ has the form $[((2, c), (2, t))]_z$, then $q_i$ must have the form $[(-, (2, t_i))]_z$ with $t_i \leq t$ and the same reasoning applies.
\end{itemize}
Note in passing that from the characterisation of minimal events of the pullback above it follows that
$T\odot S$ is negative.

Let us now show condition \emph{(2)}. 
Take an immediate conflict in $T \odot S$. Necessarily it must originate in a conflict in $P$:
\[
w_1 \longvoc{[(s, t)]_{\cup w_1}} z \longcov{[(s', t')]_{\cup w_2}} w_2
\]
Necessarily by Lemma \ref{lemma:pbconflict} this conflict must originate from one of the projections. Let us
suppose w.l.o.g. that the following is a conflict in $S \parallel {\oc C}$.
\[
\Pi_1~w_1 \longvoc{s} \Pi_1~z \longcov{s'} \Pi_1~w_2
\]
Since $\sigma$ is single-threaded, there must be $s''\in S\parallel {C}$ such that $s''\leq s$ and $s''\leq s'$. Necessarily,
there is $t''\in {A}\parallel T$ such that $(s'', t'')\in z$. Take a minimal predecessor $p\leq [(s'', t'')]_z$;
it is necessarily visible (and in ${C}$) since $S$ and $T$ are negative. It is also below $[(s, t)]_{\cup w_1}$ and
$[(s', t')]_{\cup w_2}$ by construction, so $\tau \odot \sigma$ is single-threaded.
\end{proof}

So, we have constructed our $\sim$-bicategory. We now prove that it is cartesian.



\subsection{A cartesian category}

First, let us note that the empty arena $1$ is such that $\oc 1 = 1$ (with the right hand side $1$ denoting
the empty cgs). Since the objects of $\CHO$ are negative arenas and the strategies are negative as well,
any morphism in $\CHO$:
\[
\sigma : \S \to \oc A^\perp \parallel \oc B
\]
is such that the minimal events of $S$ must map to $\oc B$. But in the particular case where $B = 1$, this means
that $S$ cannot have any minimal events, so it is necessarily the unique trivial map from the empty set
to $\oc A^\perp \parallel \oc B$. It follows that $1$ is a terminal object.

\paragraph{Projections.} We start by noting the following isomorphism.

\begin{lemma}
Let $A$ and $B$ be arenas. Then there is an isomorphism in $\ESSP$:
\[
\oc (A\parallel B) \stackrel{\gamma_{A, B}}{\iso} \oc A \parallel \oc B
\]
\end{lemma}
\begin{proof}
%We start with the simple remark that by construction, for $\alpha \in \oc (A\parallel B)$, we either have 
%$\lbl\,\alpha$ of the form $(1, a)$ (in which case $\alpha$ is only defined on events in the component $A$) or
%of the form $(1, b)$. We fix the convention that in this proof, an event in $\oc (A\parallel B)$ whose label is in
%$A$ (resp. in $B$) will be denoted by $\alpha$ (resp. $\beta$).
%
We define $\gamma_{A, B}$ as the map:
\[
\begin{array}{rcccll}
\gamma_{A, B} &:& \oc (A\parallel B) &\to& \oc A \parallel \oc B\\
&& \alpha &\mapsto& (1, \alpha') &
        \left\{\begin{array}{rclcll}
                \alpha' &:& [a] &\to& \omega & (\lbl\,\alpha = (1, a))\\
                && a' &\mapsto& \alpha(1, a')
                \end{array}\right.\\
&& \beta &\mapsto& (2, \beta') &
        \left\{\begin{array}{rclcll}
                \beta' &:& [b] &\to& \omega & (\lbl\,\beta = (2, b))\\
                && b' &\mapsto& \alpha(1, b')
                \end{array}\right.
\end{array}
\]
This is clearly a map of $\ESP$s, and it has an obvious inverse $\gamma_{A, B}^{-1}$. Both
preserve labels and as isomorphism of $\ESP$s they are rigid, so they transport isomorphisms
on $\oc (A\parallel B)$ (order-isomorphisms preserving labels) to isomorphisms on $\oc A \parallel \oc B$. Therefore
they are actually isomorphisms in $\ESSP$.
\end{proof}

From that it follows that we have maps:
\[
\begin{array}{rcccl}
\inje_A &:& \oc A &\to& \oc (A\times B)\\
	&&  \alpha&\mapsto& \gamma_{A, B}^{-1}(1, \alpha)\\\\
\inje_B &:& \oc B &\to& \oc (A\times B)\\
	&& \beta &\mapsto& \gamma_{A, B}^{-1}(2, \beta)
\end{array}
\]
which are such that $\inje_{A^\perp}$ and $\inje_{B^\perp}$ are strong-receptive and courteous whenever
$A$ and $B$ are negative. Therefore we define by lifting:
\[
\begin{array}{rcccccl}
\varpi_A &=& \lift{\inje_{A^\perp}} &:& A\times B &\choto& A\\
\varpi_B &=& \lift{\inje_{B^\perp}} &:& A\times B &\choto& B
\end{array}
\]

\paragraph{Pairing.} For $A, B, C$ negative we need to define the pairing of:
\[
\begin{array}{rcccl}
\sigma &:& \S &\to& \oc C^\perp \parallel \oc A\\
\tau &:& \T &\to& \oc C^\perp \parallel \oc B
\end{array}
\]
We would like to set:
\[
\begin{array}{rcccl}
\tuple{\sigma, \tau} &:& \S \parallel \T &\to& \oc C^\perp \parallel \oc (A\times B)\\
&& (1, s) &\mapsto& (\oc C^\perp \parallel \inje_A)\circ \sigma\\
&& (2, t) &\mapsto& (\oc C^\perp \parallel \inje_B)\circ \tau
\end{array}
\]
However this might fail local injectivity, since $\sigma$ and $\tau$ might have
a common codomain on $\oc C^\perp$. So we need to reindex their moves to make sure 
that no such collision can occur. In order to do that we introduce two maps:
\[
\begin{array}{rccccl}
\iota_{o} &:& \oc A &\to& \oc A&\\
&&\alpha &\mapsto& \alpha' &\text{where $\left\{\begin{array}{ll}
					\alpha'(a) = 2\alpha(a) + 1&\text{(if $a$ minimal)}\\
					\alpha'(a) = \alpha(a)&\text{(otherwise)}\end{array}\right.$}\\\\
\iota_{e} &:& \oc A &\to& \oc A\\
&&\alpha &\mapsto& \alpha' &\text{where $\left\{\begin{array}{ll}
					\alpha'(a) = 2\alpha(a)&\text{(if $a$ minimal)}\\
					\alpha'(a) = \alpha(a)&\text{(otherwise)}\end{array}\right.$}\\\\
\end{array}
\]
It is immediate to check that $\iota_e$ and $\iota_o$ are maps of essp. Moreover, they have disjoint codomains,
$\iota_e^\perp$ and $\iota_o^\perp$ are strong-receptive (since we only change the copy index of minimal events)
and courteous, and they are both symmetric with the identity: $\iota_e \sim \id_{\oc A}$ and 
$\iota_o \sim \id_{\oc A}$.

It follows that we have weak equivalences:
\begin{eqnarray*}
(\iota_o^\perp \parallel \oc A) \circ \sigma &\simeq& \sigma\\
(\iota_e^\perp \parallel \oc B) \circ \tau &\simeq& \tau
\end{eqnarray*}
And we can now form the pairing:
\[
\begin{array}{rccccl}
\tuple{\sigma, \tau} &:& \S \parallel \T &\to& \oc C^\perp \parallel \oc (A\times B)\\
&&(1, s) &\mapsto& (\iota_o^\perp \parallel \inje_A)\circ \sigma\\
&&(2, s) &\mapsto& (\iota_e^\perp \parallel \inje_B)\circ \tau
\end{array}
\]
It is then direct -- a straightforward variant of the neutrality of copycat under composition -- to check:
\begin{eqnarray*}
\varpi_A \odot \tuple{\sigma, \tau} &\simeq& \sigma\\
\varpi_B \odot \tuple{\sigma, \tau} &\simeq& \tau
\end{eqnarray*}

In order to have a cartesian category, we still have to prove:

\begin{lemma}[Surjective pairing]
For any negative arenas $A, B$ and negative single-threaded $\sim$-strategy $\sigma : C \choto A\times B$
we have the weak equivalence:
\[
\sigma \simeq \tuple{\varpi_A \odot \sigma, \varpi_B \odot \tau}
\]
\end{lemma}
\begin{proof}
Let us write $\sigma : \S \to \oc C^\perp \parallel \oc (A\times B)$. By condition \emph{(1)} of
single-threadedness, each event $s\in S$ has a unique minimal dependency $s'\in S$. By negativity
of arenas and strategies $s'$ must map either to $A$ (more formally to an event of the form
$\{(1, a) \mapsto n\}$ for $a\in \min(A)$) or to $B$ (more formally to an event of the form
$\{(2, b) \mapsto n\}$ for $b\in \min(B)$). Write $S_A$ for the subset of $S$ comprising
events whose minimal dependency map to $A$, and similarly write $S_B$. Then $S_A$ and
$S_B$ are down-closed, otherwise that would contradict condition \emph{(1)} of 
single-threadedness. Therefore, they are event structures. The same reasoning holds for
symmetries, so we have the decomposition $\S = \S_A \cup \S_B$.

Take $x\in \conf{S}$. For the reason above, $x$ decomposes uniquely in $x_A \cup x_B$,
with $x_A \in \conf{S_A}$ and $x_B \in \conf{S_B}$. From $x_A$ and $x_B$ we can
(by an immediate variation on the neutrality of copycat) build 
$x'_A \in \CC_{\oc A} \odot S$
(composing the $\sim$-strategies $\varpi_A$ -- which has ``internal'' event structure $\CC_{\oc A}$ --
and $\sigma$) and $x'_B \in \CC_{\oc B}\odot S$, so
\[
x'_A \parallel x'_B \in \conf{\CC_{\oc A}\odot S \parallel \CC_{\oc B} \odot T}
\]
which is the event structure for the $\sim$-strategy $\tuple{\varpi_A \odot \sigma, \varpi_B \odot \tau}$.
This operation satisfies by construction the conditions of Lemma \ref{lem:mapification},
so induce a map. The operation lifts smoothly on symmetries, so the map preserves
symmetry as well. This construction preserves the projection to the game on the nose.

Reciprocally take $x'_A \in \CC_{\oc A} \odot S$ and $x'_B \in \CC_{\oc B}\odot S$. Again
by an immediate variation on the neutrality of copycat we can get corresponding
$x_A \in \conf{S}$ and $x_B \in \conf{S}$ in a way preserving the projection to the game,
the covering relation and compatible union of configurations. Now, it actually follows that
$x_A \cup x_B\in \conf{S}$ as well: indeed events in $x_A$ and $x_B$ cannot share their
minimal dependencies, since for $x_A$ they map to $A$ and to $B$ for $x_B$. Therefore
by condition \emph{(2)} of single-threadedness $x_A$ and $x_B$ are compatible. 
The correspondence from $x'_A, x'_B$ to $x_A \cup x_B$ preserves covering and compatible
unions so by Lemma \ref{lem:mapification} induces a map, and one can show that it preserves
symmetry by performing the exact same construction at the level of symmetries. The projection
to the game is again preserved on the nose.

Finally the correspondence generates an isomorphism, since we have only transformed the events
via the correspondence between $\CC_{\oc A} \odot S_A$ and $S_A$, which is an isomorphism.
\end{proof}

So putting all of this together, we have proved

\begin{proposition}
The $\sim$-bicategory $\CHO$ satisfies the laws of a cartesian category up to weak equivalence.
\end{proposition}

\subsection{A cartesian closed category}

$\CHO$ is a sub-$\sim$-bicategory of $\TCG$ which is compact closed, so we could expect
the closed structure of $\CHO$ to correspond to the compact closed structure of $\TCG$; however
we run into the issue that the arena $A^\perp \times B$ is not an object of $\CHO$, since
it is not negative. So we proceed as in \cite{DBLP:journals/iandc/HylandO00}, and replace it with a negative variant where
minimal events of $A^\perp$ are set to depend on minimal events of $B$.


So, we start by recaling the arrow arena construction of \cite{DBLP:journals/iandc/HylandO00}. For two negative arenas $A$ and 
$B$, we define the arrow arena $A\tto B$ as having:
\begin{itemize}
\item Events,
$\{(1, (b, a))\mid a\in A\,\&\,b\in\min(B)\} \cup \{(2, b)\mid b\in B\}$.                                                       \item Causality,
\[
\begin{array}{l}
\{((1, (b,a_1)), (1, (b,a_2)))\mid a_1 \leq a_2\,\&\,b\in\min(B)\} \cup \\
\{((2, b_1), (2, b_2))\mid b_1 \leq b_2\} \cup \\
\{((2, b),(1, (b,a)))\mid a\in A\,\&\, b\in \min(B)\}
\end{array}
\]
\item Polarity, $\pol((1, (b,a))) = -\pol(a)$ and $\pol((2, b)) = \pol(b)$.
\end{itemize}

To show that this gives a closed structure, we need to relate it to the 
compact closed structure of $\TCG$. To that effect, we will now define a map of essps:
\[
\xi_{A, B} : !(A\tto B) \to \oc A^\perp \parallel \oc B
\]
For events $b\in B$ we use $\sharp b$ for the natural number associated to 
$b$ by the countability of $B$. We also use $\tuple{-, -} : \omega^2 \to \omega$
for any injective function; the collision with the pairing operation should not
generate any confusion.

We set:

\[
\begin{array}{rcccl}
\chi_{A, B} &:& \oc (A\tto B) &\to& \oc A^\perp \parallel \oc B\\
&&(\alpha : [(1, (b, a))] \to \omega) &\mapsto& \alpha'\\
&&(\beta : [(2, b)] \to \omega) &\mapsto& \beta'
\end{array}
\]

where:
\[
\begin{array}{rccccl}
\alpha' &:& [a] &\to&\omega\\
&& a' &\mapsto& \tuple{\sharp b, \alpha((2, b)), \alpha((1, (b, a')))} &\text{(if $a'\in \min(A)$)}\\
&& a' &\mapsto& \alpha((1, (b, a'))) &\text{(otherwise)}
\end{array}
\]

and:
\[
\begin{array}{rcccl}
\beta' &:& [b] &\to& \omega\\
&& b' &\mapsto& \beta((2, b'))
\end{array}
\]

With this definition $\chi_{A, B}$ preserves symmetry, is strong-receptive (it
does not change the copy indices of negative events, since minimal events of $A^\perp$ are positive)
and courteous (it only breaks immediate causal links from minimal events of $B$ to minimal
events of $A^\perp$, so from negative to positive). This allows us, from $\sigma : \S \to \oc C^\perp \parallel \oc (A\tto B)$,
to define:
\[
\begin{array}{rcl}
\Phi(\sigma) &:& \S \to \oc C^\perp \parallel (\oc A^\perp \parallel \oc B)\\
&=& (\oc C^\perp \parallel \chi_{A, B})\circ \sigma
\end{array}
\]
Reciprocally, we can go in the other direction using the following lemma.

\begin{lemma}
Any single-threaded map of ess $\sigma : \S \to \oc C^\perp \parallel (\oc A^\perp \parallel \oc B)$
such that minimal events of $\S$ map to $\oc B$ (as in a negative strategy in the presence of polarities)
factors uniquely through $\oc C^\perp \parallel \chi_{A, B}$ up to weak equivalence.
\label{lem:chi_factor}
\end{lemma}
\begin{proof}
We define $\sigma' : \S \to \oc C^\perp \parallel \oc (A\tto B)$.
For $s\in S$, then if $\sigma(s) = (1, \gamma)$ we set $\sigma'(s) = (1, \gamma)$ still.

If $\sigma(s) = (2, (2, \beta))$ with $\beta : [b] \to \omega$, then we set $\sigma'(s) = (2, \beta')$ with
\[
\begin{array}{rcccl}
\beta' &:& [(2, b)] &\to& \omega\\
&& (2, b') &\mapsto& \beta(b')
\end{array}
\]

If $\sigma(s) = (2, (1, \alpha))$ with $\alpha : [a] \to \omega$, then by condition \emph{(1)} of single-threadedness there is a
unique minimal $s' \leq s$. Since $S$ is negative, $s'$ must be negative as well, but the only negative
minimal events of $\oc C^\perp \parallel (\oc A^\perp \parallel \oc B)$ have the form $(2, (2, \beta))$
with $\beta = \{b\mapsto n\}$. Therefore we set:
\[
\begin{array}{rcccl}
\alpha' &:& [(1, (b, a))] &\to& \omega\\
&& (1, (b, a')) &\mapsto& \alpha(a')\\
&& (2, b) &\mapsto& n
\end{array}
\]
and we define $\sigma'(s) = (2, \alpha')$.

It is routine to check that this preserves symmetry, is strong-receptive and courteous, and that its composition with
$\chi_{A, B}$ is weakly equivalent to $\sigma$ -- copy indices have been heavily modified, but labels and causal dependency
remains the same. Uniqueness up to symmetry follows from the fact that arena labels have to be preserved, and the dependency
annotations in $\oc (A\tto B)$ are forced by the causality in $S$. Only copy indices can be modified, and they do not
matter up to symmetry.
\end{proof}

From that, we deduce the following.

\begin{proposition}
There is a bijection $\Phi$ up to weak equivalence, preserving and reflecting weak equivalence, between:
\begin{itemize}
\item Negative, single-threaded $\sim$-strategies $\sigma : \S \to \C^\perp \parallel \oc (A\tto B)$,
\item Negative, single-threaded $\sim$-strategies $\sigma' : \S \to \C^\perp \parallel (\oc A^\perp \parallel \oc B)$.
\end{itemize}
Moreover this bijection is compatible with pre-composition: for all $\tau : \T \to \oc D^\perp \parallel \oc C$, 
we have:
\[
\Phi(\sigma)\odot \tau \simeq \Phi(\sigma \odot \tau)
\]
\end{proposition}
\begin{proof}
On the one hand $\Phi(\sigma)$ is obtained as $(\oc C^\perp \parallel \chi_{A, B})\circ \sigma$, while
$\Phi^{-1}(\sigma')$ is obtained by the unique factorisation of Lemma \ref{lem:chi_factor}. The bijection 
up to weak equivalence follows from Lemma \ref{lem:chi_factor} as well.

To check that $\Phi$ commutes with composition, we consider the two following pullbacks:
\[
\xymatrix@C=30pt@R=10pt{
\P
        \pb{315}
        \ar[d]
        \ar[r]&
\T\parallel \oc (A \tto B)
        \ar[d]^{\tau \parallel \oc (A \tto B)}\\
\oc D\parallel \S
        \ar[r]^{\oc D\parallel \Phi(\sigma)}&
\oc D\parallel \oc C \parallel \oc (A\tto B)
}
\hspace{10pt}
\xymatrix@C=30pt@R=10pt{
\P'
        \pb{315}
        \ar[d]
        \ar[r]&
\T\parallel (\oc A^\perp \parallel \oc B)
        \ar[d]^{\tau \parallel (\oc A^\perp\parallel \oc B)}\\
\oc D\parallel \S
        \ar[r]^{\oc D\parallel \sigma}&
\oc D\parallel \oc C \parallel (\oc A^\perp \parallel \oc B)
}
\]
The maps:
\begin{eqnarray*}
\T\parallel \chi_{A, B} &:& \T\parallel \oc (A\tto B) \to \T \parallel (\oc A^\perp \parallel \oc B)\\
\oc D\parallel \S &:& \oc D\parallel \S \to \oc D\parallel \S\\
\oc D\parallel \oc C \parallel \chi_{A, B} &\to& \oc D\parallel \oc C \parallel \oc A^\perp \parallel \oc B
\end{eqnarray*}
map the base of the left hand side pullback to the base of the right
hand side pullback, which generate a map $h:\P\to \P'$. Reciprocally, we
have seen in the proof of Lemma \ref{lem:comp_wt} that the composition
pullback $\P'$ is single-threaded. Using that observation, we can define
maps from $\P'$ to $\T {\parallel} \oc (A \tto B)$ as in Lemma \ref{lem:chi_factor}.
This map along with the identity on $\oc D {\parallel} \S$ induces
an inverse $h^{-1} : \P' {\rightarrow} \P$ for $h$.  
It follows from uniqueness in Lemma \ref{lem:chi_factor} that
$h$ and $h'$ are inverse of each other up to symmetry, yielding a weak equivalence.
After projection to visible events, this gives a weak equivalence
between $\tau \odot \Phi(\sigma)$ and $\Phi(\tau \odot \sigma)$.
\end{proof}

From that, it is now straightforward to deduce the cartesian closed structure.

\begin{theorem}
The $\sim$-bicategory $\CHO$ satisfies the laws of a cartesian closed category up to weak equivalence.
\end{theorem}
\begin{proof}
We already know that it is cartesian.

Firstly, evaluation is defined as:
\[
\begin{array}{rcl}
ev_{A, B}  &:& A \times (A\tto B) \choto B\\
                &=& \lift{\lambda_{\oc A^\perp}^{-1}}\odot \epsilon_{\oc A} \odot \lift{\alpha_{\oc A^\perp, \oc A, \oc B^\perp}} \odot (\oc A \parallel_s \Phi(\cc_{\oc (A\tto B)}))\odot \lift{\gamma_{A^\perp, (A\tto B)^\perp}^{-1}}
\end{array}
\]
Likewise curryfication of $\sigma : \S \to \oc (A\times C)^\perp \parallel \oc B$ is obtained by:
\[
\begin{array}{rcl}
\Lambda(\sigma) &:& \oc C \choto \oc (A\tto B)\\
                        &=& \Phi((\oc A^\perp \parallel_s (\sigma \odot \lift{\gamma_{A^\perp, C^\perp}}))\odot \lift{\alpha_{\oc A^\perp \parallel \oc A^\perp \parallel \oc C}^{-1}}\odot (\eta_{\oc A} \parallel_s \oc C))
\end{array}
\]
The required verifications are routine calculations, using the fact that $\Phi$ is a bijection
and the compact closed structure of $\CGS$ -- all the structural isomorphisms eliminate each other.
%There are two equations to check. First, $\beta$-reduction. Take $\sigma : \oc (A \parallel C) \profto B$. We calculate:
%
%\begin{eqnarray*}
%&&ev_{A, B}^\CHO \odot (A \parallel^\CHO \Lambda^\CHO(\sigma))\\
%&=& ev_{A, B} \odot (\oc A \parallel_s (\lift{\zeta_{A, B}^{-1}})) \odot \lift{\gamma_{A, A\toplus B}^{-1}}
%\odot \lift{\gamma_{A, A\toplus B}}\odot (\oc A \parallel_s \lift{\zeta_{A, B}}\odot \Lambda(\sigma \odot \lift{\gamma_{A, C}})) \odot \lift{\gamma_{A, C}^{-1}}\\
%&=& \sigma
%\end{eqnarray*}
%Then, $\eta$-expansion. From $\sigma : \oc C \profto \oc (A\toplus B)$
%\begin{eqnarray*}
%&& \Lambda^\CHO(ev_{A, B}^\CHO \odot (A \parallel^\CHO \sigma))\\
%&=& \lift{\zeta_{A, B}} \odot \Lambda(ev_{A, B} \odot (\oc A \parallel_s (\lift{\zeta_{A, B}^{-1}})) \odot \lift{\gamma_{A, A\toplus B}}^{-1} \odot \lift{\gamma_{A, A\toplus B}}\odot (\oc A \parallel_s \sigma) \odot \lift{\gamma_{A, C}^{-1}} \odot \lift{\gamma_{A, C}})\\
%&=& \lift{\zeta_{A, B}} \odot \Lambda(ev_{A, B} \odot (\oc A \parallel_s (\lift{\zeta_{A, B}^{-1}})) \odot (\oc A \parallel_s \sigma))\\
%&=& \sigma
%\end{eqnarray*}
\end{proof}


%\subsection{Recursion}
%%The goal of this subsection is to show that we can build some
%%fixpoints inside $\CHO$. To do we mimic the usual proof using limits of
%%chain in a domain. To do so, we consider the inclusion order on
%%strategies which makes the construction very easy, mainly by building
%%the limit in sets. However this does not make a domain since there is
%%no least element, so we have more of a \emph{domain forest}. However,
%%every element lie above the minimal strategy, up to isomorphism. 
%%
%%Since this order is obviously not preserved by 2-simulation, we work
%%with explicit representation of strategies in this section.
%
%\subsubsection{A dcpo of $\sim$-strategies}
%
%We compute least upper bounds of $\sim$-strategies using this concrete partial ordering:
%
%\begin{definition}[Inclusion] Let $\A, \B$ be event structures with
%  symmetries and polarities. We say that $\A \inc \B$ whenever $A\subseteq B$, 
%  all data on $\A$ (causality, consistency, polarities, symmetry) is the restriction of that of $\B$,
%  and the inclusion induces a map of essps $\A\hookrightarrow \B$ (so $A$ is down-closed in $B$).
%\end{definition}
%
%The relation $\inc$ is clearly a partial order on event structures with symmetry and
%polarities. We set:
%
%\begin{definition}[Inclusion of $\sim$-strategies]
%  Let ${\sigma} : \S {\rightarrow} \A$ and ${\tau} : \T {\rightarrow} \A$
%  be strategies. We say that ${\sigma} \inc {\tau}$ when $\S \inc \T$
%  and for all $s {\in} S, {\sigma}(s) = {\tau}(s)$.
%\end{definition}
%
%This partial order on $\sim$-strategies is directed complete. Indeed if $\mathbb{D}$ is a 
%directed set of $\sim$-strategies on a cgs $\A$, then we define:
%\[
%\begin{array}{rcl}
%\bigsqcup_{(\sigma : \S \to \A) \in \mathbb{D}} \sigma &:& (\bigcup_{(\sigma : \S \to \A)\in \mathbb{D}} \S) \to \A
%\end{array}
%\]
%It is direct to check that this defines a $\sim$-strategy, which is a least upper bound for $\mathbb{D}$. 
%Additionally if $\sim$-strategies in $\mathbb{D}$ are negative or single-threaded, this is still the case
%of $\bigsqcup \mathbb{D}$.
%
%So, $\inc$ equips the set of $\sim$-strategies with a structure of dcpo. It does not
%have a least element though: a minimal strategy $\sigma : \S \to \A$ contains exactly
%events in $\S$ for the initial negative segment of $\A$ by receptivity, but can give
%arbitrary names for those.
%
%We pick one distinguished minimal $\sim$-strategy on a cgs $\A$. Let us write $\A^-$ for the 
%initial negative segment of $\A$ -- the maximal purely negative cgs such that $\A^- \inc \A$ 
%(not to be confused with the negative thin sub-symmetry $\A_-$). We set:
%\[
%\bot_\A : \A^- \to \A
%\]
%acting as the identity map. Clearly $\bot_\A$ is a $\sim$-strategy, negative and single-threaded, 
%and is minimal for $\inc$ because anything strictly smaller would fail receptivity.
%
%Every strategy is isomorphic to such a strategy:
%
%\begin{lemma}
%  Let ${\sigma} : \S {\rightarrow} \A$ be a strategy. There exists a
%  strategy $\sigma^\dagger : \S^\dagger {\rightarrow} \A$ isomorphic to
%  ${\sigma}$ such that $\bot_A \inc {\sigma^\dagger}$.
%\end{lemma}
%\begin{proof}
%  By receptivity $S$ contains an initial segment isomorphic to the
%  minimal negative events of $A$. $\S^\dagger$ is obtained by replacing
%  those events by the corresponding events of $A$, and renaming the
%  other events of $\S$ to avoid any potential collision. It is routine to
%  check that we get an isomorphic strategy on $A$ and we clearly have
%  ${\sigma} {\cong} {\sigma}^\dagger$.
%\end{proof}
%%Moreover, we have limits wrt $\inc$.
%%\begin{lemma}
%%  Let $({\sigma}_i : \S_i {\rightarrow} \A)$ be a family of strategies
%%  on $\A$ such that ${\sigma}_i \inc {\sigma}_{i+1}$ for all $i {\in}
%%  {\mathbb{N}}$.  Then there exists ${\sigma} : \S {\rightarrow} \A$
%%  which is the least upper bound of the chain $({\sigma}_i)$.
%%\end{lemma}
%%\begin{proof}
%%  We define $S = \bigcup_{i {\in} {\omega}} S_i$. Causality, and
%%  coherence are inherited from the $S_i$ (coherence is well defined
%%  because it only speaks of finite sets). Symmetry is dealt in a
%%  similar way. It is automatically thin. Because the inclusion commute
%%  in the game, we can define ${\sigma} : S {\rightarrow} A$ as sending
%%  $s$ to ${\sigma}_i(s)$ where $i$ is such that $s {\in} S_i$ (it does not
%%  matter which one by definition of the inclusion).
%%
%%  If there is a strategy ${\tau} : \T {\rightarrow} \A$ such that for all $i {\in} {\mathbb{N}}, {\sigma}_i
%%  \inc {\tau}$, we have that $\S_i \inc \T$ so $\S \inc \T$ and it follows that
%%  ${\sigma} \inc {\tau}$. So ${\sigma}$ is the desired limit.
%%\end{proof}
%%${\sigma}$ is denoted $\bigcup_{n {\in} {\omega}} {\sigma}_n$. As a
%%result, restricting to the strategies that share the minimal events of
%%the game, we obtain a domain. (We get a domain for any choice of the
%%representation of the minimal negative events of the game).
%%
%%\begin{corollary}
%%  The set $Dom(A, B) = \{ {\sigma} {\in} \CHO(A, B) \ |\ \bot \inc {\sigma} \}$ is a domain.
%%\end{corollary}
%
%The main operations we have for constructing strategies are continuous:
%
%\begin{lemma}
%  Composition, parallel composition, pairing, curryfication and the $(-)^\dagger$ operation 
%  introduced just above are continuous for $\inc$.
%\label{lem:opcont}
%\end{lemma}
%\begin{proof}
%  Direct.
%\end{proof}
%
%\subsubsection{Fixpoint combinator in $\CHO$}
%
%We are now ready to prove that there is a fixpoint combinator in $\CHO$. For $\A$ a cgs, 
%we write $\D_\A$ for the pointed dcpo of negative single-threaded $\sim$-strategies above
%$\bot_\A$. We consider the following operation on $\D_{\oc(A\tto A)^\perp \parallel \oc A}$:
%
%\[
%F(\sigma) = {\left((A \Rightarrow A) \xrightarrow{{\langle}\sigma, {\id_{A\tto A}}{\rangle}} A \times (A \Rightarrow A) \xrightarrow{ev_{A, A}} A\right)}^{\dagger}
%\]
%
%By Lemma \ref{lem:opcont}, $F$ is continuous and because of the
%outermost dagger, it has indeed value in $\D_{\oc (A\tto A)^\perp \parallel \oc A}$.
%Therefore, we can take its fixpoint:
%\[
%\Fix_A \in D_{\oc (A\tto A)^\perp \parallel \oc A}
%\]
%
%By construction, it satisfies
%
%\[ 
%\Fix_A \simeq ev_{A, A} \odot \tuple{\Fix, \id_{A\tto A}} : (A \Rightarrow A) \choto A
%\]
%
%  As a consequence, we have:
%\begin{corollary}\label{lemma:fixeqn}
%  Let $\sigma : \Gamma \choto A\tto A$. Then, 
%\[
%\Fix_A \odot \sigma \simeq ev_{A, A} \odot \tuple{\Fix_A \odot \sigma, \sigma} : \Gamma \choto A
%\]
%\end{corollary}
%\begin{proof}
%Direct using the equation above and the cartesian closed laws.
%%  \begin{aligned}
%%   \Fix {\odot} {\sigma} {\simeq} ev {\odot} {\langle}id, \Fix{\rangle} {\odot} {\sigma} {\simeq} ev {\odot} {\langle}{\sigma}, \Fix {\odot} {\sigma}{\rangle} {\simeq} {\Lambda}^{-1} {\sigma} {\odot} {\langle}id, \Fix {\odot} {\sigma}{\rangle}
%%  \end{aligned}$$
%\end{proof}

\subsection{Recursion}

\subsubsection{A dcpo of $\sim$-strategies}

We compute least upper bounds of $\sim$-strategies using this concrete partial ordering:

\begin{definition}[Inclusion] Let $\A, \B$ be event structures with
  symmetry and polarities. We say that $\A \inc \B$ whenever $A\subseteq B$,
  all data on $\A$ (causality, consistency, polarities, symmetry) is the restriction of that of $\B$,
  and the inclusion induces a map of essps $\A\hookrightarrow \B$ (so $A$ is down-closed in $B$).
\end{definition}

The relation $\inc$ is clearly a partial order on event structures with symmetry and
polarities. We set:

\begin{definition}[Inclusion of $\sim$-strategies]
  Let ${\sigma} : \S {\rightarrow} \A$ and ${\tau} : \T {\rightarrow} \A$
  be strategies. We say that ${\sigma} \inc {\tau}$ when $\S \inc \T$
  and for all $s {\in} S, {\sigma}(s) = {\tau}(s)$.
\end{definition}

This partial order on $\sim$-strategies is directed complete. Indeed if $\mathbb{D}$ is a
directed set of $\sim$-strategies on a cgs $\A$, then we define:
\[
\begin{array}{rcl}
\bigsqcup_{(\sigma : \S \to \A) \in \mathbb{D}} \sigma &:& (\bigcup_{(\sigma : \S \to \A)\in \mathbb{D}} \S) \to \A
\end{array}
\]
It is direct to check that this defines a $\sim$-strategy, which is a least upper bound for $\mathbb{D}$.
Additionally if $\sim$-strategies in $\mathbb{D}$ are negative or single-threaded, this is still the case
of $\bigsqcup \mathbb{D}$.

So, $\inc$ equips the set of $\sim$-strategies with a structure of dcpo. It does not
have a least element though: a minimal strategy $\sigma : \S \to \A$ has as events in $\S$ an initial
negative segment corresponding to that of $\A$, so there are as many minimal strategies as possible
renamings of this segment.

We pick one distinguished minimal $\sim$-strategy on a cgs $\A$. Let us write $\A^-$ for the
initial negative segment of $\A$: the maximal purely negative cgs such that $\A^- \inc \A$
(not to be confused with the negative thin sub-symmetry $\A_-$). We set:
\[
\bot_\A : \A^- \to \A
\]
acting as the identity map. Clearly $\bot_\A$ is a $\sim$-strategy, negative and single-threaded,
and is minimal for $\inc$ because anything strictly smaller would fail receptivity.

Every strategy is isomorphic to a strategy lying over $\bot_\A$:

\begin{lemma}
  Let ${\sigma} : \S {\rightarrow} \A$ be a strategy. There exists a
  strategy $\sigma^\dagger : \S^\dagger {\rightarrow} \A$ isomorphic to
  ${\sigma}$ such that $\bot_A \inc {\sigma^\dagger}$.
\end{lemma}
\begin{proof}
  By receptivity $S$ contains an initial segment isomorphic to the
  minimal negative events of $A$. $\S^\dagger$ is obtained by replacing
  those events by the corresponding events of $A$, and renaming the
  other events of $\S$ to avoid any potential collision. It is routine to
  check that we get an isomorphic strategy on $A$ and we clearly have
  ${\sigma} {\cong} {\sigma}^\dagger$.
\end{proof}
%Moreover, we have limits wrt $\inc$.
%\begin{lemma}
%  Let $({\sigma}_i : \S_i {\rightarrow} \A)$ be a family of strategies
%  on $\A$ such that ${\sigma}_i \inc {\sigma}_{i+1}$ for all $i {\in}
%  {\mathbb{N}}$.  Then there exists ${\sigma} : \S {\rightarrow} \A$
%  which is the least upper bound of the chain $({\sigma}_i)$.
%\end{lemma}
%\begin{proof}
%  We define $S = \bigcup_{i {\in} {\omega}} S_i$. Causality, and
%  coherence are inherited from the $S_i$ (coherence is well defined
%  because it only speaks of finite sets). Symmetry is dealt in a
%  similar way. It is automatically thin. Because the inclusion commute
%  in the game, we can define ${\sigma} : S {\rightarrow} A$ as sending
%  $s$ to ${\sigma}_i(s)$ where $i$ is such that $s {\in} S_i$ (it does not
%  matter which one by definition of the inclusion).
%
%  If there is a strategy ${\tau} : \T {\rightarrow} \A$ such that for all $i {\in} {\mathbb{N}}, {\sigma}_i
%  \inc {\tau}$, we have that $\S_i \inc \T$ so $\S \inc \T$ and it follows that
%  ${\sigma} \inc {\tau}$. So ${\sigma}$ is the desired limit.
%\end{proof}
%${\sigma}$ is denoted $\bigcup_{n {\in} {\omega}} {\sigma}_n$. As a
%result, restricting to the strategies that share the minimal events of
%the game, we obtain a domain. (We get a domain for any choice of the
%representation of the minimal negative events of the game).
%
%\begin{corollary}
%  The set $Dom(A, B) = \{ {\sigma} {\in} \CHO(A, B) \ |\ \bot \inc {\sigma} \}$ is a domain.
%\end{corollary}

The main operations we have for constructing strategies are continuous:

\begin{lemma}
  Composition, parallel composition, pairing, curryfication and the $(-)^\dagger$ operation
  introduced just above are continuous for $\inc$.
\label{lem:opcont}
\end{lemma}
\begin{proof}
  Direct.
\end{proof}


\subsubsection{Fixpoint combinator in $\CHO$}

We are now ready to prove that there is a fixpoint combinator in $\CHO$. For $\A$ a cgs,
we write $\D_\A$ for the pointed dcpo of negative single-threaded $\sim$-strategies above
$\bot_\A$. We consider the following operation on $\D_{\oc(A\tto A)^\perp \parallel \oc A}$:

\[
F(\sigma) = {\left((A \Rightarrow A) \xrightarrow{{\langle}\sigma, {\id_{A\tto A}}{\rangle}} A \times (A \Rightarrow A) \xrightarrow{ev_{A, A}} A\right)}^{\dagger}
\]

By Lemma \ref{lem:opcont}, $F$ is continuous and because of the
outermost dagger, it has indeed value in $\D_{\oc (A\tto A)^\perp \parallel \oc A}$.
Therefore, we can take its fixpoint:
\[
\Fix_A \in D_{\oc (A\tto A)^\perp \parallel \oc A}
\]

By construction, it satisfies

\[ 
\Fix_A \simeq ev_{A, A} \odot \tuple{\Fix, \id_{A\tto A}} : (A \Rightarrow A) \choto A
\]

  As a consequence, we have:
\begin{corollary}\label{lemma:fixeqn}
  Let $\sigma : \Gamma \choto A\tto A$. Then,
\[
\Fix_A \odot \sigma \simeq ev_{A, A} \odot \tuple{\Fix_A \odot \sigma, \sigma} : \Gamma \choto A
\]
\end{corollary}
\begin{proof}
Direct using the equation above and the cartesian closed laws.
%  \begin{aligned}
%   \Fix {\odot} {\sigma} {\simeq} ev {\odot} {\langle}id, \Fix{\rangle} {\odot} {\sigma} {\simeq} ev {\odot} {\langle}{\sigma}, \Fix {\odot} {\sigma}{\rangle} {\simeq} {\Lambda}^{-1} {\sigma} {\odot} {\langle}id, \Fix {\odot} {\sigma}{\rangle}
%  \end{aligned}$$
\end{proof}

Using this structure, one can follow the lines of \cite{DBLP:journals/iandc/HylandO00} and
define the interpretation of PCF in $\CHO$. Of course, $\sim$-strategies in $\CHO$ have many more
possible behaviours than those coming from terms of PCF, including complex concurrent and non-deterministic
behaviours, but also behaviours typically associated with stateful computation. 

In the final subsection we show however how to define in $\CHO$ a subcategory corresponding exactly to the
cartesian closed category from \cite{DBLP:journals/iandc/HylandO00} of deterministic innocent strategies (modulo the
Questions/Answers distinction).


\subsection{Embedding of standard Hyland-Ong innocent strategies}

In this final subsection, we construct a sub-$\sim$-bicategory $\CHOInn$ of $\CHO$ whose quotient under weak equivalence
is isomorphic to the standard category of arenas and innocent strategies. We will first recall the basic definitions
of the usual category $\Inn$ of arenas and innocent strategies, and then relate $\Inn$ and $\CHOInn$.

\subsubsection{The category $\Inn$}

%We keep the same definition of arenas \rkPierre{Remove questions/answers} as in the previous sections \rkPierre{Write $\vdash$ for
%causality in the arena.}. We give no proof.

This section is mainly there for reference and to fix the notions and notations. The construction is
standard, so we only give the definitions and the properties, but skip all proofs. From now on, all arenas are
considered negative.

\paragraph{Plays, strategies.} First, we recall the notions of plays and strategies on an arena.

\begin{definition}
Let $\Sigma$ be an alphabet. A \textbf{pointing string} on $\Sigma$ is a sequence $m_0 m_1 \dots m_n$ of elements of $\Sigma$
when each $m_i$ may be equipped with a \emph{pointer} to an earlier $m_j$ (\emph{i.e.} $j < i$). In that case we write
$m_i \to m_j$. 
\end{definition}

\begin{definition}
Let $m$ be a pointing string on $\Sigma$, and $\Sigma' \subseteq \Sigma$. The the restriction $m' = m\restrict \Sigma'$ of
$m$ to $\Sigma'$ is obtained by removing in $m$ all moves from $\Sigma \setminus \Sigma'$. The move $m'_i$ points to $m'_j$
if there is a pointer chain between the corresponding moves in $m$, passing only through $\Sigma \setminus \Sigma'$.

The definition extends trivially if $\Sigma' \hookrightarrow \Sigma$ is an injection instead of an inclusion.
\end{definition}

\paragraph{Notations.} We write $|m|$ for the length of $m$, $m'\sqsubseteq m$ for the prefix ordering, $m'\sqsubseteq^P m$
if additionally $m'$ is $P$-ending. 

\begin{definition}
If $A$ is an arena, then a \textbf{legal play} on $A$ is a pointing string $m$ on $A$ such that:
\begin{itemize}
\item If $m_i$ has no pointer, then $m_i \in \min(A)$,
\item If $m_i \to m_j$, then $m_j \vdash_A m_i$,
\item For all $0 \leq i \leq |m|-2$, $\pol(m_i) \neq \pol(m_{i+1})$.
\end{itemize}
Let $\leg{A}$ be the set of legal plays on $A$.
\end{definition}

\begin{definition}
A \textbf{(deterministic) strategy} $\ssigma : A$ on $A$ is a non-empty, Opponent-branching, even-prefix closed set of even-length legal
plays on $A$.
\end{definition}

\paragraph{Copycat, composition.}

\begin{definition}
The copycat strategy is defined by:
\[
\id_A = \{m\in \leg{A_1\tto A_2} \mid \forall m'\sqsubseteq^P m, m'\restrict A_1 = m'\restrict A_2\}
\]
\end{definition}

\begin{definition}
Let $\ssigma : A\tto B$ and $\stau : B \tto C$ be two strategies. Their \textbf{interaction} is:
\[
\ssigma \parallel \stau = \{u\in (A\tto B)\tto C\mid u\restrict A, B \in \ssigma \& u\restrict B, C\in \stau \& u \restrict A, C \in \leg{A\tto C}\}
\]
Their \textbf{composition} is then defined by:
\[
\stau \odot \ssigma = \{u\restrict A, C\mid u \in \ssigma \parallel \stau\}
\]
\end{definition}

It is well-known that composition is associative and forms a category.

\paragraph{Visibility, innocence.}

\begin{definition}
Let $m\in \leg{A}$. Its \textbf{P-view} is defined inductively as follows:
\begin{eqnarray*}
\pview{mi} &=& i\\
\pview{mpm'o} &=& \pview{mp}o\\
\pview{mp} &=& \pview{m}p
\end{eqnarray*}
where in the first line $i\in \min(A)$, in the second $o\to p$ and we have $\pol(o) =-$ and $\pol(p) = +$. Pointers are
preserved if the target of the pointer is in the $P$-view, lost otherwise. 
\end{definition}

For $m\in \leg{A}$, the P-view $\pview{m}$ is in general just a pointing string on $A$; not a legal play since some pointers
might be lost. For a play $m\in \leg{A}$, we say that $m$ \textbf{is a P-view} if $\pview{m} = m$; it is easy to see that
this is equivalent to the fact that Opponent always points to the previous move.

\begin{definition}
Let $m\in \leg{A}$. We say that $m$ is \textbf{P-visible} if for all $m'\sqsubseteq m$, $\pview{m'} \in \leg{A}$. In other
words pointers are not lost when computing the P-view of prefixes of $m$, so Player always points within its P-view.

A strategy $\ssigma : A$ is \textbf{visible} when all its plays are P-visible.
\end{definition}

Visible strategies are stable under composition and form a sub-category of the category of arenas and strategies. We can
now define:

\begin{definition}
Let $\ssigma : A$ be a visible strategy. It is \textbf{innocent} if for all $m, mop, no \in \ssigma$ with 
$\pview{mo} = \pview{no}$, then $nop\in \sigma$ as well (with the same pointer).
\end{definition}

Innocent strategies are stable under composition, and form a CCC. 


From the definition it follows that innocent strategies are entirely characterized by their set of P-views, so to define
an innocent strategy it is sufficient to define a set of P-views, and to compose innocent strategies it is sufficient
to compute only interactions that give rise to P-views.

\subsubsection{The $\sim$-bicategory $\CHOInn$}

Let us now define the sub-$\sim$-bicategory of $\CHO$ corresponding to it. In this section, we consider negative
single-threaded $\sim$-strategies -- however, the conditions introduced here and the corresponding reasonings only
concern the underlying strategy $\sigma : S\to A$ of $\sim$-strategies $\sigma : \S \to \A$, so we will mostly
ignore symmetry in this subsubsection.

We introduce two further conditions: sequential innocence and determinism. 

\begin{definition}
An esp $S$ is \textbf{sequential innocent} iff it is:
\begin{itemize}
\item[(1)] \emph{Backward sequential}: for all $s\in S$, $[s]$ is a total order,
\item[(2)] \emph{Forward sequential}: for all $s\in S$ with $s\imc s_1^+$, $s\imc s_2^+$, then
$[s_1] \cup [s_2] \not \in \conf{S}$.
\end{itemize}
In particular, a strategy $\sigma :S \to A$ is sequential innocent iff $S$ is.
\end{definition}

It is obvious that copycat is sequential innocent, as are maps obtained through lifting. Note that
we call that \emph{sequential innocence} and not just innocence, as we have (in a forthcoming companion paper) a notion of innocence
that accepts strategies with concurrent behaviour such as that for the parallel or.

We now show that backward sequentiality is stable under composition.

\begin{lemma}
Let $\sigma : S \to A$ and $\tau : T \to A^\perp$ be two backward sequential strategies. Then, $S \circledast T$
is backward sequential as well.
\label{lem:pbbs}
\end{lemma}
\begin{proof}
It suffices to show that in $S \circledast T$, each event has at most one immediate causal dependency; but that follows immediately
from Lemma \ref{lem:imc_pullback}, backward sequentiality of $S$ and $T$ and the fact that $A$ is a forest. 
\end{proof}

\begin{proposition}
If $\sigma : S \to A^\perp \parallel B$ and $\tau : T \to B^\perp \parallel C$ are backward sequential, so is 
$\tau \odot \sigma$.
\end{proposition}
\begin{proof}
By Lemma \ref{lem:pbbs}, the composition pullback $S \circledast T$ is backward sequential as well. From that it follows from 
a straightforward induction that events in $T \odot S$ have at most one predecessor as well, so $\tau \odot \sigma$ is
backward sequential.
\end{proof}

We now show that forward sequentiality is stable under composition.

\begin{lemma}
Let $\sigma : S \to A^\perp \parallel B$ and $\tau : T \to B^\perp \parallel C$ be forward sequential. Then,
$\tau \odot \sigma$ is forward sequential as well.
\end{lemma}
\begin{proof}
Let $c\imc_{T\odot S} c_1^+, c_2^+$. By definition of projection, we must have:
\[
\xymatrix@C=5pt{
&&&&[(s_{i+1}, t_{i+1})]_{x_1}\ar[r]&\dots\ar[r]&[(s_n,t_n)]_{x_1} \ar[r]&c_1\\
c \ar[r]& [(s_1, t_1)]_x \ar[r]& \dots \ar[r]& [(s_i, t_i)]_x \ar[ur]\ar[dr]\\
&&&&[(s'_{i+1}, t'_{i+1})]_{x_2}\ar[r]&\dots\ar[r]&[(s'_p,t'_p)]_{x_2} \ar[r]&c_2
}
\]
in the interaction pullback $P = (S\parallel C) \circledast (A\parallel T)$. Suppose wlog that $\pol(s_i) = -$. By
Lemma \ref{lem:imc_pullback},
we either have $s_i \imc s_{i+1}$ or $t_i \imc t_{i+1}$. But if $t_i \imc t_{i+1}$, then $\tau t_i \imc \tau t_{i+1}$ as well
by courtesy. It follows that $s_i \leq s_{i+1}$, but necessarily $s_i \imc s_{i+1}$ otherwise that would contradict
$[(s_i, t_i)]_{x_1} \imc [(s_{i+1}, t_{i+1})]_{x_1}$. For the same reason, $s_i \imc s'_{i+1}$ as well. Therefore by forward
sequentiality of $\sigma$, $[s_{i+1}] \cup [s'_{i+1}] \not \in \conf{S}$. But $c_1 \cup c_2$ must contain 
$[s_{i+1}] \cup [s'_{i+1}]$, so cannot be a valid configuration of the pullback -- so $[c_1]_{T\odot S} \cup [c_2]_{T\odot S}
\not \in \conf{T\odot S}$.
\end{proof}

So, we have a bicategory of sequential innocent strategies. All these constructions being orthogonal with 
symmetry, we also have a $\sim$-bicategory of thin concurrent games and sequential innocent strategies -- and
a $\sim$-bicategory of negative arenas and sequential innocent strategies. Strategies obtained by lifting are sequential
innocent and it is preserved by ccc operations, hence there is a $\sim$-bicategory satisfying ccc laws up to weak 
equivalence of negative arenas and single-threaded sequential innocent strategies.

\begin{definition}
For $A$ a conflict-free esp, a strategy $\sigma : S \to A$ is \textbf{deterministic} iff any finite
subset of $S$ is consistent.
\end{definition}

This is not the standard definition of deterministic concurrent strategies (for that, see \cite{DBLP:journals/fac/Winskel12}), but it 
is a specialization of it in a case -- such as here -- when the games are conflict-free.
Clearly copycat on a conflict-free game is deterministic in the sense above.
For self-completeness, we prove that deterministic strategies are stable under composition.

\begin{lemma}
Let $A$ be a conflict-free esp, 
and let $\sigma : S \to A$ and $\tau : T \to A^\perp$ be deterministic. Then, every finite subset of $S\circledast T$
is consistent. Therefore, deterministic strategies are stable under composition.
\end{lemma}
\begin{proof}
First, note that since all finite subsets of events of $S$ and $T$ are consistent it follows that $\sigma$ and
$\tau$ are injective. Thefore for any $s\in S$, there is at most one $t\in T$ such that $\sigma s = \tau t$.
Take a finite set of configurations of $S\circledast T$, represented as secured bijections:
\[
x_i \stackrel{\sigma}{\iso} \sigma x_i = \tau y_i \stackrel{\tau}{\iso} y_i
\]
for $1 \leq i \leq n$. From the observation above, we have that
\[
\cup_{1\leq i _leq n} x_i \stackrel{\sigma}{\iso} \sigma(\cup_{1\leq i \leq n} x_i) = \tau(\cup_{1\leq i \leq n} y_i) \stackrel{\tau}{\iso} \cup_{1\leq i \leq n} y_i
\]
is still a bijection. Since $x_i$ and $y_i$, as configurations of respectively $S$ and $T$, are down-closed, it immediately
follows that this bijection is secured, making it a configuration of $S\circledast T$ corresponding to the union of
the confiurations of $S\circledast T$ that we started with. It also follows that all finite sets of events of the projection
are consistent, hence deterministic strategies are stable under composition.
\end{proof}

Note that although non-deterministic sequential innocent $\sim$-strategies are not automatically single-threaded -- they might
fail condition (2) of single-threadedness, deterministic sequential innocent $\sim$-strategies automatically are
and therefore form a sub-$\sim$-bicategory of $\CHO$ satisfying the equations of a ccc up to weak equivalence.
We call this $\sim$-bicategory $\CHOInn$.

\subsubsection{Relating $\CHOInn$ and $\Inn$}

\paragraph{From $\CHOInn$ to $\Inn$.}
First, let us show how to associate an innocent strategy in the usual Hyland-Ong sense to any negative deterministic
sequential innocent $\sim$-strategy $\sigma : \S \to \oc A^\perp \parallel \oc B$. For the rest of this paragraph,
we fix $\sigma$.

Note first that for any $s\in S$, by sequential innocence $[s]$ is a total order:
\[
s_0 \imc s_1 \imc \dots \imc s_n = s
\]
to which we associate the sequence:
\[
(\lbl (\sigma s_0), \lbl (\sigma s_1), \dots, \lbl (\sigma s_n))
\]
Additionally, this sequence is equipped with pointers by setting $\lbl (\sigma s_i)$ to point to $\lbl (\sigma s_j)$
if, either $\sigma s_j \imc \sigma s_i$, or $j = 0$ and $\sigma s_i$ is minimal in $\oc A$ -- the second case is here because
we started with $\sigma : \S \to \oc A^\perp \parallel \oc B$ rather than $\sigma : \S \to \oc (A\tto B)$. We denote this
pointing sequence by $\P(s)$.


Let us now make a few observations on this pointing sequence. First of all it is alternating: indeed by courtesy $S$
can only enrich the causality of $\oc A^\perp \parallel \oc B$ with causal links from negative to positive events, 
and $\oc A^\perp \parallel \oc B$ is alternating. Moreover, all Opponent moves in $\P(s)$ must point to the previous
move; indeed otherwise there would be $s_j^+, s_k^+, s_i^-$ with $\sigma s_j \imc \sigma s_i$, but
$s_j < s_k \imc s_i$. But by courtesy that would mean that $\sigma s_k \imc \sigma s_i$ as well, so $\sigma s_k = \sigma s_j$
since $\oc A^\perp \parallel \oc B$ is a forest -- contradiction. Moreover all Player moves are equipped with a pointer
(since $[s]\in \conf{S}$, and for any ${s'}^+\leq s$, either $\sigma s'$ is not minimal in $\oc A^\perp \parallel \oc B$
and it has an immediate dependency, or it is minimal in $\oc A^\perp$, in which case it is by definition set to point to
$\lbl (\sigma s_0)$). So we have proved that $\P(s)$ is a P-view.


Now, we are in a position to form:
\[
\P(\sigma) = \{\epsilon\} \cup \{\P(s) \mid s^+\in S\}
\]
obtaining a set of P-ending P-views. We now wish to show that this set of P-views defines an innocent strategy. For that,
it has to be O-branching. For that, we will need the following key lemma.

\begin{lemma}
Let $s, s' \in S$, such that $|[s]| = |[s']|$. Then, the following three propositions are equivalent.
\begin{itemize}
\item[(1)] $\P(s) = \P(s')$,
\item[(2)] The unique order-isomorphism $\theta : [s] \iso [s']$ is in the isomorphism family of $\S$,
\item[(3)] The unique order-isomorphism $\theta : [s] \iso [s']$ is such that $\sigma~\theta$ is in the
isomorphism family of $\oc A^\perp \parallel \oc B$.
\end{itemize}
\label{lem:unique_theta}
\end{lemma}
\begin{proof}
$(1) \Rightarrow (2)$. By induction on $\leq_S$. If $s, s'$ are minimal then since $\lbl (\sigma s) = \lbl (\sigma s')$ they can only
differ on their copy indices. By definition of the isomorphism family of $\oc A^\perp \parallel \oc B$, the unique bijection 
between the singletons $\{\sigma s\}$ and $\{\sigma s'\}$ is a valid isomorphism. Since $\sigma$ is negative,
it follows that the unique bijection between $\{s\}$ and $\{s'\}$ is a valid isomorphism by strong-receptivity.

Now suppose that $[s_1] \stackrel{\theta}{\iso_\S} [s_2]$, and suppose $s_1 \imc s'_1$ and $s_2 \imc s'_2$,
with $\P(s'_1) = \P(s'_2)$. If $\pol(s'_1) = \pol(s'_2) = -$, then the same reasoning as above applies. Suppose now that
$\pol(s'_1) = \pol(s'_2) = +$. By induction hypothesis we have $[s_1] \stackrel{\theta}{\iso_\S} [s_2]$, and
$[s_1] \cov{s'_1}$. By the extension property of isomorphism families, there is $s''_2$ such that 
$\theta \cov{(s'_1, s''_2)}$, writing $\theta' = \theta \cup \{(s'_1, s''_2)\}$. By property of isomorphism families
$\theta'$ is an order-isomorphism, therefore $s_2 \imc s''_2$. By forward sequentiality and determinism of $\sigma$,
we must then have $s'_2 = s''_2$, so the unique order-isomorphism between $[s'_1]$ and $[s'_2]$ is indeed in the
isomorphism family of $\S$.

$(2) \Rightarrow (3)$. Obvious.

$(3) \Rightarrow (1)$. Immediate by definition of $\P$.
\end{proof}

From this lemma, it follows that $\P(\sigma)$ is O-branching. Indeed, suppose we have $s_1 \imc {s'}^+_1$, $s_2 \imc {s'}^+_2$
with $\P(s_1) = \P(s_2)$. From the lemma above, the unique order-isomorphism $\theta$ satisfies 
\[
[s_1] \stackrel{\theta}{\iso_\S} [s_2]
\]
by the extension property of isomorphism families, we must have $\theta\cov{(s'_1, s''_2)}$, so
$[s_2] \cov{s''_2}$. By determinism, forward sequentiality and the fact that $\theta$ is an order-iso,
it follows that $s''_2 = s'_2$. But from that we get by $\sigma$ the iso:
\[
\sigma [s_1] \cup \{\sigma s'_1\} \stackrel{\sigma (\theta_cup \{(s'_1, s'_2)\})}{\iso_{\oc A^\perp \parallel \oc B}} \sigma [s_2] \cup \{\sigma s'_2\}
\]
so by definition of the isomorphism family of $\oc A^\perp \parallel \oc B$, we get that $\sigma s'_1$ and $\sigma s'_2$ have
the same label and dependency in $\oc A^\perp \parallel \oc B$, so $\P(s'_1) = \P(s'_2)$.


So, we have established that $\P(\sigma)$ is a non-empty (by construction) set of even-length P-views, obviously
even-prefix-closed. So, it induces an innocent strategy in the usual Hyland-Ong sense, still written $\P(\sigma)$. 

Let us note in passing that $\P$ is well-defined on weak equivalence classes of strategies. If $\sigma : \S \to \oc A ^\perp 
\parallel \oc B$ and $\sigma' : \S' \to \oc B^\perp \parallel \oc C$ and $\sigma \stackrel{\phi}{\simeq} \sigma'$ is a 
weak equivalence, then $\P(\sigma) = \P(\sigma')$. Indeed for any $s\in S$, it is immediate to check that $\P(s) = \P(\phi(s))$.
We will show later on that the converse also holds: if $\P(\sigma) = \P(\sigma')$, then $\sigma \simeq \sigma'$.

\paragraph{Functoriality of $\P$.} Now we prove that this gives a functor.

\begin{lemma}
For any arena $A$, we have:
\[
\P(\cc_{\oc A}) = \id_A
\]
\end{lemma}
\begin{proof}
$\subseteq$. By immediate induction on $\leq_A$, for any $s\in \CC_{\oc A}$, for any $m'\sqsubseteq^P \P(s)$ we
have $m'\restrict A_1 = m'\restrict A_2$ (where $\id_A : A_1 \tto A_2$ is labeled for convenience).

$\supseteq$. From $m$ a P-ending P-view in $\id_A$, we have $m\restrict A_1 = m\restrict A_2$. Suppose wlog that 
the last move of $m$ is in $A_1$. In fact (by property of P-views of copycat) $m\restrict A_1$ must be a pointer chain, 
hence we obtain $\alpha^+\in \oc A^\perp$ by adding an arbitrary choice of copy indices. By construction we have
$\P((1, \alpha)) = m$.
\end{proof}

\begin{lemma}
For all $\sigma : \S \to \oc A^\perp \parallel \oc B$ and $\tau : T \to \oc B^\perp \parallel \oc C$ negative 
deterministic sequential innocent $\sim$-strategies, we have:
\[
\P(\tau \odot \sigma) = \P(\tau) \odot \P(\sigma)
\]
\end{lemma}
\begin{proof}
Let $P = (S \parallel \oc C) \circledast (\oc A \parallel T)$ be the pullback involved in the composition of
$\sigma$ and $\tau$. For $p\in P$, by Lemma \ref{lem:pbbs} $[p]$ is a total order:
\[
p_0 \imc p_1 \imc \dots \imc p_n = p
\]
We define $\P(p)$ similarly to the corresponding definition on strategies, as the sequence
\[
(\lbl ((\sigma \circledast \tau) p_0), \dots, \lbl ((\sigma \circledast \tau) p_n))
\]
with the pointers defined by causality in $\oc A \parallel \oc B \parallel \oc C$ for events that are non-minimal
in the game, $\lbl ((\sigma \circledast \tau) p_0)$ for moves minimal in $\oc B$. For $\lbl ((\sigma \circledast \tau) p_i)$
minimal in $\oc A$, necessarily $\Pi_1 p_i \in S$ is positive, and hence $[\Pi_1 \pi_i]_S$ has a unique minimal event
corresponding to some $\Pi_1 p_j$; then $\lbl ((\sigma \circledast \tau) p_i)$ is set to point
to $\lbl ((\sigma \circledast \tau) p_j)$.


Let $P_n$ be its restriction to events whose causal history has exactly $n$ events. 
Likewise for $\ssigma : A\tto B$ and $\stau : B \tto C$ two innocent strategies in the Hyland-Ong sense,
let $\sigma \parallel_n \tau$ be the similarly restricted interaction, comprising pointing strings $u$ on $(A\tto B) \tto C$
of length $n$, such that $u \restrict A, B$ is either in $\ssigma$ or an immediate Opponent extension of a play in 
$\ssigma$, $u \restrict B, C$ is either in $\stau$ or an immediate extension of a play in $\stau$. Additionally, we require
that $u \restrict A, C \in \leg{A\tto C}$ is a P-view, \emph{i.e.} that external Opponent moves always point to the
previous move.


We show by induction on $n$ that 
\[
\P(P_n) = \P(\sigma) \parallel_n \P(\tau)
\]

$\subseteq$. Take $p\in P_{n+1}$. If $p$ is an external Opponent move, suppose wlog that it is in $A$. Take
$p'\imc p$. Necessarily $\P(p')$ terminates with a move in $A$ with Player polarity in $A\tto B$. Then
$\P(p) \restrict A, B$ is an Opponent extension of a play in $\sigma$ by induction hypothesis and 
$\P(p) \restrict B, C = \P(p')\restrict B, C \in \tau$. Finally $\P(p) \restrict A, C \in \leg{A\tto C}$,
since it consists in an Opponent extension of P-ending $\P(p') \restrict A, C$ which is in $\leg{A\tto C}$ 
by induction hypothesis.

Otherwise $p'\imc p$ is positive, either for $\sigma$ or $\tau$, suppose wlog that it is for $\sigma$. Then either
$\P(p) \restrict B, C = \P(p') \restrict B, C \in \leg{B\tto C}$, or it is an immediate Opponent extension of
$\P(p') \restrict B, C \in \leg{B, C}$ as required. If $p$ corresponds to an event in $\oc B$, then obviously
$\P(p) \restrict A, C \in \leg{A \tto C}$. If $p$ corresponds to an event in $\oc A$, then if $p'$ corresponds to
an event in $\oc A$, $\P(p) \restrict A, C$ is an extension of $\P(p') \restrict A\tto C$ preserving alternation,
so in $\leg{A\tto C}$. Finally if $p'$ corresponds to an event in $\oc B$, we still have $\P(p')\in \P(\sigma) 
\parallel_n \P(\tau)$ terminating by a move with Opponent polarity in $B$. By standard reasoning on polarities
in interactions, it follows that the last move of $\P(p')$ appearing in $A$ (if any) must have a Player polarity
in $A$. Therfore the extension of $\P(p')$ with $\lbl ((\sigma \circledast \tau) p)$ preserves alternation in $A\tto C$
and $\P(p) \restrict A, C \in \leg{A\tto C}$. So it remains to show that $\P(p) \restrict A, B \in \P(\sigma)$.
For that, we need to show that for all $m\sqsubseteq^P \P(p) \restrict A, B$, $\pview{m} \in \P(\sigma)$. For any
strict P-ending prefix, it is true by induction hypothesis, so we must just show that it holds for $m = \P(p) \restrict A, B$.
We calculate:
\[
\pview{\P(p) \restrict A, B} = \pview{\P(p') \restrict A, B} (\lbl ((\sigma \circledast \tau) p))
\]
where by induction hypothesis, $\pview{\P(p') \restrict A, B}$ is an Opponent extension of a P-view in $\P(\sigma)$,
therefore there is ${s'}^-\in S$ such that $\pview{\P(p')\restrict A, B} = \P(s')$. From the usual arguments about 
immediate causality in a composition pullback, we have necessarily $s' \imc \Pi_1 p$. From there it is direct to observe
that $\P(\Pi_1 p) = \pview{\P(p) \restrict A, B}$ as required, so $\P(p) \in \P(\sigma) \parallel_{n+1} \P(\tau)$.


$\supseteq$. Take $um \in \P(\sigma) \parallel_{n+1} \P(\tau)$, by induction hypothesis there if $p\in P_n$
such that $\P(p) = u$. If $m$ is an external O-move, then it is straightforward to extend $p$ accordingly, with
the unique corresponding move with copy index $0$, as ensured by receptivity. Otherwise $m$ is either a $\sigma$-move
or a $\tau$-move. Let us assume wlog that it is a $\sigma$-move. By hypothesis we have
\[
\pview{um\restrict A, B} = \pview{u\restrict A, B} m \in \P(\sigma)
\]
therefore there is $s'\in S$ such that $\P(s') = \pview{u\restrict A, B} m$. By backward sequentiality, $s'$
has a unique immediate dependency $s\imc s'$, necessarily with $\P(s) = \pview{u\restrict A, B}$. But
then, we observe that $\P(\pi_1 p) = \pview{\P(p)\restrict A, B}$, which follows from an immediate induction on $\leq_P$.
Therefore, $\P(s) = \P(\pi_1 p)$. So by Lemma \ref{lem:unique_theta}, the unique order-isomorphism satisfies:
\[
[s] \stackrel{\theta}{\iso_\S} [\pi_1 p]
\]
So using backward sequentiality and the extension property of isomorphism families, $\pi_1 p \imc s''$. By receptivity,
there is $c\in \oc A \parallel S$ such that $p \imc [((1, s''), c)]_x = p'$, for some $x$ (that is here irrelevant, since
all finite sets of events in the pullback are consistent, $\sigma$ and $\tau$ being deterministic). By construction, we
have as required $\P(p') = um$.
\end{proof}

So, we have constructed a functor:
\[
\P : \CHOInn \to \Inn
\]
Note that $\P$ satisfies the laws for a functor, even though its source is a $\sim$-bicategory rather than
a category. We will now show that this functor is full and faithful.

\paragraph{$\P$ is faithful.} First, we prove that it is faithful. Take $\sigma : \S \to \oc A^\perp \parallel
\oc B$ and $\sigma' : \S' \to \oc A^\perp \parallel \oc B$ negative, deterministic sequential innocent such that
$\P(\sigma) = \P(\sigma')$, we want to establish that $\sigma \simeq \sigma'$. 

\begin{lemma}
There is a isomorphism $\phi : \S \iso \S'$, such that $\sigma' \circ \phi \sim \sigma$. In particular, $\phi$ is a weak
equivalence.
\end{lemma}
\begin{proof}
In a backward innocent event structure $S$, we say that $s\in S$ have \emph{depth} $n$ if $[s]$ contains exactly $n$ events.
We write $\S_n$ for the projection of $\S$ to events of depth less or equal than $n$. By induction on $n$, we define 
an isomorphism of essps $\phi_n : \S_n \iso \S'_n$ such that $\sigma' \circ \phi_n \sim \sigma$, such that 
$\phi_n$ preserves depth and preserves the copy index of (the projection to the game of) events of negative polarity.
Moreover, we ask that the family $(\phi_n)_n$ is compatible, meaning that $\phi_{n+1}$ agrees with $\phi_n$ on events
of depth less than $n$.

For $n+1$ odd, the extension of $\phi_n$ is forced by receptivity and the requirement that $\phi_{n+1}$ preserves 
the copy index of events of negative polarity. For $n+1$ even, pick $s\in S$ of depth $n+1$. Since $n+1$ even, 
by alternation of the game and courtesy of $\sigma$, $\pol(s) = +$. Pick its immediate dependency $s_0 \imc s$, and
$s'_0 = \phi_n(s_0) \in S'$. Since $\P(\sigma) = \P(\sigma')$, there is $s'' \in S'$ such that $\P(s) = \P(s'')$. Take
$s''_0 \imc s''$. Necessarily, $\P(s_0) = \P(s''_0)$. Now, note that since $\phi_n(s_0) = s'_0$ we have
$\P(s_0) = \P(s'_0)$ as well -- it follows from $\sigma' \circ \phi_n \sim \sigma$ and Lemma \ref{lem:unique_theta}. 
Therefore, $\P(s'_0) = \P(s''_0)$. By Lemma \ref{lem:unique_theta}, the unique order-isomorphism satisfies:
\[
[s'_0] \stackrel{\theta}{\iso_{\S'}} [s''_0]
\]
But from $s''_0 \imc s''$, we know by the extension property that there is $s'_0 \imc s'$ as well such that
$\theta \cov{(s', s'')}$. We set $\phi_{n+1}(s) = s'$. Note that $s'$ is uniquely determined by
forward sequentiality and determinism, from that it is easy to deduce that $\phi_{n+1}$ so defined yields
an order-isomorphism, and by construction it satisfies the requirements.

Forming $\phi = \bigsqcup_{n\in \omega} \phi_n$ we get the required weak equivalence. The fact that $\phi$ preserves
symmetry is an obvious consequence of Lemma \ref{lem:unique_theta}.
\end{proof}

Note that one consequence of that is that for $\CHOInn$-strategies, if $\sigma$ and $\sigma'$ are weakly equivalent
then the weak equivalence can actually be assumed to be an isomorphism between the corresponding essps $\S$ and $\S'$.


\paragraph{$\P$ is full.}
Finally, it remains to show that $\P$ is full. Take $\ssigma : A\tto B$ a Hyland-Ong innocent strategy. Write
$PV(\ssigma)$ for the set of P-views of $\ssigma$, possibly extended by a ending Opponent move pointing to the
latest move. For $m \in PV(\ssigma)$, write $O(m)$ for the set of O-moves in $m$. Define an essp $\S$ having:
\begin{itemize}
\item Events, pairs $(m, \alpha)$ where $\alpha : O(m) \to \omega$,
\item Order, $(m, \alpha) \leq (m', \alpha')$ iff $m\sqsubseteq m'$ and $\alpha, \alpha'$ compatible on their
common domain.
\item Consistency, every finite set.
\item Symmetry, the unique order-isomorphism between $[(m, \alpha)]$ and $[(m', \alpha')]$ when $m = m'$.
\end{itemize}
By induction on $n$, we now define:
\[
\sigma_n : \S_n \to \oc A^\perp \parallel \oc B
\]
Take $(m, \alpha) \imc (m', \alpha')$, and assume that $m' = mb$ with $b$ in $B$, the other case is similar.
If $m'$ is O-ending, then we set, with $\sigma_n((m, \alpha)) = (2, \beta)$:
\[
\sigma_{n+1}((m', \alpha')) = (2, \beta \cup \{b \mapsto \alpha'(b)\})
\]
so the copy index of Opponent is set in the game as it is in the strategy. On the other hand if $m'$ is P-ending 
(and so $\alpha = \alpha'$), we set:
\[
\sigma_{n+1}((m', \alpha)) = (2, \beta \cup \{b \mapsto \tuple{\sharp m, \sharp \alpha}\})
\]
where $\sharp m, \sharp \alpha$ denote natural numbers representing uniquely $m$ and $\alpha$, and
$\tuple{-, -} : \omega^2 \to \omega$ is an arbitrary injection. 

It is direct to check that $\sigma = \bigsqcup_{n\in \omega} \sigma_n$ defines a $\sim$-strategy, and
by construction we have $\P(\sigma) = \ssigma$ as needed -- so $\P$ is full.


cho.tex
\documentclass{article}
\usepackage{graphicx}
\usepackage{mathrsfs}
\usepackage{mathpartir}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{cmll}
\usepackage[all]{xy}

\usepackage{mathpazo}
\usepackage{hyperref}
\usepackage{amsthm}
\usepackage{stmaryrd}
%\usepackage{MnSymbol}
\usepackage{todonotes}

\input{macros}


\begin{document}

%% ACTUAL DOCUMNT
\title{Concurrent Hyland-Ong games}
\author{Simon Castellan, Pierre Clairambault, Glynn Winskel}

\maketitle

\begin{abstract}
In this technical report, we build a cartesian closed category of non-deterministic concurrent strategies playing
on arenas. We show that this CCC admits as a sub-CCC the standard category of arenas and Hyland-Ong innocent strategies.
Our strategies, have much more possible behaviours than standard Hyland-Ong innocent strategies -- however the
purpose of this technical report is to define our CCC, and we leave for later its use for semantics of programming
languages.
\end{abstract}

\tableofcontents

\section{Introduction}

In \cite{DBLP:conf/lics/RideauW11}, Rideau and Winskel have introduced a compositional framework for games based on event structures. The
purpose of this note is to build an extension of Hyland-Ong arena games where strategies, instead of trees, are
event structures. With this, we hope to be able to use the flexibility of the Hyland-Ong approach within a 
more expressive metalanguage, and through this get finer models for complex effectful programming languages,
with concurrency in mind.

The purpose of this note is to describe the cartesian closed category in which our future developments will take
place. In Section \ref{sec:prelim}, we start with some technical preliminaries on event structures, stable
families, and symmetry. In Section \ref{sec:tcg}, we build the compact closed category equipped with the adequate
notions of symmetry. In Section \ref{sec:cho}, we use it to build our ccc that we call concurrent Hyland-Ong games,
and we show that its subcategory of deterministic sequential strategies coincides with the standard ccc of arena games and
innocent strategies.

\section{Preliminaries}
\label{sec:prelim}

\input{prelim}

\section{Thin concurrent games with symmetry}
\label{sec:tcg}

\input{tcg}

\section{Concurrent Hyland-Ong games}
\label{sec:cho}

\input{ccccho}

%\appendix
%
%\section{Technical appendix}
%
%\input{appendix}


\bibliographystyle{alpha}
\bibliography{biblio}

\end{document}

macros.tex
% Macros
\newcommand{\por}{\mathrm{por}}
\newcommand{\Bool}{\mathbb{B}}
\newcommand{\ttrue}{\mathtt{t\!t}}
\newcommand{\tfalse}{\mathtt{f\!f}}
\newcommand{\PCF}{\mathrm{PCF}}
\newcommand{\PCFPOR}{\mathrm{PCF}_{\parallel}}
\newcommand{\tbool}{\mathbb{B}}
\newcommand{\tnat}{\mathbb{N}}
\newcommand{\tx}{\mathbb{X}}
\newcommand{\Con}{\mathrm{Con}}
\newcommand{\conf}[1]{\mathscr{C}(#1)}
\newcommand{\cov}{{{\mathrel-\joinrel\subset}}}
\newcommand{\longcov}[1]{{\stackrel{#1}{\mathrel-\joinrel\relbar\joinrel\subset\,}}}
\newcommand{\imc}{\rightarrowtriangle}
\newcommand{\lbl}{\mathrm{lbl}}
\newcommand{\intr}[1]{\llbracket #1 \rrbracket}
\newcommand{\tto}{\Rightarrow}
\newcommand{\gcc}{\mathrm{gcc}}
\newcommand{\id}{\mathrm{id}}
\def\profto{\!\!\!\xymatrix@C-.75pc{\ar[r]|-{\! +\!} &}\!\!\! }%profarrow
\newdir{pb}{:(1,-1)@^{|-}}
\def\pb#1{\save[]+<16 pt,0 pt>:a(#1)\ar@{pb{}}[]\restore}
\newcommand{\StratPor}{\mathcal{CHO}_\parallel}
\newcommand{\CStrat}{{\StratPor}}
\newcommand{\CollapseCStrat}{\StratPor/\simeq}
\newcommand{\ScottD}{\mathcal{SD}}
\newcommand{\CGS}{\mathrm{TCG}}
\newcommand{\A}{\mathcal{A}}
\newcommand{\B}{\mathcal{B}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\D}{\mathcal{D}}
\newcommand{\E}{\mathcal{E}}
\renewcommand{\S}{\mathcal{S}}
\newcommand{\R}{\mathcal{R}}
\newcommand{\T}{\mathcal{T}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\X}{\mathcal{X}}
\newcommand{\flow}[1]{{#1}_{\mathrm{flow}}}
\newcommand{\real}{\Vdash}
\newcommand{\Qu}{\mathrm{Qu}}
\newcommand{\An}{\mathrm{An}}
\newcommand{\restr}{\upharpoonright}
\newcommand{\cgsto}{\stackrel{\small{\CGS}}{\profto}}
\newcommand{\stratporto}{\stackrel{\small{\StratPor}}{\profto}}
\newcommand{\choto}{\stackrel{\small{\CHO}}{\profto}}
\newcommand{\ssigma}{\mathfrak{s}}
\newcommand{\stau}{\mathfrak{t}}

\DeclareMathOperator{\ifpcf}{if}
\DeclareMathOperator{\ptr}{ptr}
\DeclareMathOperator{\zero}{zero}
\DeclareMathOperator{\ffb}{ff}
\DeclareMathOperator{\ttb}{tt}
\DeclareMathOperator{\iszero}{iszero}
\DeclareMathOperator{\succpcf}{succ}
\DeclareMathOperator{\oppcf}{op}
\DeclareMathOperator{\fix}{fix}
\DeclareMathOperator{\pred}{pred}
\DeclareMathOperator{\truepcf}{true}
\DeclareMathOperator{\falsepcf}{false}
\newcommand{\hide}[1]{}
\newcommand{\indcc}[1]{\widehat{ \gamma_A}}

\newcommand{\nemove}{\ocirc}

\newcommand{\Stop}{\hbox{\rm Stop}}

\newcommand{\pfrule}[2]{{{\hbox{{$#1$}}\over{\strut \hbox{{$#2$}}}}}}
 \def\fatbar{\mathop{[\!]}}
 
 \newcommand{\cpar}[2]{(#1,#2)}

\newcommand{\FV}{{\rm fv}}
\newcommand{\lam}{\lambda}
\newcommand{\sncirc}{\oast} 
\newcommand{\emptyenv}{\emptyset}
\newcommand{\ev}{{\it ev}}
%\newcommand{\nstar}{*}
\newcommand{\nstar}{o}
\newcommand{\stcomp}[3]{\exists #1.\, [\, #2 \mathrel{%\mid
\vvbar} #3\, ]}
\newcommand{\Q}{{\cal Q}}
\newcommand{\Eta}{{\rm H}}
\newcommand{\Ga}{\Gamma}

\newcommand{\Nat}{{\cat N}}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{prop}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{notation}[theorem]{Notation}
\newtheorem{example}[theorem]{Example}
\newtheorem{exercise}[theorem]{Exercise}
\newtheorem{convention}[theorem]{Convention}
\newtheorem{conjecture}[theorem]{Conjecture}
\theoremstyle{remark}

\newtheorem*{theorem*}{Theorem} 

\def\endpf{}
\def\endex{{\hspace*{\fill}\hbox{$\Box$}}}
\def\endremark{{\hspace*{\fill}\hbox{$\Box$}}}

\newcommand{\op}{{\rm op}}
\newcommand{\rigpar}{\parr_{r}}

\newcommand{\bigfrac}[2]{\frac{\mbox{\(#1\)}}{\mbox{\(#2\)}}}
 
%\usepackage{graphicx}
%\sloppy
 \usepackage[all]{xy}
%\UseComputerModernTips

\newcommand{\Prof}{{\bf Prof}}
\newcommand{\Glin}{\to_G}
\newcommand{\emptygame}{\emptyset}
\newcommand{\incompat}{\nuparrow}
\newcommand{\opmove}{\ominus}
\newcommand{\plmove}{\oplus}
% Mathematics
%\renewcommand{\IEEEQED}{\IEEEQEDopen}
 
\def\profto{\!\!\!\xymatrix@C-.75pc{\ar[r]|-{\! +\!} &}\!\!\! }%profarrow
\newcommand{\spano}[5]{{\xymatrix{
    & {#3}\ar[dl]_{#2}\ar[dr]^-{#4} &\\
      {#1} && {#5} 
  }}}
\def\all{\forall}


\newdir{pb}{:(1,-1)@^{|-}}
\def\pb#1{\save[]+<16 pt,0 pt>:a(#1)\ar@{pb{}}[]\restore}


\newcommand{\pref}{{\mathop{\footnotesize{\bullet}.}}}
\newcommand{\prefu}{{\mathop{\footnotesize{\bullet}}}}

%\newcommand{\scirc}{{\mathrel{\!\,\odot\,\! }}}

\newcommand{\wor}{\vee}
\newcommand{\wand}{\wedge}
\newcommand{\denM}[1]{\den{#1}_{{\scriptscriptstyle M}}}
\newcommand{\denl}[1]{\den{#1}^l}
\newcommand{\sat}{\models}
\newcommand{\satM}{\models_{{\scriptscriptstyle M}}}
\newcommand{\co}{\mathbin{{\it co}}}
\newcommand{\vvbar}{{\mathbin{\parallel}}}
\newcommand{\scirc}{{{\odot}}}
\newcommand{\cbel}{{{\mathrel-\joinrel\sqsubset}}}
\newcommand{\rcbel}{{{\mathrel\sqsupset\joinrel\!-}}}

\renewcommand{\max}{{\it max}}
\newcommand{\Neg}{{\it Neg}}
\newcommand{\setdif}{\setminus}
\renewcommand{\bar}[1]{{\overline{{#1}}}}
\newcommand{\mkprof}[1]{#1\mbox{``}}
\newcommand{\al}{\alpha}
\newcommand{\be}{\beta}
\newcommand{\ga}{\gamma}
\newcommand{\sig}{\sigma}
\newcommand{\ups}{\upsilon}

\newcommand{\fsubseteq}{\subseteq_{\rm fin}}
\newcommand{\pprod}{\times}
\newcommand{\CC}{{\rm C\!\!C}}
%\newcommand{\CC}{{\rm C}}
\newcommand{\cc}{\ c\!\!\!\!c\,}
%\newcommand{\cc}{\gamma}
\newcommand{\pol}{{\it pol}}
\newcommand{\rstd}{\mathbin\upharpoonright}
%\newcommand{\hide}[2]{[Proj #1 on #2}]
\renewcommand{\mod}[1]{{|{{#1}}|}}
%\newcommand{\Strat}{{\bf Strategy}}
\newcommand{\Strat}{{\mathbf{Games}}}
\newcommand{\Lin}{{\mathbf{Lin}}}
\newcommand{\DLin}{{\mathbf{DLin}}}
\newcommand{\WStrat}{{\mathbf{WGames}}}
\newcommand{\DStrat}{{\mathbf{DGames}}}
\newcommand{\WDStrat}{{\mathbf{WDGames}}}
\newcommand{\Sep}{{\rm Sep}}
\newcommand{\Act}{{\it Act}}
\newcommand{\IS}{{\mathbb S}}
\newcommand{\Fix}{{Y}}
\newcommand{\Dom}{\textbf{Dom}}
\newcommand{\terme}[1]{#1^\text{PCF}}
\newcommand{\G}{{\mathcal G}}
\newcommand{\extequiv}{\cong_{\text{ext}}}
\newcommand{\Saug}{{\mathcal S\!{\it aug}}}
\newcommand{\bel}{\sqsubseteq}
%\newcommand{\bel}{\propnl}
%\newcommand{\spano}[5]{{\xymatrix{
%    & {#3}\ar[dl]_{#2}\ar[dr]^-{#4} &\\
%      {#1} && {#5} 
%  }}}
  \newcommand{\spanpl}[5]{{\xymatrix{
    & {#3}\ar@{_{(}->}[dl]_{#2}\ar[dr]^-{#4} &\\
      {#1} && {#5} 
  }}}
\newcommand{\AS}{(A, l_A, r_A)}
\newcommand{\BS}{(B, l_B, r_B)}
%\newcommand{\ES}{(E, l_E, r_E)}
\newcommand{\Term}{\varpi}
\newcommand{\SA}{\cal S\!A}
\newcommand{\SB}{\cal S\!B}
\newcommand{\PES}{{\cal P\!E}}
\newcommand{\PFil}{{\cal P\!F}}
\newcommand{\PAlt}{{\cal P\!A}}
\newcommand{\ESS}{{\cal E\!S\!S}}
%\newcommand{\ES}{{\cal E}}
\newcommand{\Cub}{{\mathbb C}}
\newcommand{\SESS}{{\mathcal S\!\ESS}}
\def\Con{{\rm Con}}
\newcommand\SF{{\cal S\!F}}
\newcommand\SPr{{\mathcal S}\!\Pr}
\newcommand{\SStFam}{{\mathcal S}\!{\mathcal F\!am}}
\newcommand{\StFam}{{\mathcal F\!am}}
\newcommand{\Fam}{{\cal F}}
\newcommand{\trace}[1]{{\rm trace}(#1)}
\newcommand{\dem}{{\it dem}}
\newcommand{\out}{{\it out }}
\newcommand{\esws}{event structure with symmetry}
\newcommand{\essws}{event structures with symmetry}
\newcommand{\eswp}{event structure with polarity}
\newcommand{\esswp}{event structures with polarity}
%\newcommand{\fconf}[1]{\:\!{\cal C}^o(#1)}
\newcommand{\fconf}[1]{{\cal C}(#1)}
\newcommand{\iconf}[1]{\:\!{\cal C}^\infty(#1)}
\newcommand{\ZZero}{\mathbb{O}} 
\newcommand{\Span}[1]{{\rm Span}_{#1}}
\newcommand{\profu}[1]{{\widetilde{#1}}}
\def\tr#1{\widetilde{#1}}
\newcommand{\parrow}{\rightharpoonup}
\newcommand{\NT}[2]{(#1\Rightarrow#2)}
\newcommand{\arr}[1]{{{\stackrel{#1}{\longrightarrow}}}}
%\newcommand{\implies}{\Rightarrow}
\newcommand{\dc}{{\mathop \downarrow}}
\newcommand{\I}{{\cal I}}
\newcommand{\arrow}{\rightarrow}
\newcommand{\set}[2]{{\{  #1\  | \  #2 \} }}
\newcommand{\setof}[1]{{\{ #1 \} }}
\newcommand{\Arr}{\Rightarrow}
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\smallcat}[1]{\mathbb{#1}} 
\newcommand{\Zero}{\smallcat{O}}
\newcommand{\bng}{{!}}
\newcommand{\ccs}[1]{\mathcal{H}\den{#1}}
\newcommand{\conjunction}[2]{\textstyle{\bigwedge_{#1}{#2}}}
\newcommand{\ctx}{\mathrel{\smash{\text{\raisebox{-3.5pt}{\shortstack{$\sqsubset$\\[-2pt]$\sim$}}}}}}
\newcommand{\curry}{\operatorname{\mathit{curry}}}
\newcommand{\den}[1]{\llbracket #1 \rrbracket}
\newcommand{\eqdef}{\mathrel{=_{\mathrm{def}}}}
\newcommand{\equivdef}{\mathrel{\equiv_{\mathrm{def}}}}
\newcommand{\fst}{\operatorname{\mathit{fst}}}
\newcommand{\iffdef}{\mathrel{\Longleftrightarrow_{\mathrm{def}}}}
\newcommand{\inclusion}{\hookrightarrow}
%\newcommand{\inj}{\operatorname{\mathit{in}}}
\newcommand{\Inj}{\operatorname{\mathit{In}}}
\newcommand{\iso}{\cong}
\newcommand{\morph}[1]{\mathrel{\xrightarrow{\smash[b]{#1}}}}
\newcommand{\new}{\operatorname{\mathit{new}}}
\newcommand{\tensor}{\otimes}
 \newcommand{\union}[2]{\textstyle{\bigcup_{#1}{#2}}}
\newcommand{\wdiag}{\delta}
\newcommand{\yon}{\mathrm{y}}
%\renewcommand{\P}{\smallcat{P}}
\renewcommand{\P}{\mathcal{P}}


%*******************EQALIGN, EQALIGNNO & LEQALIGNNO***********************

\def\mxxth{\mathsurround=0pt}
\dimendef\dimenxx=0
\def\openup{\afterassignment\xxpenup\dimenxx=}
\def\xxpenup{\advance\lineskip\dimenxx
  \advance\baselineskip\dimenxx \advance\lineskiplimit\dimenxx}
\def\eqalign#1{\,\vcenter{\openup1\jot \mxxth
  \ialign{\strut\hfil$\displaystyle{##}$&$\displaystyle{{}##}$\hfil
     \crcr#1\crcr}}\,}

\newif\ifdtxxp
\def\displxxy{\global\dtxxptrue \openup1\jot \mxxth
  \everycr{\noalign{\ifdtxxp \global\dtxxpfalse
      \vskip-\lineskiplimit \vskip\normallineskiplimit
      \else \penalty\interdisplaylinepenalty \fi}}}
\def\displaylines#1{\displxxy
  \halign{\hbox to\displaywidth{$\hfil\displaystyle##\hfil$}\crcr
      #1\crcr}}

\newskip\mycntring \mycntring=0pt plus 1000pt minus 1000pt
\def\eqalignno#1{\displxxy \tabskip=\mycntring
  \halign to\displaywidth{\hfil$\displaystyle{##}$\tabskip=0pt
      &$\displaystyle{{}##}$\hfil\tabskip=\mycntring
      &\llap{$##$}\tabskip=0pt\crcr
      #1\crcr}}
\def\leqalignno#1{\displxxy \tabskip=\mycntring
  \halign to\displaywidth{\hfil$\displaystyle{##}$\tabskip=0pt
      &$\displaystyle{{}##}$\hfil\tabskip=\mycntring
      &\kern-\displaywidth\rlap{$##$}\tabskip=\displaywidth\crcr
      #1\crcr}}

%***********************************************************************


% Abbreviations
\newcommand{\ie}{{\it i.e.}}
\newcommand{\eg}{{\it e.g.}}
\newcommand{\cf}{{\it cf.}}
\newcommand{\etc}{{\it etc.}}
\newcommand{\viz}{{\it viz.}}

%New arrow heads
\newdir{C}{%
!/4.5pt/@{( }*:(1,-.2)@{}*:(1,+.2)@_{}}

\newdir{|>}{%
!/4.5pt/@{|}*:(1,-.2)@{>}*:(1,+.2)@_{>}}


\newcommand{\myparagraph}[1]{\vspace{2mm}\noindent\emph{#1.}\ \ }
\newenvironment{myproof}[1][Proof]{\noindent\emph{#1.}\ \ }
{\hfill\hbox{$\Box$}\vspace{1mm}}

\newcommand{\dotcup}{\ensuremath{\mathaccent\cdot\cup}}

% Definitions for todonotes
\newcommand{\rkPierreInline}[1]{\todo[inline,color=blue!40]{Pierre --- #1}}
\newcommand{\rkPierre}[1]{\todo[color=blue!40]{Pierre --- #1}}
\newcommand{\rkSimonInline}[1]{\todo[inline,color=red!40]{Simon --- #1}}
\newcommand{\rkSimon}[1]{\todo[color=red!40]{Simon --- #1}}

% Macros de Pierre
\newcommand{\ESP}{\mathcal{E\!S\!P}}
\newcommand{\ESSP}{\mathcal{E\!S\!S\!P}}
\newcommand{\EP}{\mathcal{E\!P}}
\newcommand{\ES}{\mathcal{E\!S}}
\newcommand{\tuple}[1]{\langle #1 \rangle}
\newcommand{\restrict}{\upharpoonright}
\newcommand{\ext}{\mathrm{ext}}
\newcommand{\proj}{\downarrow}
\newcommand{\longvoc}[1]{{\stackrel{#1}{\mathrel\supset\joinrel\relbar\joinrel\!\!-}}}
\newcommand{\linear}{\multimap}
\newcommand{\dep}{\mathrm{dep}}
\newcommand{\aug}{\mathrm{aug}}
\newcommand{\dom}{\mathrm{dom}}
\newcommand{\codom}{\mathrm{codom}}
\newcommand{\lift}[1]{\overline{#1}}
\newcommand{\inj}{\mathrm{Inj}}
\newcommand{\inje}{\mathrm{i}}
\newcommand{\img}{\mathrm{Im}}
\newcommand{\threads}{\mathbb{T}}
\newcommand{\toplus}{\mathop{-\!\!\!-\!\!\!\raisebox{-1pt}{$\boxplus$}}}
\newcommand{\hash}{\sharp}
\newcommand{\ind}{\mathrm{ind}}
\newcommand{\leg}[1]{\mathcal{L}_{#1}}
\renewcommand{\tilde}[1]{\widetilde{#1}}

% Categories of games
\newcommand{\TCG}{\mathrm{TCG}} %Thin concurrent games
\newcommand{\NTCG}{\mathrm{TCG}^-} %Negative thin concurrent games
\newcommand{\WTCG}{\mathrm{TCG}^-_{wt}} %Negative well-threaded thin concurrent games
\newcommand{\CHO}{\mathrm{Cho}}
\newcommand{\Inn}{\mathrm{Inn}}
\newcommand{\CHOInn}{\mathrm{ChoInn}}
\newcommand{\inc}{\trianglelefteq}
\newcommand{\eqclass}[1]{\underline{#1}}
\newcommand{\PStrat}{\mathrm{PStrat}}
\newcommand{\nf}[1]{#1_{\text{rf}}}

% views
\newlength{\viewht}
\newlength{\viewlift}                                                                                                                         
\newlength{\viewdp}
\newlength{\viewdrop}
% pview
\newcommand{\pview}[1]{%                   Player view
\settoheight{\viewht}{\makebox{$#1$}}% get height
\setlength{\viewlift}{\viewht}%
\addtolength{\viewlift}{-1ex}%
\raisebox{0.3\viewlift}{%       raise the left corner
  \makebox{$\ulcorner$}}%  put the corner in
  \!#1\!%                  put the argument in and squish up a bit
\settoheight{\viewht}{\makebox{$#1$}}% get height again!
\setlength{\viewlift}{\viewht}%                                                                                                               \addtolength{\viewlift}{-1ex}%
\raisebox{0.3\viewlift}{%       raise the right corner
  \makebox{$\urcorner$}}%  put it in
}

prelim.tex
\subsection{Event structures and maps}

Let us start with some elementary definitions on event structures.
Here we only give some basic definitions, notations and properties, but we will skip proofs. This
is intended as a reference only, a more comprehensive introduction to event structures and
stable families can be found \emph{e.g.} in \cite{WGames}.

\subsubsection{The categories $\ES$ and $\ESP$}

\begin{definition}
An \textbf{event structure} (es for short) comprises $(E, \leq, \Con)$,   consisting of a   
 set $E$, of \textbf{events} which are
partially ordered by $\leq$, the \textbf{causal dependency relation},
and a  nonempty \textbf{consistency relation} $\Con$ consisting of finite subsets of $E$, 
which satisfy
$$
\eqalign{
&\set{e'}{e'\leq e}\hbox{ is finite for all } e\in E,\cr
&\setof{e}\in\Con \hbox{  for all } e\in E,\cr
&Y\subseteq X\in\Con \implies Y\in \Con,\ \hbox{ and}\cr
&X\in\Con \ \&\  e\leq e'\in X \implies 
X\cup\setof{e}\in\Con.\cr}
$$
\end{definition}

Event structures support the following notion of state.

\begin{definition}
The   (finite) \textbf{configurations}, $\conf E$,  of an event structure $E$ consist of
those  finite subsets 
$x\subseteq E$ which are
\begin{itemize} 
\item[]
{\em Consistent:} %$ \forall X\subseteq x.\   X \hbox{ is finite} \Rightarrow X\in\Con$
$x\in\Con$,  and
%
\item[]
{\em Down-closed:}
$\forall e, e'.\ e'\leq e\in x \implies e' \in x$.
\end{itemize} 
\end{definition}

\paragraph{Notations.} We recall some basic notations on event structures. If $e\in E$, its \textbf{prime configuration}
is $[e] = \{e'\in E\mid e' \leq e\}$. If $e, e' \in E$ are such that
$e < e'$ and no other event lies in between, we write $e \imc e'$. If $x\in \conf{E}$ and $e \in E$ is such that
$e\not \in x$ and $x\cup \{e\} \in \conf{E}$, we write $x \cov{e}$, or just $x \longcov x\cup \{e\}$.

Moreover, if two configurations $x, y$ of $E$ are such that $x \cup y$
is consistent then we write that $x$ and $y$ are
\emph{compatible}. (It is equivalent to asking that $x \cup y$ is a
configuration of $E$.)


We now introduce total maps between event structures.

\begin{definition}
A \textbf{total map} $f : (E, \leq_E, \Con_E) \to (F, \leq_F, \Con_F)$ between event structures
(written $f: E \to F$ for conciseness) is a function $f : E \to F$ such that:
\begin{itemize}
\item[(1)] For all $x\in \conf{E}$, $f\,x \in \conf{F}$,
\item[(2)] For all $e, e'\in x\in \conf{E}$, $f\,e = f\,e' \implies e = e'$.
\end{itemize}
\end{definition}

We write $\ES$ for the category of event structures and total maps between them. An \textbf{event structure
with polarities} (esp for short) is an es $E$ equipped with a \textbf{polarity function} $\pol_E : E \to \{-, +\}$
specifying for each event $e\in E$, whether it is positive/Player ($\pol(e) = +$) or negative/Opponent ($\pol(e) = -$).
The names negative/Opponent and positive/Player will be used interchangeably in this paper. Maps of esp
are supposed to preserve polarities, and form a category $\ESP$.

\paragraph{Notations.} If $E$ is an esp, when introducing events of $E$ we will sometimes label them with
polarities, as in $e^-, e^+$. In such a case the labeling is not part of the identifier and can be thought of
as typing information -- the identifier $e$ can later be used without the annotation. Typically we might
say "let $e^- \in E$" to abbreviate "let $e\in E$ such that $\pol(e) = -$".

\subsubsection{Two constructions on event structures}

We introduce two constructions on event structures, that will be useful later on. We spell them out
for plain event structures, but they obviously also make sense in the presence of polarities.

\paragraph{Restriction.} Let $E$ be an event structure, and $R\subseteq E$. The \emph{restriction} of $E$
to $R$ comprises events whose causal dependencies are all in $R$.

\begin{definition}
There is an event structure $E\restr R$, the \textbf{restriction} of $E$ to $R$, having:
\begin{itemize}
\item \emph{Events:} 
\[
\{e\in E \mid [e] \subseteq R\}
\]
\item \emph{Causality, consistency:} same as in $E$.
\end{itemize}
\end{definition}

For $(E, \F_E)$ a stable family one can also form its restriction to $R$ by restricting $\F_E$ to subseteq
of $R$. We can then check that $\conf{E\restr R} = \conf{E}\restr R$, and for all $(E, \F_E)$
stable family we have $\Pr((E, \F_E)\restr R) = \Pr((E, \F_E)) \restr \max^{-1}R$.


\paragraph{Projection.} Let $E$ be an event structure, and $V\subseteq E$. The \emph{projection} of $E$ to
$V$ hides the causal dependencies that are not in $V$.

\begin{definition}
For $E$ an event structure and $V\subseteq E$ there is an event structure $E\proj V$, the \textbf{projection}
of $E$ to $V$, having:
\begin{itemize}
\item \emph{Events:} Those of $V$,
\item \emph{Causality, consistency:} Induced by $E$.
\end{itemize}
\end{definition}

\subsubsection{Some lemmas on event structures}

The two following technical lemmas will be useful in our development.

\begin{lemma}\label{lem:incmap}
Let $f: E \to F$ be a map of event structures, and let $x, y \in \conf{E}$ be compatible configurations such that $x, y \subseteq z$ and
$f(x) \subseteq f(y)$, then $x \subseteq y$.
\end{lemma}
\begin{proof}
Suppose this is not the case, then there is $e\in x$ such that $e \not \in y$. But still $f(e) \in f(y)$ so there is
$e'\in y$ such that $f(e) = f(e')$. But since $x, y \subseteq z\in \conf{E}$, by local injectivity we have $e = e'$, absurd.
\end{proof}

\begin{lemma}[Mapification]
Suppose there is a total function $p: \conf{R} \to \conf{S}$ preserving $\cov$ and \emph{preserving bounded unions} in the sense that for all
$x, y\in \conf{R}$ such that $x$ and $y$ are compatible, then $p(x\cup y) = p(x) \cup p(y)$. Then there is a unique total map of event structure
$\hat{p} : R \arrow S$ such that for all $x\in \conf{R}$, $\hat{p}(x) = p(x)$.
\label{lem:mapification}
\end{lemma}
\begin{proof}
For an event $r\in R$, we necessarily have $p([e)) ~ \cov ~ p([e])$, let us write $p([e]) = p([e)) \cup \{e'\}$. We set
$\hat{p}(e) = e'$. Now, suppose $x \longcov{e} y$ in $\conf{R}$. Necessarily,
\begin{eqnarray*}
p(y)    &=& p(x \cup [e])\\
        &=& p(x) \cup p([e])\\
        &=& p(x) \cup p([e)) \cup \{\hat{p}(e)\}\\
        &=& p(x) \cup \{\hat{p}(e)\}
\end{eqnarray*}
from which it follows by immediate induction that for any configuration $x\in \conf{R}$, $\hat{p}(x) = p(x)$.
Finally, $\hat{p}$ is a map of event structures since it evidently preserves configurations, and is locally injective since it preserves
$\cov$.
\end{proof}

\subsection{Stable families, and structure in $\ES$}

In this subsection, we aim to construct some structure in $\ES$: namely, products and pullbacks. Those are
notably difficult to describe combinatorially directly on event structures. Instead, it is more convenient to
first describe the category of \emph{stable families}, of which $\ES$ can be seen as a full category. Products
(and pullbacks) are more direct to construct in stable families, and are then easily transported to $\ES$.

\subsubsection{Stable families}

\begin{definition}
Let $E$ be a set of events equipped with a non-empty $\F_E \subseteq_f E$ (a set of finite subsets) set of configurations. For $X\subseteq \F_E$
we say that $X$ is \textbf{compatible}, written $X\uparrow$, iff there is $x\in \F_E$ such that $\cup X \subseteq x$.
We define a \textbf{stable family} as such a pair $(E, \F_E)$ satisfying the additional axioms:
\begin{itemize}
\item[(1)] \emph{Completeness:} For $X\subseteq \F_E$, if $X\uparrow$ then $\cup X \in \F_E$ as well.
\item[(2)] \emph{Stability:} For $X\subseteq \F_E$, if $X\uparrow$ then $\cap X \in \F_E$ as well.
\item[(3)] \emph{Coincidence-freeness:} For $e, e'\in x\in \F$ with $e\neq e'$, then there is $y\in \F_E$
with $y\subseteq x$ and $e\in y \Leftrightarrow e'\not \in y$.
\end{itemize}
A map $f: (E, \F_E) \to (F, \F_F)$ of stable families is a function $f:E\to F$ preserving configurations,
and locally injective in the sense that forall $e, e'\in x\in \F_E$, $f(e) = f(e') \implies e = e'$.
This forms a category $\SF$ of stable families and maps between them.
\end{definition}

When speaking about a stable family $(E, \F_E)$ we will sometimes leave $E$ implicit and refer to it as $\F_E$.
If $E$ is an event structure, $(E, \conf{E})$ is a stable family. Obviously the operation $\conf{-}$ gives a functor:
\[
\conf{-} : \ES \to \SF
\]
which is full and faithful.

We now define the product of stable families.

\begin{definition}
For stable families $(A, \F_A)$ and $(B, \F_B)$ their product is $(A\times B, \F_{A\times B})$, where
$x\subseteq A\times B$ is in $\F_{A\times B}$ iff it satisfies:
\begin{itemize}
\item[(1)] Projections: $\pi_1 x \in \F_A$ and $\pi_2 x \in \F_B$
\item[(2)] Injectivity of projections: If $e, e' \in x$ with $\pi_i e = \pi_i e'$, then $e = e'$.
\item[(3)] Coincidence-freeness: If $e, e'\in x$ with $e\neq e'$, then there exists $y \subseteq x$ with
$\pi_1 y \in \F_A$ and $\pi_2 y \in \F_B$ as well, and $e\in y \Leftrightarrow e'\not \in y$.
\end{itemize}
\end{definition}

This definition yields a stable family, and actually gives a product in $\SF$.
This product can be transported to event structures as follows.

\subsubsection{Products in event structures}
%% XXX: Weird formulation: it seems like we have a canonical event
%% structure for every stable family
We now construct a right adjoint to $\conf{-}$ which, to any stable family, associates a canonical event structure 
representing it.

\paragraph{Primes.} Let $(E, \F_E)$ be a stable family, and $x\in \F_E$. Then there is a partial order induced
on $x$ by, for $e, e'\in x$:
\[
e \leq_x e' \Leftrightarrow \forall y \subseteq x,\,\,y\in \F_E\,\,\&\,\,e'\in y \implies e \in y
\]
We also have the corresponding notion of immediate dependency $e \imc_x e'$.

Then for $e\in x\in \F_E$, we can define the \textbf{prime}:
\[
[e]_x = \{e'\in x \mid e'\leq_x e\}
\]
It is then easy to show that $[e]_x \in \F_E$.

\begin{definition}
For a stable family $(E, \F_E)$ we define an event structure $\Pr((E,\F_E))$ having:
\begin{itemize}
\item \emph{Events:} primes $[e]_x$.
\item \emph{Causality:} inclusion.
\item \emph{Consistency:} For $X$ a finite set of primes, $X \in \Con_{\Pr((E, \F_E))}$ iff $\cup X \in \F_E$.
\end{itemize}
\end{definition}

Then one can check that $\Pr(-)$ extends to a functor from stable families to event structures, which is
right adjoint to $\conf{-}$. For event structures $A$ and $B$ we can now define:

\[
A\times B = \Pr(\conf{A}\times \conf{B})
\]


This defines a product of $A$ and $B$ in the category of event structures.

\subsubsection{Pullbacks in $\ES$}

We have seen how one can define products in $\ES$. Take now $f, g : E \to F$. Defining $R \subseteq E$ 
as $e\in R$ iff $f(e) = g(e)$, one can check that $E\restr R$ is an equalizer of $f$ and $g$. Together
with the product introduced above, this permits to construct pullbacks in $\ES$. 

Let $f: A \to C$ and $g: B \to C$. Form their pullback by expanding the definition above.

\[
\xymatrix@R=20pt@C=20pt{
& A\circledast B
	\ar[dl]_{\Pi_1}
	\ar[dr]^{\Pi_2}
	\pb{270}\\
A 	\ar[dr]_{f}&&
B
	\ar[dl]^{g}\\
&C
}
\]

Precisely, we first define $R \subseteq A\times B$ as the set of events $c\in A\times B$ such that $f\,(\Pi_1\,c) = 
g\,(\Pi_2\,c)$. Then we set: 
\[
A \circledast B = \Pr(\conf{A} \times \conf{B} \restr R)
\]
and thereby obtain the pullback of $f$ and $g$. Unfolding the definitions, we can see that events of
$A \circledast B$ have the form:
\[
[(a, b)]_x
\]
where $x \in \conf{A}\times \conf{B} \restr R$ and $(a, b)\in x$, and for all $(a', b')\in x$ we have
$f\,a' = g\,b'$ (so in particular $f\,a = g\,b$).

\subsubsection{Technical lemmas on the pullback}

The pullback will be of key importance in our development. We will make use of the following technical lemmas,
for a pullback $A\circledast B$ of $f : A \to C$ and $g: B \to C$.

\begin{lemma}[Characterization of immediate causality]
Take $f: A\to C$ and $g: B \to C$, and take their pullback $A\circledast B$. Suppose moreover that in the
pullback, we have:
\[
[(a, b)]_x \imc [(a', b')]_x
\]
Then necessarily, $a\imc a'$ or $b\imc b'$.
\label{lem:imc_pullback}\label{causality_in_the_pullback}
\end{lemma}
\begin{proof}
Suppose first we have $a \leq a'$ or $b\leq b'$, say \emph{w.l.o.g.} $a < a'$. Suppose, looking for a 
contradiction, that this dependency is not immediate: there is $a''$ such that $a < a'' < a'$. But then
$[(a', b')]_x$ must contain some $(a'', b'')$. Then we have:
\[
[(a, b)]_x \subset [(a'', b'')]_x \subset [(a', b')]_x
\]
Contradicting the immediate causality $[(a, b)]_x \imc [(a', b')]_x$, so $a\imc a'$.

Suppose we have neither $a\leq a'$ nor $b \leq b'$. But then, setting $y = [(a', b')]_x$ we
have $y \setminus (a, b) \in \conf{A\circledast B}$. To prove that, the only non-trivial condition
to check is that its projections are still configurations. Suppose by contradiction that $\pi_1 (y\setminus (a,b)) 
\not \in \conf{A}$. This means that there is $a''\in y$ such that $a \leq a''$, so $y\setminus (a,b)$ is not 
down-closed anymore. But then there is $(a'', b'') \in y$ with:
\[
(a, b) \leq_x (a'', b'')
\]
But $(a'', b'') \leq_x (a', b')$ as well by definition of $y$, so that contradicts the hypothesis $[(a, b)]_x \imc [(a', b')]_x$.
\end{proof}

\begin{lemma}[Characterization of immediate conflict]
Take $f: A\to C$ and $g: B \to C$, and take their pullback $A\circledast B$. Suppose moreover that in the
pullback, we have $x\in \conf{A\circledast B}$ with $x \longcov{[(a, b)]_y}, x \longcov{[(a', b')_{y'}]}$
but $x \cup \{[(a, b)]_y, [(a', b')]_{y'}\} \not \in \conf{A\circledast B}$. Then either
$\Pi_1\,x \cup \{a, a'\} \not \in \conf{A}$, or $\Pi_2\,y\cup \{b, b'\} \not \in \conf{B}$.
\label{lem:conflict_pullback}\label{lemma:pbconflict}
\end{lemma}
\begin{proof}
If we had both $\Pi_1\,\cup \{a, a'\} \in \conf{A}$ and $\Pi_2\,\cup \{b, b'\}$, then 
$x \cup \{[(a, b)]_y, [(a', b')]_{y'}\}$ would have its two projections respectively in $\conf{A}$ and
$\conf{B}$. However it obviously satisfies the other conditions of configurations of the product, and
is in the restriction involved in the definition of the pullback; therefore it is a valid configuration
of $A\circledast B$, absurd.
\end{proof}


Very often, we will reason at the level of configurations of the pullback rather than events. Such configurations
can be presented a bit more simply:

\begin{proposition}
Configurations of $A\circledast B$ uniquely correspond to the composition bijections between $x\in \conf{A}$ and
$y\in \conf{B}$:
\[
x \stackrel{f}{\iso} f(x) = g(y) \stackrel{g}{\iso} y
\]
that are \textbf{secured}, in the sense that the transitive relation generated by
$(a, b) \leq (a', b')$ iff $a\leq a'$ or $b\leq b'$ is a partial order -- in other words there is no causal loop.
\label{prop:secured}
\label{secured1}
\end{proposition}
\begin{proof}
Simple verification.
\end{proof}


\subsection{Symmetry}

The basic theory of event structures with symmetry is introduced and developed in \cite{DBLP:journals/entcs/Winskel07}. In this
preliminary section, we oly recall some basic definitions, then state and/or prove some lemmas used in our
development.

\subsubsection{Event structures with symmetry}

\begin{definition}[Open maps]
  A map $f : A {\rightarrow} B$ between event structures is \emph{open} whenever
  it is rigid (preserves causal dependency) and for each configuration
  $x$ of $A$ and $y$ configuration of $B$ such that $fx \subseteq y$
  then $x$ can be extended to a configuration $x'$ of $A$ such that
  $fx' = y$.
\end{definition}
\begin{definition}[Event structure with symmetry]
  An event structure with symmetry (ess for short) $\A$ is a tuple $(A, \tilde A, l_A, r_A)$
  where $A$ and $\tilde{A}$ are event structures, and $l_A, r_A$ form a span:
  \[
  \xymatrix{
  A&\tilde{A}\ar[l]_{l_A} \ar[r]^{r_A}& A
  }
  \]
  such that $l_A, r_A$ are jointly monic (\emph{i.e.} their pairing $\tuple{l_A, r_A}$ is
  monic) and satisfy diagrams presenting categorically equivalence relations, see \emph{e.g.} \cite{DBLP:journals/entcs/Winskel07}.
  Moreover, $l_A$ and $r_A$ are supposed to be open maps.
\end{definition}

We do not recall the diagrams expressing the fact that $l_A, r_A$ form an equivalence since they
are standard, and actually not used much in our development.


We use the notation $\A, \B, \C$ to range over event structures with symmetry whose underlying event structures will be denoted $A, B, C, {\ldots}$ and symmetries $\tilde A, \tilde B, \tilde C, {\ldots}$
An alternative definition of event structures with symmetry can be
given in terms of isomorphism families:
\begin{definition}[Isomorphism families]
  An \textbf{isomorphism family} on event structure $A$ is a set 
  $\mathbb S_A$ of
  bijections between configurations of $A$ containing the identities $\id_x : x \iso x$,
  closed under composition and inverse, and satisfying two
  more properties:
  \begin{itemize}
  \item Whenever ${\theta}: x {\cong} y {\in} \mathbb S_A$ and $x'$ a
    sub-configuration of $x$ then ${\theta}\vert_{x'}$ the restriction
    of ${\theta}$ to $x'$ must belong to $\mathbb S_A$
  \item Whenever ${\theta} : x {\cong} y {\in} \mathbb S_A$ and $x \subseteq x' {\in} {\mathscr{C}}(A)$
    then there exists ${\theta}' \supseteq {\theta}$ in $\mathbb S_A$ such that the
    domain of ${\theta}'$ is $x'$.
  \end{itemize}
\end{definition}
Note that because of restriction, any bijection which belongs to $\mathbb S_A$ is also an order-isomorphism,
\emph{i.e.} it preserves and reflects causal order. 

Isomorphism families can be regarded as a more concrete presentation of symmetries on event structures. Any
symmetry $(\tilde{A}, l_A, r_A)$ on event structure $A$ generates an isomorphism family by setting:
\[
\mathbb{S}_A = \{\{(l_A \tilde{a}, r_A \tilde{a})\mid \tilde{a}\in x\} \mid x\in \conf{\tilde{A}}\}
\]
Likewise $\mathbb{S}_A$ is a stable family on the set of events $A\times A$, therefore one can redefine
the symmetry \emph{via} the primes construction, as $\Pr(\mathbb{S}_A)$. One can check that the event 
structure defined in this way along with the obvious projections is a symmetry isomorphic to the original.
This connection is worked out in all details in \cite{DBLP:journals/entcs/Winskel07}. In our development, we will mostly work with the
isomorphism families and leave the symmetry implicit.

If $\A$ is an event structure with symmetry, we will write:
\[
x \stackrel{\theta}{\iso_\A} y 
\]
if $\theta : x \iso y$ is in $\mathbb{S}_A$.

\begin{definition}[Maps of event structures with symmetry]
  A map $f : \A {\rightarrow} \B$ of event structures with symmetry is a
  map $f : A {\rightarrow} B$ of event structures such that for each
  isomorphism $x \stackrel{\theta}{\iso_\A} y$, the bijection induced by $f$:
  \[
  f\,\theta = \{(f(a_1), f(a_2))\mid (a_1, a_2) \in \theta\}
  \]
  is in $\mathbb{S}_B$.

  Or equivalently, there exists a (necessarily
  unique) map $\tilde f : \tilde A{\rightarrow} \tilde B$ such that $l_B \circ \tilde{f}= f\circ l_A$,
  and $r_B \circ \tilde{f} = f \circ r_B$.
\end{definition}

There is a category $\ESS$ of event structures with symmetry and maps preserving symmery, and a 
category $\ESSP$ in the presence of polarities, which the isomorphisms and maps should preserve.

Symmetry allow us to identify maps that play symmetric events:
\begin{definition}[Symmetric maps]
  Let $f, g : \A {\rightarrow} \B$ be two parallel maps of event structures with
  symmetry. We say that $f$ and $g$ are symmetric (notation: $f\sim
  g$) when for any configuration $x$ in $A$, the induced bijection:
  \[
  \theta = \{(f(a), g(a))\mid a \in x\}
  \]
  is in $\mathbb{S}_B$.

  Or equivalently, there is a (necessarily unique) $h : A\to \tilde{B}$ such that 
  $l_B \circ h = f$ and $r_B \circ h = g$.
\end{definition}
This relation $\sim$ is preserved by composition,
which makes $\ESS$ and $\ESSP$ enriched over equivalence relations, or (rather degenerate) strict 2-categories.

%As an example of symmetry, one can endow $\oc A$ with a symmetry:
%\begin{lemma}[Symmetry on $\oc A$]
%  The set of isomorphisms of $\oc A$ consisting in the sets of all the order-isomorphisms:
%\[
%x \stackrel{\theta}{\iso} y
%\]
%such that $\lbl\circ \theta = \lbl$ is a symmetry on $!A$
%\end{lemma}
%\begin{proof}
%  Clearly this set contains the identity and is stable under
%  composition, inverse and restriction. If we have $x \stackrel{{\theta}} {\cong}
%  y$ and $x \longcov{{\alpha}:[a] {\rightarrow} {\omega}}$ then we must have $[a) \subseteq
%  \lbl(x)$ and thus we can define ${\alpha}'(a) = {\alpha}(a)$ and ${\alpha}'(b) =
%  \ind({\theta}(b))$. That gives ${\alpha}' : [a] {\rightarrow} {\omega}$ such that $y \longcov {\alpha'}$ and
%  ${\theta} \cup\{{\alpha}, {\alpha}'\}$ is a valid symmetry of $!A$.
%\end{proof}
\subsubsection{Higher symmetry}
\label{sec:highsymm}

%The category of event structures with symmetry does not have pullbacks
%in general but has pseudo-pullbacks. We have a similar characterisation
%of configurations of a pseudo pullback, similar to the one of Lemma
%\ref{secured1}:
%\begin{lemma}\label{secured2}
%  Let $f : \A {\rightarrow} \C, g : \B {\rightarrow} \C$ be maps between event structures with
%  symmetry. Configurations of the pseudo-pullback are triples $(x, {\theta},
%  y)$ such that $x {\in} {\mathscr{C}}(A)$, $y {\in} {\mathscr{C}}(B)$ and ${\theta} {\in} \mathbb S_C$ with $fx
%  \stackrel{{\theta}} {\cong} gy$. Isomorphisms between $(x, {\theta}, y)$ and $(x', {\theta},
%  y')$ in the symmetry of the pseudo-pullback are given by ${\varphi} : x {\cong} x'$ and ${\psi} : y {\cong} y'$ such that
%$$\xymatrix{
%\ar[d]_{f{\varphi}} fx \ar[r]^{{\theta}} & gy \ar[d]^{g{\psi}} \\
%fx' \ar[r]_{{\theta}'} & gy'
%}$$
%\end{lemma}
%
%
%If $\A$ is an event structure with symmetry, then $\tilde{\A}$ can be obtained, itself as an event structure
%with symmetry, via the pseudo-pullback:
%\[
%\xymatrix{
%&\tilde{\A}
%        \ar[dl]
%        \ar[dr]
%        \ar@{}[dd]|{\sim}
%        \pb{270}\\
%\A       \ar[dr]_{id_\A}&&
%\A       \ar[dl]^{id_\A}\\
%&\A
%}
%\]

If $\A$ is an event structure with symmetry, then its symmetry $\tilde{A}$ is itself canonically equipped with a 
symmetry. Although it can be described via a universal property (pseudopullbacks -- see \cite{lics14}), here
we define it instead through its isomorphism family. 

As we have seen above, configurations of $\tilde{A}$ correspond to isomorphisms $\theta \in \mathbb{S}_A$. By abuse of
notations, we will often silently go from one to the other. In particular, configurations on $\tilde{\tilde{A}}$ should
correspond to certain bijections between isomorphisms $\theta, \theta'\in \mathbb{S}_A$ (seen as subsets of $A\times A$).
We ask the isomorphism family of $\tilde{A}$ to comprise bijections between $\theta, \theta'$ corresponding to 
commuting squares: 
\[
\xymatrix@R=15pt@C=15pt{
x       \ar@{}[r]|{\stackrel{\phi}{\iso_\A}}&
x'\\
y       \ar@{}[u]|{\theta \rotatebox{-90}{$\iso$}_\A}
        \ar@{}[r]|{\stackrel{\phi'}{\iso_\A}}&
y'      \ar@{}[u]|{{\theta'}\rotatebox{-90}{$\iso$}_\A}
}
\]
According to this characterisation, $l_{\tilde{A}}$ sends this square to its left side and $r_{\tilde{A}}$ sends it
to its right side. However, there are now additional maps $u_{\tilde{A}}$ sending it to its upper side and $d_{\tilde{A}}$
sending it to its lower side. These additional projections satisfy the diagram:

\[
\xymatrix@R=0pt{
&\tilde{\tilde{S}}
        \ar[dl]_{l_{\tilde{S}}}
        \ar[dd]^{u_{\tilde{S}}}
        \ar[dr]^{r_{\tilde{S}}}&&&
\tilde{\tilde{S}}
        \ar[dl]_{l_{\tilde{S}}}
        \ar[dd]^{d_{\tilde{S}}}
        \ar[dr]^{r_{\tilde{S}}}\\
\tilde{S} \ar[dd]_{l_S}&&
\tilde{S} \ar[dd]^{r_S}&
\tilde{S} \ar[dd]_{r_S}&&
\tilde{S} \ar[dd]^{r_S}\\
&\tilde{S}\ar[dl]_{l_S}
        \ar[dr]^{r_S}&&&
\tilde{S} \ar[dl]_{l_S}
        \ar[dr]^{r_S}\\
S&&S&S&&S
}
\]

We write $\tilde{\A}$ for $\tilde{A}$ \emph{equipped with its symmetry} $\tilde{\tilde{A}}$.
We can now automatically lift some properties from maps $f: \A \to \B$ to $\tilde{f}:\tilde{\A}\to \tilde{\B}$:

\begin{lemma}
We have the following lifting properties.
\begin{enumerate}
\item If $f : \A \arrow \B$ is a morphism in $\ESS/\ESSP$, then $\tilde{f} : \tilde{\A} \arrow \tilde{\B}$ preserves symmetry as well.
\item If $f \sim g$, then $\tilde{f} \sim \tilde{g}$,
%\item If $\sigma : S \arrow A$ has a canonical extension, so does $\tilde{\sigma}$. Moreover, the canonical extension of $\tilde{S}$ coincides
%with that of $S$ in the sense that for all isomorphism $\theta_1 \iso_{\phi} \theta_2$ in $\tilde{\tilde{A}}$ such that $\theta_1 \subseteq \theta'_1$,
%we have:
%\begin{eqnarray*}
%u_{\tilde{A}}(\ext(\phi, \theta'_1)) &=& \ext(u_{\tilde{A}}(\phi), l_{\tilde{A}}(\theta'_1))\\
%d_{\tilde{A}}(\ext(\phi, \theta'_1)) &=& \ext(d_{\tilde{A}}(\phi), r_{\tilde{A}}(\theta'_1))
%\end{eqnarray*}
\end{enumerate}
\label{lem:lifting}
\end{lemma}
\begin{proof}
\emph{(1)} We need to check that $\tilde{f} : \tilde{A} \arrow \tilde{B}$ preserves symmetry. Take a isomorphism in $\tilde{\tilde{A}}$, corresponding
to a square:
\[
\xymatrix{
x       \ar@{}[d]|{\theta \rotatebox{270}{$\iso$}_{\A}}
        \ar@{}[r]|{\stackrel{\phi_1}{\iso_{\A}}}&
x'      \ar@{}[d]|{\theta' \rotatebox{270}{$\iso$}_{\A}}\\
y       \ar@{}[r]|{\stackrel{\phi_2}{\iso_{\A}}}&
y'
}
\]
The component-wise image of this isomorphism by $\tilde{f}$ corresponds to the commuting square:
\[
\xymatrix{
fx       \ar@{}[d]|{f\theta \rotatebox{270}{$\iso$}_{\B}}
        \ar@{}[r]|{\stackrel{f\phi_1}{\iso_{\B}}}&
fx'      \ar@{}[d]|{f\theta' \rotatebox{270}{$\iso$}_{\B}}\\
fy       \ar@{}[r]|{\stackrel{f \phi_2}{\iso_{\B}}}&
fy'
}
\]
which corresponds to a configuration of the isomorphism family of $\tilde{\B}$ by definition.

\emph{(2)} Suppose $f \sim g$, this means that for any $x\in \conf{A}$, the isomorphism $\theta_x = \{(fa, ga)\mid a\in x\}$ is in the isomorphism
family of $x$. Then it is clear that for any isomorphism $x \iso_\phi y$ in the isomorphism family of $A$, the following square commutes:
\[
\xymatrix{
fx       \ar@{}[d]|{\rotatebox{270}{$\iso$}_{f \phi}}
        \ar@{}[r]|{\iso_{\theta_x}}&
gx      \ar@{}[d]|{\rotatebox{270}{$\iso$}_{g \phi}}\\
fy       \ar@{}[r]|{\iso_{\theta_y}}&
gy
}
\]
Indeed take $(a, b)\in \phi$. Then we have $(fa, fb)\in f \phi$, $(ga, gb)\in g\phi$, $(fa, ga)\in \theta_x$ and $(fb, gb)\in \theta_y$.
But this square corresponds to an isomorphism between $f\phi$ and $g\phi$ in $\tilde{B}$, so we do have $\tilde{f} \sim \tilde{g}$.

\end{proof}

\subsubsection{Projections with symmetry}

In this small subsection, we introduce a few definitions and lemmas regarding the generalisation
of projection in the presence of symmetry.

\begin{definition}
Let $\A$ be an event structure with symmetry. A subset $V\subseteq A$ is \emph{closed under symmetry} iff, setting
\[
\tilde{V} = \{\tilde{a}\in \tilde{A} \mid l_A(\tilde{a}) \in V\}
\]
we have $\sigma_A(\tilde{V}) = \tilde{V}$ (where $\sigma_A : \tilde{A} \to \tilde{A}$ is the map expressing that as an equivalence relation, the
symmetry is symmetric).
\label{def:closed_symm}
\end{definition}

\begin{prop}
Let $\A$ be an event structure with symmetry, let $V$ be a subset of the events of $A$ closed under symmetry. Then the triple
$(\tilde{A} \proj \tilde{V}, l_A \restrict \tilde{V}, r_A \restrict \tilde{V})$ (where $\restrict$ denotes function restriction) is
a symmetry on $A\proj V$.

The event structure with symmetry $(A \proj V, \tilde{A} \proj \tilde{V})$ is called the \textbf{projection} of $A$ on $V$.
\label{prop:proj_symm}
\end{prop}
\begin{proof}
A subset $V$ is closed under symmetry if and only if it is the domain of a partial map of event structures preserving
symmetry. According to this, this proposition is a restatement of the partial-total factorisation result for event
structures with symmetry \cite{lics14,DBLP:journals/entcs/Winskel07}.
\end{proof}


tcg.tex
In this section, we introduce the basic compact closed category that serves
as a base for our forthcoming concurrent generalisation of Hyland-Ong games.
The basic idea is to construct a compact closed ($\sim$-bi-)category 
analogous to \cite{DBLP:conf/lics/RideauW11} in the presence of symmetry. 


In \cite{lics14}, we constructed such a compact closed category of concurrent games based
on event structures with symmetry. What we describe here is very
close to \cite{lics14}, but does differ in a crucial point. In the basic compact closed
category of \cite{lics14} strategies are \emph{saturated}, in the sense that whenever they
are in position to play a particular event they must also be prepared to play (non-deterministically)
all events symmetric to it. Saturation enables a greater generality (it is required
in particular to define an exponential on non-polarized games). However, for the vast majority
of the applications that we have in mind to program semantics, that generality does not seem
to be needed. So instead of directly building on \cite{lics14}, we start by developing a non-saturated
variant of it.


As the reader will see, developing such a non-saturated variant is far from being a formality. In fact,
it is arguably the most significant technical contribution of this paper -- it is definitely the part
whose development took the most time and effort. Its key advantage is that the symmetry-aware constructions
on games and strategies involved are all compatible with \cite{DBLP:conf/lics/RideauW11} -- meaning that although the \emph{soundness}
of the basic operations on games and strategies heavily involves symmetry, their \emph{definition} is independent 
from symmetry.
So, ignoring the symmetry layer, one immediately gets the games of \cite{DBLP:conf/lics/RideauW11}. This is in contrast with \cite{lics14} where
composition and copycat are changed to a symmetry-aware version. Whereas in \cite{lics14} the key difficulty was to 
find symmetry-friendly notions of copycat and composition, here we find conditions that make the copycat and
composition of \cite{DBLP:conf/lics/RideauW11} symmetry-friendly.


Beyond its technical advantages, we believe that this approach yields more economical representations of
the execution of programs.

\subsection{Thin concurrent games with symmetry}

In this first subsection, we define the notion of games that we are going to work
with.

\begin{definition}
  An essp $\A$ is thin if for all $x\stackrel{\theta}{\iso_\A} y$, if
  $\theta$ has positive extensions to valid isomorphisms $x_1
  \stackrel{\theta_1}{\iso_\A} y_1$ and $x_2
  \stackrel{\theta_2}{\iso_\A} y_2$ with $\theta \subseteq^+ \theta_1,
  \theta \subseteq^+\theta_2$, if $x_1 \cup x_2 \in \conf{A}$ then
  $\theta_1 \cup \theta_2$ is a valid isomorphism as well. 

  Or equivalently, $l_A$ and $r_A$ reflects positive compatibility.
\end{definition}

In order to state the definition below, we need the notion of
sub-symmetry. A \textbf{sub-symmetry} of an essp $\A$ is 
a sub-event structure $\tilde{A}'$ of $\tilde{A}$ that
is still a symmetry for $A$. We say that it is a \textbf{receptive
  sub-symmetry} if for any $x\in \conf{\tilde{A}'}$, if $x\subseteq^-
y \in \conf{\tilde{A}}$, then $y\in \conf{\tilde{A}'}$ as well. In
other words a sub-symmetry is receptive when the embedding map $\id_A
: (A, \tilde{A}') \to (A, \tilde{A})$ is strong-receptive (in the sense of \cite{lics14}, 
also recalled later).

\begin{definition}[Thin Concurrent game]
  A \textbf{thin concurrent game} (tcg for short) is an essp such that:
  \begin{itemize}
%  \item $(A,\leq)$ is a conflict-free forest: if $a, a' \leq a''$ then either $a\leq a'$ or $a'\leq a$.
%  \item $A$ is alternating: if $a \imc a'$ then $\pol(a) \neq \pol(a')$.
  \item It is \textbf{race-preserving}, \emph{i.e.} the projection $l_A : \tilde A \to A$ preserves 
  races: if $x\in \conf{\tilde{A}}$ with
  $x\cov{a_1^-}, x\cov{a_2^+}$ but $x\cup \{a_1, a_2\} \not \in \conf{\tilde{A}}$, then $l_A\,x \cup \{l_A\,a_1, l_A\,a_2\}
  \not \in \conf{A}$ either. It automatically follows that $r_A$ preserves races as well.
  \item $\A$ has $\tilde{A}_-$ and $\tilde{A}_+$, thin receptive sub-symmetries of $\A^\perp$ and $\A$ respectively.
  \end{itemize}
\end{definition}

The fact that $l_A$ preserves races will be essential for copycat to have a symmetry.
Along with the sub-symmetry condition, they will ensure that composition preserves equivalence 
between strategies.

The set of concurrent games with symmetry is closed under parallel composition and dual $(-)^\perp$, in the
obvious way.

%Moreover, it contains $!A$ for any arena $A$:
%\begin{proposition}\label{prop:def_oc}
%  If $A$ is an arena, $!A$ is a concurrent games with symmetry.
%\end{proposition}
%\begin{proof}
%  It is clear that $!A$ is an alternating forest. We already built the
%  symmetry on $!A$. It is clearly race-free. To build the thin
%  sub-symmetries $!A_+$ and $!A_-$, consider the isomorphism of $!A$
%  that preserve label and indices of positive or negative events.
%\end{proof}

\begin{definition}
  A \textbf{pre-$\sim$-strategy} $\sigma : \S \to \A$ is just a map of essps.

  A \textbf{$\sim$-strategy} ${\sigma} : \S {\rightarrow} \A$ is a pre-$\sim$-strategy such that:
\begin{itemize}
\item[(1)] $\sigma : S \to A$ is \textbf{courteous}\footnote{Called \emph{innocent} in \cite{DBLP:conf/lics/RideauW11} and \cite{lics14} -- we
switched to courteous here (following \cite{DBLP:conf/concur/MelliesM07}) to avoid collision with Hyland-Ong innocence.}: if
$s_1, s_2 \in S$ such that $s_1 \imc s_2$ and $\pol(s_1) = +$ or $\pol(s_2) = -$, then $\sigma\,s_1 \imc \sigma\,s_2$.
\item[(2)] $\sigma : \S \to \A$ is \textbf{strong-receptive}: if
\[
x \stackrel{\theta}{\iso_\S} y
\]
with $\sigma\,\theta \cov{(a_1, a_2)}$, then there is a unique $\theta \cov{(s_1, s_2)}$ such that
$\sigma s_1 = a_1$ and $\sigma s_2 = a_2$. Equivalently, $\tilde{\sigma}$ is receptive in the sense
of \cite{DBLP:conf/lics/RideauW11}. Together with courtesy, this means that $\tilde{\sigma}$ is a
strategy in the sense of \cite{DBLP:conf/lics/RideauW11}.
\item[(3)] $\sigma : \S \to \A$ is \textbf{thin}, in the sense that $\S$ is thin.
\end{itemize}

Recall from \cite{DBLP:conf/lics/RideauW11} that a map of essp $\sigma : S \to A$ (without symmetry) is referred to as a \textbf{pre-strategy},
and a \textbf{strategy} if it satisfies \emph{(1)} and \emph{(2)}. We will use this terminology later on in the 
text when the map has to be considered independently of symmetry.
\end{definition}

Note that it automatically follows that $\tilde{\sigma} : \tilde{\S} \to \tilde{\A}$ is itself a $\sim$-strategy:

\begin{lemma}
  Let ${\sigma} : \S {\rightarrow} \A$ be a $\sim$-strategy, then so is $\tilde {\sigma} : \tilde \S {\rightarrow} \tilde \A$.
\end{lemma}
\begin{proof}
  Courtesy is a consequence of the rigidity of $l$ and $r$. Thus
  we only need to prove that $\tilde{\sigma}$ is strong-receptive,
  \emph{i.e.} that $\tilde{\tilde{\sigma}}$ is receptive, and that $\tilde{\S}$ is thin. Suppose we
  have a configuration in $\tilde{\tilde{S}}$, represented by a
  square:
\[
\xymatrix{
x_1     \ar@{}[r]^{\phi}|{\iso_S}&
x_2\\
y_1     \ar@{}[r]^{\phi'}|{\iso_S}
        \ar@{}[u]^{\theta~}|{\rotatebox{270}{$\iso$}_S}&
y_2     \ar@{}[u]^{~\theta'}|{\rotatebox{270}{$\iso$}_S}
}
\]
Suppose that the image by $\tilde{\tilde{\sigma}}$ of this configuration extends in the following way:
\[
\xymatrix@C=50pt{
\sigma x_1\cup\{a_1\}
        \ar@{}[r]^{\sigma\phi \cup \{(a_1, a_2)\}}|{\iso_A}&
\sigma x_2\cup\{a_2\}\\
\sigma y_1\cup\{a'_1\}
        \ar@{}[r]^{\sigma\phi' \cup \{a'_1, a'_2\}}|{\iso_A}
        \ar@{}[u]^{\sigma \theta \cup \{(a_1, a'_1)\}~}|{\rotatebox{270}{$\iso$}_A}&
\sigma y_2\cup \{a'_2\}
        \ar@{}[u]_{~\sigma \theta'\cup \{(a_2, a'_2)\}}|{\rotatebox{270}{$\iso$}_A}
}
\]
where all $a_1, a_2, a'_1, a'_2$ have negative polarity. By receptivity of $\sigma$ there are unique $s_1, s_2, s'_1, s'_2$ mapping
respectively to $a_1, a_2, a'_1, a'_2$ by $\sigma$. By receptivity of $\tilde{\sigma}$, we necessarily have that
$\theta \longcov{(s_1, s'_1)}, \theta' \longcov{(s_2, s'_2)}, \phi \longcov{(s_1, s_2)}$ and $\phi'\longcov{(s'_1, s'_2)}$,
so that the following commutative diagram corresponds to an isomorphism in $\tilde{\tilde{A}}$.
\[
\xymatrix@C=45pt{
x_1\cup\{s_1\}
        \ar@{}[r]^{\phi\cup \{(s_1, s_2)\}}|{\iso_S}&
x_2\cup\{s_2\}\\
y_1\cup\{s'_1\}
        \ar@{}[u]^{\theta\cup \{(s_1, s'_1)\}~}|{\rotatebox{270}{$\iso$}_S}
        \ar@{}[r]^{\phi'\cup \{(s'_1, s'_2)\}}|{\iso_S}&
y_2\cup\{s'_2\}
        \ar@{}[u]_{~\theta'\cup \{(s_2, s'_2)\}}|{\rotatebox{270}{$\iso$}_S}
}
\]
uniqueness is a trivial consequence of the uniqueness for receptivity
of $\sigma$.

Let us now show that $\tilde{\S}$ is thin. Take a configuration of $\tilde{\tilde{S}}$, regarded
as a commuting square:
\[
\xymatrix{
x_1     \ar@{}[r]^{\phi}|{\iso_S}&
x_2\\
y_1     \ar@{}[r]^{\phi'}|{\iso_S}
        \ar@{}[u]^{\theta~}|{\rotatebox{270}{$\iso$}_S}&
y_2     \ar@{}[u]^{~\theta'}|{\rotatebox{270}{$\iso$}_S}
}
\]
Suppose it extends positively to $\phi_1$, $\phi'_1$, $\theta_1$, $\theta'_1$,
and alternatively to $\phi_2, \phi'_2, \theta_2, \theta'_2$ with compatible left projections. Since $\S$
is thin, it follows that $\phi_1 \cup \phi_2, \phi'_1 \cup \phi'_2, \theta_1\cup \theta_2$ are compatible.
By composition, it also follows that $\theta'_1 \cup \theta'_2$ is compatible as well. Putting these 
together, the two extensions of the commuting square are compatible as well, so the left projection
reflects positive compatibility.
\end{proof}

\subsection{Weak equivalence of $\sim$-strategies}

As notion of equivalence between $\sim$-strategies we introduce \emph{weak equivalence},
that adequately weakens isomorphism of strategies in the presence of symmetry. In particular,
it allows us to consider equivalent $\sim$-strategies that might play the same events, but
with a different choice of copy indices.

\begin{definition}[Weak equivalence]
  Let ${\sigma} : \S {\rightarrow} \A$ and ${\tau} : \T {\rightarrow} \A$ be $\sim$-strategies on a tcg $\A$. 
  A \textbf{weak equivalence} between $\sigma$ and $\tau$ is given by two morphisms of essps $f: \S \to \T$
  and $g: \T \to \S$ such that $f\circ g \sim \id_\T$, $g\circ f \sim \id_\S$, $\tau \circ f \sim \sigma$ and
  $\sigma \circ g \sim \tau$.
\end{definition}

A central difficulty in our endeavour will be to show that weak equivalence
is preserved under composition. Readers familiar with AJM games may note that
this difficulty already exists there, where one has to show that equivalence
between strategies is preserved under composition. Here, the richer structure
of our strategies makes this fact more technical. This is where our \emph{thin}
requirement on essps comes in. 

In particular, preservation of weak equivalence under composition will use the
fact that the isomorphism family of thin essps satisfy the coherent positive
extension property below.

\begin{definition}
Let $\A$ be an essp. We say that $\A$ has a \textbf{coherent extension} iff for each $x\stackrel{\theta}{\iso_A} y$,
for each $x \subseteq^+ x'\in \conf{A}$ there is $y \subseteq^+ y'\in \conf{A}$ and $x'\stackrel{\ext(\theta, x')}{\iso_A} y'$ 
such that $\theta \subseteq^+ \ext(\theta, x')$. Moreover the function $\ext$ (the \emph{coherent extension}) should 
satisfy the two following properties:
\begin{itemize}
\item \emph{(monotonicity)} If $x_1 \iso_{\theta} y_1$ and $x_1 \subseteq^+ x_2 \subseteq^+ x_3$, then
\[
\ext(\ext(\theta, x_2), x_3) = \ext(\theta, x_3)
\]
\item \emph{(stability)} If $x_1 \iso_{\theta_1} y_1$, $\theta_1 \subseteq^- \theta_2$ (writing $x_2 \iso_{\theta_2} y_2$)
with $x_1 \subseteq^+ x'_1$ such that $\{\ext(\theta_1, x'_1), \theta_2\} \uparrow$, then
\[
\ext(\theta_1, x'_1) \subseteq \ext(\theta_2, x_2 \cup x'_1)
\]
\end{itemize}
\end{definition}
This condition is implied by the thin condition:
\begin{lemma}
If $\sigma : \S \to \A$ is a $\sim$-strategy, then $\S$ has a coherent extension.
\label{lem:cohext}
\end{lemma}
\begin{proof}
Note first that for any $x \stackrel{\theta}{\iso_S} y$ and $x \subseteq^+ x'$, then by the extension property of
isomorphism families there is $y \subseteq^+ y'$ and $\theta \subseteq \theta'$ such that
$x' \stackrel{\theta'}{\iso_S} y'$. But $\theta'$ is actually uniquely defined since if there was
another $x' \stackrel{\theta''}{\iso_S} y''$ it would yield a positive conflict. Since $\sigma$ is a thin
strategy, this positive conflict should be preserved by $l_S$ but that is obviously not the case, therefore
$\theta' = \theta''$. Using that, the monotonicity condition is obvious.

For stability, take $x_1 \iso_{\theta_1} y_1$, $\theta_1 \subseteq^- \theta_2$ (writing $x_2 \iso_{\theta_2} y_2$) with
$x_1 \subseteq^+ x'_1$ such that $\{\ext(\theta_1, x'_1), \theta_2\} \uparrow$. By restriction, there is $\theta
\subseteq \ext(\theta_2, x_2 \cup x'_1)$ such that $l_A(\theta) = x'_1$. By restriction again it restricts again to
$\theta' \subseteq \theta$ with $l(\theta') = x_1$. But then $\theta'$ and $\ext(\theta_1, x'_1)$ are two positive
extensions of $\theta_1$ whose left projection is $x'_1$. If their right projection was different then that would
be a positive conflict in $\tilde{S}$, immediately contradicting preservation of positive conflict. Therefore
$\theta'$ and $\ext(\theta_1, x'_1)$ must be equal.
\end{proof}


\begin{lemma}
Suppose $\sigma : \S \to \A$ is a $\sim$-strategy. Then, the coherent extension of $\tilde{\S}$ coincides
with that of $\S$ in the sense that for any isomorphism $\theta_1 \stackrel{\phi}{\iso_{\tilde{S}}} \theta_2$ such that $\theta_1 \subseteq^+ \theta'_1$,
we have:
\begin{eqnarray*}
u_{\tilde{S}}(\ext(\phi, \theta'_1)) &=& \ext(u_{\tilde{S}}(\phi), l_{\tilde{A}}(\theta'_1))\\
d_{\tilde{S}}(\ext(\phi, \theta'_1)) &=& \ext(d_{\tilde{S}}(\phi), r_{\tilde{A}}(\theta'_1))
\end{eqnarray*}
\label{lem:liftingce}
\end{lemma}
\begin{proof}
%As we have seen, configurations of $\tilde{\tilde{S}}$ can be described as commuting squares:
%\[
%\xymatrix@R=15pt@C=15pt{
%x       \ar@{}[r]|{\stackrel{\phi}{\iso_S}}&
%x'\\
%y       \ar@{}[u]|{\theta\rotatebox{90}{$\iso$}_S}
%        \ar@{}[r]|{\stackrel{\phi'}{\iso_S}}&
%y'      \ar@{}[u]|{{\theta'}\rotatebox{90}{$\iso$}_S}
%}
%\]
%Where, $l_{\tilde{S}}$ sends this square to its left side and $r_{\tilde{S}}$ sends it to its right side. Suppose there are
%two conflicting positive extensions, for $i\in \{1, 2\}$:
%\[
%\xymatrix@R=15pt@C=15pt{
%x_i       \ar@{}[r]|{\stackrel{\phi_i}{\iso_S}}&
%x'_i\\
%y_i       \ar@{}[u]|{\theta_i\rotatebox{90}{$\iso$}_S}
%        \ar@{}[r]|{\stackrel{\phi'_i}{\iso_S}}&
%y'_i      \ar@{}[u]|{{\theta'_i}\rotatebox{90}{$\iso$}_S}
%}
%\]
%The fact that this is a conflict amounts to the fact that one of $\phi_1\cup \phi_2$, $\phi'_1 \cup \phi'_2$,
%$\theta_1\cup \theta_2$, $\theta'_1 \cup \theta'_2$ is not a valid isomorphism. Note that this must be true
%for at least two of them, since the fourth can be obtained via composition. So it must be true for at least
%one which shares an endpoint with the left hand side of the square. Since $l_S$ and $r_S$ preserve positive
%conflict, it follows that $x_1 \cup x_2 \not \in \conf{S}$ or $y_1 \cup y_2 \not \in \conf{S}$. Therefore
%$\theta_1 \cup \theta_2$ cannot be a valid isomorphism, and $l_{\tilde{S}}$ preserves positive conflict.
%
First, we describe the coherent extension of $\tilde{\S}$. Take a configuration of $\tilde{\tilde{S}}$, described
as a commuting square of isomorphisms:
\[
\xymatrix{
x_1     \ar@{}[r]^{\psi}|{\iso_\S}&
x_2\\
y_1     \ar@{}[r]^{\psi'}|{\iso_\S}
        \ar@{}[u]^{\theta_1}|{\rotatebox{270}{$\iso$}_\S}&
y_2     \ar@{}[u]^{~\theta_2}|{\rotatebox{270}{$\iso$}_\S}
}
\]
Suppose also that $\theta_1$ extends positively to $x'_1 \iso_{\theta'_1} y'_1$. Then, the unique positive
extension is:
\[
\xymatrix@C=40pt{
&x'_1
        \ar@{}[r]|{\iso_{\ext(\psi, x'_1)}}
&x'_2\\
x'_1
        \ar@{=}[ur]
&x_1    \ar@{}[l]|{\supseteq}
        \ar@{}[u]|{\rotatebox{90}{$\subseteq$}}
        \ar@{}[r]|{\iso_\psi}
&x_2
        \ar@{}[u]|{\rotatebox{90}{$\subseteq$}}
        \ar@{}[r]|{\subseteq}
&x'_2
        \ar@{=}[ul]\\
y'_1
        \ar@{}[u]|{\rotatebox{90}{$\iso$}_{\theta'_1}}
&y_1
        \ar@{}[l]|{\supseteq}
        \ar@{}[u]|{\rotatebox{90}{$\iso$}_{\theta_1}}
        \ar@{}[r]|{\iso_{\psi'}}
&y_2
        \ar@{}[u]|{\rotatebox{90}{$\iso$}_{\theta_2}}
        \ar@{}[r]|{\subseteq}
&y'_2   
        \ar@{}[u]|{\rotatebox{90}{$\iso$}_{\theta'_2}}\\
&y'_1
        \ar@{=}[ul]
        \ar@{}[u]|{\rotatebox{90}{$\supseteq$}}
        \ar@{}[r]|{\iso_{\ext(\psi', y'_1)}}
&y'_2
        \ar@{}[u]|{\rotatebox{90}{$\supseteq$}}
        \ar@{=}[ur]
}
\]
where $\theta'_2 = \ext(\psi', y'_1) \circ (\theta'_1)^{-1} \circ \ext(\psi, x'_1)^{-1}$. The outer commuting
square gives us an extension $\ext(\phi, \theta'_1)$ of $\phi$, which satisfies the required equations.
\end{proof}


\subsection{Copycat} We now proceed to show how copycat
adapts to our framework. The definition of copycat without symmetry (as given \emph{e.g.} in \cite{DBLP:conf/lics/RideauW11,WGames}),
gives us:
\[
\cc_A : \CC_A \to A^\perp \parallel A
\]
We need to equip it with a symmetry. 

We start by showing that $\CC$ can be extended to a functor:
\[
\CC : \ESP \to \ESP
\]
Indeed, one can check that for $f : A \to B$ a map of esps, the map defined as:
\[
\begin{array}{rcccl}
\CC_f &:& \CC_A &\to& \CC_B\\
&& (1, a) &\mapsto& (1, f~a)\\
&& (2, a) &\mapsto& (2, f~a)
\end{array}
\]
It is still a map of esps, and by definition it is immediate that the construction is indeed functorial. This allows
us to formulate the tentative definition of a symmetry on copycat:
\begin{eqnarray*}
\widetilde{\CC_A} &=& \CC_{\tilde{A}}\\
l_{\CC_A} &=& \CC_{l_A}\\
r_{\CC_A} &=& \CC_{r_A}
\end{eqnarray*}
We need to check that $(\CC_{\tilde{A}}, \CC_{l_A}, \CC_{r_A})$ indeed is a symmetry on $\CC_A$. First we show that
it is an equivalence relation, which relies on the following lemma:


%We will use the \emph{Scott order} on the configurations of an esp $A$, defined by:
%\[
%x \sqsubseteq y \Leftrightarrow x \supseteq^- \subseteq^+ y
%\]
%

\begin{lemma}
The functor $\CC$ preserves pullbacks.
\end{lemma}
\begin{proof}
First, it is easy to check that the functors $(-)^\perp : \ESP \to \ESP$ and $\parallel : \ESP^2 \to \ESP$ preserve pullbacks.
So if we have a pullback square in $\ESP$:
\[
\xymatrix@R=10pt@C=10pt{
&P      \ar[dl]_{\Pi_1}
        \ar[dr]^{\Pi_2}
        \pb{270}\\
A       \ar[dr]_{f}&&
B       \ar[dl]^{g}\\
&C
}
\]
then the following is a pullback square as well:
\[
\xymatrix@R=10pt@C=10pt{
&P^\perp\parallel P
        \ar[dl]_{\Pi_1^\perp\parallel \Pi_1}
        \ar[dr]^{\Pi_2^\perp\parallel \Pi_2}
        \pb{270}\\
A^\perp \parallel A
        \ar[dr]_{f^\perp\parallel f }&&
B^\perp \parallel B
        \ar[dl]^{g^\perp \parallel g}\\
&C^\perp \parallel C
}
\]
We want to transport the universal property of the above pullback to the following commuting square:
\[
\xymatrix@R=10pt@C=10pt{
&\CC_P  \ar[dl]_{\CC_{\Pi_1}}
        \ar[dr]^{\CC_{\Pi_2}}
        \pb{270}\\
\CC_A   \ar[dr]_{\CC_f}&&
\CC_B   \ar[dl]^{\CC_g}\\
&\CC_C
}
\]
To do that, take $h_1 : X \to \CC_A$ and $h_2 : X \to \CC_B$ making the square commute, and form
$h = \tuple{\cc_A \circ h_1, \cc_B \circ h_2}$ using the universal property of the above pullback
square. To any $x\in \conf{X}$, $h$ associates a configuration $h(x)\in \conf{P^\perp\parallel P}$. By
Proposition \ref{prop:secured}, it corresponds to a secured bijection:
\[
\theta : y \iso (f^\perp \parallel f)(y) = (g^\perp \parallel g)(z) \iso z
\]
with $y\in \conf{A^\perp \parallel A}$ and $z\in \conf{B^\perp \parallel B}$. By definition of $f^\perp \parallel f$ and
$g^\perp \parallel g$ and writing $y = y_1 + y_2$ and $z = z_1 + z_2$, this decomposes into two secured bijections:
\[
\begin{array}{rcrcrcrcl}
\theta_1 &:& y_1 &\iso & f(y_1) &=& g(z_1) &\iso& z_1\\
\theta_2 &:& y_2 &\iso & f(y_2) &=& g(z_2) &\iso& z_2\\
\end{array}
\]
But we also know that $h_1(x) \in \CC_A$ and $h_2(x) \in \CC_B$, therefore $y_1 \supseteq^+ y_1 \cap y_2 \subseteq^- y_2$
and $z_1 \supseteq^+ z_1 \cap z_2 \subseteq^- z_2$. By definition of $\theta_1$ and $\theta_2$ we must have
$\theta_1 \supseteq^+ \theta_1 \cap \theta_2 \subseteq^- \theta_2$ as well, so $\theta_1 \sqsubseteq \theta_2$. From that,
we conclude that $h(x) \in \CC_P$ as needed, and the square above is a pullback.
\end{proof}

From that, it is immediate to deduce that $(\CC_{\tilde{A}}, \CC_{l_A}, \CC_{r_A})$ is an equivalence relation
from the fact that $(\tilde{A}, l_A, r_A)$ is one. We then need to check that $\CC_{l_A}$ and $\CC_{r_A}$ are open maps,
which relies on the following lemma.

\begin{lemma}
Let $\A$ be a tcg, then $\CC_{l_A}$ and $\CC_{r_A}$ are open.
\label{lem:cc_open}
\end{lemma}
\begin{proof}
Let us detail it for $\CC_{l_A}$. First, we note that it is rigid. Indeed, immediate causal links in $\CC_{\tilde{A}}$ have
one of the forms:
\begin{eqnarray*}
(i, \tilde{a}) &\imc& (i, \tilde{a'})\\
(i, \tilde{a}) &\imc& (3-i, \tilde{a})
\end{eqnarray*}
In the first case, we necessarily also have $\tilde{a} \imc \tilde{a'}$ in $\tilde{A}$. Since $l_A$ is rigid, we have
$l_A\,\tilde{a} \imc l_A\,\tilde{a'}$ as well. Therefore $(i, l_A\,\tilde{a}) \imc (i, l_A\,\tilde{a'})$ in $\CC_A$, but
that is by definition $\CC_{l_A}\,(i, l_A\,\tilde{a}) \imc \CC_{l_A}\,(i, l_A\,\tilde{a'})$. In the second case we
have $\CC_{l_A}\,(i, \tilde{a}) = (i, l_A\,\tilde{a}) \imc (3-i, l_A\,\tilde{a}) = \CC_{l_A}\,(3-i, \tilde{a})$ as well
by definition of copycat.

We now prove that $\CC_{l_A}$ has the configuration extension property. A configuration $x\in \conf{\CC_{\tilde{A}}}$ 
corresponds to a diagram \cite{DBLP:conf/lics/RideauW11,WGames}:
\[
\xymatrix{
x_1     \ar@{}[r]|{\supseteq^+}
        \ar@{}[d]|{\rotatebox{270}{$\iso$}_{\theta_1}}
&
x_1\cap x_2
        \ar@{}[r]|{\subseteq^-}
        \ar@{}[d]|{\rotatebox{270}{$\iso$}_{\theta_1 \cap \theta_2}}&
x_2     \ar@{}[d]|{\rotatebox{270}{$\iso$}_{\theta_2}}\\
y_1     \ar@{}[r]|{\supseteq^+}&
y_1\cap y_2
        \ar@{}[r]|{\subseteq^-}&
y_2
}
\]
where the upper side corresponds to $l_A(x)\in \conf{\CC_A}$ and the lower side corresponds to $r_A(x) \in \conf{\CC_A}$. Suppose
now that we have $l_A(x) \longcov{a}$. There are three possible cases.

Suppose first that the upper side of the diagram above extends to:
\[
x_1 \supseteq^+ x_1 \cap x_2 \subseteq^- x_2 \cup \{a\}
\]
with $\pol(a) = -$. By the extension property of isomorphism families, there is an extension $\theta_2 \longcov{(a, a')}$, yielding
an obvious extension of the diagram above, hence an extension of $x$. If the upper side extends to:
\[
x_1 \cup \{a\} \supseteq^+ x_1 \cap x_2 \subseteq^- x_2 
\]
with $\pol(a) = +$, then the situation is symmetric and is dealt with similarly.

If the upper side extends to:
\[
x_1 \supseteq^+ x_1 \cap x_2 \subseteq^- x_2 \cup \{a\}
\]
with $\pol(a) = +$. Then, the situation is a bit more subtle. Indeed in this case, we necessarily have $a\in x_1$, so in the domain of
$\theta_1$. Therefore there is $(a, a') \in \theta_1$ with $a' \in y_1$. So any extension $\theta'_2$ of $\theta_2$ to $a$ must satisfy
$\theta'_2(a) = a'$. This invites us to simply define $\theta'_2 = \theta_2 \cup \{(a, a')\}$, however we have to check that this is
allowed. Suppose this is not. Then, we note that $(x_1 \cap x_2) \cup \{a\} \in \conf{A}$. Indeed $a\in x_1$ and $x_2 \longcov{a}$, so
the dependencies of $a$ are in $x_1 \cap x_2$. So we can restrict $\theta_1$ on the left to it, necessarily yielding the
bijection $(\theta_1 \cap \theta_2) \cup \{(a, a')\}$ which is therefore a valid isomorphism of $A$. So we have two valid extensions
of $\theta_1 \cap \theta_2$:
\[
(\theta_1 \cap \theta_2) \cup \{(a, a')\} \supseteq^+ \theta_1 \cap \theta_2 \subseteq^- \theta_2
\]
If they are compatible, then $\theta \cup \{(a, a')\}$ is a valid isomorphism, providing the required extension of $x$. Otherwise this
is a race. By hypothesis, $l_A$ preserves races, so we have another race:
\[
(x_1 \cap x_2) \cup \{a\} \supseteq^+ x_1 \cap x_2 \subseteq^- x_2
\]
Therefore, $x_2 \cup \{a\} \not \in \conf{A}$, absurd. So, $l_{\CC_A}$ is open. The same reasoning holds for $r_{\CC_A}$.
\end{proof}

With the two lemmas above, we have proved that if $\A$ is a tcg, then $\CC_A$ can
be equipped with a symmetry $(\CC_{\tilde{A}}, \CC_{l_A}, \CC_{r_A})$
making $\CC_A$ an essp.  By definition, we also have $\cc_{\tilde{A}}
: \tilde{\CC_A} \to \tilde{A}^\perp \parallel \tilde{A}$ a
strategy. In order to get a $\sim$-strategy, the last thing to check is
that $\CC_{l_A}$ reflects positive compatibility. But for any esp $A$ positive extensions
of $\CC_A$ are always compatible, so this is trivial. Therefore we have:

\begin{prop}
The triple $(\CC_{\tilde{A}}, \CC_{l_A}, \CC_{r_A})$ is a symmetry and makes $\CC_A$ an essp, written $\CC_\A$.
Moreover,
\[
\cc_{\A} : \CC_\A \to \A^\perp \parallel \A
\]
is a $\sim$-strategy.
\label{prop:cc_thin}
\end{prop}

Here it is crucial that $\A$ is race-preserving, otherwise Lemma \ref{lem:cc_open} fails;
this was initially one of the motivations for the saturated development of \cite{lics14}.

Let us conclude this sub-section with a few technical lemmas on strategies and $\sim$-strategies.

%\begin{lemma}
%Let $\sigma : S \to A$ be a receptive courteous pre-$\sim$-strategy on a game with symmetry $A$,
%then $\tilde{S}$ is race-free as well.
%\label{lem:strat_racefree}
%\end{lemma}
%\begin{proof}
%It is in general the case that for any strategy:
%\[
%\sigma : S \to A
%\]
%if $A$ is race-free, then so is $S$. Indeed suppose there is a race in $S$, \emph{i.e.} $x\in \conf{S}$
%such that $x\longcov{s_1}, x\longcov{s_2}$ but $x\cup \{s_1, s_2\}\not \in \conf{S}$, with $\pol(s_1) =-$ and
%$\pol(s_2) = +$. Then if $\sigma x, \sigma s_1, \sigma s_2$ do not form a race in $A$, by receptivity of $\sigma$ there is 
%a unique $s'_2 \in S$ such that $\sigma s'_2 = \sigma s_2$ and $x\cup \{s_1, s'_2\} \in \conf{S}$. But then
%by courtesy $s'_2$ cannot immediately depend on $s_1$, since $\sigma s_2$ is concurrent with $\sigma s_1$.
%Therefore $x\cup \{s'_2\} \in \conf{S}$ as well. But now there are two distinct $s_2, s'_2$ compactible
%with $x$ and mapping to $\sigma s_2$, absurd by receptivity. So, $S$ is race-free.
%
%Applying this to $\tilde{\sigma} : \tilde{S} \to \tilde{A}$, it follows that $\tilde{S}$ is race-free.
%\end{proof}

\begin{lemma}
Let $\sigma : S \to A$ be a strategy, then for any $x\in \conf{S}$, if
$x \cov{s_1}$ and $x\cov{s_2}$ with $\pol(s_1) = -$ or $\pol(s_2)=-$, and 
$\sigma\,x \cup \{\sigma\,s_1, \sigma\,s_2\} \in \conf{A}$,
then $x\cup \{s_1, s_2\} \in \conf{S}$ as well. In particular, $\sigma$ preserves races.
\label{lem:strat_pres_race}
\end{lemma}
\begin{proof}
Elementary verification, using receptivity and courtesy.
\end{proof}

\begin{lemma}
Let $\sigma : \S \to \A$ be a strong-receptive courteous pre-$\sim$-strategy on a tcg $\A$,
then $\S$ is race-preserving as well.
\label{lem:strat_racepres}
\end{lemma}
\begin{proof}
Suppose $x \stackrel{\theta}{\iso_\S} y$ with two valid extensions $\theta \subseteq^+ \theta_1$
and $\theta \subseteq^- \theta_2$, such that $l_S\,\theta_1$ and $l_S\,\theta_2$ are compatible.
Then $\sigma\,(l_S\,\theta_1) = l_A\,(\sigma\,\theta_1)$ and $\sigma\,(l_S\,\theta_2) = l_A\,(\sigma\,\theta_2)$
are compatible as well. Since $l_A$ preserves races, $\sigma\,\theta_1$ and $\sigma\,\theta_2$ are
compatible. So $\sigma\,\theta_1 \subseteq^- \sigma\,\theta_1 \cup \sigma\,\theta_2$. It follows
by strong-receptivity that there is $\theta_1 \subseteq^- \theta_3$ such that
$\sigma\,\theta_3 = \sigma\,\theta_1 \cup \sigma\,\theta_2$. Finally, by Lemma \ref{lem:strat_racepres}
we have $\theta_3 = \theta_1 \cup \theta_2$ as well.
\end{proof}

\subsection{Interaction of $\sim$-strategies}

We now give the technical background preliminary to the definition of the composition of
$\sim$-strategies.

\subsubsection{Defining pullbacks}

As a first step towards defining the composition of $\sim$-strategies, we now show how to compute their interaction,
formulated as a pullback in $\ESS$. The
key remark here is that despite the general phenomenon that the category of event structures with symmetry does not
have pullbacks (see \cite{DBLP:journals/entcs/Winskel07}), the pullbacks involved in the composition of $\sim$-strategies (really, of
strong-receptive pre-$\sim$-strategies) do exist.
Moreover, if $\sigma : \S \to \A$ and $\tau : \T \to \A^\perp$ are strong-receptive pre-$\sim$-strategies, then
their pullback in $\ESS$ is obtained as the pullback of $\sigma$ and $\tau$
regarded as plain maps of esps, equipped with the symmetry obtained by taking the pullback of $\tilde{\sigma}$ and
$\tilde{\tau}$ regarded also as plain maps of esps, as we show in the following lemma.

\begin{lemma}
Let $\sigma : \S \arrow \A$ and $\tau : \T \arrow \A^{\perp}$ be courteous strong-receptive pre-$\sim$-strategies.
Then, forgetting polarities, the pullback
\[
\xymatrix@R=10pt@C=10pt{
&\S\circledast \T      \ar[dl]
        \ar[dr]
        \pb{270}\\
\S       \ar[dr]_{\sigma}&&
\T       \ar[dl]^{\tau}\\
&\A
}
\]
exists in $\ESS$ and has symmetry; its base event structure is the pullback $S \circledast T$ in $\ES$ and
its symmetry is the pullback $\tilde{S}\circledast \tilde{T}$ in $\ES$, with the obvious projections.
\label{lem:pullbackstrat}
\end{lemma}
\begin{proof}
We first take the pullback in $\ES$:
\[
\xymatrix@R=10pt@C=10pt{
&S\circledast T
	\ar[dl]_{\Pi_1}
        \ar[dr]^{\Pi_2}
        \pb{270}\\
S       \ar[dr]_{\sigma}&&
T       \ar[dl]^{\tau}\\
&A
}
\]
in event structures and maps, which we know always exists. Then we take the pullback:
\[
\xymatrix@R=10pt@C=10pt{
&\tilde{S}\circledast \tilde{T}
	\ar[dl]_{\tilde{\Pi_1}}
        \ar[dr]^{\tilde{\Pi_2}}
        \pb{270}\\
\tilde{S}       \ar[dr]_{\tilde{\sigma}}&&
\tilde{T}       \ar[dl]^{\tilde{\tau}}\\
&\tilde{A}
}
\]
in plain event structures and maps, which always exists as well. Exploiting the universal property of the first pullback, we get maps:
\[
\xymatrix@R=20pt@C=20pt{
&\tilde{S}\circledast \tilde{T}
        \ar@{.>}[d]|{l_{S\circledast T}}
        \ar@/_/[ddl]_{l_S \circ \tilde{\Pi_1}}
        \ar@/^/[ddr]^{l_T \circ \tilde{\Pi_2}}\\
&S\circledast T      \ar[dl]_{\Pi_1}
        \ar[dr]^{\Pi_2}
        \pb{270}\\
S       \ar[dr]_{\sigma}&&
T       \ar[dl]^{\tau}\\
&A
}
~~~~~~~~~~
\xymatrix@R=20pt@C=20pt{
&\tilde{S}\circledast \tilde{T}
        \ar@{.>}[d]|{r_{S\circledast T}}
        \ar@/_/[ddl]_{r_S \circ \tilde{\Pi_1}}
        \ar@/^/[ddr]^{r_T \circ \tilde{\Pi_2}}\\
&S\circledast T     \ar[dl]_{\Pi_1}
        \ar[dr]^{\Pi_2}
        \pb{270}\\
S       \ar[dr]_{\sigma}&&
T       \ar[dl]^{\tau}\\
&A
}
\]
That $(\tilde{S}\circledast \tilde{T}, l_{S\circledast T}, r_{S\circledast T})$ form an equivalence relation on 
$S\circledast T$ follows
from a simple diagram chasing, and so does the fact that $l_{S\circledast T}$ and $r_{S\circledast T}$ are jointly monic.
The key property left is that they are open.

Let us prove rigidity first. Recall that:
\[
\tilde{S}\circledast \tilde{T} = \Pr(\conf{\tilde{S}} \times \conf{\tilde{T}} \restrict R)
\]
where $R = \{(\tilde{s}, \tilde{t})\mid \tilde{\sigma}(\tilde{s}) = \tilde{\tau}(\tilde{t})\}$. Then, suppose that
\[
[(\tilde{s}, \tilde{t})]_{\tilde{x}} \imc [(\tilde{s'}, \tilde{t'})]_{\tilde{x}}
\]
in $\tilde{S}\circledast \tilde{T}$. This means that we also have:
\[
(\tilde{s}, \tilde{t}) \imc_{\tilde{x}} (\tilde{s'}, \tilde{t'})
\]
in $\conf{\tilde{S}} \times \conf{\tilde{T}}$ by definition of $\Pr$
and restriction. It follows by lemma \ref{lem:imc_pullback}
that either $\tilde{s} \imc \tilde{s'}$ in $\tilde{S}$ or $\tilde{t}
\imc \tilde{t'}$ in $\tilde{T}$; the cases being symmetric, let us
suppose \emph{w.l.o.g.} that $\tilde{s} \imc \tilde{s'}$. Since $l_S$
is open thus rigid, writing $s_1 = l_S(\tilde{s})$ and $s'_1 =
l_S(\tilde{s'})$ we have that $s_1 \imc s'_1$ in $S$. It follows that
necessarily, $(s_1, t_1) \imc_{x_1} (s'_1, t'_1)$, where $t_1 =
l_T(\tilde{t})$, $t'_1 = l_T(\tilde{t'})$, and:
\[
x_1 = (l_S \times l_T)~\tilde{x}
\]
(obviously $x_1 \in \conf{S} \times \conf{T}$). By definition of $\Pr$ and restriction, this implies that
$[(s_1, t_1)]_{x_1} \imc [(s'_1, t'_1)]_{x_1}$ in $\Pr(\conf{S} \times \conf{T} \restrict R')$ where $R' = \{(s,t)\mid \sigma(s) = \tau(t)\}$. But
$[(s_1, t_1)]_{x_1} = l_{S\circledast T}([(\tilde{s}, \tilde{t})]_{\tilde{x}})$ and $[(s'_1, t'_1)]_{x_1} = 
l_{S\circledast T}([(\tilde{s'}, \tilde{t'})]_{\tilde{x}})$, therefore
$l_{S\circledast T}$ preserves immediate causality. The same argument applies for $r_{S\circledast T}$ as well, 
therefore $l_{S\circledast T}$ and $r_{S\circledast T}$ are rigid.


It remains to prove that $l_{S\circledast T}, r_{S\circledast T}$ have the configuration extension property; let us prove it w.l.o.g. for $l_{S\circledast T}$. Let
$z\in \conf{\tilde{S}\circledast \tilde{T}}$. By Proposition \ref{prop:secured}, this corresponds to a secured bijection:
\[
\phi : \theta_1 \iso \tilde{\sigma}~\theta_1 = \tilde{\tau}~\theta_2 \iso \theta_2
\]
where $x_l \stackrel{\theta_1}{\iso_S} x_r$ and $y_l \stackrel{\theta_2}{\iso_T} y_r$. Then, $l_{S\circledast T}$ maps this secured bijection to:
\[
\phi_l : x_l \iso \sigma~x_l = \tau~y_l \iso y_l
\]
where $\phi_l \circ l_S = l_T \circ \phi$. Suppose now that $\phi_l$ extends to:
\[
\phi_l\cup \{(s_l, t_l)\} : x_l\cup \{s_l\} \iso (\sigma~x_l)\cup \sigma~s = (\tau~y_l)\cup \tau~t_l \iso y_l \cup \{t_l\}
\]
The events $s_l$ and $t_l$ must have complementary polarities in $S$ and $T$, so one of them is negative -- suppose w.l.o.g. that
it is $s_l$. That means that $t_l$ is positive. By the extension property of isomorphism families (or alternatively, since
$l_T$ is open), there is $t_r\in T$ such that $y_l \cup \{t_l\} \stackrel{\theta_2\cup \{(t_l, t_r)\}}{\iso_T} 
y_r \cup \{t_r\}$. So by receptivity of $\tilde{\sigma}$, there is a corresponding extension of
$x_l \stackrel{\theta_1}{\iso_S} x_r$ to
$x_l \cup \{s_l\} \stackrel{\theta_2\cup \{(s_l, s_r)\}}{\iso_S} x_r \cup \{s_r\}$ such that $\sigma~s_l = \tau~t_l$
and $\sigma~s_r = \tau~t_r$. Moreover 
\[
\theta_1 \cup \{(s_l, s_r)\} \iso \tilde{\sigma}~\theta_1 \cup \{(\sigma~s_l, \sigma~s_r)\} =
\tilde{\tau}~\theta_2 \cup \{(\tau~t_l, \tau~t_r)\} \iso \theta_2 \cup \{(t_l, t_r)\}
\]
which is still a secured bijection by construction, so we have proved the configuration extension property.
\end{proof}

With this definition, composition of $\sim$-strategies can be defined as in \cite{DBLP:conf/lics/RideauW11} through the
pullback construction followed by projection. We leave the details for later because we still have one
key difficulty to overcome: the fact that weak equivalence is preserved by composition.

\subsubsection{Pullbacks as bipullbacks}

We now get to the bigger obstacle to the definition of thin concurrent
games. 

In \cite{DBLP:conf/lics/RideauW11}, preservation of isomorphism by composition follows from the universal
property of the pullback. However, here for $\sim$-strategies $\sigma : \S \to \A$ and $\tau : \T \to \A$, we
have defined their weak equivalence through the existence of certain maps
$f : \S \to \T$ and $g : \T \to \S$ with respect to which the projections
to the game commutes \emph{up to symmetry}. But nothing, in the universal
property of the pullback, ensures that it is compatible with this notion
of equivalence.

For that, we prove that the pullback of $\sim$-strategies also satisfies the
universal property up to symmetry of \emph{bipullbacks} -- which corresponds
to a pullback in the quotient category.

\begin{definition}
  A bipullback of two maps $f : \A {\rightarrow} \C$ and $g : \B {\rightarrow} \C$ of ess is
  an object $\mathcal{P}$ and two maps ${\Pi}_1 : \mathcal P {\rightarrow} \A$ and ${\Pi}_2 : \mathcal P {\rightarrow} \B$ such
  that $f\circ {\Pi}_1 \sim g \circ {\Pi}_2$ and for all maps $x: \X {\rightarrow} \A$ and $y : \X
  {\rightarrow} \B$ such that $f\circ x \sim g\circ y$, there exists a map of ess $h : \X
  {\rightarrow} \mathcal P$ unique up to symmetry such that ${\Pi}_1\circ h \sim f$ and $\Pi_2 \circ h \sim g$.
\end{definition}

\begin{prop}
  Suppose $\sigma : \S \arrow \A$ and $\tau : \T \arrow \A^{\perp}$
  are strong-receptive courteous pre-$\sim$-strategies with receptive thin sub-symmetries. Then, forgetting polarities,
  the pullback of $\sigma$ and $\tau$ in $\ESS$ is also a bipullback.
\label{prop:pullbi}
\end{prop}
\begin{proof}
Suppose we have $f: \R \arrow \S$ and $g : \R \arrow \T$ such that the square commutes up to equivalence, \emph{i.e.} for any $z\in \conf{R}$
there is an isomorphism $\sigma f z \stackrel{\phi_z}{\iso_A} \tau g z$.

Suppose we have a chain:
\[
\emptyset = z_0 ~ \cov ~ z_1 ~ \cov ~ z_2 ~ \cov ~ \dots ~ \cov ~ z_n
\]
of configurations of $R$. For each $i \leq n$, we will build a diagram of the shape:
\[
\xymatrix{
f(z_i)  \ar@{}[r]^{\theta^S_i}|{\iso_S}
        \ar@{|->}[d]_{\sigma}&
x_i     \ar@{|->}[dr]_{\sigma}&&
y_i     \ar@{|->}[dl]^{\tau}
        \ar@{}[r]^{\theta^T_i}|{\iso_T}&
g(z_i)  \ar@{|->}[d]^{\tau}\\
\sigma(f(z_i))  \ar@{}[rr]^{\sigma \theta^S_i}|{\iso_A}&&
v_i     \ar@{}[rr]^{\tau \theta^T_i}|{\iso_A}&&
\tau(g(z_i))
}
\]
such that $\tau \theta^T_i \circ \sigma \theta^S_i = \phi_{z_i}$, and where $\theta^S_i$ and $\theta^T_i$ are respectively
in the receptive thin sub-symmetries $\tilde{S}_+$ and $\tilde{T}_+$. This is done by induction on $i$.

For $i=0$, this diagram is built by setting all components to $\emptyset$. Suppose now the diagram constructed for $i$, and
take $z_i \longcov{r} z_{i+1}$. Necessarily, either $\pol(f(r)) = +$ or $\pol(g(r)) = +$. Suppose \emph{w.l.o.g.} that it is the former,
the other case will be symmetric. We write $f(r) = s_1$, and we set:
\[
\theta^S_{i+1} = \ext(\theta^S_i, f(z_i)\cup \{s_1\})
\]
We write $\theta^S_{i+1} = \theta^S_{i} \cup \{(s_1, s_2)\}$. Likewise, we write that $\phi z_i \longcov{(\sigma s_1, a)} \phi z_{i+1}$.
Then by hypothesis, we have:
\[
\tau \theta^T_{i} \longcov{(\sigma s_2, a)}
\]
Moreover, $\pol_{A^\perp}(\sigma t) = \pol_{A^\perp}(a) = -$, therefore by strong-receptivity there are unique $t_1, t_2 \in T$ such that
$\tau t_1 = \sigma s_2$ and $\tau t_2 = a$, and:
\[
\theta^T_i ~~ \longcov{(t_1, t_2)}
\]
We set $\theta^T_{i+1} = \theta^T_i \cup \{(t_1, t_2)\}$, yielding a valid extension of the diagram for $i+1$.
By induction, the diagram is well-defined for any $n\in \mathbb{N}$.


Now, we want to show that the diagram obtained for $n$ does not depend on the particular chain $z_0 ~ \cov ~ \dots ~ \cov ~ z_n$ but only on $z_i$. This is
done by showing that this construction is invariant under permutations of independent events in the chain $(z_i)$.
Suppose $z_i \longcov{r} z_{i+1}$ and $z_{i+1} \longcov{r'} z_{i+2}$ where $r$ and $r'$ are concurrent. It follows that there is another chain:
\[
\emptyset = z'_0 ~ \cov ~ z'_1 ~ \cov ~ \dots ~ \cov ~ z'_n
\]
defined by $z'_j = z_j$ for all $j\leq i$, $z'_{i+1} = z_{i}\cup \{r'\}$, and $z'_j = z_j$ for all $j\geq i+2$.

We perform the construction described above on $(z_i)$ and $(z'_i)$, and compare the results. The components of the diagrams obtained by applying
the construction to $(z_j)_{0\leq j \leq n}$ will be called $x_j, y_j, v_j, \theta^S_j, \theta^T_j$ and the components of the diagrams obtained by
applying the construction to $(z'_j)_{0 \leq j \leq n}$ will be called $x'_j, y'_j, v'_j, {\theta'}^S_j, {\theta'}^T_j$. By construction, it is obvious
that these diagrams coincide for $j\leq i$. We will now compare them for $i+2$.



There are two independent cases: permutation of two events yielding events in $A$ of the same polarity, and permutation of two events yielding events
in $A$ of opposite polarity. We start by the former. Without loss of generality, suppose $\pol(\sigma (f r)) = \pol(\sigma (fr')) = +$
and write $f\,r = s$ and $f\,r' = s'$. Since $r$ and $r'$ are concurrent, it follows that $s$ and $s'$ are concurrent as well. We have:
\begin{eqnarray*}
\theta^S_{i+2} &=& \ext(\ext(\theta^S_i, f(z_i) \cup \{s\}), f(z_i) \cup \{s, s'\})\\
{\theta'}^S_{i+2} &=& \ext(\ext({\theta'}^S_i, f(z_i) \cup \{s'\}), f(z_i) \cup \{s', s\})
\end{eqnarray*}
but we know that $\theta^S_i = {\theta'}^S_i$, so they are both equal to $\ext(\theta^S_i, f(z_i) \cup \{s, s'\})$ by monotonicity. By uniqueness of
receptivity, we also have that $\theta^T_{i+2} = {\theta'}^T_{i+2}$, so the two diagrams coincide at $i+2$. 
%Since the construction only depends on
%the previous step, it is obvious that this equality extends up to $n$. 
Note that it also follows from this reasoning (and we will use it later) that:
\begin{eqnarray*}
\theta^S_{i+2} &=& \theta^S_{i+1} \cup {\theta'}^S_{i+1}\\
\theta^T_{i+2} &=& \theta^T_{i+1} \cup {\theta'}^T_{i+1}
\end{eqnarray*}
Clearly $\theta^S_{i+1} = \ext(\theta^S_i, f(z_i) \cup \{s\}) \subseteq \theta^S_{i+2}$ and the same holds for ${\theta'}^S_{i+1}$ therefore
we have the inclusion $\theta^S_{i+1} \cup {\theta'}^S_{i+1} \subseteq \theta^S_{i+2}$, the equality follows because these two isomorphisms
have the same domain and codomain. The second equality follows by uniqueness of receptivity.


Now suppose that $r$ and $r'$ yield events in $A$ of opposite polarity. Suppose \emph{w.l.o.g.} that $\pol(\sigma (f r)) = +$ and $\pol(\sigma (f r'))
 = -$. We write $f(r) = s_1$ and $g(r) = t_2$, $f(r') = s'_1$ and $g(r') = t'_2$. We display the diagram obtained for $z_{i+1}$:
\[
\xymatrix@C=15pt{
f(z_i)\cup\{s_1\}                       \ar@{}[r]^{\theta^S_{i+1}}|{\iso_S}
                                        \ar@{|->}[d]_{\sigma}&
x_i\cup \{s_2\}                         \ar@{|->}[dr]_{\sigma}&&
y_i\cup \{t_1\}                         \ar@{|->}[dl]^{\tau}
                                        \ar@{}[r]^{\theta^T_{i+1}}|{\iso_T}&
g(z_i)\cup\{t_2\}                       \ar@{|->}[d]^{\tau}\\
\sigma(f(z_i))\cup\{\sigma s_1\}        \ar@{}[rr]^{\sigma \theta^S_{i+1}}|{\iso_A}&&
v_i\cup \{\sigma s_2\}                  \ar@{}[rr]^{\tau \theta^T_{i+1}}|{\iso_A}&&
\tau(g(z_i))\cup \{\tau t_2\}
}
\]
Where $s_2$ and $\theta^S_{i+1}$ are obtained from $s_1$ by coherent extension of $\theta^S_i$, $\tau t_1$ is 
fixed to be $\sigma\,s_2$ from which $t_1$ follows uniquely by receptivity,
and $\theta^T_{i+1} = \theta^T_i \cup \{(t_1, t_2)\}$ is valid by strong-receptivity.

Likewise, the diagram for $z'_{i+1}$ is:
\[
\xymatrix@C=15pt{
f(z_i)\cup\{s'_1\}                      \ar@{}[r]^{{\theta'}^S_{i+1}}|{\iso_S}
                                        \ar@{|->}[d]_{\sigma}&
x_i\cup \{s'_2\}                        \ar@{|->}[dr]_{\sigma}&&
y_i\cup \{t'_1\}                        \ar@{|->}[dl]^{\tau}
                                        \ar@{}[r]^{{\theta'}^T_{i+1}}|{\iso_T}&
g(z_i)\cup\{t'_2\}                      \ar@{|->}[d]^{\tau}\\
\sigma(f(z_i))\cup\{\sigma s'_1\}       \ar@{}[rr]^{\sigma {\theta'}^S_{i+1}}|{\iso_A}&&
v_i\cup \{\sigma s'_2\}                 \ar@{}[rr]^{\tau {\theta'}^T_{i+1}}|{\iso_A}&&
\tau(g(z_i))\cup \{\tau t'_2\}
}
\]
We now show that the diagram obtained for $z_{i+2}$ is the (component-wise) union of those two.

We know by the diagram obtained for $z'_{i+1}$ that $\ext((\theta^T_i)^{-1}, g(z_i) \cup \{t'_2\}) = (\theta^T_i)^{-1} \cup \{(t'_2, t'_1)\}$.
Moreover, we know that $g(z_i) \cup \{t_2, t'_2\} \in \conf{S}$ since $r$ and $r'$ are concurrent. Moreover $\pol(t_2) \neq \pol(t'_2)$, so since by Lemma \ref{lem:strat_racepres} (using that $\A$, as a tcg, is race-preserving) $\T$ is race-preserving
it follows that $(\theta^T_i)^{-1} \cup \{(t_2, t_1), (t'_2, t'_1)\}$ is in
the isomorphism family of $T$. Therefore by the stability axiom of coherent extensions, it follows that
\[
\ext((\theta^T_{i})^{-1}, g(z_i) \cup \{t'_2\}) \subseteq \ext((\theta^T_{i})^{-1}\cup \{(t_2, t_1)\}, g(z_i) \cup \{t_2, t'_2\})
\]
or, in other words:
\[
(\theta^T_i)^{-1} \cup \{(t'_2, t'_1)\} \subseteq \ext((\theta^T_{i+1})^{-1}, g(z_i) \cup \{t_2, t'_2\})
\]
which implies $(t'_2, t'_1) \in \ext((\theta^T_{i+1})^{-1}, g(z_i) \cup \{t_2, t'_2\})$. We also have $(t_2, t_1) \in \ext((\theta^T_{i+1})^{-1}, g(z_i)
\cup \{t_2, t'_2\})$ since $(t_2, t_1) \in (\theta^T_{i+1})^{-1}$, so it immediately follows that $\theta^T_{i+2} = \theta^T_{i+1} \cup {\theta'}^T_{i+1}$. The reasoning for $\theta^S_{i+2} = \theta^S_{i+1} \cup {\theta'}^S_{i+1}$ is symmetric.


We have proved that the construction of this diagram is invariant under permutation of concurrent events,
so the diagram for a chain
$z_0 ~ \cov ~ \dots ~ \cov ~ z_n$ only depends on $z_n$ and is independent of the particular chain used to reach it. So we have a construction which to
any configuration $z\in \conf{R}$ associates a diagram:
\[
\xymatrix{
f(z)  \ar@{}[r]|{\iso_{\theta^S_z}}
        \ar@{|->}[d]_{\sigma}&
x_z     \ar@{|->}[dr]_{\sigma}&&
y_z     \ar@{|->}[dl]^{\tau}
        \ar@{}[r]|{\iso_{\theta^T_z}}&
g(z)  \ar@{|->}[d]^{\tau}\\
\sigma(f(z))  \ar@{}[rr]|{\iso_{\sigma \theta^S_z}}&&
v_z     \ar@{}[rr]|{\iso_{\tau \theta^T_z}}&&
\tau(g(z))
}
\]


Now, we define the following functions:
\[
\begin{array}{rcccl}
f'&:&\conf{R}   &\arrow&\conf{S}\\
 & &z           &\mapsto& x_z
\end{array}
~~~~~~~~
\begin{array}{rcccl}
g'&:&\conf{R}   &\arrow&\conf{T}\\
 & &z           &\mapsto& y_z
\end{array}
\]
~~~~~~~~
\[
\begin{array}{rcccl}
h'_1&:&\conf{R} &\arrow&\conf{\tilde{S}}\\
    & &z        &\mapsto&\theta^S_z
\end{array}
~~~~~~~~
\begin{array}{rcccl}
h'_2&:&\conf{R} &\arrow&\conf{\tilde{T}}\\
    & &z        &\mapsto&\theta^T_z
\end{array}
\]
By definition, it is obvious that these functions preserve $\cov$. Additionally they preserve bounded union. Indeed,
take any of the functions $f: \conf{R} \to \conf{E}$ defined above.
We have seen during the construction of the functions above that for any diagram:
\[
\xymatrix@R=5pt@C=5pt{
&z\\
y\ar[ur]
&&y'\ar[ul]\\
&x\ar[ul]\ar[ur]
}
\]
in $\conf{R}$, we have $f(z) = f(y) \cup f(y')$. Now suppose $x, y\in \conf{R}$ are compatible. Pick a chain
\[
\emptyset = x_0 ~ \longcov{a_1} ~ \dots ~ \longcov{a_n} x_n = x
\]
and similarly, a chain:
\[
\emptyset = y_0 ~ \longcov{b_1} ~ \dots ~ \longcov{b_n} y_p = y
\]
We have the following lattice of sub-configurations of $x \cup y$ whose order preserve the chains $(x_i)_{0\leq i \leq n}$
and $(y_i)_{0\leq i \leq p}$:
\[
\xymatrix@R=5pt@C=5pt{
&&&~\\
&&~\ar[ur]^{b_p}&&~\ar[ul]_{a_n}\\
&~\ar@{.}[ur]&&&&~\ar@{.}[ul]\\
~\ar[ur]^{b_1}&&&&&&~\ar[ul]_{a_1}\\
&~\ar[ul]^{a_n}&&&&~\ar[ur]_{b_p}\\
&&~\ar@{.}[ul]&&~\ar@{.}[ur]\\
&&&~\ar[ul]^{a_1}\ar[ur]_{b_1}
}
\]
By induction on this diagram using the union property mentioned above, we have that $f(x\cup y) = f(x) \cup f(y)$. Therefore
by Lemma \ref{lem:mapification}, there are unique maps of event structures $\hat{f'} : R \to S$, $\hat{g'} : R \to G$,
$\hat{h'_1} : R \to \tilde{S}$ and $\hat{h'_2} : R \to \tilde{S}$. By the uniqueness property of the map construction, the
hat construction preserves commuting diagrams. It follows that the following diagram (in $\ES$) commutes:

\[
\xymatrix{
&&&R
        \ar@/_2.5pc/[ddlll]_{f}
        \ar@/_/[dll]_{\hat{h'_1}}
        \ar@/_/[ddl]_{\hat{f'}}
        \ar@{.>}[d]|{\langle \hat{f'}, \hat{g'} \rangle}
        \ar@/^/[ddr]^{\hat{g'}}
        \ar@/^/[drr]^{\hat{h'_2}}
        \ar@/^2.5pc/[ddrrr]^{g}\\
&\tilde{S}
        \ar[dl]^{l_S}
        \ar[dr]_{r_S}
&&S\circledast T     \pb{270}
        \ar[dl]^{\Pi_1}
        \ar[dr]_{\Pi_2}
&&\tilde{T}
        \ar[dl]^{l_T}
        \ar[dr]_{r_T}\\
S&&S    \ar[dr]_{\sigma}
&&T     \ar[dl]^{\tau}
&&T\\
&&&A
}
\]
which exactly means that $\tuple{\hat{f'}, \hat{g'}}$ is the required mediating arrow making the two triangles of the pullback diagram commute
up to symmetry. Of course for now $h = \tuple{\hat{f'}, \hat{g'}}$ is just a map of event structures and not of event structures with
symmetry, so we need to define
$\tilde{h} : \tilde{R} \to \tilde{S}\circledast \tilde{T}$. Note that by Lemmas \ref{lem:lifting} and \ref{lem:liftingce}, all the components lift to symmetries,
so the same construction can be carried out on the diagram below, where all components have been replaced with their symmetry.
\[
\xymatrix{
&&&\tilde{R}
        \ar@/_2.5pc/[ddlll]_{\tilde{f}}
        \ar@/_/[dll]_{\hat{\tilde{h'_1}}}
        \ar@/_/[ddl]_{\hat{\tilde{f'}}}
%        \ar@{.>}[d]|{\langle \hat{\tilde{f'}}, \hat{\tilde{g'}} \rangle}
        \ar@/^/[ddr]^{\hat{\tilde{g'}}}
        \ar@/^/[drr]^{\hat{\tilde{h'_2}}}
        \ar@/^2.5pc/[ddrrr]^{\tilde{g}}\\
&\tilde{\tilde{S}}
        \ar[dl]^{l_{\tilde{S}}}
        \ar[dr]_{r_{\tilde{S}}}
&&\tilde{S}\circledast \tilde{T}     \pb{270}
        \ar[dl]^{\tilde{\Pi_1}}
        \ar[dr]_{\tilde{\Pi_2}}
&&\tilde{\tilde{T}}
        \ar[dl]^{l_{\tilde{T}}}
        \ar[dr]_{r_{\tilde{T}}}\\
S&&\tilde{S}    \ar[dr]_{\tilde{\sigma}}
&&\tilde{T}     \ar[dl]^{\tilde{\tau}}
&&\tilde{T}\\
&&&\tilde{A}
}
\]
The same process as before can be applied on this diagram, yielding $\langle \hat{\tilde{f'}}, \hat{\tilde{g'}} \rangle : \tilde{R} \to \tilde{S}\circledast \tilde{T}$.

Furthermore, this diagram projects to the previous one in two distinct ways: (1) by mapping each $\tilde{E}$ to $E$ via $l_E$, and each $\tilde{\tilde{E}}$
to $\tilde{E}$ via $u_{\tilde{E}}$, and (2) by mapping each $\tilde{E}$ to $E$ via $r_E$, and each $\tilde{\tilde{E}}$ to $\tilde{E}$ via $d_{\tilde{E}}$.
By Lemmas \ref{lem:lifting} and \ref{lem:liftingce} all the constructions used to build $\langle \hat{\tilde{f'}}, \hat{\tilde{g'}} \rangle :
\tilde{R} \to \tilde{S}\circledast \tilde{T}$ all commute with these projections. It follows that
\begin{eqnarray*}
l_{S\circledast T} \circ \langle \hat{\tilde{f'}}, \hat{\tilde{g'}} \rangle : \tilde{R} \to \tilde{S}\circledast \tilde{T} &=& \langle \hat{f'}, \hat{g'} \rangle \circ l_R\\
r_{S\circledast T} \circ \langle \hat{\tilde{f'}}, \hat{\tilde{g'}} \rangle : \tilde{R} \to \tilde{S}\circledast \tilde{T} &=& \langle \hat{f'}, \hat{g'} \rangle \circ r_R\\
\end{eqnarray*}
So $\langle \hat{f'}, \hat{g'} \rangle$ preserves symmetry as needed.


It remains to prove that the mediating arrow is unique up to symmetry. Suppose there are two mediating arrows:
\[
\xymatrix{
&R      \ar@/_/[ddl]_f
        \ar@/^/[ddr]^g
        \ar@{}[ddl]|{~~\sim}
        \ar@{}[ddr]|{\sim~~}
        \ar@{.>}[d]|{k, k'}\\
&S\circledast T      \ar[dl]^{\Pi_1}
        \ar[dr]_{\Pi_2}
        \pb{270}\\
S       \ar[dr]_{\sigma}&&
T       \ar[dl]^{\tau}\\
&A
}
\]
Then we know that for all $z\in \conf{R}$, $\theta_z = \{(f(r), \Pi_1\circ k(r))\mid r\in z\}$ and $\theta'_z = 
\{(f(r), \Pi_1\circ k'(r))\mid r\in z\}$ are in the isomorphism family of $S$. It follows that for all $z\in \conf{R}$,
the isomorphism
\[
\psi_z = \{(\Pi_1\circ k(r), \Pi_1\circ k'(r))\mid r\in z\}
\]
 is in the isomorphism family of $S$ as well, since
it is obtained by composition of $\theta_z$ and $\theta'_z$. So there is a map:
\[
\psi : R \arrow \tilde{S}
\]
such that $l_S \circ \psi = \Pi_1 \circ k$ and $r_S \circ \psi = \Pi_1 \circ k'$. By the same reasoning
there is a map $\psi' : R \arrow \tilde{T}$ such that $l_T \circ \psi' = \Pi_2 \circ k$ and $r_T \circ \psi' = \Pi_2 \circ k'$. Moreover,
we have $\tilde{\sigma} \circ \psi = \tilde{\tau} \circ \psi'$: this obviously holds once post-composed by $l_A$ and $r_A$, so
this equation follows by joint monicity. By the universal property of $\tilde{S}\circledast \tilde{T}$, there is a unique map $h:S \to \tilde{S}\circledast \tilde{T}$ such that
$\tilde{\Pi_1} \circ h = \psi$ and $\tilde{\Pi_2} \circ h = \psi'$. By post-composing with the left and right maps we get:
\begin{eqnarray*}
\Pi_1 \circ l_{S\circledast T} \circ h &=& \Pi_1 \circ k\\
\Pi_1 \circ r_{S\circledast T} \circ h &=& \Pi_1 \circ k'\\
\Pi_2 \circ l_{S\circledast T} \circ h &=& \Pi_2 \circ k\\
\Pi_2 \circ r_{S\circledast T} \circ h &=& \Pi_2 \circ k'
\end{eqnarray*}
It follows from the universal property of the pullback for $S\circledast T$ that $l_{S\circledast T} \circ h = k$ and 
$r_{S\circledast T} \circ h = k'$, so $k \sim k'$ as needed.
\end{proof}



\subsection{Composition of $\sim$-strategies}
We now proceed to define the composition of $\sim$-strategies. Given
two $\sim$-strategies $\sigma : \S \to \A^\perp \parallel \B$ and
$\tau : \T \to \B^\perp \parallel \C$, we compose them as
before by first (forgetting polarities) taking the pullback
$(\S\parallel \C) \circledast (\A\parallel \T)$, which exists by
Lemma \ref{lem:pullbackstrat} and has symmetry $(\tilde{S} \parallel
\tilde{C})\circledast (\tilde{A} \parallel \tilde{T})$. Then, we
define:
\[
V = \{p\in (S\parallel C) \circledast (A\parallel T) \mid (\sigma \parallel C)\circ\Pi_1~p \not \in B\}
\]
This set of events is closed under symmetry (see Definition \ref{def:closed_symm}), as it is the left projection of $\tilde{V}$
defined similarly on $(\tilde{S}\parallel \tilde{C}) \circledast (\tilde{A}\parallel \tilde{T})$. So by Proposition
\ref{prop:proj_symm} there is an event structure with symmetry:
\[
\T\odot \S = (\S\parallel \C) \circledast (\A\parallel \T) \proj V
\]
Note that by definition, this is exactly the same as the composition $T \odot S$ of $\sigma : S \to A^\perp \parallel B$ and 
$\tau : T \to B^\perp \parallel C$ regarded as strategies without symmetry, equipped with the symmetry $\tilde{T} \odot \tilde{S}$
obtained as the composition of $\tilde \sigma : \tilde{S} \to \tilde{A}^\perp \parallel \tilde{B}$ and $\tilde{\tau} : \tilde{T} \to
\tilde{B}^\perp \parallel \tilde{C}$ regarded as well as strategies without symmetry. In other words, we have the following
equality:
\begin{eqnarray*}
\widetilde{T\odot S} &=& \tilde{T} \odot \tilde{S}
\end{eqnarray*}
between esps, which reflects the earlier $\tilde{\CC_A} = \CC_{\tilde{A}}$. Interestingly, it can be checked that
the equality above also holds when $\tilde{T}, \tilde{S}$ and $\widetilde{T\odot S}$ are regarded as event structures
with symmetry equipped with the free higher symmetry (see Subsection \ref{sec:highsymm}).

Since in particular composition following this definition is compatible with usual composition without symmetry,
it follows that the composition of $\sim$-strategies is a strong-receptive courteous pre-$\sim$-strategy; we check
below that it is thin as well and hence is a $\sim$-strategy.

\begin{lemma}
Let $\sigma : \S \to \A^\perp \parallel \B$ and $\tau : \T \to \B^\perp \parallel \C$ be $\sim$-strategies, then
$\tau \odot \sigma : \T\odot \S \to \A^\perp \parallel \C$ is a $\sim$-strategy.
\end{lemma}
\begin{proof}
We only have to check that $\tau\odot \sigma$ is thin, \emph{i.e.} that $l_{T\odot S}$ reflects
positive compatibility. Take a configuration of $\tilde{T}\odot \tilde{S}$ (so also 
a configuration of $(\tilde{S}\parallel \tilde{C})\circledast (\tilde{A} \parallel \tilde{T})$)
represented as a commuting diagram:
\[
\xymatrix@R=20pt@C=20pt{
x_1	\ar@{}[r]|{\iso}^{\sigma}
	\ar@{}[d]|{\theta_1 \rotatebox{90}{$\iso$}_{\S\parallel \C}}&
\sigma\,x_1
	\ar@{}[r]|{=}&
\tau\,y_1
	\ar@{}[r]|{\iso}^{\tau}&
y_1	\ar@{}[d]|{\theta'_1 \rotatebox{90}{$\iso$}_{\A\parallel \T}}\\
x'_1	\ar@{}[r]|{\iso}^{\sigma}&
\sigma\,x'_1
	\ar@{}[r]|{=}&
\tau\,y'_1
	\ar@{}[r]|{\iso}^{\tau}&
y'_1
}
\]
Suppose that, as a configuration of $\tilde{T}\odot \tilde{S}$, it extends positively to
two other versions of this diagram, with components labeled $2$ and $3$ respectively, such 
that the left projections ($x_2, y_2$ and $x_3, y_3$) are compatible. Regarded as configurations of
$(\tilde{S} \parallel \tilde{C}) \circledast (\tilde{A} \parallel \tilde{A})$, these extensions
are not necessarily positive; however the new visible events have positive polarity in $A^\perp \parallel C$.
For simplicity suppose the extensions to $x_2, y_2$ and $x_3, y_3$ to be atomic, the general case
will follow by immediate induction. If the extensions of $x_1$ to $x_2, x_3$ have different polarities,
then the extensions of $\theta_1$ to $\theta_2, \theta_3$ and of $\theta'_1$ to $\theta'_2, \theta'_3$
are compatible as well by race-preservation of $\S\parallel \C^\perp$ and $\A \parallel \T$ (which
follows from Lemma \ref{lem:strat_racepres}). If
the extensions of $x_1$ to $x_2, x_3$ are both positive, then they cannot both be in $\C^\perp$ as
that would contradict the fact that new visible events have positive polarity. If they
are both in $\S$, then the extensions of $\theta_1$ to $\theta_2, \theta_3$ are compatible since $\S$
is thin, and the extensions of $\theta'_1$ to $\theta'_2, \theta'_3$ are compatible by Lemma \ref{lem:strat_pres_race}
since $\A\parallel \tau$ is courteous and strong-receptive. If one (say $x_2$) is in $\S$ and the other (say
$x_3$) is in $\C$, then $\theta_2$ and $\theta_3$ are compatible by definition of $\parallel$, and 
$\theta'_2$ and $\theta'_3$ are compatible by Lemma \ref{lem:strat_pres_race} since $\A\parallel \tau$
is strong-receptive and courteous.
\end{proof}

So, from the results of \cite{DBLP:conf/lics/RideauW11} we know that tcgs and $\sim$-strategies up to isomorphism form a bicategory.
However, as argued before, for this setting of strategies up to symmetry to make sense, we need
to check that weak equivalence is preserved by composition. In proving so we will use crucially Proposition \ref{prop:pullbi}.
Note that Proposition \ref{prop:pullbi} was proved for pullbacks of the form $\sigma : \S \to \A$ and $\tau : \T \to
\A^\perp$ where both $\sigma$ and $\tau$ admit receptive thin
sub-symmetries -- this is the case for the composition pullback, since
concurrent games with symmetry were assumed to have receptive
thin sub-symmetries.

\begin{lemma}
Let $\sigma : \S \to \A^\perp \parallel \B$, $\sigma' : \S' \to \A^\perp \parallel \B$ with $\sigma \simeq \sigma'$ and
$\tau : \T \to \B^\perp \parallel \C$, $\tau' : \T' \to \B^\perp \parallel \C$ with $\tau \simeq \tau'$. Then:
\[
\tau \odot \sigma \simeq \tau' \odot \sigma'
\]
\label{lem:we_congruence}
\end{lemma}
\begin{proof}
We show that if $\sigma \simeq \sigma'$ then $\tau \odot \sigma \simeq \tau \odot \sigma'$, the general case easily follows
from that. Let us write $P = (\S\parallel \C)\circledast (\A\parallel \T)$ and $P' = (\S'\parallel \C)\circledast (\A\parallel \T)$
the two composition pullbacks. By definition of weak equivalence, there are maps $f : \S \to \S'$ and $g: \S' \to \S$ such that
$\sigma' \circ f \sim \sigma$, $\sigma \circ g \sim \sigma'$, $f\circ g \sim \id_{\S'}$ and $g\circ f \sim \id_\S$.
Therefore, forgetting polarities, the following square commutes up to symmetry:
\[
\xymatrix@R=10pt@C=10pt{
&\P'
	\ar[dl]_{(f\parallel C)\circ \Pi'_1}
	\ar[dr]^{\Pi'_2}
	\ar@{}[dd]|{\sim}\\
\S'\parallel \C
	\ar[dr]^{\sigma'\parallel \C}&&
\A\parallel \T
	\ar[dl]^{\A\parallel \tau}\\
&\A\parallel \B \parallel \C
}
\]
But besides being a pullback, $\P$ is a bipullback by Proposition \ref{prop:pullbi}. Indeed, although the 
courteous strong-receptive pre-$\sim$-strategy 
$\sigma \parallel \C^\perp : \S \parallel \C^\perp \to \A^\perp \parallel \B \parallel \C^\perp$ is not thin (because
$\id_\A : \A \to \A$ is not thin in general), its symmetry has a receptive thin sub-symmetry 
$\tilde{S} \parallel \tilde{C}_-$, and likewise
%$A\parallel \tau : A \parallel T \to A \parallel B^\perp \parallel C$ 
$\tilde{A} \parallel \tilde{T}$ has a receptive thin sub-symmetry $\tilde{A}_+\parallel \tilde{T}$.

From there it is immediate to apply the universal property of bipullbacks to obtain $f' : \P \to \P'$ and
$g': \P' \to \P$ satisfying the required commutations up to symmetry, and the weak equivalence between
the two compositions follow by restriction.
\end{proof}

We have defined a structure $\CGS$, with:
\begin{itemize}
\item Objects: concurrent games with symmetry,
\item Morphisms from $\A$ to $\B$: $\sim$-strategies $\sigma : \S \to \A^\perp \parallel \B$, with 
an identity $\sim$-strategy $\cc_\A : \CC_\A \to \A^\perp \parallel \A$,
\item $2$-cells: weak equivalences.
\end{itemize}

For $\sigma : \S \to \A^\perp \parallel \B$ a morphism in $\CGS$, we will sometimes write $\sigma : \A \cgsto \B$.

Since our construction extends \cite{DBLP:conf/lics/RideauW11} conservatively, we get that copycat is neutral with respect to composition
up to isomorphism, hence up to weak equivalence. In fact the compositional structure is completely similar to \cite{DBLP:conf/lics/RideauW11}.
except that our composition is performed by an universal property up to $\sim$ rather than strict. For the same
reasons as in \cite{DBLP:conf/lics/RideauW11}, it follows that the laws of a bicategory are satisfied up to symmetry; we call that
a $\sim$-bicategory. In fact as in \cite{DBLP:conf/lics/RideauW11,lics14} we also have:

\subsection{Compact closed structure}

We show that $\CGS$ satisfies the laws of a compact closed category up to $\simeq$.

\paragraph{Bifunctor.} We first remark that parallel composition $\parallel$ on cgs extends to a functor:
\[
\parallel_s : \CGS/\!\!\simeq \times \CGS/\!\!\simeq \to \CGS/\!\!\simeq
\]
For $\sim$-strategies $\sigma_1 : \S_1 \to \A_1^\perp \parallel \B_1$ and $\sigma_2 : \S_2 \to \A_2^\perp \parallel \B_2$,
we set:
\[
\sigma_1 \parallel_s \sigma_2 : \S_1 \parallel \S_2 \to (\A_1\parallel \A_2)^\perp \parallel (\B_1 \parallel \B_2)
\]
to be the obvious map of essps. It is direct to show the bifunctor laws, which are in fact satisfied up to
isomorphisms. 

\paragraph{Lifting.}
In order to give the structural maps of the compact closed stucture, it will be useful to be able to
automatically lift maps of essps to $\sim$-strategies.
For that, we start by noticing that given a strong-receptive, courteous map
of essps $f^\perp : \B^\perp \to \A^\perp$, one can always lift it to a
$\sim$-strategy $\lift{f}: \A \profto \B$, defined by:
\[
\begin{array}{rcrcl}
\lift{f} &:& \CC_\B &\to& \A^\perp \parallel \B\\
&& c &\mapsto & (f^\perp \parallel \B)\circ \cc_\B(c)
\end{array}
\]
The $\sim$-pre-strategy $\lift{f}$ is courteous and strong-receptive because these properties are stable under
composition in $\ESSP$. It is also thin, which is automatically inherited from $\CC_\B$. Moreover, we note that
if $f, g: \B \to \A$ are symmetric then $\lift{f}$ and $\lift{g}$ are weakly equivalent; indeed the 
identity $\id_{\CC_B}$ in both directions provides a weak equivalence.

We now characterise the configurations and symmetries corresponding to the composition of $\sim$-strategies with lifted maps.

\begin{lemma}
Let $f^\perp : \B^\perp \to \A^\perp$ be a strong-receptive, courteous map of essps with $\A, \B$ tcgs, and 
%$\sigma : \S \to \B^\perp \parallel \C$ be a strong-receptive, courteous $\sim$-pre-strategy. Then $\sigma\odot \lift{f} : 
$\sigma : \S \to \B^\perp \parallel \C$ be a $\sim$-strategy. Then $\sigma\odot \lift{f} : 
\A\cgsto \C$ is isomorphic (in $\ESSP/\A^\perp \parallel \C$) to $(f^\perp \parallel \C)\circ \sigma : \S \to \A^\perp \parallel \C$.
\label{lem:lifting1}
\end{lemma}
\begin{proof}
Consider the pullback $(\CC_\B\parallel \C)\circledast (\A\parallel \S)$ (along the maps $(f \parallel \B \parallel \C)\circ 
(\cc_\B \parallel \C)$ and $\A\parallel \sigma$) involved in the definition of 
$\sigma \odot \lift{f}$. 

For each $x\in \conf{S}$ we have $\sigma(x) = x_B + x_C$, we write $\sigma_B = x_B$ and $\sigma_C = x_C$.
By Proposition \ref{prop:secured},  configurations of the pullback correspond to composite
secured bijections:
\[
x_B \parallel \sigma_B\,y \parallel \sigma_C\,y \iso f(x_B)\parallel \sigma_B\,y \parallel \sigma_C\,y \iso f(x_B)\parallel y
\]
with $x_B \sqsubseteq \sigma_B\,y \in \conf{B}$ (where $\sqsubseteq$, defined as $\supseteq^+ \subseteq^-$ is the Scott order
-- see \emph{e.g.} \cite{WGames}) and $y\in \conf{S}$. Clearly, this space of configurations is
isomorphic to the space of configurations of the pullback $(\CC_B\parallel C)\circledast (B \parallel S)$ (along the maps
$(\cc_B \parallel C)\circledast (B\parallel \sigma)$), described by the composite secured bijections:
\[
x_B \parallel \sigma_B\,y \parallel \sigma_C\,y \iso x_B\parallel \sigma_B\,y \parallel \sigma_C\,y \iso x_B\parallel y
\]
with $x_B \sqsubseteq \sigma_B\,y$. This isomorphism of configurations preserves $\cov$ and compatible unions, so
it is an isomorphism of event structures between the corresponding pullbacks. Additionally it sends visible events to
visible events, so it yields an isomorphism (of $\ESP$) making the following diagram commute:
\[
\xymatrix{
S \odot \lift{f}
	\ar[r]^{f'}
	\ar[d]^{\sigma \odot \lift{f}}&
S\odot \CC_B
	\ar[d]^{\sigma \odot \cc_B}\\
A^\perp \parallel C&
B^\perp \parallel C
	\ar[l]_{f^\perp \parallel C}
}
\]
By composition with the usual isomorphism $\sigma \odot \cc_B \iso \sigma$, this yields the required isomorphism between
$\sigma\odot \lift{f}$ and $(f^\perp \parallel C)\circ \sigma$. This isomorphism preserves symmetry, since the
very same construction can be performed the symmetries in a way preserving projections.
\end{proof}

Note that from the lemma above already follows a useful property of lifting: it is functorial.

\begin{lemma}
Let $f^\perp : \C^\perp \to \B^\perp$ and $g^\perp : \B^\perp \to \A^\perp$ be strong-receptive, courteous maps
of essps. Then, we have an isomorphism in $\ESSP/\A^\perp \parallel \C$:
\[
\lift{f}\odot \lift{g} = \lift{g\circ f}
\]
\label{lem:lifting_functorial}
\end{lemma}
\begin{proof}
Direct application of Lemma \ref{lem:lifting1}.
\end{proof}

% Lemme adapté, mais est-ce qu'on en a vraiment besoin ?
%\begin{lemma}
%Let $f^\perp : \C^\perp \to \B^\perp$ be a strong-receptive, courteous map of essps with $\A, \B$ cgs,
%and $\sigma : \S \to \A^\perp \parallel \B$ be a $\sim$-strategy.
%Then, the composite
%$\lift{f}\odot \sigma : \CC_\C \odot \S \to \A^\perp \parallel \B$ is isomorphic (in the slice category $\ESSP/\A^\perp \parallel \B$)
%to the map:
%\[
%\S\circledast (\A^\perp\parallel \C) \stackrel{\Pi_2}{\to} \A^\perp \parallel \B
%\]
%where $\S\circledast (\A^\perp\parallel \C)$ is obtained by the pullback in $\ESSP$ of the maps
%$\sigma : \S \to \A^\perp \parallel \B$ and $\A^\perp \parallel f : \A^\perp \parallel \C \to \A^\perp \parallel \B$.
%\label{lem:lifting2}
%\end{lemma}
%\begin{proof}
%The proof essentially mimics the identity property of copycat.
%
%The composition $\lift{f}\odot \sigma$ is defined through the pullback $(\S\parallel \C)\circledast (\A\parallel \CC_\C)$;
%and from the definition we know that configurations of $\CC_C \odot S$ correspond with configurations of
%the pullback $(S\parallel C)\circledast (A\parallel \CC_C)$ where each event is dominated by a visible one. By
%Proposition \ref{prop:secured} and a direct analysis (using courtesy of $\sigma$), these configurations correspond to triples:
%\[
%\{(x_S, y_C, z_C)\in \conf{S}\times \conf{C}^2\mid \sigma_B\,x_S = f(y_C) \wedge y_C \subseteq^- z_C\}
%\]
%
%Likewise, configurations of the pullback $S\circledast (A^\perp\parallel C)$ correspond to pairs:
%\[
%\{(x_S, x_C)\in \conf{S}\times \conf{C}\mid \sigma_B\,x_S = f(x_C)\}
%\]
%
%From a triple $(x_S, y_C, z_C)$ such that $\sigma_B\,x_2 = f(y_C)$ and $y_C\subseteq^- z_C$, we know by receptivity
%of $\sigma$ that there is a unique $x_S \subseteq^- x'_S$ such that $\sigma_B\,x'_S = f(z_C)$; so we associate to
%$(x_S, y_C, z_C)$ the pair $(x'_S, z_C)$.
%Reciprocally from a pair $(x_S, x_C)$ such that $\sigma_B\,x_S = f(x_C)$, we define $x'_S$ as the smallest configuration 
%of $S$ such that $x'_S \subseteq^- x_S$ and we associate to $(x_S, x_C)$ the triple $(x_S, f(\sigma_B\,x_S), x_C)$.
%
%These associations preserve bounded unions of configurations of the pullback, by uniqueness of receptivity. They do
%not preserve the covering relation on the pullback $(S\parallel C)\circledast (A\parallel \CC_C)$; but they preserve
%it on its projection to visible events, \emph{i.e.} minimal extensions such that each event is dominated by a visible one.
%These associations preserve the mappings $(x_S, y_C, z_C) \mapsto \sigma_A\,x_S\parallel z_C$ and
%$(x_S, x_C) \mapsto \sigma_A\,x_S \parallel x_C$, so they yield an isomorphism of $\ESP/A^\perp \parallel B$ between
%$\lift{f}\odot \sigma$ and $\Pi_2 : S\circledast (A^\perp\parallel C) \to A^\perp \parallel C$. The same construction
%works with symmetries as well and preserves projections, so this extends to an isomorphism in $\ESSP/\A^\perp \parallel \B$.
%\end{proof}

\paragraph{Compact closed structure.} In $\ESSP$, parallel composition has a unit up to isomorphism, namely the 
empty game $1$. In fact equipped with $\parallel$, $\ESSP$ has a symmetric monoidal structure given by the following 
natural isomorphisms:
\[
\begin{array}{rcccl}
\rho_\A &:& \A \parallel 1 &\to& \A\\
\lambda_\A &:& 1 \parallel \A &\to& \A\\
s_{\A, \B} &:& \A \parallel \B &\to& \B \parallel \A\\
\alpha_{\A, \B, \C} &:& (\A\parallel \B) \parallel \C &\to& \A \parallel (\B \parallel \C)
\end{array}
\]
Then, these lift to:
\[
\begin{array}{rcccl}
\lift{\rho_{\A^\perp}^{-1}} &:& \A \parallel 1 &\cgsto& \A\\
\lift{\lambda_{\A^\perp}^{-1}} &:& 1 \parallel \A &\cgsto& \A\\
\lift{s_{\A^\perp, \B^\perp}^{-1}} &:& \A \parallel \B &\cgsto& \B \parallel \A\\
\lift{\alpha_{\A^\perp, \B^\perp, \C^\perp}^{-1}} &:& (\A\parallel \B) \parallel \C &\cgsto& \A \parallel (\B \parallel \C)
\end{array}
\]
which satisfy the required equations by Lemma \ref{lem:lifting_functorial}. 

Note also the duality: for $\sigma : \A\cgsto \B$ we also have $\sigma^\perp : \B^\perp \cgsto \A^\perp$, such that
$(\tau \odot \sigma)^\perp = \sigma^\perp \odot \tau^\perp$. Using that, the fact that the essp maps above are isomorphisms
and Lemma \ref{lem:lifting1}, it is straightforward to show that the liftings above are natural.

Finally, we have the obvious maps:
\[
\begin{array}{rcccl}
\eta_\A &:& \CC_\A &\to & 1^\perp \parallel (\A^\perp \parallel \A)\\
\epsilon_\A &:& \CC_\A &\to& (\A \parallel \A^\perp)^\perp \parallel 1
\end{array}
\]
and it is a direct variant of the neutrality of copycat under composition to check that these obey
the required unit and co-unit laws, so we have:

\begin{proposition}
The category $\CGS/\!\!\simeq$ is compact closed.
\end{proposition}

cho.bbl
\begin{thebibliography}{CCW14}

\bibitem[CCW14]{lics14}
Simon Castellan, Pierre Clairambault, and Glynn Winskel.
\newblock Symmetry in concurrent games.
\newblock In {\em CSL-LICS}, 2014.

\bibitem[HO00]{DBLP:journals/iandc/HylandO00}
J.~M.~E. Hyland and C.-H.~Luke Ong.
\newblock On full abstraction for {PCF: I, II, and III}.
\newblock {\em Inf. Comput.}, 163(2):285--408, 2000.

\bibitem[MM07]{DBLP:conf/concur/MelliesM07}
Paul-Andr{\'e} Melli{\`e}s and Samuel Mimram.
\newblock Asynchronous games: Innocence without alternation.
\newblock In Lu\'{\i}s Caires and Vasco~Thudichum Vasconcelos, editors, {\em
  CONCUR}, volume 4703 of {\em LNCS}, pages 395--411. Springer, 2007.

\bibitem[RW11]{DBLP:conf/lics/RideauW11}
Silvain Rideau and Glynn Winskel.
\newblock Concurrent strategies.
\newblock In {\em LICS}, pages 409--418. IEEE Computer Society, 2011.

\bibitem[Win07]{DBLP:journals/entcs/Winskel07}
Glynn Winskel.
\newblock Event structures with symmetry.
\newblock {\em Electr. Notes Theor. Comput. Sci.}, 172:611--652, 2007.

\bibitem[Win11]{WGames}
Glynn Winskel.
\newblock Event structures, stable families and games.
\newblock {\em Lecture notes, Aarhus University, At
  http://daimi.au.dk/$\sim$gwinskel}, 2011.

\bibitem[Win12]{DBLP:journals/fac/Winskel12}
Glynn Winskel.
\newblock Deterministic concurrent strategies.
\newblock {\em Formal Asp. Comput.}, 24(4-6):647--660, 2012.

\end{thebibliography}
