2.1 Arenas and legal positions

A game is a certain kind of a directed rooted forest, where the paths from a root represent possible developments or positions in a ‘game in the ordinary sense’ (e.g., chess). These positions are finite sequences of vertices or moves, ^{Footnote 2} and a play in the game proceeds as its participants alternately perform moves along a gradual growth of a position.

For technical convenience, we identify a game with the set of all positions in the game. We focus on standard two-person games between Player (P) (or a mathematician) and Opponent (O) (or an oracle), in which O always starts a play.

Technically, games are based on two preliminary concepts: arenas and legal positions. An arena defines the basic components of a game, which in turn induces legal positions in the arena that specify the basic rules of the game in the sense that each position in the game must be legal. Let us first recall these two concepts.

Convention 2.1.2. We abbreviate a move $m^{xy}$ as m, and instead define $\lambda(m) := xy$ , $\lambda^\mathrm{OP}(m) := x$ and $\lambda^\mathrm{QA}(m) := y$ . A move m is called an O-move if $\lambda^\mathrm{OP}(m) = \mathrm{O}$ , a P-move if $\lambda^\mathrm{OP}(m) = \mathrm{P}$ , a question if $\lambda^\mathrm{QA}(m) = \mathrm{Q}$ , and an answer if $\lambda^\mathrm{QA}(m) = \mathrm{A}$ .

• • $M_A$ is a set of moves;

• • $\vdash_A$ , called the enabling relation, is a subset of the cartesian product $(\{ \star \} \cup M_A) \times M_A$ , where $\star$ is an arbitrarily fixed element such that $\star \not \in M_A$ , that satisfies

  • - (E1) If $\star \vdash_A m$ , then $\lambda (m) = \mathrm{OQ}$ ;

  • - (E2) If $m \vdash_A n$ and $\lambda^\mathrm{QA} (n) = \mathrm{A}$ , then $\lambda^\mathrm{QA} (m) = \mathrm{Q}$ ;

  • - (E3) If $m \vdash_A n$ and $m \neq \star$ , then $\lambda^\mathrm{OP} (m) \neq \lambda^\mathrm{OP} (n)$ .

We call a move $m \in M_A$ initial if $\star \vdash_A m$ , and define $M_A^{\mathrm{Init}} := \{ \, m \in M_A \mid \star \vdash_A m \, \}$ . An arena A is said to be well-founded if so is the enabling relation $\vdash_A$ , i.e., if there is no sequence $(m_i)_{i \in \mathbb{N}}$ of moves $m_i \in M_A$ such that $\star \vdash_A m_0$ and $m_i \vdash_A m_{i+1}$ for all $i \in \mathbb{N}$ .

An arena A specifies moves in a game, each of which is O’s/P’s question/answer, and the relation $m \vdash_A n$ defining that the move n can be performed specifically for the move m during a play in the game (see Definition 2.1.5), where $\star \vdash_A m$ means that O can initiate a play by m in the game. The axioms E1, E2 and E3 are then to be read as follows:

• • E1 sets the convention that an initial move must be O’s question;

• • E2 states that an answer must be performed for a question;

• • E3 says that an O-move must be performed for a P-move, and vice versa.

We next review a legal position, which is a class of a finite sequence of moves equipped with a pointer from later to earlier elements of the sequence. The idea is that each non-initial occurrence of a move in a legal position is made for a specific previous occurrence, and a pointer specifies such pairs of occurrences. Pointers enable us to distinguish similar yet different plays (Abramsky and McCusker Reference Abramsky and McCusker1999b, Section 2.4) and define views (Definition 2.1.10), where views play crucial roles for constraints on strategies (Definition 2.2.6).

We call a finite sequence of moves together with a pointer a justified (j-) sequence. A legal position is then a particular kind of a j-sequence.

Convention 2.1.6. Let $\boldsymbol{s} = (\boldsymbol{s}, \mathcal{J}_{\boldsymbol{s}})$ be a j-sequence.

• • An occurrence $(\boldsymbol{s}(i), i)$ is said to be initial in the j-sequence $\boldsymbol{s}$ if $\mathcal{J}_{\boldsymbol{s}}(i) = 0$ ;

• • We say that the occurrence $(\boldsymbol{s}({\mathcal{J}_{\boldsymbol{s}}(i)}), \mathcal{J}_{\boldsymbol{s}}(i))$ is the justifier of a non-initial one $(\boldsymbol{s}(i), i)$ in the j-sequence $\boldsymbol{s}$ , and $(\boldsymbol{s}(i), i)$ is justified by $(\boldsymbol{s}({\mathcal{J}_{\boldsymbol{s}}(i)}), \mathcal{J}_{\boldsymbol{s}}(i))$ in $\boldsymbol{s}$ ;

• • A j-sequence $\boldsymbol{s}$ is said to be in an arena A if its elements are moves in A, and its pointer respects the enabling relation $\vdash_A$ in the sense that

  \begin{equation*}\forall i \in \overline{|\boldsymbol{s}|} . \, \big(\mathcal{J}_{\boldsymbol{s}}(i) = 0 \Rightarrow \star \vdash_A \boldsymbol{s}(i)\big) \wedge \big(\mathcal{J}_{\boldsymbol{s}}(i) \neq 0 \Rightarrow \boldsymbol{s}({\mathcal{J}_{\boldsymbol{s}}(i)}) \vdash_A \boldsymbol{s}(i)\big)\end{equation*}
  holds, where we write $\mathscr{J}_A$ for the set of all j-sequences in A.

Convention 2.1.8. Henceforth, we are casual about the distinction between moves and their occurrences in a sequence; e.g., we often keep the pointer $\mathcal{J}_{\boldsymbol{s}}$ of a j-sequence $\boldsymbol{s} = (\boldsymbol{s}, \mathcal{J}_{\boldsymbol{s}})$ implicit (as it is mostly clear), and abbreviate an occurrence $(\boldsymbol{s}(i), i)$ as $\boldsymbol{s}(i)$ . Moreover:

• • We informally write $\mathcal{J}_{\boldsymbol{s}}(\boldsymbol{s}(i)) = \boldsymbol{s}(j)$ if $\mathcal{J}_{\boldsymbol{s}}(i) = j > 0$ ;

• • We extend the notation $\boldsymbol{s}(i)$ ( $i \in |\boldsymbol{s}|$ ) to $i = 0$ by $\boldsymbol{s}(0) := \star$ so that the pair $(\star, 0)$ can be seen as justifying initial occurrences in $\boldsymbol{s}$ . We then write $\mathcal{J}_{\boldsymbol{s}}(\boldsymbol{s}(i)) = \boldsymbol{s}(j)$ even if $\mathcal{J}_{\boldsymbol{s}}(i) = j = 0$ , i.e., $\boldsymbol{s}(j) = \star$ . This is convenient; e.g., see Definitions 2.1.9 and 2.3.3.

1. (1) $\lceil \boldsymbol{\epsilon} \rceil := \boldsymbol{\epsilon}$ ;

2. (2) $\lceil \boldsymbol{s} m \rceil := \lceil \boldsymbol{s} \rceil . m$ if m is a P-move, where the justifier of m is kept unchanged;

3. (3) $\lceil \boldsymbol{s} m \rceil := m$ if m is initial;

4. (4) $\lceil \boldsymbol{s} m \boldsymbol{t} n \rceil := \lceil \boldsymbol{s} \rceil . m n$ if n is an O-move such that m justifies n;

5. (5) $\lfloor \boldsymbol{\epsilon} \rfloor := \boldsymbol{\epsilon}$ ;

6. (6) $\lfloor \boldsymbol{s} m \rfloor := \lfloor \boldsymbol{s} \rfloor . m$ if m is an O-move, where the justifier of m is kept unchanged;

7. (7) $\lfloor \boldsymbol{s} m \boldsymbol{t} n \rfloor := \lfloor \boldsymbol{s} \rfloor . m n$ if n is a P-move such that m justifies n.

The idea of views is as follows. For a j-sequence $\boldsymbol{s} m$ such that m is a P- (respectively, O-) move, the P-view $\lceil \boldsymbol{s} \rceil$ (respectively, O-view $\lfloor \boldsymbol{s} \rfloor$ ) is the currently ‘relevant part’ of $\boldsymbol{s}$ for P (respectively, O). In other words, P (respectively, O) is concerned only with the last occurrence of an O- (respectively, P-) move, its justifier and that justifier’s P- (respectively, O-) view, which then recursively proceeds. See Coquand (Reference Coquand1995) for an explanation of views in terms of logical calculi, and Curien (Reference Curien1998) in terms of lambda-calculi.

• • (Alternation) If $\boldsymbol{s} = \boldsymbol{s}_{\textbf{1}} m n \boldsymbol{s}_{\textbf{2}}$ , then $\lambda^\mathrm{OP} (m) \neq \lambda^\mathrm{OP} (n)$ ;

• • (Visibility) If $\boldsymbol{s} = \boldsymbol{t} m \boldsymbol{u}$ with m non-initial, then $\mathcal{J}_{\boldsymbol{s}}(m)$ occurs in the P-view $\lceil \boldsymbol{t} \rceil$ if m is a P-move, and in the O-view $\lfloor \boldsymbol{t} \rfloor$ otherwise.

