Simon Castellan
email: simon.castellan@ens-lyon.fr

Pierre Clairambault
email: pierre.clairambault@ens-lyon.fr

Silvain Rideau
email: silvain.rideau@berkeley.edu

Glynn Winskel
email: glynn.winskel@cl.cam.ac.uk

Creative Commons

GAMES AND STRATEGIES AS EVENT STRUCTURES

Keywords: 1998 ACM Subject Classification: F.3.2 Games, event structures, concurrency

niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Games are ubiquitous. They appear in many areas, such as economics, logic, and computer science. They provide a valuable language in which one can model situations where the evolution of a system is determined by the choices of several agents. The agents are players performing moves according to rules that model the situation at hand, and the evolution of the system follows from the sequence of moves reflecting the decisions of the players. The outcome of the game might be a payoff for each player, a successful refutation of a logical formula, a bug exposed in a program -or, in some instances, we might just be interested in the play itself as a description of the evolution of a system. Although games can in general involve many players, they often (as in this paper) focus on two players: Player (Proponent, ∃loïse, Verifier, . . . ) and Opponent (∀bélard, Spoiler, . . . ) each one defending their interests while subject to attacks of the other. Two-player games are perfectly suited to the representation of open systems: one player plays for the system at hand, while the other is deemed external and plays for the environment. Player may be regarded as representing a team of players, whose interaction yields the system under study.

In their traditional formulation, games are highly sequential: the behaviour of a game determines a tree of which the nodes are the positions and the branches describe the different choices available to a player. The interaction between the players results in the selection of a potentially infinite branch of the game tree. Most of the time, each position belongs to exactly one player and the other has to wait until a move is played. Often, the game also obeys the condition of alternation where players are additionally required to play in turns.

Despite this sequential nature, one also would like to use games to represent situations that are concurrent or distributed, e.g. several systems running in parallel, possibly with synchronizations or shared resources. Of course such concurrent applications of games exist, but it is worth pointing out that in the overwhelming majority of cases concurrency is represented indirectly via the interleaving, or linearization, of atomic actions of the participants. Rather than using a notion of game that does justice to the distributed nature of the system, a tree-based, inherently sequential representation is opted for, where a branch is a total ordering of the implicitly partially ordered evolution of the system. In other words, concurrency is modelled by removing alternation, but the basic tree-based understanding remains unquestioned. Of course, that representation has been useful and sufficiently accurate to a large extent, and a significant and successful body of work follows from this choice. But we believe nonetheless that a more precise causal representation is to be preferred. Our reasons and a further discussion on this point can be found in Section 2.

However, causal representations of concurrent processes have a richer structure than trees, and require more elaborate tools to be dealt with properly. It was not clear at first on what mathematical formalism one should rely on for this endeavour. The first causal foundations for concurrent games emerged in the late nineties in the game semantics community; due to Abramsky and Melliès [START_REF] Abramsky | Concurrent games and full completeness[END_REF], they were used to build a fully complete model of multiplicative additive linear logic (MALL). The idea was to switch from a tree to a domain of positions, and formulate (deterministic) strategies as closure operators on this domain. Later, Melliès and Mimram [START_REF] Melliès | Asynchronous games: Innocence without alternation[END_REF] connected this position-based approach to a more traditional play-based formulation in the framework of asynchronous gamesin this setting (deterministic) strategies were manipulated as traditional sets of plays, but with closure properties ensuring an underlying causal order between moves. In parallel, Faggian and Piccollo [START_REF] Faggian | Partial orders, event structures and linear strategies[END_REF] had developed a setting where the (deterministic) strategies were manipulated explicitly as partial orders, rather than the partial order being recovered a posteriori. Finally, in 2011 Rideau and Winskel [START_REF] Rideau | Concurrent strategies[END_REF] generalized all prior work by proposing a setting where (non-deterministic) strategies are described as event structures, thus benefiting from a body of work on event structure models for concurrency.

The present paper aims to be a detailed and self-contained introduction to this latter formulation of concurrent games: it covers details and extends the results of [START_REF] Rideau | Concurrent strategies[END_REF]. In Section 2, we start with a gentle introduction to the basic ideas behind the representation of concurrent processes as event structures, with an eye towards the application to games. In this setting, both games and "pre-strategies" playing on them are event structures, with a pre-strategy being essentially an event structure labelled by moves of the game. But pre-strategies, thought of as prototypical strategies for Player, are too expressive: they may impose unreasonable constraints on Opponent, and can behave in ways that are not consistent with their standing for interaction in an asynchronous distributed environment. As an answer to this, strategies are introduced in Section 3 as the pre-strategies that are preserved under composition with an asynchronous forwarder, formalized as a copycat strategy. This provides an adequately robust notion of strategy on an event structure, and a non-deterministic generalization of the earlier notions of concurrent strategies mentioned above. We prove the main result of [START_REF] Rideau | Concurrent strategies[END_REF]: that strategies are exactly the pre-strategies obeying conditions called receptivity and courtesy. The paper [START_REF] Rideau | Concurrent strategies[END_REF] also constructed a bicategory of concurrent games and strategies between them, akin to Joyal's category of Conway games [START_REF] Joyal | Remarques sur la thorie des jeux deux personnes[END_REF]. In Section 4, we give a detailed proof of that result. Finally in Section 5 we show that just as Joyal's category, our category is compact closed and can provide a basis for games-based models of higher-order computation. In Section 6, we conclude.

1.0.1. Other related work. Many other notions of games for concurrency have appeared in the literature.

In the verification community, "concurrent games" [START_REF] De Alfaro | Concurrent omega-regular games[END_REF][START_REF] Luca De Alfaro | Concurrent reachability games[END_REF] refer to variations of Blackwell games [START_REF] Donald A Martin | The determinacy of blackwell games[END_REF]: there is a tree (or a graph) of positions. The game is played in rounds: at each round, both players select their behaviour from a pool of possible actions. This selection is independent, and with no information on the other player's choice. The next position is decided as a function of both player's choices. In contrast to our setting, their focus is on enforcing the independence of the two players in each round, rather than describing a general concurrent computation. In particular, plays are still totally ordered. Games in event structures are closer to the games played in Zielonka automata [START_REF] Genest | Asynchronous games over tree architectures[END_REF], which could be unfolded to event structures. However, our focus is more on the unfoldings themselves, and on their compositional structure.

Through our focus on compositionality, we are very close to the notions of games for concurrency studied in the semantics community [START_REF] Laird | A game semantics of idealized CSP[END_REF][START_REF] Ghica | Angelic semantics of fine-grained concurrency[END_REF]. Just as we do, they form categories of games and strategies where concurrent processes can be modelled. However, these models are based on interleavings rather than partial orders: rather than opting for a primitive representation of concurrency based on partial orders, they represent the execution of a concurrent process via the non-deterministic schedulings of its possible actions.

Finally, in a different direction, let us cite the "playgrounds" of Hirschowitz et al [START_REF] Hirschowitz | Innocent strategies as presheaves and interactive equivalences for CCS[END_REF][START_REF] Hirschowitz | Full abstraction for fair testing in CCS[END_REF], and the multi-token Geometry of Interaction of Dal Lago et al [START_REF] Dal Lago | The geometry of synchronization[END_REF]. Both formalisms aim at providing a non interleaving-based representation of concurrent processes and of their execution. They should both relate to our approach, in the sense that from their settings one could extract an event structure, which is arguably more abstract and syntax-independent than the models used there.

Event structures, games and pre-strategies

In this section we introduce the basic notions underlying our development, from event structures to pre-strategies represented by them.

2.1. Events for concurrent and distributed systems.

2.1.1. Causality and independence. It is common to describe the evolution of a process or system by listing its events, i.e. the observable actions occurring through time. For instance, one could describe an interaction with a coffee vending machine as a sequence: coin • coffee that we call a trace, where coin represents the action of inserting a coin in the machine, and coffee represents the action of getting a coffee. In fact, the input/output behaviour of the vending machine may be modelled by the set: Coffee = {ǫ, coin, coin • coffee} where ǫ is the empty sequence (and with possibly more iterations of the interaction if one is not interested in a one-use coffee vending machine). Nearby the coffee machine, there is a tea machine modelled by: Tea = {ǫ, coin ′ , coin ′ • tea} where we use coin ′ to distinguish it from coin.

The two machines may be interacted with in parallel -one may for instance pay for a coffee, then, while waiting for the machine to deliver, also pay for a tea, and then obtain both. This behaviour may be represented as coin • coin ′ • coffee • tea. In fact, the system formed by both machines can be modelled as:

{ǫ, coin, coin • coin ′ , coin • coffee, coin • coin ′ • coffee, coin • coffee • coin ′ , coin • coin ′ • tea, coin • coin ′ • coffee • tea, coin • coin ′ • tea • coffee, coin • coffee • coin ′ • tea, coin ′ , coin ′ • coin, coin ′ • tea, coin ′ • coin • tea, coin ′ • tea • coin, coin ′ • coin • tea • coffee, coin ′ • coin • coffee, coin ′ • coin • coffee • tea, coin ′ • tea • coin • coffee}
This follows the so-called interleaving-based approach to modelling concurrent and parallel systems: that two independent processes interacted with in parallel should behave as the set of interleavings of the traces of the original processes. This approach proved powerful and versatile, and provides the basis for most developments on models of concurrency.

However, it suffers from some drawbacks. To cite two of them: (1) as should appear clearly in our example, this representation gets exponentially bigger than the original system -this is the so-called state explosion problem, which is a main challenge in interleavingbased model-checking of concurrent systems, (2) it is unreadable, and obfuscates the key information of which events depend on which events. Instead of the large set of traces above, one would like to manage with only the partial order generating it displayed in Figure 1, for which the set of traces above is the set of all linearizations. This idea is far from new:

coffee tea coin v v coin ′ v v
Figure 1. Partial order semantics for the coffee and tea machines advocated first by Petri, it is known as the independence, partial order, causal, or truly concurrent approach to models of concurrency. Although causal models yield smaller and more intuitive representations of the dynamics of a concurrent process, they can be quite subtle to manipulate and manage. Operations that are straightforward for interleavingbased approaches, and say based on simple induction, can be more mathematically involved when carried out in a partial-ordered setting.

2.1.2. Event structures. Our example above is purely deterministic: it appears visibly in the partial order of Figure 1 that no irreversible choice is ever made in the evolution of the system. Whatever order the events of a prefix of the partial order of Figure 1 appear, they can be completed to the maximal set {coin, coffee, coin ′ , tea}. In this sense the order in which these events occur is irrelevant. To express non-determinism, one needs to enrich the partial order. A natural way to do that is to follow Winskel [START_REF] Winskel | Event structures[END_REF] and add a consistency relation on top of the partial order, as follows.

Definition 2.1 (Event structures). An event structure (es for short) is a tuple (E, ≤ E , Con E ) where E is a set of events, ≤ E is a partial order on E called causality and Con E is a non-empty set of finite subsets of E called consistency, such that:

∀e ∈ E, [e] = {e ′ ∈ E | e ′ ≤ E e} is finite, ∀e ∈ E, {e} ∈ Con E , ∀X ∈ Con E , ∀Y ⊆ X, Y ∈ Con E , ∀X ∈ Con E , ∀e ∈ X, ∀e ′ ≤ E e, X ∪ {e ′ } ∈ Con E
We will often omit the subscripts in ≤ E , Con E if they are obvious from the context, and use E both for the event structure and its underlying set of events.

If X ⊆ E is in Con, then we say that it is consistent, and its events may occur together. The states of an event structure E, called configurations, are the sets x ⊆ E that are both consistent (in the sense that every finite subset belongs to Con E ) and downclosed (i.e. for all e ∈ x, for all e ′ ≤ e, one has e ′ ∈ x). Here we shall work exclusively with finite configurations, those finite sets x ⊆ E that are both consistent and down-closed; the set of such configurations of E is written C (E), and is partially ordered by inclusion. Configurations with a maximal element are called prime configurations, they are those of the form [e] for e ∈ E. We will also use the notation [e) = [e] \ {e}. Between configurations, the covering relation x-⊂y means that y is obtained from x by adding exactly one event:

y is an atomic extension of x. We might also write x e --⊂ to mean that e ∈ x and x ∪ {e} ∈ C (E); this says that the event e is enabled at x. It is easy to prove that the relation ⊆ between configurations is the transitive reflexive closure of -⊂; in fact -⊂ is its transitive reduction.

When drawing event structures, we will not portray the full partial order ≤ but its transitive reduction; the immediate causality generating it defined as e e ′ whenever e < e ′ and for any e ≤ e ′′ ≤ e ′ , either e = e ′′ or e ′′ = e ′ . Finally, we say two events e, e ′ are concurrent when they are consistent and incomparable for ≤ E .

Event structures can express non binary conflict, e.g. one can have three events {1, 2, 3} with consistent subsets those with at most two elements: all events are pairwise consistent, but not the three of them together. This extra generality makes for a smooth theory, but in many examples consistency is equivalently described by a complementary irreflexive binary conflict relation ♯, that relates any two events that cannot occur together, i.e. X ∈ Con iff for all e, e ′ ∈ X, ¬(e ♯ e ′ ). It follows then from the axioms of event structures that if e ♯ e ′ and e ′ ≤ e ′′ , then e ♯ e ′′ as well -we call this conflict inherited. A conflict e ♯ e ′ that is not inherited is called minimal, and represented as e / o e ′ . In order to alleviate the notation, when drawing event structures with binary conflict we only represent minimal conflicts.

As an example, consider a (less popular) variant of the coffee machine above: when a coin is inserted it will produce a tea or a coffee, nondeterministically. The corresponding event structure can be represented as follows:

coffee / o / o / o / o / o / o tea coin j w w w w R S S c t t t t
Its configurations are {{∅}, {coin}, {coin, coffee}, {coin, tea}}. We will never get both tea and coffee even though both are enabled by coin.

2.1.3. Simple parallel composition. Whereas using traces the operation of putting two systems in parallel without communication or interaction was the source of a combinatorial explosion, in event structures it only consists in putting two event structures side by side. For instance, the event structure of Figure 1 is obtained in a transparent way from event structures for the coffee and tea machines. Generally: Definition 2.2. Given two event structures E and F their simple parallel composition (or just parallel composition for short) E F is defined as the event structure comprising:

• Events:

{0} × E ∪ {1} × F (tagged disjoint union of E and F ), • Causality: (i, c) ≤ E F (j, c ′ ) when i = j = 0 and c ≤ E c ′ or i = j = 1 and c ≤ F c ′ ,
• Consistency defined as:

X ∈ Con E F iff {a | (0, a) ∈ X} ∈ Con E & {b | (1, b) ∈ X} ∈ Con F
Thus, E F is E and F put side-by-side with no causality or conflict between them. As a result, configurations of E F can be easily described in terms of those of E and F -namely there is a canonical order-isomorphism C (E F ) ∼ = C (E) × C (F ) (where configurations are ordered by inclusion). We will denote by x y ∈ C (E F ) the configuration corresponding to (x, y) ∈ C (E) × C (F ). When denoting events of a parallel composition E 1 E 2 , we will not always write the explicit injections (as in (0, e) or (1, e)). Instead, we will often annotate or name the events so as to disambiguate the components they belong to (as in e.g. e 1 , e 2 ).

2.1.4. Conjunctive causality and projection. In this setting of event structures causality is conjunctive rather than disjunctive: states/configurations need to be down-closed, so for an event to occur it is required that all of its dependencies have occurred before. For instance, in the event structure of Figure 2 the user needs to both insert a coin and press a button in order to get a drink (inserting a coin and pressing both buttons results in a non-deterministic choice).

coffee / o / o / o / o / o / o / o / o / o / o / o / o tea coin I R R a q q q q
SelectCoffee e e l SelectTea k Figure 2. An event structure for a vending machine with selection Plain event structures cannot express that an event may occur for two distinct, independent reasons -such as in saying that coffee can be obtain through a coin or through an override mechanism. In event structures, expressing that would require two distinct events coffee and coffee ′ , with different causal histories. The apparent limitation that each event has a unique, unambiguous causal history enables us to perform the following projection operation 1 : Definition 2.3. If E is an event structure and V ⊆ E is a subset of events, then the projection E ↓ V has V as events, and causality and consistency directly inherited from V : if e 1 , e 2 ∈ V then e 1 ≤ E↓V e 2 iff e 1 ≤ E e 2 , and for X a finite subset of V , X ∈ Con E↓V iff X ∈ Con E .

