If denotes the set of -structures, for a relational signature, there is a comonad on , where
The elements of are finite nonempty sequences in
CoKleisli morphisms correspond to winning strateges for duplicator in the existential Ehrenfeucht-Fraïssé game of length , played from to , i.e the one where spoiler only plays in , duplicator only plays in , and the two substructures are only required to satisfy the same formulas from the positive existential fragment. The correspondence between strategies and coKleisli morphisms is that, given a sequence of choices by Spoiler , is the choice by Duplicator (supposed to correspond to .
There are also a description of the “proper” Ehrenfeucht-Fraïssé game in terms of this comonad, see Abramsky-Shah 2018 for more details.
Definition
Let be as above.
The underlying set of , given a -structure , is, as noted above, the set of nonempty sequences with .
The action on functions is defined in the obvious way, .
The counit is defined by
Given a relation symbol , if and only if
For each , either is a prefix of and vice versa
And .
The comultiplication is given by , i.e by taking the sequence of prefixes of the sequence.