# From Thin Concurrent Games to Generalized Species of Structures (Extended Version)

Pierre Clairambault, Federico Olimpieri, Hugo Paquet

► To cite this version:

Pierre Clairambault, Federico Olimpieri, Hugo Paquet. From Thin Concurrent Games to Generalized Species of Structures (Extended Version). Logical Methods in Computer Science, 2025, Volume21,Issue4, 10.46298/lmcs-21(4:12)2025 . hal-05383180

HAL Id: hal-05383180

https://hal.science/hal-05383180v1

Submitted on 26 Nov 2025

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons Attribution 4.0 International License
# FROM THIN CONCURRENT GAMES TO GENERALIZED SPECIES OF STRUCTURES (EXTENDED VERSION)

PIERRE CLAIRAMBAULT ⚫ª, FEDERICO OLIMPIERI ⚫ª, AND HUGO PAQUET ⚫ᵇ

**ABSTRACT.** Two families of denotational models have emerged from the semantic analysis of linear logic: *dynamic* models, typically presented as game semantics, and *static* models, typically based on a category of relations. In this paper we introduce a formal bridge between a dynamic model and a static model: the model of *thin concurrent games and strategies*, based on event structures, and the model of *generalized species of structures*, based on distributors. A special focus of this paper is the two-dimensional nature of the dynamic-static relationship, which we formalize with double categories and bicategories.

In the first part of the paper, we construct a symmetric monoidal oplax functor from linear concurrent strategies to distributors. We highlight two fundamental differences between the two models: the composition mechanism, and the representation of resource symmetries.

In the second part of the paper, we adapt established methods from game semantics (visible strategies, payoff structure) to enforce a tighter connection between the two models. We obtain a cartesian closed pseudofunctor, which we exploit to shed new light on recent results in the theory of the λ-calculus.

## 1. INTRODUCTION

The discovery of linear logic has had a deep influence on programming language semantics. The linear analysis of resources provides a refined perspective that leads, for instance, to important notions of program approximation [BM20] and differentiation [ER03]. Denotational models for higher-order programming languages can be constructed from this resource-aware perspective, exploiting the fact that every model of linear logic is also a model of the simply-typed λ-calculus.

In this paper, we clarify the relationship between two such denotational models:

* *Thin concurrent games*, a framework for game semantics introduced by Castellan, Clairambault, and Winskel [CCW19], in which programs are modeled as concurrent strategies.

* *Generalized species of structures*, a combinatorial model developed by Fiore, Gambino, Hyland, and Winskel [FGHW08], in which programs are interpreted as categorical distributors (or profunctors) over groupoids.

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

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

<footnote>ª Aix Marseille Univ, CNRS, LIS, Marseille, France
*e-mail address:* pierre.clairambault@lis-lab.fr, federico.olimpieri@lis-lab.fr</footnote>

<footnote>ᵇ Inria, École Normale Supérieure – PSL, CNRS, Paris, France
*e-mail address:* Hugo.Paquet@inria.fr</footnote>
We carry out this comparison in a two-dimensional setting also including morphisms between strategies and morphisms between distributors. In the language of bicategory theory, our first key contribution is a symmetric monoidal, *oplax* functor of bicategories

$$ \begin{array}{ccc} \text{games, strategies} & & \text{groupoids, distributors and} \\ & \longrightarrow & \text{natural transformations} \\ \text{and maps} & & \end{array} \qquad (1.1) $$

showing, in particular, that symmetries of strategies can be explained via groupoid actions.

## 1.1. Static and dynamic models.
This work fits in a long line of research on the relationship between *static* and *dynamic* denotational models arising from linear logic.

In a static model, programs are represented by their input/output behavior, or by collecting representations of completed executions. The simplest example is given by the category of sets and relations: this is the relational model of linear logic (Section 2.1 or [Gir87]). In a dynamic model, programs are represented by their interactive behavior with respect to every possible execution environment. This includes game semantics ([HO00, AJM00]), which has proved incredibly proficient at modeling various computational features or effects ([AHM98, Lai97, GM08]).

To illustrate the difference, the identity at type $1 \to 1$ in game semantics is a *strategy* gathering *plays* which represent chronologically an exchange of information and control flow between the *program* and its *environment*:

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

In contrast, in the relational model, $1 \to 1$ is a one-element set containing a single input/output pair. The identity relation over it can be seen as a collapsed version of the strategy above:

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

This suggests a simple equation

$$ \textit{game semantics} = \textit{relational model} + \textit{time}, $$

so that going from game semantics to the relational model is a simple matter of forgetting the temporal order of execution, an intuition first explored in [BDER97b].

But this naive intuition hides a fundamental difference between the composition mechanisms in static and dynamic models: strategies may *deadlock*, while relations cannot. More precisely, in game semantics, two strategies can synchronize by performing the same actions *in the same order*, whereas in the collapsed version, only the actions matter and not the order. Thus, as was quickly established [BDER97b], one cannot simply forget time in a functorial way, and composition is usually only preserved in an *oplax* manner, as in (1.1).

Static collapses of game semantics require an adequate notion of *position* for a game. This is somewhat difficult to define in traditional game semantics, but very natural in alternative causal versions such as concurrent games, because we can look at configurations of the underlying event structure (Section 4.1, see also [Mel06, Mel05]).
The subtle relationship between static and dynamic models was refined by many authors over almost three decades (see e.g. [BDER97b, Mel05, Bou09, CM10, TO16]), to identify settings in which functoriality can be restored – in particular, our work inherits insights from Mellies’ line of work on asynchronous games [Mel05]. Leveraging this, we show (in Section 7) how the oplax functor (1.1) can be strictified to a *pseudofunctor*, that preserves composition up to isomorphism.

**1.2. Proof-relevant models and symmetries.** Our aim here is to take the static-dynamic relationship to a new level that takes into account the symmetries implicit in the resource usage. Symmetry plays an important role in game semantics (Section 5, or [AJM00, Mel06, CCW14, Paq22]), but so far connections only exist with static models whose symmetries are implicit or quotiented, like the relational model. We argue that generalized species, which represent combinatorial structures in terms of their symmetries, provide a convenient target for a static collapse of thin concurrent games.

The two models we consider are “proof-relevant” [KMO23], in the sense that the interpretation of a program provides, for each possible execution, a set of proofs or *witnesses* that this execution can be realized. This high degree of intensionality is useful for modelling languages with non-deterministic features [TO15, CCPW18]. In a proof-relevant model, symmetries arise naturally in the linear duplication of witnesses. In Section 2.2 we discuss the limitations of a proof-relevant model without symmetries.

**1.3. Two-dimensional categories: bicategories and double categories.** Proof-relevant models are naturally organized as two-dimensional categories, because programs are interpreted as structured objects (e.g. strategies or distributors) between which there is a natural notion of morphism. There are various kinds of 2-dimensional categories. This line of research is primarily about semantics in *bicategories*, and indeed the final sections of this paper (Section 7, Section 8) are about bicategories with structure and bicategorical functors. However, in order to properly relate static and dynamic models, we find it conceptually important and technically useful to regard them as richer structures: *pseudo double categories*. We do not assume any prior knowledge of double categories, and we give more precise motivation in Section 3.

**1.4. Bicategorical models of the λ-calculus.** As further motivation for this work, we note that the two-dimensional and proof-relevant aspects are significant on the syntactic side. The interpretation of λ-terms in generalized species has a presentation in terms of an *intersection type system* [TAO17, Oli21], that takes into account the symmetries and can be exploited to characterize computational properties and equational theories of the λ-calculus. More generally, the structural 2-cells in a cartesian closed bicategory have a syntactic interpretation as *βη-rewriting steps* in the simply-typed λ-calculus ([FS19, See87]).

In Section 7 we connect to this line of work by constructing a cartesian closed pseudo-functor, which preserves the semantics of λ-terms in both typed and untyped settings.

**1.5. Outline of the paper and key contributions.** The paper is organized as follows.
Finally, this long version also allows for further illustration: we showcase the induced correspondence between game semantics and generalized species over an example λ-term.

## 2. A TOUR OF STATIC SEMANTICS

In this section we present three static models: the basic relational model **Rel** (Section 2.1), a proof-relevant version of it which we call **PRRel** (Section 2.2), and the model **Dist** of groupoids and distributors (Section 2.3).

### 2.1. The relational model of linear logic.
We start with the relational model, which gives a denotational interpretation in the category **Rel** of sets and relations. A type A is interpreted as a set $\llbracket A \rrbracket$, and a program $\vdash M : A$ is interpreted as a subset $\llbracket M \rrbracket \subseteq \llbracket A \rrbracket$. The set $\llbracket A \rrbracket$ is often called the web of A, and we think of its elements as representations of completed program executions. The subset $\llbracket M \rrbracket$ contains the executions that the program M can realize.

**Example 2.1.** The ground type for booleans is interpreted as $\llbracket \mathbb{B} \rrbracket = \{\mathbf{tt}, \mathbf{ff}\}$, and the constant $\vdash \mathbf{tt} : \mathbb{B}$ as $\llbracket \mathbf{tt} \rrbracket = \{\mathbf{tt}\}$.

The interpretation of a program M is computed compositionally, following the methodology of denotational semantics, using the categorical structure we describe below.

#### 2.1.1. Basic categorical structure.
The category **Rel** is defined to have sets as objects, and as morphisms the relations from A to B, i.e. the subsets $R \subseteq A \times B$, with the usual notions of identity and composition for relations. Its monoidal product is the cartesian product of sets. If $R_i \in \mathbf{Rel}[A_i, B_i]$ for $i = 1, 2$, then the relation $R_1 \times R_2 \in \mathbf{Rel}[A_1 \times A_2, B_1 \times B_2]$ is defined to contain the pairs $((a_1, a_2), (b_1, b_2))$ with $(a_i, b_i) \in R_i$. The unit I is a fixed singleton set, say $\{*\}$. This monoidal structure is closed, with linear arrow $A \to B = A \times B$.

Moreover **Rel** has finite cartesian products: the product of sets A and B is given by the disjoint union $A + B = \{1\} \times A \uplus \{2\} \times B$, and the empty set is a terminal object.

#### 2.1.2. The exponential modality.
The exponential modality of **Rel** is based on finite multisets. If A is a set, we write $\mathcal{M}(A)$ for the set of finite multisets on A. To denote specific multisets we use a list-like notation, as in e.g. $[0, 1, 1] \in \mathcal{M}(\mathbb{N})$.

Given a set A, its **bang** !A is the set $\mathcal{M}(A)$. This extends to a comonad ! on **Rel**, satisfying the required conditions for a model of intuitionistic linear logic: the Seely isomorphisms

$$ \mathcal{M}(A + B) \cong \mathcal{M}(A) \times \mathcal{M}(B) \quad \mathcal{M}(\emptyset) \cong I $$

make ! a symmetric monoidal functor from $(\mathbf{Rel}, +, \emptyset)$ to $(\mathbf{Rel}, \times, I)$, satisfying a coherence axiom [Mel09, §7.3]. From this, we obtain that the Kleisli category **Rel**! is cartesian closed and thus a model of the simply-typed λ-calculus.
2.1.3. Conditionals and non-determinism. The category **Rel**! also supports further primitives in a call-by-name setting.

**Example 2.2.** Considering the term $\vdash M : \mathbb{B} \to \mathbb{B}$ of PCF

$$ \vdash \lambda x^{\mathbb{B}}. \mathbf{if} x \mathbf{then} x \\ \mathbf{else} \mathbf{if} x \mathbf{then} \mathbf{ff} \mathbf{else} \mathbf{tt} : \mathbb{B} \to \mathbb{B}, $$

then $[[M]] = \{([\mathbf{tt}, \mathbf{tt}], \mathbf{tt}), ([\mathbf{tt}, \mathbf{ff}], \mathbf{ff}), ([\mathbf{ff}, \mathbf{ff}], \mathbf{tt})\}$, representing the possible executions given a multiset of values for $x$.

As a further example, **Rel** supports the interpretation of non-deterministic computation: consider $\vdash \mathbf{choice} : \mathbb{B}$ a non-deterministic primitive that may evaluate to either **tt** or **ff**. Then we can set $[[\mathbf{choice}]] = \{\mathbf{tt}, \mathbf{ff}\}$ so that we have

$$ [[\mathbf{if choice then tt else tt}]] = \{\mathbf{tt}\}. \qquad (2.1) $$

The relational model is a cornerstone of static semantics, and the foundation of many recent developments in denotational semantics [BEM07, dC18, LMMP13]. In this paper we are concerned with its *proof-relevant* extensions. Roughly speaking, one motivation is to keep separate different execution paths that lead to the same value, as with value **tt** in (2.1).

2.2. **Proof-relevant relations.** To showcase this, we consider a notion of proof-relevant relation between sets (e.g. [Gir88, GJ17]). The idea is to record not only the executions that a program may achieve, but also the distinct ways in which each execution is realized. We replace relations $[[M]] \subseteq A \times B$ with *proof-relevant relations*

$$ [[M]] : A \times B \to \mathbf{Set}, $$

so that each point of the web has an associated set of witnesses. In this model, for instance, $[[\mathbf{if choice then tt else tt}]](\mathbf{tt})$ from (2.1) should be a set $\{*_1, *_2\}$ containing two witnesses, because there are two possible paths to the value **tt**.

Formally, the model is organized as a categorical structure with sets as objects, functors $\alpha : A \times B \to \mathbf{Set}$ (with $A \times B$ viewed as a discrete category) as morphisms, composed with

$$ (\beta \circ \alpha)(a, c) = \sum_{b \in B} \alpha(a, b) \times \beta(b, c) \qquad (2.2) $$