In other words, the projection E ↓ V is obtained by considering the events not in V to be invisible: they occur silently, and are not observable anymore. Because causality is conjunctive, for an event e ∈ E ↓ V there is never any ambiguity as to what events caused it in E.

Each configuration y ∈ C (E) projects to y ∩ V ∈ C (E ↓ V ) -reciprocally, any x ∈ C (E ↓ V ) has a minimal witness [x] E = {e ′ ∈ E | e ′ ≤ E e ∈ x} ∈ C (E), yielding a bijection: C (E ↓ V ) ∼ = {x ∈ C (E) | ∀e ∈ x maximal, e ∈ V } x → [x] E y ∩ V
→ y that preserves and reflects inclusion. This feature will be key to the hiding step of the composition of strategies, introduced later. 2.1.5. Polarity and pre-strategies. We now move towards games. We consider two-player games between Player (considered as having positive polarity) and Opponent (considered as having negative polarity). Each event is equipped with a polarity, indicating which player has the responsibility to play it. Definition 2.4. An event structure with polarities (esp for short) is an event structure A along with a function pol A : A → {-, +} associating to each event a polarity.

When introducing events of an esp A, we might annotate them in order to indicate their polarity. For instance, in "let a -∈ A", a ranges over all events of A of negative polarity. For configurations x, y ∈ C (A), we will write x ⊆ -y if x ⊆ y and all events in y \ x are negative; x ⊆ + y is defined dually. For an esp A, we will write A ⊥ for its dual, i.e. A with the same data, except for the polarity which is reversed.

We define games to be simply esps. The terms game and esp will however not be used interchangeably: we will use games for those esps used to specify the interface at which two players interact (strategies will also be certain esps). For instance, one could model the interface of the vending machine above by saying that Player plays according to the program of the coffee machine, Opponent plays for the user, and the game describes the observable actions through which they interact on the physical device. Following this idea, the game for the physical interface of the coffee machine would have events 1 General event structures [START_REF] Winskel | Events in computation[END_REF] avoid this restriction, though they do not support a reasonable projection operation.

{coin -, SelectCoffee -, SelectTea -, coffee + , tea + }, for causality the discrete partial order (i.e. the order contains only the reflexive pairs), and all sets consistent. This game is a discrete partial order, but in general games can feature non-trivial causality and consistency.

The strategy for Player would then describe the behaviour of the vending machine at this interface, represented as an event structure as well (such as Figure 2). Both games and strategies are expressed as esps; they will nonetheless play very different roles in the development. Following this idea, we now define pre-strategies -strategies, defined later, will be subject to further conditions. Definition 2.5. A pre-strategy on a game A is an esp S labelled by A, that is, a function σ : S → A which:

(1) Obeys the rules of the game (preserves configurations):

∀x ∈ C (S), σx ∈ C (A)
(2) Plays linearly (local injectivity):

∀s, s ′ ∈ x ∈ C (S), σs = σs ′ =⇒ s = s ′
(3) Preserves polarity: ∀s ∈ S, pol A (σs) = pol S (s) Note that σ does not need to preserve the order. On the other hand, as we will see later (Lemma 2.13) it follows from these axioms that it always reflects it for consistent events.

As announced, a pre-strategy on A is an esp S along with a labelling function σ : S → A. The esp structure on A brings constraints, that the labelling function has to respect. It is easy to check that the event structure of Figure 2 is a pre-strategy on the game M = {coin -, SelectCoffee -, SelectTea -, coffee + , tea + } (with trivial causality and all subsets consistent), with the obvious map to it given by the labels. In the rest of this paper, when drawing pre-strategies we will follow the presentation of Figure 2: we will draw the event structure S, with events written as their image via σ.

Remark 2.6. A pre-strategy σ : S → A is locally injective but may not be injective: there may well be several incompatible events in S mapping to the same event in A. This is true even for two events s 1 , s 2 ∈ S sharing the same causal history, e.g. [s 1 ) = [s 2 ). For instance, the following variant of Figure 2 represents a valid pre-strategy on the game M above.

coffee + / o / o / o coffee + coin - v v B I I V j j j j j j j j SelectCoffee - f f m v v
The intuition here is that the coffee machine secretly tosses a coin (it has plenty of those after all), but the result does not change its behaviour: it serves the coffee nonetheless. The intensional information of this nondeterministic choice, despite being unobservable, can be recorded by our semantics. This intensionality means that our model will not validate the idempotency law for nondeterministic choice: the event structures e

/ o / o / o
e and e are not isomorphic.

Though it is not covered in this paper, one may opt for a variant of our setting that does validate idempotency (see e.g. [START_REF] Castellan | Causality vs. interleavings in concurrent game semantics[END_REF]). But as a consequence we would also lose the branching information. To illustrate this, consider the following variant of the pre-strategy above, playing on an extension of M popular in the United Kingdom.

milk + SelectMilk - v v SelectMilk - coffee + / o / o / o / o / o v v coffee + v v coin - v v A I I V i i i i i i i i i i SelectCoffee - ! f f m v v
In this version, the user has the possibility of requesting milk after the coffee is served. But in the pre-strategy above, they may not always get it: something may go wrong in the machine before the coffee is served, leading to a state where SelectMilk -is ineffective and the user frustrated. The highly intensional, non-idempotent representation of concurrency we opt for in this paper allows us to record this branching information. In settings where this branching information is not relevant, such as in [START_REF] Castellan | Causality vs. interleavings in concurrent game semantics[END_REF], it can be easily forgotten.

Besides being natural (we hope) as a first tentative definition of strategies, the prestrategies defined above match the standard notion of maps between event structures. Definition 2.7. If E, F are event structures, a (total) map of event structures from E to F is a function on events f : E → F satisfying (1) and (2) above.

The identity function on E is a map of event structures and those are stable under composition; in other words there is a category E of event structures and maps.

Later on we will also consider partial maps between event structures (Definition 4.2), but throughout this paper all maps are considered total unless explicitly said otherwise. We also have a category EP of esps, and maps preserving polarities -technically pre-strategies are exactly maps of esps. We keep a distinguished terminology, because in the sequel we will encounter maps of esps that it is unwise to regard as pre-strategies.

We note in passing that simple parallel composition extends to esps by defining the polarity of A B as pol A B (0, a) = pol A (a) and pol A B (1, b) = pol B (b) -this entails that parallel composition commutes with the duality operation, i.e. (A B) ⊥ = A ⊥ B ⊥ . Two pre-strategies σ : S → A and τ : T → B playing respectively on A and B can be combined to form a pre-strategy σ τ : S T → A B defined by (σ τ )(0, a) = (0, σ(a)) and (σ τ )(1, b) = (1, τ (b)). In fact with this definition, simple parallel composition acts functorially on maps of es and esp and equip the categories E and EP with the structure of a symmetric monoidal category (with the empty event structure 1 as unit).

At this point, the reader may find confusing the fact that although there are polarities in games and pre-strategies, these are not taken into special account in the definition of prestrategies (besides their preservation by the labeling function). This makes pre-strategies more powerful than perhaps wished: a pre-strategy may constrain the external Opponent beyond the rules of the game. Taking S = 1 the empty event structure, and writing ⊖ for the esp with just one negative event, the empty map S → ⊖ is a valid pre-strategy. As S has no counterpart for the unique negative move in the game, this pre-strategy fails to acknowledge Opponent's right to play it. This is in contradiction with the idea that Opponent's available actions should only depend on the game, and not be controllable by Player. We will see in Section 3 other ways in which pre-strategies may constrain Opponent in unintended ways. This is because the current definition is an intermediate step, towards the notion of strategy introduced in Section 3 that will take polarity more carefully into account. Whereas pre-strategies axiomatize the polarity-agnostic description of the evolution of a concurrent process on an interface, strategies will satisfy polarity-specific constraints, e.g. a strategy cannot prevent its opponent from playing a move enabled in the game. But for the remainder of this section, polarities are present only to set the stage for Section 3.

2.2. Interaction of pre-strategies. Pre-strategies playing on A ⊥ are pre-strategies for Opponent or counter pre-strategies. Given a pre-strategy σ : S → A and a counter prestrategy τ : T → A ⊥ , we proceed to explain how they interact with each other. As σ and τ have opposite expectations for the polarity of events in A, their interaction will drop all information about polarities, i.e. it will be a map of event structures (in E):

σ ∧ τ : S ∧ T → A
where A is silently coerced to an event structure without polarities. We regard it again as an event structure S ∧ T describing the causal structure of actions that both σ and τ agree to, along with a labeling σ ∧ τ of S ∧ T by events of (a polarity-agnostic version of) A.

In fact, the definition of interaction makes use neither of the polarity information in S, T , or A, nor of its preservation by σ and τ . So we will define it in this section as an operation which for two maps σ : S → A and τ : T → A in E, yields a map σ ∧τ : S ∧T → A in E. Polarities will only become relevant again in Section 2.3, when we define composition.

As we will see, interaction is very close to the product of event structures used in [START_REF] Winskel | Event structure semantics for CCS and related languages[END_REF][START_REF] Winskel | Event structures[END_REF] to interpret the synchronising parallel composition of CCS (we will see that it corresponds to a pullback in E).

2.2.1. Secured bijections. The interaction of σ and τ should follow the behaviour that σ and τ agree on: in a given state, it should be ready to play c ∈ A whenever σ and τ are. In particular, this means that an event c ∈ A played by σ and τ should be played in their interaction only after all the dependencies in S and T are satisfied. For instance the interaction of the following two event structures labelled on the interface A = a b c (consisting in three concurrent events)

c c a v v b a b v v (σ) (τ )
should give rise to the interaction σ ∧ τ :

c a R S S c t t t t t t b i t t t t t t (σ ∧ τ )
with immediate causal links imported from both S and T . Similarly, a set of events should be consistent in the interaction when the corresponding projections in S and T are.

At this point, one is tempted to define the events of S ∧ T as synchronized events: pairs (s, t) ∈ S × T such that σs = τ t. This works correctly when the maps σ and τ are injective but fails in general. For instance, consider the interaction of the two labelled event structures:

b b a / o / o / o / o a ′ a v v (σ) (τ )
Here, σ has two copies a and a ′ of the event a ∈ A (by local injectivity, the two copies must be in conflict) and τ plays b after a. However, because σ has two ways of playing a, the interaction has two possible causal histories for b: either after (a, a) ∈ S × T or after (a ′ , a) ∈ S × T . Since in event structures, each event comes with a unique causal history, those two histories for b must correspond to two different events in S ∧ T , which should therefore look like:

b b ′ a v v / o / o / o a ′ v v
We see that S ∧ T has four events, whereas there are only three possible synchronized pairs: (a, a), (a ′ , a) and (b, b) -thus events of S ∧ T will be more than just pairs. Our approach will be to construct the desired event structure S ∧ T indirectly via the set of configurations that we wish it to have. In the example above, configurations of the diagram are in one-to-one correspondence with synchronized configurations: pairs (x, y) ∈ C (S) × C (T ) such that σx = τ y. By local injectivity, in such a situation σ and τ induce a bijection ϕ : x ≃ σx = τ y ≃ y that is not order preserving in general (we use the notation ≃, as opposed to ∼ =, to insist on the fact that although x, σ x, τ y and y are canonically partially ordered by ≤ S , ≤ A , ≤ T , these bijections do not preserve this order). Note that its graph is a set of synchronized (paired) events as above.

Such bijections will be used to represent configurations of the interaction. But as configurations of an event structure (yet to be defined), the graphs of these bijections should be ordered as well. As shown above, the order on S ∧ T should be inherited from that of S and T . However, the transitive closure of the relation induced by the orders of S and T is, in general, not an order. For instance in the following picture

Drug Money Money v v Drug v v (σ) (τ )
there is a deadlock : σ (the dealer) waits for the money to be delivered before presenting the drug while τ (the buyer) waits for the drug before offering the dollars. Their interaction should be empty as in the empty configuration there is no common event that σ and τ are both ready to play. This is reflected by the fact that on the bijection {(Money, Money), (Drug, Drug)} the preorder induced by S and T is not an order: it has a loop. To eliminate such loops, we introduce secured bijections:

Definition 2.8 (Secured bijection). A secured bijection between two (finite) orders (q, ≤ q ) and (q ′ , ≤ q ′ ) is a bijection ϕ : q ≃ q ′ such that the reflexive and transitive closure of the following relation on the graph of ϕ is an order:

(a, b) ⊳ (a ′ , b ′ ) when a < q a ′ or b < q ′ b ′
Secured bijections need not preserve the order but they do not contradict it: if a < q b then ϕ b < q ′ ϕ a as otherwise this would constitute a cycle.

Equivalently, secured bijections are those bijections satisfying a reachability property akin to one of configurations of event structures, which can always be reached from the empty configuration by successive additions of events. We invite the reader to check the following lemma, which is useful in forging an intuition on the role of the notion.

Lemma 2.9. Let (q, ≤ q ) and (q ′ , ≤ q ′ ). Then a bijection ϕ : q ≃ q ′ is secured, iff there is a sequence of (graphs of) bijections:

(ϕ 0 : x 0 ≃ y 0 ) (a 1 ,b 1 ) --⊂ (ϕ 1 : x 1 ≃ y 1 ) (a 2 ,b 2 ) --⊂ . . . (an,bn) --⊂ (ϕ n : x n ≃ y n )
such that ϕ 0 is the empty bijection, ϕ n = ϕ, and for all 0 ≤ i ≤ n, x i ∈ C (q) and y i ∈ C (q ′ ) (i.e. they are down-closed).

Secured bijections can be used to give a very concise description of the desired states of S ∧ T : write B sec σ,τ for the following set, ordered by inclusion.

B sec σ,τ = {ϕ | ϕ : x σ ≃ σx = τ y τ ≃ y is secured, with x ∈ C (S), y ∈ C (T )}.
Since secured bijections are by definition equipped with a canonical order, the elements of B sec σ,τ can be seen as ordered sets. Immediate causal links in a secured bijection are related to those of the underlying orders:

Lemma 2.10. Let ϕ : q ≃ q ′ be a secured bijection. If we have (a, b) ϕ (a ′ , b ′ ) then either a q a ′ or b q ′ b ′ . Proof. From (a, b) ϕ (a ′ , b ′ ) we deduce (a, b) ⊳ (a ′ , b ′ ). Hence either a < q a ′ or b < q ′ b ′ .
Assume for instance a < q a ′ . If we do not have a q a ′ then there exists a 0 ∈ q such that a < a 0 < a ′ . Then (a 0 , ϕ a 0 ) ∈ ϕ and we have (a, b) < ϕ (a 0 , ϕ a 0 ) < ϕ (a ′ , b ′ ) contradicting the hypothesis.

Prime secured bijections. The order (B sec

σ,τ , ⊆) is (up to isomorphism) the order of configurations of the event structure we are looking for. We can now reconstruct an event structure whose order of configurations matches this order: events are identified as the prime secured bijections, i.e. those with a top (i.e. greatest) synchronized event (s, t). In other words there will be an event for each synchronized pair (s, t) along with a consistent causal history for it, i.e. a prime secured bijection with (s, t) as top element. In particular, if there is none (because of a cycle), it would not appear in the interaction. With these ingredients we can form an event structure: Definition 2.11 (Interaction of pre-strategies). Let σ : S → A and τ : T → A be maps of event structures. We define the event structure S ∧ T as follows:

• Events: those elements of B sec σ,τ that have a top event, • Causality: inclusion of graphs, • Consistency: a finite set X of (graphs of) secured bijections is consistent when its union is still (the graph of) a secured bijection in B sec σ,τ . We invite the reader to apply this definition on the examples at the beginning of Section 2.2.1, and check that we obtain the event structures announced.

It is routine to check that S ∧ T is an event structure such that C (S ∧ T ) is orderisomorphic to B sec σ,τ : Lemma 2.12. For each configuration x ∈ C (S ∧ T ), then ϕ x = ∪x : x S ≃ x T ∈ B sec σ,τ is a secured bijection. Moreover, this assignment is such that

