module Game where
-- in which we formalise some Game Semantics in Agda

-- Core game semantics:
open import Game-Core public

-- Standard copycat strategies:
open import Game-Morphs public
open import Game-Strats public

-- Annotations on games:

-- For example, Annotation G (λ _ → String) would be a game where each
-- node is annotated by a string. We allow the annotation type to
-- depend on the current subgame, for integration with formulas.

data Annotation (G : Game) (A : Game  Set) : Set where
  ν : A G  ((i : Mov G)  Annotation (G  i) A)  Annotation G A