and with identity morphisms given by $\mathrm{id}_A(a, a') = \{*\}$ if $a = a'$ and empty otherwise<fnref n="1" />. An important observation is that this does not form a category. Categorical laws are only *iso-morphisms*, with for instance $(\mathrm{id}_B \circ \alpha)(a, b) = \alpha(a, b) \times \{*\} \cong \alpha(a, b)$. We obtain a *bicategory*: a two-dimensional structure incorporating 2-cells – morphisms between morphisms – with categorical laws holding only up to coherent invertible 2-cells.

We call this bicategory **PRRel**. This model shares (in a bicategorical sense) much of the structure of **Rel**, and may be used to interpret e.g. the linear $\lambda$-calculus. We use **PRRel** as a static collapse of a basic dynamic model in Section 4.3.

<footnote n="1">¹A more standard presentation of this model is via the bicategory of spans of sets, with sets as objects and spans $A \leftarrow S \to B$ as morphisms.</footnote>
**Limitations of a proof-relevant model without symmetry.** Unfortunately, the finite multiset functor on **Rel** does not seem to extend to **PRRel**. Intuitively, the objective of keeping track of individual execution witnesses is in tension with the quotient involved in constructing finite multisets, which blurs out the identity of individual resource accesses<fnref n="2" />. Proof-relevant models that do support an exponential modality do so by replacing finite multisets with a categorification, such as finite lists related by explicit permutations – *symmetries*.

**2.3. Distributors and generalized species of structures.** This categorification yields, among other possible approaches, the bicategory of *distributors*. *Distributors* are symmetry-aware proof-relevant relations – here we consider distributors on *groupoids*, i.e. small categories in which every morphism is invertible.

**2.3.1. The bicategory of groupoids and distributors.** If $A$ and $B$ are groupoids, a **distributor** from $A$ to $B$ (also known as a *profunctor* or *bimodule*) is a functor

$$ \alpha : A^{\text{op}} \times B \to \mathbf{Set}. $$

Thus, for every $a \in A$ and $b \in B$ we have a set $\alpha(a, b)$ of witnesses, but unlike in **PRRel** we also have symmetries, in the form of an action by morphisms in $A$ and $B$. If $x \in \alpha(a, b)$ and $g \in B(b, b')$, we write $g \cdot x$ for the functorial action $\alpha(\text{id}, g)(x) \in \alpha(a, b')$. Similarly, if $f \in A(a', a)$, we write $x \cdot f \in \alpha(a', b)$ for $\alpha(f, \text{id})$. The actions must commute, so we can write $g \cdot x \cdot f$ for $(g \cdot x) \cdot f = g \cdot (x \cdot f) \in \alpha(a', b')$.

We define a bicategory **Dist** with groupoids as objects, distributors as morphisms, and natural transformations as 2-cells ([Yon60, Bén73]). The **identity distributor** on $A$ is

$$ \mathrm{id}_A = A[-, -] : A^{\text{op}} \times A \to \mathbf{Set}, $$

the hom-set functor. The **composition** of two distributors $\alpha : A^{\text{op}} \times B \to \mathbf{Set}$ and $\beta : B^{\text{op}} \times C \to \mathbf{Set}$ is obtained as a categorified version of (2.2), defined in terms of a coend:

$$ (\beta \bullet \alpha)(a, c) = \int_{b \in B} \alpha(a, b) \times \beta(b, c). \qquad (2.3) $$

Concretely, $(\beta \bullet \alpha)(a, c)$ consists in pairs $(x, y)$, where $x \in \alpha(a, b)$ and $y \in \beta(b, c)$ for some $b \in B$, quotiented by $(g \cdot x, y) \sim (x, y \cdot g)$ for $x \in \alpha(a, b)$, $g \in B(b, b')$ and $y \in \beta(b', c)$ – by convention, we use $y \bullet x \in (\beta \bullet \alpha)(a, c)$ as a notation for the (equivalence class of) the pair $(x, y)$.

The bicategory **Dist** has a symmetric monoidal structure given by the cartesian product $A \times B$ of groupoids, extended pointwise to distributors. There is a closed structure given by $A \dashv B = A^{\text{op}} \times B$. Finally, **Dist** has cartesian products given by the disjoint union $A + B$ of groupoids.

<footnote n="2">²In technical terms, the functor $M(-)$ on **Set** is not cartesian – does not preserve pullbacks – and so does not preserve the composition of spans.</footnote>
### 2.3.2. The exponential modality.
In this model with explicit symmetries, the exponential modality is not given by finite multisets, but instead by finite lists with explicit permutations.

**Definition 2.3.** For a groupoid $A$, there is a groupoid $\mathbf{Sym}(A)$ with as objects the finite lists $(a_1...a_n)$ of objects of $A$, and as morphisms $(a_1...a_n) \to (a'_1...a'_m)$ the pairs $(\pi, (f_i)_{1\le i\le n})$, where $\pi: \{1,...,n\} \cong \{1,...,m\}$ is a bijection and $f_i \in A(a_i, a'_{\pi(i)})$ for each $i=1,...,n$.

More abstractly, $\mathbf{Sym}(A)$ is the free symmetric (strict) monoidal category over $A$. This extends to a pseudo-comonad on $\mathbf{Dist}$, where pseudo means that the comonad laws only hold up to coherent invertible 2-cells [Lac00, FGHW08].

### 2.3.3. Generalized species of structures.
The Kleisli bicategory $\mathbf{Dist}_{\mathbf{Sym}}$ is denoted $\mathbf{Esp}$, and the morphisms in $\mathbf{Esp}$ are called generalized species of structures [FGHW08]. Concretely, $\mathbf{Esp}$ has the same objects as $\mathbf{Dist}$; morphisms are generalized species$^3$, defined as distributors from $\mathbf{Sym}(A)$ to $B$; and 2-cells are natural transformations. Equipped with

$$ \mathbf{Sym}(A+B) \simeq \mathbf{Sym}(A) \times \mathbf{Sym}(B) \qquad \mathbf{Sym}(\emptyset) \simeq I $$

the Seely equivalences, $\mathbf{Dist}$ is a bicategorical model of linear logic. In particular, the bicategory $\mathbf{Esp}$ is cartesian closed.

### 2.3.4. Relationship with PRRel.
Distributors conservatively extend the proof-relevant relations of Section 2.2: if we regard sets as discrete groupoids, we get an embedding $\mathbf{PRRel} \hookrightarrow \mathbf{Dist}$ that preserves the symmetric monoidal closed structure and the cartesian structure. Explicit symmetries appear essential in defining an exponential modality in a proof-relevant model: even when $A$ is a discrete groupoid, $\mathbf{Sym}(A)$ is not discrete.

## 3. DOUBLE CATEGORIES FOR STATIC MODELS

The models $\mathbf{PRRel}$ and $\mathbf{Dist}$ are bicategories: they have objects, morphisms, and 2-cells. This 2-dimensional structure is essential, because the laws for composition are only satisfied up to invertible 2-cells. Although $\mathbf{Rel}$ is a category, we can regard it as a degenerate bicategory where the laws for composition hold strictly, and with 2-cells given by the usual order on relations: if $R, R' \in \mathbf{Rel}(A, B)$, then we have a 2-cell $R \Rightarrow R'$ whenever $R \subseteq R'$ as subsets of $A \times B$. (This is a proof-irrelevant counterpart of the 2-dimensional structure in $\mathbf{PRRel}$ and $\mathbf{Dist}$.)

The point of this section is to establish that each of these bicategories arises as a fragment of a larger categorical structure known as a pseudo double category, which consists of objects, two kinds of morphisms (known as horizontal and vertical), and 2-cells. Horizontal morphisms compose weakly (as in a bicategory) and vertical morphisms compose strictly (as in a category). The motivation for considering this more general structure is that, for many bicategories, there exists a simpler class of morphisms between the objects for which composition is strictly associative and unital. This can be exploited to simplify certain structural proofs, as we will do.

<footnote n="3">³If $A = B = 1$, then a generalized species corresponds to a combinatorial species in the classical sense of Joyal [Joy81]. This can be further generalized to arbitrary small categories $A$ and $B$ [FGHW08], but we do not need this generality.</footnote>
We first give the definition of a pseudo double category. We usually drop the adjective “pseudo” in the paper. Pseudo-double categories are originally due to Ehresmann [Ehr63]. For a detailed reference on double category theory that includes monoidal double categories, functors between them, and monads, see [GGV24, Sections 2–5]. For the theory of double monads, see also [CS10].

**Definition 3.1.** A **pseudo double category** (e.g. [GGV24, Def. 2.1]) consists of:

* a class of objects;

* **vertical morphisms** between the objects, typically displayed as $A \to B$, with the structure of a category (that is, identity morphisms, and a composition operation satisfying axioms);

* **horizontal morphisms** between the objects, typically displayed as $A \dashrightarrow B$, with identity morphisms and a composition operation;

* square-shaped 2-cells between pairs of vertical morphisms and pairs of horizontal morphisms, as follows:

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

which can be composed horizontally and vertically. When the vertical boundaries $f$ and $g$ are identity morphisms, a 2-cell is called **globular**.

Horizontal morphisms can be composed, but associativity and unit laws only hold weakly, just like in a bcategory: up to coherent, invertible, globular 2-cells, whose names we omit.

An immediate observation is that a pseudo double category $\mathcal{D}$ always has an underlying bcategory over the same objects, consisting of horizontal morphisms and globular 2-cells. We call this the **horizontal bcategory H(\mathcal{D})**. It is well-known that our bcategories **Rel**, **PRRel**, and **Dist** all arise in this way from pseudo double categories with a natural class of vertical morphisms, as we explain now.

**3.1. Examples: static models as double categories.** To define a double category from a bcategory, we must define a class of vertical morphisms and an appropriate notion of 2-cells. In **Rel** and **PRRel**, the objects are sets, and the vertical morphisms are taken to be functions. In **Dist**, the objects are groupoids, and the vertical morphisms will be functors.

**Example 3.2** (The double category of relations). The double category $\mathcal{Rel}$ has the following components:

* objects: sets;

* vertical morphisms: functions;

* horizontal morphisms: relations;

* and a 2-cell of type

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

exists when $(a, b) \in \mathcal{R}$ implies $(f(a), g(b)) \in \mathcal{S}$ for every $a, b$.
When $f$ and $g$ are identity functions, there is a 2-cell as above just when $R \subseteq S$. So the horizontal bicategory $\mathbf{H}(\mathbf{Rel})$ is exactly the bicategory $\mathbf{Rel}$ of sets and relations.

We now turn to proof-relevant relations and distributors. Since $\mathbf{PRRel}$ can be regarded as the full sub-bicategory of $\mathbf{Dist}$ over the discrete groupoids, we start with the more general model.

**Example 3.3** (The double category of groupoids and distributors). The double category $\mathbf{Dist}$ has the following components:

• objects: groupoids;

• vertical morphisms $A \to B$: functors;

• horizontal morphisms $A \dashrightarrow B$: distributors $A^{\text{op}} \times B \to \mathbf{Set}$;

• 2-cells of type

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

are natural transformations $\alpha(a, b) \Rightarrow \beta(F(a), G(b))$ between functors $A^{\text{op}} \times B \to \mathbf{Set}$.

It is clear that $\mathbf{H}(\mathbf{Dist}) = \mathbf{Dist}$. We can consider the discrete sub-model, with no symmetries:

**Example 3.4** (The double category of proof-relevant relations). If we restrict the objects in $\mathbf{Dist}$ to discrete skeletal groupoids (i.e. sets), we obtain a double category called $\mathbf{PRRel}$. Up to isomorphism, this double category has sets as objects, and functions as vertical morphisms. Then $\mathbf{H}(\mathbf{PRRel})$ corresponds to our bicategory $\mathbf{PRRel}$.

A **double functor** between double categories defines an appropriate mapping of objects, vertical and horizontal morphisms, and 2-cells, with coherence data similar to that for a functor of bicategories. Note that a double functor can be lax, oplax, or pseudo, depending on the nature of the globular compositor 2-cell. Between double functors, there are two possible kinds of natural transformations: vertical and horizontal [GGV24, Def. 3.4 and Def. 3.5].

### 3.2. Companions and conjoints.
Our three examples share a common feature: a vertical morphism always induces a pair of horizontal morphisms. For example, in $\mathbf{Rel}$, a function $f: A \to B$ induces relations $\hat{f} = \{(a, f(a)) \mid a \in A\}: A \dashrightarrow B$ and $\tilde{f} = \{(f(a), a) \mid a \in A\}: B \dashrightarrow A$. In $\mathbf{Dist}$ (and so also in $\mathbf{PRRel}$) we have a similar construction: if $A$ and $B$ are groupoids and $F: A \to B$ is a functor, there are distributors $\hat{F}: A \dashrightarrow B$ and $\tilde{F}: B \dashrightarrow A$, defined below

$$ \hat{F}: A^{\text{op}} \times B \to \mathbf{Set} $$

$$ (a, b) \mapsto B[F(a), b] $$

$$ \tilde{F}: B^{\text{op}} \times A \to \mathbf{Set} $$

$$ (b, a) \mapsto B[b, F(a)] $$

These constructions are instances of an abstract notion in double category theory.

**Definition 3.5.** Let $\mathcal{D}$ be a pseudo double category and let $S: A \to B$ be a vertical morphism. A **companion** of $S$ is a horizontal morphism $\hat{S}: A \dashrightarrow B$ together with a pair
of 2-cells

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

satisfying appropriate axioms (e.g. [GGV24, Def. 2.6]). A **conjoint** of $S$ is defined dually, as a horizontal morphism $\tilde{F} : B \dashrightarrow A$ with corresponding data and axioms.

Any two companions of $S$, and any two conjoints, are canonically isomorphic. The constructions we gave for relations and profunctors provide companions and conjoints, and in this case the accompanying 2-cells are trivial.

**Lemma 3.6.** In Rel, PRRel, and Dist, all vertical morphisms have companions and conjoints.

A pseudo double category with this property is often directly presented as a proarrow equipment [Woo82]. We do not use equipments in this paper, because the double category of games we present in the next section only admits companions and conjoints for a subclass of vertical morphisms, and so we must discuss these notions explicitly.

Note that a functor $F : A \to B$ also determines a pair of species $\hat{F} \in \mathbf{Esp}[A, B]$ and $\tilde{F} \in \mathbf{Esp}[B, A]$, respectively defined by

$$ \hat{F}((a_1, \dots, a_n), b) = \mathbf{Sym}(B)[(F(a_1), \dots, F(a_n)), (b)] $$

$$ \tilde{F}((b_1, \dots, b_n), a) = \mathbf{Sym}(B)[(b_1, \dots, b_n), (F(a))]. $$

This construction gives companions and conjoints for $F$ in an alternative double category consisting of groupoids, functors, and generalized species. We omit the details of this double category, which we do not use in the paper. (The notations $\hat{F}$ and $\tilde{F}$ refer ambiguously to the induced distributors or to the induced species, but this will be clear from context.)

**3.3. Symmetric monoidal structure in double categories.** In this paper we primarily exploit the double-categorical structure of our models to simplify the description of symmetric monoidal structure in the underlying bicategories. This technique is well-established [Shu10]. Symmetric monoidal double categories have a much simpler definition than symmetric monoidal bicategories, because we can use vertical morphisms to encode the associativity, unit, and symmetry constraints of the monoidal product. Since vertical morphisms form a strict category, we can use strict categorical notions, avoiding the numerous coherence axioms that are needed when defining a symmetric monoidal bicategory.

**Definition 3.7.** A **symmetric monoidal double category** is a double category $\mathbb{D}$ equipped with a double functor $\otimes : \mathbb{D} \times \mathbb{D} \to \mathbb{D}$, an object $I$, and vertical double natural transformations for symmetry, associativity, and unitality: in particular there are vertical 1-cells

$$ (A \otimes B) \otimes C \xrightarrow{a_{A,B,C}} A \otimes (B \otimes C) \quad A \otimes I \xrightarrow{r_A} A \quad I \otimes A \xrightarrow{l_A} A \quad A \otimes B \xrightarrow{b_{A,B}} B \otimes A $$

satisfying a number of coherence axioms (see e.g. [GGV24, Def. 4.1] for a fully explicit definition).
In general, if a double category $\mathcal{D}$ is symmetric monoidal, then the underlying horizontal bicategory $\mathbf{H}(\mathcal{D})$ has no reason to be symmetric monoidal, since the monoidal data was defined only at the vertical level, and the horizontal bicategory has no access to it. But, when the structural isomorphisms have horizontal companions, the symmetric monoidal structure can be lifted the horizontal level. This is due to Shulman and Wester-Hansen [HS19, Thm 1.2]:

**Theorem 3.8** [HS19]. Let $\mathcal{D}$ be a symmetric monoidal double category, and suppose that in $\mathcal{D}$ all vertical isomorphisms have companions. Then the bicategory $\mathbf{H}(\mathcal{D})$ is symmetric monoidal in a canonical way.

Furthermore, if $\mathcal{E}$ is also a symmetric monoidal double category where all vertical isomorphisms have companions, then every symmetric monoidal pseudo double functor $F: \mathcal{D} \to \mathcal{E}$ induces a symmetric monoidal pseudofunctor $\mathbf{H}(F): \mathbf{H}(\mathcal{D}) \to \mathbf{H}(\mathcal{E})$.

We can then directly verify the following property:

**Lemma 3.9.** The double categories $\mathbf{Rel}$, $\mathbf{PRRel}$, and $\mathbf{Dist}$ are symmetric monoidal, and the induced symmetric monoidal structure on $\mathbf{Rel}$, $\mathbf{PRRel}$, and $\mathbf{Dist}$ corresponds to that given in Section 2.

**3.4. Another application of companions and conjoints in $\mathbf{Dist}$**. In the rest of this section, we discuss an elementary construction on distributors which will be useful in Section 7.

**Definition 3.10.** For a distributor $\alpha: A \dashrightarrow B$, i.e. a functor $\alpha: A^{\text{op}} \times B \to \text{Set}$, and functors $S: A' \to A$ and $T: B' \to B$, we define distributors $\alpha[S]: A' \dashrightarrow B$ and $[T]\alpha: A \dashrightarrow B'$ by $\alpha[S](a, b) = \alpha(Sa, b)$ and $[T]\alpha(a, b) = \alpha(a, Tb)$.

This construction extends in the obvious way to functors between hom-categories:

$$-[S] : \mathbf{Dist}[A, B] \to \mathbf{Dist}[A', B], \quad [T] - : \mathbf{Dist}[A, B] \to \mathbf{Dist}[A, B'].$$

The distributors $\alpha[S]$ and $[T]\beta$ can be presented using companions and conjoints:

**Lemma 3.11.** For $\alpha: A \dashrightarrow B$, $S: A' \to A$ and $T: B' \to B$, there are natural isomorphisms

$$\alpha[S] \cong A' \xrightarrow{\hat{S}} A \xrightarrow{\alpha} B \quad \text{and} \quad [T]\alpha = A \xrightarrow{\alpha} B \xrightarrow{\tilde{T}} B'$$

*Proof.* The first isomorphism is because $\int^{a \in A} \alpha(a, b) \times A[Sa', a] \cong \alpha(Sa', b)$ by the density formula for coends. The second one is similar. $\square$

We now introduce a few lemmas expressing compatibility of these operations with other constructions on distributors.

**Lemma 3.12.** Consider distributors $\alpha \in \mathbf{Dist}[A, B]$, $\beta \in \mathbf{Dist}[B, C]$ and functors $S: A' \to A$, $T: C' \to C$.

Then we have natural isomorphisms, additionally natural in $S$ and $T$:

$$(\beta \bullet \alpha)[S] \cong \beta \bullet \alpha[S], \quad [T](\beta \bullet \alpha) \cong [T]\beta \bullet \alpha.$$

*Proof.* Immediate from Lemma 3.11, and by associativity and naturality of composition. $\square$
**Lemma 3.13.** Consider $\alpha \in \text{Dist}[A, B]$ and $\beta \in \text{Dist}[B', C]$ distributors, with an adjunction
the consisting of $L : B \dashv B' : R$ and natural unit and counit $\eta_b \in B[b, RLb]$ and $\epsilon_{b'} \in B[LRb', b']$. Then, we have a natural isomorphism

$$ \beta[L] \bullet \alpha \cong \beta \bullet [R]\alpha $$

whose action is as follows for $t \bullet s \in (\beta[L] \bullet \alpha)(a, c)$,

$$ \xi_{\alpha, \beta, e}(t \bullet s) = t \bullet \alpha(a, \eta_b)(s) \in (\beta \bullet [R]\alpha)(a, c), $$

and as follows for $t' \bullet s' \in (\beta \bullet [R]\alpha)(a, c)$,

$$ \xi_{\alpha, \beta, e}^{-1}(t' \bullet s') = \beta(\epsilon_{b'}, c)(t') \bullet s' \in (\beta[L] \bullet \alpha)(a, c). $$

This induces a natural isomorphism

$$ \chi_e : \text{id}_{B'}[L] \cong [R] \text{id}_B \in \text{Dist}[B, B'] $$

as a special case of the above, using the composition laws for distributors.

*Proof.* From the adjunction property it is easy to check that $\hat{L} \cong \check{R}$, and the result follows by associativity of composition. $\square$

## 4. CONCURRENT GAMES AND STATIC COLLAPSE

We now construct a dynamic model based on concurrent games and strategies, without symmetries. We show that it has a static double categorical collapse in the model of proof-relevant relations introduced in Section 2.2.

**4.1. Rudiments of concurrent games.** Game semantics presents computation in terms of a two-player game: *Player* plays for the program under scrutiny, while *Opponent* plays for the execution environment. So a program is interpreted as a *strategy* for Player, and this strategy is constrained by a notion of *game*, specified by the type. The framework of concurrent games ([MM07, FP09, RW11]) is not merely a game semantics for concurrency, but a deep reworking of the basic mechanisms of game semantics using causal “truly concurrent” structures from concurrency theory [NPW79].

**4.1.1. Event structures.** Concurrent games and strategies are based on event structures. An event structure represents the behaviour of a system as a set of possible computational events equipped with dependency and incompatibility constraints.

**Definition 4.1.** An event structure (es) is $E = (|E|, \leq_E, \#_E)$, where $|E|$ is a (countable) set of events, $\leq_E$ is a partial order called **causal dependency** and $\#_E$ is an irreflexive symmetric binary relation on $|E|$ called **conflict**, satisfying:

(1) $\forall e \in |E|, [e]_E = \{e' \in |E| \mid e' \leq_E e\}$ is finite,

(2) $\forall e_1 \#_E e_2, \forall e'_2 \geq_E e_2, e_1 \#_E e'_2$.
Operationally, an event can occur if all its dependencies are met, and no conflicting events have occurred. A finite set $x \subseteq_f |E|$ down-closed for $\le_E$ and comprising no conflicting pair is called a **configuration** – we write $\mathscr{C}(E)$ for the set of configurations on $E$, naturally ordered by inclusion. If $x \in \mathscr{C}(E)$ and $e \in |E|$ is such that $e \notin x$ but $x \cup \{e\} \in \mathscr{C}(E)$, we say that $e$ is **enabled** by $x$ and write $x \vdash_E e$. For $e_1, e_2 \in |E|$ we write $e_1 \to_E e_2$ for the **immediate causal dependency**, i.e. $e_1 <_E e_2$ with no event strictly in between.

There is an accompanying notion of *map*: a **map of event structures** from $E$ to $F$ is a function $f: |E| \to |F|$ such that: (1) for all $x \in \mathscr{C}(E)$, the direct image $fx \in \mathscr{C}(F)$; and (2) for all $x \in \mathscr{C}(E)$ and $e, e' \in x$, if $fe = fe'$ then $e = e'$. There is a category **ES** of event structures and maps.

4.1.2. *Games and strategies.* Throughout this paper, we will gradually refine our notion of game. For now, a **plain game** is simply an event structure $A$ together with a **polarity function** $\text{pol}_A: |A| \to \{-, +\}$ which specifies, for each event $a \in A$, whether it is **positive** (i.e. due to Player / the program) or **negative** (i.e. due to Opponent / the environment). Events are often called **moves**, and annotated with their polarity (as in $a^-, a^+$).

A strategy is an event structure with a projection map to $A$:

**Definition 4.2.** Consider $A$ a plain game. A **strategy** on $A$, written $\sigma: A$, is an event structure $\sigma$ together with a map $\partial_\sigma: \sigma \to A$ called the **display map**, satisfying:

(1) for all $x \in \mathscr{C}(\sigma)$ and $\partial_\sigma x \vdash_A a^-$, there is a unique $x \vdash_\sigma s$ such that $\partial_\sigma s = a$.

(2) for all $s_1 \to_\sigma s_2$, if $\text{pol}_A(\partial_\sigma(s_1)) = +$ or $\text{pol}_A(\partial_\sigma(s_2)) = -$, then $\partial_\sigma(s_1) \to_A \partial_\sigma(s_2)$.

Informally, the two conditions (called *receptivity* and *courtesy*) ensure that the strategy does not constrain the behavior of Opponent any more than the game does. They are essential for the compositional structure we describe below, but they do not play a major role in this paper.

As a simple example, the usual game $\mathbb{B}$ for booleans in call-by-name is

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

drawn following the order from top to bottom, with the wiggly line indicating conflict. Player moves are blue, and Opponent moves are red – Opponent initiates computation with the first move **q**, to which Player can react with either **tt** or **ff**.

Just like **PRRel**, strategies give a “proof-relevant” account of execution, in the sense that moves and configurations of the game can have multiple witnesses in the strategy. For example, on the left below, **b** and **c** are mapped to the same move **tt**:

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

Note that we denote immediate causality by $\to$ in strategies, while we use dotted lines for games. This lets us represent the strategy in a single diagram, as on the right above.

4.1.3. *Morphisms between strategies.* For $\sigma$ and $\tau$ two strategies on $A$, a **morphism** from $\sigma$ to $\tau$, written $f: \sigma \Rightarrow \tau$, is a map of event structures $f: \sigma \to \tau$ preserving the dependency relation $\le$ (we say it is **rigid**) and such that $\partial_\tau \circ f = \partial_\sigma$.
4.1.4. **+-covered configurations.** We now describe a useful technical tool: a strategy is completely characterized by a subset of its configurations, called +-covered.

For a strategy $\sigma$ on a game $A$, a configuration $x \in \mathscr{C}(\sigma)$ is **+-covered** if all its maximal events are positive, so every Opponent move has at least one Player successor. We write $\mathscr{C}^+(\sigma)$ for the partial order of +-covered configurations of $\sigma$. Those are fairly important, because morphisms between strategies may be entirely described through their action on +-covered configurations:

**Lemma 4.3.** Consider $\sigma, \tau : A$ two strategies on a plain game $A$. Assume there is a function

$$f : \mathscr{C}^+(\sigma) \to \mathscr{C}^+(\tau)$$

compatible with display maps and preserving unions. Then, there is a unique morphism of strategies $\hat{f} : \sigma \Rightarrow \tau$ such that for all $x \in \mathscr{C}^+(\sigma)$, $\hat{f}x = f x$.

This is [Cla24, Lemma 6.3.4]. We also mention the immediate consequence:

**Lemma 4.4.** Consider a plain game $A$, and strategies $\sigma, \tau : A$.

If $f : \mathscr{C}^+(\sigma) \cong \mathscr{C}^+(\tau)$ is an order-isomorphism such that $\partial_\tau \circ f = \partial_\sigma$, then there is a unique isomorphism of strategies $\hat{f} : \sigma \cong \tau$ such that for all $x \in \mathscr{C}^+(\sigma)$, $\hat{f}(x) = f(x)$.

**4.2. A double category of concurrent games and strategies.** We construct a double category whose objects are plain games, horizontal morphisms are strategies between games, vertical morphisms are maps of games, and 2-cells are morphisms of strategies. The main technical point is the composition of strategies.

4.2.1. *Strategies between games.* If $A$ is a plain game, its **dual** $A^\perp$ has the same components as $A$ except for the reversed polarity. In particular $\mathscr{C}(A) = \mathscr{C}(A^\perp)$. The **tensor** $A \otimes B$ of $A$ and $B$ is simply $A$ and $B$ side by side, with no interaction – its events are the tagged disjoint union $|A \otimes B| = |A| + |B| = \{1\} \times |A| \oplus \{2\} \times |B|$, and other components are inherited. We write $x_A \otimes x_B$ for the configuration of $A \otimes B$ that has $x_A \in \mathscr{C}(A)$ on the left and $x_B \in \mathscr{C}(B)$ on the right, informing an order-isomorphism

$$- \otimes - : \mathscr{C}(A) \times \mathscr{C}(B) \cong \mathscr{C}(A \otimes B). \qquad (4.1)$$

Finally, the **hom** $A \vdash B$ is $A^\perp \otimes B$. As above, its configurations are denoted $x_A \vdash x_B$ for $x_A \in \mathscr{C}(A)$ and $x_B \in \mathscr{C}(B)$.

**Definition 4.5.** A strategy from $A$ to $B$ is a strategy on the game $A \vdash B$. If $\sigma : A \vdash B$ and $x^\sigma \in \mathscr{C}(\sigma)$, by convention we write $\partial_\sigma(x^\sigma) = x_A^\sigma \vdash x_B^\sigma \in \mathscr{C}(A \vdash B)$.

Our first example of a strategy between games is the **copycat** strategy $c_A$, which is the identity morphism on $A$ in our bicategory, i.e. the horizontal identity. Concretely, copycat on $A$ has the same events as $A \vdash A$, but adds immediate causal links between copies of the same move across components, from the negative copy to the positive. By Lemma 4.4, the following characterizes copycat up to isomorphism.

**Proposition 4.6.** If $A$ is a game, there is an order-isomorphism

$$c_{(-)} : \mathscr{C}(A) \cong \mathscr{C}^{+}(c_A)$$

such that for all $x \in \mathscr{C}(A)$, $\partial_{c_A}(c_x) = x \vdash x$.

*Proof.* Follows from [Cla24, Lemma 6.4.4]. □
<figure><img src="image_12.png" /><figcaption>Figure 1: An example of matching but causally incompatible configurations, in the composition of $\sigma: U \to U$ and $\tau: U \to U \cup N$. The underlying games are left undefined, but can be recovered by removing the arrows $\to$. The configurations are matching on $U \to U$, but the arrows $\to$ impose incompatible orders (i.e. a cycle) between the two occurrences of $\checkmark$.</figcaption></figure>

### 4.2.2. *Composition.*
Consider $\sigma: A \vdash B$ and $\tau: B \vdash C$. We define their composition $\tau \odot \sigma: A \vdash C$. This is a dynamic model, and to successfully synchronize, $\sigma$ and $\tau$ must agree to play the same events in the same order; this is defined in two steps.

We say that configurations $x^\sigma \in \mathscr{C}(\sigma)$ and $x^\tau \in \mathscr{C}(\tau)$ are **matching** if they reach the same configuration on $B$, i.e. $x_B^\sigma = x_B^\tau = x_B$. If that is the case, it induces a synchronization (and we may then ask if that synchronization induces a deadlock). If all events of $x^\sigma$ and $x^\tau$ were in $B$, this synchronization would take the form of a bijection $x^\sigma \simeq x^\tau$. But some moves of $x^\sigma$ are in $A$ and some moves of $x^\tau$ are in $C$, so instead we form the bijection

$$ \varphi[x^\sigma, x^\tau] : x^\sigma \parallel x_C^\tau \stackrel{\partial_\sigma \parallel x_C^\tau}{\simeq} x_A^\sigma \parallel x_B \parallel x_C^\tau \stackrel{x_A^\sigma \parallel \partial_\tau^{-1}}{\simeq} x_A^\sigma \parallel x^\tau $$

where $x \parallel y$ is the tagged disjoint union. This uses the fact that from the conditions on maps of event structures, $\partial_\sigma: x^\sigma \simeq x_A^\sigma \vdash x_B^\sigma$ is a bijection and likewise for $\partial_\tau$.

Now that the synchronization is formed, we import the causal constraints of $\sigma$ and $\tau$ to (the graph of) $\varphi[x^\sigma, x^\tau]$, via (with $m, m' \in x^\sigma \parallel x_C^\tau$ and $n, n' \in x_A^\sigma \parallel x^\tau$):

$$ (m, n) \triangleleft_\sigma (m', n') \Leftrightarrow m <_{\sigma \parallel C} m' $$

$$ (m, n) \triangleleft_\tau (m', n') \Leftrightarrow n <_{A \parallel \tau} n' $$

letting us finally say that matching $x^\sigma$ and $x^\tau$ are **causally compatible** if $\triangleleft = \triangleleft_\sigma \cup \triangleleft_\tau$ on (the graph of) $\varphi[x^\sigma, x^\tau]$ is acyclic. In particular, $x^\sigma$ and $x^\tau$ in Figure 1 are not causally compatible, the synchronization induces a deadlock.

The **composition** of $\sigma$ and $\tau$ is the unique (up to iso) strategy whose $+-$covered configurations are essentially causally compatible pairs of $+-$covered configurations. Write $\mathbf{CC}(\sigma, \tau)$ for the set of causally compatible pairs $(x^\sigma, x^\tau) \in \mathscr{C}^+(\sigma) \times \mathscr{C}^+(\tau)$, ordered componentwise.

**Proposition 4.7.** *Consider strategies $\sigma: A \vdash B$ and $\tau: B \vdash C$.*

*There is a strategy $\tau \odot \sigma: A \vdash C$, unique up to isomorphism, with an order-isomorphism*

$$ - \odot - : \mathbf{CC}(\sigma, \tau) \cong \mathscr{C}^+(\tau \odot \sigma) $$

s.t. for all $x^\sigma \in \mathscr{C}^+(\sigma)$ and $x^\tau \in \mathscr{C}^+(\tau)$ causally compatible,

$$ \partial_{\tau \odot \sigma} (x^\tau \odot x^\sigma) = x_A^\sigma \vdash x_C^\tau. $$
*Proof.* See [Cla24, Proposition 6.2.1]. □

This description of composition emphasizes the conceptual difference between a static model, in which composition is based on matching pairs as in (2.2), and a dynamic model, based on causal compatibility and sensitive to deadlocks.

**4.2.3. The double category $\mathbb{CG}$**. We assemble strategies and games into a general compositional framework. This is a double category whose vertical morphisms are maps of event structures, which compose strictly, and whose horizontal morphisms are strategies between games, which compose weakly. Altogether, we get:

**Theorem 4.8.** *There is a double category $\mathbb{CG}$ with components as follows:*

• objects are plain games;

• vertical morphisms $A \to B$ are polarity-preserving rigid maps of event structures $A \to B$ (also referred to as maps of games);

• horizontal morphisms $A \dashrightarrow B$ are strategies on $A \vdash B$;

• 2-cells of type

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

are rigid maps $f : \sigma \to \tau$ such that the following diagram commutes

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

*We write $\mathbf{CG}$ for the horizontal bicategory $\mathbf{H}(\mathbb{CG})$. It is clear that 2-cells in the bicategory $\mathbb{CG}$ correspond to the morphisms of strategies described in Section 4.1.3.*

*Proof sketch.* We have already introduced most of the necessary components, and here we mention two final points.

First, the copycat construction is functorial, as required in a double category. More precisely, for a vertical morphism $h : A \to B$, there is a rigid map of event structures $\mathfrak{c}_h : \mathfrak{c}_A \to \mathfrak{c}_B$, defined to have the same action on events as $h \vdash h : (A \vdash A) \to (B \vdash B)$. This defines a 2-cell

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

in a functorial way.

Another remaining challenge is to define the “horizontal composition” of 2-cells

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

$$ \begin{tikzcd} A \arrow[r, "\tau \circled{\sigma}"] \arrow[d, "\sigma'"] & C \arrow[d] \\ h \arrow[d, "g \circled{f}"] & l \arrow[d] \\ A' \arrow[r, "\tau' "] & C' \arrow[r, "\tau' \circled{\sigma'}"] & C' \end{tikzcd} \quad (4.2) $$
given by the diagrams below

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

The two companion axioms are easy to verify.

**Proposition 4.10.** The double category $\mathbb{CG}$ has all companions of vertical isomorphisms.

Applying Theorem 3.8, we deduce:

**Corollary 4.11.** The bicategory $\mathbb{CG}$, equipped with the tensor product $\otimes$ and the associated structural data, is symmetric monoidal.

**4.3. A static collapse of concurrent games.** We are ready to define our first collapse from dynamic to static semantics. Formally, we describe an oplax double functor $\|-\| : \mathbb{CG} \to \mathbb{PRRel}$, where *oplax* means that composition is not preserved: instead we have globular 2-cells $\|\tau \odot \sigma\| \to \|\tau\| \circ \|\sigma\|$ which embed the causally compatible pairs into the matching pairs.

The image of a plain game $A$ is the set $\mathscr{C}(A)$. To a strategy $\sigma : A \vdash B$, we associate

$$ \|\sigma\|(x_A, x_B) = \{x^\sigma \in \mathscr{C}^+(\sigma) \mid \partial_\sigma(x^\sigma) = x_A \vdash x_B\} $$

yielding a proof-relevant relation $\|\sigma\|$ from $\mathscr{C}(A)$ to $\mathscr{C}(B)$. To a 2-cell

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

we associate the family of functions mapping $x^\sigma \in \|\sigma\|(x_A, x_B)$ to $f(x^\sigma) \in \|\sigma'\|(h(x_A), k(x_B))$, for $x_A \in A$ and $x_B \in B$.

**Proposition 4.6** induces an isomorphism of $\|\mathbb{C}_A\|$ with the identity proof-relevant relation. From Proposition 4.7 we obtain a function $\|\tau \odot \sigma\| \to \|\tau\| \circ \|\sigma\|$. This is non-invertible in general, because some matching pairs are not causally compatible (see Figure 1).

Finally, there is a bijection $\|A \otimes B\| \cong \|A\| \otimes \|B\|$ for games $A$ and $B$, which extends to an isomorphism of proof-relevant relations $\|\sigma \otimes \tau\| \cong \|\sigma\| \otimes \|\tau\|$, and a similar situation on 2-cells. Overall the double functor (strongly) preserves the symmetric monoidal structure.

**Theorem 4.12.** This data determines a monoidal oplax double functor $\|-\| : \mathbb{CG} \to \mathbb{PRRel}$.

We omit the proof, as the theorem is a special case of the more elaborate version to come, which includes symmetries. Note that, although this involves a lot of algebraic data, we emphasize that it would be incomparably harder to establish a similar result directly at the bicategorical level. (We discuss a lifting of this theorem to the respective bicategories in Section 6.2, when required for our applications in semantics.)
In summary, we can regard **CG** as a dynamic version of **PRRel**, where the witnesses in **PRRel** are reached over time and composition is sensitive to deadlocks.

## 5. ACCOMMODATING SYMMETRY

In this section, we look at a model of concurrent games enriched with symmetry, known as thin concurrent games [CCW19]. We start by explaining the basics of event structures with symmetry and thin concurrent games (Section 5.1). Then we explain how strategies in thin concurrent games can be viewed as distributors (Section 5.2). We then define the double category $\mathcal{T}\mathcal{C}\mathcal{G}$ (Section 5.3) and construct a monoidal oplax functor $\mathcal{T}\mathcal{C}\mathcal{G} \to \mathcal{D}\mathit{ist}$ (Section 5.4). Finally we discuss the exponential modality (Section 5.5).

**5.1. Symmetry and thin concurrent games.** Recall that we went from **PRRel** to **Dist** by replacing sets with groupoids. We now go from **CG** to **TCG** by replacing the set of configurations $\mathscr{C}(A)$ with a groupoid of configurations $\mathscr{S}(A)$ whose morphisms are chosen bijections called *symmetries*, that behave well with respect to the causal order.

**5.1.1. Event structures with symmetry.** Our model is based on the following notion of event structure with symmetry [Win07]:

**Definition 5.1.** An isomorphism family on $E$ is a groupoid $\mathscr{S}(E)$ having as objects all configurations, and as morphisms certain bijections between configurations, satisfying:

*restriction*: for all $\theta: x \simeq y \in \mathscr{S}(E)$ and $x \supseteq x' \in \mathscr{C}(E)$, there is $\theta' \supseteq \theta' \in \mathscr{S}(E)$ such that $\theta' : x' \simeq y'$.

*extension*: for all $\theta: x \simeq y \in \mathscr{S}(E)$, $x \subseteq x' \in \mathscr{C}(E)$, there is $\theta' \subseteq \theta' \in \mathscr{S}(E)$ such that $\theta' : x' \simeq y'$.

We call $(E, \mathscr{S}(E))$ an **event structure with symmetry (ess)**.

We refer to morphisms in $\mathscr{S}(E)$ as **symmetries**, and write $\theta: x \cong_E y$ if $\theta: x \simeq y$ with $\theta \in \mathscr{S}(E)$. The **domain** $\mathrm{dom}(\theta)$ of $\theta: x \cong_E y$ is $x$, and likewise its **codomain** $\mathrm{cod}(\theta)$ is $y$. A **map of ess** $E \to F$ is a map of event structures that preserves symmetry: the bijection

$$f\theta \quad \stackrel{\text{def}}{=} \quad fx \quad \stackrel{f^{-1}}{\cong} \quad x \quad \stackrel{\theta}{\cong} \quad y \quad \stackrel{f}{\cong} \quad fy,$$

is in $\mathscr{S}(F)$ for every $\theta: x \cong_E y$ (recall that $f$ restricted to any $y$ is bijective). This makes $f: \mathscr{S}(E) \to \mathscr{S}(F)$ a functor of groupoids.

We can define a 2-category **ESS** of ess, maps of ess, and natural transformations between the induced functors. For $f, g: E \to F$ such a natural transformation is necessarily unique [Win07], and corresponds to the fact that for every $x \in \mathscr{C}(E)$ the composite bijection

$$f x \quad \stackrel{f^{-1}}{\cong} \quad x \quad \stackrel{g}{\cong} \quad g x$$

via local injectivity of $f$ and $g$, is in $\mathscr{S}(F)$. So this is an equivalence, denoted $f \sim g$.
5.1.2. *Thin games.* We define games with symmetry. To match the polarized structure, a game is an ess with two sub-symmetries, one for each player (see e.g. [Mel03, CCW19, Paq22]).

**Definition 5.2.** A thin concurrent game (tcg) is a game $A$ with isomorphism families $\mathcal{S}(A), \mathcal{S}_+(A), \mathcal{S}_-(A)$ s.t. $\mathcal{S}_+(A), \mathcal{S}_-(A) \subseteq \mathcal{S}(A)$, symmetries preserve polarity, and

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

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

(3) if $\theta \in \mathcal{S}_+(A)$, $\theta \subseteq \theta' \in \mathcal{S}(A)$, then $\theta' \in \mathcal{S}_+(A)$,

where $\theta \subseteq^p \theta'$ is $\theta \subseteq \theta'$ with (pairs of) events of polarity $p$.

Elements of $\mathcal{S}_+(A)$ (resp. $\mathcal{S}_-(A)$) are called **positive** (resp. **negative**); they intuitively correspond to symmetries carried by positive (resp. negative) moves, and thus introduced by Player (resp. Opponent). We write $\theta : x \cong_A^- y$ (resp. $\theta : x \cong_A^+ y$) if $\theta \in \mathcal{S}_-(A)$ (resp. $\theta \in \mathcal{S}_+(A)$).

Each symmetry has a unique positive-negative factorization [Cla24, Lemma 7.1.18]:

**Lemma 5.3.** For $A$ a tcg and $\theta : x \cong_A z$, there are unique $y \in \mathcal{C}(A)$, $\theta_- : x \cong_A^- y$ and $\theta_+ : y \cong_A^+ z$ s.t. $\theta = \theta_+ \circ \theta_-.$

We extend with symmetry the basic constructions on games: the **dual** $A^{\perp}$ has the same symmetries as $A$, but $\mathcal{S}_+(A^{\perp}) = \mathcal{S}_-(A)$ and $\mathcal{S}_-(A^{\perp}) = \mathcal{S}_+(A)$; the **tensor** $A_1 \otimes A_2$ has symmetries of the form $\theta_1 \otimes \theta_2 : x_1 \otimes x_2 \cong_{A_1 \otimes A_2} y_1 \otimes y_2$, where each $\theta_i : x_i \cong_{A_i} y_i$, and similarly for positive and negative symmetries; the **hom** $A \vdash B$ is $A^{\perp} \otimes B$.

5.1.3. *Thin strategies.* We now define strategies on thin concurrent games:

**Definition 5.4.** Consider $A$ a tcg. A **strategy** on $A$, written $\sigma : A$, is an ess $\sigma$ equipped with a morphism of ess $\partial_\sigma : \sigma \to A$ forming a strategy in the sense of Definition 4.2, and such that:

(1) if $\theta \in \mathcal{S}(\sigma)$, $\partial_\sigma \theta \vdash_A (a^-, b^-)$, there are unique $\theta \vdash_\sigma (s, t)$ s.t. $\partial_\sigma s = a$ and $\partial_\sigma t = b$.

(2) if $\theta : x \cong_\sigma y$, $\partial_\sigma \theta \in \mathcal{S}_+(A)$, then $x = y$ and $\theta = \mathrm{id}_x$.

As before, a **strategy from A to B** is a strategy on $\sigma : A \vdash B$.

The first condition forces $\sigma$ to acknowledge Opponent symmetries in $A$; the notation $\theta \vdash_A (a, b)$ means $(a, b) \notin \theta$ and $\theta \cup \{(a, b)\} \in \mathcal{S}(A)$. The second condition is **thinness**: it means that any non-identity symmetry in the strategy must originate from Opponent.

5.1.4. *Comparison with the “saturated” approach.* The “thin” approach is only one possible way of adding symmetry to games. Other models (e.g. [BDER97a, CCW14, Mel19]) follow a different approach, where strategies satisfy a saturation condition.

We explain the difference in the language of concurrent games. Consider a strategy $\sigma : A$ on a tcg, in the sense of Definition 5.4 *without* conditions (1) and (2). The saturation
Proof. Existence by Lem. 5.5, uniqueness by (2) of Definition 5.4. □

Thus we may set $\|\sigma\|(\Omega_A, \Omega_B)(\theta_A^-, x^\sigma, \theta_B^+)$ as the positive witness $(\theta_A^-, y^\sigma, \theta_B^+)$ above.
This immediately gives us a distributor:

**Proposition 5.7.** We have $\|\sigma\| : \mathcal{S}(A)^{\text{op}} \times \mathcal{S}(B) \to \text{Set}$.

**5.3. The double category of thin concurrent games.** We now define the double category $\mathbb{T}\text{CG}$ of thin concurrent games. We have already defined the objects (tcgs, Definition 5.2) and the horizontal morphisms (thin strategies, Definition 5.4), so it remains to define the vertical morphisms and 2-cells, and appropriate compositions and identities.

**5.3.1. Vertical morphisms: maps between tcgs.** Recall that in $\mathbb{CG}$ the vertical morphisms between games are rigid maps of event structures preserving the polarity of moves. Here we define **maps of tcgs** $A \to B$ to be rigid maps of event structures with symmetry, preserving the polarity of moves, and preserving the polarity of symmetry bijections.

**5.3.2. 2-cells: morphisms of strategies.** We now define generalized morphisms between strategies. The 2-cells of $\mathbb{T}\text{CG}$ are more liberal than those in $\mathbb{CG}$, because there should be an isomorphism between two strategies which play symmetric – rather than equal – moves. Recall the 2-dimensional structure in **ESS**, given by the equivalence relation $\sim$ on morphisms (Section 5.1.1). For two maps $f, g : E \to A$ into a tcg, we write $f \sim^+ g$ if $f \sim g$ and for every $x \in \mathcal{C}(E)$ the symmetry obtained as the composition

$$f x \stackrel{f^{-1}}{\sim} x \stackrel{g}{\sim} gx,$$

witnessing $f \sim g$ for $x$, is positive.

**Definition 5.8.** Let $\sigma : A \vdash B$ and $\tau : C \vdash D$ be thin strategies, and let $h : A \to C$ and $k : B \to D$ be maps of tcgs. A **positive morphism of strategies** of type

$$\begin{array}{ccc}
A & \xrightarrow{\sigma} & B \\
h & \searrow & \downarrow f \\
C & \xrightarrow{\tau} & D
\end{array}$$

is a rigid map of ess $f : \sigma \to \tau$ s.t. the following diagram commutes up to positive symmetry:

$$\begin{array}{ccc}
\sigma & \xrightarrow{f} & \tau \\
\partial_{\sigma} & \searrow & \partial_{\tau} \\
A \vdash B & \xrightarrow{\sim} & C \vdash D.
\end{array}$$

i.e. $\partial_{\tau} \circ f \sim^{+} (h \vdash k) \circ \partial_{\sigma}$.

As a convention, if $f$ is a 2-cell as above, for $x^\sigma \in \mathcal{C}(\sigma)$ we write

$$f[x^\sigma] : (h \vdash k)(\partial_\sigma x^\sigma) \cong_A^+ \partial_\tau(f x^\sigma)$$

for the positive symmetry witnessing this.
5.3.3. **Composition and identity.** The composition of thin strategies $\sigma : A \vdash B$ and $\tau : B \vdash C$ is obtained by equipping $\tau \odot \sigma$ (Proposition 4.7) with an adequate isomorphism family. If $\mathcal{S}^+(\sigma)$ is the restriction of $\mathcal{S}(\sigma)$ to $+-$covered configurations, then we can write $\mathbf{CC}(\mathcal{S}^+(\sigma), \mathcal{S}^+(\tau))$ for the pairs $(\varphi^\sigma, \varphi^\tau)$ of symmetries which are matching, i.e. $\varphi_B^\sigma = \varphi_B^\tau$ and whose domain (and necessarily, codomain) are causally compatible.

**Proposition 5.9.** Consider $\sigma : A \vdash B$ and $\tau : B \vdash C$ thin strategies.

There is a unique symmetry on $\tau \odot \sigma$ with a bijection commuting with dom and cod

$$(- \odot -) : \mathbf{CC}(\mathcal{S}^+(\sigma), \mathcal{S}^+(\tau)) \approx \mathcal{S}^+(\tau \odot \sigma)$$

and compatible with display maps, i.e. $(\varphi^\tau \odot \varphi^\sigma)_A = \varphi_A^\sigma$ and $(\varphi^\tau \odot \varphi^\sigma)_C = \varphi_C^\tau$.

*Proof.* This follows from [Cla24, Proposition 7.3.1]. □

Most of the effort in organizing these components into a double category is due to the difficulty of composing 2-cells horizontally. Suppose we have a pair of 2-cells $f$ and $g$ as in (4.2), but where all components now have symmetry. Explicitly we have

$$\begin{tikzcd}
  \sigma \arrow[r, "f"] \arrow[d, "\partial_\sigma"] & \sigma' \arrow[d, "\sim^+"'] \\
  A \vdash B \arrow[r, "\sim^+", "h \vdash k"] & A' \vdash B'
\end{tikzcd}
\quad
\begin{tikzcd}
  \tau \arrow[r, "g"] \arrow[d, "\partial_\tau"] & \tau' \arrow[d, "\sim^+"'] \\
  B \vdash C \arrow[r, "\sim^+", "k \vdash l"] & B' \vdash C'
\end{tikzcd}$$

and we must define an appropriate map $g \odot f : \tau \odot \sigma \to \tau' \odot \sigma'$.

Recall (from the discussion following Theorem 4.8) that in the analogous situation in $\mathbb{C}G$, $g \odot f : \tau \odot \sigma \Rightarrow \tau' \odot \sigma'$ was characterized by $(g \odot f)(x^\tau \odot x^\sigma) = g(x^\tau) \odot f(x^\sigma)$. In $\mathbb{T}CG$ this simple description is no longer possible, as we may not have a matching situation $f(x^\sigma)_{B'} = g(x^\tau)_{B'}$. Instead, these two configurations are matching up to a symmetry

$$\theta_{x^\sigma, x^\tau}^{f,g} : f(x^\sigma)_{B'} \cong_{B'} g(x^\tau)_{B'}$$

obtained as $\theta_{x^\sigma, x^\tau}^{f,g} = g[x^\tau]_{B'} \circ f[x^\sigma]_{B'}^{-1}$. Fortunately, interaction of thin strategies supports a notion of synchronization *up to symmetry* [Cla24, Proposition 7.4.4]:

**Proposition 5.10.** Consider $x^\sigma \in \mathcal{C}^+(\sigma)$, $\theta : x_B^\sigma \cong_B x_C^\tau$, $x^\tau \in \mathcal{C}^+(\tau)$ **causally compatible**, i.e. the relation $\triangleleft$ induced on the graph of the composite bijection

$$x^\sigma \parallel x_C^\tau \stackrel{\partial_\sigma \parallel x_C^\tau}{\cong} x_A^\sigma \parallel x_B^\sigma \parallel x_C^\tau \stackrel{x_A^\sigma \parallel \theta \parallel x_C^\tau}{\cong} x_A^\sigma \parallel x_B^\tau \parallel x_C^\tau \stackrel{x_A^\sigma \parallel \partial_\tau^{-1}}{\cong} x_A^\sigma \parallel x^\tau$$

by $\langle\sigma\rangle_C$ and $\langle A \rangle_\tau$ as in Section 4.2.2, is acyclic – we also say the composite bijection is **secured**.

Then, there are unique $y^\tau \odot y^\sigma \in \mathcal{C}^+(\tau \odot \sigma)$ with symmetries $\varphi^\sigma : x^\sigma \cong_\sigma y^\sigma$ and $\varphi^\tau : x^\tau \cong_\tau y^\tau$, such that $\varphi_A^\sigma \in \mathcal{S}_-(A)$ and $\varphi_C^\tau \in \mathcal{S}_+(C)$, and $\varphi_B^\tau \circ \theta = \varphi_B^\sigma$.

In that case, we write $y^\tau \odot y^\sigma = x^\tau \odot_\theta x^\sigma$. With that notation, there is a unique positive morphism $g \odot f : \tau \odot \sigma \Rightarrow \tau' \odot \sigma'$ s.t. $(g \odot f)(x^\tau \odot x^\sigma) = g(x^\tau) \odot_{\theta_{x^\sigma, x^\tau}^{f,g}} f(x^\sigma)$. This serves as a definition of the horizontal composition of 2-cells, see [Paq20] or [Cla24, Theorem 7.4.13].

Finally, for the identity horizontal morphism in $\mathbb{T}CG$, we equip the copycat strategy $c_A : A \vdash A$ (Proposition 4.6) with the unique symmetry that has an iso

$$c_{(-)} : \mathcal{S}(A) \cong \mathcal{S}^{+}(c_A)$$

commuting with dom and cod, such that $\partial_{c_A}(c_\theta) = \theta \vdash \theta$.
The tensor product $\otimes$ of tcgs extends to a symmetric monoidal structure. We omit all of the details, as the situation is completely analogous to that in $\mathbb{C}G$, using that the symmetry is always handled componentwise in a tensor product of games. The following proposition assembles all of the structure defined in this section.

**Proposition 5.11.** There is a symmetric monoidal double category $\mathbb{T}\mathbb{C}G$, and a symmetric monoidal embedding $\mathbb{C}G \hookrightarrow \mathbb{T}\mathbb{C}G$.

Thus we have extended our basic model $\mathbb{C}G$ with symmetries. The new model supports an exponential modality, which we discuss in Section 5.5.

5.4. **An oplax functor $\mathbb{T}\mathbb{C}G \to \mathbb{Dist}$**. We now give the components of an oplax double functor $\mathbb{T}\mathbb{C}G \to \mathbb{Dist}$. We have already explained the action on objects and horizontal morphisms, by mapping every strategy to a distributor (Section 5.2). We turn to the action on vertical morphisms and 2-cells.

5.4.1. *From maps of tcgs to functors of groupoids.* If $A$ and $B$ are tcgs, and $l: A \to B$ is a map preserving symmetries, then the action of $l$ on configurations and symmetries determines a functor $\|l\|: \mathcal{S}(A) \to \mathcal{S}(B)$.

5.4.2. *From positive morphisms to natural transformations.* We must show that a 2-cell in $\mathbb{T}\mathbb{C}G$, say $f$ in the diagram below,

$$ \begin{tikzcd} \sigma \arrow[r, "f"] \arrow[d, "\partial_\sigma"] & \tau \arrow[d, "\sim"] \\ A \vdash B \arrow[r, "h \vdash k"', "\cong"] & C \vdash D \arrow[l, "\partial_\tau"'] \end{tikzcd} $$

determines a natural transformation of distributors $\|\sigma\|(x_A, x_B) \Rightarrow \|\tau\|(h(x_A), k(x_B))$. Its components are the functions

$$ \begin{array}{rcl} \|f\|_{x_A, x_B}: & \|\sigma\|(x_A, x_B) & \to \|\tau\|(h(x_A), k(x_B)) \\ & (\theta_A^-, x^\sigma, \theta_B^+) & \mapsto (\theta_C^x \circ h(\theta_A^-), f(x^\sigma), k(\theta_B^+) \circ \theta_D^{x-1}) \end{array} $$

for $x_A \in \mathcal{C}(A)$ and $x_B \in \mathcal{C}(B)$, where $\theta_C^x: h(x_A^\sigma) \cong_C^- f(x^\sigma)_C$ and $\theta_D^x: k(x_B^\sigma) \cong_D^+ f(x^\sigma)_D$ are determined by the commutative diagram above, by definition of $\sim^+$ (see Section 5.3). This is natural, as an application of Proposition 5.6.

5.4.3. **The unitor and compositor.** To complete the construction of the double functor $\|-\|$, we must define appropriate globular 2-cells. This double functor will be **oplax normal**, meaning that there are invertible **unitors** and non-invertible **compositors**. We define these in the next two propositions.

**Proposition 5.12.** Consider $A$ a tcg. Then, there is a natural iso

$$ \mathrm{pid}^A : \|\mathbb{c}_A\| \cong \mathcal{S}(A)[-, -] : \mathcal{S}(A)^{\mathrm{op}} \times \mathcal{S}(A) \to \mathrm{Set}. $$

*Proof.* Consider $(\theta^-, \mathbb{c}_z, \theta^+) \in \|\mathbb{c}_A\|(x, y)$, with $\theta^- : x \cong_A^- z$ and $\theta^+ : z \cong_A^+ y$. We set $\mathrm{pid}^A(\theta^-, \mathbb{c}_z, \theta^+) = \theta^+ \circ \theta^-$; naturality and invertibility follow from Lemma 5.3. $\square$

Likewise, for two strategies $\sigma: A \vdash B$ and $\tau: B \vdash C$, we have a compositor as follows.
**Proof.** There are three coherence diagrams to check for functoriality, involving only globular 2-cells. The preservation of the associator is straightforward. For the preservation of the unitor, we establish that the diagram of globular 2-cells

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

commutes for any $\sigma: A \vdash B$. For this, consider $w = (\theta_A^-, \mathbf{c}_{x_B^\sigma} \odot x^\sigma, \theta_B^+) \in \|\mathbf{c}_B \odot \sigma\|(x_A, x_B)$. We have $\mathbf{pcomp}(w) = ((\theta_A^-, x^\sigma, \mathrm{id}), (\mathrm{id}, \mathbf{c}_{x_B^\sigma}, \theta_B^+))$, sent by $\mathrm{pid} \bullet \|\sigma\|$ to $((\theta_A^-, x^\sigma, \mathrm{id}), \theta_B^+)$. Now

$$((\theta_A^-, x^\sigma, \mathrm{id}), \theta_B^+) = ((\theta_A^-, x^\sigma, \mathrm{id}), \mathrm{id}_{x_B} \cdot \theta_B^+) \\ \sim (\theta_B^+ \cdot (\theta_A^-, x^\sigma, \mathrm{id}_{x_B^\sigma}), \mathrm{id}_{x_B}) \\ = ((\theta_A^-, x^\sigma, \theta_B^+), \mathrm{id}_{x_B})$$

satisfying $\rho((\theta_A^-, x^\sigma, \theta_B^+), \mathrm{id}_{x_B}) = (\theta_A^-, x^\sigma, \theta_B^+)$ as required. The other coherence diagram for the unitor is symmetric.

We must additionally show that the double functor has a symmetric monoidal structure. All the necessary data is defined in the obvious way: we have a vertical transformation consisting of vertical isomorphisms

$$\|A\| \otimes \|B\| \xrightarrow{\cong} \|A \otimes B\|$$

and invertible 2-cells

$$\|A\| \otimes \|B\| \xrightarrow{\|\sigma\| \otimes \|\tau\|} \|A'\| \otimes \|B'\| \\ \cong \downarrow \qquad \downarrow \qquad \cong \\ \|A \otimes B\| \xrightarrow{\|\sigma \otimes \tau\|} \|A' \otimes B'\|$$

as well as a vertical isomorphism $I \cong \|I\|$ (we use the same $I$ for monoidal units in different categories) and an invertible 2-cell

$$\begin{array}{ccc} I & \xrightarrow{\mathrm{id}_I} & I \\ \cong \downarrow & \downarrow & \cong \\ \|I\| & \xrightarrow{\|\mathbf{c}_I\|} & \|I\| \end{array}$$

These must satisfy a small number of coherence axioms (see [GGV24, Def. 5.1]), which are all immediately verified. $\square$

At this point, we have defined an oplax double functor preserving the monoidal structure appropriately. This is not a pseudo double functor: in general, the compositor 2-cell is not invertible, as witnessed in the example of Figure 1. We will address this below in §6, by specializing the games and strategies we consider to ensure that no deadlock arises. Before that, we discuss another orthogonal issue: the collapse above does not preserve the exponential modality !.
5.5. **Difficulties with the exponential modality.** First, we recall how to construct an exponential modality on $\mathbb{T}\mathcal{C}\mathcal{G}$.

5.5.1. *An exponential modality in polarized $\mathbb{T}\mathcal{C}\mathcal{G}$.* For an ess $E$, the ess !E is an infinitary symmetric tensor product, where the elements of the indexing set are called **copy indices**:

**Definition 5.16.** Consider $E$ an ess. Then !E has: *events*, $|!E| = \mathbb{N} \times |E|$; *causality and conflict* inherited transparently. The *isomorphism family* $\mathcal{S}(!E)$ comprises all bijections

$$ \theta : \|_{i \in \mathbb{N}} x_i \approx \|_{i \in \mathbb{N}} y_i $$

between configurations such that there is a bijection $\pi : \mathbb{N} \approx \mathbb{N}$ and for every $i \in \mathbb{N}$, a symmetry $\theta_i : x_i \cong_A y_{\pi(i)}$, such that for every $(j, a) \in |!E|$, we have $\theta(j, a) = (\pi(j), \theta_j(a))$.

To extend this to tcgs, we must treat separately the positive and negative symmetries. We explained earlier that intuitively, symmetries that only change the copy indices of negative moves should be negative, and likewise for positive moves – but this naive definition does not yield a tcg in general [CCW19]. To obtain a sensible extension of ! to tcgs, we must restrict to a polarized setting in which tcgs are **negative**, meaning that all minimal events are negative. For a negative tcg $A$, a symmetry $\theta \in \mathcal{S}(!A)$ is in the sub-family $\mathcal{S}_-(!A)$ if each $\theta_i$ in Definition 5.16 is negative in $\mathcal{S}(A)$, whereas $\theta$ is in $\mathcal{S}_+(!A)$ if each $\theta_i$ is in $\mathcal{S}_+(A)$ and **additionally** $\pi$ is the identity bijection. This extends to a horizontal double comonad on the sub-double-category $\mathbb{T}\mathcal{C}\mathcal{G}^-$ of *negative* tcgs – this is detailed for instance in [Paq20].

5.5.2. *Our functor does not preserve the modality.* However, in this paper we shall not adopt that exact construction, because that exponential modality ! on $\mathbb{T}\mathcal{C}\mathcal{G}^-$ is not preserved by the oplax functor of Theorem 5.15. We illustrate with an example:

**Example 5.17.** Consider $I$ the empty tcg.

Then, the two groupoids $\mathcal{S}(!I)$ and $\mathbf{Sym}(\mathcal{S}(I))$ are not equivalent in general. Indeed, !I is still empty so that $\mathcal{S}(!I)$ is a singleton groupoid. In contrast, $\mathbf{Sym}(\mathcal{S}(I))$ includes

$$ \emptyset, \emptyset\emptyset, \emptyset\emptyset\emptyset, \dots, $$

i.e. countably many non-isomorphic objects.

Intuitively, the relational model and its relatives such as $\mathbf{Dist}$ record how many times we “do nothing”, whereas $\mathbb{T}\mathcal{C}\mathcal{G}$ only records when we do something. Thus, although one can construct a cartesian closed Kleisli bicategory from the restriction of $\mathbb{T}\mathcal{C}\mathcal{G}$ to negative games [Paq20], the functor $\| - \|$ will not preserve cartesian closed structure.

We shall resolve this in §7 by adopting a notion of games where not all configurations are considered “valid” and correspond to a point of the web in the relational model. Before we do that, let us address the oplax aspect of our collapse.
## 6. VISIBLE STRATEGIES AND A PSEUDOFUNCTOR

A fundamental difference between dynamic and static models is the ability for dynamic models to detect deadlocks, via the causal nature of strategies. This situation is encapsulated in the “oplax-ness” of the double functor $\|-\| : \mathbb{T}\mathcal{C}\mathcal{G} \to \mathcal{D}\mathit{ist}$. In this section, we show how to restrict the games and strategies so that deadlocks never occur, which resolves the mismatch and gives a pseudo double functor, that preserves composition up to iso. To perform this restriction, we import from [Cla24] the mechanism of visibility. This gives a new double category $\mathbb{V}\mathit{is}$. In this new setting, the symmetric monoidal oplax double functor of Theorem 5.15 becomes a symmetric monoidal pseudo double functor $\mathbb{V}\mathit{is} \to \mathcal{D}\mathit{ist}$. The restriction to $\mathbb{V}\mathit{is}$ is significant, e.g. the game model of mutable state [CC24, Cla24] is no longer included, but we retain a model of the $\lambda$-calculus.

### 6.1. The double category $\mathbb{V}\mathit{is}$. We first introduce the restricted double category $\mathbb{V}\mathit{is}$.

Games and strategies in $\mathbb{T}\mathcal{C}\mathcal{G}$ are very general, and mostly independent of the specific computational paradigms they represent. In contrast, in $\mathbb{V}\mathit{is}$, all games are close to those obtained by the interpretation of simple types, and strategies are somewhat close to those needed to model $\lambda$-terms. (We do have a bit more: for instance, $\mathbb{V}\mathit{is}$ supports pure parallel higher-order computation [CCW15].)

#### 6.1.1. Arenas.
The objects of our refined model are called arenas. Arenas narrow down the causal structure to an alternating forest, required for the definition of visible strategies.

**Definition 6.1.** An arena is a tcg $A$ such that

(1) if $a_1, a_2 \leqslant_A a_3$ then $a_1 \leqslant_A a_2$ or $a_2 \leqslant_A a_1$,

(2) if $a_1 \to_A a_2$, then $\mathrm{pol}_A(a_1) \neq \mathrm{pol}_A(a_2)$.

Moreover, $A$ is called a **--arena** if $A$ is negative as a tcg.

The dual, tensor and hom operations on tcgs preserve arenas.

A key consequence of this definition is that any non-minimal $a \in A$ has a unique causal predecessor, called its **justifier**, and denoted $j(a) \in A$ with $j(a) \to_A a$.

#### 6.1.2. Visible strategies.
Visibility captures a property of purely-functional parallel programs, in which threads may fork and join but each should be a well-formed stand-alone sequential execution. In an event structure $E$, a thread is formalized as a **grounded causal chain** ($\mathbf{gcc}$), i.e. a finite set $\rho \subseteq_f |E|$ on which $\leq_E$ is a total order, forming a sequence

$$ \rho_1 \to_E \dots \to_E \rho_n $$

where $\rho_1$ is minimal in $E$. We write $\mathbf{gcc}(E)$ for the set of gccs. A gcc need not be a configuration (although it will always be if the strategy interprets a sequential program). A strategy is *visible* if gccs only reach valid states of the arena:

**Definition 6.2** [CCW15, Cla24]. Consider $A$ an arena. Then $\sigma : A$ is **visible** if it is:

*pointed*: for any $s \in \sigma$, there is a unique $\mathrm{init}(s) \leqslant_{\sigma} s$ minimal in $\sigma$, which is negative,

*valid-gccs*: for all $\rho \in \mathrm{gcc}(\sigma)$, $\partial_{\sigma}(\rho) \in \mathcal{C}(A)$.
A key consequence of this definition is that it equips all non-initial moves of $\sigma$ with a *justifier*, analogously to Hyland-Ong games: if $s \in \sigma$ is such that $\partial_\sigma s$ is non-initial, then $j(s)$ is the (unique) $s' \in \sigma$ such that $\partial_\sigma s' \to_A \partial_\sigma s$; if $\partial_\sigma s$ is initial but positive, we set $j(s) = \text{init}(s)$. Then, *visibility* entails the following fact: for any gcc in $\sigma$ of the form

$$ \rho = \rho_1 \dashv_E \dots \dashv_E \rho_n^+ , $$

the justifier $j(\rho_n^+)$ of $\rho_n^+$ must appear in $\rho$ – this is clearly analogous to the notion of *visibility* from Hyland-Ong games [HO00], explaining the terminology. The key property of visible strategies for us here is that their composition is always deadlock-free [Cla24, Lemma 10.4.8]:

**Lemma 6.3.** Consider $A, B, C$ --arenas, $\sigma : A \vdash B$ and $\tau : B \vdash C$ visible strategies, $x^\sigma \in \mathscr{C}(\sigma)$ and $x^\tau \in \mathscr{C}(\tau)$ with a symmetry $\theta : x_B^\sigma \cong_B x_B^\tau$.

Then, $x^\sigma, \theta, x^\tau$ are causally compatible in the sense of Proposition 5.10.

Copycat strategies on --arenas are visible, and visible strategies are closed under composition [Cla24], so we may consider the sub-double-category of $\mathcal{T}\mathcal{C}\mathcal{G}$ over the --arenas and the visible strategies, containing all vertical morphisms and 2-cells between them. We call this double category $\mathcal{V}\mathcal{I}\mathcal{S}$, and as usual we set $\mathcal{V}\mathcal{I}\mathcal{S} = \mathbf{H}(\mathcal{V}\mathcal{I}\mathcal{S})$, the bicategory of --arenas, visible strategies, and (globular) positive morphisms.

6.1.3. A pseudo double functor. By restriction of the components from Theorem 5.15, we have an oplax double functor

$$ \|-\| : \mathcal{V}\mathcal{I}\mathcal{S} \to \mathcal{D}\mathit{ist}. $$

This is actually a pseudo double functor, in that the compositor is invertible:

**Theorem 6.4.** We have a pseudo double functor $\|-\| : \mathcal{V}\mathcal{I}\mathcal{S} \to \mathcal{D}\mathit{ist}$.

*Proof.* We must show that for all $x_A \in \mathscr{C}(A)$ and $x_C \in \mathscr{C}(C)$, $\mathbf{pcomp}^{\sigma, \tau}(x_A, x_C)$ is a bijection. For surjectivity, consider

$$ \mathbf{w}^{\sigma} = (\theta_{A}^{-}, x^{\sigma}, \theta_{B}^{+}) \in \|\sigma\|(x_{A}, x_{B}) $$

$$ \mathbf{w}^{\tau} = (\theta_{B}^{-}, x^{\tau}, \theta_{C}^{+}) \in \|\tau\|(x_{B}, x_{C}) $$

composable witnesses. By Lemma 6.3, $(x^\sigma, \theta_B^- \circ \theta_B^+, x^\tau)$ is causally compatible. By Proposition 5.10, there are unique $y^\tau \odot y^\sigma \in \mathscr{C}^+(\tau \odot \sigma)$ along with $\varphi^\sigma, \varphi^\tau, \vartheta_A^-, \vartheta_C^+$ such that:

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

which, writing $\Theta_B = \varphi_B^\sigma \circ \theta_B^{+1} = \varphi_B^\tau \circ \theta_B^-$, entails

$$ \mathbf{v}^{\sigma} = (\vartheta_{A}^{-}, y^{\sigma}, \text{id}_{y_{B}}) = \Theta_{B} \cdot (\theta_{A}^{-}, x^{\sigma}, \theta_{B}^{+}) $$

$$ \mathbf{v}^{\tau} = (\text{id}_{y_B}, y^{\tau}, \vartheta_{C}^{+}) = (\vartheta_{B}^{-}, x^{\tau}, \theta_{C}^{+}) \cdot \Theta_{B} $$

so $(\mathbf{v}^\sigma, \mathbf{v}^\tau) = (\Theta_B \cdot \mathbf{w}^\sigma, \mathbf{v}^\tau) \sim (\mathbf{w}^\sigma, \mathbf{v}^\tau \cdot \Theta_B) = (\mathbf{w}^\sigma, \mathbf{w}^\tau)$. Now $(\mathbf{v}^\sigma, \mathbf{v}^\tau) = \mathbf{pcomp}^{\sigma, \tau}(\vartheta_A^-, y^\tau \odot y^\sigma, \vartheta_C^+)$, showing surjectivity.

Now, for injectivity, consider two witnesses

$$ (\theta_A^-, x^\tau \odot x^\sigma, \theta_C^+) \in \|\tau \odot \sigma\|(x_A, x_C), \quad (\vartheta_A^-, y^\tau \odot y^\sigma, \vartheta_C^+) \in \|\tau \odot \sigma\|(x_A, x_C), $$
s.t. $\mathbf{pcomp}(\theta_A^-, x^\tau \odot x^\sigma, \theta_C^+) \sim \mathbf{pcomp}(\vartheta_A^-, y^\tau \odot y^\sigma, \vartheta_C^+)$, i.e., there are components such that

$$((\theta_A^-, x^\sigma, \mathrm{id}), (\mathrm{id}, x^\tau, \theta_C^+)) = ((\theta_A^-, x^\sigma, \mathrm{id}), (\mathrm{id}, y^\tau, \vartheta_C^+) \cdot \Theta_B)$$

$$((\vartheta_A^-, y^\sigma, \mathrm{id}), (\mathrm{id}, y^\tau, \vartheta_C^+)) = (\Theta_B \cdot (\theta_A^-, x^\sigma, \mathrm{id}), (\mathrm{id}, y^\tau, \vartheta_C^+))$$

which by definition of the functorial action, means that

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

commutes for some $\varphi^\sigma : x^\sigma \cong_\sigma y^\sigma$ and $\psi^\tau : x^\tau \cong_\tau y^\tau$. So

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

has a positive display, hence is an identity symmetry by condition (2) of Definition 5.4 – thus from the diagram, $(\theta_A^-, x^\tau \odot x^\sigma, \theta_C^+) = (\vartheta_A^-, y^\tau \odot y^\sigma, \vartheta_C^+)$ as needed to conclude. $\square$

**6.2. Symmetric monoidal structure.** Visible strategies are closed under the tensor product $\otimes$, and so the symmetric monoidal structure in TCG restricts to Vis. Since all components restrict, we deduce that $\|-\| : Vis \to Dist$ is a symmetric monoidal (pseudo) double functor.

Applying Theorem 3.8, we obtain a symmetric monoidal pseudofunctor between the induced horizontal bicategories.

**Theorem 6.5.** *The horizontal restriction of the collapse double functor $\|-\|$ is a symmetric monoidal pseudofunctor of bicategories $\|-\| : Vis \to TCG$.*

We emphasize that this theorem makes essential use of the double categorical aspects, which makes the 2-dimensional symmetric monoidal structure manageable. Now that this is established, we can focus directly on the bicategorical structure, as we move towards applications in the semantics of the $\lambda$-calculus.

## 7. A CARTESIAN CLOSED PSEUDOFUNCTOR

The paper until this point has focused on the preservation of symmetric monoidal structure by our collapse functor. In this section we add further structure to Vis to ensure the preservation of the exponential modality, so that our collapse lifts to the Kleisli bicategory; we then show that the corresponding pseudofunctor is cartesian closed. This development is mostly independent from the preservation of the linear monoidal structure detailed above; mainly by lack of a mature bicategorical theory of models of linear logic.

To ensure preservation of the exponential modality, we must first address the mismatch identified in Section 5.5. We shall do that now, by introducing a mechanism that identifies those positions in games that correspond to points of the relational model.
<figure><img src="image_22.png" /><figcaption>Figure 2: Payoff tables for operations on arenas, with $A \mathcal{N} B = (A^{\perp} \otimes B^{\perp})^{\perp}$.</figcaption></figure>

**7.1. Payoff and winning.** The additional mechanism we import here is inspired from Melliès [Mel05]; see also the detailed construction in [Cla24]. As mentioned above, it helps in ignoring intermediate configurations arising in games which are not complete, i.e. they do not correspond to a valid state in relational models. In addition, this mechanism makes the ambient games model linear rather than affine; it forces strategies to explore all available resources, solving another mismatch between games and relational models.

**7.1.1. The bicategory Wis.** Here we construct a new bicategory of games and strategies, integrating both mechanisms of visibility and winning.

**Games with payoff.** Our new notion of game is that of a *board*:

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

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

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

where $a \sim_A a'$ means an **immediate conflict**, i.e. $a \#_A a'$ and it is not inherited.

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

$$ \textit{initialized: } \kappa_A(\emptyset) \geq 0. $$

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

The function $\kappa_A$ assigns a value to each configuration. Configurations with payoff 0 are called **complete**: they correspond to *terminated* executions, which have reached an adequate stopping point where all calls have adequately returned – we write $\mathcal{C}^0(A)$ for the set of complete configurations on $A$. Otherwise, $\kappa_A$ assigns a responsibility for non-completeness. If $\kappa_A(x) = -1$ then Player is responsible, otherwise it is Opponent.

The earlier constructions on arenas specialize into constructions on boards. If $A$ is a board, then the **dual** $A^{\perp}$ has payoff $\kappa_{A^{\perp}} = -\kappa_A$. If $A$ and $B$ are boards, then we set the **tensor** (*resp.* the **par**) as having as underlying arena the tensor, and payoff $\kappa_{A \otimes B}(x_A \otimes x_B) = \kappa_A(x_A) \otimes \kappa_B(x_B)$ (*resp.* $\kappa_{A \mathcal{N} B}(x_A \otimes x_B) = \kappa_A(x_A) \mathcal{N} \kappa_B(x_B)$), using the operations on payoff defined in Figure 2. If $A, B$ are **--boards**, then the **hom-board** is defined as $A \vdash B = A^{\perp} \mathcal{N} B$, i.e. with $\kappa_{A \vdash B} = \kappa_{A^{\perp}}(x_A) \mathcal{N} \kappa_B(x_B)$.

Note that by definition of payoff, the order-isomorphism of (4.1) refines to bijections:

$$ - \otimes - : \mathcal{C}^0(A) \times \mathcal{C}^0(B) \cong \mathcal{C}^0(A \otimes B), \qquad (7.1) $$

$$ - \mathcal{N} - : \mathcal{C}^0(A) \times \mathcal{C}^0(B) \cong \mathcal{C}^0(A \mathcal{N} B). \qquad (7.2) $$
**Winning strategies.** We turn to strategies. The payoff is taken into account in the definition, as follows:

**Definition 7.2.** Consider A a board, and $\sigma: A$ a visible strategy.

We say that $\sigma$ is **winning** if for all $x^\sigma \in \mathscr{C}^+(\sigma)$, we have $\kappa_A(\partial_\sigma x^\sigma) \ge 0$.

It is rather easy to show that copycat strategies are winning, and that winning strategies are stable under composition [Cla24, Proposition 8.2.15]. Thus we obtain a bicategory **Wis** with objects the $--$boards, morphisms from A to B the winning strategies on $A \vdash B$, and 2-cells the positive morphisms.

**7.1.2. Adjusting the pseudofunctor.** We now show how to adjust the pseudofunctor of Section 6.1.3 to account for the new structure we have just introduced.

Firstly, as before, to each $--$board A we shall associate a groupoid. However, it shall not be the groupoid $\mathscr{S}(A)$ of symmetries between all configurations as before, instead we set $\|A\|$ as the groupoid $\mathscr{G}(A)$ having as objects the set $\mathscr{C}^0(A)$ of configurations of null payoff, with morphisms from $x_A$ to $y_A$ still comprising all the symmetries in A.

The same definition as in Section 5.2 now yields a distributor

$$ \|\sigma\| : \|A\|^{\text{OP}} \times \|B\| \to \text{Set} $$

with those restricted groupoids – we keep the same definition for $\|\sigma\|$, which should cause no confusion as this notation shall remain fixed until the end of the paper. As before, we have:

**Theorem 7.3.** We have $\|-\| : \text{Wis} \to \text{Dist}$ a pseudofunctor.

*Proof.* The new definition of $\mathscr{G}(A)$ imposes only one new proof obligation, namely that for $\sigma: A \vdash B$, $\tau: B \vdash C$, $x_A \in \mathscr{G}(A)$ and $x_C \in \mathscr{G}(B)$, then

$$ \mathrm{pcomp}_{x_A, x_C}^{\sigma, \tau} : \|\tau\odot\sigma\|(x_A, x_C) \to (\|\tau\| \bullet \|\sigma\|)(x_A, x_C) $$

as defined in the proof of Proposition 5.13, is still well-defined. Indeed, it sends a witness $(\theta_A^-, x^\tau \odot x^\sigma, \theta_C^+)$ $\in \|\tau\odot\sigma\|(x_A, x_C)$ to (the equivalence class of) the pair

$$ ((\theta_A^-, x^\sigma, \mathrm{id}_{x_B}), (\mathrm{id}_{x_B}, x^\tau, \theta_C^+)) \in (\|\tau\| \bullet \|\sigma\|)(x_A, x_C) $$

for $x_B^\sigma = x_B^\tau = x_B$, exploiting that $x^\sigma$ and $x^\tau$ are matching; but this assumes that $(\theta_A^-, x^\sigma, \mathrm{id}_{x_B}) \in \|\sigma\|(x_A, x_B)$ and $(\mathrm{id}_{x_B}, x^\tau, \theta_C^+) \in \|\tau\|(x_B, x_C)$, which only makes sense provided $x_B$ has null payoff (and thus lies in $\|B\|$). Thus seeking a contradiction, assume that $\kappa_B(x_B) = 1$. But then $\kappa_{B \perp \mathscr{N}_C}(\partial_\tau(x^\tau)) = -1 \mathscr{N} 0 = -1$, which is impossible since $x^\tau \in \mathscr{C}^+(\tau)$ and $\tau$ is winning. Symmetrically if $\kappa_B(x_B) = -1$ then this contradicts that $\sigma$ is winning since $x^\sigma \in \mathscr{C}^+(\sigma)$. Hence, $\kappa_B(x_B) = 0$ as required.

The other components of the pseudofunctor remain unchanged. $\square$

But we are not just interested in **Wis** and **Dist**: we need a pseudofunctor relating the Kleisli bicategories for the corresponding exponential modalities in the two models.

**7.2. The exponential modality on Wis.** First, we detail the construction of the exponential modality on **Wis** (written !), along with its algebraic structure.
### 7.2.1. The exponential modality for boards.
The construction of !A as a countable symmetric tensor of copies of A (Section 5.5) can be extended to --boards. Note that any configuration of !A has a representation as $\|_{i \in I} x_i$ for $I \subseteq_f \mathbb{N}$, and this representation is unique if we insist that every $x_i$ is non-empty. Using that, we set (all $x_i$ below are non-empty):

$$ \kappa_{!A} : \mathscr{C}(!A) \to \{-1, 0, +1\} \\ \|_{i \in I} x_i \mapsto \bigotimes_{i \in I} \kappa_A(x_i) $$

that is well-defined because $\otimes$ is associative on $\{-1, 0, +1\}$. If A is a --board, then this results in a --board; but !A is never strict, even if A is strict.

### 7.2.2. Strict boards.
To precisely capture the relationship between ! and **Sym** we use **strict** boards (Def. 6.1), where $\emptyset$ has payoff 1 and is not considered complete. Indeed, the situation with the empty configuration was at the heart of the issue in Section 5.5.2. We now state the following key property: for strict boards, the two constructions **Sym** and ! are equivalent.

**Proposition 7.4.** Consider a strict board A. There is an adjoint equivalence of categories:

$$ L_A^! : \mathbf{Sym}(\mathscr{G}(A)) \simeq \mathscr{G}(!A) : R_A^! $$

*Proof.* We first show that we can identify the objects of $\mathscr{G}(!A)$ with families $(x_i)_{i \in I}$ of objects of $\mathscr{G}(A)$, where $I$ is a finite subset of natural numbers. We observed above that any configuration $x \in \mathscr{C}(!A)$ can be uniquely written as $x = \|_{i \in I} x_i$ where $I \subseteq_f \mathbb{N}$, and $x_i \in \mathscr{C}(A)$ is non-empty for all $i \in I$; yielding a family $(x_i)_{i \in I}$. In addition, as $\kappa_{!A}(x) = 0$, by definition of the tensor on payoff values we must have $\kappa_A(x_i) = 0$ for every $i \in I$, i.e. $x_i \in \mathscr{G}(A)$. This representation of $x \in \mathscr{G}(!A)$ as a family $(x_i)_{i \in I}$ is clearly injective. Surjectivity boils down to the fact that each $x_i$ is non-empty, which follows from $\kappa_A(x_i) = 0$ since A is strict.

Thus, from right to left, $R_A^!$ sends $(x_i)_{i \in I}$ to the sequence $x_{i_1} \dots x_{i_n}$ for $I = \{i_1, \dots, i_n\}$ sorted in increasing order. From left to right, $L_A^!$ sends $x_1 \dots x_n$ to $(x_i)_{i \in \{1 \dots n\}}$. $\square$

Although this equivalence only holds for strict arenas, it shall suffice for our purposes.

From now on, we use implicitly and without further mention the representation of complete configurations of !A as families of complete configurations of A.

### 7.2.3. Relative pseudocomonads.
The pseudofunctor **Wis** $\to$ **Dist** does not preserve the exponential modality as a pseudocomonad on **Wis**, but as a pseudocomonad *relative* to the sub-bicategory of strict arenas. We recall the categorical notions.

Recall that a monad on category $\mathcal{C}$ relative to a functor $J : \mathcal{D} \to \mathcal{C}$ is a functor $T : \mathcal{D} \to \mathcal{C}$ with a restricted monadic structure, which we can use to form a Kleisli category $\mathcal{C}_T$ with objects those of $\mathcal{D}$. (Often, $\mathcal{D}$ is a sub-bicategory of $\mathcal{C}$ and $J$ is the inclusion functor.) This generalizes to relative pseudomonads [FGHW18] and pseudocomonads:

**Definition 7.5.** Consider $J : \mathcal{C} \to \mathcal{D}$ a pseudofunctor between bicategories. A relative pseudocomonad $T$ over $J$ consists of:

(1) an object $TX \in \mathcal{D}$, for every $X \in \mathcal{C}$,

(2) a family of functors $(-)_X^* : \mathcal{D}[TX, JY] \to \mathcal{D}[TX, TY]$,

(3) a family of morphisms $i_X \in \mathcal{D}[TX, JX]$,

(4) a natural family of invertible 2-cells, for $f \in \mathcal{D}[TX, JY]$ and $g \in \mathcal{D}[TY, JZ]$:

$$ \mu_{f,g} : (g \circ f^*)^* \stackrel{\sim}{\Rightarrow} g^* \circ f^* $$
<figure><img src="image_23.png" /><figcaption>Figure 3: Coherence conditions for relative pseudocomonads</figcaption></figure>

(5) a natural family of invertible 2-cells, for $f \in \mathcal{D}[TX, JY]$:

$$ \eta_f : f \xrightarrow{\approx} i_Y \circ f^* $$

(6) a family of invertible 2-cells $\theta_X : i_X^* \xrightarrow{\approx} \mathrm{id}_{TX}$, where $X, Y, Z$ range over objects of $\mathcal{C}$, subject to the coherence conditions in Figure 3.

Those conditions are just what is needed to form a Kleisli bicategory written $\mathcal{D}_T$, with objects those of $\mathcal{C}$, morphisms and 2-cells from $X$ to $Y$ the category $\mathcal{D}[TX, JY]$. We can compose $f \in \mathcal{D}[TX, JY]$ and $g \in \mathcal{D}[TY, JZ]$ as $g \circ_T f = g \circ f^*$, and the identity on $X$ is $i_X$.

### 7.2.4. The exponential relative pseudocomonad.
We now form a concrete relative pseudocomonad on **Wis**. Here, **C** is the sub-bicategory **Wis**<sub>s</sub> of strict arenas, and **J**: **Wis**<sub>s</sub> $\hookrightarrow$ **Wis** the embedding. Note that even if **A** is strict, !**A** is not strict, and so ! is not an endo(pseudo)functor; instead we have !: **Wis**<sub>s</sub> $\to$ **Wis**.

We now outline the components in Definition 7.5. For the component (2), we must introduce additional notions. Fix an injection $\langle-, -\rangle$: $\mathbb{N}^2 \to \mathbb{N}$. If $I \subseteq_f \mathbb{N}$ and $J_i \subseteq_f \mathbb{N}$ for all $i \in I$, write $\sqcup_{i \in I} J_i \subseteq_f \mathbb{N}$ for the set of all $\langle i, j \rangle$ for $i \in I$ and $j \in J_i$. Then, we may define:

**Definition 7.6.** Consider $\sigma \in \mathbf{Wis}[!A, B]$. Its promotion $\sigma^!$ has ess $!\sigma$, and display map the unique map of ess such that

$$ \partial_{\sigma^!}((x^{\sigma,i})_{i \in I}) = (x_{A,j}^{\sigma,i})_{\langle i,j \rangle \in \sqcup_{i \in I} J_i} \vdash (x_B^{\sigma,i})_{i \in I} \quad (7.3) $$

where $\partial_{\sigma}(x^{\sigma,i}) = (x_{A,j}^{\sigma,i})_{j \in J_i} \vdash x_B^{\sigma,i}$ for all $i \in I$.

For (3), the dereliction $\mathrm{der}_A \in \mathbf{Wis}[!A, A]$ on strict $A$ has ess $\mathfrak{c}_A$, and display map $\partial_{\mathrm{der}_A}(\mathfrak{c}_x) = (x)_{\{0\}} \vdash x$. For (4), we shall use a positive isomorphism

$$ \mathrm{join}_{\sigma, \tau} : (\tau \odot \sigma!)^! \xrightarrow{\approx} \tau! \odot \sigma! $$
sending $(x_i^T \odot (x_{i,j}^\sigma)_{j \in J_i})_{i \in I}$ to $(x_i^T)_{i \in I} \odot (x_{i,j}^\sigma)_{\langle i,j \rangle \in \text{L}_{i \in I} J_i}$. For (5), given $B$ strict and $\sigma \in \text{Wis}[!A, B]$ we have a positive iso runit$_\sigma$: $\sigma \cong \text{der}_B \odot \sigma^!$ sending $x^\sigma \in \mathscr{C}^+(\sigma)$ to $\mathscr{C}x_B^\sigma \odot (x^\sigma)_{\{0\}} \in \mathscr{C}^+(\text{der}_B \odot \sigma^!)$. Finally, for (6) we have lunit$_A$: $\text{der}_A^! \cong \mathscr{C}!_A$ sending $(\mathscr{C}_{x_i})_{i \in I}$ to $\mathscr{C}(x_i)_{i \in I}$. For all those, we use the fact that positive isos are entirely determined by their action on +-covered configurations, see e.g. [Cla24, Lemma 7.2.11].

Altogether, this gives us:

**Theorem 7.7.** *The components described above define a pseudocomonad ! relative to the embedding of Wis$_s$ into Wis.*

The naturality and coherence laws follow from lengthy but direct calculations, which we omit. In particular, there is a Kleisli bicategory **Wis**! whose objects are strict boards – in the next section we shall see that this is a cartesian closed bicategory.

**7.3. The exponential modality on Dist.** For the sake of relating **Wis** and **Dist**, we also need to properly introduce the exponential modality structure of **Sym**(-) on **Dist**, which we shall also present as a relative pseudocomonad to ease the correspondence.

**7.3.1. The groupoid Sym(A).** For $A$ a groupoid, the objects of **Sym**(A) are sequences of objects of $A$, written $\langle a_1, \dots, a_n \rangle$, or just $\langle a_i \rangle_{i \in n}$ – implicitly treating $n$ as the set $\{1, \dots, n\}$. There can be a morphism from $\langle a_i \rangle_{i \in n}$ to $\langle b_j \rangle_{j \in p}$ only when $n = p$, in which case it is a permutation $\pi$ on $n$, along with a family comprising $f_i \in A(a_{\pi(i)}, b_i)$ for each $i \in n$, written

$$ \langle f_i \rangle_{i \in n}^{\pi} \in \mathbf{Sym}(A)(\langle a_i \rangle_{i \in n}, \langle b_j \rangle_{j \in n}), $$

which we write simply as $\langle f_i \rangle_{i \in n}$ when $\pi$ is the identity. We insist that we have $f_i \in A(a_{\pi(i)}, b_i)$ rather than $f_i \in A(a_i, b_{\pi(i)})$: the family $(f_i)_{i \in n}$ is thought of as indexed by the codomain, not the domain. This distinction will make calculations easier later on.

We shall also write $\langle a_{i,j} \rangle_{i \in n, j \in p_i} \in \mathbf{Sym}(A)$ for the concatenated sequence $a_{1,j} \dots a_{n,j}$.

**7.3.2. Promotion and dereliction in Dist.** Next, we present the relative pseudocomonad structure on **Dist**. We follow Definition 7.5, even though this is not really relative; it shall be a pseudocomonad “relative” to the inclusion of **Dist** in **Dist**. For this structure, we shall keep the same notations as in Definition 7.5, to avoid notational collisions with the relative pseudocomonad in games.

We start with promotion. Recall that if $\alpha \in \text{Dist}(\mathbf{Sym}(A), B)$, the coend formula

$$ \alpha^{\dagger}(\vec{a}, \langle b_1, \dots, b_n \rangle) = \int^{\vec{a}_1, \dots, \vec{a}_n} \left( \prod_{i=1}^{n} \alpha(\vec{a}_i, b_i) \right) \times \mathbf{Sym}(A)[\vec{a}_1 \dots \vec{a}_n, \vec{a}] $$

yields a distributor $\alpha^{\dagger} \in \text{Dist}[\mathbf{Sym}(A), \mathbf{Sym}(B)]$, called the **promotion** of $\alpha$. Concretely, this means that witnesses in $\alpha^{\dagger}(\vec{a}, \langle b_1, \dots, b_n \rangle)$ consist in the choice of three components

$$ (\vec{a}_1, \dots, \vec{a}_n \in \mathbf{Sym}(A), \quad \langle s_i \rangle_{i \in n} \in \prod_{i=1}^{n} \alpha(\vec{a}_i, b_i), \quad f \in \mathbf{Sym}(A)[\vec{a}_1 \dots \vec{a}_n, \vec{a}]), \quad (7.4) $$

subject to the following equivalence relation, for each $(f_i \in \mathbf{Sym}(A)[\vec{a}_i, \vec{a}_i^\prime])_{1 \le i \le n}$:

$$ (\vec{a}_1, \dots, \vec{a}_n, \langle s_i \rangle_{i \in n}, f \circ (f_1 \dots f_n)) \sim (\vec{a}_1^\prime, \dots, \vec{a}_n^\prime, \langle \alpha(f_i, b_i)(s_i) \rangle_{i \in n}, f) \quad (7.5) $$
for $s_i \in \alpha(\vec{a}_i, b_i)$, $f \in \mathbf{Sym}(A)[\vec{a}'_1 \dots \vec{a}'_n, \vec{a}]$.

Here, we make some notational simplifications. Firstly, the data of the $\vec{a}_i$s is redundant, provided other components are typed. Secondly, writing $\vec{a}_i = \langle a_{i,1}, \dots, a_{i,p_i} \rangle$ and $\vec{a} = \langle a'_1, \dots, a'_p \rangle$, then a morphism $f \in \mathbf{Sym}(A)[\vec{a}'_1 \dots \vec{a}'_n, \vec{a}]$ is some $\langle f_i \rangle_{i \in p_i}^{\pi}$ for $\pi : p \simeq \sum_{i=1}^n p_i$; but up to (7.5) we can – and we will – always assume that the $f_i$s are identities, and only $\pi$ remains. So altogether, a witness in $\alpha^\dagger(\vec{a}, \langle b_1, \dots, b_n \rangle)$ as in (7.4) is specified by

$$ \langle s_i \rangle_{i \in n}^{\pi} \in \alpha^{\dagger}(\vec{a}, \langle b_1, \dots, b_n \rangle) $$

an expression where $s_i \in \alpha(\vec{a}_i, b_i)$ and $\pi : p \simeq \sum_{i=1}^n p_i$; from now on we fix this notation<fnref n="4" /> – note in passing that we may omit the permutation for the identity, e.g. $\langle s_i \rangle_{i \in n} = \langle s_i \rangle_{i \in n}^{\mathrm{id}}$.

For dereliction, we simply have $i_A(\langle a \rangle, a') = A[a, a']$.

**7.3.3. Additional components.** We carry on with the additional component of the relative pseudocomonad structure. For every $\alpha \in \mathrm{Dist}[\mathbf{Sym}A, B]$ and $\beta \in \mathrm{Dist}[\mathbf{Sym}B, C]$, we need

$$ \mu_{\alpha, \beta} : (\beta \bullet \alpha^{\dagger})^{\dagger} \cong \beta^{\dagger} \bullet \alpha^{\dagger} $$

a natural iso which, given $s_{i,j} \in \alpha(\vec{a}_{i,j}, b_{i,j})$ and $t_i \in \beta(\vec{b}_i, c_i)$ for $1 \le i \le n$, $1 \le j \le p_i$, $\vec{a}_{i,j} = \langle a_{i,j,1}, \dots, a_{i,j,k_{i,j}} \rangle$, $\pi_i : \sum_{j \in p_i} k_{ij} \simeq \sum_{j \in p_i} k_{ij}$ and $\pi : \sum_{i,j} k_{ij} \simeq \sum_{i,j} k_{ij}$, is set to

$$ (\mu_{\alpha, \beta})_{\vec{a}, \vec{c}}(\langle t_i \bullet \langle s_{i,j} \rangle_{j \in p_i}^{\pi_i} \rangle_{i \in n}^{\pi}) = \langle t_i \rangle_{i \in n} \bullet \langle s_{i,j} \rangle_{i \in n, j \in p_i}^{\pi \circ \sum \pi_i} $$

For cancellation of dereliction we need, for any $\alpha \in \mathrm{Dist}[\mathbf{Sym}A, B]$, natural isos

$$ \eta_{\alpha} : \alpha \cong i_B \bullet \alpha^{\dagger}, $$

$$ \theta_A : i_A^{\dagger} \cong \mathrm{id}_{\mathbf{Sym}A} $$

set by $(\eta_{\alpha})_{\vec{a},b}(s) = \mathrm{id}_b \bullet \langle s \rangle$ for $s \in \alpha(\vec{a}, b)$; and $\theta_A(\langle f_i \rangle_{i \in n}^{\pi}) = \langle f_i \rangle_{i \in n}^{\pi}$ for $(f_i \in A[a_i, a'_i])_{i \in n}$.

**Theorem 7.8.** This specifies a (relative) pseudocomonad Sym on Dist.

As usual, we refer to the Kleisli bicategory $\mathrm{Dist}_{\mathbf{Sym}}$ as $\mathrm{Esp}$.

**7.4. Lifting $\|\|$ to the Kleisli bicategories.** We show how to lift $\|\|$ to a pseudofunctor $\|\| : \mathrm{Wis}_I \to \mathrm{Esp}$. (We give a direct proof, although one could write down a notion of pseudofunctor between relative pseudocomonads that lifts to the Kleisli bicategories [Str72].)

Before we delve into the proof, we introduce some additional notation.

**7.4.1. Additional conventions and notations.** If $X$ is a set, write $\mathbf{Fam}(X)$ for the set of families $(x_i)_{i \in I}$ indexed by $I \subseteq f \mathbb{N}$. This also applies to categories: if $A$ is a category, then $\mathbf{Fam}(A)$ has morphisms from $(x_i)_{i \in I}$ to $(y_j)_{j \in J}$ given by a permutation $\pi : I \simeq J$, and a family $(f_i : x_i \to y_{\pi(i)})_{i \in I}$ of morphisms in $A$ – so that $\mathcal{G}(!A) \cong \mathbf{Fam}(\mathcal{G}(A))$. If $I$ is a finite subset of natural numbers, let $|I|$ be its cardinal and $\kappa_I : I \simeq |I|$ be the unique monotone bijection. If $(x_i)_{i \in I}$ is a family, for simplicity we write $(x_i)_{i \in |I|}$ for the reindexing $(x_{\kappa_I^{-1}(j)})_{j \in |I|}$. Similarly, if $I \subseteq f \mathbb{N}$ and $(J_i)_{i \in I}$ is a family with $J_i \subseteq f \mathbb{N}$ for all $i \in I$, we write

$$ \kappa_{I, (J_i)} : \bigsqcup_{i \in I} J_i \simeq \sum_{i \in I} |J_i| $$

for the bijection corresponding to arranging (encodings of) pairs $\langle i, j \rangle$ in lexicographic order.

<footnote n="4">⁴Note the double brackets, which we adopt to ease the distinction with morphisms of $\mathbf{Sym}(A)$.</footnote>
We also introduce a notation for morphisms in **Fam**(C), in line with the earlier notation introduced for **Sym**(A): we shall sometimes write $(f_j)_{j \in J}^{\pi}$ for the element of **Fam**(C)[$(x_i)_{i \in I}$, $(y_j)_{j \in J}$] normally consisting of

$$ (\pi^{-1} : I \simeq J, (f_{\pi^{-1}(i)} \in C[x_i, y_{\pi^{-1}(i)}])_{i \in I}). $$

Notice that the family is indexed by its target index set instead of the source.

### 7.4.2. Preservators for exponentials.
To lift $\|\cdot\|$ to the Kleisli bicategories, we must introduce explicit natural isomorphisms acting on witnesses for dereliction and promotion. We make repeated use of the actions of functors on distributors introduced in Definition 3.10.

**Lemma 7.9.** For any strict board A, there is a natural isomorphism

$$ \mathbf{pder}_A : \|\mathrm{der}_A\|[L_A^!] \cong i_{\mathscr{G}(A)} \in \mathrm{Dist}[\mathrm{Sym}(\mathscr{G}(A)), \mathscr{G}(A)] $$

*Proof.* From the definition, $\|\mathrm{der}_A\|[L_A^!](\langle x_i \rangle_{i \in n}, y)$ is non-empty iff $n=1$, in which case

$$ \begin{aligned} \|\mathrm{der}_A\|[L_A^!](\langle x \rangle, y) &= \|\mathrm{der}_A\|((x)_{i \in \{1\}}, y) \\ &= \{[(\theta^-)^{\{0\}} \approx^{\{1\}} \mathbf{c}_z \in \mathscr{C}^+(\mathrm{der}_A), \theta^+] | \theta^- : x \cong_A^- z, \theta^+ : z \cong_A^+ y\} \end{aligned} $$

where $\partial_{\mathrm{der}_A}(\mathbf{c}_z) = (z)_{\{0\}} \vdash z$. This is sent by $\mathbf{pder}_A$ to

$$ \theta^+ \circ \theta^- \in \mathrm{der}_{\mathscr{G}(A)}[\langle x \rangle, y] $$

which is a bijection by Lemma 5.3. Additional verifications are routine.

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

Likewise, there is another natural isomorphism for preservation of promotion:

**Lemma 7.10.** For any $\sigma \in \mathbf{Wis}[!A, B]$, there is a natural isomorphism

$$ \mathbf{pprom}_{\sigma} : \|\sigma'\|[L_A^!] \cong [R_B^!](\|\sigma\|[L_A^!])^{\dagger}, $$

between distributors in $\mathrm{Dist}[\mathrm{Sym}(\mathscr{G}(A)), \mathscr{G}(!B)]$. Furthermore, it is natural in $\sigma$.

*Proof.* Recall that $+\text{-covered configurations of } \sigma'$ correspond to families $(x^{\sigma',i})_{i \in I}$; and

$$ \partial((x^{\sigma',i})_{i \in I}) = (x_{A,j}^{\sigma',i})_{\langle i,j \rangle \in \bigsqcup_{i \in I} J_i} \vdash (x_B^{\sigma',i})_{i \in I} $$

provided $\partial(x^{\sigma',i}) = (x_{A,j}^{\sigma',i})_{j \in J_i} \vdash x_B^{\sigma',i}$ for all $i \in I$.

Now, consider $\langle x_{A,k} \rangle_{k \in p} \in \mathrm{Sym}(\mathscr{G}(A))$, and $(x_{B,l})_{l \in L} \in \mathscr{G}(!B)$. We have:

$$ \|\sigma'\|[L_A^!](\langle x_{A,k} \rangle_{k \in p}, (x_{B,l})_{l \in L}) = \|\sigma'\|((x_{A,k})_{k \in p}, (x_{B,l})_{l \in L}) $$

which, by definition, is composed of triples

$$ [(\theta_{i,j}^-)^{\pi}_{\langle i,j \rangle \in \bigsqcup_{i \in I} J_i}, (x^{\sigma',i})_{i \in I} \in \mathscr{C}^+(\sigma'), (\theta_l^+)^{\bar{\varpi}}_{l \in L}] \in \|\sigma'\|((x_{A,k})_{k \in p}, (x_{B,l})_{l \in L}) $$

where $\pi : \bigsqcup_{i \in I} J_i \cong p$ is a bijection, $\theta_{i,j}^- : x_{A,\pi\langle i,j \rangle} \cong_A^- x_{A,j}^{\sigma',i}$, and $(\theta_l^+)^{\bar{\varpi}}_L : (x_B^{\sigma',i})_{i \in I} \cong_{!B}^+ (x_{B,l})_{l \in L}$.

This can be simplified: the positivity of $(\theta_l^+)^{\bar{\varpi}}_L$ entails $L=I$ and $\bar{\varpi} = \mathrm{id}_I$. We are left with

$$ [(\theta_{i,j}^-)^{\pi}_{\langle i,j \rangle \in \bigsqcup_{i \in I} J_i}, (x^{\sigma',i})_{i \in I} \in \mathscr{C}^+(\sigma'), (\theta_i^+)^{\bar{\varpi}}_{i \in I}] \in \|\sigma'\|((x_{A,k})_{k \in p}, (x_{B,i})_{i \in I}). $$

We may finally define $\mathbf{pprom}_{\sigma}$ to send the above witness to:

$$ \langle\langle [(\theta_{i,j}^-)^{\kappa_{J_i}}_{j \in J_i}, x^{\sigma',i}, \theta_i^+] \rangle\rangle^{\bar{\pi}}_{i \in I | i \in I} \in (\|\sigma\|[L_A^!])^{\dagger}(\langle A, k \rangle_{k \in p}, \langle x_{B,i} \rangle_{i \in I | i \in I}) $$

where $\bar{\pi}$ is the unique bijection such that the composition $\bigsqcup_{i \in I} J_i \stackrel{\kappa_{I,(J_i)}}{\cong} \sum_{i \in I} |J_i| \stackrel{\bar{\pi}}{\cong} p$ is $\pi$.

It is routine, if lengthy, to verify that this is a bijection, along with naturality in $\sigma$. □
By analogy with the *unitors* and *associators* forming a pseudofunctor, we refer to the
natural isomorphisms above as the **preservators**.

7.4.3. *Coherence of the preservators.* We show a series of lemmas expressing coherence between the preservators and the components of the relative pseudocomonads.

First, we have compatibility with cancellation of dereliction, expressed in two lemmas:

**Lemma 7.11.** For any strict board $A$, the following diagram commutes

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

with all arrows the obvious structural maps or obtained by Lemmas 3.13, 7.9 and 7.10.

*Proof.* This diagram is an equation of natural isomorphisms between distributors

$$
\mathbf{Sym}(\mathcal{G}(A))^{\mathrm{op}} \times \mathcal{G}(!A) \to \mathbf{Set},
$$

so taking $\langle z_i \rangle_{i \in I} \in \mathbf{Sym}(\mathcal{G}(A))$ and $(y_i)_{i \in I} \in \mathcal{G}(!A)$, it boils down to an equality between functions, checked pointwise. An element of $\|\mathbf{c}_{!A}\|[L_A^!](\langle z_i \rangle_{i \in I}, (y_i)_{i \in I})$ comprises

$$
[(\theta_i^-)^\pi_{i \in I}, \quad \mathbf{c}_{(x_i)_{i \in I}} \in \mathcal{C}^+(\mathbf{c}_{!A}), \quad (\theta_i^+)^{i \in I}] \quad \in \quad \|\mathbf{c}_{!A}\|[L_A^!](\langle z_i \rangle_{i \in I}, (y_i)_{i \in I}).
$$

where $\pi : I \simeq |I|$ is any bijection, $\theta_i^- : z_i \cong_A^- x_i$ and $\theta_i^+ : x_i \cong_A^+ y_i$.

Using the description of the action of *pder* and *pprom* on witnesses outlined earlier, we
calculate its image alongside the two paths around the diagram. In both cases, we get

$$
\langle \theta_i^+ \circ \theta_i^- \rangle_{i \in I}^{\bar{\pi}} \in i_{\mathcal{G}(A)}^{\dagger} (\langle z_i \rangle_{i \in I}, \langle y_i \rangle_{i \in I}) = ([R_A^!], i_{\mathcal{G}(A)}^{\dagger}) (\langle z_i \rangle_{i \in I}, (y_i)_{i \in I}),
$$

where $\bar{\pi} : |I| \simeq |I|$ is the only bijection such that $\bar{\pi} \circ \kappa_I = \pi$. $\square$

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

This will show that the two models deal with Kleisli composition with dereliction on
the left in the same way. Similarly, though not quite symmetrically, the next lemma deals
with the Kleisli composition with dereliction on the right hand side:

**Lemma 7.12.** Consider $\sigma \in \mathbf{Wis}[!A, B]$. Then the diagram commutes

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

with all arrows the obvious structural maps or obtained by Lemmas 3.13, 3.13, 7.9 and 7.10.
*Proof.* This diagram states an equality between natural isomorphisms between distributors

$$ \mathbf{Sym}(\mathcal{G}(A))^{\mathrm{op}} \times \mathcal{G}(B) \to \mathbf{Set}, $$

which again can be checked pointwise. Taking $\langle x_{A,i} \rangle_{i \in I} \in \mathbf{Sym}(\mathcal{G}(A))$ and $x_B \in \mathcal{G}(B)$, an element of $(\|\mathrm{der}_B \odot \sigma^!\|[L_A^!]) (\langle x_{A,i} \rangle_{i \in I}, x_B)$ is formed of three components

$$ [(\theta_i^-)^{\pi}_{\langle 0,i \rangle} \in \sqcup_{\{0\}} I, \quad \mathbf{C}_{x_B^\sigma} \odot (x^\sigma)_{\{0\}} \in \mathcal{C}^+(\mathrm{der}_B \odot \sigma^!), \quad \theta_+] $$

where $\pi : \sqcup_{\{0\}} I \simeq |I|$, $\theta_i^- : x_{A,i} \cong_A x_{A,i}^\sigma$, and $\theta^+ : x_B^\sigma \cong_B x_B$.

Following the upper path in the diagram, this is sent to:

$$ \mathrm{id}_{x_B} \cdot \langle\langle [(\theta_i^-)^{\pi'}_{i \in I}, x^\sigma, \theta^+ ] \rangle\rangle \in i_{\mathcal{G}(B)} \cdot (\|\sigma\|[L_A^!])^\dagger (\langle x_{A,i} \rangle_{i \in I}, x_B) \quad (7.6) $$

where $\pi' : I \simeq |I|$ is the unique bijection such that $\sqcup_{\{0\}} I \stackrel{\mathrm{snd}}{\simeq} I \stackrel{\pi'}{\simeq} |I|$ is $\pi$.

On the other hand, following the lower path, we get:

$$ \theta^+ \cdot \langle\langle [(\theta_i^-)^{\kappa_I}_{i \in I}, x^\sigma, \mathrm{id}_{x_B^\sigma}] \rangle\rangle^{\bar{\pi}} \in \mathrm{der}_{\mathcal{G}(B)} \cdot (\|\sigma\|[L_A^!])^\dagger (\langle x_{A,i} \rangle_{i \in I}, x_B), \quad (7.7) $$

for $\bar{\pi} : |I| \simeq |I|$ the only bijection such that $\sqcup_{\{0\}} I \stackrel{\kappa_{\{0\},(I)}}{\simeq} |I| \stackrel{\bar{\pi}}{\simeq} |I|$ is $\pi$. But recall that $\kappa_{\{0\},(I)} : \sqcup_{\{0\}} I \simeq |I|$ is the bijection arranging pairs in lexicographic order, and $\kappa_I : I \simeq |I|$ is the unique monotone bijection. From that and the definition of $\bar{\pi}$ and $\pi'$, it follows that $\bar{\pi} \circ \kappa_I = \pi'$, which entails that (7.7) is equivalent to (7.6). $\square$

Finally, we have compatibility with the multiplication join/μ, expressed via:

**Lemma 7.13.** If $\sigma \in \mathbf{Wis}[!A, B]$ and $\tau \in \mathbf{Wis}[!B, C]$, then the following diagram commutes

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

with all arrows the obvious structural maps or obtained by Lemmas 3.13, 3.13, 7.9 and 7.10.

*Proof.* This diagram states an equality between natural isomorphisms between distributors

$$ \mathbf{Sym}(\mathcal{G}(A))^{\mathrm{op}} \times \mathcal{G}(!C) \to \mathbf{Set} $$

which again can be checked pointwise. Taking $\langle x_{A,l} \rangle_{l \in n} \in \mathbf{Sym}(\mathcal{G}(A))$ and $(x_{C,i})_{i \in I} \in \mathcal{G}(!C)$, an element of $\|\tau^! \odot \sigma^!\|[L_A^!](\langle x_{A,l} \rangle_{l \in n}, (x_{C,i})_{i \in I})$ comprises

$$ [(\theta_{i,j,k}^-)^{\pi}_{\langle\langle i,j \rangle\rangle, k}, \quad (x^{\tau,i})_{i \in I} \odot (x^{\sigma,i,j})_{\langle i,j \rangle \in \sqcup_{i \in I} J_i}, \quad (\theta_i^+)^{\pi'}_{i \in I}] $$
where $\partial_{\tau} x^{\tau, i} = (x_{B,j}^{\tau, i})_{j \in J_i} \vdash x_{C}^{\tau, i}$, $\partial_{\sigma} x^{\sigma, i, j} = (x_{A,k}^{\sigma, i, j})_{k \in K_{i,j}}$, so that

$$ \partial_{\sigma!}((x^{\sigma,i,j})_{\langle i,j \rangle}) = (x_{A,k}^{\sigma,i,j})_{\langle\langle i,j \rangle,k\rangle} \vdash (x_{B}^{\sigma,i,j})_{\langle i,j \rangle}, \quad \partial_{\tau!}((x^{\tau,i})_{i \in I}) = (x_{B,j}^{\tau,i})_{\langle i,j \rangle} \vdash (x_{C}^{\tau,i})_{i \in I} $$

with $x_B^{\sigma, i, j} = x_{B,j}^{\tau, i}$, $\pi: \sqcup_{\langle i,j \rangle} K_{i,j} \simeq n$, $\theta_{i,j,k}^{-} : x_{A,\pi(\langle i,j \rangle,k)} \cong_{A} x_{A,k}^{\sigma, i, j}$ and $\theta_{i}^{+} : x_{C}^{\tau, i} \cong_{C} x_{C,i}$.

For the left hand side path, a careful calculation shows that this is sent to

$$ \langle\langle [(x_{B,j}^{\tau,i})_{j \in J_i}^{\kappa_{J_i}}, x^{\tau,i}, \theta_i^+] \rangle\rangle_{|i| \in |I|} \bullet \langle\langle [(\theta_{ijk}^{-})_{k \in K_{ij}}^{\kappa_{K_{ij}}}, x^{\sigma,i,j}, x_B^{\sigma,i,j}] \rangle\rangle_{|i| \in |I|, |j| \in |J_i|}^{\pi'} $$

where $\pi' : n \simeq n$ is the only bijection such that $\pi' \circ \kappa_{I,(J),(K)} = \pi$, where $\kappa_{I,(J),(K)}: \sqcup_{\langle i,j \rangle} K_{i,j} \simeq \sum_{i \in I} \sum_{j \in J_i} |K_{ij}| = n$ arranges the triples $(i, j, k)$ in lexicographic order.

Likewise, for the right hand side path, it is sent to

$$ \langle\langle [(x_{B,j}^{\tau,i})_{j \in J_i}^{\kappa_{J_i}}, x^{\tau,i}, \theta_i^+)] \rangle\rangle_{|i| \in |I|}^{\omega} \bullet \langle\langle [(\theta_{ijk}^{-})_{k \in K_{ij}}^{\kappa_{K_{ij}}}, x^{\sigma,i,j}, x_B^{\sigma,i,j}] \rangle\rangle_{|\langle i,j \rangle| \in |\sqcup_{i \in I} J_i|}^{\omega'} $$

where $\omega: \sum_{i \in I} |J_i| \simeq \sum_{i \in I} |J_i|$ is obtained as $\kappa_{\sqcup_i J_i} \circ \kappa_{I,(J)}^{-1}$ – that is, it links the lexicographic ordering of pairs $(i, j)$, and their ordering following their representations $\langle i, j \rangle \in \mathbb{N}$. Likewise, $\omega' : n \simeq n$ is the unique bijection such that $\omega' \circ \kappa_{\sqcup_i J_i,(K)} = \pi$ – that is, it is $\pi$ where $i, j, k$ are ordered in the lexicographic order of the pairs $\langle i, j \rangle, k$.

It is then routine to show that these two witnesses are equivalent, as required. $\square$

**7.4.4. Preservation of Kleisli composition.** Finally, we are equipped to show how $\|\cdot\|$ lifts to the Kleisli bicategories. Recall that, for $\sigma \in \mathbf{Wis}[!A, B]$, we have

$$ \|\sigma\|_! = \|\sigma\|[R_A^!] \in \mathrm{Dist}[\mathrm{Sym}(\mathcal{G}(A)), \mathcal{G}(B)]. $$

Thus, we may set:

$$ \mathrm{pid}_A^! = \mathrm{pder}_A : \|\mathrm{der}_A\|_! \cong i_{\mathcal{G}(A)} $$

for the natural isomorphism witnessing preservation of identity. Likewise, for $\sigma \in \mathbf{Wis}[!A, B]$ and $\tau \in \mathbf{Wis}[!B, C]$, we set the natural iso witnessing preservation of composition as

$$ \begin{align*} \mathrm{pcomp}_{\sigma, \tau}^! : \|\tau \odot \sigma'\|_! &= \|\tau \odot \sigma'\|[L_A^!] \\ \mathrm{pcomp}_{\sigma, \tau}^! &\cong (\|\tau\| \cdot \|\sigma'\|[L_A^!]) \\ &\cong \|\tau\| \cdot \|\sigma'\|[L_A^!] \\ \mathrm{pprom}_{\sigma}^! &\cong \|\tau\| \cdot [R_B^!](\|\sigma\|[L_A^!])^{\dagger} \\ &\cong \|\tau\|[R_B^!] \cdot (\|\sigma\|[L_A^!])^{\dagger} \\ &\cong \|\tau\|_! \cdot \|\sigma\|_!^{\dagger} \end{align*} $$

These definitions provide the necessary components for:

**Theorem 7.14.** *This provides the data for a pseudofunctor*

$$ \|\cdot\|_! : \mathbf{Wis}_! \to \mathbf{Esp}. $$

*Proof.* Naturality of $\mathrm{pcomp}_{\sigma, \tau}^!$ in $\sigma$ and $\tau$ is direct by composition of natural isos. The coherence diagrams follow by diagram chasing, relying on Lemmas 7.11, 7.12 and 7.13. $\square$

**7.5. Cartesian closed structure.** We show the bicategory $\mathbf{Wis}_!$ is cartesian closed, using typical constructions in concurrent games, in sufficient detail to keep the paper self-contained. For a precise definition of the structure of cartesian closed bicategories we refer to [Sav20].
7.5.1. Cartesian products in Wis<sub>i</sub>. The empty board $\top$, with $\kappa_\top(\emptyset) = 1$, is strict, and it is direct that $\top$ is a terminal object in Wis<sub>i</sub>, since any negative strategy $A \vdash \top$ must be empty. Now if $A, B$ are strict, the product board $A \& B$ is defined as $A \otimes B$, except that all events of $A$ are in conflict with events of $B$. This means that configurations of $A \& B$ are either empty, or of the form $\{1\} \times x$ for $x \in \mathscr{C}(A)$ (written $i_1(x)$) or $\{2\} \times x$ for $x \in \mathscr{C}(B)$ (written $i_2(x)$). For the payoff, we set $\kappa_{A\&B}(\emptyset) = 1$ and $\kappa_{A_1\&A_2}(i_i(x)) = \kappa_{A_i}(x)$, making $A \& B$ a strict arena. By strictness, we have an isomorphism

$$L_{A,B}^{\&} : \mathscr{G}(A \& B) \cong \mathscr{G}(A) + \mathscr{G}(B) : R_{A,B}^{\&}$$

which reflects the definition of binary products in Esp. The first projection $\pi_A \in \mathbf{Wis}[!(A \& B), A]$ has ess $c_A$, with display map the map of ess characterized by

$$\partial(c_x) = (i_1(x))_{\{0\}} \vdash x,$$

with the second projection defined symmetrically. If $\sigma \in \mathbf{Wis}[!\Gamma, A]$ and $\tau \in \mathbf{Wis}[!\Gamma, B]$, their pairing has ess $\sigma \& \tau$ and display map the unique such that

$$\partial(i_1(x^\sigma)) = x_\Gamma^\sigma \vdash i_1(x_A^\sigma) \in \mathscr{C}(!\Gamma \vdash A \& B),$$

and likewise for $\partial(i_2(x^\tau))$, yielding $\langle\sigma, \tau\rangle \in \mathbf{Wis}[!\Gamma, A \& B]$. This extends to a functor $\langle-, -\rangle : \mathbf{Wis}![\Gamma, A] \times \mathbf{Wis}![\Gamma, B] \to \mathbf{Wis}![\Gamma, A \& B]$ in a straightforward way.

**Proposition 7.15.** For any strict arenas $\Gamma, A$ and $B$, there is an adjoint equivalence

$$\begin{tikzcd}[column sep=2.8em, row sep=2.8em]
\mathbf{Wis}_![\Gamma, A \& B] \arrow[r, "\cong"'] & \mathbf{Wis}_![\Gamma, A] \times \mathbf{Wis}_![\Gamma, B] \arrow[d, "\langle-, -\rangle"] \\
\mathbf{Wis}_![\Gamma, A \& B] \arrow[r, "(\pi_A \odot (-)^1, \pi_B \odot (-)^1)"', "\cong"] & \mathbf{Wis}_![\Gamma, A] \times \mathbf{Wis}_![\Gamma, B]
\end{tikzcd}$$

providing the data to turn $A \& B$ into a cartesian product in the bicategorical sense.

*Proof.* To witness the equivalence, we need three natural isomorphisms

$$\eta_\sigma : \sigma \cong \langle \pi_1 \odot \sigma^\prime, \pi_2 \odot \sigma^\prime \rangle, \quad \epsilon_{\sigma_1, \sigma_2}^i : \pi_i \odot \langle \sigma_1, \sigma_2 \rangle^\prime \cong \sigma_i$$

for $\sigma \in \mathbf{Wis}![\Gamma, A_1 \& A_2]$, $\sigma_i \in \mathbf{Wis}![\Gamma, A_i]$ and $i \in \{1, 2\}$.

We focus first on the former. Notice that for all $x^\sigma \in \mathscr{C}^+(\sigma)$, if $x^\sigma$ is non-empty then as $\sigma$ is negative and the $A_i$ are strict, the minimal event of $x^\sigma$ must occur in $A_1$ or $A_2$. We set

$$\begin{array}{rcl}
\eta_\sigma : & \sigma & \cong \langle \pi_1 \odot \sigma^\prime, \pi_2 \odot \sigma^\prime \rangle \\
& \emptyset & \mapsto \emptyset \\
& x^\sigma & \mapsto i_i(c_{x_{A_i}^\sigma} \odot (x^\sigma)_{\{0\}}) \quad (\text{if } x^\sigma \neq \emptyset, \partial(x^\sigma) = x_\Gamma^\sigma \vdash i_i(x_{A_i}^\sigma))
\end{array}$$

yielding a positive isomorphism, additionally natural in $\sigma$. For the co-unit, we set

$$\epsilon_{\sigma_1, \sigma_2}^i : \pi_i \odot \langle \sigma_1, \sigma_2 \rangle^\prime \cong \sigma_i \\ c_{x_{A_i}^\sigma} \odot (i_i(x^\sigma))_{\{0\}} \mapsto x^\sigma_i$$

again a positive isomorphism natural in $\sigma_1$ and $\sigma_2$. For the adjunction, we check that

$$\begin{tikzcd}[column sep=2.8em, row sep=2.8em]
\pi_i \odot \sigma^! \arrow[r, "\pi_i \odot \eta_\sigma^!"'] & \pi_i \odot \langle \pi_1 \odot \sigma^! , \pi_2 \odot \sigma^! \rangle \arrow[d, "\epsilon_{\pi_1 \odot \sigma^! , \pi_2 \odot \sigma^!}^i"'] \\
& \pi_i \odot \sigma^! \arrow[r, "\cong"'] & \pi_i \odot \langle \sigma_1, \sigma_2 \rangle^! \arrow[d, "\langle \sigma_1, \sigma_2 \rangle^! , \epsilon_{\sigma_1, \sigma_2}^2"'] \\
& & \langle \sigma_1, \sigma_2 \rangle
\end{tikzcd}$$

commute for all $i = 1, 2$, $\sigma \in \mathbf{Wis}![\Gamma, A_1 \& A_2]$, $\sigma_i \in \mathbf{Wis}![\Gamma, A_i]$, which is direct. $\square$

<figure><img src="image_29.png" /></figure>
7.5.2. Closed structure in Wis!. Recall that the objects of Wis! are strict boards, and observe that any strict board B is isomorphic to $\&_{i \in I} B_i$ where the $B_i$ are pointed, meaning that they have exactly one minimal event. We first define a linear arrow for a --board A and a pointed strict board B, by setting $A \dasharrow B$ to be $A \vdash B$ with a stricter dependency order, so that all events in A causally depend on the unique minimal move in B.

This is generalized for any strict B as

$$A \dasharrow \&_{i \in I} B_i = \&_{i \in I}(A \dasharrow B_i)$$

whose configurations have a convenient description:

**Lemma 7.16.** For any --board A, and strict board B, we have

$$(- \dasharrow -) : \mathcal{C}^0(A) \times \mathcal{C}^0(B) \cong \mathcal{C}^0(A \dasharrow B).$$

*Proof.* Straightforward, using crucially the fact that since B is strict, a configuration of null payoff in B must be non-empty, so that the A component is always reachable. $\square$

Now for A, B strict, we define the arrow $A \Rightarrow B$ as $!A \dasharrow B$. This is equipped with

$$\mathbf{ev}_{A,B} \in \mathbf{Wis}![((!A \dasharrow B) \& A), B]$$

an evaluation strategy consisting of the ess $\mathbf{c}_{!A \to B}$, and where the display map is

$$\partial(\mathbf{c}_{(x_A^i)_{i \in I} \dasharrow x_B}) = (i_1((x_A^i)_{i \in I} \dasharrow x_B))_{\langle 0,0 \rangle} \dashv (i_2(x_A^i))_{\langle 1, i \rangle \in \Sigma_{\langle 1 \rangle} I} \vdash x_B$$

if $x_B \neq \emptyset$, and empty otherwise, with $\dashv$ the union of families with disjoint index sets. Likewise, the **currying** of $\sigma \in \mathbf{Wis}![\Gamma \& A), B]$ is a strategy $\Lambda(\sigma)$ with ess $\sigma$ and display

$$\partial_{\Lambda(\sigma)}(x^{\sigma}) = (x_{\Gamma}^{i})_{i \in I} \vdash (x_{A}^{j})_{j \in J} \dasharrow x_{B}$$

for $x^{\sigma} \neq \emptyset$, where $\partial_{\sigma}(x^{\sigma}) = (i_1(x_{\Gamma}^i))_{i \in I} \dashv (i_2(x_A^j))_{j \in J} \vdash x_B$.

Altogether, this gives a functor $\Lambda : \mathbf{Wis}![\Gamma \& A, B] \to \mathbf{Wis}![\Gamma, A \Rightarrow B]$.

**Proposition 7.17.** For any strict $\Gamma$, A and B, there is an adjoint equivalence

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

providing the data to turn $A \Rightarrow B$ into an exponential object in the bicategorical sense.

*Proof.* To witness the equivalence, we need two natural isomorphisms

$$\eta_{\sigma} : \sigma \cong \Lambda(\mathbf{ev}_{A,B} \odot \langle\sigma \odot \pi_{\Gamma}^{!}, \pi_{A}^{!}\rangle), \quad \beta_{\tau} : \mathbf{ev}_{A,B} \odot \langle\Lambda(\tau) \odot \pi_{\Gamma}^{!}, \pi_{A}^{!}\rangle \cong \tau$$

for $\sigma \in \mathbf{Wis}![\Gamma, A \Rightarrow B]$ and $\tau \in \mathbf{Wis}![\Gamma \& A, B]$. For the former, we set

$$\eta_{\sigma}(x^{\sigma}) = \mathbf{c}_{(x_{A,i})_{i \to x_B} \odot ((i_1(x^{\sigma} \odot (\mathbf{c}_{x_{\Gamma,j})_{j \in J}}))_{\langle 0,0 \rangle} \dashv (i_2(\mathbf{c}_{x_{A,i}}))_{\langle 1,i \rangle})}$$

where $\partial_{\sigma}(x^{\sigma}) = (x_{\Gamma,j})_{j \in J} \vdash (x_{A,i})_{i \in I} \dasharrow x_B$. A careful check shows this is well-defined and

$$\partial_{\Lambda}(\mathbf{ev}_{A,B} \odot \langle\sigma \odot \pi_{\Gamma}^{!}, \pi_{A}^{!}\rangle)(\eta_{\sigma}(x^{\sigma})) = (x_{\Gamma,j})_{\langle\langle 0,0 \rangle, \langle j,0 \rangle\rangle} \vdash (x_{A,i})_{\langle\langle 1,i \rangle, 0\rangle} \dasharrow x_B$$

which is clearly positively symmetric to $\partial_{\sigma}(x^{\sigma})$ as required. Likewise, the expression

$$y = \mathbf{c}_{(x_{A,i})_{i \to x_B} \odot ((i_1(x^{\tau} \odot (\mathbf{c}_{x_{\Gamma,j})_{j \in J}}))_{\langle 0,0 \rangle} \dashv (i_2(\mathbf{c}_{x_{A,i}}))_{\langle 1,i \rangle})}$$
captures exactly all +-covered configurations of $\mathbf{ev}_{A,B} \odot \langle \Lambda(\tau) \odot \pi_{\Gamma}^{!}, \pi_{A} \rangle^{!}$, displaying to

$$(i_1(x_{\Gamma,j})) \llbracket \langle 0,0 \rangle, \langle j,0 \rangle \rrbracket \rightsquigarrow (i_2(x_{A,i})) \llbracket \langle 1,i \rangle, 0 \rangle \vdash x_B$$

for $\partial_{\tau}(x^{\tau}) = (i_1(x_{\Gamma,j}))_{j \in J} \rightsquigarrow (i_2(x_{A,i}))_{i \in I} \vdash x_B$; we set $\beta_{\tau}(y) = x^{\tau}$. Unfolding these definitions, a careful calculation confirms that the triangle identities hold. $\square$

### 7.5.3. Cartesian closed structure in Esp.
Here, we briefly review the cartesian closed structure of Esp. Firstly, we have $\top$ the empty groupoid, with an adjoint equivalence

$$\mathbf{Esp}[\Gamma, \top] \approx 1$$

for 1 the category with one object (and one morphism). For binary products, given A and B groupoids, we simply set their **with** as the disjoint sum $A \& B = A + B$; writing as in games $i_1(a) \in A + B$ for $a \in A$ and $i_2(b) \in A + B$ for $b \in B$. For projections, we set distributors

$$\pi_1 : \mathbf{Sym}(A + B)^{\mathrm{op}} \times A \to \mathbf{Set} \qquad \pi_2 : \mathbf{Sym}(A + B)^{\mathrm{op}} \times B \to \mathbf{Set} \\ (\langle i_1(a) \rangle, a') \mapsto A[a, a'] \qquad (\langle i_2(b) \rangle, b') \mapsto B[b, b']$$

and for the pairing of $\alpha \in \mathrm{Dist}[\mathbf{Sym}(\Gamma), A]$ and $\beta \in \mathrm{Dist}[\mathbf{Sym}(\Gamma), B]$, we set

$$\langle \alpha, \beta \rangle : \mathbf{Sym}(\Gamma)^{\mathrm{op}} \times (A + B) \to \mathbf{Set} \\ (\vec{\gamma}, i_1(a)) \mapsto \alpha(\vec{\gamma}, a) \\ (\vec{\gamma}, i_2(b)) \mapsto \beta(\vec{\gamma}, b)$$

with obvious functorial action. We skip the details of the adjoint equivalence

$$\mathbf{Esp}[\Gamma, A \& B] \approx \mathbf{Esp}[\Gamma, A] \times \mathbf{Esp}[\Gamma, B],$$

which are straightforward and not required for the remainder of this paper.

Given groupoids A and B, the **arrow** is $A \Rightarrow B = \mathbf{Sym}(A)^{\mathrm{op}} \times B$. For **evaluation**,

$$\mathbf{ev}'_{A,B} : (\mathbf{Sym}(A \Rightarrow B) \times \mathbf{Sym}(A))^{\mathrm{op}} \times B \to \mathbf{Set} \\ ((\langle \langle \vec{a}, b \rangle \rangle, \vec{a}'), b') \mapsto \mathbf{Sym}(A)[\vec{a}', \vec{a}] \times B[b, b']$$

and empty otherwise, provides the core of the evaluation mechanism; but we need a distributor in $\mathbf{Esp}[\mathbf{Sym}(A)^{\mathrm{op}} \times B + \mathbf{Sym}(A), B]$. For that, we set $\mathbf{ev}_{A,B} = \mathbf{ev}'_{A,B}[L_{A \Rightarrow B,A}^{\mathrm{see}}]$, i.e.

$$\mathbf{ev}_{A,B}(\vec{s}, a) = \mathbf{ev}'_{A,B}(L_{A \Rightarrow B,A}^{\mathrm{see}}(\vec{s}), b)$$

where $L_{A,B}^{\mathrm{see}} : \mathbf{Sym}(A + B) \approx \mathbf{Sym}(A) \times \mathbf{Sym}(B) : R_{A,B}^{\mathrm{see}}$ is the Seely equivalence.

Finally, the **currying** of $\alpha \in \mathbf{Esp}[\Gamma + A, B]$ is defined by

$$\Lambda(\alpha) : \mathbf{Sym}(\Gamma)^{\mathrm{op}} \times (\mathbf{Sym}(A)^{\mathrm{op}} \times B) \to \mathbf{Set} \\ (\vec{\gamma}, (\vec{a}, b)) \mapsto \alpha(R_{\Gamma,A}^{\mathrm{see}}(\vec{\gamma}, \vec{a}), b)$$

informing an adjoint equivalence $\mathbf{Esp}[\Gamma, A \Rightarrow B] \approx \mathbf{Esp}[\Gamma + A, B]$ as in Proposition 7.17.
7.6. **A cartesian closed pseudofunctor.** We first show that the pseudofunctor $\|-\|! : \mathbf{Wis} \to \mathbf{Esp}$ preserves the cartesian structure. The key observation is that:

**Lemma 7.18.** Consider A, B two mixed boards. Then, the distributor

$$ \langle \|\pi_A\|!, \|\pi_B\|! \rangle \in \mathbf{Esp}[\mathcal{G}(A \& B), \mathcal{G}(A) + \mathcal{G}(B)] $$

is naturally isomorphic to $\widehat{L_{A,B}^{\&}}$.

This is a straightforward variation on the proof that $\|-\|$ preserves the identity. From this, we obtain that the pseudofunctor $\|-\|$! preserves products:

**Proposition 7.19.** The pseudofunctor $\|-\|$! is a fp-pseudofunctor in the sense of [FS19].

*Proof.* The terminal object is preserved in a strict sense, since $\mathcal{G}(\top)$ is empty. For preservation of binary products, we must provide the missing components for an adjoint equivalence

$$ \mathcal{G}(A \& B) \xrightarrow{\substack{\langle \|\pi_A\|!, \|\pi_B\|! \rangle \\ \qquad \qquad \qquad \qquad \xrightarrow{\cong} \mathcal{G}(A) + \mathcal{G}(B) \\ \qquad \qquad \qquad \qquad \xrightarrow{\mathbf{q}^{\&}_{A,B}}}} \mathcal{q}^{\&}_{A,B} $$

in **Esp**. But the iso $L_{A,B}^{\&} : \mathcal{G}(A \& B) \cong \mathcal{G}(A) + \mathcal{G}(B) : R_{A,B}^{\&}$ lifts to an adjoint equivalence

$$ \widehat{L_{A,B}^{\&}} : \mathcal{G}(A \& B) \simeq \mathcal{G}(A) + \mathcal{G}(B) : \widehat{R_{A,B}^{\&}} $$

in **Esp**; so providing $\mathbf{q}^{\&}_{A,B} = \widehat{R_{A,B}^{\&}}$, we conclude via Lemma 7.18. $\square$

Finally, it remains to prove that the cartesian closed structure is preserved as well. Observe that if A and B are --boards with B strict, then we have an adjoint equivalence

$$ L_{A,B} \xrightarrow{\mathcal{G}(A \Rightarrow B)} \mathbf{Sym}(\mathcal{G}(A))^{\text{op}} \times \mathcal{G}(B) : \widehat{R_{A,B}} $$

using first Lemma 7.16 as since B is strict, its complete configurations are non-empty; and observing that this decomposition also holds for symmetries; followed by Proposition 7.4.

Now, as for binary products, our key observation is the following:

**Lemma 7.20.** Consider A and B two --boards, with B strict. Then, the distributor

$$ \Lambda(\|\mathbf{ev}_{A,B}\|! \bullet! \mathbf{q}^{\&}_{A \Rightarrow B,A}) \in \mathbf{Esp}[\mathcal{G}(A \Rightarrow B), \mathbf{Sym}(\mathcal{G}(A))^{\text{op}} \times \mathcal{G}(B)] $$

is naturally isomorphic to $\widehat{L_{A,B}^{\&}}$.

*Proof.* Unfolding the definitions on both sides, this boils down to a natural isomorphism

$$ \|\mathbf{ev}_{A,B}\|((i_1((x_{A,i})_{i \in I} \to x_B))_0 \uplus (i_2(y_{A,j})_{j \in n}, y_B) \\ \cong \mathbf{Sym}(\mathcal{G}(A))[\langle y_{A,j} \rangle_{j \in n}, \langle x_{A,i} \rangle_{i \in I}] \times \mathcal{G}(B)[x_B, y_B] $$

which again is a variation on the preservation of the identity by $\|-\|$. $\square$

We may now use this to conclude:

**Proposition 7.21.** The pseudofunctor $\|-\|$! is a cc-pseudofunctor in the sense of [FS19].
*Proof.* We must provide the missing components for an adjoint equivalence

$$ \mathcal{G}(A \Rightarrow B) \underset{\mathbf{q} \underset{\mathcal{G}(A) \Rightarrow \mathcal{G}(B)}{\rightleftharpoons}}^{\Lambda(\|\mathbf{e}v_{A,B}\|_1 \bullet \mathbf{q}_{A \Rightarrow B,A}^{\&})} \mathcal{G}(A) + \mathcal{G}(B) $$

in **Esp.** But the equivalence $L_{A,B} \colon \mathcal{G}(A \Rightarrow B) \simeq \mathbf{Sym}(\mathcal{G}(A))^{\text{op}} \times \mathcal{G}(B) : R_{A,B} \twoheadrightarrow$ lifts to

$$ \widehat{L}_{A,B} : \mathcal{G}(A \Rightarrow B) \simeq \mathbf{Sym}(\mathcal{G}(A))^{\text{op}} \times \mathcal{G}(B) : \widehat{R}_{A,B} $$

in **Esp.** so providing $\mathbf{q}_{A,B} = \widehat{R}_{A,B}$, we conclude via Lemma 7.20. □

Altogether this completes the proof of our main theorem:

**Theorem 7.22.** We have a cartesian closed pseudofunctor $\|-\|_! : \mathbf{Wis}_! \to \mathbf{Esp.}$

*Note.* We have constructed a cartesian closed pseudofunctor directly, without leveraging the preservation of symmetric monoidal structure established in earlier sections. Although the cartesian closed structure is related to the monoidal structure via Seely isomorphisms, the theory of bicategorical models of linear logic, and a fortiori functors between models, is still under-developed, and a direct approach seemed more achievable. This is an important aspect of this work which deserves further investigation.

# 8. SOME CONSEQUENCES FOR THE $\lambda$-CALCULUS

Finally, for the last technical section of this paper, we illustrate this pseudofunctor by relating a dynamic and a static model of the pure (untyped) $\lambda$-calculus.

## 8.1. Two models of the pure $\lambda$-calculus.

8.1.1. A reflexive object in $\mathbf{Wis}_!$. Our bicategory of games contains a **universal arena U** with an isomorphism of arenas

$$ \mathrm{unf}_U : U \cong U \Rightarrow U : \mathrm{fld}_U $$

making $U$ an extensional reflexive object [Bar85]. Concretely, $U$ is constructed corecursively as the solution of the following ‘domain-like equation’: $U = \otimes_N!U \dashv o$, where $o$ is the arena with one negative move $*$, $\kappa_o(\emptyset) = 1$ and $\kappa_o(\{*\}) = 0$.

Following the interpretation of the $\lambda$-calculus in a reflexive object, we have, for every closed $\lambda$-term $M$, a strategy $[M] : U$. This strategy has a clear interpretation: it is a representation of the *Nakajima tree* of $M$ (see e.g. [KNO02, CP18]).
Types:

$$ \mathcal{D} \ni a ::= * \mid \langle a_1, \dots, a_k \rangle \to a $$

Proof-relevant subtyping:

$$ \begin{array}{ccc} \overline{\text{id}_* : * \to *} & \overline{\vec{f}^\sigma : \vec{b} \to \vec{a} \quad f : a \to b} & \overline{\vec{f}^\sigma \to f : (\vec{a} \to a) \to (\vec{b} \to b)} \\ \sigma \in S_k \quad f_1 : a_{\sigma 1} \to b_1 \quad \dots \quad f_k : a_{\sigma k} \to b_k & & \\ \langle f_1, \dots, f_k \rangle^\sigma : \langle a_1, \dots, a_k \rangle \to \langle b_1, \dots, b_k \rangle & & \end{array} $$

<caption>Figure 4: Graph of intersection types G.</caption>

8.1.2. *The Pure λ-Calculus in Esp.* Likewise, one can construct models of the λ-calculus in Esp [FGHW08, Oli21, KMO23]. A categorified graph model [KMO23] consists of a small category $\mathcal{D}$ together with an embedding

$$ \iota : \mathbf{Sym}(\mathcal{D})^{\mathrm{op}} \times \mathcal{D} \hookrightarrow \mathcal{D}. $$

We adopt a type-theoretic understanding of these models, setting $\vec{a} \to a := \iota(\vec{a}, a)$. The main intuition is that elements of $\mathcal{D}$ are *types*, where the arrow type is built exploiting *sequences of types*. These sequences correspond to a notion of k-ary intersection types [Oli21], by setting $(a_1 \cap \dots \cap a_k) := \langle a_1, \dots, a_k \rangle$. The *free* categorified graph model can be presented syntactically as the category generated by the graph in Figure 4. Composition and identities are defined by induction in the natural way, exploiting the definition of composition of morphisms of sequences induced by $\mathbf{Sym}(-)$. We shall now *complete* $\mathcal{D}$ in an appropriate way, producing an extensional model that we will then relate to the universal arena $\mathbf{U}$.

8.2. **Constructing an extensional model $\mathcal{D}^*$**. The extensional model $\mathcal{D}^*$ is defined as an appropriate completion of $\mathcal{D}$, where we add chosen isomorphisms between types in a coherent way. This construction can be defined in abstract categorical terms as an appropriate pseudocolimit (a *coisoinserter*), but in the present paper we will just give its explicit syntactic presentation. The following construction is a particular case of *completion of partial algebras* for categorified graph models, in the sense of [KMO23].

We start by adding the following two arrows to the graph of intersection types G :

$$ \overline{e : * \to \langle\rangle \to *} \qquad \overline{e^{-1} : \langle\rangle \to * \to *} $$

resulting in a graph $G^*$. We now want to obtain a category from $G^*$. Identities are the same as $\mathcal{D}$. Composition is inherited from the composition of $\mathcal{D}$, by adding the following cases:

$$ e \circ \mathrm{id}_* = e \qquad \mathrm{id}_{\langle\rangle \to *} \circ e^{-1} = e^{-1} \qquad e \circ e^{-1} = \mathrm{id}_{\langle\rangle \to *} \qquad e^{-1} \circ e = \mathrm{id}_*. $$

The category $\mathcal{D}^*$ is a categorified graph model:

$$ \iota^* : \mathbf{Sym}(\mathcal{D}^*)^{\mathrm{op}} \times \mathcal{D}^* \hookrightarrow \mathcal{D}^* \qquad (\vec{a}, a) \mapsto \vec{a} \to a $$
**Theorem 8.1** [KMO23]. The functor $ι^*$ is fully faithful and essentially surjective on objects.

**Morphism actions and congruence on type derivations.** We now explain how the interpretation of $\lambda$-terms in **Esp** can be presented exploiting intersection types.

The intuition is that the semantics of a term will compute all its terminating executions in face of a given environment. These executions can be encoded by the means of an intersection type system. Given $a \in \mathcal{D}$, $[[M]]_{\text{Esp}}^D(a)$ will appear (up to a canonical isomorphism) as the set of derivations of the judgement $\vdash M : a$ in the type system. The construction of this system reflects the corresponding operations on distributors: in particular derivations carry explicit symmetries, $[[M]]_{\text{Esp}}^D(a)$ is really the set of derivations *quotiented* by an equivalence relation letting symmetries flow though the concrete derivation.

Let $\mathcal{D}$ be a categorified graph model. A *type declaration* over $\mathcal{D}$ consists of a pair $x : \vec{a}$ where $x$ is a variable of the $\lambda$-calculus and $\vec{a} \in \text{Sym}(\mathcal{D})$. A *type context* consists of a sequence of type declarations $x_1 : \vec{a}_1, \dots, x_n : \vec{a}_n$. Type contexts are denoted with greek letters $\gamma, \delta \dots$. Given two type contexts $\gamma = x_1 : \vec{a}_1, \dots, x_n : \vec{a}_n$ and $\delta = x_1 : \vec{b}_1, \dots, x_n : \vec{b}_n$ we define their *pointwise concatenation* as $\gamma \otimes \delta = x_1 : \vec{a}_1 :: \vec{b}_1, \dots, x_n : \vec{a}_n :: \vec{b}_n$ where $\vec{a}_i :: \vec{b}_i$ denotes list concatenation. A *morphism* of type contexts $\eta : \gamma \to \delta$ consist of a family of morphisms $\vec{f}_i^{\sigma_i} : \vec{a}_i \to \vec{b}_i$ for $i \in [n]$. Morphisms of type contexts are denoted with greek letters $\eta, \theta \dots$. The definition of the type system is given in Figure 5.

Given a type derivation $\pi$ of conclusion $\gamma \vdash M : a$ and type morphisms $\theta : \delta \to \gamma$ and $f : a \to b$ we define contravariant and covariant actions on derivations:

$$ \begin{array}{ccc} \pi\{\theta\} & &[f]\pi \\ \vdots & & \vdots \\ \delta \vdash M : a & & \gamma \vdash M : b \end{array} $$

The explicit definitions are given, respectively, in Figures 6 and 7. By a straightforward induction, one can prove that both actions are compositional and unital in the appropriate way, that is $(\pi\{\theta\})\{\theta'\} = \pi\{\theta \circ \theta'\}, \pi\{id\} = \pi$ and $[g]([f]\pi) = [g \circ f]\pi, [id]\pi = \pi$.

By the means of these morphism actions, we define an *equivalence relation* on type derivations, as the smallest equivalence relation generated by the rules of Figure 8 and that is compatible with the structure of type derivations. This equivalence corresponds to the one induced by an appropriate *coend formula*: namely, the coend formula that derives from the categorified graph model interpretations of application and $\lambda$-abstraction in **Esp**.

**Intersection type distributors.** We are now ready to introduce the syntactic presentation of the categorified graph model semantics, namely intersection type distributors.

Given a $\lambda$-term $M$ and a categorified graph model $\mathcal{D}$, with $\vec{x} \supseteq \text{fv}(M)$, we define

$$ \text{ITD}^{\mathcal{D}}(M)_{\vec{x}} : (\text{Sym}(\mathcal{D}) \overbrace{\otimes \cdots \otimes}^{|\vec{x}| \text{ times}} \text{Sym}(\mathcal{D}))^{op} \times \mathcal{D} \to \text{Set} $$

the intersection type distributor of $M$, by the following family of sets:

$$ \text{ITD}^{\mathcal{D}}(M)_{x_1, \dots, x_n}(\vec{a}_1, \dots, \vec{a}_n; a) = \left\{ \begin{array}{c} \pi \\ \vdots \\ \pi \end{array} \middle| x_1 : \vec{a}_1, \dots, x_n : \vec{a}_n \vdash M : a \right\} / \sim . $$
$$ \frac{f : a' \to a}{x_1 : \langle\rangle, \dots, x_i : \langle a' \rangle, \dots, x_n : \langle\rangle \vdash x_i : a} $$

$$ \frac{\gamma, x : \vec{a} \vdash \mathbf{M} : a \quad f : (\vec{a} \to a) \to b}{\gamma \vdash \lambda x.M : b} $$

$$ \frac{\gamma_0 \vdash \mathbf{M} : \langle a_1, \dots, a_k \rangle \to a \quad (\gamma_i \vdash \mathbf{N} : a_i)_{i=1}^k \quad \eta : \delta \to \bigotimes_{i=1}^k \gamma_i}{\delta \vdash \mathbf{MN} : a} $$

<caption>Figure 5: Intersection type system over a graph model $\mathcal{D}$.</caption>

$$ \left( \frac{f : a' \to a}{\langle\rangle, \dots, \langle a' \rangle, \dots, \langle\rangle \vdash a} \right) \{g : b \to a'\} = \frac{f \circ g}{\langle\rangle, \dots, \langle b \rangle, \dots, \langle\rangle \vdash a} \\ \left( \frac{\pi \quad \vdots \quad \delta, \vec{a} \vdash a \quad f : (\vec{a} \to a) \to b}{\delta \vdash b} \right) \{\eta\} = \frac{\pi \{\eta, \mathrm{id}_{\vec{a}}\} \quad \vdots \quad \delta', \vec{a} \vdash a \quad f : (\vec{a} \to a) \to b}{\delta' \vdash \vec{a} \to a} $$

$$ \left( \frac{\pi_1 \quad \vdots \quad \gamma_0 \vdash \vec{a} \to a \quad \left( \left( \begin{array}{c} \pi_i \\ \vdots \\ \gamma_i \vdash a_i \end{array} \right)_{i=1}^k \quad \theta : \delta \to \bigotimes_{j=0}^k \gamma_j \right)}{\delta \vdash a} \right) \{\eta\} = \frac{\pi_1 \quad \vdots \quad \gamma_0 \vdash \vec{a} \to a \quad \left( \left( \begin{array}{c} \pi_i \\ \vdots \\ \gamma_i \vdash a_i \end{array} \right)_{i=1}^k \quad \theta \circ \eta}{\delta' \vdash a} $$

where $\vec{a} = \langle a_1, \dots, a_k \rangle$ and $\eta : \delta' \to \delta$.

<caption>Figure 6: Right action on derivations.</caption>

Stating the connection between the intersection type distributor of a term and its species of structure semantics requires the *Seely equivalence* for contexts:

$$ L_{\vec{x}}^{\text{see}} : \mathbf{Sym}(\mathcal{D} + \dots + \mathcal{D}) \simeq \mathbf{Sym}(\mathcal{D}) \times \dots \times \mathbf{Sym}(\mathcal{D}) : R_{\vec{x}}^{\text{see}} $$

**Theorem 8.2** [KMO23]. Let $M$ be a $\lambda$-term, $\vec{x} \supseteq \mathrm{fv}(M)$ and $\mathcal{D}$ a categorified graph model. Then, we have an isomorphism, natural in $\delta$ and $a$:

$$ \mathrm{ITD}(M)_{\vec{x}}(\delta, a) \cong [M]_{\mathrm{Esp}}^{\mathcal{D}}(R_{\vec{x}}^{\mathrm{see}}(\delta), a). $$

**8.3. Relating the Interpretations.** We first relate the reflexive objects.

**Theorem 8.3.** We have an adjoint equivalence of groupoids: $L^U : \mathcal{G}(U) \simeq \mathcal{D}^* : R^U$.

*Proof.* First, $\mathcal{G}(U)$ is *isomorphic* to that presented via the grammar in Figure 9. Indeed,

$$ \mathcal{G}(U) = \mathcal{G}(\otimes^{\mathbb{N}}!U \to o) \cong \mathcal{G}(\otimes^{\mathbb{N}}!U) \times \mathcal{G}(o) $$
$$ [g : a \to b] \left( \frac{f : a' \to a}{\diamond, \dots, \langle a' \rangle, \dots, \diamond \vdash a} \right) = \frac{g \circ f : a' \to b}{\diamond, \dots, \langle a' \rangle, \dots, \diamond \vdash b} $$

$$ [g : a' \to b] \left( \frac{\begin{smallmatrix} \pi \\ \vdots \\ \delta, \vec{a} \vdash a \\ \vdots \\ f : (\vec{a} \to a) \to a' \end{smallmatrix}}{\delta \vdash a} \right) = \frac{\begin{smallmatrix} \pi \\ \vdots \\ \delta, \vec{a} \vdash a \\ \vdots \\ g \circ f : (\vec{a} \to a) \to b \end{smallmatrix}}{\delta \vdash b} $$

$$ [g : a \to b] \left( \frac{\begin{smallmatrix} \pi_0 \\ \vdots \\ \gamma_0 \vdash \vec{a} \to a \\ \vdots \\ \pi_i \\ \vdots \\ \gamma_i \vdash a_i \end{smallmatrix}^{k}_{i=1} \quad \eta : \delta \to \bigotimes_{j=0}^{k} \Gamma_j}{\delta \vdash a} \right) = \frac{[id_{\vec{a}} \to g]\pi_0}{\gamma_0 \vdash \vec{a} \to b} \quad \left( \frac{\begin{smallmatrix} \pi_i \\ \vdots \\ \gamma_i \vdash a_i \end{smallmatrix}^{k}_{i=1}}{\Delta \vdash b} \quad \eta \right) $$

where $\vec{a} = \langle a_1, \dots, a_k \rangle$.

<caption>Figure 7: Left action on derivations.</caption>

$$ \frac{\begin{array}{c} \pi_0 \\ \vdots \\ \gamma_0 \vdash \vec{b} \to a \\ \vdots \\ \pi_0 \{\theta_0\} \\ \vdots \\ \gamma_0 \vdash \vec{a} \to a \end{array}}{\delta \vdash a} \left( \begin{array}{c} [f_i] \pi_{\sigma(i)} \\ \vdots \\ \gamma_{\sigma(i)} \vdash b_i \end{array} \right)_{i=1}^k (id_{\gamma_0} \otimes \sigma^*) \circ \eta \sim \frac{\begin{array}{c} [\vec{f}^\sigma \to id_a] \pi_0 \\ \vdots \\ \gamma_0 \vdash \vec{a} \to a \\ \vdots \\ \pi_0 \{\theta_i\} \\ \vdots \\ \gamma_i \vdash a_i \end{array}}{\delta \vdash a} \left( \begin{array}{c} \pi_i \\ \vdots \\ \gamma_i \vdash a_i \end{array} \right)_{i=1}^k \eta \sim \frac{\begin{array}{c} \pi_0 \\ \vdots \\ \gamma_0' \vdash \vec{a} \to a \\ \vdots \\ \pi_0 \{\theta_0\} \\ \vdots \\ \gamma_0' \vdash \vec{a} \to a \end{array}}{\delta \vdash a} \left( \begin{array}{c} \pi_i \\ \vdots \\ \gamma_i' \vdash a_i \end{array} \right)_{i=1}^k ((\bigotimes_{j=0}^k \theta_j) \circ \eta) \sim \frac{[g] \pi \{id_\delta, \vec{g}^\sigma\}}{\delta \vdash b} \frac{\begin{array}{c} \pi \\ \vdots \\ \delta, \vec{a}' \vdash a' \\ \vdots \\ f : (\vec{a}' \to a) \to b \end{array}}{\delta \vdash b} \frac{\begin{array}{c} \pi \\ \vdots \\ \delta, \vec{a}' \vdash a \\ \vdots \\ f : (\vec{a} \to a) \to b \end{array}}{\delta \vdash b} $$

where $\langle f_1, \dots, f_k \rangle^\sigma : \vec{a} = \langle a_1, \dots, a_k \rangle \to \vec{b} = \langle b_1, \dots, b_k \rangle$, $\vec{g}^\sigma : \vec{a}' \to \vec{a}$, $g : a \to a'$ and $\theta_i : \gamma_i \to \gamma_i'$.

$\sigma^*$ denotes the canonical morphism $\sigma^* : \bigotimes_i^k \Gamma_i \to \bigotimes_{i=1}^k \Gamma_{\sigma(i)}$ for a permutation $\sigma$.

<caption>Figure 8: Congruence on derivations.</caption>

where $\mathcal{G}(o) = \{\emptyset\}$. Likewise, (the obvious infinitary generalization of) (7.2) informs a bijection between $\mathcal{G}(\otimes^\mathbb{N}!U)$ and the sequences $\prod_{n \in \omega} \mathcal{G}(!U)$ which are empty almost everywhere – those may be represented uniquely as sequence $(x_1, \dots, x_n)$ where $x_i \in \mathcal{G}(!U)$ and $x_1$ is non-empty, removing the heading infinite stream of empty configurations. Finally, $\mathcal{G}(!U)$ is in bijection with families $(x_i)_{i \in I}$ for $I \subseteq f \mathbb{N}$, as outlined in the proof of Proposition 7.4. From these observations, the claimed bijection is direct and extends to symmetries.
Objects:

$$
\begin{array}{r@{\;}c@{\;}l@{\quad}l}
\mathcal{G}(\mathbf{U}) \ni v & ::= & (\bar{v}_1, \dots, \bar{v}_k) \dashv\!\!\dashv & (\bar{v}_1 \text{ non-empty.}) \\
& & \bar{v} ::= (v_i)_{i \in I \subseteq f}^{N}
\end{array}
$$

Morphisms:

$$
\begin{array}{c@{\qquad}c}
\begin{array}{c}
\theta_i : \bar{v}_i \cong \bar{v}_i' \\
\hline
(\theta_1, \dots, \theta_n) \dashv\!\!\dashv : (\bar{v}_1, \dots, \bar{v}_n) \dashv\!\!\dashv \rightarrow (\bar{v}_1', \dots, \bar{v}_n') \dashv\!\!\dashv
\end{array}
&
\begin{array}{c}
\pi : I \cong I' \\
\hline
(\theta_i)_{i \in I}^{\pi} : (v_i)_{i \in I} \rightarrow (v_j')_{j \in I'}
\end{array}
\end{array}
$$

<figure><img src="image_31.png" /><figcaption>Figure 10: Compatibility with unfoldings</figcaption></figure>

Hence, we treat Figure 9 as a syntactic presentation of $\mathcal{G}(\mathbf{U})$. Armed with this, we may
now define the components of the desired equivalence simply by induction, with:

$$
\begin{align*}
L^{\mathcal{U}}((\bar{v}_1, \dots, \bar{v}_k) \dashv \ast) &= L^{\mathcal{U}}(\bar{v}_1) \dashv \dots \dashv L^{\mathcal{U}}(\bar{v}_k) \dashv \ast \\
L^{\mathcal{U}}((v_i)_{i \in I}) &= \langle L^{\mathcal{U}}(v_{i_1}), \dots, L^{\mathcal{U}}(v_{i_n}) \rangle \quad (\text{where } I = \{i_1 < \dots < i_n\})
\end{align*}
$$

$$
\begin{align*}
R^{\mathcal{U}}(\langle\rangle \dashv a) &= R^{\mathcal{U}}(a) \\
R^{\mathcal{U}}(\vec{a}_1 \dashv \dots \dashv \vec{a}_n \dashv \ast) &= (R^{\mathcal{U}}(\vec{a}_1), \dots, R^{\mathcal{U}}(\vec{a}_n)) \dashv \ast \quad (\vec{a}_1 \text{ non-empty}) \\
R^{\mathcal{U}}(\langle a_1, \dots, a_n \rangle) &= (R^{\mathcal{U}}(a_i))_{1 \le i \le n}
\end{align*}
$$

which easily extends to an equivalence as claimed.

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

Additionally, this equivalence is compatible with unfoldings in the sense that the diagram
of Figure 10 commutes, and compatible with folding in the same way.

Using our Theorem 7.22, it follows that:

**Theorem 8.4.** For any closed term *M*, we have a natural iso

$$
[[M]]_{\text{Esp}}^{D*} \cong [[[M]]_{\text{Wis}_!}^{U}]^{\|!} \circ R^U
$$
This shows that, for $a \in \mathcal{D}^*$, the set $[M]_{\text{Esp}}^{\mathcal{D}^*}(a)$ described in Theorem 8.2 as a set of derivations up to congruence may be equivalently described, up to canonical isomorphism, as

$$ \{(x, \theta^+) \mid x \in \mathcal{C}^+([M]_{\text{Wis}!}^{\mathcal{U}}), \theta^+ : \partial(x) \cong_{\mathcal{U}} R^{\mathcal{U}}(a)\}. $$

In other words, the interpretation of pure $\lambda$-terms as species computes the set of $+-$ covered configurations equipped with a positive symmetry. Interestingly, this set is constructed without quotient, and thus provides canonical representatives for the equivalence classes of derivations. We now include a detailed example illustrating this by examining the interpretation of a simple $\lambda$-term in both models.

**Example 8.5.** Take the $\lambda$-term $M = xx$. We shall compute its species interpretation on appropriate points and then compare it to its concurrent game semantics.

The species interpretation of $xx$ consists of a distributor

$$ [xx]_{\text{Esp}}^{\mathcal{D}^*}(-; -) : \text{Sym}(\mathcal{D}^*)^{op} \times \mathcal{D}^* \to \text{Set} $$

We evaluate the functor on $[xx]_{\text{Esp}}^{\mathcal{D}^*}(\langle\langle*, *\rangle\rangle \to *, *, *; *)$. To compute an element of this set, we shall exploit the type theoretic presentation of the semantics. Following Figure 5, an element of $[xx]_{\text{Esp}}^{\mathcal{D}^*}(\langle\langle*, *\rangle\rangle \to *, *, *; *)$ can be defined by the following derivation scheme:

$$ \begin{array}{ccc} \begin{array}{c} f : c_0 \to (\langle b_1, b_2 \rangle \to *) \\ x : \langle c_0 \rangle \vdash x : \langle b_1, b_2 \rangle \to * \end{array} & \begin{array}{c} g_1 : c_1 \to b_1 \\ x : \langle c_1 \rangle \vdash x : b_1 \end{array} & \begin{array}{c} g_2 : c_2 \to b_2 \\ x : \langle c_2 \rangle \vdash x : b_2 \end{array} \\ \eta & & \\ \hline x : \langle\langle*, *\rangle\rangle \to *, *, * \rangle \vdash xx : * \end{array} $$

written $\pi_{\eta}^{f,g_1,g_2}$, where $\eta = (f_0, f_1, f_2) : (\langle\langle*, *\rangle\rangle \to *, *, *) \to (c_0, c_1, c_2)$. as a consequence of Theorem 8.1, we have $c_0 = \langle a_1, a_2 \rangle \to a$ and $f = \langle f_1, f_2 \rangle^{\tau} \to g$ with $f_1 : b_{\tau i} \to a_i, g : a \to *$.

Then, by the congruence on derivations induced by the coend formula, we have that

$$ \begin{array}{c} \pi_{\eta}^{f,g_1,g_2} \sim \\ \hline \begin{array}{c} \displaystyle \frac{id_{\langle b_1, b_2 \rangle \to *} \qquad \frac{id_{b_1}}{x : \langle b_1 \rangle \vdash x : b_1} \qquad \frac{id_{b_2}}{x : \langle b_2 \rangle \vdash x : b_2} \qquad (f, g_1, g_2) \circ \eta}{x : \langle\langle b_1, b_2 \rangle\rangle \to *} \vdash x : \langle b_1, b_2 \rangle \to * \end{array} \\ \hline x : \langle\langle*, *\rangle\rangle \to *, *, * \rangle \vdash xx : * \end{array} $$

Hence, we can restrict to the derivation scheme:

$$ \begin{array}{c} \displaystyle \frac{id_{\langle b_1, b_2 \rangle \to *} \qquad \frac{id_{b_1}}{x : \langle b_1 \rangle \vdash x : b_1} \qquad \frac{id_{b_2}}{x : \langle b_2 \rangle \vdash x : b_2} \qquad \theta}{x : \langle\langle b_1, b_2 \rangle\rangle \to *} \vdash x : \langle b_1, b_2 \rangle \to * \qquad \theta} \\ \hline x : \langle\langle*, *\rangle\rangle \to *, *, * \rangle \vdash xx : * \end{array} \qquad (8.1) $$

where $\theta = \langle h_0, h_1, h_2 \rangle^{\sigma}$, where the permutation $\sigma$ is either the identity or the swap between the two occurrences of $*$. Actually, one can prove that there are just two different equivalence classes of derivations in $[xx]_{\text{Esp}}^{\mathcal{D}^*}(\langle\langle*, *\rangle\rangle \to *, *, *; *)$. These correspond precisely to the choice of either the identity or the swap permutation in the following restricted schema:

$$ \begin{array}{c} \displaystyle \frac{id_{\langle*, *\rangle \to *}}{x : \langle\langle*, *\rangle\rangle \to *} \vdash x : \langle*, *\rangle \to * \qquad \frac{id_*}{x : \langle*\rangle \vdash x : *} \qquad \frac{id_*}{x : \langle*\rangle \vdash x : *} \qquad \theta}{x : \langle\langle*, *\rangle\rangle \to *, *, * \rangle \vdash xx : *} \end{array} \qquad (8.2) $$
where now $\theta = \langle h_0, h_1, h_2 \rangle^\sigma$ with $h_i$ being the appropriate identity morphism. This happens because for any isomorphism $b_1 \cong *$, $b_2 \cong *$, we can prove that 8.1 and 8.2 are equivalent by the rules of congruence (Figure 8).

Now, let us consider the game semantics side of things. As $xx$ has just one free variable, $[[x x]]_{\mathbf{Wis}_i}$ is a strategy on $!U \vdash U$. For our example, the useful unfolding of that is $!((\otimes^N!U) \dashv o) \vdash U$ – and following the equivalence of Theorem 8.3, the point $(\langle\langle*, *\rangle\rangle \dashv *, *, *; *)$ corresponds to the configuration in the diagram below:

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

where the numbers in index are the copy indices, corresponding to the distinct copies generated by the exponential modality – $x$ is called three times, and one of these calls its argument twice; the copy indices simply follow the rank in the sequence representation in $\mathcal{D}^*$. Now, the configurations of $[[x x]]_{\mathbf{Wis}_i}$ whose display is symmetric to the above turn out to be those of the form

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

for arbitrary $i, j \in \mathbb{N}$. If we insist that the display is positively symmetric to the configuration above, then this fixes $i = 0$ and $j = 1$, so that there is only one such configuration of $[[x x]]_{\mathbf{Wis}_i}$. Any finally, there are exactly two positive symmetries

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

as the only degree of freedom is whether or not to swap the two standalone positive qs. Hence, we recover the same number of witnesses as in generalized species of structure; though as the reader can observe, the reasoning and the objects of study are very different.

Finally, in what follows, we show how our cartesian closed pseudofunctor allows us to transfer results from game semantics to generalized species. It is known that the game semantics of the $\lambda$-calculus captures the maximal sensible $\lambda$-theory $\mathcal{H}^*$, because strategies coincide with the corresponding normal forms, Nakajima trees – this was first shown in traditional game semantics by Ker et al. [KNO02], and adapted to concurrent games (additionally with probabilistic choice) – in [CP18]. Using Theorem 8.4, we can deduce a result on the $\lambda$-theory induced by $\mathcal{D}^*$. Given a model $\mathcal{D}$ of $\lambda$-calculus in an arbitrary bicategory, the *theory* induced by $\mathcal{D}$ is the $\lambda$-theory induced by the relation on $\lambda$-terms:

$$ \{(M, N) \mid M, N \in \Lambda \text{ s.t. } [[M]]^D \cong [[N]]^D.\} $$
The correspondence established in this paper allows us to derive the following new result:

**Corollary 8.6.** The theory of $\mathcal{D}^*$ is $\mathcal{H}^*$.

*Proof.* Consider two $\lambda$-terms $M$ and $N$. If $M \equiv_{\mathcal{H}^*} N$, then $[[M]]_{\mathbf{Wis}_t}^{\mathbf{U}} \cong [[N]]_{\mathbf{Wis}_t}^{\mathbf{U}}$ and by Theorem 8.4, $[[M]]_{\mathbf{Esp}}^{\mathcal{D}^*} \cong [[N]]_{\mathbf{Esp}}^{\mathcal{D}^*}$.

Reciprocally, isomorphisms in **Esp** form a sensible $\lambda$-theory (see [KMO23], Corollary 6.14). As $\mathcal{H}^*$ is the greatest sensible $\lambda$-theory, it must include isomorphisms in **Esp**. $\square$

This is a simple application, but recent work suggests that there is much to explore in
the bicategorical semantics of the $\lambda$-calculus [KMO23].

9. CONCLUSION

In this paper, we have mapped out the links between thin concurrent games and generalized species of structures, two bicategorical models of linear logic and programming languages. By giving a proof-relevant and bicategorical extension of the relationship between dynamic and static models, we have established the new state of the art in this line of work.

This bridges previously disconnected semantic realms. In the past, such bridges have proved fruitful for transporting results between dynamic and static semantics ([CCPW18, CdV20, CP18]). This opens up many perspectives: bicategorical models are a very active field, and several recent developments may be re-examined in light of this connection ([Oli21, TAO18, CdV20]).

Moreover, this work exposes fundamental phenomena regarding symmetries in quantita-
tive semantics. Symmetries lie at the heart of both thin concurrent games and generalized
species, but they are treated completely differently: in **Esp**, witnesses referring to multiple
copies of a resource are closed under the action of all symmetries ("saturated"), whereas
**TCG** relies on a mechanism for choreographing a choice of copy indices, providing an address
for individual resources ("thin"). This distinction is also at the forefront of a recent line
of work on *thin spans of groupoids* [CF23, CF24], which shares with game semantics this
handling of symmetry, without the the combinatorial details of event structures.

ACKNOWLEDGMENT

This work was supported by the ANR project DyVerSe (ANR-19-CE48-0010-01); by the Labex MiLyon (ANR-10-LABX-0070) of Université de Lyon, within the program “Investissements d’Avenir” (ANR-11-IDEX-0007), operated by the French National Research Agency (ANR); by the US Air Force Office for Scientific Research under award number FA9550-21-1-0007; by a Royal Society University Research Fellowship; by a Paris Region Fellowship co-funded by the European Union (Marie Sklodowska-Curie grant agreement 945298); and by the PEPR integrated project EPiQ ANR-22-PETQ-0007 part of Plan France 2030
REFERENCES

[AHM98] Samson Abramsky, Kohei Honda, and Guy McCusker. A fully abstract game semantics for general references. In *LICS*, pages 334–344. IEEE Computer Society, 1998.

[AJM00] Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. *Inf. Comput.*, 163(2):409–470, 2000.

[Bar85] Hendrik Pieter Barendregt. *The lambda calculus - its syntax and semantics*, volume 103 of *Studies in logic and the foundations of mathematics*. North-Holland, 1985.

[BDER97a] Patrick Baillot, Vincent Danos, Thomas Ehrhard, and Laurent Regnier. Believe it or not, AJM's games model is a model of classical linear logic. In *LICS*, pages 68–75. IEEE Computer Society, 1997.

[BDER97b] Patrick Baillot, Vincent Danos, Thomas Ehrhard, and Laurent Regnier. Timeless games. In Mogens Nielsen and Wolfgang Thomas, editors, *Computer Science Logic, 11th International Workshop, CSL '97, Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected Papers*, volume 1414 of *Lecture Notes in Computer Science*, pages 56–77. Springer, 1997.
doi:10.1007/BFb0028007.

[BEM07] Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Not enough points is enough. In Jacques Duparc and Thomas A. Henzinger, editors, *Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings*, volume 4646 of *Lecture Notes in Computer Science*, pages 298–312. Springer, 2007.
doi:10.1007/978-3-540-74915-8\_24.

[Bén73] Jean Bénabou. Les distributeurs. *Université Catholique de Louvain, Institut de Mathématique Pure et Appliquée*, rapport, 33, 1973.

[BM20] Davide Barbarossa and Giulio Manzonetto. Taylor subsumes Scott, Berry, Kahn and Plotkin. *Proc. ACM Program. Lang.*, 4(POPL):1–1:1–23, 2020.

[Bou09] Pierre Boudes. Thick subtrees, games and experiments. In Pierre-Louis Curien, editor, *Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings*, volume 5608 of *Lecture Notes in Computer Science*, pages 65–79. Springer, 2009.
doi:10.1007/978-3-642-02273-9\_7.

[CC24] Simon Castellan and Pierre Clairambault. Disentangling parallelism and interference in game semantics. *Log. Methods Comput. Sci.*, 20(3), 2024.

[CCPW18] Simon Castellan, Pierre Clairambault, Hugo Paquet, and Glynn Winskel. The concurrent game semantics of probabilistic PCF. In *LICS*, pages 215–224. ACM, 2018.

[CCRW17] Simon Castellan, Pierre Clairambault, Silvain Rideau, and Glynn Winskel. Games and strategies as event structures. *Log. Methods Comput. Sci.*, 13(3), 2017.

[CCW14] Simon Castellan, Pierre Clairambault, and Glynn Winskel. Symmetry in concurrent games. In *CSL-LICS*, pages 28:1–28:10. ACM, 2014.

[CCW15] Simon Castellan, Pierre Clairambault, and Glynn Winskel. The parallel intensionally fully abstract games model of PCF. In *2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science*, pages 232–243. IEEE, 2015.

[CCW19] Simon Castellan, Pierre Clairambault, and Glynn Winskel. Thin games with symmetry and concurrent Hyland-Ong games. *Log. Methods Comput. Sci.*, 15(1), 2019.

[CdV20] Pierre Clairambault and Marc de Visme. Full abstraction for the quantum lambda-calculus. *Proc. ACM Program. Lang.*, 4(POPL):63:1–63:28, 2020.
doi:10.1145/3371131.

[CF23] Pierre Clairambault and Simon Forest. The cartesian closed bicategory of thin spans of groupoids. In *38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023*, pages 1–13. IEEE, 2023.
doi:10.1109/LICS56636.2023.10175754.

[CF24] Pierre Clairambault and Simon Forest. An analysis of symmetry in quantitative semantics. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, *Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024*, pages 26:1–26:13. ACM, 2024.
doi:10.1145/3661814.3662092.

[Cla24] Pierre Clairambault. Causal investigations in interactive semantics, 2024. Habilitation à Diriger les Recherches.

[CM10] Ana C. Calderon and Guy McCusker. Understanding game semantics through coherence spaces. In *MFPS*, volume 265 of *Electronic Notes in Theoretical Computer Science*, pages 231–244. Elsevier, 2010.
[COP23] Pierre Clairambault, Federico Olimpieri, and Hugo Paquet. From thin concurrent games to generalized species of structures. In *38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023*, pages 1-14. IEEE, 2023. doi: 10.1109/LICS56636.2023.10175681.

[CP18] Pierre Clairambault and Hugo Paquet. Fully abstract models of the probabilistic lambda-calculus. In Dan R. Ghica and Achim Jung, editors, *27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK*, volume 119 of LIPIcs, pages 16:1-16:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. doi:10.4230/LIPIcs.CSL.2018.16.

[CS10] G S H Cruttwell and Michael A Shulman. A unified framework for generalized multicategories. *Theory and Applications of Categories*, 24(21):580-655, 2010.

[dC18] Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. *Math. Struct. Comput. Sci.*, 28(7):1169-1203, 2018. doi:10.1017/S0960129516000396.

[Ehr63] Charles Ehresmann. Catégories structurées. In *Annales scientifiques de l'École Normale Supérieure*, volume 80, pages 349-426, 1963.

[ER03] Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. *Theor. Comput. Sci.*, 309(1-3):1-41, 2003.

[FGHW08] Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory of generalised species of structures. *Journal of the London Mathematical Society*, 77(1):203-220, 2008.

[FGHW18] Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures. *Selecta Mathematica*, 24(3):2791-2830, 2018.

[FP09] Claudia Faggian and Mauro Piccolo. Partial orders, event structures and linear strategies. In *TLCA*, volume 5608 of Lecture Notes in Computer Science, pages 95-111. Springer, 2009.

[FS19] Marcelo Fiore and Philip Saville. A type theory for cartesian closed bicategories (extended abstract). In *34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019*, pages 1-13. IEEE, 2019. doi:10.1109/LICS.2019.8785708.

[GGV24] Nicola Gambino, Richard Garner, and Christina Vasilakopoulou. Monoidal kleisli bicategories and the arithmetic product of coloured symmetric sequences. *Doc. Math.*, 29:627-702, 2024.

[Gir87] Jean-Yves Girard. Linear logic. *Theor. Comput. Sci.*, 50:1-102, 1987. doi:10.1016/0304-3975(87)90045-4.

[Gir88] Jean-Yves Girard. Normal functors, power series and λ-calculus. *Annals of pure and applied logic*, 37(2):129-177, 1988.

[GJ17] Nicola Gambino and André Joyal. *On operads, bimodules and analytic functors*, volume 249. American Mathematical Society, 2017.

[GM08] Dan R. Ghica and Andrzej S. Murawski. Angelic semantics of fine-grained concurrency. *Ann. Pure Appl. Log.*, 151(2-3):89-114, 2008.

[HO00] J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: I, II, and III. *Inf. Comput.*, 163(2):285-408, 2000. doi:10.1006/inco.2000.2917.

[HS19] Linde Wester Hansen and Michael Shulman. Constructing symmetric monoidal bicategories functorially. *arXiv preprint arXiv:1910.09240*, 2019.

[Joy81] André Joyal. Une théorie combinatoire des séries formelles. *Advances in mathematics*, 42(1):1-82, 1981.

[KMO23] Axel Kerinec, Giulio Manzonetto, and Federico Olimpieri. Why are proofs relevant in proof-relevant models? *PACMPL*, 7(POPL):8:1-8:31, 2023. doi:10.1145/3571201.

[KNO02] Andrew D. Ker, Hanno Nickau, and C.-H. Luke Ong. Innocent game models of untyped lambda-calculus. *Theor. Comput. Sci.*, 272(1-2):247-292, 2002.

[Lac00] Stephen Lack. A coherent approach to pseudomonads. *Advances in Mathematics*, 152(2):179-202, 2000.

[Lai97] James Laird. Full abstraction for functional languages with control. In *LICS*, pages 58-67. IEEE Computer Society, 1997.

[LMMP13] Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. Weighted relational models of typed lambda-calculi. In *28th Annual ACM/IEEE Symposium on Logic in Computer Science*,
LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 301-310. IEEE Computer Society, 2013. doi:10.1109/LICS.2013.36.

[Mel03] Paul-André Mellies. Asynchronous games 1: Uniformity by group invariance, 2003.

[Mel05] Paul-André Mellès. Asynchronous games 4: A fully complete model of propositional linear logic. In *LICS*, pages 386-395. IEEE Computer Society, 2005.

[Mel06] Paul-André Mellès. Asynchronous games 2: The true concurrency of innocence. *Theor. Comput. Sci.*, 358(2-3):200-228, 2006.

[Mel09] Paul-André Mellies. Categorical semantics of linear logic. *Panoramas et syntheses*, 27:15-215, 2009.

[Mel19] Paul-André Mellès. Template games and differential linear logic. In *LICS*, pages 1-13. IEEE, 2019.

[MM07] Paul-André Mellès and Samuel Mimram. Asynchronous games: Innocence without alternation. In *CONCUR*, volume 4703 of *Lecture Notes in Computer Science*, pages 395-411. Springer, 2007.

[NPW79] Mogens Nielsen, Gordon D. Plotkin, and Glynn Winskel. Petri nets, event structures and domains. In *Semantics of Concurrent Computation*, volume 70 of *Lecture Notes in Computer Science*, pages 266-284. Springer, 1979.

[Oli21] Federico Olimpieri. Intersection type distributors. In *36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021*, pages 1-15. IEEE, 2021. doi:10.1109/LICS52264.2021.9470617.

[Paq20] Hugo Paquet. *Probabilistic concurrent game semantics*. PhD thesis, 2020.

[Paq22] Hugo Paquet. Bi-invariance for uniform strategies on event structures. In *MFPS*, 2022.

[RW11] Silvain Rideau and Glynn Winskel. Concurrent strategies. In *LICS*, pages 409-418. IEEE Computer Society, 2011.

[Sav20] Philip Saville. Cartesian closed bicategories: type theory and coherence, 2020. doi:10.48550/arxiv.2007.00624.

[See87] Robert A. G. Seely. Modelling computations: A 2-categorical framework. In *Proceedings of the Symposium on Logic in Computer Science (LICS '87), Ithaca, New York, USA, June 22-25, 1987*, pages 65-71. IEEE Computer Society, 1987.

[Shu10] Michael A Shulman. Constructing symmetric monoidal bicategories. *arXiv preprint arXiv:1004.0993*, 2010.

[Str72] Ross Street. The formal theory of monads. *Journal of Pure and Applied Algebra*, 2(2):149-168, 1972.

[TAO17] Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong. Generalised species of rigid resource terms. In *32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017*, pages 1-12. IEEE Computer Society, 2017. doi:10.1109/LICS.2017.8005093.

[TAO18] Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong. Species, profunctors and Taylor expansion weighted by SMCC: A unified framework for modelling nondeterministic, probabilistic and quantum programs. In *LICS*, pages 889-898. ACM, 2018.

[TO15] Takeshi Tsukada and C.-H. Luke Ong. Nondeterminism in game semantics via sheaves. In *LICS*, pages 220-231. IEEE Computer Society, 2015.

[TO16] Takeshi Tsukada and C.-H. Luke Ong. Plays as resource terms via non-idempotent intersection types. In *LICS*, pages 237-246. ACM, 2016.

[Win07] Glynn Winskel. Event structures with symmetry. *Electron. Notes Theor. Comput. Sci.*, 172:611-652, 2007.

[Woo82] Richard J Wood. Abstract proarrows I. *Cahiers de topologie et géométrie différentielle*, 23(3):279-290, 1982.

[Yon60] Nobuo Yoneda. On ext and exact sequences. *J. Fac. Sci. Univ. Tokyo Sect. I*, 8(507-576):1960, 1960.