minor additions for game

Co-authored-by: Paulo Oliva <[email protected]>

source/Games/List.lagda

@@ -0,0 +1,42 @@
+Martin Escardo, Paulo Oliva, 2024
+
+The list monad.
+
+\begin{code}
+
+{-# OPTIONS --safe --without-K #-}
+
+module Games.List where
+
+open import Games.Monad
+open import MLTT.Spartan hiding (J)
+open import MLTT.List hiding (map)
+
+𝕃 : Monad
+𝕃 = record {
+ functor = List ;
+ η       = [_] ;
+ ext     = List-ext ;
+ ext-η   = concat-singletons ;
+ unit    = List-ext-unit ;
+ assoc   = List-ext-assoc
+ }
+
+module List-definitions where
+
+ _⊗ᴸ⁺_ : {X : Type} {Y : X → Type}
+      → List X
+      → ((x : X) → List (Y x))
+      → List (Σ x ꞉ X , Y x)
+ _⊗ᴸ⁺_ = _⊗_ 𝕃
+
+ ηᴸ⁺ : {X : Type} → X → List X
+ ηᴸ⁺ = η 𝕃
+
+ extᴸ⁺ : {X Y : Type} → (X → List Y) → List X → List Y
+ extᴸ⁺ = ext 𝕃
+
+ mapᴸ⁺ : {X Y : Type} → (X → Y) → List X → List Y
+ mapᴸ⁺ = map 𝕃
+
+\end{code}

source/Games/index.lagda

@@ -17,8 +17,9 @@ import Games.J                       -- Selection monad.
 import Games.K                       -- Continuation (or quantifier) monad.
 import Games.JK                      -- Relationship between the two mondas.
 import Games.Monad                   -- (Automatically strong, wild) monads on types.
-import Games.Reader
-import Games.NonEmptyList
+import Games.Reader                  -- Reader monad.
+import Games.List                    -- List monad.
+import Games.NonEmptyList            -- Non-empty list monad.
 import Games.TicTacToe0
 import Games.TicTacToe1              -- Like TicTacToe0 but using Games.Constructor.
 import Games.TicTacToe2              -- More efficient and less elegant version.

source/MLTT/List.lagda

@@ -409,6 +409,11 @@ List-ext : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
          → (X → List Y) → (List X → List Y)
 List-ext f xs = concat (map f xs)
 
+List-ext-unit : {X : 𝓤 ̇ } {Y : 𝓥 ̇ }
+                (f : X → List Y) (x : X)
+              → f x ++ [] ＝ f x
+List-ext-unit f x = ([]-right-neutral (f x))⁻¹
+
 List-ext-assoc
  : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ }
    (g : Y → List Z) (f : X → List Y)