A legal position is in an arena A if it is a j-sequence in A (Definition 2.1.5). We write $\mathscr{L}_A$ for the set of all legal positions in A.

As already noted, legal positions in an arena are to specify the basic rules of a game in the sense that positions in the game must be legal (Definition 2.2.1) so that

• • During a play in the game, O makes the first move by a question (by E1),^{Footnote 3} and then P and O alternately perform moves (by alternation), where each non-initial move is made for a specific previous occurrence, viz., its justifier;^{Footnote 4}

• • The justifier of each non-initial occurrence is in the ‘relevant part’ (by visibility).

2.2 Games and strategies

We are now ready to recall the central concepts: games and strategies. For convenience, we slightly modify the original definition of games by McCusker (Reference McCusker1998):

1. (1) The set G is nonempty and prefix-closed (i.e., $\boldsymbol{s}m \in G \Rightarrow \boldsymbol{s} \in G$ );

2. (2) The pair $\mathrm{Arn}(G) := (M_G, \vdash_G)$ ^{Footnote 5} is an arena, where $M_G := \{ \, \boldsymbol{s}(i) \mid \boldsymbol{s} \in G, i \in \overline{|\boldsymbol{s}|} \, \}$ and $\vdash_G \, := \{ \, (\star, \boldsymbol{s}(j)) \mid \boldsymbol{s} \in G, \mathcal{J}_{\boldsymbol{s}}(j) = 0 \, \}\cup \{ \, (\boldsymbol{s}(i), \boldsymbol{s}(j)) \mid \boldsymbol{s} \in G, \mathcal{J}_{\boldsymbol{s}}(j)= i > 0 \, \}$ .

A game G is said to be well-founded if so is the arena $\mathrm{Arn}(G)$ , and well-opened if each of its elements has at most one initial occurrence (i.e., the conjunction of $\boldsymbol{s}m \in G$ and $m \in M_G^{\mathrm{Init}}$ implies $\boldsymbol{s} = \boldsymbol{\epsilon}$ ). We call elements of G (valid) positions in G.

A subgame of a game G is a game $H \subseteq G$ , and $\mathrm{sub}(G) := \{ \, H \mid \textit{H}\,\text{is a subgame of}\, \textit{G} \, \}$ .

However, ${\mathrm{!}} G$ is well-defined even if G is not thread-closed. Also, we later focus on well-opened games (for the identities in the categories of games to be well-defined), which are trivially thread-closed. For these reasons, we omit thread-closure in Definition 2.2.1.

Each game G is non-empty since it has the empty position $\boldsymbol{\epsilon}$ or the ‘starting moment,’ and it is prefix-closed since each nonempty position or ‘moment’ in G has the previous ‘moment.’ It is easy to see that positions in G are all legal in the arena $\mathrm{Arn}(G)$ ; i.e., legality is the minimum requirement on positions. Later, we focus on well-opened, well-founded games since identities in the categories of these games behave well (Section 2.3).

The tuple $\mathcal{M}(G) := (M_G, \lambda_G, \vdash_G, G)$ , where $\lambda_G : m \mapsto \lambda(m)$ (Definition 2.1.1), forms a game in the sense of McCusker (Reference McCusker1998)^{Footnote 7} whose labels are embedded into moves, which we call an MC-game. Conversely, given an MC-game H, the set $P_H$ of all positions in H is a game in the sense of Definition 2.2.1. Further, the MC-game $\mathcal{M}(G)$ satisfies: Each move $m \in M_G$ occurs in a position in G, and each pair $\star \vdash_G m$ or $m_1 \vdash_G m_2$ is used in a position in G. We call an MC-game economical if it satisfies these two conditions. Then, the map $\mathcal{M}$ defines a bijection between games and economical MC-games with the inverse $H \mapsto P_H$ .

Because the two axioms on economical MC-games only exclude unused structures, the simplification of MC-games into games is harmless. We may even dispense with arenas (and the second axiom in Definition 2.2.1) by directly axiomatising the effects of arenas on legal positions (Footnotes 3–4), but we do not since arenas are convenient for defining constructions on games (Definition 2.3.3).

The idea is that a strategy $\sigma : G$ describes for P how to play on the game G by the computation $\boldsymbol{s}m \in G^{\mathrm{Odd}} \mapsto \boldsymbol{s}mn \in \sigma$ (n.b., m is an O-move, and n is a P-move), which is unique, if any, by the determinacy of $\sigma$ , and in general partial because there can be no output $\boldsymbol{s}mn \in \sigma$ for some input $\boldsymbol{s}m \in G^{\mathrm{Odd}}$ .

Definition 2.2.4 (closure on strategies). The closure of a strategy $\sigma : G$ with respect to another game H is the subgame $\overline{\sigma}_H \subseteq \sigma \cup H$ defined inductively by

\begin{equation*}\overline{\sigma}_H := \{ \boldsymbol{\epsilon} \} \cup \{ \, \boldsymbol{s}m \in H^{\mathrm{Odd}} \mid \boldsymbol{s} \in \overline{\sigma}_H \, \} \cup \{ \, \boldsymbol{t}lr \in \sigma \mid \boldsymbol{t}l \in \overline{\sigma}_H \, \}.\end{equation*}

We utilise this closure operation in Section 3. We leave it to the reader to verify by induction that the equation $\overline{\sigma}_G = \sigma \cup \{ \, \boldsymbol{s}m \in G \mid \boldsymbol{s} \in \sigma \, \}$ holds for all strategies $\sigma : G$ .

The flat game on a given set S is the game $\mathrm{flat}(S) := \mathrm{Pref}(\{ \, q^{\mathrm{OQ}} . m^{\mathrm{PA}} \mid m \in S \, \})$ , where q is an arbitrarily fixed element such that $q \not\in S$ , and $q^{\mathrm{OQ}}$ justifies $m^{\mathrm{PA}}$ . It has strategies $\bot := \{ \boldsymbol{\epsilon} \}$ and $\underline{m} := \{ \boldsymbol{\epsilon}, q m \}$ for each $m \in S$ . Consider, for instance, the empty game $0 := \mathrm{flat}(\emptyset)$ and the natural number game $N := \mathrm{flat}(\mathbb{N})$ .

Next, recall that not every strategy corresponds to a (formal) proof. For instance, the empty game 0 models falsity, and thus the strategy $\bot : 0$ should not be an interpretation of a proof. We therefore carve out strategies corresponding to proofs as winning ones:

We think of winning strategies as proofs in classical logic as follows. First, proofs should not get ‘stuck,’ so strategies for proofs must be total. Next, imposing innocence on strategies corresponds to excluding stateful terms (Abramsky et al. Reference Abramsky, Honda and McCusker1998; Abramsky and McCusker Reference Abramsky and McCusker1997, Reference Abramsky and McCusker1999a). Since logic is concerned with truths, which are independent of ‘passage of time,’ proofs should not depended on ‘states of arguments.’ Hence, we impose innocence on strategies for proofs. Finally, we need noetherianity to handle infinite plays: If a play by an innocent, noetherian strategy keeps growing infinitely, then it cannot be P’s ‘intention,’ so the play must be ‘win’ for P. Technically, noetherianity is crucial for the closure of winning strategies under composition (Definition 2.3.6).

In addition, well-bracketing bans classical reasoning or control operators (Laird Reference Laird1997). Hence, we regard winning, well-bracketed strategies as proofs in intuitionistic logic.

2.3 Constructions on games and strategies

We next recall constructions on games and strategies. Because they are standard in the literature, we leave expositions and examples to Abramsky and McCusker Reference Abramsky and McCusker(1999b, Section 3.2).

Convention 2.3.1. We omit ‘tags’ for disjoint union $\uplus$ . For instance, we write $x \in S \uplus T$ if $x \in S$ or $x \in T$ ; moreover, given relations $R_S \subseteq S \times S$ and $R_T \subseteq T \times T$ , we write $R_S \uplus R_T$ for the relation on $S \uplus T$ such that $(x, y) \in R_S \uplus R_T$ precisely when $(x, y) \in R_S$ or $(x, y) \in R_T$ .

Notation 2.3.4 Notationally, exponential ${\mathrm{!}}$ precedes other constructions on games, while tensor $\otimes$ and product $\mathbin{\&}$ precede linear implication $\multimap$ and implication $\Rightarrow$ .

We leave it to the reader to verify that these constructions on games correspond to those on economical MC games (McCusker Reference McCusker1998) under the bijection $\mathcal{M}$ .

For the dereliction $\mathrm{der}_G$ to be well-defined, we must focus on well-opened games G; see McCusker (Reference McCusker1998, pp. 42–43) for the details. Although well-opened games are not closed under exponential, it does not matter for us, just like McCusker (Reference McCusker1998, p. 43), because we only need cartesian closure, not exponential itself, and because well-opened games are closed under implication and product (Lemma 2.3.5).

• • Well-opened games as objects;

• • Strategies on the implication $G \Rightarrow H$ as morphisms $G \rightarrow H$ ;