ϕ x → x (s, t) → [(s, t)] ϕx is an order-isomorphism ϕ x ∼ = x
, where [(s, t)] ϕx denotes the down-closure of (s, t) inside the ordered set ϕ x . Moreover, the mapping x → ϕ x defines an order isomorphism

C (S ∧ T ) ∼ = B sec σ,τ . Proof. Let x ∈ C (S ∧ T ). By definition of consistency in S ∧ T , ∪x is the graph of a secured bijection ϕ x ∈ B sec σ,τ .
Any element of x is a secured bijection with a maximal element (s, t), and hence is [(s, t)] ϕx . Thus, [(s, t)] ϕx → (s, t) defines an order-isomorphism x ∼ = ϕ x . This yields a map C (S ∧ T ) → B sec σ,τ . The converse maps a secured bijection ϕ to the set of elements of S ∧ T included in ϕ.

By local injectivity of σ and τ , a secured bijection ϕ : x ≃ y is entirely determined by x and y. Therefore, C (S ∧ T ) is also order-isomorphic to the set of pairs (x, y) ∈ C (S) × C (T ) such that σx = τ y and such that the induced bijection between x and y is secured, partially ordered by componentwise inclusion -we will use this description later on in the proofs. 2.2.3. The interaction pullback. Events of S ∧ T have the form ϕ with a top element (s, t). The mappings Π 1 : ϕ → s and Π 2 : ϕ → t induce maps of event structures S ∧ T → S and S ∧ T → T that make the following diagram commute:

S ∧ T Π 1 z z v v v v v Π 2 6 6 s s s s s S σ 6 6 r r r r r T τ z z u u u u u A
Writing π i for the (set-theoretic) projections, by Lemma 2.12, for every x ∈ C (S ∧ T ) we have

π 1 ϕ x = Π 1 x as π 1 (s, t) = s = Π 1 [(s, t)] ϕx
and similarly for π 2 and Π 2 . Those maps furthermore satisfy a universal property making formal the intuition of a "generalized intersection": (S ∧ T, Π 1 , Π 2 ) is the pullback of σ : S → A and τ : T → A, meaning that that the above diagram commutes and for each map of event structures α : X → S and β :

X → T satisfying X α,β α Ù Ù β ! ! S ∧ T c Π 1 | | x x x x x x x x x Π 2 4 4 p p p p p p p p p S σ 4 4 p p p p p p p p p T τ | | x x x x x x x x x A there is a unique map α, β : X → S ∧ T such that Π 1 • α, β = α and Π 2 • α, β = β.
To construct α, β , we will need the following lemma stating the precise sense in which maps of event structures reflect the causal order: Lemma 2.13. Let f : A → B be a map of event structures and a, b

∈ A such that {a, b} is consistent. If f (a) ≤ f (b) then a ≤ b. Proof. Since f is a map of event structures, f [b] is down-closed as a configuration of B. Since f (a) ≤ f (b) ∈ f [b] by hypothesis, it follows that f (a) ∈ f [b] and thus f (a) = f (c) for some c ≤ b. Since {a, b} is consistent so is {a, b, c} and local injectivity implies a = c ≤ b as desired.
We can now prove that our construction yields a pullback: Lemma 2.14 (The interaction is a pullback). Let σ : S → A and τ : T → A be maps of event structures. The triple (S ∧ T, Π 1 , Π 2 ) is a pullback for σ and τ .

Proof. We have already noticed that the inner square commutes.

Existence of α, β : Assume we have an event structure X with two maps α : X → S and β :

X → T such that σ • α = τ • β. Let a ∈ X. The bijection (by local injectivity of α, β): ϕ a = {(α a ′ , β a ′ ) | a ′ ≤ X a} : α[a] ≃ β[a]
is secured as a consequence of Lemma 2.13, as a cycle in it would be reflected to X. Define α, β (a) = [(α(a), β(a))] ϕa to be the secured bijection obtained as the down-closure of (α(a), β(a)) inside the canonical order on the graph of ϕ a : it has a maximal event by construction, and thus is an event of S ∧ T . It is a good exercise to check that this function defines a map of event structures; which makes the two triangles commute.

Uniqueness of α, β : Assume we have another map ψ : X → S ∧ T making the two triangles commute. We will check that α, β and ψ have the same action on configurations, which will imply (by Lemma 2.15 below) that they are the same. Let z ∈ C (X). Its image through ψ and α, β are (under the order-isomorphism C (S ∧T ) ∼ = B sec σ,τ ) secured bijections ϕ : x ≃ y and ϕ ′ : x ′ ≃ y ′ . But by commutation of the two triangles in the pullback we must have x = x ′ = α z and y = y ′ = β z, thus ϕ = ϕ ′ (as ϕ is uniquely determined from x, y by local injectivity).

In the proof of uniqueness, we only compared the maps by their action on configurations and deduced they were equal on events. This is justified by the following simple fact, that will be useful later on: Lemma 2.15. Let f, g : A → B be parallel maps of event structures such that for all configuration x ∈ C (A) we have f x = gx. Then f = g.

Proof. Let a ∈ A. Write [a) for the configuration [a]\{a}. By hypothesis we have f [a] = g[a] and f [a) = g[a) as sets, thus {f (a)} = f [a] \ f [a) = g[a] \ g[a) = {g(a)} and hence f (a) = g(a).
2.3. Composition of pre-strategies. Building on our understanding of the interaction of pre-strategies as a pullback, we can now proceed to define the notion of composition, which is of critical importance in particular for the application of our games to semantics of programming languages. For that we need to define what is a pre-strategy σ from game A to game B, and given also

τ from B to C, what is τ ⊙ σ from A to C.
Following Joyal [START_REF] Joyal | Remarques sur la thorie des jeux deux personnes[END_REF], we will define a pre-strategy from A to B to be simply a prestrategy on the composite game A ⊥ B. Let us show how to compose such pre-strategies. From σ : S → A ⊥ B and τ : T → B ⊥ C, we need to build a pre-strategy τ ⊙ σ on the game A ⊥ C. Note that from such a notion of composition we can recover a notion of application when A is the empty event structure 1. As usual in game semantics, composition is defined in two steps: firstly, we construct the interaction of the two strategies as an event structure where the two strategies communicate freely. Secondly, the internal synchronisation steps are hidden away. We will now detail these two steps.

To illustrate them, let B be the game tt + / o ff + of booleans (two conflicting positive events). Consider the following pre-strategies σ and τ respectively playing on 1 ⊥ B 1 and B ⊥ 1 B 2 (where indices are just there to disambiguate otherwise identical copies of B):

ff + 2 tt + 2 tt + 1 / o / o / o / o / o / o / o / o ff + 1 tt - 1 v v / o / o / o / o / o / o / o / o ff - 1 v v (σ) (τ )
The pre-strategy σ performs a nondeterministic choice: it can either play true or false. Likewise, τ computes the negation of a boolean: when Opponent plays true or false on B 1 it answers the negation of that in B 2 . 2.3.1. Interaction. Ignoring the polarities, σ and τ are maps of event structures S → A B and T → B C. They do not play on the same game so it is not possible to make them interact directly. To solve this problem we pad them out with identity maps in order to get pre-strategies on A B C.

Thus we consider σ id C : S C → A B C and id A τ : A T → A B C. Since the identity map on any A accepts all possible behaviour appearing in A, only σ and τ give constraints on A and C respectively. In our example, the interaction is:

ff 2 tt 2 tt 1 v v / o / o / o / o / o / o / o / o / o / o / o / o / o / o / o / o / o / o / o ff 1 v v (σ id C ) ∧ (id A τ )
This interaction will be written τ ⊛ σ : T ⊛ S → A B C. (Note the change of order from (σ id C ) ∧ (id A τ ) to τ ⊛ σ, which reflects the standard notation for composition. In particular, when A = C = 1, σ ∧ τ is the same as τ ⊛ σ.) 2.3.2. Hiding. From τ ⊛ σ : T ⊛ S → A B C we need to obtain a map to A C. For an event p ∈ T ⊛ S we say that it is visible if it maps to A or C, invisible otherwise. Let us write V for the set of visible events of T ⊛ S.

We now obtain the composition by hiding invisible events: formally, T ⊙S = (T ⊛S) ↓ V . The obvious function τ ⊙ σ : T ⊙ S → A C, got as the restriction of τ ⊛ σ, defines a map of event structures. Polarities on T ⊙ S are inherited from those of A ⊥ C to make τ ⊙ σ a pre-strategy on A ⊥ C. In our example this yields the pre-strategy on B (notice the inheritance of conflict -the conflict between ff 2 and tt 2 becomes minimal after hiding):

ff + 2 / o / o / o / o / o / o / o / o / o / o / o tt + 2 τ ⊙ σ
We get back the original nondeterministic boolean -the non-deterministic boolean is invariant under negation. But in what sense is it the same, exactly? 2.3.3. Isomorphisms of pre-strategies. They are not equal (set-theoretically) because the underlying sets are not the same, but they are isomorphic: Definition 2.16 (Isomorphism of pre-strategies). Let σ : S → A and τ : T → A be two pre-strategies on a common game A. An isomorphism between σ and τ is an isomorphism of event structures φ : S ∼ = T commuting with the action on the game:

S σ 1 1 c c c c c c c c φ C C T τ A
In this case, we write φ : σ ∼ = τ or simply σ ∼ = τ when the specific φ does not matter.

Isomorphism is the most precise equivalence that makes sense on pre-strategies: two isomorphic pre-strategies have the same intensional behaviour.

Constructing isomorphisms at the level of events can be sometimes cumbersome especially in the case when the event structures are generated from an order of configurations as is the case for the interaction (Section 2.2). Fortunately, order-isomorphisms between configurations of event structures induce isomorphisms on the event structures (cf. [START_REF] Nielsen | Petri nets, event structures and domains[END_REF]).

Lemma 2.17. Let A and B be event structures. For every order-isomorphism ϕ : C (A) ∼ = C (B) there is a unique isomorphism of event structures φ : A ∼ = B satisfying φ(x) = ϕ(x) for every configuration x ∈ C (A). This induces a bijective correspondence between orderisomorphisms C (A) ∼ = C (B) and isomorphisms of event structures A ∼ = B.

Proof. Since it is an order-isomorphism, ϕ preserves the covering relation on configurations. We define φ through this property: indeed for all a ∈ A we have [a)-⊂[a], therefore ϕ [a)-⊂ϕ [a]; let us write φ a for the event added in this covering. In order to establish that φ is a map of event structures whose image of configurations matches ϕ, the key property will be that for all x-⊂x ∪ {a}, the event added in ϕ x-⊂ϕ(x ∪ {a}) is indeed φ a.

For that, we remark that ϕ preserves commuting squares of coverings of the form:

y 1 -⊂ a 1 z x -⊂ a 2 -⊂ a 1 y 2 -⊂ a 2
in the sense that their images are squares where parallel arrows correspond to the same event. Since ϕ preserves -⊂, the image of the square as above is:

ϕ y 1 -⊂ b ′ 1 ϕ z ϕ x -⊂ b 2 -⊂ b 1 ϕ y 2 -⊂ b ′ 2 If ϕ y 1 = ϕ y 2 then y 1 = y 2 so a 1 = a 2 and a 1 ∈ y 1 , contradicting y 1 a 1 --⊂ . So since ϕ y 1 = ϕ y 2 we have b 2 = b 1 , therefore b 1 = b ′
1 and b 2 = b ′ 2 . Now, by induction on x we prove that φx = ϕx. Clearly ϕ∅ = φ∅ = ∅. Now take x a --⊂ y, and write ϕx b --⊂ ϕy. We have covering diagrams as below:

x a --⊂ y ϕx b --⊂ ϕy . . . -⊂ . . . -⊂ → . . . -⊂ . . . -⊂ [a) a --⊂ -⊂ [a] -⊂ ϕ[a) φa --⊂ -⊂ ϕ[a] -⊂
where the left hand side diagram decomposes into commuting squares of coverings where all horizontal coverings add a. Since those are preserved, it follows that b = φ a. Hence φ y = φ x ∪ { φ a} = ϕ x ∪ {b} = ϕ y.

Obviously it follows that φ preserves configurations. It is also locally injective since x and ϕ x = φ x have the same cardinal (as ϕ preserves coverings). Thus φ is a map of event structures. From Lemma 2.15 it follows that φ and φ -1 are inverses.

Uniqueness is obvious by Lemma 2.15 and the bijective correspondence follows.

It will follow from the developments of Section 4 that up to this notion of isomorphism of pre-strategies, composition is associative: Proposition 2.18. Let σ : S → A ⊥ B, τ : T → B ⊥ C and ρ : U → C ⊥ D be pre-strategies. Then, there is an isomorphism α σ,τ,ρ : (U ⊙ T ) ⊙ S → U ⊙ (T ⊙ S) making the following diagram commute:

(U ⊙ T ) ⊙ S ασ,τ,ρ G G (ρ⊙τ )⊙σ 8 8 x x x x x x x x x x U ⊙ (T ⊙ S) ρ⊙(τ ⊙σ) x x p p p p p p p p p p A ⊥ D
Proof. The isomorphism is constructed in Section 4.3.

To accompany this associative composition, the next section will start by introducing a copycat pre-strategy, that serves as a candidate for an identity. The copycat pre-strategy

c c A : C C A → A ⊥ A
is an asynchronous forwarder : every negative move on one side triggers the corresponding positive move on the other side. It is idempotent, but we will see that it is not an identity: pre-strategies and copycat do not form a category. We will define strategies as those prestrategies for which copycat is an identity, and characterise them concretely.

Strategies

As previously hinted at, pre-strategies currently take little account of polarity, and hence have an unreasonable expressive power: they can for instance constrain the order in which Opponent plays their moves, or prevent them from playing at all. We have encountered just before Section 2.2 a simple example of that: the empty pre-strategy on the game ⊖ with just one negative move. By not acknowledging the ⊖, Player denies Opponent the right to play, even though the game allows it.

One guiding principle for the notion of strategy is that they should form a category, so there should be a copycat strategy, neutral for composition with respect to other strategies. The presence of an identity for composition is of course key to the application of our setting in denotational semantics, which relies on a categorical formalisation, but we argue that there is a more down-to-earth motivation for it. The copycat strategy, to be introduced formally below, acts as an asynchronous forwarder. Accordingly, composing with copycat will eliminate overly synchronous behaviour from pre-strategies. Examples include the prestrategy in the previous paragraph not acknowledging Opponent's move, or a pre-strategy playing on a game ⊕ 1 ⊕ 2 with two independent positive events, which plays the moves ⊕ 1 ⊕ 2 in order. As the moves are independent in the game, the ordering ⊕ 1 ⊕ 2 played by the strategy will not be respected by an asynchronous environment -two successive packets sent on the network might arrive in the other order. These intuitions will be revisited formally via examples after the definition of the copycat pre-strategy.

In this section we will define the copycat (pre)strategy, and then characterise the strategies: those pre-strategies invariant under their composition with copycat. We provide examples of pre-strategies that do not behave well in presence of latency and give two criteria (courtesy and receptivity) that are proved necessary and sufficient for a pre-strategy to be a strategy (Theorem 3.20).

3.1.

Copycat and its action on strategies. On A ⊥ A, each move of A appears twice (with dual polarities). The copycat pre-strategy waits for a negative occurrence to be played and then plays the corresponding positive move. In formal terms, it has the causality (1i, a)

(i, a) for every positive move (i, a) of A ⊥ A. Note that this behaviour corresponds to that of the usual copycat strategy in game semantics.

For instance, on the game W = Click -Done + of an interface where Player (the program) can signal it has finished a long computation or Opponent (the user) can click on the screen, the copycat strategy looks like:

W ⊥ 1 W 2 Click + 1 Click - 2 1 l l r Done - 1 1 D D P Done + 2 ( c c W ) 1
Copycat forwards the negative events from one side to the other: acting as the program on the right and as the user on the left. Even if copycat is a pre-strategy from W to itself, it does not necessarily entail a left-to-right flow of information as can be seen for the event Click, rather from negative to positive. This general construction yields a pre-strategy playing on A ⊥ A for any game A. Definition 3.1 (Copycat). Let A be a game. Define C C A to be the following event structure:

