Theory and Applications of Categories, Vol. 34, No. 19, 2019, pp. 514–572.

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS
CLOVIS EBERHART, TOM HIRSCHOWITZ
Abstract. We unify previous constructions from our work on concurrent game semantics into a single categorical framework. From an operational description of positions
and moves in some game, called a signature, we produce a pseudo double category, inwhich objects are positions and vertical morphisms are plays. The considered games
are multi-player, so it makes sense to consider embeddings of positions: these are thehorizontal morphisms. Finally, cells may be thought of as embeddings of plays preserving initial and final positions. In order to be suitable for game semantics, the obtained
pseudo double category should enjoy a certain fibredness property. Under suitable hypotheses, we show that our construction actually produces such a fibred pseudo double
category, from which we can define relevant categories of plays, and thus of strategies.
We give a first necessary and sufficient criterion for this to hold and then a sufficient
criterion that can be checked more easily.

Contents
1
2
3
4
5
A

Introduction
Preliminaries
Signatures for pseudo double categories
Fibredness
Conclusion
Miscellaneous properties of presheaf categories

514
518
524
536
566
569

1. Introduction
Game semantics has provided adequate models for a variety of (idealised) programming
languages. Game models have arisen in several variants [19, 28, 1, 24, 25, 31, 5] which,despite their differences, all consider some notion of two-player game, from which they
construct a category with games as objects and strategies as morphisms, and where composition of strategies is obtained through the standard pattern of ‘parallel composition
plus hiding’.
In previous work [18, 9], we constructed models of process calculi, namely CCS [26]and the π-calculus [27], which have a lot in common with standard game models, but
Eberhart is supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST.
Received by the editors 2018-11-22 and, in final form, 2019-06-10.
Transmitted by Richard Garner. Published on 2019-06-14.
2010 Mathematics Subject Classification: 18C50, 03B70, 68Q55.
Key words and phrases: concurrent game semantics, pseudo double categories, factorisation systems.
c Clovis Eberhart, Tom Hirschowitz, 2019. Permission to copy for private use granted.

514

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

515

also a lot of differences. On the one hand, they feature a notion of game and programs
are interpreted as strategies, but, on the other hand, the games are no longer two-player,
and no attempt is made at constructing a category of games and strategies following
the pattern of parallel composition plus hiding. More importantly, the very notions ofpositions and moves look completely different from the standard ones. Indeed, standardly,
a game roughly consists of a collection of moves, and plays are sequences of moves (andthere may not even be a notion of position). In our work, to start with, there is arather elaborate notion of position, intuitively a hypergraph whose nodes model players
and whose edges model communication channels. Moves are then introduced as higherdimensional edges. Thus, plays are some kind of higher-dimensional hypergraphs. Partof the difficulty of our work was to organise plays over a given position X into a category
E(X). A natural notion of strategy is then given by presheaves over this category: if σ isa presheaf over E(X) and u is a play over X, then σ(u) represents all the ways σ has toaccept u.
The complex nature of plays motivated the second author to axiomatise what is needed
for them to yield sensible game models. This resulted in the notion of playground [18],which are pseudo double categories with lots of additional structure and properties.
However, in order to organise plays into categories E(X), without looking into, e.g.,
innocence, only a certain fibredness property is needed. This property holds in our firsttwo models [18, 9], where it was proved by hand, in non-trivial, different ways. For ourlatest work in this area [8], we wanted to rely on a generic construction, hence the present
paper1 .
Our main contribution is thus a generic construction of such fibred pseudo double
categories (i.e., that satisfy the fibredness property) from more basic data. The kind ofbasic data we will use is the notion of signature defined in Section 3, where we constructa pseudo double category D(S) from any signature S. In Section 4, we prove that, undersuitable hypotheses on S, D(S) is fibred. More precisely, we provide two results:• Under a necessary and sufficient, but hard-to-verify condition, essentially sayingthat fibredness is satisfied for all “generators” (called seeds) in S, we prove that
D(S) is fibred (Theorem 4.3.14).
• We then exhibit sufficient, easier-to-verify conditions for the hard-to-verify condition
above to hold (Theorem 4.4.20).
By plugging both results together, we obtain (Corollary 4.4.21) that any S satisfying the
given sufficient conditions yields a fibred D(S).
Overview. Let us briefly sketch how we create such graphical models and show thatthey are fibred. We start from a base category C describing the operational semantics
of a language. This base category comes with a notion of dimension. Objects of lower
dimensions are called players and channels and describe positions of the game, which arebasically graphs of players and channels. Players are the agents of the game and channels
1This paper is based on the preprint [7], on which [8] actually relies.

516

CLOVIS EBERHART, TOM HIRSCHOWITZ

are the means by which they can communicate. For example, in the π-calculus, a position
simply represents the topology of communication between agents, as in:
c
x

y,

a

which represents a position with two players x and y who can communicate through thechannel a, and x knows a private channel c. Objects of higher dimension describe thedynamics of the game. For example, in the π-calculus, a synchronisation where x sends c
on a and y receives it is drawn as on the left below.
c
x0

y0

a

c
x0

a

x

y0

x0

y

x

c

a

y0

y
c

x

a

y

Here, the initial position of the synchronisation is drawn at the bottom, the final positionat the top, and we can see that, in the final position, the avatar y 0 of y knows thechannel c that x has sent them. For the π-calculus, synchronisation corresponds to an
object of higher dimension in the category C. Each object of higher dimension of C isassigned such a graph, which we call a move. We further call the assignment of all thesemoves a signature. A play is a composite (pasting) of such moves. Formally, positions
are presheaves over the first two dimensions of C (the graphs represent the positions’categories of elements). Moves are cospans Y → M ← X of presheaves over C, where X
is the initial position, Y is the final position, and M represents the move. For example,
the cospan corresponding to synchronisation in the π-calculus is drawn next to it, with
X at the bottom, Y at the top, M in the middle, and the morphisms are inclusions.
From any signature S, we build a pseudo double category D(S), which, to simplify,
is a gadget that has a set of objects (here, positions), and for all objects X and Y , a
set of horizontal morphisms X → Y (here, inclusions of X into Y ) and a set of vertical
X (here, plays starting from X and ending in Y ). It also has, for all
morphisms Y
perimeters as below, a set of cells α (which here represents the fact that u embeds into
u0 in a certain sense).
Y

k

Y0

u•

α

•u0

X

h

X0

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

517

We then want to define a category E(X) of plays over a fixed position X whose morphisms
u → u0 would represent the fact that u0 is an extension of u (E(X) depends on thesignature S, but we leave the dependency implicit for readability). The natural definitionof a morphism from u : Y
X to u0 : Y 0
X is thus a tuple of an object Z, a verticalmorphism w : Z → Y , a horizontal morphism h : Z → Y 0 , and a cell α as in:
Z

h

Y0

α

•u0

w•

Y
u•

X

X.

For this definition to yield a category, we need to be able to compose such morphisms,
i.e., to canonically find a dashed part and a β to the solid part of:
Z 00

h0

Z0
β

•

•w0

Y0

h

Z

Y 00

α0

w•
α

Y

•u00

•u0

u•

X

X

X,

so we need to be able to canonically restrict a play w0 to a smaller position Z. This is theproperty we call fibredness: for all plays u : Y
X and morphisms h : X 0 → X, there
must exist a play u0 : Y 0
X 0 and a cell α as below such that, for all commuting diagramsas the solid part of
Y 00
k0
u00 •

k00
α00

X 00

Y0
α0
u0 •

h00

X0

k
α

h0
h

Y
•u

X,

there is a unique dashed arrow k 00 and corresponding cell α00 (this basically means thatu0 is really a restriction of u along h and is necessary for composition in E(X) to be welldefined).

518

CLOVIS EBERHART, TOM HIRSCHOWITZ

To prove fibredness, we appeal to factorisation systems [12, 3]. This algebraic tool
allows to factor all morphisms of a category as r ◦ l, where l and r belong to fixed classes
L and R that are orthogonal, which means that they have a certain lifting property. We
build a factorisation system whose class L is generated by the legs X → M for all cospans
Y → M ← X in the signature (i.e., for all moves). This allows us to compute restrictions
as follows.
X is a cospan of presheaves Y → U ← X, so we are
Remember that a play u : Y
actually faced with a situation like the solid part of the left-hand side diagram below,
which we complete by factoring l ◦ h as h0 ◦ l0 (using the factorisation system) and thentaking the pullback of f and h0 .
Y 00
Y0

h00

f0

Y
f

f 00

q 00
s00

U 00
s0

U0

h0

l0

X0

U
l

h

f0

l00

U0

X 00

l0

h00

X0

Y
f

q0
h0

U
l

q
s

X

Y0

h

X

We then get the desired universal property by building s0 and s00 in the right-hand side
diagram: the former comes from the lifting property of our factorisation system (between
l00 and h0 ), and the latter follows by universal property of pullback.
It then remains to show that Y 0 → U 0 ← X 0 is a play, which we prove by induction,
under the hypothesis that it is the case for moves. We then give a sufficient criterion on
C for the restriction to be a play.

2. Preliminaries
In this section, we recall a few needed notions and constructions. In Section 2.1, we recall
pseudo double categories, which will be at the heart of our construction. Factorisation
systems are then recalled in Section 2.2. They will play a crucial role in showing thatthe pseudo double categories we produce are fibred. Finally, in Section 2.3, we introduce
a variant of the π-calculus, tailored to our needs. Other useful, technical results fromthe literature about monos, pullbacks, and pushouts in Set and presheaf categories arecollected in Appendix A.
2.1. Pseudo double categories. A pseudo double category [10, 11, 15, 16, 22, 13] D
consists of the following data.
• A set ob(D) of objects.

519

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS• For each pair of objects X, X 0 in ob(D), a set of horizontal morphisms Dh (X, X 0 )and a set of vertical morphisms Dv (X, X 0 ). We distinguish both sets notationallyby writing morphisms in Dh with normal arrows and morphisms in Dv with.
• For each square as below left, a set of cells D(h, h0 , u, u0 ), pictured as on the right.
X0

Y0

h

u0

u

X

X0

h

Y0

u

α

u0

Y

h0

X

Y

h0

• Composition and identities for Dh and Dv .
• Horizontal composition and identities
h

A

α

u

C

k

B

β

v

D

h0

E
w

7→

E

β◦α

u

F

k0

k◦h

A

C

k0 ◦h0

id A

A

w

u

F

A

id u

B

u

B.

id B

• Vertical composition and identities
A

h

B

u

α

u0

C

h0

v

E

β

h00

D

h

A
7→

β•α

v•u

E

v0

B

F

h00

B

id •h

id •A

v 0 •u0

h

A

id •B

B.

h

F

• For all vertical morphisms A u B

v

C

w

C, cells

Aw•(v•u)A

αu,v,w

A(w•v)•uid •B •u

D

λu

A
u

B

u•id •AρuuB(where trivial border means identity border).
These data are furthermore subject to the following conditions:• Horizontal composition of morphisms and cells is associative and unital, i.e., verticalmorphisms and cells form a category.

520

CLOVIS EBERHART, TOM HIRSCHOWITZ• Vertical composition of morphisms and cells is associative and unital up to thenatural and coherent isomorphisms αu,v,w , λu , and ρu . Coherence is here a generalisation of coherence for monoidal categories, see Garner [13] for the full definition.
In particular, Dv forms a bicategory.
• The interchange law holds, in the sense that both ways of parsing the following
diagram coincide:
X

l

u

α

Y

k

v

Z

β
h

X0
Y

u0
0
v0

Z

l0

X 00

α0
k0
β0

0
h0

Y

u00
00
v 00
00

Z ,

i.e., (β 0 ◦ β) • (α0 ◦ α) = (β 0 • α0 ) ◦ (β • α).
2.1.1. Notation. We denote the vertical, resp. horizontal, domain and codomain mapsby domv (α), codv (α), domh (α), and codh (α). E.g., in the first given cell α above, we haveu = domh (α), u0 = codh (α), h = domv (α), and h0 = codv (α).
We denote by DH the category with vertical morphisms as objects and cells as morphisms, and by DV the bicategory with horizontal morphisms as objects and cells asmorphisms. Domain and codomain maps extend to functors domv , codv : DH → Dh anddomh , codh : DV → Dv . We will refer to domv and codv simply as dom and cod, reserving
subscripts for domh and codh .
The game semantical intuition of a double category is as follows. Objects are thoughtof as positions in a certain, potentially multiparty game, and horizontal morphisms asembeddings of positions. This means positions may be parts of global positions in thegame, e.g., the immediate neighbourhood of a particular player. Vertical morphisms
Y , then, are thought of as plays with initial position Y and final position X (theX
direction is chosen to make fibredness look like taking pullbacks).
Some of our constructions will be based on the following example:
2.1.2. Example. Starting from any category C with pushouts, consider the pseudo double category Cospan(C) with
• C itself as horizontal category, i.e., Cospan(C)h = C,
• as vertical morphisms X

Y all cospans X → U ← Y , and• as cells all commuting diagrams
X

k

X0

U

l

U0

Y

h

Y 0,

(1)

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

521

with dom(k, l, h) = k, domh (k, l, h) = (X → U ← Y ), etc.
Composition in Cospan(C)v is defined by (some global choice of) pushout and composition
in Cospan(C)V follows by universal property of pushout.
2.2. Factorisation systems. Factorisation systems [12, 3] are a tool we will use toprove that the pseudo double categories we produce are fibred.
In any category C, we say that l : A → C is left orthogonal to r : B → D, or equivalently
that r is right orthogonal to l, if and only if for all commuting squares as the solid part of
A
l

C

u

B

d

r

v

D,

there exists a unique d as shown making both triangles commute.
2.2.1. Notation. We denote by l ⊥ r the existence of a unique such d for all u and v,
and extend the notation to sets of arrows by writing L ⊥ R when l ⊥ r for all l ∈ L
and r ∈ R. Similarly, L⊥ denotes the class of all arrows that are right orthogonal to allarrows of L, and symmetrically for ⊥ R.
2.2.2. Definition. A factorisation system on a category C consists of two classes ofmaps L and R such that L = ⊥ R, L⊥ = R, and any morphism f : C → D factors as
lf

rf

