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