FIBRED PSEUDO DOUBLE CATEGORIES FOR GAME SEMANTICS

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, in which 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 the horizontal 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.