C−
→ Af −→ D with lf ∈ L and rf ∈ R.
2.2.3. Notation. In accordance with standard notation for epi-mono factorisation (see, while arrows in R
next example), arrows in L are denoted with the special arrow tip
are denoted with.
2.2.4. Example. The first example of a factorisation system is given by the classes Epi
and Mono, respectively of surjections and injections, in Set. Indeed, it is well-known that
all functions factor through their images as a surjection followed by an injection. Perhaps
less well-known is that Epi and Mono are orthogonal. Indeed, take a commuting square
X

u

r

l

Y

X0

v

Y0

with l ∈ Epi and r ∈ Mono. Then the definition d(l(x)) = u(x) indeed defines a function:
any y in Y has an image through d because l is surjective, and the definition does notdepend on the chosen x because, if l(x1 ) = l(x2 ), then r(d(l(x1 ))) = r(u(x1 )) = v(l(x1 )) =v(l(x2 )) = r(u(x2 )) = r(d(l(x2 ))), and r is injective. This is the only choice of function
from Y to X 0 that makes both triangles commute because r is mono.

522

CLOVIS EBERHART, TOM HIRSCHOWITZThis extends to presheaf categories: for any small category C, epi and monic naturalb which we also denote by (Epi, Mono).
transformations form a factorisation system on C,
The classes (Mono, Epi) do not form a factorisation system. For example,
0

2

1

1

possesses two distinct diagonal fillers. (They in fact form a weak factorisation system,
which means that the diagonal filler always exists, but may not be unique.)
The factorisation systems that we will be interested in will be cofibrantly generated.
Cofibrant generation refers to the fact that L and R are defined from some generating set
J, merely by the lifting property: R = J ⊥ and L = ⊥ R. In fact, in many useful cases, it
is even a rather small set. In our case, it will be bounded by the cardinality of C. Though
it is not trivial – this uses the famous “small object” argument, we have:
2.2.5. Theorem. [Bousfield [3]] For any set J of maps in any locally presentable category C, (⊥ (J ⊥ ), J ⊥ ) forms a factorisation system. We say this factorisation system iscofibrantly generated by J.
2.2.6. Example. The (Epi, Mono) factorisation system on Set is cofibrantly generated
b isby the singleton {2 → 1}. For any C, the (Epi, Mono) factorisation system on C
cofibrantly generated by the set of all maps ∇yc : 2 · yc → yc , for c ∈ ob(C).
A crucial property of factorisation systems is the following:
2.2.7. Lemma. For any factorisation system (L, R), L contains all isomorphisms and isstable under right cancellation, composition and pushout.
Stability under right cancellation means that if some composite h ◦ g is in L for g ∈ L,then so is h.
Stability under pushout means that given any pushout square
A

f

l0

l

C

B

g

D,

if l ∈ L, then also l0 ∈ L.
Dually, R contains all isomorphisms and is stable under left cancellation, compositionand pullback (in the obvious dual sense to stability under right cancellation and pushout).
So in particular both classes determine identity-on-objects subcategories of C.

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

523

2.3. The π-calculus. In this section, we introduce a variant of the π-calculus, that wewill use as a running example. It is slightly unusual in the sense that:• its terms are possibly infinite, which spares us the need to define constructors for
replication or to put recursion in our language,• the reduction of terms is done in terms of a chemical abstract machine, in the styleof Berry and Boudol [2].
2.3.1. Definition. Processes of the π-calculus are terms coinductively generated by thegrammarγ ` g P1
γ`

...
X

γ`P
γ`Q
γ `P |Qγ `g P nPii∈nγ, a ` Pγ `g νa.Pγ`Pγ `g τ.Pa∈γγ, b ` Pγ `g a(b).P

a, b ∈ γγ`P,γ `g āhbi.P

where• we have two judgements, ` for processes and `g for guarded processes;• γ ranges over finite sets of natural numbers, and• γ, a is defined if and only if a ∈/ γ and then denotes γ ] {a}.
To define the reduction of our π-calculus, we first need to define the configurations of
the chemical abstract machine:
2.3.2. Definition. A configuration is a pair of a finite set of natural numbers γ and afinite multiset of processes γ ` Pi . We write such a configuration hγ k P1 , . . . , Pn i.
The notation below is a formal definition to make sense of the intuitive notation P + Q
when P is a guarded process and Q is a sum, and which does exactly what one would
expect:P
2.3.3. Notation. For any γ `g P P, γ ` Q of the form i∈n Qi , and injection h : n ,→n + 1, we denote by P +h Q the sum j∈n+1 Pj , where Ph(i) = Qi for all i ∈ n and Pk = P ,for k the unique element of (n + 1) \ Im(h).
We finally define the reduction of configurations:hγ k a(b).P +h R, āhci.Q +h0 R0 i → hγ k P [b 7→ c], Qi
hγ k τ.P +h Ri → hγ k P i

hγ k P | Qi → hγ k P, Qi

hγ k νa.P +h Ri → hγ, a k P i

hγ1 k S1 i → hγ2 k S2 i
hγ1 k S ∪ S1 i → hγ2 k S ∪ S2 i

524

CLOVIS EBERHART, TOM HIRSCHOWITZ

3. Signatures for pseudo double categories
In this section, we define the notion of signature and illustrate it with the example ofthe π-calculus. We start by generalising the method used in the previous sheaf models
to define the notion of signature. We then abstractly give the construction of the pseudo
double category D(S) associated to any signature S. Finally, we define the relevant categories of plays from D(S), and introduce fibredness in passing, as a natural condition forcomposition to be well-defined in such categories.
Any signature S will comprise a base category C, and D(S) will be a sub-pseudo doubleb (as defined in Example 2.1.2). Very roughly, C will be equipped
category of Cospan(C)with a notion of dimension, and S will consist of a selection of cospans
s

t

Y →
− M←
−X

(2)

b v , where X and Y have dimension at mostb viewed as morphisms Y
X in Cospan(C)in C
1 and M may have arbitrary dimension. We will call these cospans seeds. The intuitionis that presheaves of dimension ≤ 1 model positions in a game (they are essentiallygraphs), while higher-dimensional presheaves model the dynamics of the game. Thus
each cospan (2) models a play, starting in position X and ending in position Y , and M
models how the play evolves from X to Y . Up to some technicalities, D(S) is the smallest
b whose objects are positions and whose vertical
sub-pseudo double category of Cospan(C)morphisms contain seeds.
3.1. A signature for the π-Calculus. In this section, we define a signature Sπ forthe π-calculus to explain and motivate the abstract notion of signature we will use in therest of the paper.
Our method may be decomposed into two steps. In the first step, we first design abase category C over which finitely presentable presheaves will model plays. This basecategory C comes with a notion of dimension:• objects of dimensions 0 and 1 are used to model positions in the game, they represent
channels and players respectively, where channels are the communication channels
players use to interact,• objects of dimension ≥ 2 represent typical moves in the game.
b that model typical moves: Y → M ← X will
We also pick a family of cospans in C
represent a move M whose initial position is X and whose final position is Y . We callsuch cospans the seeds of our game. The cospans we pick should satisfy some form ofcompatibility if we want our model to be fibred, so we actually pick a functor S : C|≥2 →b H , where C|≥2 is the full subcategory of C spanning the objects of dimension
Cospan(C)≥ 2. In the second step (see Section 3.3 for details), we construct the smallest sub-pseudobdouble category of Cospan(C)• whose objects are positions,

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

525• whose vertical morphisms include all identities and seeds, and• which contains all pushouts of the form
id •h

id •Z

id •Z 0S(µ)

M,

for all moves µ in C|≥2 and morphisms h : Z → Z 0 between positions.
The last point intuitively says that moves (modelled by seeds) may occur in context.
We will here produce our example signature Sπ . The signature we get is exactly theone we used for our previous model of the π-calculus [9]. By then applying the second
step to Sπ , we get exactly the pseudo double category that our model of the π-calculus
is built on. The model of CCS defined in [18] and the variant of HON games obtainedin [8] are obtained by defining signatures for CCS and HON games and applying the samemachinery.
Let us describe the game based on the operational description of our π-calculus given
in Section 2.3. A position will be a finite hypergraph (i.e., a graph in which edges do notlink two vertices but an arbitrary number of them). In a position, we call nodes players
and edges channels. A player who is linked to n channels is a placeholder for a processγ ` P with n free communication channels, i.e., where |γ| = n. A channel that is linked
to n players is thought of as a communication channel that is shared by n processes. Our
game is intrinsically multi-party in the sense that there are several players in a play.
3.1.1. Example. The position below is a position with three players x, y1 , and y2 , andtwo channels c1 and c2 . The first channel c1 is shared between all three players, while thesecond channel c2 is private to x.
y1
c1

x

c2

y2

Formally, positions are presheaves over the following category:
3.1.2. Definition. Let C1 have
• an object ∗,• an object [n] for each n in N,• morphisms s1 , . . . , sn : ∗ → [n] for each n in N.
The ∗ object represents channels, while [n] objects represent n-ary players.

526

CLOVIS EBERHART, TOM HIRSCHOWITZ

3.1.3. Example. The informal position of Example 3.1.1 is modelled as the presheaf X
withX(∗) = {c1 , c2 },X([1]) = {y1 , y2 },X([2]) = {x},X([n]) = ∅ otherwise,x · s 1 = c1 ,and x · s2 = c2 .

and whose action on non-trivial morphisms is:
y 1 · s 1 = c1 ,y2 · s1 = c1 ,The graphical representation we have given in Example 3.1.1 is a representation of thecategory of elements of X (the only information lost with that representation is the orderof channels, i.e., whether x · s1 is c1 or c2 ).
Let us now describe moves in the game. They are typically given by the operationaldescription of the language, which, in the case of the π-calculus, are the rules given in
Section 2.3. Each rule in our calculus will correspond to a move in our game.
The move for parallel composition goes as follows: a player x may fork to turn into
two new players who know the same channels as x. Graphically, if the player who plays
the move is binary (i.e., they know two channels), this is pictured as:
y2

y1
π

x

,