• • The composition $\psi \bullet \phi := \psi \circ \phi^\dagger : G \Rightarrow J$ of strategies as the composition of morphisms $\phi : G \rightarrow H$ and $\psi : H \rightarrow J$ ;

• • The dereliction $\mathrm{der}_G$ as the identity on each object G.

The subcategory $\mathbb{LG}_{\mathrm{!}}$ (respectively, $\mathbb{WG}_{\mathrm{!}}$ ) of $\mathbb{G}_{\mathrm{!}}$ consists of well-founded, well-opened games and winning (respectively, winning, well-bracketed) strategies.

We use the subscript $(\_)_{\mathrm{!}}$ to distinguish these categories from the linear ones (McCusker Reference McCusker1998, Section 3.3), in which morphisms $G \rightarrow H$ are strategies on the linear implication $G \multimap H$ .

Games in $\mathbb{G}_{\mathrm{!}}$ (respectively, $\mathbb{LG}_{\mathrm{!}}$ and $\mathbb{WG}_{\mathrm{!}}$ ) are well-opened (respectively, well-opened and well-founded) for the identities to be well-defined (Lemma 2.3.7). Note that strategies in $\mathbb{G}_{\mathrm{!}}$ have no constraints, so they embody unrestricted computations. In contrast, strategies in $\mathbb{LG}_{\mathrm{!}}$ (respectively, $\mathbb{WG}_{\mathrm{!}}$ ) are winning (respectively, winning and well-bracketed), formulating proofs in classical logic (respectively, proofs in intuitionistic logic).

These categories are cartesian closed, where a terminal object, product and exponential objects are the terminal game T, product $\mathbin{\&}$ and implication $\Rightarrow$ , respectively. In fact, since morphisms in these categories are the same as those in the cartesian closed categories of MC-games (McCusker Reference McCusker1998, Section 3.3), our categories also satisfy the equational axioms on cartesian closure in the same way. Thus, by Lemmata 2.3.5 and 2.3.7, we conclude:

Notation 2.3.10 Henceforth, we employ the following notations:

• • Given a strategy $\sigma : G$ , we write $\sigma^{T} : T \multimap G$ and $\sigma^{{\mathrm{!}} T} : T \Rightarrow G$ for the evident strategies that coincide with $\sigma$ up to ‘tags’;

• • Given strategies $\phi : T \multimap G$ and $\phi' : T \Rightarrow G$ , we write $\phi_{T}, \phi'_{{\mathrm{!}} T} : G$ for the evident strategies that coincide with $\phi$ and $\phi'$ up to ‘tags,’ respectively;

• • Given strategies $\psi : G \multimap H$ and $\sigma : G$ , we define $\psi \circ \sigma := (\psi \circ \sigma^{T})_{T} : H$ ;

• • Given strategies $\sigma : G$ and $\tau : H$ , we define $\sigma \otimes \tau := ((\sigma^{T} \otimes \tau^{T}) \circ \iota)_{T} : G \otimes H$ , where $\iota$ is the unique strategy on $T \multimap T \otimes T$ , and $\langle \sigma, \tau \rangle := \langle \sigma^{T}, \tau^{T} \rangle_{T} : G \mathbin{\&} H$ ;

• • Given a strategy $\sigma : G$ , we define $\sigma^\dagger := ((\sigma^{{\mathrm{!}} T})^\dagger)_{{\mathrm{!}} T} : {\mathrm{!}} G$ .

3.1 Predicate games

We reformulate the idea of a p-game $\Gamma = (|\Gamma|, \| \Gamma \|)$ sketched above in a technically handier way as follows. First, recall that the closure $\overline{\gamma}_{|\Gamma|}$ of a strategy $\gamma : |\Gamma|$ with respect to the ambient game $|\Gamma|$ (Definition 2.2.4) is characterised by a simple form

(1) \begin{equation}\overline{\gamma}_{|\Gamma|} = \gamma \cup \{ \, \boldsymbol{s}m \in |\Gamma| \mid \boldsymbol{s} \in \gamma \, \}.\end{equation}

Second, the central condition $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}} : \Gamma(\gamma)$ is equivalent to another relation

(2) \begin{equation}\overline{\gamma}_{|\Gamma|} \preccurlyeq \Gamma(\gamma)\end{equation}

by Proposition 3.1.2, where the symbol $\preccurlyeq$ denotes Chroboczek’s beautiful liveness ordering:

1. (1) If $\boldsymbol{s} \in (G \cap H)^{\mathrm{Even}}$ and $\boldsymbol{s}m \in H^{\mathrm{Odd}}$ , then $\boldsymbol{s}m \in G^{\mathrm{Odd}}$ ;

2. (2) If $\boldsymbol{t}l \in (G \cap H)^{\mathrm{Odd}}$ and $\boldsymbol{t}lr \in G^{\mathrm{Even}}$ , then $\boldsymbol{t}lr \in H^{\mathrm{Even}}$ .

Assume $\overline{\sigma}_{G} \not\preccurlyeq H$ ; it remains to show $\overline{\sigma}_H^{\mathrm{Even}} \not\subseteq H^{\mathrm{Even}}$ . By $\overline{\sigma}_{G} \not\preccurlyeq H$ , there is some $\boldsymbol{s}mn \in \overline{\sigma}_G^{\mathrm{Even}}$ with $\boldsymbol{s}m \in \overline{\sigma}_G \cap H$ and $\boldsymbol{s}mn \not\in H$ . Note that $\boldsymbol{s}mn \in \overline{\sigma}_G^{\mathrm{Even}}$ implies $\boldsymbol{s}mn \in \sigma$ . We also see by induction on the lengths of positions that $\overline{\sigma}_G \cap H \subseteq \overline{\sigma}_H$ , whence $\boldsymbol{s}m \in \overline{\sigma}_H$ . Then, $\boldsymbol{s}mn \in \overline{\sigma}_H$ follows from $\boldsymbol{s}m \in \overline{\sigma}_H$ and $\boldsymbol{s}mn \in \sigma$ . We have therefore shown $\overline{\sigma}_H^{\mathrm{Even}} \not\subseteq H^{\mathrm{Even}}$ since $\boldsymbol{s}mn \in \overline{\sigma}_H^{\mathrm{Even}}$ and $\boldsymbol{s}mn \not\in H^{\mathrm{Even}}$ .

Proposition 3.1.2 reduces the relation $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}} : \Gamma(\gamma)$ to the one $\overline{\gamma}_{|\Gamma|} \preccurlyeq \Gamma(\gamma)$ , where $\overline{\gamma}_{|\Gamma|}$ is often easier to handle than $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}}$ by its simple form $ \overline{\gamma}_{|\Gamma|} = \gamma \cup \{ \, \boldsymbol{s}m \in |\Gamma| \mid \boldsymbol{s} \in \gamma \, \}$ (1). Also, if $\overline{\gamma}_{|\Gamma|} \preccurlyeq \Gamma(\gamma)$ (2), then Proposition 3.1.2 simplifies $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}}$ by the equation $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}} = \gamma \cap \Gamma(\gamma)$ .

We are now ready to introduce the central concept of the present work:

• • A p-game $\Gamma$ is well-founded (respectively, well-opened) if so is the game $|\Gamma|$ ;

• • A strategy on a p-game $\Gamma$ , written $\gamma : \Gamma$ , is a strategy $\gamma : |\Gamma|$ that satisfies $\overline{\gamma}_{|\Gamma|} \preccurlyeq \Gamma(\gamma)$ , and it is total (respectively, innocent, noetherian, well-bracketed) if so is the strategy $\gamma \cap \Gamma(\gamma) : \Gamma(\gamma)$ , where $\mathrm{st}(\Gamma) := \{ \, \gamma \mid \gamma : \Gamma \, \}$ and $\overline{\gamma}_\Gamma := \overline{\gamma}_{\Gamma(\gamma)}$ for all $\gamma : \Gamma$ ;

• • A position in a p-game $\Gamma$ is an element $\boldsymbol{s} \in \overline{\gamma}_\Gamma$ for some strategy $\gamma : \Gamma$ .

The main point of the generalisation of a game $|\Gamma|$ to a p-game $\Gamma = (|\Gamma|, \| \Gamma \|)$ is that P can only select a strategy $\gamma : |\Gamma|$ that satisfies $\overline{\gamma}_{|\Gamma|} \preccurlyeq \Gamma(\gamma)$ , and this choice $\gamma : \Gamma$ fixes the underlying game $\Gamma(\gamma)$ . In essence, the game-semantic counterpart of the path from STLC to MLTT (Section 1.1) is the family $\| \Gamma \|$ added to $|\Gamma|$ , which brings these strategy filtering and game fixing abilities to $|\Gamma|$ . As we have seen, the first and the second abilities address the first and the second problems listed at the beginning of Section 3, respectively.

3.2 Cartesian closed categories of predicate games

Next, we lift the constructions on games (Section 2.3) to p-games. The cases of product $\mathbin{\&}$ , tensor $\otimes$ and exponential ${\mathrm{!}}$ are straightforward since we can construct them pointwisely:

Notation 3.2.1. Let G be a game, $\boldsymbol{s} \in {\mathrm{!}} G$ and $i \in \mathbb{N}$ . We write $\boldsymbol{s} \upharpoonright i$ for the j-subsequence of $\boldsymbol{s}$ that consists of occurrences hereditarily justified by the $(i+1)$ st initial occurrence in $\boldsymbol{s}$ . For instance, if $\boldsymbol{s} = q2q1q0 \in {\mathrm{!}} N$ , then $\boldsymbol{s} \upharpoonright 0 = q2$ , $\boldsymbol{s} \upharpoonright 1 = q1$ and $\boldsymbol{s} \upharpoonright 2 = q0$ .

Convention 3.2.2. Given a strategy $\sigma$ on the tensor $G_0 \otimes G_1$ of games $G_i$ ( $i = 0, 1$ ), let

(3)

Similarly, given a strategy $\tau$ on the exponential ${\mathrm{!}} G$ of a game G and $j \in \mathbb{N}$ , let

(4) \begin{equation}\tau \upharpoonright j := \begin{cases} \{ \, \boldsymbol{s} \upharpoonright j \mid \boldsymbol{s} \in \tau \, \} &\text{if $\{ \, \boldsymbol{s} \upharpoonright k \mid \boldsymbol{s} \in \tau \, \} : G$ for all $k \in \mathbb{N}$;} \\ \uparrow &\text{otherwise.} \end{cases}\end{equation}

Given a p-game $\Gamma$ , we let the value $\Gamma(\uparrow)$ to be undefined, and the constructions $\otimes$ , $\multimap$ , $\&$ and ${\mathrm{!}}$ on undefined games to be undefined. Finally, we extend the relation $\overline{\gamma}_{|\Gamma|} \preccurlyeq \Gamma(\gamma)$ by defining that it does not hold if the game $\Gamma(\gamma)$ is undefined.

Definition 3.2.3 (product and tensor on predicate games). The product of p-games $\Gamma$ and $\Delta$ is the p-game $\Gamma \mathbin{\&} \Delta$ defined by

and their tensor is the p-game $\Gamma \otimes \Delta$ defined by

Definition 3.2.4 (countable tensor). The countable tensor of a family $\{ G_i \}_{i \in \mathbb{N}}$ of subgames $G_i \subseteq H$ is the subgame $\otimes_{i \in \mathbb{N}}G_i \subseteq {\mathrm{!}} H$ defined by

\begin{equation*}\otimes_{i \in \mathbb{N}}G_i := \{ \, \boldsymbol{s} \in {\mathrm{!}} H \mid \forall j \in \mathbb{N} . \, \boldsymbol{s} \upharpoonright j \in G_j \, \}.\end{equation*}

Similarly to tensor, we apply the above convention for the constructions on undefined objects to countable tensor too.

Definition 3.2.5 (exponential of predicate games). The exponential of a p-game $\Gamma$ is the p-game ${\mathrm{!}} \Gamma$ defined by

Accordingly, strategies on $\Gamma \mathbin{\&} \Delta$ are the pairings $\langle \gamma, \delta \rangle$ of $\gamma : \Gamma$ and $\delta : \Delta$ . Besides, by Convention 3.2.2, strategies on $\Gamma \otimes \Delta$ are the tensors $\gamma \otimes \delta$ of $\gamma : \Gamma$ and $\delta : \Delta$ , and strategies on ${\mathrm{!}} \Gamma$ are those $\sigma : {\mathrm{!}} |\Gamma|$ such that $\{ \, \boldsymbol{s} \upharpoonright i \mid \boldsymbol{s} \in \sigma \, \} : \Gamma$ for all $i \in \mathbb{N}$ .

In contrast, we cannot apply the pointwise method to linear implication $\multimap$ : If we define $|\Delta^\Gamma| := |\Delta|^{|\Gamma|}$ for the linear implication $\Delta^\Gamma$ , then it is unclear how to decompose strategies $\phi : |\Delta|^\Gamma$ into those on $|\Gamma|$ and $|\Delta|$ . We overcome this problem based on the elegant game semantics of universal quantification (Abramsky and Jagadeesan Reference Abramsky and Jagadeesan2005, p. 17):

Definition 3.2.6 (linear implication and implication between predicate games). The linear implication between p-games $\Gamma$ and $\Delta$ is the p-game $\Gamma \multimap \Delta$ (also denoted by $\Delta^\Gamma$ ) defined by $|\Delta^\Gamma| := |\Delta|^{|\Gamma|}$ and for all $\phi : |\Delta^\Gamma|$

\begin{align*}(\Delta^\Gamma)(\phi) &:= \{ \boldsymbol{\epsilon} \} \cup \{ \, \boldsymbol{s}m \in |\Delta^\Gamma|^{\mathrm{Odd}} \mid \boldsymbol{s} \in (\Delta^\Gamma)(\phi), \exists \gamma : \Gamma . \, \boldsymbol{s}m \in \Delta(\phi \circ \gamma)^{\overline{\gamma}_{\Gamma}} \, \} \\&\cup \{ \, \boldsymbol{t}lr \in |\Delta^\Gamma|^{\mathrm{Even}} \mid \boldsymbol{t}l \in (\Delta^\Gamma)(\phi), \forall \gamma : \Gamma . \, \boldsymbol{t}l \in \Delta(\phi \circ \gamma)^{\overline{\gamma}_{\Gamma}} \Rightarrow \boldsymbol{t}lr \in \Delta(\phi \circ \gamma)^{\overline{\gamma}_{\Gamma}} \, \},\end{align*}

and the implication between $\Gamma$ and $\Delta$ is the linear implication $\Gamma \Rightarrow \Delta := {\mathrm{!}} \Gamma \multimap \Delta$ .

The first clause of the inductive definition of the subgame $(\Delta^\Gamma)(\phi) \subseteq |\Delta^\Gamma|$ is the base case. The second clause specifies one of the two inductive steps: At an even-length position $\boldsymbol{s} \in (\Delta^\Gamma)(\phi)^{\mathrm{Even}}$ , O can make a move m as in $\Delta(\phi \circ \gamma)^{\overline{\gamma}_{\Gamma}} \subseteq |\Delta^\Gamma|$ for any $\gamma : \Gamma$ not yet excluded, i.e., $\boldsymbol{s} \in \Delta(\phi \circ \gamma)^{\overline{\gamma}_{\Gamma}}$ . Finally, the third clause stipulates the other inductive step: At an odd-length position $\boldsymbol{t}l \in (\Delta^\Gamma)(\phi)^{\mathrm{Odd}}$ , the next move r by the strategy $\phi$ must be as in $\Delta(\phi \circ \gamma)^{\overline{\gamma}_{\Gamma}} \subseteq |\Delta^\Gamma|$ for all $\gamma : \Gamma$ not yet excluded, i.e., $\boldsymbol{t}l \in \Delta(\phi \circ \gamma)^{\overline{\gamma}_{\Gamma}}$ .

The basic idea is that, in the subgame $\Delta^\Gamma(\phi) \subseteq |\Delta^\Gamma|$ , O can play as in any subgame $\Delta(\phi \circ \gamma)^{\overline{\gamma}_{\Gamma}} \subseteq |\Delta^\Gamma|$ not yet excluded; then, since P or $\phi$ should see what $\gamma : \Gamma$ is only via plays, $\Delta^\Gamma(\phi)$ only allows P to play as in $\Delta(\phi \circ \gamma)^{\overline{\gamma}_{\Gamma}}$ for all $\gamma$ not yet excluded.

In particular, O’s strategy $\gamma : \Gamma$ on the domain $|\Gamma|$ determines its underlying game $\overline{\gamma}_\Gamma$ , and P’s play by $\phi : \Delta^\Gamma$ on the domain must be as in $\overline{\gamma}_\Gamma$ for all possible $\gamma$ not yet excluded. This is crucial for the composition of strategies between p-games to be well-defined (Lemma 3.2.9); see Footnote 15. This additional subtlety is the main difference from the game semantics of universal quantification by Abramsky and Jagadeesan (Reference Abramsky and Jagadeesan2005). For instance, a strategy $\phi : |\Sigma(N_{[0]}, (\mathrm{List}_N)_{[1]})| \multimap |N_{[2]}|$ that contains the position $q_{[2]} m_{[1]}$ is not on the p-game $\Sigma(N_{[0]}, (\mathrm{List}_N)_{[1]}) \multimap N_{[2]}$ whatever m is since at the position $q_{[2]}$ the strategy $\langle \underline{0}, \top \rangle : \Sigma(N, (\mathrm{List}_N))$ is not excluded, where $\Sigma(N, \mathrm{List}_N)(\langle \underline{0}, \top \rangle) = N \mathbin{\&} T$ .

As emphasised before, strategies $\phi : \Delta^\Gamma$ are indeed ordinary ones (Definition 2.2.3), which just satisfy additional axioms. In particular, this means that $\phi$ can see O’s strategy $\gamma : \Gamma$ on the domain $\Gamma$ only gradually and often incompletely via plays; i.e., $\gamma$ is not directly visible to $\phi$ . In this way, our approach retains the intensionality of standard game semantics.

1. (1) The copy-cat $\mathrm{cp}_{|\Gamma|}$ is a well-bracketed strategy on the linear implication $\Gamma \multimap \Gamma$ , and it is winning if $\Gamma$ is well-founded;

2. (2) The dereliction $\mathrm{der}_{|\Delta|}$ is a well-bracketed strategy on the implication $\Delta \Rightarrow \Delta$ , and it is winning if $\Delta$ is well-founded.

We only show $(\overline{\mathrm{cp}_{|\Gamma|}})_{|\Gamma|^{|\Gamma|}} \preccurlyeq \Gamma^\Gamma(\mathrm{cp}_{|\Gamma|})$ because it is the only nontrivial point. We do it by induction on the lengths of positions. The base case and the inductive step on odd-length positions are trivial. For the other inductive step, assume $\boldsymbol{t}lr \in \mathrm{cp}_{|\Gamma|}$ and $\boldsymbol{t}l \in (\overline{\mathrm{cp}_{|\Gamma|}})_{|\Gamma|^{|\Gamma|}} \cap \Gamma^\Gamma(\mathrm{cp}_{|\Gamma|})$ ; we have to show $\boldsymbol{t}lr \in \Gamma^\Gamma(\mathrm{cp}_{|\Gamma|})$ . Then, by $\boldsymbol{t}l \in \Gamma^\Gamma(\mathrm{cp}_{|\Gamma|})$ and $\boldsymbol{t}lr \in \mathrm{cp}_{|\Gamma|}$ , we see that $\boldsymbol{t}lr$ satisfies the inductive condition for $\boldsymbol{t}lr \in \Gamma^\Gamma(\mathrm{cp}_{|\Gamma|})$ .

The same induction shows that $\phi \otimes \sigma$ is total if so are $\phi$ and $\sigma$ , and Lemma 2.3.7 proves that $\phi \otimes \sigma$ is innocent (respectively, noetherian and well-bracketed) if so are $\phi$ and $\sigma$ .

We next verify $\psi \circ \phi : \Gamma \multimap \Theta$ , for which it suffices to prove $(\overline{\psi \circ \phi})_{|\Theta|^{|\Gamma|}} \preccurlyeq \Theta^\Gamma(\psi \circ \phi)$ . Again, we do it by induction on the lengths of positions; the base case and inductive step on odd-length positions are again trivial. For the remaining inductive step, assume $\boldsymbol{t}lr \in \psi \circ \phi$ and $\boldsymbol{t}l \in (\overline{\psi \circ \phi})_{|\Theta|^{|\Gamma|}} \cap (\Theta)^{\Gamma }(\psi \circ \phi)$ ; we have to show $\boldsymbol{t}lr \in (\Theta)^{\Gamma }(\psi \circ \phi)$ . Similarly to the case of tensor, fix $\gamma : \Gamma$ with $\boldsymbol{t}l \in \Theta(\psi \circ \phi \circ \gamma)^{\overline{\gamma}_\Gamma}$ ; it suffices to show $\boldsymbol{t}lr \in \Theta(\psi \circ \phi \circ \gamma)^{\overline{\gamma}_\Gamma}$ . Let l be in $\Gamma$ ; the other case is analogous. We have $\boldsymbol{t}l = (\boldsymbol{w} \upharpoonright |\Gamma|, |\Theta|) . l$ for unique $\boldsymbol{w} \in \phi \parallel \psi$ (Definition 2.3.6) by the covering lemma (Abramsky Reference Abramsky1997, p. 12). The computation of $\phi \parallel \psi$ on $\boldsymbol{w}l$ produces r after playing a finite part $\boldsymbol{u}$ of a position in the intermediate game $\mathrm{Pref}(\mathrm{cp}_{|\Delta|})$ (Abramsky Reference Abramsky1997, p. 11). Crucially, $\phi : \Delta^\Gamma$ and $\psi : \Theta^\Delta$ imply by induction that $\boldsymbol{u}$ is a suffix of a position in $(\overline{\mathrm{cp}_{|\Delta|}})_{\Delta(\phi \circ \gamma)^{\Delta(\phi \circ \gamma)}}$ .^{Footnote 15} This shows $\boldsymbol{t}lr \in \Theta(\psi \circ \phi \circ \gamma)^{\overline{\gamma}_\Gamma}$ .

Finally, the same inductive argument, combined with the proof of Lemma 2.3.7, verifies that $\psi \circ \phi$ is winning if so are $\phi$ and $\psi$ , and it trivially follows from Lemma 2.3.7 that $\psi \circ \phi$ is well-bracketed if so are $\phi$ and $\sigma$ .

We are now ready to summarise the present section:

• • Well-opened p-games as objects;

• • Strategies on the implication $\Gamma \Rightarrow \Delta$ as morphisms $\Gamma \rightarrow \Delta$ ;

• • The composition $\psi \bullet \phi := \psi \circ \phi^\dagger : \Gamma \Rightarrow \Theta$ of strategies as the composition of morphisms $\phi : \Gamma \rightarrow \Delta$ and $\psi : \Delta \rightarrow \Theta$ ;

• • The dereliction $\mathrm{der}_{|\Gamma|} : \Gamma \Rightarrow \Gamma$ as the identity $\mathrm{id}_\Gamma$ on each object $\Gamma$ .

The subcategory $\mathbb{LPG}_{\mathrm{!}}$ (respectively, $\mathbb{WPG}_{\mathrm{!}}$ ) of $\mathbb{PG}_{\mathrm{!}}$ consists of well-founded, well-opened p-games and winning (respectively, winning, well-bracketed) strategies.

Just like games in Definition 2.3.8, p-games in $\mathbb{PG}_{\mathrm{!}}$ (respectively, $\mathbb{LPG}_{\mathrm{!}}$ and $\mathbb{WPG}_{\mathrm{!}}$ ) are well-opened (respectively, well-founded and well-opened) for the identities to be well-defined.

However, our game semantics of MLTT (Section 4) together with these six categories implies that some combinations of dependent types and linearity/effects are already there in game semantics. We leave it as future work to study such combinations.

Notation 3.2.13 Let us write $\mathbb{PG}_{\mathrm{!}}(\Gamma)$ , $\mathbb{LPG}_{\mathrm{!}}(\Gamma)$ and $\mathbb{WPG}_{\mathrm{!}}(\Gamma)$ for the hom-sets $\mathbb{PG}_{\mathrm{!}}(T, \Gamma)$ , $\mathbb{LPG}_{\mathrm{!}}(T, \Gamma)$ and $\mathbb{WPG}_{\mathrm{!}}(T, \Gamma)$ , respectively, for each object $\Gamma$ , and identify $\Gamma$ with $\mathbb{PG}_{\mathrm{!}}(\Gamma)$ . Thus, e.g., we say that $\gamma : \Gamma$ is winning and well-bracketed if $\gamma \in \mathbb{WPG}_{\mathrm{!}}(\Gamma)$ .

Finally, let us show a categorically pleasing feature of p-games, where we focus on the category $\mathbb{WPG}_{\mathrm{!}}$ . First, we define an equivalence relation $\simeq$ between morphisms $\phi, \phi' : \Gamma \rightarrow \Delta$ by $\phi \simeq \phi' :\Leftrightarrow \phi \bullet \gamma = \phi' \bullet \gamma : \Delta$ for all $\gamma \in \mathbb{WPG}_{\mathrm{!}}(\Gamma)$ ; i.e., $\phi \simeq \phi'$ if $\phi$ and $\phi'$ are extensionally equal. Next, we define a category $\mathbb{WPG}_{\mathrm{!}}^{\simeq}$ out of $\mathbb{WPG}_{\mathrm{!}}$ , in which objects are those of $\mathbb{WPG}_{\mathrm{!}}$ , and morphisms $\Gamma \rightarrow \Delta$ are the equivalence classes $[\phi]$ of morphisms $\phi : \Gamma \rightarrow \Delta$ in $\mathbb{WPG}_{\mathrm{!}}$ with respect to $\simeq$ . The composition of morphisms $[\phi] : \Gamma \rightarrow \Delta$ and $[\psi] : \Delta \rightarrow \Theta$ in $\mathbb{WPG}_{\mathrm{!}}^{\simeq}$ is given by $[\psi] \bullet [\phi] := [\psi \bullet \phi]$ , and the identities in $\mathbb{WPG}_{\mathrm{!}}^{\simeq}$ by $\mathrm{id}_\Gamma := [\mathrm{der}_{|\Gamma|}]$ for all $\Gamma \in \mathbb{WPG}_{\mathrm{!}}^{\simeq}$ . We leave it to the reader to check that $\mathbb{WPG}_{\mathrm{!}}^{\simeq}$ forms a cartesian closed category. Then:

Next, given an object $\Theta'$ and a morphism $[\varphi] : \Theta' \rightarrow \Gamma$ such that $[\phi_1] \bullet [\varphi] = [\phi_2] \bullet [\varphi]$ , we clearly have $[\varphi] : \Theta' \rightarrow \Theta$ and $[\mathrm{der}_{|\Theta|}] \bullet [\varphi] = [\varphi]$ , where we leave the details to the reader.

Then, if another morphism $[\varphi'] : \Theta' \rightarrow \Theta$ also satisfies $[\mathrm{der}_{|\Theta|}] \bullet [\varphi'] = [\varphi]$ , then $[\varphi'] = [\mathrm{der}_{|\Theta|}] \bullet [\varphi'] = [\varphi]$ . We have shown the universal property of the pair $(\Theta, [\mathrm{der}_{|\Theta|}])$ .

Finally, the category $\mathbb{WPG}_{\mathrm{!}}^{\simeq}$ gives rise to a locally cartesian closed category in the same way as the category of sets and functions.

The quotient of morphisms with respect to $\simeq$ in the category $\mathbb{WPG}_{\mathrm{!}}^{\simeq}$ is for Corollary 3.2.14 because there is no equaliser of the strategies $\underline{0}, \underline{1} : N \rightrightarrows N$ in the category $\mathbb{WPG}_{\mathrm{!}}$ .

This categorical structure is novel. For instance, if we apply the proof of Corollary 3.2.14 to morphisms $[\kappa_{\underline{0}}], [\mathbin{\geqslant}] : N \mathbin{\&} N \rightrightarrows N$ in the category $\mathbb{WPG}_{\mathrm{!}}^{\simeq}$ such that $\kappa_{\underline{0}}$ is any strategy with $\kappa_{\underline{0}} \bullet \sigma = \underline{0}$ for all $\sigma : N \mathbin{\&} N$ , and $\geqslant$ is any strategy such that $\mathbin{\geqslant} \bullet \mathbin{\langle \underline{k}, \underline{n} \rangle} = \underline{0}$ if and only if $k \geqslant n$ for all $k, n \in \mathbb{N}$ , then their equaliser is the p-game that interprets the Sigma type $\Sigma_\mathrm{{x:N}N_b(x)}$ (see the beginning of Section 3). Thus, this construction is impossible for games.

Finally, recall that locally cartesian closed categories are the categorical semantics of extensional MLTT (Clairambault and Dybjer Reference Clairambault and Dybjer2014; Seely Reference Seely1984). Therefore, the category $\mathbb{WPG}_{\mathrm{!}}^{\simeq}$ provides game semantics of extensional MLTT. Let us emphasise, however, that our main result is game semantics of intensional MLTT in the category $\mathbb{WPG}_{\mathrm{!}}$ that does not satisfy equality reflection (Section 4.6), where recall that extensional MLTT is obtained from the intensional one by adding equality reflection. Corollary 3.2.14 exhibits the difference between the two variants of MLTT in terms of game semantics: the extensional quotient $\simeq$ .

4.1 Dependent predicate games

First, we interpret dependent types by well-opened, well-founded dependent p-games:

• • A linearly dependent p-game L is well-opened (respectively, well-founded) if so is the underlying game $|L|$ ;

• • The extension of the family $\| L \|$ is the family $L^\star = \{ L^\star(\gamma) \}_{\gamma : \Gamma}$ of p-games $L^\star(\gamma)$ defined by

  

• • A dependent predicate (p-) game over $\Gamma$ is a linearly dependent p-game over the exponential ${\mathrm{!}} \Gamma$ .

Notation 4.1.2. We write $\mathscr{D}_\ell(\Gamma)$ (respectively, $\mathscr{D}_\ell^{\mathrm{w}}(\Gamma)$ ) for the set of all linearly dependent p-games (respectively, well-opened, well-founded ones) over a p-game $\Gamma$ , and $\{ \Gamma' \}_\Gamma$ or $\{ \Gamma' \}$ for the constant one at $\Gamma'$ , i.e., $\{ \Gamma' \}_\Gamma := (\Gamma', (\gamma : \Gamma) \mapsto \Gamma')$ . We define $\mathscr{D}(\Gamma) := \mathscr{D}_\ell({\mathrm{!}} \Gamma)$ and $\mathscr{D}^{\mathrm{w}}(\Gamma) := \mathscr{D}^{\mathrm{w}}_\ell({\mathrm{!}} \Gamma)$ . We write $\gamma_0^\dagger$ for an element of the set $\mathbb{WPG}_{\mathrm{!}}({\mathrm{!}} \Gamma)$ , where $\gamma_0 \in \mathbb{WPG}_{\mathrm{!}}(\Gamma)$ , because it is innocent, thence the promotion of an element of the set $\mathbb{WPG}_{\mathrm{!}}(\Gamma)$ .

Let us explain Definition 4.1.1 as follows. Yamada (Reference Yamada2022) defines p-games $\mathcal{U}$ that interpret universes (Martin-Löf Reference Martin-Löf1975) and encodes well-opened, well-founded dependent p-games A over a p-game $\Gamma$ by morphisms $\phi_A : \Gamma \rightarrow \mathcal{U}$ in the category $\mathbb{WPG}_{\mathrm{!}}$ . Therefore, the family $\|A\|$ looks like the map $(\gamma : {\mathrm{!}} \Gamma) \mapsto \mathrm{El}(\phi_A \circ \gamma)$ , where $\mathrm{El}(\mu) \in \mathbb{WPG}_{\mathrm{!}}$ is the p-game encoded by an element $\mu \in \mathbb{WPG}_{\mathrm{!}}(\mathcal{U})$ . However, $\phi_A \circ \gamma$ can be invalid as an encoding (i.e., $\phi_A \circ \gamma \not \in \mathbb{WPG}_{\mathrm{!}}(\mathcal{U})$ ), e.g., when $\phi_A \circ \gamma$ is partial, where $A(\gamma) = \mathrm{El}(\phi_A \circ \gamma)$ is undefined. This suggests us to restrict the domain of $\|A\|$ to the set $\mathbb{WPG}_{\mathrm{!}}({\mathrm{!}} \Gamma)$ , so that $\mathrm{El}(\phi_A \bullet \gamma_0) \in \mathbb{WPG}_{\mathrm{!}}$ for all $\gamma_0^\dagger \in \mathbb{WPG}_{\mathrm{!}}({\mathrm{!}} \Gamma)$ . Then, $\| A \|$ is trivially continuous as elements of $\mathbb{WPG}_{\mathrm{!}}({\mathrm{!}} \Gamma)$ are all total.^{Footnote 16}

Then, we also need the ambient game $|A|$ . For instance, if $A = \{ N \}_{{\mathrm{!}} 0}$ , then the family $\|A\|$ is empty (since $\mathbb{WPG}_{\mathrm{!}}({\mathrm{!}} 0) = \emptyset$ ), so $\| A \|$ cannot retain the natural number p-game N. Here, note that the constant one $\{ N \}_{{\mathrm{!}} 0}$ is intended to be essentially the same as N. We address this problem by adding the underlying game $|A|$ and extending $\|A\|$ to $A^\star$ .

Example 4.1.3 Let us slightly modify the examples $\mathrm{List}_N, N_b \in \mathscr{D}^{\mathrm{w}}(N)$ presented at the beginning of Section 3 by

and

4.2 Pi on dependent predicate games

We next interpret Pi types. Our idea is best explained by the naive set-theoretic semantics as follows. Recall first that the set-theoretic semantics interprets a simple type C and a term x : C as a set C and an element $x \in C$ , respectively, and a dependent type D over C as a family $D = \{ D(x) \}_{x \in C}$ of sets D(x). Then, given a dependent type $\mathrm{x : C} \vdash \mathrm{D(x) \ type}$ , the set-theoretic semantics interprets the Pi type $\Pi_\mathrm{{x:C}D(x)}$ as the set of all maps f from the set C to the union $\bigcup_{x : C} D(x)$ such that $f(x) \in D(x)$ for all $x \in C$ , called dependent maps from C to D. Hence, in light of implication between p-games (Definition 3.2.6), it is now clear how to interpret Pi types. We interpret them by:

Definition 4.2.1 (linear-Pi and Pi). Let L be a linearly dependent p-game over a p-game $\Gamma$ , and A a dependent p-game over $\Gamma$ . The linear-Pi from $\Gamma$ to L is the p-game $\Pi_\ell (\Gamma, L)$ defined by $|\Pi_\ell (\Gamma, L)| := |L|^{|\Gamma|}$ and for all $\phi : |\Pi_\ell (\Gamma, L)|$

\begin{align*}\Pi_\ell (\Gamma, L)(\phi) &:= \{ \boldsymbol{\epsilon} \} \cup \{ \, \boldsymbol{s}m \in |\Pi_\ell (\Gamma, L)|^{\mathrm{Odd}} \mid \boldsymbol{s} \in \Pi_\ell (\Gamma, L)(\phi), \exists \gamma : \Gamma . \, \boldsymbol{s}m \in L^\star(\gamma)(\phi \circ \gamma)^{\overline{\gamma}_\Gamma} \, \} \\&\cup \{ \, \boldsymbol{t}lr \in |\Pi_\ell (\Gamma, L)|^{\mathrm{Even}} \mid \boldsymbol{t}l \in \Pi_\ell (\Gamma, L)(\phi), \forall \gamma : \Gamma . \, \boldsymbol{t}l \in L^\star(\gamma)(\phi \circ \gamma)^{\overline{\gamma}_\Gamma} \\ &\Rightarrow \boldsymbol{t}lr \in L^\star(\gamma)(\phi \circ \gamma)^{\overline{\gamma}_\Gamma} \, \},\end{align*}

and the Pi from $\Gamma$ to A is the linear-Pi

\begin{equation*}\Pi (\Gamma, A) := \Pi_\ell({\mathrm{!}} \Gamma, A).\end{equation*}

The idea of linear-Pi is that it is linear implication except that it additionally satisfies type dependency. Specifically, the type dependency means that the codomain of a linear-Pi $\Pi_\ell (\Gamma, L)$ is the p-game $L(\gamma)$ if the strategy $\gamma : \Gamma$ on the domain $\Gamma$ satisfies $\gamma \in \mathbb{WPG}_{\mathrm{!}}(\Gamma)$ , and the constant one $\mathscr{P}(|L|)$ otherwise. We then define Pi out of linear-Pi and exponential in the same way as we define implication out of linear implication and exponential.

Accordingly, it is no surprise that linear-Pi (respectively, Pi) generalises linear implication (respectively, implication): Given p-games $\Gamma$ and $\Gamma'$ , we have $\Pi_\ell (\Gamma, \{ \Gamma' \}_\Gamma) = \Gamma \multimap \Gamma'$ (respectively, $\Pi (\Gamma, \{ \Gamma' \}_{{\mathrm{!}} \Gamma}) = \Gamma \Rightarrow \Gamma'$ ).

Essentially the same proof as the one of Lemma 3.2.7 on linear implication shows:

This theorem also implies that, given a (well-opened, well-founded) dependent p-game A over a (well-opened, well-founded) p-game $\Gamma$ , the Pi $\Pi(\Gamma, A)$ is a (well-opened, well-founded) p-game. For an interpretation of MLTT, however, we have to lift Pi to the case where $\Gamma$ is also a dependent p-game. We address this problem in Section 4.5.1.

At this point, O can further play on $\Pi(N, \mathrm{List}_N)$ . For instance, O can make another move $q_{[k']}$ on the codomain such that $k \neq k'$ ; then, $\zeta$ again makes the move $q_{[0]}$ on the domain. If O answers it by $n'_{[0]}$ for any $n' \in \mathbb{N}_+$ , then $\zeta$ plays $0_{[k']}$ on the codomain. If $n \neq n'$ , $k > n$ or $k' > n$ , then $\zeta$ no longer has to play within the subgame $N \Rightarrow \mathrm{List}_N(\underline{n}^\dagger)$ . In contrast, if $n = n'$ , $k \leqslant n$ and $k' \leqslant n$ , then $\zeta$ still has to play on the subgame $N \Rightarrow \mathrm{List}_N(\underline{n}^\dagger)$ , and its computation still satisfies this condition. In this way, a play by $\zeta$ proceeds.

Let us emphasise that the input strategy $\gamma : {\mathrm{!}} N$ in the Pi $\Pi(N, \mathrm{List}_N)$ is only gradually and incompletely revealed by O during a play, which will never be complete.

4.3 Sigma on dependent predicate games

We next interpret Sigma types. Recall that the set-theoretic semantics interprets the Sigma type $\Sigma_\mathrm{{x:C}D(x)}$ on a dependent type $\mathrm{x : C} \vdash \mathrm{D(x) \ type}$ by the set of all pairs (c, d) with $c \in C$ and $d \in D(c)$ , called dependent pairs on C and D. Thus, we interpret Sigma types by:

The idea of a Sigma $\Sigma (\Gamma, A)$ is simply that strategies on $\Sigma (\Gamma, A)$ are the pairings $\langle \gamma, \alpha \rangle : |\Gamma| \mathbin{\&} |A|$ that satisfy $\gamma : \Gamma$ and $\alpha : A(\gamma^\dagger)$ whenever $\gamma \in \mathbb{WPG}_{\mathrm{!}}(\Gamma)$ . The second condition matches the constraint on the Pi $\Pi(\Gamma, A)$ as we see in Theorem 4.4.3 and Lemma 4.5.1.2.

When A is a constant dependent p-game $\{ \Gamma' \}_{{\mathrm{!}} \Gamma}$ , the Sigma $\Sigma (\Gamma, \{ \Gamma' \}_{{\mathrm{!}} \Gamma})$ coincides with the product $\Gamma \mathbin{\&} \Gamma'$ . In this sense, Sigma generalises product on p-games.

Let $\Gamma \in \mathbb{WPG}_{\mathrm{!}}$ and $A \in \mathscr{D}^{\mathrm{w}}(\Gamma)$ . The Sigma $\Sigma(\Gamma, A) \in \mathbb{WPG}_{\mathrm{!}}$ achieves the following highly nontrivial point. First, the categorical view on semantics of MLTT (Definition 4.4.1) tells us that there must be a bijection between strategies $\psi \in \mathbb{WPG}_{\mathrm{!}}(\Delta, \Sigma(\Gamma, A))$ and pairs of strategies $\phi \in \mathbb{WPG}_{\mathrm{!}}(\Delta, \Gamma)$ and , where the dependent p-game $A\{ \phi \} \in \mathscr{D}^{\mathrm{w}}(\Delta)$ is defined by $|A\{ \phi \}| := |A|$ and $A\{\phi\}(\delta) := A(\phi^\dagger \circ \delta)$ ( $\delta \in \mathbb{WPG}_{\mathrm{!}}({\mathrm{!}} \Delta)$ ). Next, recall that the underlying game of the codomain $A\{\phi\}$ of $\Pi(\Delta, A\{\phi\})$ is gradually revealed along the gradual specification of a strategy $\delta$ on the domain ${\mathrm{!}} \Delta$ . Nevertheless, since the Sigma $\Sigma(\Gamma, A)$ does not refer to $\Delta$ , unlike the Pi $\Pi(\Delta, A\{\phi\})$ , the challenge is to define $\Sigma(\Gamma, A)$ in such a way that strategies $\psi \in \mathbb{WPG}_{\mathrm{!}}(\Delta, \Sigma(\Gamma, A))$ attain the bijection.^{Footnote 17} Then, our definition of $\Sigma(\Gamma, A)$ meets this nontrivial requirement (Theorem 4.4.3).

The pairing $\langle \underline{k}, \underline{n_1} \otimes \underline{n_2} \otimes \dots \otimes \underline{n_k} \rangle$ for any $k, n_1, n_2, \dots, n_k \in \mathbb{N}$ is winning (and well-bracketed) on the Sigma $\Sigma(N, \mathrm{List}_N)$ because the choice of a strategy in a p-game can control odd-length positions (as illustrated at the beginning of Section 3). Moreover, given a morphism $\phi : \Sigma(N, \mathrm{List}_N) \rightarrow \Delta$ in the category $\mathbb{WPG}_{\mathrm{!}}$ , the composition

\begin{equation*}T \stackrel{\langle \underline{k}, \underline{n_1} \otimes \underline{n_2} \otimes \dots \otimes \underline{n_k} \rangle}{\longrightarrow} \Sigma(N, \mathrm{List}_N) \stackrel{\phi}{\rightarrow} \Delta\end{equation*}

is a well-defined morphism in $\mathbb{WPG}_{\mathrm{!}}$ , which is in particular a winning strategy (Lemma 2.9).

In contrast, the list $(\underline{k}, \underline{n_1} \otimes \underline{n_2} \otimes \dots \otimes \underline{n_k})$ is partial on the list $(N, \mathrm{List}_N)$ in Abramsky et al. (Reference Abramsky, Jagadeesan and Vákár2015), Vákár et al. (Reference Vákár, Jagadeesan and Abramsky2018), where we regard the p-game N and the components of the dependent p-game $\mathrm{List}_N$ as games in the evident way, since there is no way in their method to prevent O from playing arbitrarily on the ambient game $|\mathrm{List}_N|$ . For instance, the pair $(\underline{0}, \top)$ is partial on the pair $(N, \mathrm{List}_N)$ . For this problem, they instead take the lists $(\underline{k}, \tau)$ of winning strategies $\underline{k} : N$ and $\tau : |\mathrm{List}_N|$ . However, the second one $\tau$ is redundant because it is total on $|\mathrm{List}_N|$ ; e.g., the pair $(\underline{0}, \top)$ is replaced with any pair $(\underline{0}, \underline{n_1} \otimes \underline{n_2} \otimes \cdots)$ such that $n_i \in \mathbb{N}$ for all $i \in \mathbb{N}$ in their approach, where $\underline{n_1} \otimes \underline{n_2} \otimes \cdots$ is an infinite iteration of tensor, but clearly neither of them is canonical. Consequently, this approach cannot properly interpret the Sigma type $\Sigma_\mathrm{{x:N} List_N(x)}$ .

More generally, Abramsky et al. use the O-sat operation (Vákár et al. Reference Vákár, Jagadeesan and Abramsky2018, Remark 4.5 and Theorem 5.6), which allows O to ignore the type dependencies of Pi and Sigma types, and impose winning on strategies against such unrestricted plays by O. However, this method generates a significant gap between their semantics and MLTT since terms $\vdash \langle \mathrm{a, b} \rangle : \Sigma\mathrm{(A, B)}$ satisfy $\vdash \mathrm{a : A}$ and $\vdash \mathrm{b : B(a)}$ , not $\mathrm{x : A} \vdash \mathrm{b : B(x)}$ . Then, how does their full completeness theorem hold? The answer is that they focus on a specific class of finite inductive types (Vákár et al. Reference Vákár, Jagadeesan and Abramsky2018, Figure 7) for which the problem disappears. As we have just seen, however, their method is unsuited for more standard types such as List_N, which is generated by the elimination rule of the N type in the presence of a universe.

In summary, the novel mathematical structure of p-games enables us to not only dispense with the formal, inductive list construction on games and strategies in Abramsky et al. (Reference Abramsky, Jagadeesan and Vákár2015), Vákár et al. (Reference Vákár, Jagadeesan and Abramsky2018) but also accurately interpret Pi and Sigma types.

Finally, recall that the interpretation of Sigma types given by Blot and Laird (Reference Blot and Laird2018) does not preserve the additive nature of product on games (Section 1.4). In contrast, our Sigma inherits the additive nature. The additive nature requires a play in $\Sigma(\Gamma, A)$ to be either a play in $\Gamma$ or A, but then we must specify the constraint on plays in A for $\Sigma(\Gamma, A)$ even without playing on $\Gamma$ at all. This is one of our main achievements.

Again, however, this construction of Sigma is not general enough for the same reason as the case of Pi (Section 4.2); we generalise Sigma in Section 4.5.2.

4.4 A game-semantic category with families

We are now ready to present our game-semantic CwF. Let us first recall the general definition of CwFs introduced by Dybjer (Reference Dybjer1996):

• • $\mathcal{C}$ is a category with a terminal object $T \in \mathcal{C}$ ;

• • Ty assigns, to each object $\Gamma \in \mathcal{C}$ , a set $\mathrm{Ty}(\Gamma)$ of types in the context $\Gamma$ ;

• • Tm assigns, to each pair $(\Gamma, A)$ of an object $\Gamma \in \mathcal{C}$ and a type $A \in \mathrm{Ty}(\Gamma)$ , a set $\mathrm{Tm}(\Gamma, A)$ of terms of type A in the context $\Gamma$ ;

• • $\_\{\_\}$ assigns, to each morphism $\phi : \Delta \to \Gamma$ in $\mathcal{C}$ , a map $\_\{\phi\} : \mathrm{Ty}(\Gamma) \to \mathrm{Ty}(\Delta)$ , called the substitution on types, and a family $\{ \_\{\phi\}_A \}_{A \in \mathrm{Ty}(\Gamma)}$ of maps $\_\{\phi\}_A : \mathrm{Tm}(\Gamma, A) \to \mathrm{Tm}(\Delta, A\{\phi\})$ , called the substitution on terms;

• • $\_ . \_$ assigns, to each pair $(\Gamma, A)$ of a context $\Gamma \in \mathcal{C}$ and a type $A \in \mathrm{Ty}(\Gamma)$ , a context $\Gamma . A \in \mathcal{C}$ , called the comprehension of A;

• • p (respectively, v) associates each pair $(\Gamma, A)$ of a context $\Gamma \in \mathcal{C}$ and a type $A \in \mathrm{Ty}(\Gamma)$ with a morphism $\mathrm{p}_A : \Gamma . A \to \Gamma$ in $\mathcal{C}$ (respectively, a term $\mathrm{v}_A \in \mathrm{Tm}(\Gamma . A, A\{\mathrm{p}_A\})$ ), called the first projection on A (respectively, the second projection on A);

• • $\langle \_, \_ \rangle_\_$ associates each triple of a morphism $\phi : \Delta \to \Gamma$ in $\mathcal{C}$ , a type $A \in \mathrm{Ty}(\Gamma)$ and a term with a morphism in $\mathcal{C}$ , called the extension of $\phi$ by ,

that satisfies, for any object $\Theta \in \mathcal{C}$ , morphism $\varphi : \Theta \to \Delta$ in $\mathcal{C}$ and term $\alpha \in \mathrm{Tm}(\Gamma, A)$ ,

• • (Ty-Id) $A \{ \mathrm{id}_\Gamma \} = A$ ;

• • (Ty-Comp) $A \{ \phi \circ \varphi \} = A \{ \phi \} \{ \varphi \}$ ;

• • (Tm-Id) $\alpha \{ \mathrm{id}_\Gamma \}_A = \alpha$ ;

• • (Tm-Comp) $\alpha \{ \phi \circ \varphi \}_A = \alpha \{ \phi \}_A \{ \varphi \}_{A\{\phi\}}$ ;

• • (Cons-L) ;

• • (Cons-R) ;

• • (Cons-Nat) ;

• • (Cons-Id) $\langle \mathrm{p}_A, \mathrm{v}_A \rangle_A = \mathrm{id}_{\Gamma . A}$ .

Roughly, judgements of MLTT are interpreted in a CwF $\mathcal{C}$ by

where denotes the semantic map or interpretation. See Hofmann (Reference Hofmann1997) for the details.

Let us now turn to our game-semantic CwF:

• • The category $\mathbb{WPG}_{\mathrm{!}}$ is given in Definition 3.2.10, and $T \in \mathbb{WPG}_{\mathrm{!}}$ in Example 3.1.5;

• • $\mathrm{Ty}(\Gamma) := \mathscr{D}^{\mathrm{w}}(\Gamma)$ ( $\Gamma \in \mathbb{WPG}_{\mathrm{!}}$ ) and $\mathrm{Tm}(\Gamma, A) := \mathbb{WPG}_{\mathrm{!}}(\Pi(\Gamma, A))$ ( $A \in \mathscr{D}^{\mathrm{w}}(\Gamma)$ );

• • Given $\phi : \Delta \rightarrow \Gamma$ in $\mathbb{WPG}_{\mathrm{!}}$ , the map $\_\{\phi\} : \mathrm{Ty}(\Gamma) \to \mathrm{Ty}(\Delta)$ is given by $|A\{ \phi \}| := |A|$ and $A \{ \phi \}(\delta_0^\dagger) := A(\phi^\dagger \bullet \delta_0)$ for all $A \in \mathrm{Ty}(\Gamma)$ and $\delta_0^\dagger \in \mathbb{WPG}_{\mathrm{!}}({\mathrm{!}} \Delta)$ , and the map $\_\{\phi\}_A : \mathrm{Tm}(\Gamma, A) \to \mathrm{Tm}(\Delta, A\{\phi\})$ by $\alpha \{ \phi \}_A := \alpha \bullet \phi$ for all $\alpha \in \mathrm{Tm}(\Gamma, A)$ ;

• • $\Gamma.A := \Sigma (\Gamma, A)$ , $\mathrm{p}_A := \mathrm{der}_{|\Gamma|} : \Sigma (\Gamma, A) \rightarrow \Gamma$ , $\mathrm{v}_A := \mathrm{der}_{|A|} : \Pi (\Sigma(\Gamma, A), A\{\mathrm{p}_A\})$ and, given , .

Given $\Gamma \in \mathbb{WPG}_{\mathrm{!}}$ and $A \in \mathscr{D}^{\mathrm{w}}(\Gamma)$ , we write $\mathbb{WPG}_{\mathrm{!}}(\Gamma, A)$ for the set $\mathrm{Tm}(\Gamma, A)$ of all terms from $\Gamma$ to A. We often omit the subscripts on components of $\mathbb{WPG}_{\mathrm{!}}$ when they are evident.

On the substitution $\alpha \{ \phi \} = \alpha \bullet \phi \in \mathbb{WPG}_{\mathrm{!}}(|\Delta|, |A|)$ ,^{Footnote 18} we see by induction on the lengths of positions that $(\overline{\alpha \{ \phi \}})_{|\Pi(\Delta, A\{ \phi \})|} \preccurlyeq \Pi(\Delta, A\{ \phi \})(\alpha \{ \phi \})$ follows from $\phi \in \mathbb{WPG}_{\mathrm{!}}(\Delta, \Gamma)$ and $\alpha \in \mathbb{WPG}_{\mathrm{!}}(\Gamma, A)$ . Besides, the same induction also shows that $\alpha\{\phi\} \cap \Pi(\Delta, A\{ \phi \})(\alpha \{ \phi \}) : \Pi(\Delta, A\{ \phi \})(\alpha \{ \phi \})$ is winning and well-bracketed, proving $\alpha \{ \phi \} \in \mathbb{WPG}_{\mathrm{!}}(\Delta, A\{ \phi \})$ .

The same induction proves $\mathrm{v}_A = \mathrm{der}_{|A|} \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Gamma, A), A\{\mathrm{p}_A\})$ , where a crucial point is that the Pi $\Pi(\Gamma, A)$ and the Sigma $\Sigma(\Gamma, A)$ are defined by the same family $A^\star$ .

On the extension , the same induction shows that follows from $\phi \in \mathbb{WPG}_{\mathrm{!}}(\Delta, \Gamma)$ and , where the fixed strategy $\phi$ in plays a crucial role even if a play in $\Pi(\Delta, \Sigma(\Gamma, A))$ starts in A.