• Events: those of A ⊥ A,

• Causality: the transitive closure of

≤ A ⊥ A ∪{((1 -i, a), (i, a)) | (i, a) + ∈ A ⊥ A} • Consistency: X is consistent in C C A iff its down-closure [X] = {a ∈ C C A | ∃b ∈ X, a ≤ C C A b} is consistent in A ⊥ A.
This makes an event structure and the identity map is a pre-strategy:

Lemma 3.2. For any game A, C C A is an esp (with polarities inherited from A ⊥ A), and the identity map written c c A : C C A → A ⊥ A is a pre-strategy, the copycat pre-strategy.

Proof. We observe that for (i, a), (j,

a ′ ) ∈ C C A , we have (i, a) ≤ C C A (j, a ′ ) iff: • Either, i = j and a ≤ A a ′ ,
• Or, i = j, and there is a ≤ A a ′′ ≤ A a ′ such that pol C C A ((i, a ′′ )) =and (by necessity) pol C C A ((j, a ′′ )) = +. Indeed, this is a transitive relation that contains the generators for ≤ C C A -dually, two events related by the relation above are related by ≤ C C A . The other axioms of event structures follow easily, and it is trivial that c c A : C C A → A ⊥ A is a map of event structures.

Immediate causal links in copycat have a very specific shape:

Lemma 3.3. We have that (i, a) C C A (j, a ′ ) if and only if one of the two following conditions is met:

(1) Either i = j, a A a ′ and either (i, a) is positive in C C A or (j, a ′ ) is negative in C C A .

(2) Or i = j and a = a ′ and (i, a) ∈ C C A is negative.

Proof. It is clear that both conditions imply (i, a) C C A (j, a ′ ). Conversely, we know