where the starting position is pictured at the bottom (it has one player x who knows twochannels) and the final one at the top (it has two players y1 and y2 who know exactly thesame channels as x). There is also something in the middle denoted by π that represents
the action of forking itself, but we do not delve into details here, as we only give an
informal presentation. This move is in accordance with the intuition that it should model
the operational description of the rule for parallel composition: according to this rule, aprocess γ ` P | Q turns into a pair of processes γ ` P and γ ` Q that know exactly thesame channels (i.e., among the channels in γ).
Following the same intuition, we easily define moves for the silent τ action and channel
creation. In the first case, a process γ ` τ.P +h R turns into a process γ ` P , i.e., a processthat knows exactly the same channels. In the second case, a process γ ` νa.P +h R turns
into a process γ, a ` P , i.e., a process that knows exactly the same channels, plus a new,fresh channel a. They are depicted as below left and below right respectively, again in
the case where the initial player is binary.
y

y

τ

x

ν

x

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

527

Finally, the synchronisation rule is slightly more complex, and the move reflects theintuition of message passing: when two processes γ ` a(b).P +h R and γ ` āhci.Q +h R0
synchronise and turn into γ ` P [b 7→ c] and γ ` Q, Q sends its channel c on a and P
receives it and treats it as a fresh channel. Therefore, if a(b).P knows n channels among
the channels of γ, P [b 7→ c] knows n + 1 of these channels (there may be repetitions, e.g.,if a(b).P already knows c, then P [b 7→ c] knows c “twice”). Moreover, note that, for bothprocesses to communicate, they need to share a common channel a. If we represent thismove graphically, for a player x who knows two channels a and c and who sends c on a,
and a player y who knows only one channel a, we obtain:
c
x0

y0

a

y,

x

where the initial position is indeed again at the bottom, and in the final position, the twoplayers have turned into x0 and y 0 , and y 0 knows c. Just like in the other moves, there issomething in the middle that represents the action of synchronising itself: the arrow that
goes from c in the bottom position to c in the top position. Again, we do not dwell on
details here, but intuitively, this arrow represents the path c’s name follows during thesynchronisation: x first fetches it, then sends it on a, the message is received by y, who
thus gains the knowledge of a new channel.
The congruence rule is not turned into a move in our game, as it is typically givenby the fact that moves only have a local effect (i.e., when a player moves, the rest of theposition is left untouched).
Following this description, we augment our base category C1 with new objects andmorphisms that model moves.
3.1.4. Definition. Let C consist of C1 , plus, for all n, m in N, a, b in n, and c, d in m:• objects πnl , πnr , πn , νn , τn , ιn,a , on,a,b , and σn,a,m,c,d ,• for all v in {πnl , πnr , τn , on,a,b }, morphisms s, t : [n] → v,
s

t

s

t

• morphisms [n + 1] →− νn ←− [n] and [n + 1] →− ιn,a ←− [n],lr

ρε• morphisms πnl →− πn ←− πnr and ιn,a →− σn,a,m,c,d ←− om,c,d ,modulo the equations:• s ◦ si = t ◦ si in C(∗, v), for all v in {πnl , πnr , τn , ιn,a , on,a,b , νn } and i in n, with n in
N and a, b in n,

528

CLOVIS EBERHART, TOM HIRSCHOWITZ• l ◦ t = r ◦ t in C([n], πn ), for all n in N,• ρ ◦ t ◦ sa = ε ◦ t ◦ sc and ρ ◦ s ◦ sn+1 = ε ◦ s ◦ sd , in C(∗, σn,a,m,c,d ), for all n, m in N,
a in n, and c, d in m.
The reader may check that drawing the categories of elements of representable presheaves on πn , νn , τn , σn,a,m,c,d look exactly like the intended graphs. We have not yet
mentioned the other objects πnl , πnr , ιn,a , and on,a,b . The first two are technical artefacts
related to the notion of view in innocent game semantics. They provide examples of
non-trivial morphisms between plays (to πn ). The latter two are the restrictions of synchronisation to each one of the two players.
The pseudo double category describing the π-calculus will be a sub-pseudo doubleb entirely determined by the choice of a functor from C|≥2 tocategory of Cospan(C),b H , where C|≥2 denotes the full subcategory of C spanning the objects not in C1 .
Cospan(C)Intuitively, this functor chooses for all objects µ of C|≥2 a cospan which will be thoughtof as the basic play consisting of just µ. This choice of cospans should of course reflect
the intuition given above, specifically, if we choose to model the move µ by a cospan
s
t
Y →
− M ←
− X, then X should represent µ’s initial position, Y its final position, and M
should “represent” µ in some way. We thus pick the cospans as follows:
s

t

− v←
− [n] (where v should really be yv , but we• for all v in {πnl , πnr , τn , on,a,b }: [n] →keep the Yoneda embedding implicit for readability),
s0

lt=rt

• for πn : [n] | [n] −→ πn ←−−− [n], where [n] | [n] is the following pushout, and s0 is
obtained by its universal property:[si ]i∈n

n·∗

[n]
s

injr

[si ]i∈n[n]πnr[n] | [n]

injl

s0

s

πnl
s

l

r

πn ,

t

• for all v in {νn , ιn,a }: [n + 1] →− v←
− [n],s0

t0• for σn,a,m,c,d : [n + 1] a,n+1 | c,d [m] −→ σn,a,m,c,d ←− [n] a | c [m], where [n] a | c [m] is the0following pushout and t is obtained by its universal property:

529

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS
sc

∗

[m]

sa

t

injr

[n]

[n] a | c [m]injlom,c,d
t0

ε

t

ιn,a

σn,a,m,c,d ,ρand similarly for [n + 1]a,n+1 | c,d and s0 :[sc ,sd ]

2·∗

[m]
s

injr

[sa ,sn+1 ][n + 1][n + 1] a,n+1 | c,d [m]injl

om,c,d
s0

ε

s

ιn,a

ρ

σn,a,m,c,d .

3.1.5. Remark. The intuition behind these definitions actually comes from starting withspans to represent the moves (as is usually done in graph rewriting) and augmenting C1
by appealing to cocomma categories, as sketched in [6]. However, starting from spans
makes the whole presentation unnecessarily more intricate (as the approach has to berefined for fibredness to hold), so we only gave the result here.
We finally need to define the functor on morphisms of C|≥2 , which is simple, since there are
few non-trivial morphisms. In fact, all non-trivial morphisms are of one of the following
forms: l : πnl → πn , r : πnr → πn , ε : ιn,a → σn,a,m,c,d , or ρ : om,c,d → σn,a,m,c,d . We summarise
our choice of morphisms in the picture below:
πnl

l

[n]

injl

πnl

l

[n]

πn

r

πnr

ιn,a

[n] | [n]

injr

[n]

[n + 1]

πn

r

πnr

ιn,a

[n]

[n]

[n]

ρ

injl

σn,a,m,c,d

ε

injr

[n + 1] a,n+1 | c,d [m]ρinjl

σn,a,m,c,d[n] a | c [m]om,c,d

ε

injr

[m]
om,c,d[m].

b H denote the obtained functor. We call
3.1.6. Definition. Let Sπ : C|≥2 → Cospan(C)seeds cospans in the image of this functor.
We now need to construct our pseudo double category based on this. Before proceeding, as we intend to provide a generic construction, we reflect a bit on the properties ofour functor Sπ , which leads us to the notion of signature.

530

CLOVIS EBERHART, TOM HIRSCHOWITZ

3.2. Signatures. We now discuss a few elementary properties of the functor Sπ : C|≥2 →b H of Definition 3.1.6. We then abstract over these properties to define our
Cospan(C)notion of signature.
Our first observation is that the category C enjoys a natural notion of dimension: ∗ hasdimension 0, each [n] has dimension 1, all τn , νn , πnl , πnr , ιn,a , and om,c,d have dimension
2, and all πn and σn,a,m,c,d have dimension 3. In particular, C forms a direct category inthe sense of Garner [14], i.e., it comes equipped with a functor to the ordinal ω viewed
as a category, which reflects identities. Presheaves X themselves inherit a dimension: theleast n such that X is empty above dimension n. The dimension of any representable isthus that of the underlying object.
b H:
Let us make a few additional observations on our functor Sπ : C|≥2 → Cospan(C)(a) the middle object of each Sπ (µ) is yµ ;(b) both legs of all selected cospans are monic;(c) all morphisms between those cospans have monic components;(d) for all such morphisms, top squares are pullbacks;(e) finally, all initial positions X are tight, in the sense that all channels c ∈ X(∗) arein the image of some X(si ).
So a first, naive notion of signature could consist of a direct category C, equipped withb H satisfying (a)–(e). However, some of the examples we havea functor C|≥2 → Cospan(C)in mind require a bit more generality, so in our abstract definition we relax things a bit.
We also need to add another, less obvious hypothesis for the proof of fibredness to hold.
Let us explain in more details the changes that need to be made to this naive definition.
Even though, in many examples, morphisms between seeds have bottom squares thatare pullbacks, we can see that the π-calculus does not. Indeed, consider the morphismρ : ιn,a → σn,a,m,c,d , the sent channel is present both in ιn,a and the initial position of
σn,a,m,c,d , but not in the initial position of ιn,a . However, we want to have a property close
to that bottom square being a pullback for the proof of fibredness to hold. There are also
relevant, though unpublished examples of base categories in which the top square of amorphism between seeds is not necessarily a pullback. Furthermore, we need the generated
pseudo double category to accommodate morphisms of cospans whose components are
non-injective. Let us thus change our tentative definition just enough to accommodate
these needs. In short, we pass from injective maps to maps which are injective except
perhaps on objects of dimension 0, and find an analogous generalisation for bottom squares
being pullbacks. We also completely drop the requirement on top squares, as it proves
useless in the definition.
Let us fix any small, direct category C for the rest of this section. By analogy withthe base category for π, we think of objects of dimension 1 as players in a game, which
may communicate with each other through objects of dimension 0. Objects of dimensions> 1 are thought of as moves in the game. Accordingly, we use the following terminology:

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

531

3.2.1. Terminology. The dimension of any object of C is its image in ω. A channel
is an object of dimension 0, a player is an object of dimension 1, and a move is an objectof dimension > 1.
3.2.2. Definition. Let a natural transformation of presheaves over C be 1D-injective
when all its components of dimensions > 0 are injective.
b is a 1D-pullback when it is a pullback in all dimensions > 0.
A square in C
3.2.3. Notation. We mark 1D-pullbacks with a dotted little square, as below.
A

B

C

D

b
3.2.4. Definition. Let D0 (C) denote the sub-pseudo double category of Cospan(C)b consisting of positions,• whose horizontal category D0 (C)h is the subcategory of C
i.e., finitely presentable presheaves of dimension ≤ 1, and 1D-injective morphisms
between them,• whose vertical morphisms are cospans with monic legs, andb with 1D-injective components and 1D-pullback• whose cells are those of Cospan(C)bottom squares.
X in D0 (C)v , X and Y are respectively

3.2.5. Terminology. For any vertical u : Y
called the initial and final positions of u.
Definition 3.2.4 only makes sense because:b
3.2.6. Proposition. D0 (C) forms a sub-pseudo double category of Cospan(C).
This relies on the following direct corollary of Lemma A.2.1:
b for any commuting cube
3.2.7. Corollary. In C,
I

B
A

I0

C
B0

A0

f

C 0,

with the marked pushouts and 1D-pullback,• if I 0 → B 0 is 1D-injective then the front square is a 1D-pullback, and• if all arrows except perhaps f are 1D-injective, then f also is.
Proof. By pointwise application of Lemma A.2.1.

532

CLOVIS EBERHART, TOM HIRSCHOWITZ

Proof of Proposition 3.2.6. The only non-trivial bit lies in showing that a verticalcomposite of componentwise 1D-injective cells with 1D-pullback bottom squares again has
1D-injective components and 1D-pullback bottom square. This is a simple consequenceof Corollary 3.2.7 and the pullback lemma.
Let us finally give an abstract definition of tightness as given in (e) for π – though thepresentation differs.
b let us denote by pl(U ) the set of players of
3.2.8. Definition. For all presheaves U in C,
U , i.e., pairs (d, x) for all morphisms x : d → U , whereP d is any representable of dimension
1. Let Pl(U ) denote the corresponding coproduct (d,x)∈pl(U ) d of representables.
A position X is tight if and only if the canonical morphism Pl(X) → X is epi.
3.2.9. Definition. A signature consists of a small, direct category C, together with afunctor S : C|≥2 → D0 (C)H making the following square commuteC|≥2S

D0 (C)H
m

C

y

(3)

b
C,

where m denotes the middle projection functor, such that for all µ ∈ C|≥2 , the initial
position of S(µ) is tight.
3.2.10. Definition. Cospans in the image of S are called the seeds of S.
Letting X, Y, Z, . . . range over positions, we get that any signature S maps any move
M to some cospan Y → M ← X which determines its initial and final positions.
3.2.11. Example. The functor Sπ of Definition 3.1.6 is a signature. Indeed, all morphisms are evidently monic and all bottom squares are 1D-pullbacks (the only one that is
not a pullback is the one that corresponds to ρ : ιn,a → σn,a,m,c,d , and it is straightforwardly
shown to be a 1D-pullback). Furthermore, all initial positions are clearly tight.
Here is an immediate, useful consequence of the definition:
3.2.12. Lemma. The functor S underlying any signature is fully faithful.
Proof. Faithfulness holds by Yoneda and fullness follows from monicity of the legs ofthe involved cospans.
3.3. From signatures to pseudo double categories. We now define and give an
explicit description of the pseudo double category D(S) associated to any signature S.
Let us start with the following observation:

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

533

3.3.1. Proposition. For any pushout square of the formid •hid •Z0

id •Z
(4)

k

S(µ)

P

b H , if h ∈ D0 (C)h (Z0 , Z) and k ∈ D0 (C)H (id • , S(µ)), i.e., h is 1D-injectivein Cospan(C)Z0
and k has 1D-injective components and 1D-pullback bottom square, then the whole squarein fact lies in D0 (C).
Proof. Indeed, given h and id •Z0 → S(µ) as above, the pushout P = (Y → M ← X)
b H . It is computed by taking pushouts levelwise, as inalways exists in Cospan(C)
Y0

Y

µ

M

Z0

(5)

Z
X0

X,

where S(µ) = (Y0 → µ ← X0 ) and the dashed arrows are obtained by universal propertyof pushout. Now, monos are stable under pushouts in Set and colimits are pointwise inpresheaf categories, so 1D-injectivity of all components follows from 1D-injectivity of all
involved morphisms. Finally, both bottom squares are pullbacks, hence 1D-pullbacks as
desired, either by Lemma A.1.1 or by the pushout lemma and Lemma A.1.4.
3.3.2. Remark. In the proposition above, k necessarily has 1D-pullback bottom square.
Indeed, both its top and bottom squares are pullback by Lemma A.1.1.
3.3.3. Definition. A move is any cospan M isomorphic to one obtained as a pushoutof the form (4).
3.3.4. Definition. The pseudo double category D(S) associated to any signature S is thesmallest sub-pseudo double category of D0 (C) such that
• D(S)h is D0 (C)h ;• D(S)H is replete and contains all moves;• D(S) is locally full, i.e., if a cell of D0 (C) has its perimeter in D(S), then it is in
D(S).

534

CLOVIS EBERHART, TOM HIRSCHOWITZ

3.3.5. Remark. By Proposition 3.3.1, saying that D(S) contains all moves entails thatall pushout squares defining moves lie inside D(S).
That D(S) is well-defined is easy: it is the intersection of all sub-pseudo double categories of D0 (C) that verify all three points above, and D0 (C) is obviously one such pseudo
double category, so we are taking the intersection of a non-empty family.
It is still useful to give a concrete description of D(S). First, its horizontal category
is just D0 (C)h . Regarding vertical morphisms, D(S) must contain all moves, and since it
is stable under vertical composition, it must also contain all finite composites of moves.
By repleteness, it should also contain all vertical morphisms isomorphic to such verticalcomposites. We thus define:
3.3.6. Definition. A play is any vertical morphism isomorphic to some vertical composite of moves.
3.3.7. Proposition. D(S) is precisely the locally full sub-pseudo double category of
D0 (C) obtained by restricting vertical morphisms to plays.
Proof. By construction, it is enough to show that the given data forms a sub-pseudob which is easy.
double category of Cospan(C),3.4. Fibredness and categories of plays. For a given pseudo double category D,
the categories of plays studied in previous work [18, 9, 8] come in several flavours. A firstvariant is based on the following category:
3.4.1. Definition. Let E denote the category• whose objects are vertical morphisms of D,• and whose morphisms u → u0 are pairs (w, α) as below left, considered equivalent
up to the equivalence relation generated by equating (w, α) with (w0 , α ◦ (u • γ)), forall cells γ as below right:
T

s

Z0

w

Z

α

u0

r

0

u

Y

T0
w0

γ

T

s

Z0

α

u0

w

Z

(6)

u

Y

Y

r

Y 0.

3.4.2. Notation. We denote the involved equivalence relation by ∼. Furthermore, in
principle, E depends on D, which should appear in the notation. For readability, we will
rely on context to disambiguate.
In order to define composition in this category, one needs to consider all diagrams ofshape the solid part ofFIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

Z 00

s0

Z0
γ

w00

Y0
β

w
α

Y

Y 00

w0

s

Z

535

u00

u0

u

X

X0

r

r0

X 00 .

Fibredness then comes in by requiring the existence of a cell γ as shown, which is canonicalin a certain sense. This allows us to define the composite of (w, α) and (w0 , β) as theequivalence class of (w • w00 , β ◦ (α • γ)).
To state the fibredness property, we first need to recall the definition of fibration.
3.4.3. Definition. For any functor p : E → B, a morphism r : e0 → e in E is cartesianwhen, as below, for all t : e00 → e and k : p(e00 ) → p(e0 ) such that p(r) ◦ k = p(t), there
exists a unique s : e00 → e0 such that p(s) = k and r ◦ s = t:
e00

t
s

e0

p(e00 )

r

e

p(t)
k

p(e0 )

p(r)

p(e).

3.4.4. Definition. A functor p : E → B is a fibration if and only if for all e in E, any
h : b0 → p(e) has a cartesian lifting, i.e., a cartesian antecedent by p with codomain e.
Here is the fibredness property:
3.4.5. Definition. A pseudo double category D is fibred if and only if the codomainfunctor cod : DH → Dh is a fibration.
Y and horizontal
Concretely, fibredness says that given any vertical morphism u : Xmorphism h : B → Y , there exists a cartesian α as below, i.e., such that for all horizontall : D → B, vertical w : C
D, and β : w → u as shown, there exists a unique filler
γ : w → v with lower border l such that α ◦ γ = β.
C
A

X
β

w

γ
v

α

u

D
l

B

h

Y

536

CLOVIS EBERHART, TOM HIRSCHOWITZ

Fibredness is related to Grandis and Paré’s double categorical Kan extensions [17] andto Shulman’s framed bicategories [32].
3.4.6. Proposition. If D is fibred, then E is indeed a category.
3.4.7. Remark. In our concurrent game models [18, 9, 8], we do not directly use E, butrather variants ‘localised’ at some position X. One such variant is the category E(X), forsome position X, whose objects are plays u : Y
X, and morphisms are those of E, ason the left in (6) that have id X as their lower border.
Our next goal is to give an abstract framework to show that, given some signature S,
D(S) is fibred. We want this framework to be abstract enough to be able to use it on theexisting examples of CCS [18], the π-calculus [9], and our signature for HON games [8].

4. Fibredness
In this section, we study the fibredness property abstractly. In order to do that, we first
define a candidate cartesian lifting of any morphism in D(S)h using factorisation systems
and show that it has all the good properties of cartesian liftings, except that it is unclear
whether it lies inside D(S)H , which is proved in the rest of the section. We then recast thedefinitions of 1D-injectivity and 1D-pullbacks in terms closer to the defining properties of
injective maps and pullbacks. We then give a necessary and sufficient condition for ourcandidate lifting to lie in D(S)H , hence for D(S) to be fibred. However, this condition is
not very useful in practice, so, in the last part, we give a sufficient condition for D(S) tobe fibred that is easier to verify.
4.1. Fibredness through factorisation systems. Our main tool to prove thatthe pseudo double category D(S) generated by a signature S is fibred will be cofibrantly
generated factorisation systems. Let us explain the core idea of the proof. In the settingof Example 2.1.2, any factorisation system (L, R) on C yields a fibred sub-pseudo double
category of Cospan(C).
We are going to refine the pseudo double category Cospan(C) into a fibred pseudo
double category. Let us consider CospanL,R (C), the locally full sub-pseudo double categoryof Cospan(C)• whose horizontal category is C,• and whose vertical morphisms Y(recalling Notation 2.2.3).

s

X are cospans Y →− Ul

X with l ∈ L

4.1.1. Proposition. The pseudo double category CospanL,R (C) forms a sub-pseudo double category of Cospan(C) that is fibred if C has pullbacks.

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

537

Proof. That CospanL,R (C) forms a pseudo double category is a simple consequence offLemma 2.2.7. To see that it is fibred, consider any vertical morphism Y →− U l X andhhorizontal morphism X 0 →− X. In order to construct a cartesian lifting of (f, l) along h,0h0

we factor the composite X 0 →− X l U as X 0 l U 0 h U , with l0 ∈ L and h0 ∈ R, andthen take the pullback of f and h0 , as in the front face below:
Y 00
f 00

q 00
s00

Y0

U 00
s0

f0

l00

U0

X 00

l0

h00

f

q0
h0

X0

(7)

U
l

q
s

Y

h

X.

The obtained morphism (h, h0 , h00 ) is generally not cartesian in Cospan(C)H , but let us
show that it is in CospanL,R (C). For this, consider any morphism (q, q 0 , q 00 ) to U such thatq = hs as above; then since l00 ∈ L (by hypothesis) and h0 ∈ R (by construction), we
obtain by the lifting property a unique s0 making everything in sight commute. But thenthe universal property of pullback gives the desired s00 .
Furthermore, in this situation, we may characterise cartesian cells as follows.
b H is cartesian if and only if it has the shape
4.1.2. Lemma. A morphism in CospanJS (C)of the front face of (7), i.e., its top square is a pullback and its middle morphism is inJS⊥ .
Proof. The “if” direction follows from the proof of Proposition 4.1.1. For the converse,b H.
the considered properties are stable under composition with isomorphisms in CospanJS (C)b H / hU 0 i
But any cartesian morphism α : hU i → hU 0 i is uniquely isomorphic in CospanJS (C)to the cartesian lifting of hU 0 i along cod(α) computed as in (7), hence the result.
For any signature S over some base category C, we will try to apply this construction to
the pseudo double category of plays D(S) over S, with the factorisation system cofibrantly
generated (remember Theorem 2.2.5) by the set JS of all “t-legs”, i.e., the set of morphisms
t
s
t
X →
− M for Y →− M ←− X spanning seeds. A map is then in JS⊥ when no new moveis added “forwards”, i.e., following the direction of time. Indeed, recalling that each M
occurring in a seed should be representable, giving a square

538

CLOVIS EBERHART, TOM HIRSCHOWITZ

X

f

r

t

M

U

µ

V

amounts by Yoneda to picking a move µ in V , whose initial position X is already available
in U . The map r is then in R when all such moves are also already in U .
Our goal now reduces to showing that D(S) is fibred as a sub-pseudo double categoryb The difficulty isb – which we henceforth abbreviate to CospanJ (C).
of Cospan⊥ (JS⊥ ),JS⊥ (C)S
that, in a situation like (7), the factorisation system yields a cartesian lifting (h, h0 , h00 ) inb of which we will further need to prove that (1) it lies in D(S)H , and (2) it is
CospanJS (C),also cartesian there. Point (2) reduces to proving that if (q, q 0 , q 00 ) is in D(S)H then so is(s, s0 , s00 ).
In fact, assuming that the candidate lifting is in D(S), its cartesianness follows fromthe fact that all mediating arrows, computed as in (7), are also in D(S). Indeed, we have:b
4.1.3. Lemma. D(S)H has the left cancellation property: for all β and α in Cospan(C)such that β ◦ α and β are in D(S)H , then also α is in D(S)H .
Proof. By 1D-analogues of the pullback lemma and left cancellation for monomorphisms.
It thus remains to prove that the candidate lifting is a play, and that the morphism(h, h0 , h00 ) lies in D(S)H . Let us record this as:
4.1.4. Lemma. Assume that in all situations like (7), if U is a play and h is 1D-injective,then U 0 is again a play and (h, h0 , h00 ) is in D(S)H . Then, D(S) is fibred.
We thus consider conditions for this to hold. In Section 4.3, we show that if it holds
for seeds, then it extends to all plays. In Section 4.4, we investigate conditions for the
result to hold for seeds.
This all relies on a few elementary facts about 1D-pullbacks, 1D-injectivity, and tightness, which we prove in Section 4.2.
4.2. 1D-pullbacks, 1D-injectivity, and tightness. This section is essentially atechnical investigation, but in passing it also clarifies the notions of 1D-pullback, 1Dinjectivity, and tightness. We first recast 1D-pullbacks and 1D-injecvitivy in terms of therestriction to objects of dimension ≥ 1. We first recall the standard chain of adjunctions
induced by restriction. Then, we give characterisations of 1D-notions in terms of theirrestrictions. We also establish 1D-variants of the standard defining properties for pullbacks
and monicity, relative to objects of dimension ≥ 1. Finally, we prove a 1D-variant of theuniversal property of pullbacks, but this time relative to tight positions, together with aneasy consequence, roughly a 1D-pullback lemma relative to tight positions.

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

539

4.2.1. Definition. Let i1 : C|≥1 ,→ C denote the full subcategory spanning objects ofdimension ≥ 1.
We have the standard chain of adjunctions:
P

d
C
|≥1

i1

⊥
∆i1
⊥
Q

b
C,

(8)

i1

Q
P
and right Kan
where ∆i1 , i1 and i1 respectively denote restriction,Qleft Kan extension
Pextension along the opposite of i1 . We will not need i1 here, and i1 essentially adds
the necessary channels in a minimal way. Indeed, a short calculation from the well-known
characterisation of left Kan extensions as coends leads to:XX(c)(if dim(c) ≥ 1)
(X)(c) = R dim(d)≥1
X(d) × C(c, d) (otherwise).
i1

4.2.2. Example. With C as in Definition 3.1.4, in the case dim(c) = 0, we thus have,e.g., n channels for each player of arity n. Furthermore, the coend ensures that, when two
players are the source and target of some move, the needed equations are enforced (e.g.,s ◦ si = t ◦ si ).
In fact, because i1 is fully faithful, the first adjunction is a coreflection:
PP
4.2.3. Proposition. The left adjoint i1 is fully faithful, and the comonad i1 ◦∆i1 isdb
idempotent, so that C|≥1 is a coreflective, full subcategory of C.
Proof. It is well known [20, Proposition 4.23] that the unit of the adjunction is an
isomorphism when we extend and restrict along a fully-faithful functor. Furthermore,
it is also well-known [23] that if the unit of an adjunction is an isomorphism, then theleft adjoint is full and faithful. The comultiplication of the induced comonad is then an
isomorphism by construction.
There is an easy characterisation of 1D-injectivity and 1D-pullbacks in terms of ∆i1 :b is 1D-injective if and only if its image by ∆i is
4.2.4. Proposition. A morphism in C
1
injective.
b is a 1D-pullback if and only if its image by ∆i is a pullback.
A square in C
1
Proof. By definition and the fact that limits are pointwise in presheaf categories.
Let us now establish a characterisation of 1D-injectivity and pullbacks analogous to
the standard defining properties of monicity and pullbacks, though relative to objects of
d
C
|≥1 .

540

CLOVIS EBERHART, TOM HIRSCHOWITZ

b as below left is a 1D-pullback if and only if for all
4.2.5. Proposition. A square in Cd
X ∈C|≥1 , u and v as below right making the outer diagram commute, there is a unique
mediating morphism h as shown, such that ph = u and qh = v:
P
A

q

p

B

i1 (X)

v

C

h

A

g

f

q

C

u

D

p

B

g

f

D.

Proof. This follows from the more general fact that for any full coreflection
L: C

⊥

D :R,

small category J, and functor D : J → D, if RD has a limit in C, then L(limj RD(j)) has
the universal property of a limit of D relative to objects of C, i.e., we have for all X ∈ C:
Z
D(LX, D(j)) ∼= D(LX, L(lim RD(j)))
jj∈Jnaturally in X. Indeed, we haveZ
Z∼
C(X, RD(j)) ∼D(LX, D(j)) == C(X, lim RD(j)) ∼= D(LX, L(lim RD(j))),
j∈J

j

j∈J

j

where the last step is by full faithfulness of L.
b The following are
4.2.6. Proposition. Consider any morphism m : X → Y in C.
equivalent:
1. m is 1D-injective;P
2. for all f, g :i1 (Z) → X, mf = mg implies f = g;
3. the square
X

X
m

X
is a 1D-pullback.

m

Y

(9)

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

541

Proof. By definition, these three items are respectively equivalent to• (1’) ∆i1 (m) is monic,• (2’) for all f, g : Z → ∆i1 (X), ∆i1 (m)f = ∆i1 (m)g implies f = g;
• (3’) the image by ∆i1 of the square (9) is a pullback.
But now these three are well-known to be equivalent.
Finally, we consider similar properties, but relative to tight positions. Let us firstobserve the following characterisation of tightness is terms of the adjunctions (8).
P
4.2.7. Lemma. For any position X, we have Pl(X) ∼=P i1 (∆i1 (X)) (recalling Definition 3.2.8). In particular, X is tight if and only if εX :i1 (∆i1 (X)) → X is epi.
Proof. By definition.
The adapted universal property of 1D-pullbacks relative to tight positions is then:
4.2.8. Lemma. For any commuting diagram as the solid part of
T

h
k
f

A

C

B

D

with the marked mono and 1D-pullback, and where T is a tight position, there exists a
unique map k making the diagram commute.
Proof. We construct in turn both dashed maps inlPl(T )
εT

T

f

A

k

C

h

B

D:

• P
l follows from universal property of 1D-pullbacks (Proposition 4.2.5), since Pl(T ) ∼=i1 (∆i1 (T )) (Lemma 4.2.7),• k then follows again by Lemma 4.2.7 (which ensures that εT is epi) and lifting inthe (Epi, Mono) factorisation system.
The construction of k however does not a priori ensure that f ◦ k = h, but f ◦ k ◦ εT =f ◦ l = h ◦ εT which entails the result by tightness.

542

CLOVIS EBERHART, TOM HIRSCHOWITZThis yields an analogue of the pullback lemma:
4.2.9. Lemma. In any commuting diagram
A

B

C

D

E

F

with the marked mono, pullback and 1D-pullback, the outer rectangle has the universal
property of pullbacks w.r.t. tight positions.
Proof. Similar to the proof of the pullback lemma, using Lemma 4.2.8.
4.3. A necessary and sufficient fibredness criterion. In this section, we prove
our first main result, namely that, under the hypothesis that seeds admit cartesian restrictions (which we investigate independently in the next section), D(S) is fibred. The
idea for this is to prove that moves admit cartesian liftings, and that cartesian liftingscompose vertically, so that one can compute the cartesian lifting of a play inductively foreach of its moves. In fact, showing that moves admit cartesian liftings reduces to proving(Lemma 4.3.11) that pushing a play P along a horizontal morphism yields a play P 0 , suchthat the morphism P → P 0 is cartesian. This is in fact not completely accurate, as it
does not directly make sense to push a play along a horizontal morphism. The point isthat a position Z can be invariant in P , namely when there is a morphism id •Z → P . For
any such invariant position Z and horizontal morphism h : Z → Z 0 , one in fact pushes
along id •h : id •Z → id •Z 0 .
In summary, we have a proof in four main steps:• we prove that cartesian cells are stable under composition;• we define invariant positions and prove that pushing plays along horizontal morphisms in the above sense yields cartesian morphisms;• we deduce that moves admit cartesian restrictions if seeds do;• finally, we prove by induction that the latter extends to plays.
Let us start with some notation:su
X will be denoted by Y −→4.3.1. Notation. The cospan underlying any play u : YtusU ←− X (using capitalisation for the middle object). We will often denote cospans Y →−tU←− X simply by hU i, leaving the context provide the missing information. Furthermore,b H (they are given by taking pushouts levelwise) and when we
pushouts exist in Cospan(C)b H . We
write pushouts of cospans, the notation means that they are cospans in Cospan(C)will often take pushouts of cospans in D0 (C)H , but such pushouts are not necessarily
pushouts in D0 (C)H (the square itself does not necessarily lie in D0 (C)H ).

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

543

Vertical composition of cartesian cells We first consider stability of cartesian cells
under vertical composition. In order to prove this, by Lemma 4.1.2, we need in particular
to show that the middle morphism of a vertical composite of cartesian cells is in JS⊥ . The
following result will prove useful for this.
4.3.2. Lemma. For any commuting diagram of 1D-injective maps of the form
U

sU

fU

U0

W

sV

V

f
sU 0

W0

fV
sV 0

V0

b such thatwith the marked 1D-pullbacks in C,• sU and sV are jointly surjective and both monic,• sU 0 and sV 0 are jointly surjective and both monic,• fU and fV are in JS⊥ ,we have that f ∈ JS⊥ .
C in JS and commuting square

Proof. Consider any morphism T
T

W

C

W 0.

We want to show that there is a unique diagonal filler C → W . ByPProposition 4.2.6,
uniqueness follows from 1D-injectivity of f and the fact that C ∼= i1 (∆i1 (C)), so weonly need to show existence. Furthermore, by joint surjectivity and because C is a representable, C → W 0 factors either through U 0 or through V 0 (possibly both).
Both cases being symmetric, we only treat one. If C → W 0 factors through U 0 , thenwe get a commuting diagram as the solid part of
T

W
k

U
l

C

U0
W 0,

hence a map k as indicated by Lemma 4.2.8, using monicity of sU . By hypothesis, U → U 0
is in JS⊥ , so there is a unique map l : C → U making both triangles commute. By
composing it with U → W , we get the desired diagonal filler.

544

CLOVIS EBERHART, TOM HIRSCHOWITZ

We may now state the first crucial lemma of this section, which states that verticalbcomposition in D0 (C) preserves CospanJS (C)-cartesianness.
b are both in
4.3.3. Lemma. If any two vertically composable double cells of Cospan(C)b and are cartesian in the latter, then their vertical composite is
D0 (C) and CospanJS (C),again cartesian (in the latter).
Proof. Consider any two composable vertical morphisms hU i = (Y → U ← X) andhV i = (Z → V ← Y ), and similarly hU 0 i and hV 0 i, together with composable cartesian
double cells α : hU i → hU 0 i and β : hV i → hV 0 i. To show that the composite is cartesian,it is enough by Lemma 4.1.2 to show that it has the shape of the front face of (7), i.e.,that its top square is a pullback and that U • V → U 0 • V 0 is right-orthogonal to JS .
Because hU i → hU 0 i is cartesian, by Lemma 4.1.2, the left face of
Y

V
U •V

U
Y0

V0
U0

U 0 • V 0,

is a pullback, so by two applications of Corollary 3.2.7 and Corollary A.2.2 respectively, its
front face is a 1D-pullback and its right one is a pullback. By Lemma 4.3.2, the obtained
map U • V → U 0 • V 0 is thus in JS⊥ . Since hV i → hV 0 i is cartesian, by Lemma 4.1.2,
the left-hand square below is a pullback, hence so is the right-hand one by the pullback
lemma:
Z

Z0

Z

Z0

V

V0

U •V

U 0 • V 0,

which concludes the proof.
Invariant positions We now turn to defining invariant positions, and proving thatpushing a play along a morphism of invariant positions yields a cartesian morphism ofplays.
4.3.4. Definition. An invariant position of a play P is a morphism id •Z → P in D(S)H .
Consider the full embedding
db
id • : C|≤1 ,→ Cospan(C)H•
X 7→ id X
of positions into general cospans given by vertical identities.

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

545

4.3.5. Proposition. The full embedding id • has a right adjoint given by (any choice of )b in the sense that the final invariant position of a cospan Y → U ← X
pullbacks in C,(the final object among invariant positions of the cospan) is given by the pullback
Z

Y

X

U.

Proof. An invariant position is equivalently a cone to the given play, so we conclude byuniversal property of pullback.
The idea behind the definition of invariant positions id •Z → hU i is that they are partsof the initial position X that are left untouched by all moves of the play. The final
invariant position is the biggest such subposition of X.
4.3.6. Example. By their characterisation as a pullback of monic maps, final invariant
positions are always subpositions of both the initial and final positions of the play.
st
In the case of the π-calculus, the final invariant position of all seeds Y →− M ←− X isX(?) · ?. Indeed, in any seed, for all channels in the initial position, there is a (necessarily
unique, by monicity) corresponding channel in the final position. There may be otherchannels in the final position (e.g., in the case of ιn,a ), but they are not part of the final
invariant position (and thus of no invariant position). Finally, in all seeds, the images ofs and t on players are disjoint, which completes the proof of this characterisation.
Let us show the following two results about invariant positions, which prepare for our
second key intermediate result, Lemma 4.3.11.
b H as below left, where Z is a position, may be
4.3.7. Lemma. Any pushout in Cospan(C)factored as below right, where Z0 is the final invariant position of U :
id •Z

hU i

id •Z

id •Z0

hU i

hV i

hW i

hV i

hV 0 i

hW i .

If hV i is isomorphic to id •Z 0 for some position Z 0 , then hV 0 i is isomorphic to id •Z00 forsome position Z00 .
Proof. The last point is a consequence of colimits being pointwise in presheaf categories.
For the first, we get a map Z → Z0 such that id •Z → hU i = id •Z → id •Z0 → hU i byadjunction. We can then define hV 0 i as the pushout of hV i along id •Z → id •Z0 and obtaina unique morphism hV 0 i → hW i by its universal property: this yields a diagram as desired,
whose right-hand square is again a pushout by the pushout lemma.

546

CLOVIS EBERHART, TOM HIRSCHOWITZ

4.3.8. Lemma. Final invariant positions are stable under pushout in the following sense:
if Z is the final invariant position of the play hU i and
id •Z

id •Z 0

hU i

hU 0 iis a pushout, then Z 0 is the final invariant position of hU 0 i.
Proof. Let us first name the involved presheaves: hU i = (Y → U ← X) and hU 0 i =(Y 0 → U 0 ← X 0 ). Since Z is the final invariant position of hU i, we may apply Corollary A.2.2 to
Z

Y
Z0

Y0

X

U
X0

U 0,

to obtain that the front face is also a pullback.
We now turn to proving the second key intermediate result, Lemma 4.3.11, which, werecall, states that pushing plays along morphisms of invariant positions yields cartesian
cells. We start by showing the following two technical results.
b H , pushout squares are preserved by vertical composition.
4.3.9. Lemma. In Cospan(C)More explicitly, given two vertically composable pushouts as below left and centre, thecomposite square below right is again a pushout:
hU0 i

hU1 i

hV0 i

hV1 i

hU0 i • hV0 i

hU1 i • hV1 i

hU2 i

hU i

hV2 i

hV i

hU2 i • hV2 i

hU i • hV i .

Proof. Let us first name the involved presheaves: hUi i = (Yi → Ui ← Xi ), hVi i = (Zi →Vi ← Yi ), and similarly for hU i and hV i. If we call Λ the posetal category with objects
0, 1, and −1, and morphisms generated by 0 → 1 and 0 → −1 (the “walking span”
b through the following diagram:category), we introduce a bifunctor from Λ × Λ to CFIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

V1

V0

V2

Y1

Y0

Y2

U1

U0

U2 .

547

By computing its colimit first horizontally, then vertically, we get hU i • hV i, which byinterchange of colimits is the desired pushout.
4.3.10. Lemma. Consider any diagram
A

f

g

l

C

h

B
k

D

b where only the outer square and the bottom right triangle are known to commute,in Ci.e., kf = hg and kl = h. If A is tight and k is 1D-injective, then also the top left triangle
commutes.
Proof. Post-composing with k, we have by hypothesis that kf = hg = klg, hence
kf εA = klgεA . By 1D-injectivity of k and Proposition 4.2.6, we get f εA = lgεA . By
tightness of A and Lemma 4.2.7, we finally obtain f = lg.
We may at last state the second key intermediate result:4.3.11. Lemma. For any pushout
id •Z

id •h

id •Z 0
(10)

k

P

P0

b H where h ∈ D0 (C)h (Z, Z 0 ) and k ∈ D(S)H (id • , P ), P 0 is a play and P → P 0
in Cospan(C)Z
is cartesian and lies in D0 (C)H (hence also in D(S)H ).
Proof. The fact that P → P 0 lies in D0 (C)H follows form 1D-injectivity of h, stabilityof monos under pushout in Set, and the fact that pushouts along monos are pullbacks byadhesivity of Set. Let us show the other properties by induction on the play.
We prepare the induction by treating the case of moves. Let us thus assume thatP = hM i is a move. We know that any move hM i is a pushout of some seed hM0 i. By
Lemma 4.3.7, we may assume that it is the pushout of hM0 i along a morphism Z0 → Z00 ,where Z0 is the final invariant position of hM0 i. Since Z0 is the final invariant position of

548

CLOVIS EBERHART, TOM HIRSCHOWITZ

hM0 i, by Lemma 4.3.8, we know that Z00 is the final invariant position of hM i. Therefore,
id •Z → hM i factors as id •Z → id •Z00 → hM i. Now, we define Z 00 as the pushout below andid •Z 00 → hP 0 i by its universal property:
id •Z

id •Z 0id •Z00

id •Z 00hP 0 i .

hM iNow, two applications of the pushout lemma give that
id •Z0id •Z 00

hM0 i

hP 0 iis a pushout, and since Z0 → Z 00 is 1D-injective (as the composite of two 1D-injectivemaps), hP 0 i is a move, which we also call hM 0 i.
Let us now show that the obtained morphism hM i → hM 0 i is cartesian, i.e., that it
has the shape of the front face of (7), by Lemma 4.1.2. By the pushout lemma, the top
square
Y

Y0

M

M0

is a pushout along Y → M , which is monic, so it is a pullback by adhesivity (Lemma A.1.4).
Moreover, to show that M → M 0 is right-orthogonal to JS , we take any T → C in JS andcommuting square as the solid part of
T

M

C

M 0.

Since M → M 0 is an isomorphism in dimensions > 1 and C is a representable of dimension> 1, C → M 0 can be factored uniquely as shown above. Now, since T is tight and M → M 0
is 1D-injective, by Lemma 4.3.10, we get that the top-left triangle commutes as well, hence
C → M is the desired diagonal filler.

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

549

Now that we have shown that moves are stable under pushouts of the desired form
and that the resulting morphism is cartesian, we proceed to show that it is also the casefor arbitrary plays by induction on hP i.
X contains zero moves, then the result is obvious. If Y → P
XIf Y → P
contains at least one move, we decompose it as hM i • hU i, for some move T → M
X
T containing fewer moves than P .
and play Y → U
Because the square below
Z

T

U

M

P

is a pushout along a monomorphism, hence a pullback, we obtain a unique dashed map asshown such that the diagram commutes. Thus, id •Z → P factors as a vertical composite
of two cells id •Z → U and id •Z → M . By Lemma 4.3.9, the desired pushout (10) is thevertical composite of the following two pushouts:
id •Z

id •Z 0id •Z

id •Z 0

hU i

hU 0 ihM i

hM 0 i .

Since hU 0 i and hM 0 i are plays by induction hypothesis, so is hP 0 i. Moreover, by induction
hypothesis again, hU i → hU 0 i and hM i → hM 0 i are cartesian, and therefore, so is hP i →hP 0 i, by Lemma 4.3.3.
4.3.12. Remark. The morphism P → P 0 thus computed is not opcartesian in general.
To see this, consider the signature Sπ of the π-calculus, and push the play P = hom,c,d ialong [m] → [n] a | c [m] to get P 0 . Now, P clearly has a morphism to σn,a,m,c,d (given bySπ (ε)), but P 0 does not, because its final position contains a player of type [n], while thefinal position of σn,a,m,c,d only contains two players of type [n + 1] and [m] respectively.
From seeds to moves The preceding result now allows us to prove our third key
intermediate result, namely:
4.3.13. Lemma. If seeds admit cartesian restrictions in D(S), then so do moves.

550

CLOVIS EBERHART, TOM HIRSCHOWITZ

Proof. Consider any move as in (5) and horizontal morphism h : X 0 → X. We start byforming the cube
Z00
Z0
X00

X0
(11)

h0

Z0

h

Z
X0

X,

where the dashed arrow is obtained by universal property of pullback. By the pullback
lemma, the left-hand face is again a pullback. Now, by Lemma 4.3.7, we may assume that
Z0 → X0 is monic, so by adhesivity the top face of (11) is again a pushout.
By Lemma 4.3.11, the morphism hµi → hM i is cartesian. By hypothesis, we obtaina cartesian lifting of hµi along h0 , say Y00 → U00 ← X00 . We get a morphism Z00 → U00 bycomposing Z00 → X00 and X00 → U00 , and then a morphism Z00 → Y00 by universal propertyof pullback, remembering that, by Lemma 4.1.2, the square
Y00

Y0

U00

µ

is a pullback. We may thus push the obtained lifting along id •Z00 → id •Z 0 to obtain aplay hU 0 i and a cartesian morphism hU00 i → hU 0 i by Lemma 4.3.11. It also induces, byb H as inuniversal property of pushout, a morphism hU 0 i → hM i in Cospan(C)id •Z00

id •Z 0hU00 iid •Z0hU 0 i
id •Z

hµi

hM i .

We want to show that hU 0 i is the cartesian restriction of hM i along h. In order to dothat, we first need to show that hU 0 i → hM i is a morphism of plays, i.e., that it belongsto D(S)H .

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

551

Now consider the following cubes:
X00

U00
X0

X0

Z00

Z0

U0

Y00

µ

Z0

X

Y0
Z

M

Y0

Y,

where, in the left-hand case, both pushouts are obtained by the pushout lemma. In theleft-hand cube, by pointwise adhesivity and Corollary 3.2.7, we obtain that U 0 → M is 1Dinjective and that the front face is a 1D-pullback. In the right-hand cube, Corollary 3.2.7
entails that Y 0 → Y is 1D-injective. This entails in particular that hU 0 i → hM i indeed isa morphism of plays.
It remains to show that hU 0 i → hM i is cartesian, for which by Lemma 4.1.2 it issufficient to show that it has the shape of the front face of (7).
First, the upper square is a pullback by pointwise application of Lemma A.2.1 in
Y00

U00
Y0

Y0

U0
µ

Y

M.

So the only point left to show is that U 0 → M lies in JS⊥ . To show this, we consider
C in JS and commuting square
any morphism T
T

U0

C

M

and show that there is a unique diagonal filler. Uniqueness follows from the fact thatU 0 → M is 1D-injective and that C ∼= Σi1 (∆i1 (C)), so we only need to show that there
exists such a diagonal filler.
First, since µ
M is an isomorphism in dimensions > 1 and C is a representable ofdimension > 1, we know that C → M factors through µ
M in a unique way. We now
want to show that T → U 0 factors through U00
U 0 in such a way that

552

CLOVIS EBERHART, TOM HIRSCHOWITZ

T

U00

U0

C

µ

M

commutes.
Stepping back a little, let us recall a cube considered above, as below left
T
X00

U00
X0

U00

C

µ,

U0

C
X0

T

µ
X

M

where we added the map T → X0 given by S(C → µ). By Lemma 4.2.9 on the front face,
using tightness of T , we obtain a unique arrow T → X 0 , which further gives by universal
property of pullback a unique dashed arrow T → X00 making everything commute. In
particular, we obtain a square as the solid part above right by composing the arrow
T → X00 we just obtained with X00
U00 .
But now U00µ is in JS⊥ , so there is a unique dashed diagonal map as shown making
both triangles commute, which gives rise to a map C → U 0 by composition, hence theresult.
From moves to plays Finally, we state and prove our first fibredness result:4.3.14. Theorem. If seeds admit cartesian restrictions in D(S), then D(S) is fibred.
Proof. Let us consider any play Y → P
X and show that its cartesian restriction
0balong X → X in CospanJS (C) lies in D(S), which is enough by Lemma 4.1.4. We proceed
by induction on Y → P
X. If it is the composite of 0 moves, then X
P and
Y → P are isomorphisms and the result is obvious. If it is the composite of n + 1
moves, then it can be decomposed as hM i • hU i for some move T → M
X and play
Y →U
T . By Lemma 4.3.13, we know that hM i admits a cartesian restriction along
0
X → X, say T 0 → V 0
X 0 . Furthermore, by induction hypothesis, hU i admits a0cartesian restriction along T → T , say Y 0 → U 0
T 0 . By Lemma 4.3.3, the verticalcomposition of hV 0 i → hM i and hU 0 i → hU i is cartesian, hence the result.

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

553

4.4. Cartesian lifting of seeds. In the previous section, we have shown that D(S)is fibred as soon as seeds admit cartesian restrictions in D(S). In this section, we exhibit
sufficient conditions for the latter to be the case. I.e., possibly under additional hypotheses, in the setting of (7), if hU i is a seed, then its restriction hU 0 i is a play and (h, h0 , h00 )is a morphism of plays.
The basic idea of our proof is that there are two possible cases: either X 0 “contains
all of” X, or it does not. In more precise terms, either h is a retraction, or it is not. In
both cases, for the given seed µ, we• first construct a candidate restriction hU 0 i,
• prove that it is indeed a play and that the morphism hU 0 i → hµi is a morphism ofplays,• and then finally show that it is a cartesian lifting of hµi along h by showing that it
has the shape of the front face of (7).
The main difference between the two cases is that, in the first one, X can be thought ofas a sub-position of X 0 , so we basically extend µ so that it is played from all of X 0 . By
contrast, in the second case, X 0 does not contain X, so it is impossible to play µ from it,and the restriction consists of all the “pieces” of µ that can be played from X 0 .
Restrictions along retractions Let us make a first hypothesis that will be useful forthe case where h is a retraction, but also for the other case. It is equivalent to asking thatmoves never erase channels, in the sense that, if a channel occurs in the initial position ofa move, then it also does in its final position. The hypothesis is the following:
X, the4.4.1. Definition. A signature S is persistent when for any seed Y → M
morphism Z → X from its final invariant position is an isomorphism in dimension 0.
4.4.2. Example. The signature Sπ of the π-calculus is persistent. Indeed, by tightnessof initial positions, it suffices to show that, for all solid parts of the diagram below, thedashed part exists:
[m]

Y

∗

M

[n]

X,

where Y → M
X is a seed. For example, let us take the seed Sπ (σn,a,m,c,d ): if thesisichannel ∗ → X factors as ∗ −→[n] → X, then the dashed part is ∗ −→[n + 1] → Y ;sisiotherwise, ∗ → X factors as ∗ −→ [m] → X, and the dashed part is ∗ −→ [m] → Y .
A non-persistent signature is any signature that has a move in which a channel iserased, e.g., a move whose graphical depiction is:554

CLOVIS EBERHART, TOM HIRSCHOWITZ.
4.4.3. Lemma. The seeds of any persistent signature admit cartesian liftings along retractions.
Proof. Consider any such signature S. By Lemma 4.1.3, it is enough to prove that theb lies in D(S). Consider any seed Y → M
cartesian lifting in CospanJS (C)X and 1D0
injective retraction h : X → X. Since h is a retraction, there is a section h0 : X → X 0
X and definesuch that hh0 = id X . We call Z the final invariant position of Y → M
0Z as the pullback
Z
r0

u

Z0

X
h0

r

Z

u0

u

X0

X

h

and r0 : Z → Z 0 by its universal property. As a section, r0 is mono, so in particular 1Dinjective. We know that u is an isomorphism in dimension 0 by persistence, and so is u0 asa pullback of u, which entails by Lemma A.1.1 in the opposite category that the left-handsquare above is a pushout in dimension 0. But in dimensions > 0, h is an isomorphism,
hence so are h0 and r0 (as a pullback of h0 ), so by the same argument, the left-hand squareis also a pushout in dimensions > 0. It is thus a pushout in all dimensions, hence ab since colimits are computed pointwise in presheaf categories.
pushout in C,
We define the cospan hM 0 i as the pushout
id •Z

id •r0id •Z 0
id •r

β

hM i

α0

id •Z

hM 0 i

(12)

α

hM i
and α : hM 0 i → hM i by its universal property. Now, if we define (l, k, h̃) = α, (l0 , k 0 , h̃0 ) =α0 , and (l00 , k 00 , h00 ) = β, we can assume without loss of generality that h00 = u0 and that

555

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICSh̃0 = h0 , since both
Z

r0

id •Z

h0

id •r0

and

u0

u

X

Z0

X0

id •Z 0
β

hM i

α0

hM 0 iare pushouts. Similarly, by the pushout lemma, we get that
Z0

r

u0

X0

id •Z 0

Z
and

u

h

id •Z

β

hM 0 i

X

id •r

α

hM i

are pushouts, so we can assume that h̃ = h. By Lemma 4.3.11 in the left-hand squareof (12), we get that hM 0 i is a play. Now, by Lemma 4.3.11 in the right-hand square, we
get that α is cartesian, so hM 0 i is a lifting of hM i along h.
4.4.4. Remark. The lemma above shows that, if a signature is persistent, then it admits
cartesian liftings along retractions. The converse actually holds. Indeed, consider any
signature S that is not persistent. This means that there is some move m0 in the basecategory C whose seed hM i is such that the morphism from the final invariant position
Z to X is not an isomorphism in dimension 0. Since that morphism is a monomorphism
as the pullback of Y → M , which is mono, it cannot be an epimorphism in dimension 0(because all epi monos are isos in Set). This implies that there is a channel c : ∗ → M forsome object ∗ of dimension 0 that is in the image of Xts

M , but not in that of Y →
− M.
[c,X]

Let us consider the move hM i and try to build its cartesian lifting along ∗+X −−→ X.
If such a cartesian lifting hU 0 i → hM i exists, because it is cartesian, id hM i must factor
through it in a unique way, as in
Y
M

Y0

Y

X

U0

M

∗+X

X.

Therefore, U 0 → M must be a retraction, but it is also 1D-injective so it is bijective indimensions > 0. In particular, U 0 (m) is isomorphic to M (m) for all moves m. Now,
since U 0 must be isomorphic to m0 in dimensions > 0, it is necessarily the composite
of a single m0 move. But the only way to play m0 from ∗ + X is to be isomorphic to556

CLOVIS EBERHART, TOM HIRSCHOWITZ
∗+s

∗+t

∗ + Y −−→ ∗ + M ←−− ∗ + X. So we want to find a pair of morphisms as the dashedarrows above when the front face has the form:∗+Y[g,g 0 ]

∗+s

∗+M

s
[f,f 0 ]

∗+t

∗+X

Y

M
t

[c,X]

X.

In particular, it must be that tc = f = sg. But we chose c such that tc is not in the imageof s, so this is impossible, hence hM i has no cartesian lifting along [c, X].
Restrictions along non-retractions When h is not a retraction, we need some more
hypotheses to construct restrictions (and ensure that they are indeed cartesian). We willneed three hypotheses. The first one, monolithicity, restricts the possible ways to modelinteractions between players. It is not necessary, but makes proofs much simpler. The
second one, fragmentation, forces all interactions to have restrictions to single players.
This condition is necessary for seeds to admit cartesian restrictions (otherwise, the seedcorresponding to an interaction could be restricted along one of the players). The lastcondition, separation, states that, if a player is created by an interaction, then it is theavatar of a single one of the players involved in that interaction. This is related to thenotion of view: to define the view of the created player, we take the view of the player
it was created by. This condition is also necessary, otherwise a player created during aninteraction could end up being created multiple times in a restriction, which would break
1D-injectivity.
First, we want to limit the possible interactions between moves:
4.4.5. Definition. A signature is monolithic when for all morphisms of plays α : (Y →X) → (Y 0 → M 0
X 0 ) between any two seeds, if X is not a representable, thenM
M = M 0.
A signature is monolithic roughly when restricting a move Y 0 → M 0
X 0 describing0
an interaction to a strict sub-position X of X cannot yield an interaction. In other words,
interactions cannot be broken down into smaller interactions (e.g., an interaction between
three players cannot be broken down into an interaction between only two of them).
Though it is possible to relax this limitation, this would not only induce an explosion of
the number of cases to analyse, but we would also need to put another kind of restriction,
which would more difficult to check, which is why we decided to stick to a simple case.
Moreover, such “partial interactions” do not appear to bring much expressiveness to ourframework.
4.4.6. Remark. Since the base category is direct, monolithicity ensures that, if there
is a morphism α between seeds as above, and X is not a representable, then α =(id Y , id M , id X ).

557

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

4.4.7. Example. The signature Sπ of the π-calculus is monolithic. Indeed, since all seeds
except σn,a,m,c,d have representables as their initial positions, if α : (Y → MX) →X 0 ) is a morphism of plays between seeds and X is not a representable,(Y 0 → M 0X) = Sπ (σn,a,m,c,d ), so in particular M = yσn,a,m,c,d . We conclude bythen (Y → M
noticing that the only morphism in C with domain σn,a,m,c,d is the identity thereon, andthus M 0 = M .
To give an example of non-monolithic signature, let us consider a π-calculus whose
output primitive broadcasts the name of a channel on another channel, i.e., more than
one player may receive that name. This could be modelled by the same base category asthat of our π-calculus, except that the synchronisation moves would be σ[(ni ,ai )]i∈k ,m,c,d ,with a list of receivers and a single sender. We give a graphical depiction of the initial andfinal positions of σ[(1,1),(2,1)],3,1,2 (a player of arity 3 broadcasting the name of its second
channel on its first one, received by two players of respective arities 1 and 2, both on theirfirst channels) below:.
There are two natural choices for morphisms in the base category C: either include σL,m,c,dinto σL0 ,m,c,d when L is a sublist of L0 up to permutation, or not (and only include ιn,aand om,c,d ’s in σL,m,c,d ). The first choice leads to a non-monolithic signature, e.g., because
there is a morphism of plays S(σ[(n,a)],m,c,d ) → S(σ[(n,a),(n0 ,a0 )],m,c,d ) and the initial positionof the former is not a representable (it contains two players). The second choice actuallyleads to a monolithic signature, so it is unclear what expressive power non-monolithicity
gives in concrete examples.
A second hypothesis that we make says that there should exist a “biggest part” of any
move from the point of view of any player involved in it. Basically, we want to ensure that
X has restrictions along all morphisms of positions h : X 0 → X, andany seed Y → µ
we prove this property by pasting together the “biggest part” of what each player in X 0
sees of µ when restricted along h. We here give a notion that entails the desired property,
and basically amounts to asking that seeds admit cartesian restrictions along morphismsof the form yd → X with respect to other seeds (as opposed to arbitrary plays):s

4.4.8. Definition. A signature is fragmented if and only if for all seeds Y →
− M
sM,x

and players x : d → X, there exists a seed YM,x −−→ M|x
fM,x : M|x → M in C such that:

tM,x

t

X

d and a morphism(a) the top square of S(fM,x ) is a pullback, and(b) for any seed Y 00 → M 00

X 00 and commuting diagram as the solid part below, there

558

CLOVIS EBERHART, TOM HIRSCHOWITZ

is a map M 00 → M|x making the diagram commute.
M 00
X 00

M|x f
d

M,x

(13)

M
X

4.4.9. Remark. Since fM,x is 1D-injective and M 00 is a representable of dimension > 1,
the morphism M 00 → M|x in the hypothesis above is necessarily unique.
4.4.10. Example. The signature Sπ of the π-calculus is fragmented. Indeed, if theintimal position X is a representable, then taking M|x = M defines the desired restriction,
so the only case left is that of σn,a,m,c,d . There are two morphisms d → X: l : [n] → X
and r : [m] → X, and ιn,a and om,c,d define the desired restrictions.
There are typically two ways to get a non-fragmented signature. There may be no
candidates M|x : this happens for example in the base category for the π-calculus without
moves of the form ιn,a and om,c,d . The other case is when M|x does not verify (b). For
this case, consider a π-calculus in which a process can broadcast a channel name on allof its other channels. The initial and final positions of such a move could be depicted as
below (for a ternary player broadcasting and a unary and a binary players receiving):.
There are two natural ways to model this on the side of the sender: either by having a
move that simultaneously models the broadcasting to all channels, or by having one on,a,b
move for each receiver. In the first case, the signature is fragmented: the synchronisation
restricts to the sender as the single broadcasting move. In the second case, the signature
is not fragmented: all on,a,b moves are candidates for M|x , but none of them verifies (b)(simply take M 00 = on,a0 ,b for a0 6= a).
4.4.11. Lemma. If the signature S is persistent, monolithic, and fragmented, then eachmorphism S(fM,x ) is a cartesian lifting of hM i along x in D(S).
This will rely on:
4.4.12. Corollary. For any seeds Y → M
diagram as the solid part of

X and S → C

T

U

X

C

V

M

T , any commuting

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

559

with the marked 1D-pullback, such that at least one of U → X and U → V is monic, may
be completed as shown.
Proof. Because M is a seed, the bottom square of S(C → M ) yields a morphism T → X
making the diagram commute. We conclude by Lemma 4.2.8.
Proof of Lemma 4.4.11. By Lemma 4.1.2, it is enough to prove that the top squareof S(fM,x ) is a pullback and that fM,x in JS⊥ . The first point holds by (a). To prove thesecond one, consider any morphism T
C in JS and commuting square
T

M|x
fM,x

C

M.

We need to show that there is a unique diagonal filler C → M|x . By Corollary 4.4.12, we
obtain a unique morphism T → d making the diagram below left commute:
T

d

X

C

M|x

M

C
T

M|x

M

d

X,

which may be arranged as on the right to have the shape of (13). We thus concludeby (b).
Lemma 4.4.11 exhibits cartesian liftings along players d → X. Let us now consider
more general cases, assuming a third property saying that each player involved in a synchronisation M (i.e., a seed whose initial position contains several players) is related
to at most one of the “biggest parts” of M , in the sense of our above explanation offragmentedness.
4.4.13. Definition. A signature S is separated if it is fragmented and, for all movesµ ∈ ob(C|≥2 ) with seed S(µ) = (Y → µX), players d ∈ ob(C|1 ), x1 : d1 → X andx2 : d2 → X, and y1 : d → µ|x1 and y2 : d → µ|x2 making
d

y1

y2

µ|x2

µ|x1
fµ,x1

fµ,x2

µ

commute, we have x1 = x2 (and hence fµ,x1 = fµ,x2 ).

560

CLOVIS EBERHART, TOM HIRSCHOWITZ

4.4.14. Remark. Separation really only says something in the case where the diagonalx : d → µ does not factor through X. Indeed, if it does, then by the properties of 1Dpullbacks, x also factors through x1 and x2 , hence by directedness of C is in fact equal tox1 and x2 .
4.4.15. Remark. Separation is related to the notion of view in game semantics (andindeed, in many of the cases we are interested in, separation is derived from what is called
the axiom of views in [18]). It basically states that any player that is created in a move
M is created by at most one player.
4.4.16. Example. The signature Sπ of the π-calculus is separated. Indeed, if the initial position X of µ is a representable, then there is only one morphism x : d → X, so
necessarily x1 = x2 . Therefore, µ|x1 = µ|x2 , and for any diagram
y1

d

fµ,xi

µ|xi

µ,

y2

we conclude by 1D-injectivity of fµ,xi . The only non-trivial case is thus that of σn,a,m,c,d .
So let us take xi : di → X for i ∈ {1, 2}, with x1 6= x2 , we can assume without loss ofgenerality that x1 picks the player of arity n and x2 that of arity m. But then σn,a,m,c,d |x1
is ιn,a and σn,a,m,c,d |x2 is om,c,d , and there is no commuting diagram of the formdy1

σn,a,m,c,d |x1
fσn,a,m,c,d ,x1y2

σn,a,m,c,d |x2

fσn,a,m,c,d ,x2

σn,a,m,c,d ,hence the result.
To get an example of non-separated signature, imagine a calculus in which two processes who know of exactly the same channels may “fuse” into a new process, according
to a rule such as P, Q → P + Q. A natural way to model such a move is to have a movef whose graphical depiction is:
y

f
x1

x2

,

and two sub-moves fl and fr , respectively corresponding to its restrictions to x1 and x2 .
Since the move is completely symmetric in P and Q, y should naturally be either in both
restrictions or in none. Intuitively, this new player should “remember” everything x1 andx2 knew, which means that its view, in game semantical terms, should contain both thoseFIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

561

of x1 and x2 . In the framework of fibred pseudo double categories, this translates to y
being both in fl and fr , which makes the signature non-separated.
We have now introduced the three hypotheses we will need to build the restriction ofa seed along a morphism h that is not a retraction. In this case, the restriction of a seedalong h has a particular form that we call a quasi-move, which basically consists of several
moves played “in parallel”, i.e., independently from one another.
4.4.17. Definition. A quasi-move is any cospan that is isomorphic to a pushout of the
form
P

•
i∈n id Zi

id •h

P

i∈n hMi i

id •Z

hU i ,

in D0 (C)H , where the hMi i’s are seeds.
4.4.18. Example. In D(Sπ ), the play depicted on the left below is a quasi-move, while
the play depicted on the right is not.

π

π

ν

ν

Indeed, the first one can be defined as the pushout
id •∗ + id •∗id •∗π1 + ν1

hU i .

However, the second play cannot be expressed as a similar pushout. Indeed, if it were aquasi-move, it should at least contain π1 , whose final invariant position is non-empty, so
the final invariant position of the whole quasi-move would also be non-empty, but thisplay has an empty final invariant position.
4.4.19. Lemma. Every quasi-move is a play.

562

CLOVIS EBERHART, TOM HIRSCHOWITZtsi
Proof. Let→
Mi i Xi ) for all i ∈ n. By Lemma 4.3.11, it is enough to
P hMi i = (Yi −show that i hMi i is a play. We proceed by induction on n. If n = 0, the result is trivial.
Otherwise, we haveXX
X
hMi i).
hMi i ∼
id •Xi ) • (id •Y1 += (hM1 i +

i

i>1

i>1

By induction hypothesis, both components are plays, so by Lemma 4.3.9, the composite
also is.
s

We can now exhibit the construction of the restriction of a seed Y →− M
0a morphism h : X → X that is not a retraction.

t

X along

4.4.20. Theorem. The seeds of any persistent, monolithic, and separated signature S
admit cartesian liftings in D(S).
Proof. By Lemma 4.4.3, it is enough to deal with the case where h is not a retraction.
We first build the candidate restriction. Let Z be the final invariant position of hM i.
By fragmentedness, we know that for each player (d, x) ∈ pl(X), there exists a seed
sM,x

tM,x

YM,x −−→ M|xd and a morphism (lM,x , fM,x , x) : M|x → hM i satisfying (a)and (b) of Definition 4.4.8. Letting Z 0 = X 0 ×X Z, for any player (d, x) ∈ pl(X 0 ) we may
thus construct by universal property of pullback a map rM,x as in
ZM,hx

YM,hx

rM,x

d

M|hx

x

Z0

(14)

r

Z

X0

h

Y
X

M,

where ZM,hx → Z comes from the universal property of Z. We first want to show thatP(d,x)∈pl(X 0 ) ZM,hx[rM,x ](d,x)∈pl(X 0 )

Z0
(15)

P

(d,x)∈pl(X 0 ) d[x](d,x)∈pl(X 0 )X0

is a pushout and that all involved maps are 1D-injective. First, it is a pullback: byLemma A.1.2, it suffices to show ZM,hx = d ×X 0 Z 0 for each x, which follows by threeconsecutive applications of the pullback lemma in (14). Because it is a pullback of two
1D-injective maps, all of its maps are in fact 1D-injective. But then, recalling that the
pullback of any isomorphism is in fact a pushout square, we have:P• in dimension 1, (d,x)∈pl(X 0 ) d → X 0 is an isomorphism andFIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

563• in dimension 0, Z 0 → X 0 is an isomorphism by persistence,
so the square is a pushout in all dimensions, hence a proper pushout.
We now define our candidate restriction hU 0 i as the quasi-move below, and hU 0 i → hM i
by its universal property:
id •[rM,x ](d,x)∈pl(X 0 )•0(d,x)∈pl(X 0 ) id ZM,hx

PP(d,x)∈pl(X 0 )M|hx(l0 ,k0 ,h0 )id •Z 0

id •r

id •Z

hU 0 i(l,k,h̃)hM i .

[S(fM,hx )](d,x)∈pl(X 0 )First, hU 0 i is a quasi-move, and therefore a play by Lemma 4.4.19. Moreover, because (15)is a pushout, we can assume without loss of generality that it is the bottom square of the
pushout defining hU 0 i. Thus, h̃ = h.
Furthermore, the morphism [S(fM,hx )](d,x)∈pl(X 0 ) is in D(S)H . Indeed, that its bottom
square is a 1D-pullback follows from Lemma A.1.2; 1D-injectivity of its bottom component
is 1D-injectivity of h◦[x](d,x)∈pl(X 0 ) ; 1D-injectivity of its top component follows from that ofits middle component.
So let us consider an object c of dimension > 0 and two morphismsP
f1 , f2 : c → (d,x)∈pl(X 0 ) M|hx that are equal when composed with [fM,hx ](d,x)∈pl(X 0 ) . Sincec is a representable, f1 and f2 must factor through one of the coproduct injections, so
fi = inj(di ,xi ) ◦fi0 for some f10 : c → M|hx1 and f20 : c → M|hx2 . We thus have a commuting
diagram
c

f20

f10

M|hx1

M|hx2
fM,hx2

fM,hx1M.

We want to exhibit a square as above but with an object d of dimension 1 instead of c. If
c is of dimension 1, we take d = c. Otherwise , by monolithicity, we know that S(c) musthave a representable as its initial position, and since all initial positions must be tight,
it must be a representable of dimension 1. We thus get a morphism x : d → c for some
object d of dimension 1. We can now compose the diagram above with that morphism,
which gives us a diagram on which we may apply the property of separation, which gives

564

CLOVIS EBERHART, TOM HIRSCHOWITZ

us that hx1 = hx2 . Now,
fM,hx1 f10 = [fM,hx ](d,x)∈pl(X 0 ) inj(d1 ,x1 ) f10= [fM,hx ](d,x)∈pl(X 0 ) f1
= [fM,hx ](d,x)∈pl(X 0 ) f2
= [fM,hx ](d,x)∈pl(X 0 ) inj(d2 ,x2 ) f20= fM,hx2 f20= fM,hx1 f20 .
P
00
Therefore, since fM,hx1 is 1D-injective and c ∼=i1 (∆i1 (c)), we have that f1 = f2 by
Proposition 4.2.6, hence f1 = f2 , so [fM,x ](d,x)∈pl(X 0 ) is indeed 1D-injective.
We now want to show that the morphism (l, k, h) : hU 0 i → hM i is in D(S)H , i.e.,that all its components are 1D-injective. We know that [rM,x ](d,x)∈pl(X 0 ) is bijective indimensions > 0, as the pullback of [x](d,x)∈pl(X 0 ) , which is by construction. Thus, thecomponents of the map (l0 , k 0 , h0 ) are bijective in dimensions > 0, which entails thathU 0 i → hM i is in D(S)H .
Finally, let us prove that hU 0 i is the restriction of hM i along h. To this end, let us
first prove that k is in JS⊥ : consider any T
C in JS and commuting square
T

U0

C

M.

By Corollary 4.4.12, we get a dashed map as in
T

X0

X

C

U0

M,

which makes the diagram commute. If C were equal to M , then, since C is direct,
C → M would be an identity, and so would T → X by Lemma 3.2.12, which contradicts
the hypothesis that h is not a retraction. Thus, C is different from M . Therefore, bymonolithicity, we know that TPis representable, and of dimension 1 by tightness. Hence,
T → X 0 factors as T = d0 → (d,x)∈pl(X 0 ) d → X 0 . We thus have the solid part of:
T

d0

C

M|hx0

inj(d0 ,x0 )P(d,x)∈pl(X 0 ) d

inj(d0 ,x0 ) P(d,x)∈pl(X 0 ) M|hx

h0

X0

h

X

k0

U0

k

M,

(16)

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

565

which we can reorganise as the solid part of:CT

M|hx0 f
d0

M
M,hx0

hx0

X

on which we can use fragmentedness to get a dashed map making both diagrams commute.
Since (16) commutes, it is obvious that C → U 0 obtained as the composite C → M|hx0 →U 0 is a desired diagonal filler.
Uniqueness of C → U 0 is given by Proposition 4.2.6, sinceP
k is 1D-injective, and C ∼= i1 (∆i1 (C)).
Lastly, we prove that the right-hand square below is a pullback:
Z0 +

P

Z0 +

P

(d,x)∈pl(X 0 ) YM,hx

Y0

Y
(17)

(d,x)∈pl(X 0 ) M|hx

U0

M.

By Lemma A.1.2, the outer square is a pullback because each of the squares below left
(by fragmentedness) and the square below right (by Lemma A.1.1) are:
YM,x

Y

Z0

Y

M|x

M

Z0

M.

Moreover, the left-hand square in (17) is also a pullback by Lemmas A.1.1, 4.3.11 (because
we know that the top squares of cartesian liftings are pullbacks), and A.1.2. Since Z 0 +P0(d,x)∈pl(X 0 ) M|x → U is epi, Lemma A.1.3 entails that the desired square is a pullback.
4.4.21. Corollary. For any persistent, monolithic, and separated signature S, D(S) is
fibred.
Proof. By Theorem 4.4.20 seeds admit cartesian restrictions, so the result follows by
Theorem 4.3.14.
As an easy application, we get:
4.4.22. Proposition. D(Sπ ) is fibred.
Proof. By Corollary 4.4.21, it suffices to verify that Sπ is persistent, monolithic, andseparated, which is routine.

566

CLOVIS EBERHART, TOM HIRSCHOWITZ

5. Conclusion
We have introduced a notion of signature for the sheaf-based approach to concurrent
game semantics [18, 9]. We have shown how to, from such a signature, automaticallybuild a pseudo double category of concurrent traces, which we interpret as plays in some
sort of game. Finally, we have introduced the notion of fibredness, which allows us tobuild categories of plays from our pseudo double categories, and given two criteria to provethat a pseudo double category is fibred, one necessary and sufficient, the other simpler but
only sufficient. The second criterion is still general enough to show that many interesting
calculi yield fibred pseudo double categories, as illustrated by the example of the πcalculus, which can also be adapted to recover this property for previous constructions
for CCS and HON games.
The link between the pseudo double category we construct and games is further explored in [8], where we build a signature for HON games and investigate the link between
the categories of plays we obtain and more traditional categories of plays.
Unfortunately, there are constructions that we would like to be able to do but that
do not fit in this framework. One limitation of this framework is that moves are definedas pushouts along any (1D-injective) map, but for some calculi, we would like to be able
to restrict the class of morphisms along which we are allowed to push. For example, ina π-calculus with match and mismatch operators, there would be a move εn,a,b that may
only be played when channels a and b are equal, and a move δn,a,b that may only beplayed when a and b are different. The first move is not difficult to define, we simply addmorphisms s, t : [n] → εn,a,b , quotient maps by ssi = tsi and tsa = tsb , and define its seedt0s0

− [n]a=b , where [n]a=b is the representable [n] whose channels a and→ εn,a,b ←to be [n]a=b −b have been identified, or, more formally, the coequaliser of
2·∗

sa
sb

[n]

and s0 and t0 are given by universal property of coequaliser applied to s and t respectively.
This is not perfect however, in the sense that the obtained signature is not fragmented.
The clean solution to overcome this problem is to define another move ε0n,a,b , with morphisms s, t : [n] → ε0n,a,b and ∂ : ε0n,a,b → εn,a,b satisfying the obvious equations, and definest

its seed as [n] →− ε0n,a,b ←− [n]. Finally, there would be a special kind of plays (called
closed-world plays) that do not contain any move built from ε0n,a,b .
However, defining δn,a,b is trickier. Indeed, the only restriction to be able to play thismove is that a and b should be different. So we should model it as an object δn,a,b withmaps s, t : [n] → δn,a,b , with the morphisms in C quotiented by ssi = tsi , and define itsstseed to be [n] →− δn,a,b ←− [n]. However, since we are allowed to push along any morphism,
nothing prevents us from building the move

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS[n][n]a=bδn,a,bM

2·∗[sa ,sb ]

567

∗
[n]

[n]a=b ,which is a move δn,a,b played by a player whose a and b channels are equal, exactly what
we wanted to avoid! So, in this case, we would want to be able to push this move only
along those morphisms that do not identify a and b. The only solution here is to allow
only plays in which all moves m over δn,a,b are such that m·(tsa ) 6= m·(tsb ) in closed-world
plays. This is much more difficult in the sense that we are refusing plays based on themorphisms along which we push seeds, rather than simply forbidding some moves.
Another example where we do not want to be able to push along any morphism isthat of HON games. Let us take the following position as a concrete example:
A

x

B

y C

.

It consists of two players, x on the left and y on the right. The basic idea is that there
are three kinds of moves in our calculus for HON games: Λ and @, which correspond to
Opponent and Proponent moves, and β, which corresponds to the synchronisation of bothmoves. The Λ and @ moves should correspond to interacting with the environment, whilethe β moves should correspond to internal moves. Therefore, even though y is able to play@ on its own (by interacting with the environment), it should not be able to play it in
the position drawn above, because such a move should be internal, and thus synchronisedwith a Λ move by x.
Moreover, the persistence property, which is necessary for our construction to admit
restrictions along retractions, is sometimes too restrictive. Indeed, in the variant of HON
games we define in [8], the notion of view differs from the notion of view that was given
in previous models of CCS and the π-calculus based on the same techniques [18, 9]. In
order to recover the standard notion of view, one would need to add a new move to thebase category, together with a seed that does not verify persistence.
Some possible future work on this framework would thus be to generalise it to accept
some or all of the examples above.

References[1] Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. Information and Computation, 163(2):409–470, 2000.
[2] Gérard Berry and Gérard Boudol. The chemical abstract machine. In Proc. 17th International
Symposium on Principles of Programming Languages, pages 81–94, 1990.

568

CLOVIS EBERHART, TOM HIRSCHOWITZ[3] Aldridge K. Bousfield. Constructions of factorization systems in categories. Journal of Pure andApplied Algebra, 9(2-3):287–329, 1977.
[4] Aurelio Carboni, Stephen Lack, and Robert F. C. Walters. Introduction to extensive and distributive categories. Journal of Pure and Applied Algebra, 84(2), 1993.
[5] Simon Castellan, Pierre Clairambault, and Glynn Winskel. The parallel intensionally fully abstract
games model of PCF. In LICS. IEEE, 2015.
[6] Clovis Eberhart and Tom Hirschowitz. Presheaves for Processes and Unfoldings. http://www.
lama.univ-savoie.fr/~eberhart/ProcUnfold.pdf, 2015. Online extended abstract for a talkat CALCO Early Ideas.
[7] Clovis Eberhart and Tom Hirschowitz. Justified sequences in string diagrams: a comparison
between two approaches to concurrent game semantics. Preprint, 2016.
[8] Clovis Eberhart and Tom Hirschowitz. Justified sequences in string diagrams: a comparison
between two approaches to concurrent game semantics. In Filippo Bonchi and Barbara König,
editors, Proc. 7th International Conference on Algebra and Coalgebra in Computer Science, volume 72 of LIPIcs, pages 10:1–10:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017.
[9] Clovis Eberhart, Tom Hirschowitz, and Thomas Seiller. An intensionally fully-abstract sheaf
model for π (expanded version). Logical Methods in Computer Science, 13(4), 2017.
[10] Charles Ehresmann. Catégories structurées. Annales scientifiques de l’Ecole Normale Supérieure,80(4):349–426, 1963.
[11] Charles Ehresmann. Catégories et structures. Dunod, 1965.
[12] P. J. Freyd and G. M. Kelly. Categories of continuous functors, I. Journal of Pure and Applied
Algebra, 2:169–191, 1972.
[13] Richard H. G. Garner. Polycategories. PhD thesis, University of Cambridge, 2006.
[14] Richard H. G. Garner. A homotopy-theoretic universal property of Leinster’s operad for weakω-categories. Math. Proc. Camb. Phil. Soc., 147:615–628, 2009.
[15] Marco Grandis and Robert Paré. Limits in double categories. Cahiers de Topologie et Géométrie
Différentielle Catégoriques, 40(3):162–220, 1999.
[16] Marco Grandis and Robert Paré. Adjoints for double categories.
Géométrie Différentielle Catégoriques, 45(3):193–240, 2004.

Cahiers de Topologie et[17] Marco Grandis and Robert Paré. Kan extensions in double categories (On weak double categories,
Part III). Theory and Applications of Categories, 20(8):152–185, 2008.
[18] Tom Hirschowitz. Full abstraction for fair testing in CCS (expanded version). Logical Methods in
Computer Science, 10(4), 2014.
[19] J. Martin E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: I, II, and III. Information
and Computation, 163(2):285–408, 2000.
[20] G. Maxwell Kelly. Basic concepts of enriched category theory, volume 64 of London MathematicalSociety Lecture Note Series. Cambridge University Press, 1982. Republished as: Reprints in
Theory and Applications of Categories 10 (2005).
[21] Stephen Lack and Pawel Sobociński. Adhesive categories. In Proc. 7th Foundations of Software
Science and Computational Structures, volume 2987 of LNCS, pages 273–288. Springer, 2004.
[22] Tom Leinster. Higher Operads, Higher Categories, volume 298 of London Mathematical Society
Lecture Notes. Cambridge University Press, Cambridge, 2004.

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

569[23] Saunders Mac Lane. Categories for the Working Mathematician. Number 5 in Graduate Texts in
Mathematics. Springer, 2nd edition, 1998.
[24] Paul-André Melliès. Asynchronous games 2: the true concurrency of innocence. In Proc. 15th
International Conference on Concurrency Theory, volume 3170 of LNCS, pages 448–465. Springer,
2004.
[25] Paul-André Melliès. Game semantics in string diagrams. In Proc. 27th Symposium on Logic in
Computer Science, pages 481–490. IEEE, 2012.
[26] Robin Milner. A Calculus of Communicating Systems, volume 92 of LNCS. Springer, 1980.
[27] Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I/II. Information and Computation, 100(1):1–77, 1992.
[28] Hanno Nickau. Hereditarily sequential functionals. In Proc. Logical Foundations of Computer
Science, volume 813 of LNCS, pages 253–264. Springer, 1994.
[29] Robert Paré. Yoneda theory for double categories.
25(17):436–489, 2011.

Theory and Applications of Categories,[30] Michal R. Przybylek. The other pullback lemma. ArXiv e-prints, November 2013.
[31] Silvain Rideau and Glynn Winskel. Concurrent strategies. In Proc. 26th Symposium on Logic in
Computer Science, pages 409–418. IEEE, 2011.
[32] Michael Shulman. Framed bicategories and monoidal fibrations.
Categories, 13(9):147–163, 2008.

Theory and Applications of

A. Miscellaneous properties of presheaf categories
We here collect a few basic results about pushouts, pullbacks and monos in presheaf
categories, which we will consider to be second nature in the sequel. The well-known
pullback and pushout lemmas are not recalled, though widely used throughout. Similarly,
let us merely recall that epis are stable under pullback, and that monos are stable underpushout in presheaf categories.
A.1. Monos, pullbacks, and adhesivity. Let us start with an easy result aboutpullbacks along monos:
A.1.1. Lemma. Any commuting square as below with j iso and m monic is a pullback.
A
jC
Proof. A simple diagram chase.

B
m

D

570

CLOVIS EBERHART, TOM HIRSCHOWITZ

The second result is specific to sets:
A.1.2. Lemma. Any commuting square of the form below left is a pullback if each rectangle as below right is.
P[fi ]i∈Ifi
A
Ai
A
i∈I AiP

i∈I kiP

i∈I BikikB[gi ]i∈I

k

Bi

gi

B

Proof. Straightforward.
The third result is an instance of the other pullback lemma [30].
A.1.3. Lemma. [Another pullback lemma] In any presheaf category, for any commuting
diagram as below with e epi, if the outer rectangle and the left-hand square are pullbacks,then so is the right-hand square.
A

X

e

B

C

Y

Z

Proof. An immediate consequence of [30, Theorem 1], given that, in any presheaf category, epimorphisms are stable under pullbacks and (Epi, Mono) is a factorisation system,
so all epimorphisms are strong.
Let us continue by recalling the adhesivity properties of presheaf categories [21].
A.1.4. Lemma. In any presheaf category, any pushout along a mono is also a pullback.
Explicitly, any pushout square
A

m

B

C

D

with m mono is also a pullback.
A.1.5. Lemma. [Adhesivity] In any presheaf category, for any commuting cube
I

B
A

I0

C
B0

A0

C 0,

FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

571

with the marked pullbacks, mono and pushout, all vertical faces are pullbacks if and only
if the top face is a pushout.
Proof. By [21, Example 6 and Proposition 8 (iii)].
A.2. Extensivity. Let us finish with a similar-looking statement, which has in fact
more to do with extensivity [4] of Set than with adhesivity.
A.2.1. Lemma. In Set, for any commuting cube
I

B
A

I0

C
f

B0
A0

C 0,

with the marked pushouts and pullback,• if I 0 → B 0 is injective then the front square is a pullback, and• if all arrows except perhaps f are injective, then f also is.
Proof. The following proof is due to Pawel Sobociński (private communication). In
Set, the map m : I 0 → B 0 , being injective, may be written as a coproduct injection
m : I 0 → I 0 +X 0 . But, injective maps being stable under pullback and coproduct injections
being stable under pushout, the whole cube may be written as
I
g

I0

I +X
A
h

g+k

I0 + X0A+X
f

A0 + X 0

A0

with f = h + k. This in particular shows that injectivity of h and k entails injectivity of
f . Let us now show that the front face is a pullback. Indeed, it is the pasting of bothleft-hand squares below:
A

A
h

A0

A+X

X

A+k

k

A + X0X0

h+X 0

A0 + X 0

X 0.

572

CLOVIS EBERHART, TOM HIRSCHOWITZ

All rows being coproduct injections, by extensivity all squares are pullbacks, hence so isthe face of interest by the pullback lemma.
A.2.2. Corollary. For any commuting cube as in Lemma A.2.1 in any presheaf category with the marked pushouts and pullback,• if I 0 → B 0 is monic then the front square is a pullback, and• if all arrows except perhaps f are monic, then f also is.
Proof. Monos and pullbacks are pointwise in presheaf categories.
National Institue of Informatics, Japan
Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry,
FranceEmail: clovis.eberhart@gmail.com, tom.hirschowitz@univ-smb.fr
This article may be accessed at http://www.tac.mta.ca/tac/

THEORY AND APPLICATIONS OF CATEGORIES will disseminate articles that significantly advancethe study of categorical algebra or methods, or that make significant new contributions to mathematicalscience using categorical methods. The scope of the journal includes: all areas of pure category theory,
including higher dimensional categories; applications of category theory to algebra, geometry and topology
and other areas of mathematics; applications of category theory to computer science, physics and othermathematical sciences; contributions to scientific knowledge that make use of categorical methods.
Articles appearing in the journal have been carefully and critically refereed under the responsibility ofmembers of the Editorial Board. Only papers judged to be both significant and excellent are acceptedfor publication.

Subscription information Individual subscribers receive abstracts of articles by e-mail as they
are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. Fulltext of the journal is freely available at http://www.tac.mta.ca/tac/.

Information for authors LATEX2e is required. Articles may be submitted in PDF by email
directly to a Transmitting Editor following the author instructions at
http://www.tac.mta.ca/tac/authinfo.html.
Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca
TEXnical editor. Michael Barr, McGill University: michael.barr@mcgill.ca
Assistant TEX editor. Gavin Seal, Ecole Polytechnique Fédérale de Lausanne:gavin seal@fastmail.fm

Transmitting editors.
Clemens Berger, Université de Nice-Sophia Antipolis: cberger@math.unice.fr
Julie Bergner, University of Virginia: jeb2md (at) virginia.edu
Richard Blute, Université d’ Ottawa: rblute@uottawa.ca
Gabriella Böhm, Wigner Research Centre for Physics: bohm.gabriella (at) wigner.mta.hu
Valeria de Paiva: Nuance Communications Inc: valeria.depaiva@gmail.com
Richard Garner, Macquarie University: richard.garner@mq.edu.au
Ezra Getzler, Northwestern University: getzler (at) northwestern(dot)edu
Kathryn Hess, Ecole Polytechnique Fédérale de Lausanne: kathryn.hess@epfl.ch
Dirk Hoffman, Universidade de Aveiro: dirk@ua.pt
Pieter Hofstra, Université d’ Ottawa: phofstra (at) uottawa.ca
Anders Kock, University of Aarhus: kock@math.au.dk
Joachim Kock, Universitat Autònoma de Barcelona: kock (at) mat.uab.cat
Stephen Lack, Macquarie University: steve.lack@mq.edu.au
F. William Lawvere, State University of New York at Buffalo: wlawvere@buffalo.edu
Tom Leinster, University of Edinburgh: Tom.Leinster@ed.ac.uk
Matias Menni, Conicet and Universidad Nacional de La Plata, Argentina: matias.menni@gmail.com
Ieke Moerdijk, Utrecht University: i.moerdijk@uu.nl
Susan Niefield, Union College: niefiels@union.edu
Robert Paré, Dalhousie University: pare@mathstat.dal.ca
Kate Ponto, University of Kentucky: kate.ponto (at) uky.edu
Jiri Rosicky, Masaryk University: rosicky@math.muni.cz
Giuseppe Rosolini, Università di Genova: rosolini@disi.unige.it
Alex Simpson, University of Ljubljana: Alex.Simpson@fmf.uni-lj.si
James Stasheff, University of North Carolina: jds@math.upenn.edu
Ross Street, Macquarie University: ross.street@mq.edu.au
Tim Van der Linden, Université catholique de Louvain: tim.vanderlinden@uclouvain.be
R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca