{-# OPTIONS --safe #-}

open import Level

open import Data.Product as Σ
open import Data.Sum as ⊎
open import Relation.Binary.PropositionalEquality

module Game-Basics where
-- Games for learning something from the set 𝔻
-- for which games have the outcome R

-- The parameter F is the type of game, where ℓr is
-- the level of the 'result type':
Game-Type : Setω
Game-Type = {ℓr : Level} (R : Set ℓr) {ℓ : Level} → Set ℓ → Set (ℓ ⊔ ℓr)

-- We require that the game type is functorial in this sense:
Functorial : Game-Type → Setω
Functorial F =
  ∀ {ℓr : Level} {R : Set ℓr}
  {ℓ ℓ'  : Level} {X : Set ℓ} {Y : Set ℓ'}
  → (f : X → Y) → F R X → F R Y


-- When modelling the teacher, we allow the teacher to have the following side-effects:
-- (1) The teacher may have an internal state T
-- (2) The teacher can surrender by throwing an exception of type R
M : ∀ {ℓt ℓr ℓ : Level} (R : Set ℓr) (T : Set ℓt) → (X : Set ℓ) → Set (ℓ ⊔ ℓt ⊔ ℓr)
M R T X = T → (R ⊎ (T × X))

M-map : ∀ {ℓt ℓr ℓ : Level} {R : Set ℓr} {T : Set ℓt} → {X : Set ℓ} → {ℓ' : Level} → {Y : Set ℓ'} → (X → Y) → (M R T X → M R T Y)
M-map f MTX t = ⊎.map₂ (Σ.map₂ f) (MTX t)