≤ C C A is generated by A ⊥ A ∪{((i, a), (1 -i, a) | (i, a) -∈ C C A }.
This means that (i, a) (j, a ′ ) implies either i = j, a = a ′ and (i, a) -∈ C C A (as desired) or i = j and a A a ′ . In this case, if (i, a) is negative and (j, a ′ ) is positive, we have (i, a)

C C A (1 -i, a) < C C A (1 -i, a ′ ) C C A (i, a ′ ) contradicting (i, a) C C A (j, a ′ ). Hence (i, a) is positive.
Copycat acts on pre-strategies on A via composition: σ → c c A ⊙ σ. This action adds latency to pre-strategies: whenever the pre-strategy plays a positive move it has to be forwarded by copycat before being visible. We can now define strategies:

Definition 3.4 (Strategy). A strategy on a game A is a pre-strategy σ : S → A such that c c A ⊙ σ ∼ = σ.
This isomorphism is, in general, not unique: in fact, strategies have in general a nontrivial group of automorphisms. Think, for instance, of the strategy σ : S → B where S has just two conflicting events s / o s ′ , both mapped to tt. This strategy σ has two automorphisms: the identity and the swap on S. Likewise, there are two isomorphisms c c B ⊙ σ ∼ = σ. Despite this, it will follow from our development that if c c A ⊙ σ ∼ = σ, then there is always a canonical such isomorphism that fits in the bicategorical picture of Section 4.

Let us try to understand this definition through examples. Consider first the composi-

tion c c W ⊙ c c W with A = W 1 , B = W 2 and C = W 3 : W ⊥ 1 W 2 W 3 Click + 1 Click 2 1 l l r Click - 3 1 l l r Done - 1 1 D D P Done 2 1 D D P Done + 3 ( c c W ⊛ c c W )
Hiding events in W 2 yields a pre-strategy isomorphic to c c W . The latency can be observed: immediate causal links of the form -+ get delayed in the interaction to - * + where * denotes an invisible event of the interaction. After hiding, the effect disappears here but it is not the case in general. Two situations can appear, calling for two conditions.

3.1.1. Courtesy. Assume we have the pre-strategy σ with event structure Done + Click - on W that forces the user to wait for the computation to be over before allowing them to click. Computing the interaction c c W ⊛ σ with A = 1, B = W 1 and C = W 2 yields:

W 1 W 2 Done 1 1 D D P Done + 2 Click 1 Click - 2 1 l l r After hiding of B = W 1 , c c W ⊙ σ has event structure Click - 2 Done + 2 .
There is no causal link anymore because in the interaction the two events are concurrent. Copycat will allow the user to Click without waiting for σ's constraint: there is no way for σ to impose this particular order of moves. In other terms the causal link is not stable under the latency added by copycat.

As a consequence, for a pre-strategy to be invariant under the action of copycat it must not have immediate causal links of the form + that were not already present in the game. In our setting, playing a move is similar to sending a packet whose sender (Player or Opponent) is given by the polarity. This condition means that unless the protocol (the game) specifies it, there is no way to force Opponent to wait for a Player message before sending their message.

Similar reasoning can be made for immediate causal links --(one cannot control the order in which Opponent sends out messages) and + + (latency can change the order in which independent messages arrive).

A pre-strategy respecting these constraints will be called courteous 2 : Definition 3.5 (Courtesy). A pre-strategy σ : S → A is courteous when for all s, s ′ ∈ S such that s s ′ and (pol(s), pol(s ′ )) = (-, +), then σs σs ′ .

Y 1 Y 2 Y 1 Y 2 o 1 O O O O 1 1 1 1 o - 2 1 1 1 1
o - 2 B q q x j j j j j j j j j j j

f f m o 1 ( c c Y ⊛ σ) ( c c Y ⊛ τ )
After hiding, only o - 2 is left in both cases. The problem with these pre-strategies is that they either duplicate or ignore a negative event -yet as we have seen, copycat acknowledges available negative moves first without depending on the pre-strategy's behaviour. Strategies must therefore have the same behaviour regarding the negative events as copycat: to accept them as soon as they are enabled in the current state of the game, and play them once. Such pre-strategies will be called receptive: 2 This condition was called innocence in [START_REF] Rideau | Concurrent strategies[END_REF]. Courtesy is preferred here to avoid the misleading collision with innocence in the sense of Hyland and Ong [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF].

For readers familiar with game semantics, it might be helpful to note that in standard games models receptivity is always present in one way or another. It is explicit and named contingent completeness in [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF], but most of the time it is hard-wired in by asking that strategies contain only plays of even length (Opponent extensions being always present, they bring no additional information).

3.2. The characterisation of strategies -overview of the proof. At this point, the main definitions for the framework are in place. The main element which is missing, is the fact that for a pre-strategy σ : S → A, it is equivalent to be a strategy (in the sense of Definition 3.4), and to be receptive and courteous -which was the main result of [START_REF] Rideau | Concurrent strategies[END_REF]. The rest of this section is devoted to proving this result, stated in Theorem 3.20. In this paper we give a different proof than the one developed in [START_REF] Rideau | Concurrent strategies[END_REF]. Our new proof is more high-level and modular, and sets up the stage better for extensions of the framework in future papers. The rest of the section is quite technical, and may be skimmed through in a first reading of the paper. We start by giving a high-level overview of the proof.

According to Definition 3.4, σ : S → A is a strategy if c c A ⊙ σ ∼ = σ. By Lemma 2.17, that means that there is a order-isomorphism

C (S) ∼ = C (C C A ⊙ S)
commuting with the projection to A. In order to characterise the existence of such an isomorphism, we need to study configurations of C C A ⊙ S for any pre-strategy σ : S → A. This will be done is several steps.

Decomposing interactions. Taking z ∈ C (C C A ⊙ S), we have its minimal witness [z] ∈ C (C C A ⊛ S)

. By Lemma 2.12, [z] corresponds to a secured bijection:

ϕ [z] : x ≃ y with x = x S x A ∈ C (S A) and y = y A ⊥ y A ∈ C (C C A ) such that σ x S = y A ⊥ and
x A = y A -in fact, as remarked below Lemma 2.12, by local injectivity, ϕ [z] (and so [z]) is determined by such x and y, i.e., by x S and y A .

We write Ψ([z]) = (x S , y A ) ∈ C (S) × C (A) for this pair, which satisfies that x S ∈ C (S) and σx S y A ∈ C (C C A ). Reciprocally (by Lemma 2.12) any such pair induces a configuration of C C A ⊛ S provided the corresponding bijection is secured -but that is always the case, as we will see; so Ψ is an iso. We will also characterise such pairs which, through Ψ, correspond to an interaction whose maximal elements are visible (i.e. a minimal witness of a configuration of C C A ⊙ S). This will yield a complete description of configurations of C C A ⊙ S in terms of certain pairs of configurations (x, y) ∈ C (S) × C (A) (step #1).

For z ∈ C (C C A ⊛ S) and Ψ(z) = (x S , x A ), one may regard x A as a not completely updated version of σ x S : some negative events of x A may not have made their way to σ x S , and reciprocally.

(W 1 W 2 ) (W 1 W 2 ) Done 1 6 6 D Click - 1 Done + 2 Done 2 8 G G T f f f f f f f f f f f f f f f f f f 1
Here, we have Ψ(z) = ({Done + 1 , Done + 2 }, {Click - 1 , Done + 2 }). In the example above, we observe two phenomena: the event Click - 1 is played on the right hand side but not forwarded to the left hand side, and the event Done + 1 is played on the left hand side but not forwarded to the right hand side. In general, with Ψ(z) = (x S , x A ), the constraint that σ x S x A ∈ C (C C A ) means that σ x S has less negative events and more positive events than x A , i.e.

x A ⊇ -x A ∩ (σ x S ) ⊆ + σ x S
This relation x ⊇ -⊆ + y is in fact a partial order on C (A) called the Scott order [START_REF] Winskel | Strategies as profunctors[END_REF], and written ⊑ A . It will yield (step #2) a characterisation of configurations of copycat as pairs (

x S , x A ) ∈ C (S) × C (A) such that x A ⊑ A σ x S .
To summarise, after steps #1 and #2, we will have achieved an equivalent description of interactions z ∈ C (C C A ⊛S) as the data of (x S , x A ) ∈ C (S)×C (A) such that x A ⊑ A σ x S , i.e. as diagrams:

x S σ

x A ⊑ A σ x S whose projection to the game via c c A ⊛ σ : C C A ⊛ S → A A is σ x S x A , where only x A will be visible after hiding. We now try to produce an isomorphism between configurations of C C A ⊛ S that are minimal witnesses of configurations of C C A ⊙ S (those whose maximal events are visible), and configurations of S. We will build transformations of configurations in the two directions.

The isomorphism.

Constructing the left-to-right part of the isomorphism C C A ⊙ S ∼ = S, we need to associate to any representation of an interaction (x S , x A ) ∈ C (S) × C (A) as above, some x ′ S ∈ C (S) mapping to x A via σ. Diagrammatically:

x S σ x A ⊑ A σ x S =⇒ ∃x ′ S σ x S σ x A ⊑ A σ x S
In fact, it will turn out that x ′ S ⊑ S x S , and (for the correspondence to be an iso) that its choice is unique. In other words, we will extract x ′ S by proving that strategies are discrete fibrations, as in Definition 3.12 (step #3).

We now focus on the right-to-left part of the construction. From x ∈ C (S), we need to provide some configuration of C C A ⊙S; so we need to provide a witness in C (C C A ⊛S). As we have seen, via Ψ we are looking for a pair (x S , x A ) such that x A ⊑ A σ x S . Note that x A is determined by the requirement that σ x = x A . From that it seems that the pair (x, x A ) does the trick: we do indeed have z = Ψ -1 (x, x A ) ∈ C (C C A ⊛ S) -and restricting it to its visible events yields the desired configuration of C C A ⊙ S. However, it will be useful in proving the isomorphism to have the minimal interaction -the minimal witness -corresponding to this configuration of the composition through hiding. The interaction Ψ -1 (x, x A ) is not always minimal:

Example 3.8. Consider σ : S → W with S comprising only one event s mapped to Click - 1 . Following the paragraph above, its configuration {s} leads to an interaction with copycat corresponding to ({s}, {Click - 1 }), represented as:

W W Click 1 Click - 1 1 l l r
Disposing of the left hand side Click 1 yields a smaller interaction witnessing the same configuration of the composition, as it is maximal and not visible.

In fact, for x ∈ C (S) there is a unique x * ⊆ x such that (x * , σ x) yields the same configuration of the composition as (x, σ x), and such that the maximal events of the represented interaction are all visible. As we will see x * is obtained from x as above, by removing maximal negative events (step #4). From this uniqueness property and the discrete fibration property, it follows that these constructions are inverses of each other.

Necessity.

From the above, we know that strategies, as discrete fibrations, compose well with copycat. It remains to show the converse: that strategies which compose well with copycat are discrete fibrations. In other words, we need to show that strategies of the form c c A ⊙ σ are always discrete fibrations. That will be a direct verification, once we have characterised the Scott order on C C A ⊙ S (step #5).

3.3.

Proof of the characterisation of strategies. Now, we detail and prove all the steps mentioned above.

3.3.1.

Step #1: Composition witnesses as pairs. We start by showing that there are no possible causal loops in an interaction with copycat, so that such interactions are entirely characterised by matching pairs of configurations. In fact we prove a slight generalisation. Lemma 3.9 (Deadlock-free lemma). Let τ : T → A ⊥ B be a pre-strategy such that if t ≤ t ′ and both t and t ′ are sent by τ to the component A ⊥ , then τ t ≤ τ t ′ . Then, given a pre-strategy σ : S → A, and configurations x of S and y of T with σx z = τ y for some configuration z of B , the induced bijection x z ≃ y is secured.

As a consequence, we have an order isomorphism:

C (T ⊛ S) ∼ = {(x, y) ∈ C (S) × C (T ) | σx z = τ y for some z in C (B)}
Proof. Assume that the bijection is not secured. Without loss of generality, there is a causal loop of the form (v 1 , t 1 ) ⊳ . . . ⊳ (v 2n , t 2n ) such that t 2i < t 2i+1 and v 2i+1 < v 2i+2 and t 2n < t 1 . Note that v i ∈ S B for every i.

Assume that v 2i+1 ∈ B. Then v 2i+2 ∈ B and we have that τ (t 2i+1 ) = v 2i+1 ≤ v 2i+2 = τ (t 2i+2 ). Hence by Lemma 2.13, it follows that t 2i+1 ≤ t 2i+2 . If the only two steps of the causal loop were (v 2i+1 , t 2i+1 ) and (v 2i , t 2i ), we have a loop in T and a contradiction. Otherwise, we can remove the steps 2i+1 and 2i+2 and keep a causal loop. Removing them, if there is a loop of length one remaining, then we have a direct contradiction (i.e. t 1 < t 1 ).

Otherwise without loss of generality we can assume v i ∈ S for every i. In this case, by hypothesis on τ we have that t 2i < t 2i+1 implies that σv 2i = τ t 2i < τ t 2i+1 = σv 2i+1 . By Lemma 2.13 again, it follows that v 1 < . . . < v 1 -a contradiction.

This establishes that the bijection induced by any pair of synchronized configurations (w, y) is secured and thus is a configuration of the interaction. We conclude with the sequence of order-isos:

C (T ⊛ S) ∼ = {ϕ : w ≃ y secured | w ∈ C (S B), y ∈ C (T ) such that τ y = (σ B) w} ∼ = {ϕ : w ≃ y | w ∈ C (S B), y ∈ C (T ) such that τ y = (σ B) w} ∼ = {(x z, y) ∈ C (S B) × C (T ) | σx z = τ y} ∼ = {(x, y) ∈ C (S) × C (T ) | σx z = τ y for some z in C (B)}
Let σ : S → A be pre-strategy. The previous lemma, instantiated with τ = c c A , gives an order-isomorphism:

Ψ σ : C (C C A ⊛ S) ∼ = {(x, y 1 y 2 ) ∈ C (S) × C (C C A ) | σx = y 1 } ∼ = {(x, y) ∈ C (S) × C (A) | σx y ∈ C (C C A )}
Every such pair represents an interaction, which gives through hiding a configuration of C C A ⊙ S. However, many interactions correspond to the same configuration of the composition. In fact, as we have seen in Section 2.3, configurations of C C A ⊙ S bijectively correspond to interactions in C C A ⊛ S whose maximal events are visible. We now characterise them.

Lemma 3.10. Let ϕ : x y ≃ σx y be a secured bijection corresponding to a configuration of C C A ⊛ S. The following are equivalent:

(i) All maximal events of ϕ are visible (ii) Every maximal event s of x is positive and σs ∈ y. Moreover, in this case, if σ is courteous, we have σx ⊆ -y.

Proof. (i) ⇒ (ii). Let s ∈ x be a maximal event. The event c = ((0, s), (0, σs)) is not visible in ϕ. Hence it is not maximal: there exists c ′ ∈ ϕ such that c ϕ c ′ . By Lemma 2.10, there are two cases:

• Either π 1 c S A π 1 c ′ , i.e. c ′ = ((0, s ′ ), (0, σs ′ )) and s x s ′ : this is absurd as s is maximal in x. • Or π 2 c C C A π 2 c ′ : by Lemma 3.3, there are two possibilities. The first one is that c ′ = ((0, s ′ ), (0, σs ′ )): absurd, as it would entail σs σs ′ and s < s ′ by Lemma 2.13 contradicting maximality. The second one is that c ′ = ((1, σs), (1, σs)).

This means that (1, σs) is positive in C C A , i.e. s is positive, and moreover (1, σs) ∈ σx y so σs ∈ y. (ii) ⇒ (i). Let c be a maximal event of ϕ and assume it is not visible. It is then of the form c = ((0, s), (0, σs)). If s x s ′ then c < ϕ ((0, s ′ ), (0, σs ′ )) which is absurd so s must be maximal in x. By assumption s is positive and σs ∈ y. Then we have (0, σs) C C A (1, σs) so c < ϕ ((1, σs), (1, σs)) which contradicts the maximality of c.

Finally, assume σ is courteous. We prove that maximal events of σx are included in y. Take σs ∈ σx a maximal event. If s is negative then (0, σ s) is positive in A ⊥ A.

Therefore we have (1, σs) ≤ C C A (0, σs). Since σx y ∈ C (C C A ), we are done. Otherwise, if s is positive it has to be maximal in x: indeed if we had s + x s ′ , by courtesy σs σx σs ′ would follow contradicting the maximality of σs. Then we can conclude by assumption: σs ∈ y as desired.

Summarizing step #1, we now know that configurations of C C A ⊙ S correspond, in an order-preserving and order-reflecting way, to pairs of configurations (x, y) ∈ C (S) × C (A), such that σ x y ∈ C (C C A ), and such that the maximal events of x are positive and also appear in y.

Now, we study the requirement that σ x y ∈ C (C C A ).

3.3.2.

Step #2: The Scott order. As observed before, for x, y ∈ C (A), y x ∈ C (C C A ) whenever y has more positive events and less negative events than x. More precisely:

Lemma 3.11 (Scott order). Let x, y ∈ C (A). The following are equivalent:

(i) y x ∈ C (C C A ) (ii) x ⊇ -(x ∩
y) ⊆ + y (where x ⊆ + y means that x ⊆ y and pol(y \ x) ⊆ {+} and similarly for x ⊇ -y) (iii) there exists z ∈ C (A) such that x ⊇ -z ⊆ + y. In this case we write x ⊑ A y: this is an order called the Scott order of A.

Proof. (i) ⇒ (ii). We show x ∩ y ⊆ + y; the other inclusion is similar. Let a -∈ y, we must show it is in x. Since (0, a) ∈ A ⊥ A is positive, we have (1, a) < C C A (0, a). The down-closure of y x implies that (1, a) ∈ y x as a ∈ y. This exactly means that a ∈ x as desired.

(ii) ⇒ (iii). clear. (iii) ⇒ (i). Assume we have x ⊇ -z ⊆ + y. The set y x is clearly consistent so we need only prove it is down-closed. Since x and y are already down-closed in A, we need only to check for the additional immediate causal links. Assume we have (1, a + ) ∈ y x (so a ∈ x). By hypothesis we have a ∈ z because it is positive. Since z ⊆ y we deduce a ∈ y that is (0, a) ∈ y x as desired. The case (0, a -) ∈ y x is similar.

It is an order. It is clearly reflexive. If x ⊇ -(x ∩ y) ⊆ + y and y ⊇ -(x ∩ y) ⊆ + x, it follows that x \ x ∩ y has to be empty thus x = x ∩ y = y.

For transitivity assume x ⊇ -(x ∩ y) ⊆ + y ⊇ -(y ∩ z) ⊆ + z. Then if a ∈ x \ z, there are two cases. If a ∈ y, then since a ∈ y ∩ z, from y ∩ z ⊆ -y we know that a is negative. If a ∈ y, then by x ∩ y ⊆ -x it must be negative. Thus x ⊇ -(x ∩ z) as desired -the other inclusion is similar. If x ⊑ A y then intuitively y has more output for less input. This is analogous to, and in special cases coincides with, the order on functions in domain theory; hence the name "Scott order" . In summary, configurations of C C A ⊛ S correspond to pairs (x, y) ∈ C (S) × C (A) with y ⊑ A σx.

3.3.3.

Step #3: Discrete fibrations. Since configurations of C C A ⊛ S can be elegantly expressed using the Scott order, it will be key to our proof that strategies satisfy a discrete fibration property with respect to it. We first recall: Definition 3.12 (Discrete fibration). Let (X, ≤ X ) and (Y, ≤ Y ) be orders and f : X → Y be a monotonic map. It is a discrete fibration when for all x ∈ X, y ∈ Y such that y ≤ Y f x there exists a unique x ′ ≤ X x ∈ X such that f x ′ = y. Now, we prove the following characterisation of courtesy and receptivity. Lemma 3.13. Let σ : S → A be a pre-strategy. The following are equivalent:

(i) σ is courteous and receptive, (ii

) σ : (C (S), ⊇ -) → (C (A), ⊇ -) and σ : (C (S), ⊆ + ) → (C (A), ⊆ + ) are discrete fibrations, (iii) σ : (C (S), ⊑ S ) → (C (A), ⊑ A ) is a discrete fibration. Proof. • (iii) ⇒ (ii) is straightforward. • (ii) ⇒ (i): Courtesy. If s + 1
s 2 in S, then by using the discrete fibration property for ⊆ + we prove σs 1 ≤ σs 2 (hence σs 1 σs 2 by Lemma 2.13). Indeed if it is not the case, then σs 1 and σs 2 are concurrent in A -otherwise we would have σs 2 ≤ σs 1 , so s 2 ≤ s 1 by Lemma 2.13, absurd.

Hence σ[s 2 ] \ {σs 1 } is a configuration of A that positively extends to σ[s 2 ]. Thus [s 2 ] should be the positive extension of a configuration x whose image in the game is σ[s 2 ] \ {σs 1 }. By local injectivity, σs 1 = σs 2 , therefore σs 2 ∈ σ[s 2 ] \ {σs 1 }. By local injectivity again, this implies that s 2 ∈ x, so s 1 ∈ x by down-closure, so

σs 1 ∈ σ[s 2 ] \ {σs 1 }, absurd.
If s 1 s - 2 , the only case not already covered by the above is that of s - 1 s - 2 . Assume σ s 1 and σ s 2 are concurrent in A. Set x = [s 2 ] \ {s 1 , s 2 } ∈ C (S). We have σx ⊆ -σx ∪ {σs 2 }, so by existence of the discrete fibration property there is x ⊆ x ∪ {s ′ 2 } ∈ C (S) and σs ′ 2 = σs 2 . But likewise, σ (x ∪ {s ′ 2 }) extends in A with σ s 1 , so by existence of the discrete fibration property there is s ′ 1 such that σ s ′ 1 = σ s 1 and x ∪ {s ′ 1 , s ′ 2 } ∈ C (S). But then by uniqueness of the dicrete fibration property we have x ∪ {s 1 , s 2 } = x ∪ {s ′ 1 , s ′ 2 } so by local injectivity s 1 = s ′ 1 and

s 2 = s ′ 2 , contradicting s 1 s 2 since x ∪ {s ′ 2 } ∈ C (S)
. Receptivity. This is just an instance of the fibration property for ⊇ -for atomic extensions.

• (i) ⇒ (iii): Let x ∈ C (S) and y ∈ C (A) such that y ⊑ σx.

Uniqueness. We prove by induction on the cardinal of y ∈ C (A), that for all x 1 , x 2 ∈ C (S), if x i ⊑ x and σx i = y, then x 1 = x 2 . Assume the result for all y ′ ∈ C (A) strictly smaller than a fixed y ∈ C (A).

First, we prove that x 1 and x 2 have the same positive events. Indeed if s 1 ∈ x 1 is positive, then by σx 1 = y = σx 2 there is a (unique) s 2 ∈ x 2 such that σs 1 = σs 2 . Since x i ⊑ x, s 1 and s 2 are in x, and by local injectivity implies s 1 = s 2 .

If all maximal events of x 1 and x 2 are positive, we are done by down-closure. Otherwise one of them has a negative maximal event, say wlog. s 1 ∈ x 1 . Since σx 1 = σx 2 there is a unique s 2 ∈ x 2 such that σs 1 = σs 2 .

If there exists s ′ 2 ∈ x 2 with s 2 s ′ 2 , since σs 2 is maximal in σx 1 = σx 2 (from Lemma 2.13, σ reflects causality), by courtesy we must have s ′ 2 positive, and hence s ′ 2 ∈ x 1 . It follows that s 1 , s 2 are consistent (both in x 1 ). Hence s 1 = s 2 , and s 1 s ′ 2 ∈ x 1 , which is absurd. Therefore s 2 is maximal in x 2 . This entails that x 1 \ {s 1 } and x 2 \ {s 2 } are configurations of S to which we can apply the induction hypothesis for the smaller y ′ := y \ {σs 1 }: the configurations x 1 \ {s 1 } and x 2 \ {s 2 } must be equal. Since σs 1 = σs 2 is a negative extension of σx 1 \ {σs 1 }, by receptivity it follows that s 1 = s 2 .

Existence. By induction on ⊏, the irreflexive version of ⊑ (by splitting it into atomic extensions). If y a + --⊂ σx, write s for the preimage of a in x. If s is not maximal in x, it means that there exists s s ′ in x. By courtesy since s is positive, we have σs σs ′ in σx. Hence a is not maximal in σx which is absurd. If σx a - --⊂ y, it is a consequence of receptivity.

Note that for a pre-strategy σ : S → A it is not equivalent to be receptive and to be a discrete fibration (C (S), ⊇ -) → (C (A), ⊇ -), as demonstrated by the following pre-strategy on the game A = ⊖ 1 ⊖ 2 :

⊖ 2 ⊖ 1 ⊖ 1 / o / o / o v v ⊖ 2 v v
This pre-strategy is receptive but not a discrete fibration for ⊇ -. Indeed, for x = ∅, y = {⊖ 1 , ⊖ 2 } there are two possible matching extensions x ⊆ x ′ . This pre-strategy fails courtesy -the equivalence only holds on courteous pre-strategies.

Putting together the description of configurations of the interaction with copycat of Lemma 3.9, the characterisation of configurations of copycat in Lemma 3.11 and the discrete fibration property above, we get the first direction of the isomorphism between C (S) and C (C C A ⊙ S).

Proposition 3.14. Let σ : S → A be receptive and courteous. The discrete fibration property yields a function:

L σ : C (C C A ⊙ S) → C (S) commuting with the projection to A (i.e. for all x ∈ C (C C A ⊙ S), σ (L σ x) = ( c c A ⊙ σ) x). Proof. Take x ∈ C (C C A ⊙ S), yielding [x] C C A ⊛S ∈ C (C C A ⊛ S).
In turn, we get

Ψ([x] C C A ⊛S ) = (y S , y A ) ∈ C (S) × C (A)
such that y A ⊑ A σ y S . But then, by the discrete fibration property, there is a unique z S ⊑ S y S ∈ C (S) such that σ z S = y A ; and we set L σ (x) = z S .

We still have to prove that L σ preserves inclusion. To establish that, we need first to characterise how the order on C (C C A ⊙ S), and in particular the covering relation, is reflected on interaction witnesses through Ψ. Lemma 3.15. Let x 1 , x 2 ∈ C (C C A ⊙ S) and let (y 1 S , y 1 A ), (y 2 S , y 2 A ) be the representations of minimal witnesses (e.g., (y 1 S , y

1 A ) = Ψ([x 1 ] C C A ⊛S )).
The following are equivalent:

x 1 + --⊂ x 2 in C C A ⊙ S ⇔ y 1 S ⊆ y 2 S & y 1 A + --⊂ y 2 A x 1 - --⊂ x 2 in C C A ⊙ S ⇔ y 1 S = y 2 S & y 1 A - --⊂ y 2 A Proof. Positive extension. Assume x 1 + --⊂ x 2 . Then ( c c A ⊙ σ) x 1 + --⊂ ( c c A ⊙ σ) x 2 implying y 1 A -⊂y 2 A . Moreover, we have [x 1 ] C C A ⊛S ⊆ [x 2 ] C C A ⊛S implying y 1 S ⊆ y 2 S .

Conversely, we have y 1

A ⊑ A y 2 A ⊑ A σy 2 S by hypothesis. Hence (y 2 S , y 1 A ) ∈ Ψ(C C A ⊛ S). Writing ⊆ 0 for extension by invisible events in C C A ⊛ S, we have:

[x 1 ] C C A ⊛S = Ψ -1 (y 1 S , y 1 A ) ⊆ 0 Ψ -1 (y 2 S , y 1 A ) + --⊂ Ψ -1 (y 2 S , y 2 A ) = [x 2 ] C C A ⊛S Hence x 1 + --⊂ x 2 as desired. Negative extension. If x 1 - --⊂ x 2 , then we have y 1 A - --⊂ y 2
A and y 1 S ⊆ y 2 S by the same argument as in the previous equivalence.

Assume there were a s ∈ y 2 S \ y 1 S . Without loss of generality s can be assumed maximal in y 2 S . By Lemma 3.10, s is positive and σs ∈ y 2 A . If we had σ s ∈ y 1 A , then we would have σ s ∈ σ y 1 S as well as y 1 A ⊑ A σ y 1 S ; so s ∈ y 1 S (by local injectivity), absurd. So, s ∈ y 2 A \ y 1 A , contradicting its positivity. Therefore, y 1 S = y 2 S as desired. Conversely, if y 1 S = y 2 S and y 1 A ---⊂ y 2 A then we have this extension in C C A ⊛ S:

[x 1 ] C C A ⊛S = Ψ -1 (y 1 S , y 1 A ) - --⊂ Ψ -1 (y 1 S , y 2 A ) = [x 2 ] C C A ⊛S yielding x 1 - --⊂ x 2 in C C A ⊙ S,
since the event we added is visible.

From that we easily get:

Proposition 3.16. Let, σ : S → A be receptive and courteous, then the function L σ :

C (C C A ⊙ S) → C (S) is monotonic.
Proof. We prove it for coverings. If x 1 , x 2 ∈ C (S) are such that x 1 -⊂x 2 , we write (y 1 S , y

1 A ) = Ψ([x 1 ] C C A ⊛S ) and (y 2 S , y 2 A ) = Ψ([x 2 ] C C A ⊛S )
for the representations of their minimal interaction witnesses.

We distinguish two cases, depending on the polarity of the extension. If x 1 - --⊂ x 2 , then by the lemma above y 1 S = y 2 S and y

1 A - --⊂ y 2 A . It immediately follows that L σ (x 1 ) - --⊂ L σ (x 2 )
by uniqueness of the discrete fibration property. If x 1 + --⊂ x 2 , then y 1 S ⊆ y 2 S and y 1 A + --⊂ y 2 A . But then by Lemma 3.10 we actually have σ y 1 S ⊆ -y 1 A and σ y 2 S ⊆ -y 2 A , from which it follows that y 1 S + --⊂ y 2 S as well. And then again, L σ (x 1 ) + --⊂ L σ (x 2 ) follows directly from uniqueness of the discrete fibration property.

3.3.4.

Step #4: Reconstructing minimal interactions. Reciprocally, from x ∈ C (S), we have seen that the pair (x, σ x) represents a configuration in C C A ⊛ S that gives us a configuration of the composition through hiding. But it might not be the minimal witness, i.e. it might not satisfy the conditions of Lemma 3.10.

In order to prove the desired isomorphism, we need to extract from x a x * such that (x * , σ x) satisfies these conditions. The configuration x * is obtained by stripping all the maximal negative events away from x, as detailed now.

Lemma 3.17. Let x ∈ C (S). There is a unique x * ⊆ x ∈ C (S) such that Ψ -1 (x * , σx) ∈ C (C C A ⊛ S) and all maximal events of Ψ -1 (x * , σx) are visible. Restricting to visible events, this yields a monotonic function

R σ : C (S) → C (C C A ⊙ S) x → (Ψ -1 (x * , σx)) ∩ (C C A ⊙ S)
Proof. Uniqueness. Assume we have two x ′ 1 and x ′ 2 in C (S) satisfying the hypotheses. The configurations Ψ

-1 (x ′ 1 , σx) ∈ C (C C A ⊛ S) and Ψ -1 (x ′ 2 , σx) ∈ C (C C A ⊛ S) correspond to secured bijections: x ′ 1 σx ϕ 1 ≃ σx ′ 1 σx x ′ 2 σx ϕ 2 ≃ σx ′ 2
σx whose maximal events are visible, and σx ⊑ σx ′ 1 , σx ⊑ σx ′ 2 . By Lemma 3.10, the maximal events of x ′ 1 and x ′ 2 are positive. Moreover, we have σx ′ 1 ⊆ -σx. Indeed, we already know that σx ′ 1 ⊇ + • ⊆ -σx, and for a + ∈ σx, we have (0, a) ≤ (1, a) ∈ C C A . So, there is ((0, s), (0, a)) ∈ ϕ 1 . Therefore, a = σs ∈ σx ′ 1 . With these two remarks, it is elementary to check (using x ′ 1 ⊆ x and local injectivity) that x ′ 1 = [x + ], where x + denotes the set of positive events of x -the same reasoning holds for x ′ 2 , and hence

x ′ 1 = x ′ 2 . Existence. Write x * = [x + ] S .
The set x \ x * contains all the negative events of x without any positive event above them, thus we have x * ⊆ -x. Thus σx ⊑ σx * , therefore Ψ -1 (x * , σx) ∈ C (C C A ⊛ S). Maximal events are visible because x * and σx satisfy the condition (ii) of Lemma 3.10.

From the definition of (-) * above, the monotonicity of R σ is clear.

3.3.5.

Step #5: Characterising the Scott order on C (C C A ⊙ S). Using the above, we can prove that indeed receptivity and courtesy are sufficient to be preserved by composition with copycat (proof forthcoming in Theorem 3.20). For necessity, we will prove that strategies obtained by composition with copycat are automatically discrete fibrations. In order to do that, we first need to study the Scott order on C (C C A ⊙ S) (we write V for the set of visible events of C C A ⊛ S, that is, the events of C C A ⊙ S).

As we have seen, configurations of C C A ⊙ S correspond to certain pairs Ψ(z) = (x, y) ∈ C (S) × C (A) where the maximal events of x are positive. Progressing in ⊑ C C A ⊙S means removing some (maximal) negative events from y, and adding some positives to it. The first part is easy, as these events had not been propagated to x yet. However, adding some positives in y might require to replay them first in x, along with their negative dependencies. For instance:

Example 3.18. Consider A = W 1
W 2 and σ playing on A, with event structure Click - 1 Done + 1 and concurrent Click - 2 . The two interactions below are minimal witnesses of (respectively)

x 1 , x 2 ∈ C (C C A ⊙ S), with x 1 ⊑ C C A ⊙S x 2 : W 1 W 2 W 1 W 2 W 1 W 2 W 1 W 2 Click - 1 Click - 2 Click - 1 A q q x i i i i i i i ⊑ Click 1 Done 1 ! 8 8 E Done + 1
We observe that although the visible part progresses w.r.t. the Scott order, the invisible part only gains events, and potentially of both polarities: it progresses w.r.t. plain inclusion.

Formally, we prove the following lemma.

Lemma 3.19. Let z, z ′ ∈ C (C C A ⊙S) and let (x, y), (x ′ , y ′ ) be the respective representations of their minimal witnesses via Ψ. The following are equivalent:

(

1) z ⊑ C C A ⊙S z ′ (2) y ⊑ A y ′ and x ⊆ x ′
Proof. Immediate consequence of Lemma 3.15.

3.3.6.

Step #6: Wrapping up. Having introduced all the tools and lemmas needed for our proof, we now prove the main theorem.

Theorem 3.20. Let σ : S → A be a pre-strategy. The following are equivalent:

(i) σ is a strategy (ii) σ : (C (S), ⊇ -) → (C (A), ⊇ -) and σ : (C (S), ⊆ + ) → (C (A), ⊆ + ) are discrete fibrations, (iii) the map σ : (C (S), ⊑ S ) → (C (A), ⊑ A ) is a discrete fibration (iv) σ is

courteous and receptive

Proof. The equivalence between (ii), (iii), (iv) is proved by Lemma 3.13.

• (i) ⇒ (iii): Let f : σ ∼ = c c A ⊙ σ be an isomorphism of strategies. Let (x, y) ∈ C (S) × C (A) with y ⊑ σx. Write Ψ([f (x)] C C A ⊛S ) = (w, σx) ∈ Ψ(C C A ⊛ S) with w ∈ C (S) and σx ⊑ σw.
Existence. Consider x 0 = [{s ∈ w | σs ∈ y}] * (Lemma 3.17). By definition the maximal events of Ψ -1 (x 0 , y) are all visible. Hence (x 0 , y) corresponds to a configuration z ∈ C (C C A ⊙ S). Applying f -1 we get a configuration x ′ ∈ C (S) whose image by σ is y. Since y ⊑ σx and x 0 ⊆ w, we have by Lemma 3.19, z ⊑ f (x). Hence x ′ ⊑ x (f -1 preserves the Scott order).

Uniqueness. Assume we have two x ′ 1 and x ′ 2 satisfying x ′ i ⊑ x and σx ′ i = y. We have

f (x ′ 1 ) = V ∩ (Ψ(x ′′ 1 , y)) and f (x ′ 2 ) = V ∩ (Ψ(x ′′ 2 , y
)) for some configurations x ′′ 1 and x ′′ 2 . Applying Lemma 3.17 we get

x ′′ 1 = x ′′ 2 which yields f (x ′ 1 ) = f (x ′ 2 ) and then x ′ 1 = x ′ 2 by injectivity of f . • (iii) ⇒ (i): We have constructed two inclusion-preserving maps L σ : C (C C A ⊙ S) → C (S) and R σ : C (S) → C (C C A ⊙ S). By construction, they are inverses -L σ • R σ = id C (S)
by uniqueness of the discrete fibration property, and

R σ • L σ = id C (C C A ⊙S)
by uniqueness of the (-) * operation in Lemma 3.17. By Lemma 2.17, this yields the desired isomorphism between c c A ⊙ σ and σ.

The bicategory of concurrent games

We have developed a notion of concurrent strategies, and characterised those which behave well in an asynchronous, distributed world. For this to serve as a basis for the compositional semantics of concurrent processes or programs, it is of paramount importance to study the categorical structure of strategies, i.e. the algebraic laws satisfied by composition.

Usually -as described first by Joyal on Conway games [Joy77] -composition of strategies yields a category having games as objects, strategies as morphisms and copycat strategies as identities. Here however, we cannot use equality to compare strategies. Indeed, take σ : S → A and σ ′ : S ′ → A two strategies on A. As we have observed in Section 2, comparing them requires us first to relate S and S ′ , which we do via a map f : S → S ′ making the obvious triangle commute. This map is in general not unique: we saw below Definition 3.4 a strategy with two automorphisms.

For many purposes, the exact identity of an isomorphism relating two strategies is irrelevant, and in these cases we can (and later will) quotient to a category. This quotient, and the investigation of its further structure, will be carried out in Section 5. But the un-quotiented structure also matters -when working with our games, one is often led to reason on representatives rather than isomorphism classes (for instance when computing infinite strategies as limits of ω-chains of finite strategies). Similarly, further developments in this framework (beyond this paper) rely on properties of composition that the quotiented category is too rough to convey. So we first investigate the composition operation without quotienting, and show how the specific isomorphisms between strategies fit in the categorical picture. This is the purpose of this section, where we will establish that games, strategies and maps between them form a bicategory. We will first review the definition of a bicategory. Then, we will turn to the construction of our concrete bicategory of concurrent games. 4.1. Bicategories. First, recall that a bicategory C consists of the following basic data (with notations inspired from our concrete bicategory of concurrent games):

• A set of objects, or 0-cells (we use A, B, C, . . . to range over objects).

• For any two objects A, B, a category C(A, B). Its objects are the morphisms or 1-cells of C (we use σ, τ, . . . to range over morphisms, and write e.g. σ : A + G G B), and its morphisms are the 2-cells of C (we range f, g, . . . to range over 2-cells, and write e.g. f : σ ⇒ τ ). • For each object A, a distinguished morphism c c A : A + G G A, called the identity. • For each objects A, B, C, a functor:

⊙ : C(B, C) × C(A, B) → C(A, C)
The functor ⊙ gives the composition τ ⊙σ : A + G G C of 1-cells σ : A + G G B and τ : B + G G C, but its functorial action also allows us to transport 2-cells alongside compositions. For instance, if f : σ ⇒ σ ′ , then τ ⊙ f : τ ⊙ σ ⇒ τ ⊙ σ ′ (A consequence of that is that isomorphism of 1-cells is a congruence, i.e. is preserved under composition).

But that is not all. In a bicategory, the associativity of ⊙ and neutrality of c c A do not in general hold in the strict sense (or we would have a 2-category), but only up to coherent isomorphisms. This means that we have the following isomorphisms:

• For any σ : A + G G B, τ : B + G G C, ρ : C + G G D, an isomorphism (the associator ):

α σ,τ,ρ : (ρ ⊙ τ ) ⊙ σ ⇒ ρ ⊙ (τ ⊙ σ)
natural in σ, ρ and τ . • For any σ : A + G G B, two isomorphisms (the unitors):

ρ σ : σ ⊙ c c A ⇒ σ λ σ : c c B ⊙ σ ⇒ σ natural in σ.
Finally, these data need to satisfy some coherence conditions: the associators are subject to Mac Lane's pentagon identity whereas the unitors must satisfy the triangle identity (those are the same as in a monoidal category). We do not recall them now, but we will state them in the course of the construction of our concrete bicategory.

We now go on to construct our concrete bicategory. We gave the definition of a bicategory in two steps: first what we called the basic data, and then natural isomorphisms for associativity and unities, subject to coherence conditions. Our construction of the concrete bicategory will follow the same lines.

4.2. Basic data of the bicategory CG. As expected, the objects of CG are the games, and the morphisms from A to B are the strategies σ : S → A ⊥ B. As in the definition above we will occasionally write σ : A + G G B, keeping the S anonymous.

For σ : S → A ⊥ B, τ : T → B ⊥ C, a 2-cell f : σ ⇒ τ is a map of esps f : S → T making the following triangle commute:

S f C C σ 5 5 r r r r r r T τ { { v v v v v v A ⊥ B
Such 2-cells can be composed as functions, and for σ : S → A ⊥ B the identity id S : S → S is a valid 2-cell id σ : σ ⇒ σ. Therefore, for any two games A and B we get a category CG(A, B) as required by the definition. 4.2.1. Functorial composition. Now, we need a functor:

⊙ : CG(B, C) × CG(A, B) → CG(A, C)
For τ : B + G G C and σ : A + G G B, its action is the composition τ ⊙ σ as in Section 2. This operation was defined on pre-strategies rather than strategies, so we note in passing: Proposition 4.1. For σ : S → A ⊥ B and τ : T → B ⊥ C strategies, τ ⊙ σ is a strategy.

Proof. We use the second formulation of the definition of strategies, as in Theorem 3.20.

Negative fibration. Take So composition, despite being defined on pre-strategies rather than strategies, preserves courtesy and receptivity -it is well-defined on 1-cells of our bicategory. We now need to prove that it is well-defined on 2-cells as well. In fact, we will show that it is well-defined on morphisms between arbitrary pre-strategies, not only those that are receptive and courteous. Until Section 4.4 (where we study compositions with copycat), the development will use neither receptivity nor courtesy.

x ∈ C (T ⊙ S) such that (τ ⊙ σ)(x) ⊆ -x ′ A x ′ C for some x ′ A x ′ C ∈ C (A ⊥ C).
Let σ : S → A ⊥ B, σ ′ : S ′ → A ⊥ B and τ : T → B ⊥ C be pre-strategies, and f : S → S ′ be a morphism from σ to σ ′ . We proved in Lemma 2.14 that the interaction T ⊛S was the pullback of σ C and A τ . By the corresponding universal property, it follows that there is a unique map f ⊛ T : S ⊛ T → S ′ ⊛ T making the required diagrams commute. In particular, this remark establishes that the interaction operation -⊛is functorial in morphisms between pre-strategies. In order for ⊙ to inherit this, it is convenient to use that ⊛ and ⊙ are related by a universal property involving partial maps: Definition 4.2. A partial map of es(p)s f : E ⇀ F is a partial function, such that for all x ∈ C (E) we have f x ∈ C (F ), and such that for all e 1 , e 2 ∈ x ∈ C (E), if f e 1 = f e 2 (with both defined), then e 1 = e 2 .

A key example of a partial map in our setting, is the hiding map: given an es(p) E and V ⊆ E, there is a partial map:

h : E ⇀ E ↓ V acting as the identity on V and undefined otherwise. So in particular, for pre-strategies σ : S → A ⊥ B and τ : T → B ⊥ C, there is a partial map:

h : T ⊛ S ⇀ T ⊙ S.
Projection and hiding provide a partial-total factorization system, which obeys: Lemma 4.3. Let f : E ⇀ F be a partial map of es(p)s, and V be the subset of events of E on which f is defined. Then, f factors as (f ↾ V ) • h (where f ↾ V : E ↓ V → F is total). Moreover, for any other factorisation f = g 2 • g 1 with g 1 : E ⇀ X and g 2 : X → F , there is a unique total h :

E ↓ V → X such that h • h = g 1 and g 2 • h = f ↾ V , as pictured in the diagram below: E h g 1 4 p p p p p p p p p f 1 ¢ ¦ ! & 1 6 A F Q V È ↓ V f ↾V h G G X g 2 | | x x x x x x x x x

F

We say that h : E ⇀ E ↓ V has the partial-total universal property.

Proof. Direct verification.

From that, it is easy to construct the functorial action of ⊙. Take σ, σ ′ , τ and f as above. As explained, we obtain T ⊛ f : T ⊛ S → T ⊛ S ′ by the universal property of the interaction pullback.

But by Lemma 4.3, the two maps h σ,τ : T ⊛ S ⇀ T ⊙ S and h σ ′ ,τ : T ⊛ S ′ ⇀ T ⊙ S ′ have the partial-total universal property. Using it, we get a unique map T ⊙ f : T ⊙ S → T ⊙ S ′ matching T ⊛ f up to hiding. It is straightforward from the universal properties that this operation is functorial, that its symmetric counterparts g ⊛ S and g ⊙ S are as well and that they satisfy the interchange laws, yielding the required bifunctor.

In fact we note in passing that ⊙ preserves more general notions of morphisms of pre-strategies, that do not leave the game invariant: Lemma 4.4. Consider two commuting diagrams between pre-strategies (using the obvious functorial action of (-) ⊥ and -in EP):

S 1 f G G σ 1 S 2 σ 2 A ⊥ 1 B 1 h ⊥ 1 h 2 G G A ⊥ 2 B 2 T 1 g G G τ 1 T 2 τ 2 B ⊥ 1 C 1 h ⊥ 2 h 3 G G B ⊥ 2 C 2
Then, the following diagram commutes.

T 1 ⊙ S 1 g⊙f G G τ 1 ⊙σ 1 T 2 ⊙ S 2 τ 2 ⊙σ 2 A ⊥ 1 C 1 h ⊥ 1 h 3 G G A ⊥ 2 C 2
Proof. For interactions first, the map g ⊛ f : T 1 ⊛ S 1 → T 2 ⊛ S 2 is defined from the universal property of the pullback for T 2 ⊛ S 2 , using the two commuting diagrams in the hypothesis. It follows by definition that the diagram

T 1 ⊛ S 1 g⊛f G G τ 1 ⊛σ 1 T 2 ⊛ S 2 τ 2 ⊛σ 2 A 1 B 1 C 1 h 1 h 2 h 3 G G A 2 B 2 C 2 commutes. The map g ⊙ f : T 1 ⊙ S 1 → T 2 ⊙ S 2
and the required diagram commutation follow from the partial-total universal property. 4.3. Associators. We now define the associator, i.e. for every three strategies σ :

A + G G B, τ : B + G G C, ρ : C + G G D, an isomorphism α σ,τ,ρ : (ρ ⊙ τ ) ⊙ σ ⇒ ρ ⊙ (τ ⊙ σ)
natural in σ, τ, ρ, and subject to Mac Lane's pentagon (detailed in the development below). We will start with the definition of the associator.

The hiding witness assigns, to any x ∈ C (F ), a canonical witness wit f (x) ∈ C (E), that projects back to x through f . The hiding witnesses give a configuration-based version of projection -or of the partial-total factorization, as established by the lemma below.

Proposition 4.6. Let f : E ⇀ F be a partial map. Then, the three following propositions are equivalent:

(i) There exists an isomorphism ϕ : E ↓ V ∼ = F such that ϕ • h = f (where V is the domain of definition of f -note that ϕ is necessarily f restricted to V ), (ii) f has the partial-total universal property, (iii) f has a hiding witness. We call hiding maps any partial maps satisfying those properties. Note that by (i) it follows that in any hiding map f is partial rigid, i.e. for any e 1 ≤ e 2 , if f (e 1 ), f (e 2 ) defined then f (e 1 ) ≤ f (e 2 ).

Proof. (i) ⇔ (ii). From left to right, we transport through ϕ the partial-total universal property of Lemma 4.3. From right to left, we use the fact that both h : E ⇀ E ↓ V and f : E ⇀ F have the partial-total universal property, yielding the desired isomorphism.

(ii) ⇒ (iii). W.l.o.g., we prove it for h :

E ⇀ E ↓ V . For x ∈ C (E ↓ V ), define wit(x) = [x] ∈ C (E). Clearly, h(wit(x)) = [x] ∩ V = x and wit(h(x)) = [x ∩ V ] ⊆ x
as required, and it preserves union by definition.

(iii) ⇒ (i). We construct the isomorphism on configurations:

p : C (E ↓ V ) → C (F ) x → f ([x]) q : C (F ) → C (E ↓ V ) y → wit(y) ∩ V
It is clear by definition that these maps are monotonic, we need to prove that they are inverses of each other. For one direction, for all y ∈ C (F ), since wit(y) ∈ C (E) it is downclosed in E and thus can only differ from [wit(y) ∩ V ] ∈ C (E) with events not in V , so f ([wit(y) ∩ V ]) = f (wit(y)) = y, i.e. p • q(y) = y.

For the other direction, we note first that if x ∈ C (E) has all its maximal events in V , then wit(f (x)) = x. Indeed, we have wit(f (x)) ⊆ x by hypothesis. But both sides map to f (x) via f , inducing by local injectivity bijections wit

(f (x)) ∩ V ≃ f (x) and x ∩ V ≃ f (x). It follows that wit(f (x)) ∩ V = x ∩ V . But x = [x ∩ V ]
since its maximal elements are visible. Putting everything together:

x = [x ∩ V ] = [wit(f (x)) ∩ V ] ⊆ wit(f (x)) ⊆ x So x = wit(f (x))
. Turning back to our main proof, we need to show that q • p(x) = x for x ∈ C (E ↓ V ), i.e. that wit(f ([x])) ∩ V = x. But by definition, [x] has its maximal events in V , so wit(f ([x])) = [x]. So we are left to prove that [x] ∩ V = x, which is clear.

So we have constructed an order-isomorphism between the domains of configurations of E ↓ V and F , which yields an isomorphism by Lemma 2.17. Finally, the required equality is obvious by Lemma 2.15. 4.3.3. Associators for composition. The third formulation of hiding maps enables us to combine them in several ways. Firstly, they are stable under composition: Lemma 4.7. Let h : E 1 ⇀ E 2 and h ′ : E 2 ⇀ E 3 be hiding maps, then h ′ • h : E 1 ⇀ E 3 is a hiding map as well.

Proof. Obvious, by composing the hiding witnesses.

We can also combine hiding maps "horizontally", using the universal property of the interaction. For that though, we need first to prove that this universal property applies to partial maps.

Lemma 4.8. A pullback square in E is also a pullback square in the category E ⊥ having event structures as objects, and partial maps as morphisms.

Proof. The proof is summarized in the following diagram:

X h f 1 f 2 X ↓ V f ′ 1 Ù Ù f ′ 2 ! ! g P c z z v v v v v v v 6 6 r r r r r r r A 6 6 r r r r r r r B z z v v v v v v v
C Take f 1 , f 2 partial maps such that the outer square commutes. Necessarily, f 1 and f 2 are defined on the same subset of events of X; call it V . By Lemma 4.3, h : X ⇀ X ↓ V satisfies the partial-total universal property. By the universal property of the pullback in E, there exists a unique g : X ↓ V → P making the triangle commutes, yielding a factorization g • h : X ⇀ P . Uniqueness follows directly from the uniqueness of the pullback and of the partial-total universal property. Therefore, we can use the universal property of the interaction pullback to manipulate and compose hiding maps. This allows us to state and prove the lemma below, which plays a similar role to the zipping lemma used in proving associativity of composition in sequential games -hence the name. Lemma 4.9 (Zipping lemma). Let h : S ⇀ S ′ be a hiding map making the following diagram commute:

S h G σ S ′ σ ′ A B C A ⊥ C G A C
Then, for ρ : U → C D, the morphism U ⊛ h : U ⊛ S ⇀ U ⊛ S ′ defined using the universal property of U ⊛ S ′ via Lemma 4.8 is a hiding map.

Proof. We show that U ⊛ h has a hiding witness. A configuration of U ⊛ S ′ corresponds to configurations x S ′ x D and x A x U of the event structures as annotated, such that:

σ ′ x S ′ = x A x C ρx U = x C x D
and such that the induced bijection between x S ′ x D and x A x U is secured.

From that, we consider wit h (x S ′ ) x D and x A x B x U , where x B is obtained by

σ(wit h (x S ′ )) = x A x B x C . By construction we have (σ D)(wit h (x S ′ ) x D ) = (A B ρ)(x A x B x U )
. The induced bijection is secured: a causal loop in it could not stay in (events projected to) B, as the causality on the corresponding pairs is entirely determined by S. So, using that h is partial rigid by Proposition 4.6 it would induce a causal loop in the original bijection, that was supposed secured. All the additional properties to check follow by construction.

At this point, we can define the associator. Recall that for σ : S → A B, τ : T → B C and ρ : U → C D we have the associator at the level of interactions:

a σ,τ,ρ : (U ⊛ T ) ⊛ S → U ⊛ (T ⊛ S)
By using the two lemmas above, we have two hiding maps:

h σ,(τ,ρ) = (U ⊛ T ) ⊛ S hτ,ρ⊛S G (U ⊙ T ) ⊛ S h σ,ρ⊙τ G (U ⊙ T ) ⊙ S h (σ,τ ),ρ = U ⊛ (T ⊛ S) U ⊛hσ,τ U ⊛ (T ⊙ S) h τ ⊙σ,ρ G U ⊙ (T ⊙ S)
From the definitions, it is easy to check that the following outer diagram commutes:

U ⊛ (T ⊛ S) aσ,τ,ρ G G h σ,(τ,ρ) (U ⊛ T ) ⊛ S h (σ,τ ),ρ U ⊙ (T ⊙ S) ασ,τ,ρ G G ρ⊙(τ ⊙σ) @ @ (U ⊙ T ) ⊙ S (ρ⊙τ )⊙σ v v m m m m m m A D
So by the partial-total universal properties of h (σ,τ ),ρ and h σ,(τ,ρ) , a σ,τ,ρ induces a unique isomorphism α σ,τ,ρ : (U ⊙ T ) ⊙ S → U ⊙ (T ⊙ S) making the two sub-diagrams commute. 4.3.4. Naturality and coherence. To conclude the associativity part of the bicategory construction, we need to check that these isomorphisms are natural in σ, τ, ρ and satisfy Mac Lane's pentagon. In both cases, the proof consists in verifying it first for interactions (as we already did earlier from the pentagon), and deducing it for composition by checking that the maps involved in the diagram for composition are canonically related to those for interaction, as above. We skip the details, that can be recovered easily.

Lemma 4.12. Let σ 1 : S

1 → A ⊥ 1 B 1 , σ 2 : S 2 → A ⊥ 2 B 2 , and f : S 1 → S 2 , h : A 1 → A 2 , h ′ : B 1 → B 2 such that the following diagram commutes: S 1 f G G σ 1 S 2 σ 2 A ⊥ 1 B 1 h ⊥ h ′ G G A ⊥ 2 B 2
Then, the following two diagrams commute as well:

A ⊥ 1 B 1 h ⊥ h ′ C C B 1 ⊙ S 1 c c B 1 ⊙σ 1 S S k k k k k k k k k k k k k k k k λσ 1 G G C C h ′ ⊙f S 1 σ 1 Y Y w w w w w w w w w f A ⊥ 2 B 2 C C B 2 ⊙ S 2 c c B 2 ⊙σ 2 S S k k k k k k k k k k k k k k k k λσ 2 G G S 2 σ 2 Y Y w w w w w w w w w A ⊥ 1 B 1 h ⊥ h ′ S 1 ⊙ C C A 1 σ 1 ⊙ c c A 1 S S k k k k k k k k k k k k k k k k ρσ 1 G G f ⊙C C h S 1 σ 1 Y Y w w w w w w w w w f A ⊥ 2 B 2 S 2 ⊙ C C A 2 σ 2 ⊙ c c A 2 S S k k k k k k k k k k k k k k k k ρσ 2 G G S 2 σ 2 Y Y w w w w w w w w w
In particular (when h, h ′ are identities), λ σ and ρ σ are natural in σ.

that it follows that both paths alongside the triangle above map x to (the configuration of T ⊙ S represented by) x S x C and x A x T .

We have finished the proof that CG is a bicategory.

A compact-closed (bi)category

In this section, we show that similarly to Joyal's category of Conway games, our bicategory of concurrent games has a compact closed structure, a structure that is central in the applications of our framework to game semantics of programming languages.

Recall that a compact closed category is a symmetric monoidal category, where each object A has a dual A * , which is related to A via two morphisms:

η A : 1 + G G A * ⊗ A ǫ A : A ⊗ A * + G G 1
where 1 is the unit of the tensor (in our concrete case it is the empty game). These morphisms have to obey two laws that are best represented in the language of string diagrams:

A A η A * ǫ A = = A A ǫ A * η A A A
Compact closed categories play an important role in the background in semantics: the equations of compact closed categories are mirrored, e.g. in the reduction rules of proof nets and in the adjunction laws (β and η-conversion) of cartesian closed or symmetric closed monoidal categories. In fact, any compact closed category is symmetric closed monoidal (more precisely, * -autonomous, and a model of MLL [START_REF] Girard | Linear logic[END_REF]): setting A ⊸ B = A * ⊗ B, we have the adjunction A ⊗ -⊣ A ⊸ -. In short, compact closed categories form the backbone of an equational presentation of the dynamics of linear higher-order computation.

But unlike Conway games, CG is a bicategory. In fact, we believe that it gives an example of a compact closed bicategory, as defined by Kelly [START_REF] Kelly | Many-variable functorial calculus[END_REF] and detailed by Stay [START_REF] Stay | Compact closed bicategories[END_REF]. However, the precise definition of a compact closed bicategory is rather intimidating. It might be possible to deduce the bicategorical compact closed structure of CG from that of the bicategory of profunctors [START_REF] Stay | Compact closed bicategories[END_REF], but we do not do so here. Although in subsequent work we occasionally rely on the algebraic laws for composition pre-quotient, the literature and body of work that we need to connect to when setting up our game semantics (for instance, models of linear logic [START_REF] Melliès | Categorical semantics of linear logic[END_REF]) does not exploit this bicategorical structure. So, we only check that the quotiented category is compact closed.

By abuse of notations, from now on we will use the same notation CG for the quotiented category instead of the bicategory. Regarded as a category, CG has esps as objects, and as morphisms strategies σ : S → A ⊥ B up to isomorphism. In the rest of this section, we check the components of a compact closed category. 5.1. The bifunctor. First, we define a bifunctor ⊗ : CG 2 → CG. On objects, A ⊗ B is simply defined as A B. On morphisms, for σ 1 : S 1 → A ⊥ 1 B 1 and σ 2 : S 2 → A ⊥ 2 B 2 , we define

σ 1 ⊗ σ 2 = S 1 S 2 σ 1 σ 2 G G (A ⊥ 1 B 1 ) (A ⊥ 2 B 2 ) γ A ⊥ 1 ,B 1 ,A ⊥ 2 ,B 2 G G (A 1 A 2 ) ⊥ (B 1 B 2 )
where γ A,B,C,D : (A B) (C D) → (A C) (B D) is the obvious isomorphism of esps. We show that this operation is a bifunctor. Firstly, it preserves the identity. Secondly, it preserves composition.

Proposition 5.2. Let:

σ 1 : S 1 → A ⊥ 1 B 1 τ 1 : T 1 → B ⊥ 1 C 1 σ 2 : S 2 → A ⊥ 2 B 2 τ 2 : T 2 → B ⊥ 2 C 2
Then, (τ 1 ⊙ σ 1 ) ⊗ (τ 2 ⊙ σ 2 ) ∼ = (τ 1 ⊗ τ 2 ) ⊙ (σ 1 ⊗ σ 2 )

Proof. We start by proving it for interactions. As the parallel composition of pullback squares is a pullback square, we have two pullbacks related by isomorphisms:

(T 1 ⊛ S 1 ) (T 2 ⊛ S 2 ) s s g g g g g gg g g g g g gg

C C c (S 1 C 1 ) (S 2 C 2 ) (σ C 1 ) (σ 2 C 2 ) C C γ S 1 ,C 1 ,S 2 ,C 2 { { (A 1 T 1 ) (A 2 T 2 ) (A 1 τ 1 ) (A 2 τ 2 )
s s g g g gg g g g g gg g g g

γ A 1 ,T 2 ,A 2 ,T 2 { { (A 1 B 1 C 1 ) (A 2 B 2 C 2 ) δ { { (T 1 T 2 ) ⊛ (S 1 S 2 )
s s g gg g g g g gg g g g g g

C C c (S 1 S 2 ) (C 1 C 2 ) (σ 1 ⊗σ 2 ) (C 1 C 2 ) C C (A 1 A 2 ) (T 1 T 2 ) (A 1 A 2 ) (τ 1 ⊗τ 2 )
s s g g g g gg g g g g g gg g

(A 1 A 2 ) (B 1 B 2 ) (C 1 C 2 )
where δ is the obvious map. By universal property of the pullback that gives an isomorphism:

γ ′ : (T 1 ⊛ S 1 ) (T 2 ⊛ S 2 ) ∼ = (T 1 T 2 ) ⊛ (S 1 S 2 ) which commutes (up to γ A 1 ,C 1 ,A 2 ,C 2 ) with the hiding maps h σ 1 ,τ 1 h σ 2 ,τ 2 and h σ 1 ⊗σ 2 ,τ 1 ⊗τ 2 , so using Proposition 4.6 and the easy fact that maps with hiding witnesses are stable by parallel composition, it follows that γ ′ corresponds to a unique isomorphism:

(T 1 ⊙ S 1 ) (T 2 ⊙ S 2 ) ∼ = (T 1 T 2 ) ⊙ (S 1 S 2 ) between strategies (τ 1 ⊙ σ 1 ) ⊗ (τ 2 ⊙ σ 2 ) and (τ 1 ⊗ τ 2 ) ⊙ (σ 1 ⊗ σ 2 ).

5.2. Lifting and symmetric monoidal structure of CG. The strategies serving as structural morphisms for the symmetric closed monoidal structure are very simple variants of copycat c c A : A + G G A. In order to construct the symmetric monoidal structure of CG, we describe a systematic way of generating such morphisms from more elementary maps of esps.

Definition 5.3. Let f : A → B be a receptive, courteous map of esps3 . Then, the map:

f : C C A → A ⊥ B a → (A ⊥ f ) • c c A (a)
is a strategy called the lifting of f . Likewise, if f : B ⊥ → A ⊥ is receptive and courteous, we define its co-lifting:

f ⊥ : C C B → A ⊥ B c → (f B) • c c B (c)
The fact that they are strategies follows from the fact that courteous receptive maps are stable under composition.

The following key lemma links composition of strategies with lifted maps and composition of the corresponding maps in E.

Lemma 5.4. Let f : B → C be a receptive courteous map of esps, and σ : S → A ⊥ B be a strategy. Then, the unitor λ σ : C C B ⊙ S → S is an isomorphism between

f ⊙ σ : C C B ⊙ S → A ⊥ C (A ⊥ f ) • σ : S → A ⊥ C
Likewise, for f : B ⊥ → A ⊥ receptive courteous and σ : S → B ⊥ C a strategy, ρ σ is an isomorphism between:

σ ⊙ f ⊥ : S ⊙ C C B → A ⊥ C (f C) • σ : S → A ⊥ C
Proof. By definition, the following two diagrams commute:

S S G G σ S σ A ⊥ B A ⊥ B G G A ⊥ B C C B C C B G G c c B C C B f B ⊥ B B ⊥ f G G B ⊥ C
This concludes the symmetric monoidal structure of CG.

5.3. Compact closed structure. The dual of a game A is simply defined as A ⊥ . We have two strategies: η A : C C A → 1 ⊥ (A ⊥ A) ǫ A : C C A → (A A ⊥ ) ⊥ 1 defined in the obvious way. We have:

Proposition 5.7. The strategies η A : 1 + G G A ⊥ A and ǫ A : A A ⊥ + G G 1 satisfy the laws for a compact closed category.

Proof. We need to check the two equations of duals in compact closed categories:

c c A ∼ = λ A ⊙ (ǫ A ⊗ c c A ) ⊙ α -1 A,A ⊥ ,A ⊙ ( c c A ⊗ η A ) ⊙ ρ A -1 c c A ⊥ ∼ = ρ A ⊥ ⊙ ( c c A ⊥ ⊗ ǫ A ) ⊙ α A ⊥ ,A,A ⊥ ⊙ (η A ⊗ c c A ⊥ ) ⊙ λ A ⊥ -1
These two isomorphisms are symmetric; we only check the first. Let us write σ : S → A ⊥ A for the resulting composition, and

ξ : U → A (A 1) (A (A A)) ((A A) A) (1 A) A
for the corresponding 5-ary composition. By Lemma 4.9, there is a hiding map h : U ⇀ S, commuting with the projection to the game. From the characterisation of configurations of pullbacks, and after eliminating redundancies, configurations of U correspond to the data of a configuration in each component A above, satisfying the following constraints:

A ⊒ 1 (A ⊒ 2 1) (A ⊒ 2 (A ⊒ 2 A)) ⊒ 2 ((A ⊒ 2 A) ⊑ 2 A) ⊒ 2
(1 A)

⊒ 3
A where, moreover, configurations whose maximal events are visible (and so correspond to configurations of S) are those where the ⊑ 1 are replaced by ⊇ + , the ⊑ 2 are replaced by equalities and the ⊑ 3 are replaced by ⊆ -. Such configurations exactly correspond to those of C C A .

This concludes the proof that CG is a compact closed category.

Conclusions

In this paper, we gave a detailed exposition of the results of [START_REF] Rideau | Concurrent strategies[END_REF], along with some extensions. We presented a notion of concurrent games based on event structures, which is a concurrent analogue of Joyal's compact closed category of Conway games [START_REF] Joyal | Remarques sur la thorie des jeux deux personnes[END_REF]. We first defined pre-strategies, as certain event structures describing the evolution of concurrent processes on an interface presented as a game. We defined strategies as those prestrategies stable under the action of an asynchronous forwarder, presented as the copycat strategy. Finally, we proved that composition of strategies obeys the laws of a bicategory, and that just as Joyal's, the corresponding quotient category is compact closed. As explained in [START_REF] Winskel | Strategies as profunctors[END_REF], it relates to the compact closed bicategory of profunctors via a lax functor. 6.0.1. Further work. The developments presented in this paper are just the beginning of the story. Since the appearance of [START_REF] Rideau | Concurrent strategies[END_REF], this framework has been used as a basis for a number of extensions. In [START_REF] Clairambault | The winning ways of concurrent games[END_REF], games were equipped with winning conditions. It was proved that winning strategies also form a bicategory, and that just as in the sequential case, well-founded games that satisfy a further condition called race-freeness are determined. This was later extended to all Borel winning conditions [START_REF] Gutierrez | On the determinacy of concurrent games on event structures with infinite winning sets[END_REF], provided in addition that concurrency is bounded in the game. Winning conditions were also generalized to a quantitative notion of payoff in [START_REF] Clairambault | On concurrent games with payoff[END_REF], and a value theorem was proved. As witnessed by these determinacy results, and despite concurrency, our games remain total information games (unlike e.g. [START_REF] Luca De Alfaro | Concurrent reachability games[END_REF]). We investigated in [START_REF] Winskel | Winning, losing and drawing in concurrent games with perfect or imperfect information[END_REF][START_REF] Clairambault | Imperfect information in logic and concurrent games[END_REF] an extension to partial information games, where determinacy is lost. The fourth author also extended the setting to probabilistic and quantum strategies [START_REF] Winskel | Distributed probabilistic and quantum strategies[END_REF].

In our basic setting, games are affine: each event can occur at most once. It is key for many applications (most notably to semantics) that one allows the replication of events, in such a way that distinct copies are indistinguishable from each other. To this effect, we equipped games with a notion of symmetry expressing indistinguishability of events and configurations. Strategies then have to respect this additional structure, by treating symmetric configurations uniformly. This can be done in two ways: the first option is to saturate strategies by forcing them to play non-deterministically all symmetric events. In [START_REF] Castellan | Symmetry in concurrent games[END_REF], we developed a bicategory of saturated strategies on games with symmetry, using it to allow replication and construct analogues of AJM [START_REF] Abramsky | Full abstraction for PCF[END_REF] and HO [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF] games. In [START_REF] Castellan | The parallel intensionally fully abstract games model of PCF[END_REF] we developed a second option, and showed that with some minimality assumption on strategies one could obtain a bicategory of uniform strategies while avoiding saturation and the addition of redundant non-deterministic choices. We showed that this gave a cartesian closed category, supporting an intensionally fully abstract model of PCF where independent sub-computations are performed in parallel. 6.0.2. Perspectives. There is a lot of ongoing work on the topic of concurrent games on event structures. On the fundamental side, we have looked for a generalization of the basic setting presented here that accommodates better events with disjunctive causality, i.e. that can occur for several distinct yet compatible reasons [START_REF] De | Strategies with parallel causes[END_REF]. On the semantic side, we have several research directions. To name a few, we want to represent non-interference as determinism in concurrent languages; to enrich strategies to keep information about possible local deadlocks or divergences; to investigate further strategies from the point of view of concurrent processes [START_REF] Castellan | Strategies as concurrent processes[END_REF]; and to mix symmetry with probabilities in order to build a denotational model combining probabilities, non-determinism and concurrency.

But beyond semantics, our concurrent games give a powerful and precise description of the evolution of concurrent processes. We wish to extend this basic framework in order to set a standard for a concurrent notion of games and strategies. We hope this framework will then be a relevant and useful tool for various purposes, from handling algorithmic issues in concurrency to investigating its logical properties. 6.0.3. Acknowledgements. We gratefully acknowledge the support of the French LABEX MILYON (ANR-10-LABX-0070), and of the ERC Advanced Grant ECSYM.

3.1. 2 .

 2 Receptivity. Consider the game Y = o -comprising a single negative event, and the two pre-strategies σ and τ on this game, with respective event structures ∅ (no moves played by σ) and o -/ o o -(τ can acknowledge the unique negative event in two different ways, non-deterministically).Their respective interactions with copycat on Y give (with A = 1, B = Y 1 and C = Y 2 ):

  Definition 3.6 (Receptivity). A pre-strategy σ : S → A is receptive when for each configuration x ∈ C (S) such that σx a - --⊂ there exists a unique s ∈ S (necessarily negative) such that x s --⊂ and σs = a.

Example 3. 7 .

 7 Consider the pre-strategy σ playing on W 1 W 2 , with event structure Done + 1 Done + 2 . The following diagram represents an interaction z ∈ C (C C A ⊛ S) of σ with copycat.

  By definition, its down-closure in T ⊛ S is a configuration y = [x] ∈ C (T ⊛ S), whose maximal elements are visible. By Lemma 2.12, this configuration is represented by (the graph of) a secured bijection ϕ ∈ B sec σ C,A τ . We write: y S y C ϕ ≃ y A y T with σy S = y A y B and τ y T = y B y C . By hypothesis we have y A y B ⊆ -y ′ A y B , and y B y C ⊆ -y B y ′ C for some y ′ A ∈ C (A ⊥ ) and y ′ C ∈ C (C). Since σ and τ are strategies, there are unique y S ⊆ y ′ S ∈ C (S) and y T ⊆ y ′ T ∈ C (T ) such that σy ′ S = y ′ A y B and τ y ′ T = y B y ′ C . The induced extension of ϕ y ′ S y ′ C ϕ ′ ≃ y ′ A y ′ T is secured: the added events only map to A and C, so there is no interaction (hence potential deadlock) between σ and τ going on. Moreover, ϕ ′ represents a configuration y ⊆ y ′ ∈ C (T ⊛ S), which maps to x ′ A x B x ′ C . By projection we get the required extension of x. Uniqueness follows directly from uniqueness for y ′ S and y ′ T . Positive fibration. Similar reasoning.

Proposition 5. 1 .

 1 For any esp A, we havec c A⊗B ∼ = c c A ⊗ c c BProof. We have the isomorphismγ A ⊥ ,B ⊥ ,A,B : (A ⊥ B ⊥ ) (A B) → (A ⊥ A) (B ⊥ B)which can also be typed asγ A ⊥ ,B ⊥ ,A,B : C C A⊗B → C C A C C B ,which obviously commutes with the projections to the game.

F F S d d d d d d d d d d d d d d d d d d d d d d d d d d d d d

This means that, technically, f is a strategy on B -though we are not thinking of it that way.

4.3.1. Associativity for interaction. For the rest of this subsection we only consider polarityagnostic operations, so we will ignore polarity from now on.

Consider σ : S → A B, τ : T → B C, and ρ : U → C D. The composition ρ ⊙ τ : U ⊙T → B D is obtained by restriction from the mediating map ρ⊛τ : U ⊛T → B C D of the interaction pullback. In turn, we can form (ρ ⊛ τ ) ⊛ σ : (U ⊛ T ) ⊛ S → A B C D as (the mediating map of) the pullback of σ C D and A (ρ ⊛ τ ). From that (using that pullbacks are stable under parallel composition) it appears that (ρ ⊛ τ ) ⊛ σ is (the mediating map of) a ternary pullback of σ C D, A τ D and A B ρ. But a similar reasoning holds for ρ ⊛ (τ ⊛ σ), so by the universal property of pullbacks, there is a unique map a σ,τ,ρ , necessarily an isomorphism, making the projections to σ C D, A τ D and A B ρ commute:

E, all bracketings of the quaternary interaction between σ, τ, ρ, δ can be obtained via pullbacks of σ C D E, A τ D E, A B ρ E and A B C δ taken in different orders. It follows from an easy diagram chase that Mac Lane's pentagon commutes at the level of interactions:

a τ ⊛σ,ρ,δ w w p p p p p p p p p p p p p p p p p

To conclude associativity, we need to show how to reproduce the same reasoning on composition, or more adequately deduce it from that on interactions. 4.3.2. Partial-total factorization and hiding witnesses. In order to deduce associators on composition and their coherence from those on interactions, we generalize the partial-total universal property of Lemma 4.3 to n-ary interactions and compositions. For instance, we need to prove that the hiding map (to be defined precisely):

has the partial-total universal property. It is rather inconvenient to prove it directlyinstead, we prove an auxiliary property that is easier to combine. Definition 4.5. Let f : E ⇀ F be a partial map. A hiding witness for f is a monotonic function:

4.4. Unitors. The last ingredients of our bicategory are the two unitors. For any strategy σ : S → A ⊥ B, those are the two isomorphisms for cancellation of copycat:

We start by defining λ σ (and ρ σ ): their definition is not strictly speaking covered by the result of Theorem 3.20 which only dealt with closed compositions of a strategy σ : S → A with c c A . However the construction is very similar and will only be roughly sketched here.

Lemma 4.10. Let σ : S → A ⊥ B. Then, there are order-isomorphisms:

where the right hand side sets are ordered by componentwise inclusion.

Proof. Straightforward adaptation of Lemma 3.9.

At this point, it is also worth mentioning that it follows from courtesy of σ that in a situation like in the lemma above, we actually have

No positive events can be added by going from x r B to x l B , as using courtesy one can show that those could not be below a visible events. That fact is not used in our development, so we skip the detailed proof.

We jump to the definition of the unitors:

Lemma 4.11. For any σ : S → A ⊥ B, there are isomorphisms of strategies:

x B given by the discrete fibration property of σ.

Proof. Straightforward adaptation of (iii) ⇒ (i) in the proof of Theorem 3.20.

We now show that the unitors λ σ , ρ σ are natural in σ. In fact, it will be helpful later on to prove here a slightly more general property: that the unitors acts naturally with respect to generalized morphisms between strategies, that change the base game as well. In order to state it, first note that the construction A → C C A on esps can be easily extended into a functor:

C C : EP → EP Indeed, for f : A → B a map of esps, we have f ⊥ f : A ⊥ A → B ⊥ B (using the obvious functorial action of (-) ⊥ and on EP). But A ⊥ A and B ⊥ B are respectively the sets of events of C C A and C C B ; and it is a simple verification that we do have

B 1 ), and the unique such (by uniqueness of the discrete fibration property). Therefore,

). And finally, using the description of their action we verify the coherence law for unitors. x C . Moreover, the induced order on triples is secured, and its maximal elements are visible. But this implies that actually x l B = x r B -it is easy to show that if (non-visible) b ∈ x l B is not in x r B , then it cannot be below a visible event. From Therefore, by Lemma 4.4, it follows that the following diagram commutes:

Combined with the isomorphism c c B ⊙ σ ∼ = σ, this concludes the proof. The other case is symmetric.

From the lemma above it immediately follows that lifting is functorial: Lemma 5.5. Let f : A → B and g : B → C be receptive courteous maps, then we have an isomorphism:

Proof. Immediate consequence of Lemma 5.4.

Using this, we can lift the symmetric closed monoidal structure of E to CG. In particular, there are natural isomorphisms in E which are componentwise receptive and courteous, and so are their inverses.

(the reuse of symbols from Section 4 for these structural morphisms should not cause any confusion). These isomorphisms can then be lifted to strategies:

which inherit from E all the coherence laws of the symmetric monoidal structure by Lemma 5.5. It remains to prove that these families are natural.

Lemma 5.6. The families ρ A , λ A , s A,B , α A,B,C are natural in all their components. Proof. A direct verification. For illustration, we detail the naturality of s A,B .

Let σ : S → A ⊥ 1 A 2 , and τ : T → B ⊥ 1 B 2 . We need to check:

But there is an obvious isomorphism s A 1 ,B 1 ∼ = s -1

. So by both parts of Lemma 5.4, this amounts to finding an isomorphism between the two maps:

and it is a simple verification to check that s S,T does the trick.