Game semantics of Martin-Löf type theory

Abstract

This work presents game semantics of Martin-Löf type theory (MLTT) equipped with the One, the Zero, the N, Pi, Sigma and Id types. Game semantics interprets a wide range of logic and computation, even the polymorphic $\lambda$-calculus; however, it has remained a well-known challenge in the past 25 years to achieve game semantics of dependent type theories such as MLTT, and past attempts lack directness or generality. For instance, the approach taken by Abramsky et al. interprets Sigma types indirectly by formal lists, not by games, making an interpretation of universes hopeless, and it is limited to a very specific class of dependent types. The difficulty of this challenge comes from a conflict between the extensionality of dependent types and the intensionality of game semantics. We overcome the challenge by inventing a novel variant of games, while we keep strategies unchanged, in such a way that this variant inherits the strong points of conventional game semantics. Also, our method enables an interpretation of subtyping on dependent types for the first time as game semantics. We finally give a new, game-semantic proof of the independence of Markov’s principle from MLTT. This proof illustrates an advantage of our intensional model over extensional ones such as Hyland’s effective topos.

1. Introduction

1.1 Martin-Löf type theory and the meaning explanation

Martin-Löf type theory (MLTT) (Martin-Löf 1975, 1982, 1984, 1998) is one of the best-known formal systems for constructive mathematics (Troelstra and van Dalen 1988), which is comparable to axiomatic set theory (Fraenkel 1922; Zermelo 1908) for classical mathematics. MLTT is also a functional programming language (Martin-Löf 1982) that generalises the simply typed lambda-calculus (STLC) (Church 1940) along the generalisation of (intuitionistic) propositional logic to higher-order (intuitionistic) predicate logic and constructive mathematics under the Curry–Howard isomorphisms (Girard et al. 1989; Sørensen and Urzyczyn 2006). By this computational nature, MLTT and similar formal systems underlie computer formalisations of mathematics and their applications to programming (Constable et al. 1986; Univalent Foundations Program 2013).

Just like axiomatic set theory is explained informally by sets, the conceptual foundation of MLTT is computations in an informal sense. That is, the fundamental idea of MLTT is to regard objects (such as numbers) and proofs in constructive mathematics uniformly as computations, and MLTT is a syntactic formalisation of this foundational idea (Martin-Löf 1982). Hence, objects and proofs in MLTT are unified into terms, where formulas are called types. This standard yet informal semantics of MLTT that interprets terms by computations is called the meaning explanation (Dybjer and Palmgren 2016, Section 5).

Nevertheless, by its informal nature, the meaning explanation cannot serve as a mathematically rigorous ground to analyse, justify or develop MLTT. Moreover, MLTT is an intricate formal system that inevitably contains superficial syntactic details, which makes it difficult to study the meta-theory of MLTT such as consistency and independence.

This problem calls for mathematical semantics (Scott 1970; Tarski 1954) of MLTT, i.e., a precise interpretation of syntactic objects in MLTT by mathematical objects, that faithfully formalises the meaning explanation, abstracts the inessential syntactic details of MLTT and advances the meta-theoretic study of MLTT.

1.2 Game semantics

Game semantics (Abramsky and Jagadeesan 1994; Abramsky et al. 2000; Hyland and Ong 2000; Nickau 1994) is a class of mathematical semantics of logic and computation that interprets types and terms by games and strategies, respectively.

Its strong point is its conceptual naturality: ‘Logic is the study of reasoning’ (Shoenfield 1967, p. 1), where one can regard ‘reasoning’ as dialogical arguments between Player (or a mathematician) and Opponent (or an oracle), and game semantics formalises this intuitive idea. Moreover, this game-semantic view is in harmony with the meaning explanation since dialogical arguments are a certain kind of computations.

Another strong advantage of game semantics is its precision in interpreting syntax as various full completeness/abstraction results (Curien 2007) in the literature have demonstrated. This precision is due to its distinguished intensionality: Game semantics interprets terms by strategies or intensional processes, while other mathematical semantics does it by extensional objects such as functions. Because terms are also intensional objects, computing in a step-by-step fashion, game semantics accomplishes a very tight correspondence between terms and strategies. This correspondence makes game semantics an exceptionally powerful tool for the study of logic and computation.

Finally, the concrete nature of game semantics enables its algorithmic applications to program analysis and verification; see Abramsky (2002).

1.3 Main results

To summarise the points so far: Mathematical semantics of MLTT that advances our understanding of MLTT, promotes its improvements and extensions, and/or clarifies its meta-theory is strongly desired, and game semantics appears to be perfect for this role by its conceptual naturality, harmony with the meaning explanation, precision in interpreting syntax and algorithmic applications. Moreover, game semantics interprets (computational) effects (Plotkin and Power 2004) and linear logic (Girard 1987) in a highly systematic fashion (see Abramsky and McCusker 1999b for the details); therefore, game semantics of MLTT, if any, may lead to MLTT combined with effects and/or linear typing.

However, although game semantics has interpreted a surprisingly wide range of logical and computational theories, even the polymorphic $\lambda$ -calculus (Abramsky and Jagadeesan 2005; Laird 2013), it has remained a well-known challenge to establish game semantics of dependent type theories (Hofmann 1997) such as MLTT. The main difficulty in achieving game semantics of MLTT is to interpret the extensional type dependency of Sigma types in terms of the intensional processes of game semantics; see the beginning of Section 3 for this point. In fact, this problem has been open for more than 25 years, and even today its definitive solution is yet to emerge though a few candidates have arisen recently (Abramsky et al. 2015; Blot and Laird 2018); see Section 1.4 for these past attempts.

Thus, we aim to provide another candidate for game semantics of MLTT with the hope that it sheds new light on this challenging problem. Motivated in this way, we prove:

Theorem (game semantics of MLTT, informally) There is new game semantics of MLTT with the One, the Zero, the N, Pi, Sigma and Id types (Sections 4.4–4.5 ).

Our key idea underlying this main theorem is to generalise games in such a way that they can interpret Sigma types, while we keep strategies unchanged, and retain the advantages of conventional game semantics such as intensionality (Section 1.2). See the beginning of Section 3 for the outline of this idea. Also, see Section 1.4 for the advantages of this method over the existing ones such as Abramsky et al. (2015), Vákár et al. (2018) and Blot and Laird (2018).

In addition, we also illustrate the utility of our game semantics by giving a new proof of the independence result shown by Mannaa and Coquand (2017):

Corollary (independence of Markov’s principle) Markov’s principle (Markov 1962 ) is independent from MLTT equipped with the types listed in the above theorem (Section 4.7 ).

The method of Mannaa and Coquand (2017) is syntactic. In contrast, our approach is game-semantic, and it provides a new, intuitive argument on why the independence holds. This corollary also illustrates an advantage of game semantics over other computational semantics since, e.g., the effective topos (Hyland 1982) cannot show the independence. Besides, by the non-inductive nature of game semantics, the present method will be easily applied to the independence of Markov’s principle from various extensions of MLTT.

Finally, the novel mathematical structure of our games enables for the first time:

Corollary (game semantics of dependent subtyping) The game semantics of MLTT of the above theorem interprets subtyping on dependent types (Section 4.8 ).

1.4 Related work and our contributions

Abramsky et al. (2015) and Vákár et al. (2018) have constructed game semantics of MLTT equipped with the One, Pi, Sigma, Id and finite inductive types. Its significance is that it is the first intensional semantics of MLTT, so it stands in sharp contrast with other computational semantics such as realisability (Streicher 2012) and domains (Palmgren and Stoltenberg-Hansen 1990) which are extensional. Their main result is a full completeness theorem. On the other hand, they only interpret Sigma types indirectly and inductively by a formal list construction and the adjunction between Pi and Sigma types. Specifically, they interpret a Sigma type $\vdash \Sigma_{\mathrm{x:C}}\mathrm{D(x)} \ \mathrm{type}$ ¹ by the list (C, D) of the game C that interprets the simple type $\vdash \mathrm{C} \ {\mathrm{type}}$ and the family $D= \{ D(x) \}_{x:C}$ of games D(x) indexed by strategies x on C that interprets the dependent type $\mathrm{x:C} \vdash \mathrm{D(x)} \ \mathrm{type}$ ; then, they interpret a term of the form $\vdash \langle \mathrm{c, d} \rangle : \Sigma_{\mathrm{{x:C}D(x)}}$ by the list (c, d) of strategies c and d that interpret the terms $\vdash \mathrm{c : C}$ and $\vdash \mathrm{d : D(c)}$ , respectively, and a term of the form $\mathrm{z} : \Sigma_\mathrm{{x:C}D(x)} \vdash \mathrm{e(z) : E(z)}$ by identifying it with another term $\mathrm{x : C, y : D(x)} \vdash \mathrm{e}(\langle \mathrm{x, y} \rangle) : E(\langle x, y \rangle)$ . In this way, they circumvent a direct interpretation of Sigma types. Consequently, they interpret types and terms by lists of (families of) games and strategies, respectively. This formal list method, however, merely simulates the term model of MLTT (Hofmann 1997, Section 2.4) and lowers the non-inductive nature of game semantics. Finally, for the winning of strategies, they use the O-sat operation (Vákár et al. 2018, Remark 4.5); however, this generates a significant gap between MLTT and their semantics, and it only works for a very specific class of finite inductive types (Vákár et al. 2018, Figure 7); see Section 4.3 for this point.

Another related work is the mathematical semantics of MLTT by Blot and Laird (2018) based on concrete data structures and sequential algorithms (Berry and Curien 1982). They model the Boolean, the N, Pi and Sigma types and a universe though their interpretation of the universe is not by game semantics but by domain theory. Their main results are full completeness/abstraction theorems. Notably, they directly interpret Sigma types without the formal list construction, overcoming the problem of the preceding work. It is fair to say, however, that this method, being based on concrete data structures and sequential algorithms, does not carry quantitative information of game semantics; i.e., it does not address the same problem as Abramsky et al. As a side note, it is possible to play on both sides of Blot and Laird’s interpretation of a Sigma type in a play, which is closer to the game semantics of multiplicative conjunction than that of additive one. On the other hand, their method admits classical reasoning, but the logical part of MLTT is intuitionistic; i.e., there is a gap between MLTT and their semantics. As a result, e.g., their semantics admits Markov’s principle. Further, they do not achieve the linear decomposition of function types or the characterisation of effects by constraints on strategies, which are flagship advantages of game semantics (Abramsky and McCusker 1999b). Finally, their interpretation of Id types by finite tuples of the Boolean type (Blot and Laird 2018, Section 9) does not work in the presence of the N type because the set $\mathbb{N}$ of all natural numbers is unbounded.

Hence, each of the existing game semantics of MLTT has pros and cons, and we have not reached a consensus on a definitive solution. In this context, the present work offers the third approach with the novel features listed below. We hope that it will eventually lead to a definitive solution in the future.

First, we give the first game semantics of both the N and Id types. The interpretation of these types enables us to show the independence of Markov’s principle from MLTT.

Second, our games are a modest generalisation of a standard variant given by McCusker (1998), and we interpret types and terms by these generalised games and (ordinary) strategies, not lists of them, respectively. Consequently, we retain the syntax-independence and the non-inductive nature of game semantics. Besides, we directly interpret Sigma types by our games, where a play occurs only in either side. Hence, we overcome the shortcomings of the preceding methods. For the idea behind our method, see the beginning of Section 3.

Third, our method inherits in principle the flagship advantages of game semantics such as the linear decomposition of function types and the characterisation of effects. Note, however, that the present work does not yet establish game semantics of a dependent type theory with linear decomposition or effects either; our approach only inherits the mathematical structure of McCusker (1998) that captures linear decomposition and effects. We leave it as future work to apply the present game semantics to solve these open problems.

Fourth, the novel mathematical structure of our games enables us to dispense with the O-sat operation in Abramsky et al. (2015), Vákár et al. (2018) so that one can interpret the type dependency of Pi and Sigma types accurately; see Section 4.3 for this point.

Finally, the mathematical structure of our games is novel. For instance, the category of our games (with a suitable quotient on strategies) has all finite limits (Corollary 3.2.14), while the category of existing games does not. Also, we achieve the first game semantics of subtyping on dependent types (Section 4.8). As a side note, to focus on the main idea of the present work, we leave it to Yamada (2022) to interpret universes (Martin-Löf 1975).

1.5 Concluding remarks

Due to the novel structure of our games, one might misunderstand that our game semantics is close to extensional semantics such as realisability and domain models. However, since our strategies are just the ordinary ones (Section 1.4), our approach inherits the advantages of standard game semantics such as intensionality (Section 1.2). In fact, the intensional features of the preceding game semantics (Abramsky et al. 2015, Section 1) are mostly valid in our game semantics (Section 4.6); e.g., both refute function extensionality. Also, our game semantics refutes Markov’s principle by its intensionality (Section 4.7), while the effective topos does not.

Last but not least, we do not show a full completeness theorem for the following reasons. First, the syntax of MLTT, specifically the N type, is not suited to fully complete game semantics. For instance, the full completeness theorems given by Abramsky et al. (2015), Vákár et al. (2018) are on modifications of MLTT which exclude the N type. However, our topic is MLTT itself (Section 1.1), so we leave a full completeness theorem on a modification of MLTT as future work. Second, our priority is more on semantics of the N type than full completeness without the N type since our motivation comes from foundations of mathematics (Section 1.1) for which the N type is crucial. Finally, one of our aims is to provide tools for the meta-theoretic study of MLTT (Section 1.1), but full completeness is not necessarily crucial for this aim. For example, the fully complete model of Blot and Laird (2018) cannot show the independence of Markov’s principle since it admits classical reasoning. Thus, we instead show the utility of our semantics by proving the independence result (Section 4.7).

1.6 The structure of the present article

The rest of this article proceeds as follows. We first recall McCusker’s games and strategies in Section 2 and generalise the games in Section 3. We then interpret MLTT by the generalised games and the strategies in Section 4, where we analyse the intensionality of our semantics in Section 4.6, give a new proof of the independence of Markov’s principle in Section 4.7, and interpret subtyping on dependent types in Section 4.8. We finally draw a conclusion and propose future work in Section 5.

2. Games and Strategies for Simple Type Theories

We first recall McCusker’s games and strategies for simple type theories (McCusker 1998), which the present work is based on. We select this variant for the following reasons. First, it inherits the strong points of both of the two best-known variants: the linear decomposition of function types (Girard 1987) accomplished by AJM-games (Abramsky et al. 2000) and the characterisation of effects by constraints on strategies (Abramsky and McCusker 1999b) that utilises pointers in HO-games (Hyland and Ong 2000) originally introduced by Coquand (1995). Our games inherit these advantages so that they will shed new light on the problem of combining MLTT and linear logic and/or effects. Second, pointers enable us to refine game semantics into a model of computation (Yamada 2019), which is highly desirable as a mathematical foundation of constructive mathematics (Section 1.1).

We assume that the reader is familiar with McCusker’s games and strategies, and leave more expositions and examples to the tutorial given by Abramsky and McCusker (1999b). We henceforth call McCusker’s games and strategies, respectively, games and strategies.

We first recall two preliminary concepts in Section 2.1, and then games and strategies in Section 2.2. We finally review standard constructions on games and strategies in Section 2.3.

Notation 2 0.1. We use the following notations throughout the present article:

• • We use bold small letters $\boldsymbol{s}, \boldsymbol{t}, \boldsymbol{u}, \boldsymbol{v}$ , etc. for sequences, in particular $\boldsymbol{\epsilon}$ for the empty sequence, and small letters a, b, m, n, x, y, etc. for elements of sequences;

• • We define $\overline{n} := \{ \, 1, 2, \dots, n \, \}$ for each $n \in \mathbb{N}_+ := \mathbb{N} \setminus \{ 0 \}$ , and $\overline{0} := \emptyset$ ;

• • We write $x_1 x_2 \dots x_{|\boldsymbol{s}|}$ for a sequence $\boldsymbol{s} = (x_1, x_2, \dots, x_{|\boldsymbol{s}|})$ , where $|\boldsymbol{s}|$ is the length of $\boldsymbol{s}$ , define $\boldsymbol{s}(i) := x_i$ ( $i \in \overline{|\boldsymbol{s}|}$ ) and write $a \in \boldsymbol{s}$ if $a = \boldsymbol{s}(j)$ for some $j \in \overline{|\boldsymbol{s}|}$ ;

• • An occurrence in a finite sequence $\boldsymbol{s}$ is a pair $(\boldsymbol{s}(i), i)$ such that $i \in \overline{|\boldsymbol{s}|}$ ;

• • A concatenation of sequences $\boldsymbol{s}$ and $\boldsymbol{t}$ is represented by their juxtaposition $\boldsymbol{s}\boldsymbol{t}$ (also written $\boldsymbol{s} . \boldsymbol{t}$ ), but we often write $a \boldsymbol{s}$ , $\boldsymbol{t} b$ , $\boldsymbol{u} c \boldsymbol{v}$ for $(a) \boldsymbol{s}$ , $\boldsymbol{t} (b)$ , $\boldsymbol{u} (c) \boldsymbol{v}$ , and so on;

• • We write $\mathrm{Even}(\boldsymbol{s})$ (respectively, $\mathrm{Odd}(\boldsymbol{s})$ ) if $\boldsymbol{s}$ is of even- (respectively, odd-) length;

• • For a set S of sequences and a predicate $\mathrm{P} \in \{ \mathrm{Even}, \mathrm{Odd} \}$ , $S^\mathrm{P} := \{ \, \boldsymbol{s} \in S \mid \mathrm{P}(\boldsymbol{s}) \, \}$ ;

• • We write $\boldsymbol{s} \preceq \boldsymbol{t}$ if $\boldsymbol{s}$ is a prefix of a sequence $\boldsymbol{t}$ , and, given a set S of sequences, $\mathrm{Pref}(S)$ for the set of all prefixes of sequences in S, i.e., $\mathrm{Pref}(S) := \{ \, \boldsymbol{s} \mid \exists \boldsymbol{t} \in S . \, \boldsymbol{s} \preceq \boldsymbol{t} \, \}$ ;

• • We use informal ‘tags’ $(\_)_{[i]}$ ( $i \in \mathbb{N}$ ) for clarity; e.g., see Definition 2.3.6.

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, ² 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.

Definition 2.1.1 (moves) Fix arbitrary pairwise distinct symbols O, P, Q and A, and call them labels. A move is any triple $m^{xy} := (m, x, y)$ such that $x \in \{ \mathrm{O}, \mathrm{P} \}$ and $y \in \{ \mathrm{Q}, \mathrm{A} \}$ .

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}$ .

Definition 2.1.3. (arenas (Hyland and Ong 2000; McCusker 1998)). An arena is a pair $A = (M_A, \vdash_A)$ such that

• • $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}$ .

Remark 2.1.4. McCusker (1998) an arena to be a triple $A = (M_A, \lambda_A, \vdash_A)$ , where labels are assigned to moves by the labelling function $\lambda_A : M_A \rightarrow \{ \mathrm{O}, \mathrm{P} \} \times \{ \mathrm{Q}, \mathrm{A} \}$ . Instead, we embed labels into moves (Definition 2.1.1). This modification is technically convenient, e.g., consider the union of games (Section 3), since it makes labels on a move unambiguous without specifying its underlying arena. Besides, the axiom E1 in McCusker (1998) further requires the logical equivalence $n \vdash_A m \Leftrightarrow n = \star$ whenever $\star \vdash_A m$ . We discard this condition too again for the union of games; see the beginning of Section 3.

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 1999b, 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.

Definition 2.1.5 (justified sequences (Coquand 1995; Hyland and Ong 2000)). A justified (j-) sequence is a pair $\boldsymbol{s} = (\boldsymbol{s}, \mathcal{J}_{\boldsymbol{s}})$ of a finite sequence $\boldsymbol{s}$ of moves and a map $\mathcal{J}_{\boldsymbol{s}} : \overline{|\boldsymbol{s}|} \rightarrow \{ 0 \} \cup \overline{|\boldsymbol{s}|-1}$ such that $0 \leqslant \mathcal{J}_{\boldsymbol{s}}(i) < i$ for all $i \in \overline{|\boldsymbol{s}|}$ , called the pointer of $\boldsymbol{s}$ .

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.

Remark 2.1.7. Unlike McCusker (1998), we define a j-sequence in such a way that it makes sense even without an underlying arena. This reformulation is convenient since it enables us to manipulate j-sequences without calculating underlying arenas.

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.

Definition 2.1.9 (justified subsequences). A justified (j-) subsequence of a j-sequence $\boldsymbol{s}$ is a j-sequence $\boldsymbol{t}$ , written $\boldsymbol{t} \sqsubseteq \boldsymbol{s}$ , whose underlying sequence is a subsequence of $\boldsymbol{s}$ , and $\mathcal{J}_{\boldsymbol{t}}(n) = m$ if and only if there are occurrences $m_1, m_2, \dots, m_k$ in $\boldsymbol{s}$ deleted in $\boldsymbol{t}$ such that $\mathcal{J}_{\boldsymbol{s}}(n) = m_1$ , $\mathcal{J}_{\boldsymbol{s}}(m_1) = m_2$ ,, $\mathcal{J}_{\boldsymbol{s}}(m_{k-1}) = m_k$ and $\mathcal{J}_{\boldsymbol{s}}(m_{k}) = m$ , where m can be $\star$ .

Definition 2.1.10 (views (Coquand 1995; Hyland and Ong 2000)). The P-view $\lceil \boldsymbol{s} \rceil$ and O-view $\lfloor \boldsymbol{s} \rfloor$ of a j-sequence $\boldsymbol{s}$ are the j-subsequences of $\boldsymbol{s}$ defined by induction:

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.

Remark 2.1.11. The P-view $\lceil \boldsymbol{s} \rceil$ or the O-view $\lfloor \boldsymbol{s} \rfloor$ may not be a j-sequence because the justifier of m may be lost in the clause (2) or (6). Nevertheless, this problem is insignificant as we later focus on visible j-sequences (Definition 2.1.12), for which this problem does not occur.

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 (1995) for an explanation of views in terms of logical calculi, and Curien (1998) in terms of lambda-calculi.

Definition 2.1.12. (legal positions (Hyland and Ong 2000)). A legal position is a j-sequence $\boldsymbol{s}$ such that

• • (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),³ 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;⁴

• • 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 (1998):

Definition 2.2.1 (games (Abramsky and McCusker 1999b; McCusker 1998)). A game is a set G of legal positions such that

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)$ ⁵ 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} \, \}$ .

Remark 2.2.2. The original article (McCusker 1998, p. 27) further imposes thread-closure on each game G: The thread $\boldsymbol{s} \upharpoonright \mathcal{I} \sqsubseteq \boldsymbol{s}$ of a position $\boldsymbol{s} \in G$ with respect to any set $\mathcal{I}$ of initial occurrences in $\boldsymbol{s}$ , which consists of occurrences hereditarily justified⁶ by elements in $\mathcal{I}$ , must be in G. This is to ensure that all positions in G are in the exponential ${\mathrm{!}} G$ (Definition 2.3.3), i.e., $G \subseteq {\mathrm{!}} G$ , which matches the intuition on exponential ${\mathrm{!}}$ in linear logic (Girard 1987).

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 (1998)⁷ 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).

Definition 2.2.3 (strategies (McCusker 1998)). A strategy on a game G is a subset $\sigma \subseteq G^{\mathrm{Even}}$ , written $\sigma : G$ , that is nonempty, even-prefix-closed (i.e., $\boldsymbol{s}mn \in \sigma \Rightarrow \boldsymbol{s} \in \sigma$ ) and deterministic (i.e., $\boldsymbol{s}mn, \boldsymbol{s}mn' \in \sigma \Rightarrow \boldsymbol{s}mn = \boldsymbol{s}mn'$ ). We define $\mathrm{st}(G) := \{ \, \sigma \mid \sigma : G \, \}$ .

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$ .

Example 2.2.5 The terminal game $T := \{ \boldsymbol{\epsilon} \}$ only has the strategy $\top := \{ \boldsymbol{\epsilon} \}$ .

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:

Definition 2.2.6 (constraints on strategies (Clairambault and Harmer 2010; Coquand 1995; Hyland and Ong 2000; Laird 1997)). A strategy $\sigma : G$ is

• • Total if it always responds: $\forall \boldsymbol{s} \in \sigma, \boldsymbol{s} m \in G . \, \exists \boldsymbol{s} m n \in \sigma$ ;

• • Innocent if it only depends on P-views: $\forall \boldsymbol{s} m n \in \sigma, \boldsymbol{t} \in \sigma, \boldsymbol{t} l \in G . \, \lceil \boldsymbol{s} m \rceil = \lceil \boldsymbol{t} l \rceil \Rightarrow \exists \boldsymbol{t}lr \in \sigma . \, \lceil \boldsymbol{s} m n \rceil = \lceil \boldsymbol{t}lr \rceil$ ;

• • Noetherian if there is no strictly increasing (with respect to the prefix relation $\preceq$ ) infinite sequence of elements in the set $\lceil \sigma \rceil := \{ \, \lceil \boldsymbol{s} \rceil \mid \boldsymbol{s} \in \sigma \, \}$ of all P-views in $\sigma$ ;

• • Winning if it is total, innocent and noetherian;

• • Well-bracketed if its ‘question-answering’ in P-views is in the ‘last-question-first-answered’ fashion: If $\boldsymbol{s} q \boldsymbol{t} a \in \sigma$ , where $\lambda^{\mathrm{QA}}(q) = \mathrm{Q}$ , $\lambda^{\mathrm{QA}}(a) = \mathrm{A}$ and $\mathcal{J}_{\boldsymbol{s}q\boldsymbol{t}a}(a) = q$ , then each question occurring in $\boldsymbol{t}'$ , where the P-view $\lceil \boldsymbol{s} q \boldsymbol{t} \rceil$ is of the form $\lceil \boldsymbol{s} q \boldsymbol{t} \rceil = \lceil \boldsymbol{s} q \rceil . \boldsymbol{t}'$ by visibility, justifies an answer occurring in $\boldsymbol{t}'$ .

Example 2.2.7 The strategies $\top : T$ and $\underline{n} : N$ for all $n \in \mathbb{N}$ are winning and well-bracketed, while the strategies $\bot : 0$ and $\bot : N$ are not even total, let alone winning.

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. 1998; Abramsky and McCusker 1997, 1999a). 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 1997). 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 (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$ .

Definition 2.3.2 (constructions on arenas (Hyland and Ong 2000; McCusker 1998)). Given arenas A and B, we define

• • $A \uplus B := (M_A \uplus M_B, \vdash_A \uplus \vdash_B)$ ;

• • If $B \neq T$ , then $A \multimap B := (\{ \, a^{(x^\bot)y} \mid a^{xy} \in M_A \, \} \uplus M_B, \vdash_{A \multimap B})$ , where $\mathrm{O}^\bot := \mathrm{P}$ , $\mathrm{P}^\bot := \mathrm{O}$ , $\star \vdash_{A \multimap B} m :\Leftrightarrow \star \vdash_B m$ and $m \vdash_{A \multimap B} n :\Leftrightarrow m \vdash_A n \vee m \vdash_B n \vee (\star \vdash_B m \wedge \star \vdash_A n)$ ;

• • $A \multimap T := T$ .⁸

Definition 2.3.3 (constructions on games (Hyland and Ong 2000;McCusker 1998)). Given games G and H, we define

• • The tensor $G \otimes H$ of G and H by

  \begin{equation*}G \otimes H := \{ \, \boldsymbol{s} \in \mathscr{L}_{\mathrm{Arn}(G) \uplus \mathrm{Arn}(H)} \mid \forall X \in \{ G, H \} . \, \boldsymbol{s} \upharpoonright X \in X \, \},\end{equation*}
  where the j-subsequence $\boldsymbol{s} \upharpoonright X \sqsubseteq \boldsymbol{s}$ consists of the occurrences of moves in X;

• • The exponential ${\mathrm{!}} G$ of G by

  \begin{equation*}{\mathrm{!}} G := \{ \, \boldsymbol{s} \in \mathscr{L}_{\mathrm{Arn}(G)} \mid \forall i \in |\boldsymbol{s}| . \, \mathcal{J}_{\boldsymbol{s}}(i) = 0 \Rightarrow \boldsymbol{s} \upharpoonright \{ (\boldsymbol{s}(i), i) \} \in G \, \},\end{equation*}
  where the j-subsequence $\boldsymbol{s} \upharpoonright \{ (\boldsymbol{s}(i), i) \} \sqsubseteq \boldsymbol{s}$ ⁹ consists of the occurrences in $\boldsymbol{s}$ hereditarily justified (Footnote 6) by the initial occurrence $(\boldsymbol{s}(i), i)$ in $\boldsymbol{s}$ ;

• • The product $G \mathbin{\&} H$ of G and H by

  \begin{equation*}G \mathbin{\&} H := \{ \, \boldsymbol{s} \in \mathscr{L}_{\mathrm{Arn}(G) \mathbin{\uplus} \mathrm{Arn}(H)} \mid (\boldsymbol{s} \upharpoonright G \in G \wedge \boldsymbol{s} \upharpoonright H = \boldsymbol{\epsilon}) \vee (\boldsymbol{s} \upharpoonright G = \boldsymbol{\epsilon} \wedge \boldsymbol{s} \upharpoonright H \in H) \, \};\end{equation*}

• • The linear implication $G \multimap H$ from G to H by

  \begin{equation*}G \multimap H := \{ \, \boldsymbol{s} \in \mathscr{L}_{\mathrm{Arn}(G) \multimap \mathrm{Arn}(H)} \mid \boldsymbol{s} \upharpoonright G^\bot \in G, \boldsymbol{s} \upharpoonright H \in H \, \} \quad \text{(also written $H^G$)},\end{equation*}
  where the j-sequence $\boldsymbol{s} \upharpoonright G^\bot$ is obtained from $\boldsymbol{s} \upharpoonright G$ by modifying all the moves $m^{(x^\bot)y}$ occurring in $\boldsymbol{s} \upharpoonright G$ into $m^{xy}$ ;

• • The implication $G \Rightarrow H$ from G to H by

  \begin{equation*}G \Rightarrow H := {\mathrm{!}} G \multimap H.\end{equation*}

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$ .

Lemma 2.3.5 (well-defined constructions on games). Games and well-founded games are both closed under tensor, product, exponential and linear implication, and well-opened ones under product, linear implication and implication.

Proof. SeeMcCusker (1998) for the closure of MC-games under these constructions. The proof is essentially the same for games. The preservation of well-founded (respectively, well-opened) ones under the constructions is obvious.

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

Definition 2.3.6 (constructions on strategies (Hyland and Ong 2000; McCusker 1998)). Given strategies $\phi : G \multimap H$ , $\sigma : J \multimap K$ , $\tau : G \multimap J$ , $\psi : H \multimap J$ and $\theta : {\mathrm{!}} G \multimap H$ , we define

• • The copy-cat $\mathrm{cp}_G : G \multimap G$ on G by

  \begin{equation*}\mathrm{cp}_G := \{ \, \boldsymbol{s} \in (G_{[0]} \multimap G_{[1]})^{\mathrm{Even}} \mid \forall \boldsymbol{t} \preceq \boldsymbol{s} . \, \mathrm{Even}(\boldsymbol{t}) \Rightarrow \boldsymbol{t} \upharpoonright G_{[0]}^\bot = \boldsymbol{t} \upharpoonright G_{[1]}, \mathrm{Init}_{G_{[0]}, G_{[1]}}(\boldsymbol{s}) \, \},\end{equation*}
  where $\mathrm{Init}_{G_{[0]}, G_{[1]}}(\boldsymbol{s})$ means that in $\boldsymbol{s}$ each initial occurrence in the domain $G_{[0]}$ points to the last initial occurrence in the codomain $G_{[1]}$ ;

• • The dereliction $\mathrm{der}_G : G \Rightarrow G$ on G by

  \begin{equation*}\mathrm{der}_G := \{ \, \boldsymbol{s} \in ({\mathrm{!}} G \multimap G)^{\mathrm{Even}} \mid \forall \boldsymbol{t} \preceq \boldsymbol{s} . \, \mathrm{Even}(\boldsymbol{t}) \Rightarrow \boldsymbol{t} \upharpoonright {\mathrm{!}} G^\bot = \boldsymbol{t} \upharpoonright G, \mathrm{Init}_{{\mathrm{!}} G, G}(\boldsymbol{s}) \, \};\end{equation*}

• • The tensor $\phi \otimes \sigma : G \otimes J \multimap H \otimes K$ of $\phi$ and $\sigma$ by

  \begin{equation*}\phi \otimes \sigma := \{ \, \boldsymbol{s} \in (G \otimes J \multimap H \otimes K) \mid \boldsymbol{s} \upharpoonright G, H \in \phi, \boldsymbol{s} \upharpoonright J, K \in \sigma \, \},\end{equation*}
  where $\boldsymbol{s} \upharpoonright G, H$ (respectively, $\boldsymbol{s} \upharpoonright J, K$ ) denotes the j-subsequence of $\boldsymbol{s}$ that consists of the occurrences of moves in G or H (respectively, J or K);

• • The pairing $\langle \phi, \tau \rangle : G \multimap H \mathbin{\&} J$ of $\phi$ and $\tau$ by

  \begin{equation*}\langle \phi, \tau \rangle := \{ \, \boldsymbol{s} \in (G \multimap H \mathbin{\&} J) \mid (\boldsymbol{s} \upharpoonright G, H \in \phi \wedge \boldsymbol{s} \upharpoonright J = \boldsymbol{\epsilon}) \vee (\boldsymbol{s} \upharpoonright G, J \in \tau \wedge \boldsymbol{s} \upharpoonright H = \boldsymbol{\epsilon}) \, \};\end{equation*}

• • The composition $\phi ; \psi : G \multimap J$ of $\phi$ and $\psi$ by

  \begin{equation*}\phi ; \psi := \{ \, \boldsymbol{s} \upharpoonright G, J \mid \boldsymbol{s} \in \phi \parallel \psi \, \} \quad \text{(also written $\psi \circ \phi$)},\end{equation*}
  where
  \begin{equation*}\phi \parallel \psi := \{ \, \boldsymbol{s} \in \mathscr{J}_{\mathrm{Arn}(((G \multimap H_{[0]}) \multimap H_{[1]}) \multimap J)} \mid \boldsymbol{s} \upharpoonright G, H_{[0]} \in \phi, \boldsymbol{s} \upharpoonright H_{[1]}, J \in \psi, \boldsymbol{s} \upharpoonright H_{[0]}^\bot, H_{[1]}^\bot \in \mathrm{cp}_H \, \},\end{equation*}
  ¹⁰ and the j-sequence $\boldsymbol{s} \upharpoonright H_{[0]}^\bot, H_{[1]}^\bot$ is obtained from the j-subsequence $\boldsymbol{s} \upharpoonright H_{[0]}, H_{[1]} \sqsubseteq \boldsymbol{s}$ by applying the operation $(\_)^\bot : m^{xy} \mapsto m^{x^\bot y}$ (Definition 2.3.2) to all occurrences $m^{xy}$ ;

• • The promotion $\theta^\dagger : {\mathrm{!}} G \multimap {\mathrm{!}} H$ of $\theta$ by

  \begin{equation*}\theta^\dagger := \{ \, \boldsymbol{s} \in ({\mathrm{!}} G \multimap {\mathrm{!}} H)^{\mathrm{Even}} \mid \forall i \in |\boldsymbol{s}| . \, \mathcal{J}_{\boldsymbol{s}}(i) = 0 \Rightarrow \boldsymbol{s} \upharpoonright \{ (\boldsymbol{s}(i), i) \} \in \theta \, \}.\end{equation*}

For the dereliction $\mathrm{der}_G$ to be well-defined, we must focus on well-opened games G; see McCusker (1998, pp. 42–43) for the details. Although well-opened games are not closed under exponential, it does not matter for us, just like McCusker (1998, 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).

Lemma 2.3.7 (well-defined constructions on strategies). If $\phi : G \multimap H$ , $\sigma : J \multimap K$ , $\tau : G \multimap J$ , $\psi : H \multimap J$ and $\theta : {\mathrm{!}} G \multimap H$ , then $\mathrm{cp}_G : G \multimap G$ , $\phi \otimes \sigma : G \otimes J \multimap H \otimes K$ , $\langle \phi, \tau \rangle : G \multimap H \mathbin{\&} J$ , $\phi ; \psi : G \multimap J$ and $\theta^\dagger : {\mathrm{!}} G \multimap {\mathrm{!}} H$ ; $\mathrm{der}_H : H \Rightarrow H$ if H is well-opened. Moreover, $\mathrm{cp}_G$ (respectively, $\mathrm{der}_H$ ) is winning and well-bracketed if G is well-founded (respectively, if H is well-opened and well-founded), and the constructions $\otimes$ , $\langle \_, \_ \rangle$ , $\circ$ and $(\_)^\dagger$ preserve winning and well-bracketing.

Proof. The nontrivial point not shown by Clairambault and Harmer (2010) or McCusker (1998) is that $\mathrm{cp}_G$ is noetherian if G is well-founded (the case for $\mathrm{der}_H$ is the same). N.b., $\mathrm{cp}_G$ is total, innocent and well-bracketed even if G is not well-founded. Given $\boldsymbol{s}mm \in \mathrm{cp}_G$ , we see by induction on $|\boldsymbol{s}|$ that the P-view $\lceil \boldsymbol{s} m \rceil$ is of the form $m_1 m_1 m_2 m_2 \dots m_k m_k m$ with $\star \vdash_{G} m_1 \vdash_{G} m_2 \vdash_G \dots \vdash_{G} m_k \vdash_{G} m$ . Thus, $\mathrm{cp}_G$ is noetherian if G is well-founded.

Definition 2.3.8 (categories of games). The category $\mathbb{G}_{\mathrm{!}}$ consists of

• • 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 1998, 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 1998, 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:

Theorem 2.3.9 (well-defined cartesian closed categories of games). The structures $\mathbb{G}_{\mathrm{!}}$ , $\mathbb{LG}_{\mathrm{!}}$ and $\mathbb{WG}_{\mathrm{!}}$ form cartesian closed categories.

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. Predicate Games

Having reviewed games and strategies in Section 2, let us now initiate our contributions. Before going into details, let us sketch our idea in the following paragraphs. In short, the main challenge is to interpret Sigma types without destroying the non-inductive nature of game semantics or the additive nature of product on games (Section 1.4), and we overcome this challenge by generalising games. Meanwhile, we keep strategies unchanged so that our method retains the advantages of conventional game semantics such as intensionality (Section 1.2).

Dependent types are not the main problem: Naively, we can interpret each dependent type $\mathrm{x : C} \vdash \mathrm{D(x)} \ \mathrm{type}$ by a family $D = \{ D(\sigma) \}_{\sigma : C}$ of games $D(\sigma)$ indexed by strategies $\sigma$ on the game C that interprets the simple type $\vdash \mathrm{C} \ \mathrm{type}$ , which we abbreviate as C. In the presence of Sigma types, dependent types with only a single variable cover those with more than one variable, and therefore we focus on the former in this introduction to Section 3.

Then, in light of product on games (Definition 2.3.3), which interprets a particular kind of Sigma types, viz., product types, it seems a natural idea to interpret the Sigma type $\Sigma_\mathrm{{x : C} D(x)}$ by a subgame $\Sigma(C, D) \subseteq C \mathbin{\&} \bigcup_{\sigma : C}D(\sigma)$ such that strategies on $\Sigma(C, D)$ are precisely the pairings $\langle \sigma, \tau \rangle$ of $\sigma : C$ and $\tau : D(\sigma)$ .

However, this idea does not work due to the following two problems:

1. (1) Each game G, by definition, determines the set $\mathrm{st}(G)$ of all strategies on G;

2. (2) It is impossible for P, when playing on such a game $\Sigma(C, D)$ , if any, to fix a strategy $\sigma : C$ , let alone a game $D(\sigma)$ , at the beginning of a play.

As an example of the first problem, consider a dependent type $\mathrm{x : N} \vdash \mathrm{N_b(x) \ type}$ such that the canonical terms of the simple type N_b(k) ( $k \in \mathbb{N}$ ) are the numerals ${\underline{\mathrm{n}}}$ such that $n \leqslant k$ , and assume that we interpret N_b by the family $N_b = \{ N_b(\sigma) \}_{\sigma : N}$ of games $N_b(\sigma)$ defined by $N_b(\underline{k}) := \mathrm{Pref}(\{ \, qn \mid n \leqslant k \, \})$ and $N_b(\bot) := N$ .¹¹ However, there is no subgame $G \subseteq N \mathbin{\&} \bigcup_{\sigma : N}N_b(\sigma) = N \mathbin{\&} N$ such that $\langle \underline{k}, \underline{n} \rangle : G$ if and only if $\underline{n} : N_b(\underline{k})$ , i.e., $n \leqslant k$ , for all $k, n \in \mathbb{N}$ since if such a game G existed, then $\langle \underline{0}, \underline{0} \rangle, \langle \underline{1}, \underline{1} \rangle : G$ , which implies $\langle \underline{0}, \underline{1} \rangle : G$ by the definition of strategies on a game (Definition 2.2.3), a contradiction. Accordingly, no game can properly interpret the Sigma type $\Sigma_\mathrm{{x:N}N_b(x)}$ .

Let us next provide an example of the second problem. Let $\mathrm{x : N} \vdash \mathrm{List_N(x) \ type}$ be a dependent type such that the canonical terms of the simple type List_N(k) ( $k \in \mathbb{N}$ ) are the k-lists of numerals, and assume that we interpret List_N by the family $\mathrm{List}_N = \{ \mathrm{List}_N(\sigma) \}_{\sigma : N}$ of games $\mathrm{List}_N(\sigma)$ such that $\mathrm{List}_N(\underline{k})$ is the k-ary tensor $\otimes$ on N, where $\mathrm{List}_N(\underline{0}) := T$ and $\mathrm{List}_N(\bot) := \bigcup_{k \in \mathbb{N}} \mathrm{List}_N(\underline{k})$ .¹² If there were a subgame $H \subseteq N \mathbin{\&} \bigcup_{\sigma : N} \mathrm{List}_N(\sigma)$ that interprets the Sigma type $\Sigma_\mathrm{{x:N} List_N(x)}$ , then the pairing $\langle \underline{k}, \underline{n_1} \otimes \underline{n_2} \otimes \cdots \otimes \underline{n_k} \rangle$ for any $k, n_1, n_2, \dots, n_k \in \mathbb{N}$ would be total on H since strategies modelling proofs must be winning (Section 2.2). Thus, there is no such a game H because O may select, by his first move, e.g., the $(k+1)$ st component of $\mathrm{List}_N(\underline{k+1})$ , for which $\langle \underline{k}, \underline{n_1} \otimes \underline{n_2} \otimes \cdots \otimes \underline{n_k} \rangle$ has no next move.

We have seen two fundamental limitations of games. We then solve this problem by generalising a game to the pair $\Gamma = (|\Gamma|, \| \Gamma \|)$ of a game $|\Gamma|$ and a family $\| \Gamma \| = \{ \Gamma(\gamma) \}_{\gamma : |\Gamma|}$ of subgames $\Gamma(\gamma) \subseteq | \Gamma |$ , called a predicate (p-) game, and define a strategy $\gamma$ on $\Gamma$ , written $\gamma : \Gamma$ , to be a strategy $\gamma : |\Gamma|$ such that $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}} : \Gamma(\gamma)$ (Definition 2.2.4). I.e., a p-game $\Gamma$ is a game $|\Gamma|$ together with a specification $\| \Gamma \|$ for strategies $\gamma : |\Gamma|$ to be on $\Gamma$ , viz., $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}} : \Gamma(\gamma)$ .

A play in a p-game $\Gamma$ therefore depends on P’s predetermined choice of a strategy $\gamma : \Gamma$ in the sense that the choice $\gamma$ defines the underlying game of the play to be $\Gamma(\gamma)$ . This additional power of P to control the underlying game of a p-game plays a central role in our approach as we shall see shortly. Note that P’s choice of a strategy must be invisible to O since otherwise O would know what P is going to do even before a play begins.

To describe this idea vividly, we informally introduce Judge (J). A play in a p-game $\Gamma$ then proceeds informally as follows. First, J asks P a question $q_\Gamma$ (‘What is your strategy?’) and P answers it by a strategy $\gamma : \Gamma$ (‘It is $\gamma$ !’). After this initial protocol between J and P, an ordinary play in the game $\Gamma(\gamma)$ between P and O follows, where P must play by the declared one $\gamma$ yet restricted to $\Gamma(\gamma)$ , i.e., $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}} : \Gamma(\gamma)$ . In this way, P declares her choice of a strategy $\gamma$ , which is observed by J yet not by O, and this choice determines the underlying subgame $\Gamma(\gamma) \subseteq |\Gamma|$ for the play between O and P to follow. Thus, we define the strategy $\gamma : \Gamma$ to be winning (respectively, well-bracketed) if so is the one $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}} : \Gamma(\gamma)$ .

Strictly speaking, J and initial protocols are nothing but informal devices for explaining the idea of requiring P to fix a strategy $\gamma : |\Gamma|$ that passes the test $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}} : \Gamma(\gamma)$ before a play in the game $\Gamma(\gamma)$ starts. Formally, neither J nor initial protocols is part of p-games; it suffices to assign, to each strategy $\gamma : \Gamma$ , the game $\Gamma(\gamma)$ by the family $\| \Gamma \|$ . However, we often add an initial protocol informally to the beginning of a play for pedagogical reasons.

This generalisation of games to p-games solves the first problem as follows. Let $\Sigma(N, N_b)$ be the p-game defined by $|\Sigma(N, N_b)| := N \mathbin{\&} N$ and

\begin{equation*}\Sigma(N, N_b)(\langle \sigma, \tau \rangle) := \begin{cases} N \mathbin{\&} N_b(\underline{k}) &\text{if $\sigma = \underline{k}$ for some $k \in \mathbb{N}$;} \\ N \mathbin{\&} N &\text{otherwise} \end{cases} \quad (\langle \sigma, \tau \rangle : |\Sigma(N, N_b)|).\end{equation*}

Observe then that strategies on this p-game $\Sigma(N, N_b)$ are pairings $\langle \sigma, \tau \rangle : N \mathbin{\&} N$ such that $\tau : N_b(\underline{k})$ if $\sigma = \underline{k}$ . For instance, typical plays by the strategy $\langle \underline{7}, \underline{3} \rangle : \Sigma(N, N_b)$ are

where J first asks P the question $q_{\Sigma(N, N_b)}$ (‘What is your strategy?’), and P answers it by $\langle \underline{7}, \underline{3} \rangle : \Sigma(N, N_b)$ (‘It is $\langle \underline{7}, \underline{3} \rangle$ !’); then, an ordinary play between P and O on the game $\Sigma(N, N_b)(\langle \underline{7}, \underline{3} \rangle) = N \mathbin{\&} N_b(\underline{7})$ follows, where P must play by the strategy $\overline{\langle \underline{7}, \underline{3} \rangle}_{N \mathbin{\&} N_b(\underline{7})}^{\mathrm{Even}} = \langle \underline{7}, \underline{3} \rangle$ . The arrows in the diagram represent pointers in j-sequences (Definition 2.1.5).

Although the predetermination of a strategy is not necessary in this example, it is clear why P cannot play by the invalid one $\langle \underline{0}, \underline{1} \rangle$ on $\Sigma(N, N_b)$ : $\overline{\langle \underline{0}, \underline{1} \rangle}_{N \mathbin{\&} N_b(\underline{0})}^{\mathrm{Even}} \not\subseteq \Sigma(N, N_b)(\langle \underline{0}, \underline{1} \rangle)$ . In this way, the specification $\| \Sigma(N, N_b) \|$ solves the first problem by filtering strategies.

In contrast, the predetermination of a strategy plays a crucial role in solving the second problem: The p-game $\Sigma(N, \mathrm{List}_N)$ defined by

interprets the Sigma type $\Sigma_\mathrm{{x:N} List_N(x)}$ . Typical plays in this p-game $\Sigma(N, \mathrm{List}_N)$ are

where the predetermination of the strategy $\langle \underline{2}, \underline{1} \otimes \underline{3} \rangle$ fixes the game $N \mathbin{\&} (N \otimes N)$ . As a result, the strategy $\overline{\langle \underline{2}, \underline{1} \otimes \underline{3} \rangle}_{N \mathbin{\&} (N \otimes N)}^{\mathrm{Even}} = \langle \underline{2}, \underline{1} \otimes \underline{3} \rangle$ is total on the p-game $\Sigma(N, \mathrm{List}_N)$ .

In this way, we achieve game semantics of Sigma types directly without the formal list construction of Abramsky et al. (2015), Vákár et al. (2018) (Section 1.4). Let us add an important remark that their method cannot properly interpret the Sigma type $\Sigma\mathrm{(N, List_N)}$ because total strategies on their interpretation of this Sigma type are the lists $(\underline{k}, \underline{n_1} \otimes \underline{n_2} \otimes \dots)$ of strategies, where the second component is an infinite iteration of tensor $\otimes$ , due to the O-sat operation (Vákár et al. 2018, Remark 4.5). We come back to this point in Section 4.3.

Besides, our game semantics of Sigma types retains the additive nature of product on games because a play in the interpretation occurs in either side, not both, which stands in sharp contrast with the interpretation of Sigma types by Blot and Laird (2018) (Section 1.4). This will be important in the future when one considers an extension of game semantics of MLTT to linear logic because it must distinguish additive and multiplicative Sigma types.

Finally, let us justify the fixing of a strategy on a p-game before the start of a play as follows. First, even in conventional game semantics, one eventually focuses on interactions between O and P in which P plays by a fixed strategy. Moreover, this predetermination of a strategy does not lose generality as each position $\boldsymbol{s}$ in a game G is the result of a play by some strategy $\sigma : G$ , viz., $\sigma := \mathrm{Pref}(\{ \boldsymbol{s} \})^{\mathrm{Even}}$ . Second, because the predetermination is not part of plays in p-games and thus invisible to O, a strategy is revealed to O only gradually and often incompletely along the development of a play (as in the case of games). Dually, O’s strategy on the domain $\Gamma$ of a given linear implication $\Gamma \multimap \Delta$ between p-games (Definition 3.2.6) is revealed to P only gradually and often incompletely via plays. As a result, the extensions of strategies on $\Gamma \multimap \Delta$ are continuous maps (as in the case of games). More generally, our method inherits the intensionality of existing game semantics (Sections 4.6–4.7).

In the rest of this section, we define p-games in Section 3.1 and generalise the constructions on games (Section 2.3) to p-games in Section 3.2, where we slightly modify the aforementioned interpretation of dependent types (Definition 3.1.3) and examples $\mathrm{List}_N$ and $N_b$ (Example 4.1.3).

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:

Definition 3.1.1 (liveness ordering (Chroboczek 2000)). The liveness ordering is the partial order $\preccurlyeq$ between games G and H (Chroboczek 2000, Definition 8 and Theorem 9) that defines $G \preccurlyeq H$ to mean that O (respectively, P) is less (respectively, more) restricted in G than in H, i.e.,

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}}$ .

Proposition 3.1.2 (liveness characterisation). Assume $\sigma : G$ and $H \in \mathrm{sub}(G)$ .

1. (1) $\overline{\sigma}_H^{\mathrm{Even}} : H$ if and only if $\overline{\sigma}_{G} \preccurlyeq H$ ;

2. (2) If $\overline{\sigma}_{G} \preccurlyeq H$ , then $\overline{\sigma}_{H}^{\mathrm{Even}} = \sigma \cap H$ .

Proof. We focus on the first clause since it is a routine to verify the second one. First, it is easy to see that the relation $\overline{\sigma}_H^{\mathrm{Even}} : H$ is equivalent to the one $\overline{\sigma}_H^{\mathrm{Even}} \subseteq H^{\mathrm{Even}}$ . Thus, it suffices to show $\overline{\sigma}_H^{\mathrm{Even}} \subseteq H^{\mathrm{Even}}$ if and only if $\overline{\sigma}_{G} \preccurlyeq H$ . The sufficiency is shown by induction on the lengths of positions, which we leave to the reader; we focus on the necessity.

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:

Definition 3.1.3 (predicate games). A predicate (p-) game is a pair $\Gamma = (|\Gamma|, \| \Gamma \|)$ of a game $|\Gamma|$ and a family $\| \Gamma \| = \{ \Gamma(\gamma) \}_{\gamma : |\Gamma|}$ of subgames $\Gamma(\gamma) \subseteq |\Gamma|$ . Moreover:

• • 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.

Remark 3.1.4. If initial protocols were part of ordinary plays or visible to O, then by duality those on the domain of each linear implication would be visible to P so that the extensions of strategies on a linear implication may not be continuous. This extensionality would ruin the intensionality of game semantics (Section 1.2). For this reason, initial protocols are not part of positions in p-games, and they are only an informal, pedagogical device.

Example 3.1.5 Given a game G, we define the p-game $\mathscr{P}(G) := (G, \kappa_G)$ , where $\kappa_G$ is the constant family at G. Clearly, $\mathrm{st}(\mathscr{P}(G)) = \mathrm{st}(G)$ . We abbreviate $\mathscr{P}(T)$ , $\mathscr{P}(0)$ and $\mathscr{P}(N)$ as T, 0 and N, and call them the terminal p-game, the empty p-game and the natural number p-game, respectively (cf. Example 2.2.5).

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 2005, 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 (2005). 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.

Lemma 3.2.7 (well-defined constructions on predicate games). P-games and well-founded p-games are both closed under product, tensor, exponential and linear implication, and well-opened ones under product, linear implication and implication.

Proof. Straightforward and left to the reader.

Lemma 3.2.8 (well-defined copy-cats and derelictions between predicate games). Suppose that $\Gamma$ is a p-game, and $\Delta$ is a well-opened p-game.

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.

Proof. We focus on the first clause since the second one is similar, where we require $\Delta$ to be well-opened for the same reason as the case of derelictions between games (Section 2.3).

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|})$ .

Lemma 3.2.9 (well-defined constructions on strategies between predicate games) By applying Definition 2.3.6 to strategies $\phi : \Gamma \multimap \Delta$ , $\psi : \Delta \multimap \Theta$ , $\sigma : \Theta \multimap \Xi$ , $\tau : \Gamma \multimap \Theta$ and $\theta : {\mathrm{!}} \Gamma \multimap \Delta$ between p-games,¹³ one gets those $\psi \circ \phi : \Gamma \multimap \Theta$ , $\phi \otimes \sigma : \Gamma \otimes \Theta \multimap \Delta \otimes \Xi$ , $\langle \phi, \tau \rangle : \Gamma \multimap \Delta \mathbin{\&} \Theta$ and $\theta^\dagger : {\mathrm{!}} \Gamma \multimap {\mathrm{!}} \Delta$ , and these constructions preserve winning and well-bracketing.

Proof. We focus on the tensor $\phi \otimes \sigma$ and the composition $\psi \circ \phi$ since the other constructions are simpler.¹⁴ First, let us show $\phi \otimes \sigma : \Gamma \otimes \Theta \multimap \Delta \otimes \Xi$ , for which it suffices to verify $(\overline{\phi \otimes \sigma})_{|\Delta \otimes \Xi|^{|\Gamma \otimes \Theta|}} \preccurlyeq (\Delta \otimes \Xi)^{\Gamma \otimes \Theta}(\phi \otimes \sigma)$ . We do it by induction on the lengths of positions. The base case and inductive step on odd-length positions are trivial. For the other step, let $\boldsymbol{s}mn \in \phi \otimes \sigma$ and $\boldsymbol{s}m \in (\overline{\phi \otimes \sigma})_{|\Delta \otimes \Xi|^{|\Gamma \otimes \Theta|}} \cap (\Delta \otimes \Xi)^{\Gamma \otimes \Theta}(\phi \otimes \sigma)$ ; we have to show $\boldsymbol{s}mn \in (\Delta \otimes \Xi)^{\Gamma \otimes \Theta}(\phi \otimes \sigma)$ . By $\boldsymbol{s}m \in (\Delta \otimes \Xi)^{\Gamma \otimes \Theta}(\phi \otimes \sigma)$ , it suffices to show $\boldsymbol{s}mn \in (\Delta \otimes \Xi)((\phi \otimes \sigma) \circ \varphi)^{\overline{\varphi}_{\Gamma \otimes \Theta}}$ for all $\varphi : \Gamma \otimes \Theta$ with $\boldsymbol{s}m \in (\Delta \otimes \Xi)((\phi \otimes \sigma) \circ \varphi)^{\overline{\varphi}_{\Gamma \otimes \Theta}}$ . Fix such $\varphi$ . Note that $\varphi = \gamma \otimes \vartheta$ for unique $\gamma : \Gamma$ and $\vartheta : \Theta$ , and $(\phi \otimes \sigma) \circ \varphi = (\phi \circ \gamma) \otimes (\sigma \circ \vartheta)$ . Thus, it suffices to show $\boldsymbol{s}mn \upharpoonright |\Delta^\Gamma| \in \Delta(\phi \circ \gamma)^{\overline{\gamma}_\Gamma}$ and $\boldsymbol{s}mn \upharpoonright |\Xi^\Theta| \in \Xi(\phi \circ \vartheta)^{\overline{\vartheta}_\Theta}$ . Let n be in $\phi$ ; the other case is similar. Then, $\boldsymbol{s}m \upharpoonright |\Delta^\Gamma| \in \Delta(\phi \circ \gamma)^{\overline{\gamma}_\Gamma}$ and $\boldsymbol{s}mn \upharpoonright |\Xi^\Theta| = \boldsymbol{s}m \upharpoonright |\Xi^\Theta| \in \Xi(\phi \circ \vartheta)^{\overline{\vartheta}_\Theta}$ by $\boldsymbol{s}m \in (\Delta \otimes \Xi)((\phi \otimes \sigma) \circ \varphi)^{\overline{\varphi}_{\Gamma \otimes \Theta}}$ . It remains to show $\boldsymbol{s}mn \upharpoonright |\Delta^\Gamma| \in \Delta(\phi \circ \gamma)^{\overline{\gamma}_\Gamma}$ , but it follows from $\phi : \Delta^\Gamma$ , $(\boldsymbol{s}m \upharpoonright |\Delta^\Gamma|).n \in \phi$ and $\boldsymbol{s}m \upharpoonright |\Delta^\Gamma| \in \overline{\phi}_{|\Delta^\Gamma|} \cap \Delta^\Gamma(\phi)$ , where $(\boldsymbol{s}m \upharpoonright |\Delta^\Gamma|).n \in \phi$ follows from $\boldsymbol{s}mn \in \phi \otimes \sigma$ , and $\boldsymbol{s}m \upharpoonright |\Delta^\Gamma| \in \overline{\phi}_{|\Delta^\Gamma|} \cap \Delta^\Gamma(\phi)$ from $(\boldsymbol{s}m \upharpoonright |\Delta^\Gamma|).n \in \phi$ , $\boldsymbol{s} \upharpoonright |\Delta^\Gamma| \in \phi \cap \Delta^\Gamma(\phi) \subseteq \Delta^\Gamma(\phi)$ and $\boldsymbol{s}m \upharpoonright |\Delta^\Gamma| \in \Delta(\phi \circ \gamma)^{\overline{\gamma}_\Gamma}$ . We have shown $\phi \otimes \sigma : \Gamma \otimes \Theta \multimap \Delta \otimes \Xi$ .

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 1997, 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 1997, 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)}}$ .¹⁵ 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:

Definition 3.2.10 (categories of predicate games). The category $\mathbb{PG}_{\mathrm{!}}$ consists of

• • 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.

Remark 3.2.11. As in the case of games in Definition 2.3.8, there are the linear counterparts of the categories $\mathbb{PG}_{\mathrm{!}}$ , $\mathbb{LPG}_{\mathrm{!}}$ and $\mathbb{WPG}_{\mathrm{!}}$ , in which morphisms $\Gamma \rightarrow \Delta$ are strategies on the linear implication $\Gamma \multimap \Delta$ . We skip them because they are not central in this work.

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.

Theorem 3.2.12 (well-defined cartesian closed categories of predicate games). The structures $\mathbb{PG}_{\mathrm{!}}$ , $\mathbb{LPG}_{\mathrm{!}}$ and $\mathbb{WPG}_{\mathrm{!}}$ form cartesian closed categories.

Proof. By Lemma 3.2.9, we can focus on $\mathbb{PG}_{\mathrm{!}}$ . The composition is well-defined by Lemma 3.2.9, and so are the identities by Lemma 3.2.8. Because morphisms in $\mathbb{PG}_{\mathrm{!}}$ are a class of morphisms in $\mathbb{G}_{\mathrm{!}}$ , and the composition and the identities in $\mathbb{PG}_{\mathrm{!}}$ are those in $\mathbb{G}_{\mathrm{!}}$ , the associativity and the unit law on $\mathbb{PG}_{\mathrm{!}}$ follow from those on $\mathbb{G}_{\mathrm{!}}$ (Theorem 2.3.9). The cartesian closure of $\mathbb{PG}_{\mathrm{!}}$ is by Example 3.1.5 and Lemma 3.2.7 and 3.2.9, where the required equations on morphisms follow from those on morphisms in $\mathbb{G}_{\mathrm{!}}$ .

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:

Corollary 3.2.14 (game-semantic finite limits and locally cartesian closure). The category $\mathbb{WPG}_{\mathrm{!}}^{\simeq}$ has all finite limits, and moreover it is locally cartesian closed.

Proof. For finite limits, it suffices to establish the equaliser of given morphisms $[\phi_1], [\phi_2] : \Gamma \rightrightarrows \Delta$ . We show that the equaliser is given by the pair $(\Theta, [\mathrm{der}_{|\Theta|}])$ , where $\Theta$ is the p-game defined by . The p-game $\Theta$ is well-defined because it does not depend on the choice of the representatives $\phi_i$ ( $i = 1, 2$ ). Note that $\theta \in \mathbb{WPG}_{\mathrm{!}}(\Theta)$ implies $\phi_1 \bullet \theta = \phi_2 \bullet \theta$ since $\mathbb{WPG}_{\mathrm{!}}(0) = \emptyset$ . Hence, it follows that the equation $[\phi_1] \bullet [\mathrm{der}_{|\Theta|}] = [\phi_2] \bullet [\mathrm{der}_{|\Theta|}]$ holds.

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 2014; Seely 1984). 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. Game Semantics of Martin-Löf Type Theory

We are now ready to present our game semantics of MLTT. Specifically, we show that the category $\mathbb{WPG}_{\mathrm{!}}$ gives rise to abstract semantics of MLTT: a category with families (CwF) introduced by Dybjer (1996). CwFs are closer to the syntax than other abstract semantics, so they enable us to see the semantic counterparts of MLTT directly. We even regard a CwF as another presentation of MLTT as Dybjer (2014) do, so we only show that $\mathbb{WPG}_{\mathrm{!}}$ forms a CwF, leaving how a CwF interprets MLTT to Hofmann (1997).

More concretely, we prove that the category $\mathbb{WPG}_{\mathrm{!}}$ gives rise to a CwF equipped with the semantic type formers (Hofmann 1997) for the One, the Zero, the N, Pi, Sigma and Id types, establishing game semantics of MLTT equipped with these types.

The rest of this section proceeds as follows. We first interpret dependent types in Section 4.1, Pi types in Section 4.2, and Sigma types in Section 4.3. We then show that the category $\mathbb{WPG}_{\mathrm{!}}$ forms a CwF in Section 4.4 and equip it with all the semantic type formers listed above in Section 4.5. Finally, we analyse the intensionality of our game semantics in Section 4.6, establish a new proof of the independence of Markov’s principle in Section 4.7, which explains why we use $\mathbb{WPG}_{\mathrm{!}}$ , not $\mathbb{PG}_{\mathrm{!}}$ or $\mathbb{LPG}_{\mathrm{!}}$ , and extend the game semantics to subtyping on dependent types in Section 4.8.

4.1 Dependent predicate games

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

Definition 4.1.1 (linearly dependent and dependent predicate games). A linearly dependent predicate (p-) game over a p-game $\Gamma$ is a pair $L = (|L|, \| L \|)$ of a game $|L|$ and a family $\| L \| = \{ L(\gamma_0) \}_{\gamma_0 \in \mathbb{WPG}_{\mathrm{!}}(\Gamma)}$ of p-games $L(\gamma_0)$ such that $|L(\gamma_0)| = |L|$ . Moreover:

• • 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 (2022) defines p-games $\mathcal{U}$ that interpret universes (Martin-Löf 1975) 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.¹⁶

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:

Theorem 4.2.2 (well-defined linear-Pi). Given a (well-opened, well-founded) linearly dependent p-game L over a (well-opened, well-founded) p-game $\Gamma$ , the linear-Pi $\Pi_\ell(\Gamma, L)$ is a (well-opened, well-founded) p-game.

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.

Example 4.2.3 A strategy $\zeta : \Pi(N, \mathrm{List}_N)$ plays as the dependent function $n \in \mathbb{N} \mapsto (0, 0, \dots, 0) \in \mathbb{N}^n$ as follows. If O makes the first move $q_{[k]}$ ( $k \in \mathbb{N}_+$ ) on the codomain $|\mathrm{List}_N|$ , where $(\_)_{[k]}$ is the ‘tag’ on the kth component in the tensor $N_{[1]} \otimes N_{[2]} \otimes \dots$ , then $\zeta$ asks the question $q_{[0]}$ on the domain ${\mathrm{!}} N_{[0]}$ , where $(\_)_{[0]}$ is another ‘tag.’ Next, if O plays by $q_{[k]}q_{[0]} \mapsto n_{[0]}$ ( $n \in \mathbb{N}_+$ ), then $\zeta$ plays by $q_{[k]}q_{[0]}n_{[0]} \mapsto 0_{[k]}$ . If $k \leqslant n$ , then the strategy $\underline{n}^\dagger \in \mathbb{WPG}_{\mathrm{!}}({\mathrm{!}} N)$ on the domain is not yet excluded; $\zeta$ is compatible with this possibility since its computation so far is within the subgame $N \Rightarrow \mathrm{List}_N(\underline{n}^\dagger) \subseteq |\Pi(N, \mathrm{List}_N)|$ .

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:

Definition 4.3.1 (Sigma). The Sigma of a p-game $\Gamma$ and a dependent p-game A over $\Gamma$ is the p-game $\Sigma (\Gamma, A)$ defined 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.

Theorem 4.3.2 (well-defined Sigma). Given a (well-opened, well-founded) dependent p-game A over a (well-opened, well-founded) p-game $\Gamma$ , the Sigma $\Sigma(\Gamma, A)$ is a (well-opened, well-founded) p-game.

Proof. Straightforward and left to the reader.

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.¹⁷ Then, our definition of $\Sigma(\Gamma, A)$ meets this nontrivial requirement (Theorem 4.4.3).

Example 4.3.3 The Sigmas $\Sigma(N, \mathrm{List}_N)$ and $\Sigma(N, N_b)$ formalise the two examples given at the beginning of Section 3, respectively.

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. (2015), Vákár et al. (2018), 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. 2018, 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. 2018, 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. (2015), Vákár et al. (2018) but also accurately interpret Pi and Sigma types.

Finally, recall that the interpretation of Sigma types given by Blot and Laird (2018) 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 (1996):

Definition 4.4.1. (CwFs (Dybjer 1996; Hofmann 1997)). A category with families (CwF) is a tuple $\mathcal{C} = (\mathcal{C}, \mathrm{Ty}, \mathrm{Tm}, \_\{\_\}, T, \_.\_, \mathrm{p}, \mathrm{v}, \langle\_,\_\rangle_\_)$ , where

• • $\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 (1997) for the details.

Let us now turn to our game-semantic CwF:

Definition 4.4.2 (a game-semantic CwF). A CwF $\mathbb{WPG}_{\mathrm{!}}$ is defined as follows:

• • 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.

Theorem 4.4.3 (a well-defined game-semantic CwF). The category $\mathbb{WPG}_{\mathrm{!}}$ together with the structures defined in Definition 4.4.2 gives rise to a CwF.

Proof. We focus on the substitution of terms, the second projections and the extensions since the other structures of $\mathbb{WPG}_{\mathrm{!}}$ are straightforward to check (e.g., the equational axioms on morphisms and terms in $\mathbb{WPG}_{\mathrm{!}}$ simply follow from Theorem 3.2.12). Let $\Gamma, \Delta \in \mathbb{WPG}_{\mathrm{!}}$ , $A \in \mathscr{D}^{\mathrm{w}}(\Gamma)$ , $\phi \in \mathbb{WPG}_{\mathrm{!}}(\Delta, \Gamma)$ , $\alpha \in \mathbb{WPG}_{\mathrm{!}}(\Gamma, A)$ and .

On the substitution $\alpha \{ \phi \} = \alpha \bullet \phi \in \mathbb{WPG}_{\mathrm{!}}(|\Delta|, |A|)$ ,¹⁸ 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.

Terms in the CwF $\mathbb{WPG}_{\mathrm{!}}$ are simply a certain class of strategies, and constructions on terms are those on strategies. This is quite desirable because it implies that the results and the techniques on existing game semantics are also available for our game semantics. It also implies that our game semantics inherits the advantages of existing game semantics (Section 1.2) such as intensionality (Section 4.6).

4.5 Game-semantic type formers

Nevertheless, CwFs only interpret the fragment of MLTT common to all types. Hence, in this section, we equip the CwF $\mathbb{WPG}_{\mathrm{!}}$ with the semantic type formers (Hofmann 1997) for the One, the Zero, the N, Pi, Sigma and Id types.

4.5.1 Game semantics of Pi types

We begin with Pi types. We first recall their semantics in an arbitrary CwF:

Definition 4.5.1.1 (CwFs with Pi types (Hofmann 1997)). A CwF $\mathcal{C}$ has Pi types if

• • ( $\Pi$ -Form) Given an object $\Gamma \in \mathcal{C}$ and types $A \in \mathrm{Ty}(\Gamma)$ and $B \in \mathrm{Ty}(\Gamma . A)$ , there is a type $\Pi (A, B) \in \mathrm{Ty}(\Gamma)$ , where we write $A \Rightarrow B$ for $\Pi (A, B)$ if $B\{ \langle \mathrm{id}_\Gamma, \alpha \rangle \} = B\{ \langle \mathrm{id}_\Gamma, \alpha' \rangle \} \in \mathrm{Ty}(\Gamma)$ for all $\alpha, \alpha' \in \mathrm{Tm}(\Gamma, A)$ ;

• • ( $\Pi$ -Intro) Given a term $\beta \in \mathrm{Tm}(\Gamma . A, B)$ , there is a term $\lambda_{A, B} (\beta) \in \mathrm{Tm}(\Gamma, \Pi (A, B))$ ;

• • ( $\Pi$ -Elim) Given terms $\kappa \in \mathrm{Tm}(\Gamma, \Pi (A, B))$ and $\alpha \in \mathrm{Tm}(\Gamma, A)$ , there is a term $\mathrm{App}_{A, B} (\kappa, \alpha) \in \mathrm{Tm}(\Gamma, B\{ \overline{\alpha} \})$ , where $\overline{\alpha} := \langle \mathrm{id}_\Gamma, \alpha \rangle_A : \Gamma \to \Gamma . A$ ;

• • ( $\Pi$ -Comp) $\mathrm{App}_{A, B} (\lambda_{A, B} (\beta) , \alpha) = \beta \{ \overline{\alpha} \}$ ;

• • ( $\Pi$ -Subst) $\Pi (A, B) \{ \phi \} = \Pi (A\{\phi\}, B\{\phi_A^+\})$ for all $\Delta \in \mathcal{C}$ and $\phi : \Delta \to \Gamma$ , where $\phi_A^+ := \langle \phi \circ \mathrm{p}_{A\{ \phi \}}, \mathrm{v}_{A\{ \phi \}} \rangle_A : \Delta . A\{ \phi \} \to \Gamma . A$ ;

• • ( $\lambda$ -Subst) $\lambda_{A, B} (\beta) \{ \phi \} = \lambda_{A\{\phi\}, B\{\phi_A^+\}} (\beta \{ \phi_A^+ \}) \in \mathrm{Tm} (\Delta, \Pi (A\{\phi\}, B\{ \phi_A^+\}))$ ;

• • (App-Subst) $\mathrm{App}_{A, B} (\kappa, \alpha) \{ \phi \} = \mathrm{App}_{A\{\phi\}, B\{\phi_A^+\}} (\kappa \{ \phi \}, \alpha \{ \phi \}) \in \mathrm{Tm} (\Delta, B\{ \overline{\alpha} \} \{ \phi \})$ .

Furthermore, $\mathcal{C}$ strictly has Pi types if it additionally satisfies

• • ( $\lambda$ -Uniq) $\lambda_{A, B} \circ \mathrm{App}_{A\{\mathrm{p}_A\}, B\{(\mathrm{p}_A)_{A\{\mathrm{p}_A\}}^+\}}(\kappa\{ \mathrm{p}_A \}, \mathrm{v}_A) = \kappa$ .

Pi types (with $\eta$ -rule) are modelled in a CwF that (strictly) has Pi types (Hofmann 1997). Let us next show that the CwF $\mathbb{WPG}_{\mathrm{!}}$ strictly has Pi types.

Lemma 4.5.1.2 (dependent currying). Given $\Gamma \in \mathbb{WPG}_{\mathrm{!}}$ , $A \in \mathscr{D}^{\mathrm{w}}(\Gamma)$ and $B \in \mathscr{D}^{\mathrm{w}}(\Sigma(\Gamma, A))$ , there is a bijection

(5) \begin{equation}\lambda_{A, B} : \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Gamma, A), B) \stackrel{\sim}{\rightarrow} \mathbb{WPG}_{\mathrm{!}}(\Gamma, \Pi(A, B)),\end{equation}

where $\Pi(A, B) \in \mathscr{D}^{\mathrm{w}}(\Gamma)$ is defined by

and $B_{\gamma_0^\dagger} \in \mathscr{D}^{\mathrm{w}}(A(\gamma_0^\dagger))$ by

Proof. Let $\phi \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Gamma, A), B)$ . Let us first construct $\phi' \in \mathbb{WPG}_{\mathrm{!}}(\Gamma, \Pi(A, B))$ from $\phi$ as follows. By the evident isomorphism $|{\mathrm{!}} \Sigma(\Gamma, A)| = {\mathrm{!}} (|\Gamma| \mathbin{\&} |A|) \cong {\mathrm{!}} |\Gamma| \otimes {\mathrm{!}} |A|$ , we adjust ‘tags’ or curry $\phi$ with respect to the adjunction between tensor $\otimes$ and linear implication $\multimap$ (McCusker 1998), obtaining another strategy $\phi' : |\Gamma| \Rightarrow (|A| \Rightarrow |B|)$ .

Next, let us show $\overline{\phi'}_{|\Pi(\Gamma, \Pi(A, B))|} \preccurlyeq \Pi(\Gamma, \Pi(A, B))(\phi')$ by induction on the length of positions, where again the only nontrivial case is the inductive step on even-length positions. This inductive step goes through by $\phi \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Gamma, A), B)$ thanks to the correspondence between the constraints on $\Pi(\Sigma(\Gamma, A), B)(\phi)$ and $\Pi(\Gamma, \Pi(A, B))(\phi')$ .

Besides, the same argument also proves that $\phi' \cap \Pi(\Gamma, \Pi(A, B))(\phi') : \Pi(\Gamma, \Pi(A, B))(\phi')$ is winning and well-bracketed, so we have shown $\lambda_{A, B}(\phi) := \phi' \in \mathbb{WPG}_{\mathrm{!}}(\Gamma, \Pi(A, B))$ .

Finally, the inverse of this construction $\lambda_{A, B}$ is given in the same vein.

Example 4.5.1.3 We define a dependent p-game $N_b^+ \in \mathscr{D}^{\mathrm{w}}(\Sigma(N, N_b))$ by $|N_b^+| := N$ and $N_b^+(\langle \underline{k}, \underline{n} \rangle^\dagger) := N_b((\underline{k+n})^\dagger)$ for all $k, n \in \mathbb{N}$ such that $k \geqslant n$ . Lemma 4.5.1.2 allows us to obtain $\lambda_{N_b, N_b^+}(\mathrm{der}_N) \in \mathbb{WPG}_{\mathrm{!}}(N, \Pi(N_b, N_b^+))$ from $\mathrm{der}_N = \mathrm{v}_{N_b^+} \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(N, N_b), N_b^+)$ .

Theorem 4.5.1.4 (game semantics of Pi types). The CwF $\mathbb{WPG}_{\mathrm{!}}$ strictly has Pi types.

Proof. Let $\Gamma \in \mathbb{WPG}_{\mathrm{!}}$ , $A \in \mathscr{D}^{\mathrm{w}}(\Gamma)$ , $B \in \mathscr{D}^{\mathrm{w}}(\Sigma(\Gamma, A))$ and $\beta \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Gamma, A), B)$ .

• • ( $\Pi$ -Form) $\Pi(A, B) \in \mathscr{D}^{\mathrm{w}}(\Gamma)$ is defined in Lemma 4.5.1.2.

• • $\Pi$ -Intro) By Lemma 4.5.1.2, we obtain $\lambda_{A, B} (\beta) \in \mathbb{WPG}_{\mathrm{!}}(\Gamma, \Pi(A, B))$ .

• • ( $\Pi$ -Elim) We define $\mathrm{App}_{A, B} (\kappa, \alpha) := \lambda_{A, B}^{-1}(\kappa) \{\overline{\alpha} \}$ for all $\kappa \in \mathbb{WPG}_{\mathrm{!}}(\Gamma, \Pi(A, B))$ and $\alpha \in \mathbb{WPG}_{\mathrm{!}}(\Gamma, A)$ . By Theorem 4.4.3, $\mathrm{App}_{A, B} (\kappa, \alpha) = \lambda_{A, B}^{-1}(\kappa) \{ \overline{\alpha} \} \in \mathbb{WPG}_{\mathrm{!}}(\Gamma, B\{ \overline{\alpha} \})$ .

• • ( $\Pi$ -Comp) $\mathrm{App}_{A, B} (\lambda_{A, B} (\beta) , \alpha) = \lambda_{A, B}^{-1}(\lambda_{A, B}(\beta)) \{ \overline{\alpha} \} = \beta \{ \overline{\alpha} \}$ .

• • ( $\Pi$ -Subst) Let $\Delta \in \mathbb{WPG}_{\mathrm{!}}$ and $\phi \in \mathbb{WPG}_{\mathrm{!}}(\Delta, \Gamma)$ . For the first components, we have

  \begin{align*}| \Pi (A, B) \{ \phi \} | &= |\Pi(A, B)| \\&= |A| \Rightarrow |B| \\&= |A\{ \phi \} | \Rightarrow |B\{ \phi_A^+ \})| \\&= | \Pi(A\{ \phi \}, B\{ \phi_A^+ \}) |.\end{align*}

For the second components, we have

\begin{align*}\textstyle \Pi (A, B) \{ \phi \} &= (\Pi (A(\phi^\dagger \circ \delta_0^\dagger), B_{\phi^\dagger \circ \delta_0^\dagger}))_{\delta_0^\dagger \in \mathbb{WPG}_{\mathrm{!}}({\mathrm{!}} \Delta)} \\&= (\Pi (A\{ \phi \}(\delta_0^\dagger), B\{ \phi_A^+ \}_{\delta_0^\dagger}))_{\delta_0^\dagger \in \mathbb{WPG}_{\mathrm{!}}({\mathrm{!}} \Delta)} \\&= \Pi(A\{ \phi \}, B\{ \phi_A^+ \}),\end{align*}

where the second equation holds since for all

we have

We have shown $\| \Pi (A, B) \{ \phi \} \| = \| \Pi(A\{ \phi \}, B\{ \phi_A^+ \}) \|$ .

• • ( $\lambda$ -Subst) By the definition of $\lambda$ , we have $\lambda_{A, B} (\beta) \{ \phi \} = \lambda_{A\{\phi\}, B\{\phi_A^+\}} (\beta \{ \phi_A^+ \})$ .

• • (App-Subst) We have

  \begin{align*}\mathrm{App}_{A, B} (\kappa, \alpha) \{ \phi \} &= \lambda_{A, B}^{-1} (\kappa) \{ \langle \mathrm{der}_{|\Gamma|}, \alpha \rangle \bullet \phi \} \\&= \lambda_{A, B}^{-1} (\kappa) \{ \langle \phi, \alpha \{ \phi \} \rangle \} \\&= \lambda_{A, B}^{-1} (\kappa) \{ \langle \phi \bullet \mathrm{p}_{A \{ \phi \}}, \mathrm{v}_{A\{\phi\}} \rangle \bullet \langle \mathrm{der}_{|\Delta|}, \alpha \{ \phi \} \rangle \} \\&= \lambda_{A, B}^{-1} (\kappa) \{ \phi_A^+ \} \{ \overline{\alpha \{ \phi \}} \} \\&= \lambda_{A\{ \phi \}, B\{ \phi_A^+ \}}^{-1} (\kappa \{ \phi \}) \{ \overline{\alpha \{ \phi \}} \} \quad \text{(by $\lambda$-Subst)} \\&= \mathrm{App}_{A\{ \phi \}, B\{ \phi_A^+ \}} (\kappa \{ \phi \}, \alpha \{ \phi \}).\end{align*}

• • ( $\lambda$ -Uniq) We have

  \begin{align*}\lambda_{A, B}(\mathrm{App}_{A\{\mathrm{p}_A\}, B\{ \mathrm{p}_A^+ \}}(\kappa\{ \mathrm{p}_A \}, \mathrm{v}_A)) &= \lambda_{A, B}(\lambda^{-1}_{A\{\mathrm{p}_A\}, B\{ \mathrm{p}_A^+ \}}(\kappa\{ \mathrm{p}_A \}) \{ \overline{\mathrm{v}_A} \}) \\&= \lambda_{A, B}(\lambda^{-1}_{A, B}(\kappa) \{ \mathrm{p}_A^+ \} \{ \overline{\mathrm{v}_A} \}) \quad \text{(by $\lambda$-Subst)} \\&= \lambda_{A, B}(\lambda^{-1}_{A, B}(\kappa) \{ \langle \mathrm{p}_A \bullet \mathrm{p}_{A\{ \mathrm{p}_A \}}, \mathrm{v}_{A\{ \mathrm{p}_A \}} \rangle \bullet \langle \mathrm{der}_{|\Sigma(\Gamma, A)|}, \mathrm{v}_A \rangle \}) \\&= \lambda_{A, B}(\lambda^{-1}_{A, B}(\kappa) \bullet \langle \mathrm{p}_A, \mathrm{v}_A \rangle) \\&= \lambda_{A, B}(\lambda^{-1}_{A, B}(\kappa) \bullet \mathrm{der}_{|\Sigma(\Gamma, A)|}) \\&= \lambda_{A, B}(\lambda^{-1}_{A, B}(\kappa)) \\&= k,\end{align*}

which completes the proof.

4.5.2 game semantics of Sigma types

Next, we consider Sigma types. Again, we first recall their semantics in an arbitrary CwF:

Definition 4.5.2.1 (CwFs with Sigma types (Hofmann 1997)). A CwF $\mathcal{C}$ has Sigma types if

• • ( $\Sigma$ -Form) Given an object $\Gamma \in \mathcal{C}$ and types $A \in \mathrm{Ty}(\Gamma)$ and $B \in \mathrm{Ty}(\Gamma . A)$ , there is a type $\Sigma (A, B) \in \mathrm{Ty}(\Gamma)$ , where we write $A \times B$ for $\Sigma (A, B)$ if $B\{ \langle \mathrm{id}_\Gamma, \alpha \rangle \} = B\{ \langle \mathrm{id}_\Gamma, \alpha' \rangle \} \in \mathrm{Ty}(\Gamma)$ for all $\alpha, \alpha' \in \mathrm{Tm}(\Gamma, A)$ ;

• • ( $\Sigma$ -Intro) There is a morphism $\mathrm{Pair}_{A, B} : \Gamma . A . B \to \Gamma . \Sigma (A, B)$ in $\mathcal{C}$ ;

• • ( $\Sigma$ -Elim) Given a type $P \in \mathrm{Ty}(\Gamma . \Sigma (A, B))$ and a term $\rho \in \mathrm{Tm}(\Gamma . A . B, P \{ \mathrm{Pair}_{A, B} \})$ , there is a term $\mathcal{R}^{\Sigma}_{A, B, P}(\rho) \in \mathrm{Tm}(\Gamma . \Sigma (A, B), P)$ ;

• • ( $\Sigma$ -Comp) $\mathcal{R}^{\Sigma}_{A, B, P}(\rho) \{ \mathrm{Pair}_{A, B}\} = \rho$ ;

• • ( $\Sigma$ -Subst) $\Sigma (A, B) \{ \phi \} = \Sigma (A\{\phi\}, B\{\phi_A^+\})$ for all $\Delta \in \mathcal{C}$ and $\phi : \Delta \to \Gamma$ in $\mathcal{C}$ ;

• • (Pair-Subst) $\mathrm{p}_{\Sigma (A, B)} \circ \mathrm{Pair}_{A, B} = \mathrm{p}_A \circ \mathrm{p}_B$ and $\phi_{\Sigma(A, B)}^+ \circ \mathrm{Pair}_{A\{\phi\}, B\{\phi_A^+\}} = \mathrm{Pair}_{A, B} \circ \phi^{++}_{A, B}$ , where $\phi^{++}_{A, B} := (\phi_A^+)^+_B : \Delta . A\{\phi\} . B\{\phi_A^+\} \to \Gamma . A . B$ ;

• • ( $\mathcal{R}^{\Sigma}$ -Subst) $\mathcal{R}^{\Sigma}_{A, B, P}(p) \{\phi^+_{\Sigma(A, B)}\} = \mathcal{R}^{\Sigma}_{A\{f\}, B\{\phi_A^+\}, P\{\phi^+_{\Sigma(A, B)}\}} (p \{ \phi_{A, B}^{++} \})$ .

In addition, $\mathcal{C}$ strictly has Sigma types if it also satisfies

• • ( $\mathcal{R}^{\Sigma}$ -Uniq) if and .

Sigma types (with $\eta$ -rule) are interpreted in a CwF that (strictly) has Sigma types (Hofmann 1997). Now, we show that our CwF $\mathbb{WPG}_{\mathrm{!}}$ strictly has Sigma types:

Theorem 4.5.2.2 (game semantics of Sigma types). The CwF $\mathbb{WPG}_{\mathrm{!}}$ strictly has Sigma types.

Proof. Let $\Gamma \in \mathbb{WPG}_{\mathrm{!}}$ , $A \in \mathscr{D}^{\mathrm{w}}(\Gamma)$ , $B \in \mathscr{D}^{\mathrm{w}}(\Sigma(\Gamma, A))$ and $P \in \mathscr{D}^{\mathrm{w}}(\Sigma(\Gamma, \Sigma(A,B)))$ .

• • ( $\Sigma$ -Form) Similarly to Pi, we define

  \begin{equation*}\Sigma (A, B) := (|A| \mathbin{\&} |B|, (\Sigma(A(\gamma_0^\dagger), B_{\gamma_0^\dagger}))_{\gamma_0^\dagger \in \mathbb{WPG}_{\mathrm{!}}({\mathrm{!}} \Gamma)}).\end{equation*}

• • ( $\Sigma$ -Intro) By the evident bijection $\Sigma(\Sigma(\Gamma,A),B) \cong \Sigma(\Gamma, \Sigma(A,B))$ , we define $\mathrm{Pair}_{A, B}$ to be the dereliction up to ‘tags,’ i.e.,

  \begin{equation*}\mathrm{Pair}_{A, B} := \langle \mathrm{p}_A \bullet \mathrm{p}_B, \langle \mathrm{v}_A \{ \mathrm{p}_B \}, \mathrm{v}_B \rangle \rangle.\end{equation*}

Note that the inverse $\mathrm{Pair}^{-1}_{A, B}$ is the pairing $\langle \langle \mathrm{p}_{\Sigma(A, B)}, \varpi^{A, B}_1 \rangle, \varpi^{A, B}_2 \rangle$ , where $\varpi^{A, B}_1 : \Sigma(\Gamma, \Sigma(A, B)) \rightarrow A \{ \mathrm{p}_{\Sigma(A, B)} \}$ and $\varpi^{A, B}_2 : \Sigma(\Gamma, \Sigma(A, B)) \rightarrow B \{ \langle \mathrm{p}_{\Sigma(A, B)}, \varpi^{A, B}_1 \rangle \}$ are the evident derelictions up to ‘tags.’

• • ( $\Sigma$ -Elim) Given $\rho \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Sigma(\Gamma, A), B), P\{\mathrm{Pair}_{A,B}\})$ , we define

  \begin{align*}\mathcal{R}^{\Sigma}_{A, B, P}(\rho) & := \rho \{ \mathrm{Pair}_{A, B}^{-1} \} \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Gamma, \Sigma (A, B)), P\{\mathrm{Pair}_{A,B}\}\{\mathrm{Pair}_{A,B}^{-1}\})\\ &= \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Gamma, \Sigma (A, B)), P).\end{align*}

• • ( $\Sigma$ -Comp) We have

  \begin{align*}\mathcal{R}^{\Sigma}_{A, B, P}(\rho) \{ \mathrm{Pair}_{A, B}\} &= \rho \{ \mathrm{Pair}_{A, B}^{-1} \} \{ \mathrm{Pair}_{A, B} \} \\&= \rho \{ \mathrm{Pair}_{A, B}^{-1} \bullet \mathrm{Pair}_{A, B} \} \\&= \rho \{ \mathrm{id}_{\Sigma(\Sigma(\Gamma, A), B)} \} \\&= \rho.\end{align*}

• • ( $\Sigma$ -Subst) Similar to the case of Pi (Theorem 4.5.1.4).

• • (Pair-Subst) $\mathrm{p}_{\Sigma (A, B)} \bullet \mathrm{Pair}_{A, B} = \mathrm{p}_{\Sigma (A, B)} \bullet \langle \mathrm{p}_A \bullet \mathrm{p}_B, \langle \mathrm{v}_A \{ \mathrm{p}_B \}, \mathrm{v}_B \rangle \rangle \notag = \mathrm{p}_A \bullet \mathrm{p}_B$ , and

  \begin{align*}\!\!\!\!\!\phi^+_{\Sigma(A, B)} \bullet \mathrm{Pair}_{A\{\phi\}, B\{\phi_A^+\}} &= \langle \phi \bullet \mathrm{p}_{\Sigma(A,B)\{\phi\}}, \mathrm{v}_{\Sigma(A,B)\{\phi\}} \rangle \bullet \mathrm{Pair}_{A\{\phi\}, B\{\phi_A^+\}} \\&= \langle \phi \bullet \mathrm{p}_{\Sigma(A\{\phi\},B\{\phi_A^+\})} \bullet \mathrm{Pair}_{A\{\phi\}, B\{\phi_A^+\}}, \mathrm{v}_{\Sigma(A,B)\{\phi\}} \{ \mathrm{Pair}_{A\{ \phi \}, B\{ \phi_A^+ \}} \}\rangle \\&= \langle \phi \bullet \mathrm{p}_{A\{ \phi \}} \bullet \mathrm{p}_{B\{ \phi_A^+ \}}, \mathrm{v}_{\Sigma(A\{ \phi \},B\{ \phi_A^+ \})} \{ \mathrm{Pair}_{A\{ \phi \}, B\{ \phi_A^+ \}} \} \rangle\\& \quad\hspace{190pt} \text{(by the above equation)} \\&= \langle \phi \bullet \mathrm{p}_{A\{ \phi \}} \bullet \mathrm{p}_{B\{ \phi_A^+ \}}, \langle \mathrm{v}_{A\{\phi\}} \{ \mathrm{p}_{B\{ \phi_A^+ \}} \}, \mathrm{v}_{B\{ \phi_A^+ \}} \rangle \rangle \\&= \langle \mathrm{p}_A \bullet \mathrm{p}_B, \langle \mathrm{v}_A \{ \mathrm{p}_B \}, \mathrm{v}_B \rangle \rangle \bullet \langle \langle \phi \bullet \mathrm{p}_{A\{ \phi \}} \bullet \mathrm{p}_{B\{ \phi_A^+ \}}, \mathrm{v}_{A\{ \phi \}}\{ \mathrm{p}_{B\{ \phi_A^+ \}} \} \rangle, \mathrm{v}_{B\{ \phi_A^+ \}} \rangle \\&= \langle \mathrm{p}_A \bullet \mathrm{p}_B, \langle \mathrm{v}_A \{ \mathrm{p}_B \}, \mathrm{v}_B \rangle \rangle \bullet \langle \langle \phi \bullet \mathrm{p}_{A\{ \phi \}}, \mathrm{v}_{A\{ \phi \}} \rangle \bullet \mathrm{p}_{B\{ \phi_A^+ \}}, \mathrm{v}_{B\{ \phi_A^+ \}} \rangle \\&= \mathrm{Pair}_{A, B} \bullet \langle \phi_A^+ \bullet \mathrm{p}_{B\{ \phi_A^+ \}}, \mathrm{v}_{B\{ \phi_A^+ \}} \rangle \\&= \mathrm{Pair}_{A, B} \bullet \phi_{A, B}^{++}.\end{align*}

• • ( $\mathcal{R}^{\Sigma}$ -Subst) We have

  \begin{align*}\mathcal{R}^{\Sigma}_{A, B, P}(\rho) \{ \phi^+_{\Sigma(A, B)} \} &= \rho \{ \mathrm{Pair}_{A, B}^{-1} \} \{ \langle \phi \bullet \mathrm{p}_{\Sigma(A,B)\{ \phi \}}, \mathrm{v}_{\Sigma(A,B)\{ \phi \}} \rangle \} \\&= \rho \{ \langle \langle \mathrm{p}_{\Sigma(A, B)}, \varpi^{A, B}_1 \rangle, \varpi^{A, B}_2 \rangle \bullet \langle \phi \bullet \mathrm{p}_{\Sigma(A,B)\{ \phi \}}, \mathrm{v}_{\Sigma(A,B)\{ \phi \}} \rangle \} \\&= \rho \{ \langle \langle \phi \bullet \mathrm{p}_{\Sigma(A, B)\{ \phi \}}, \varpi^{A\{ \phi \}, B\{ \phi_A^+ \}}_1 \rangle, \varpi^{A\{ \phi \}, B\{ \phi_A^+ \}}_2 \rangle \} \\&\quad \hspace{155pt}\text{(by the definition of $\varpi_1$ and $\varpi_2$)} \\&= \rho \{ \langle \langle \phi \bullet \mathrm{p}_{A\{ \phi \}}, \mathrm{v}_{A\{\phi\}} \rangle \bullet \mathrm{p}_{B\{ \phi_A^+ \}}, \mathrm{v}_{B\{ \phi_A^+ \}} \rangle \}\\ & \quad \{ \langle \langle \mathrm{p}_{\Sigma(A, B)\{ \phi \}}, \varpi^{A\{ \phi \}, B\{ \phi_A^+ \}}_1 \rangle, \varpi^{A\{ \phi \}, B\{ \phi_A^+ \}}_2 \rangle \} \\&= \rho \{ \langle \phi_A^+ \bullet \mathrm{p}_{B\{ \phi_A^+ \}}, \mathrm{v}_{B\{ \phi_A^+ \}} \rangle \} \{ \mathrm{Pair}_{A\{ \phi \}, B\{ \phi_A^+ \}}^{-1} \} \\&= \mathcal{R}^{\Sigma}_{A\{ \phi \}, B\{ \phi_A^+ \}, P\{ \phi_{\Sigma(A, B)}^+ \}} (\rho \{ \phi_{A, B}^{++} \}).\end{align*}

• • ( $\mathcal{R}^{\Sigma}$ -Uniq) Given with , we have

  

which completes the proof.

4.5.3 Game semantics of the N type

We next present our game semantics of the N type. Again, we first recall its semantics in an arbitrary CwF:

Definition 4.5.3.1 (CwFs with the N type (Hofmann 1997)). A CwF $\mathcal{C}$ has the N type if

• • (N-Form) There is a type $N^{[\Gamma]} \in \mathrm{Ty}(\Gamma)$ for each $\Gamma \in \mathcal{C}$ . We abbreviate it as N.

• • (N-Intro) There are a term $\underline{0}_{\Gamma} \in \mathrm{Tm}(\Gamma, N)$ and a morphism $\mathrm{succ}_{\Gamma} : \Gamma . N \to \Gamma . N$ in $\mathcal{C}$ that satisfy, for all $\phi : \Delta \to \Gamma$ and $\psi : \Delta . N \to \Gamma$ in $\mathcal{C}$ , the equations

  

  where the last equation makes sense as we have $\mathrm{succ}_{\Gamma} \circ \langle \psi, \mathrm{v}_{N} \rangle_{N}, \langle \psi, \mathrm{v}_{N}\{\mathrm{succ}_{\Delta}\} \rangle_{N} : \Delta . N \to \Gamma . N$ by N-Subst given below.

Notation 4.5.3.2. Let $\mathrm{zero}_\Gamma := \langle \mathrm{id}_\Gamma, \underline{0}_\Gamma \rangle_N : \Gamma \to \Gamma . N$ for all $\Gamma \in \mathcal{C}$ , which satisfies $\mathrm{zero}_\Gamma \circ \phi = \langle \phi, \underline{0}_\Delta \rangle_N = \langle \phi, \mathrm{v}_N \{ \mathrm{zero}_\Delta \} \rangle_N : \Delta \to \Gamma . N$ for all $\phi : \Delta \to \Gamma$ in $\mathcal{C}$ . We define $\underline{n}_\Gamma \in \mathrm{Tm}(\Gamma, N)$ for all $n \in \mathbb{N}$ : $\underline{0}_\Gamma$ is already given, and $\underline{n+1}_\Gamma := \mathrm{v}_N \{ \mathrm{succ}_\Gamma \circ \langle \mathrm{id}_\Gamma, \underline{n}_\Gamma \rangle_N \}$ .

• • (N-Elim) Given a type $P \in \mathrm{Ty}(\Gamma . N)$ and terms $c_{\mathrm{z}} \in \mathrm{Tm}(\Gamma, P\{\mathrm{zero}\})$ and $c_{\mathrm{s}} \in \mathrm{Tm}(\Gamma . N . P, P\{ \mathrm{succ} \circ \mathrm{p}_P\})$ , there is a term $\mathcal{R}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}}) \in \mathrm{Tm}(\Gamma . N, P)$ ;

• • (N-Comp) We have

  \begin{align*}\mathcal{R}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}}) \{ \mathrm{zero} \} &= c_{\mathrm{z}} \in \mathrm{Tm}(\Gamma, P\{\mathrm{zero}\}); \\\mathcal{R}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}}) \{ \mathrm{succ} \} &= c_{\mathrm{s}} \{ \langle \mathrm{id}_{\Gamma . N}, \mathcal{R}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}}) \rangle_{P} \} \in \mathrm{Tm}(\Gamma . N, P\{\mathrm{succ}\});\end{align*}

• • (N-Subst) $N^{[\Gamma]}\{\phi\} = N^{[\Delta]} \in \mathrm{Ty}(\Delta)$ ;

• • ( $\mathcal{R}^{N}$ -Subst) $\mathcal{R}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}}) \{\phi_N^+\} = \mathcal{R}^{N}_{P\{\phi_N^+\}}(c_{\mathrm{z}}\{\phi\}, c_{\mathrm{s}}\{\phi_{N, P}^{++}\}) \in \mathrm{Tm}(\Delta . N, P\{\phi_N^+\})$ .

The N type is interpreted in a CwF that has the N type (Hofmann 1997). Let us now present our game semantics of the N type, which is based on the standard game semantics of the functional programming language PCF (Abramsky and McCusker 1999b):

Theorem 4.5.3.3 (game semantics of the N type). The CwF $\mathbb{WPG}_{\mathrm{!}}$ has the N type.

Proof. Let $\Gamma, \Delta \in \mathbb{WPG}_{\mathrm{!}}$ , $\phi \in \mathbb{WPG}_{\mathrm{!}}(\Delta, \Gamma)$ and $\psi \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Delta, \{ N \}_{{\mathrm{!}} \Delta}), \Gamma)$ .

• • (N-Form) $N^{[\Gamma]} := \{ N \}_{{\mathrm{!}} \Gamma} \in \mathscr{D}^{\mathrm{w}}(\Gamma)$ , where N is defined in Example 3.1.5.

• • (N-Intro) Let $\underline{0}_\Gamma \in \mathbb{WPG}_{\mathrm{!}}(\Gamma, \{ N \})$ be $\underline{0} : N$ (Examples 2.2.5 and 3.1.5) up to ‘tags,’ and $\mathrm{succ}_\Gamma := \langle \mathrm{p}, \mathrm{sc}_\Gamma \rangle \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Gamma, \{ N \}), \Sigma(\Gamma, \{ N \}))$ , where

  \begin{equation*}\mathrm{sc}_\Gamma := \mathrm{Pref}(\{ \, q_{[1]}q_{[0]}n_{[0]}(n+1)_{[1]} \mid n \in \mathbb{N} \, \})^{\mathrm{Even}} \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Gamma, \{ N_{[0]} \}), \{ N_{[1]} \}).\end{equation*}

Clearly, we have $\underline{0}_\Gamma \bullet \phi = \underline{0}_\Delta$ and $\mathrm{sc}_\Gamma \bullet \langle \psi, \mathrm{v}_{\{N\}_\Delta} \rangle = \mathrm{sc}_\Delta = \mathrm{v}_{\{N\}_\Delta}\{ \mathrm{succ}_\Delta \}$ , so the required three equations hold.

• • (N-Elim) Given a type $P \in \mathscr{D}^{\mathrm{w}}(\Sigma(\Gamma, \{ N \}))$ and terms $c_{\mathrm{z}} \in \mathbb{WPG}_{\mathrm{!}}(\Gamma, P\{ \mathrm{zero} \})$ and $c_{\mathrm{s}} \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Sigma(\Gamma, \{ N \}), P), P\{ \mathrm{succ} \bullet \mathrm{p}_P\})$ , there are terms

  \begin{align*}&\widetilde{c}_{\mathrm{z}} \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Pi(\Sigma(\Gamma, \{N\}), P), \{ \Sigma(\Gamma, \{ N \}) \}), P\{ \mathrm{zero} \bullet \mathrm{p} \bullet \mathrm{v} \}); \\&\widetilde{c}_{\mathrm{s}} \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Pi(\Sigma(\Gamma, \{N\}), P), \{ \Sigma(\Gamma, \{ N \}) \}), P\{ \mathrm{succ} \bullet \mathrm{v} \}),\end{align*}
  where $\mathrm{v} \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Pi(\Sigma(\Gamma, \{N\}), P), \{ \Sigma(\Gamma, \{ N \}) \}), \{ \Sigma(\Gamma, \{ N \}) \} \{ \mathrm{p} \})$ is the constant second projection $\pi_2 \in \mathbb{WPG}_{\mathrm{!}}(\Pi((\Gamma \mathbin{\&} N), P) \mathbin{\&} (\Gamma \mathbin{\&} N ), \Gamma \mathbin{\&} N)$ so that the compositions $\mathrm{p} \bullet \mathrm{v}$ and $\mathrm{succ} \bullet \mathrm{v}$ are well-defined, given respectively by
  \begin{align*}\widetilde{c}_{\mathrm{z}} &:= \big(|\Pi(\Sigma(\Gamma, \{ N \}), P)| \mathbin{\&} |\Sigma(\Gamma, \{ N \})| \stackrel{\mathrm{v}}{\longrightarrow} |\Sigma(\Gamma, \{ N \})| \stackrel{\mathrm{p}}{\longrightarrow} |\Gamma| \stackrel{c_{\mathrm{z}}}{\longrightarrow} |P\{ \mathrm{zero} \}|\big); \\\widetilde{c}_{\mathrm{s}} &:= \big(|\Pi(\Sigma(\Gamma, \{N\}), P)| \mathbin{\&} |\Sigma(\Gamma, \{N\})| \stackrel{\langle \mathrm{v}, \mathrm{ev}_P \rangle}{\longrightarrow} |\Sigma(\Gamma, \{N\})| \mathbin{\&} |P| \stackrel{c_{\mathrm{s}}}{\longrightarrow} \textstyle |P\{ \mathrm{succ} \bullet \mathrm{p} \}|\big),\end{align*}
  where the term $\mathrm{ev}_P \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Pi(\Sigma(\Gamma, \{N\}), P), \{ \Sigma(\Gamma, \{N\}) \}), P\{\mathrm{v}\})$ is the evaluation [Abramsky, 1997], i.e.,
  \begin{equation*}\mathrm{ev}_P := \lambda^{-1}(\mathrm{der}_{\Pi(\Sigma(\Gamma, \{ N \}), P)}).\end{equation*}

Next, we define $\mathrm{pred}_\Gamma := \langle \mathrm{p}, \mathrm{pd}_\Gamma \rangle \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Gamma, \{ N \}), \Sigma(\Gamma, \{ N \}))$ , where

\begin{align*}& \mathrm{pd}_\Gamma := \\ & \mathrm{Pref}(\{ q_{[1]}q_{[0]}0_{[0]}0_{[1]} \} \cup \{ \, q_{[1]}q_{[0]}(n+1)_{[0]}n_{[1]} \mid n \in \mathbb{N} \, \})^{\mathrm{Even}} \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Gamma, \{ N_{[0]} \}), \{ N_{[1]} \}).\end{align*}

Also, let $\mathrm{cond}_P \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Sigma(\Sigma(\Gamma, \{ N \}), P\{ \mathrm{zero} \bullet \mathrm{p} \}), P\{ \mathrm{succ} \bullet \mathrm{pred} \bullet \mathrm{p} \}), P\{ \mathrm{p} \bullet \mathrm{p} \})$ be the game semantics of conditionals (Abramsky and McCusker 1999b): Given any initial move, it asks the number n on N, and plays as the dereliction between $P\{ \mathrm{zero} \bullet \mathrm{p} \}$ and $P\{ \mathrm{p} \bullet \mathrm{p} \}$ if $n = 0$ , and between $P\{ \mathrm{succ} \bullet \mathrm{pred} \bullet \mathrm{p} \}$ and $P\{ \mathrm{p} \bullet \mathrm{p} \}$ otherwise. We then define a morphism $\mathcal{F}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}}) \in \mathbb{WPG}_{\mathrm{!}}(\Pi(\Sigma(\Gamma, \{N\}), P), \Pi(\Sigma(\Gamma, \{N\}), P))$ by

(6) \begin{equation}\mathcal{F}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}}) := \lambda_{\{ \Sigma(\Gamma, \{ N \}) \}, \{ P\{ \mathrm{v} \} \}} (\mathrm{cond}_P \{ \langle \langle \mathrm{v}, \widetilde{c}_{\mathrm{z}} \rangle, \widetilde{c_{\mathrm{s}}}\{ \langle \mathrm{p}, \mathrm{pred} \bullet \mathrm{v} \rangle \} \rangle \}),\end{equation}

which is well-defined thanks to the equation

\begin{align*}(\mathrm{succ} \bullet \mathrm{v}) \bullet \langle \mathrm{p}, \mathrm{pred} \bullet \mathrm{v} \rangle &= \mathrm{succ} \bullet \mathrm{pred} \bullet \mathrm{v} \\&= (\mathrm{succ} \bullet \mathrm{pred} \bullet \mathrm{p}) \bullet \langle \mathrm{v}, \widetilde{c}_{\mathrm{z}} \rangle.\end{align*}

Finally, let $\mathcal{R}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}}) \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Gamma, \{N\}), P)$ be the least upper bound of the chain $(\mathcal{R}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}})_n : \Pi(\Sigma(\Gamma, \{N\}), P))_{n \in \mathbb{N}}$ given by

The main difference from the game semantics of fixed-point combinators (Abramsky and McCusker 1999b) is that the strategy pred occurring in $\mathcal{F}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}})$ (6) decreases the parameter number on the p-game N at every recursive call by $\mathcal{F}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}})$ , so that the term $\mathcal{R}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}})$ is total and noetherian.

• • (N-Comp) By the definition of $\mathcal{R}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}})$ , we clearly have the equations

  \begin{align*}\mathcal{R}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}}) \{ \mathrm{zero} \} &= c_{\mathrm{z}} \in \mathbb{WPG}_{\mathrm{!}}(\Gamma, P \{ \mathrm{zero} \}); \\\mathcal{R}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}}) \{ \mathrm{succ} \} &= c_{\mathrm{s}} \{ \langle \mathrm{der}_{\Sigma(\Gamma, \{N\})}, \mathcal{R}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}}) \rangle \} \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Gamma, \{N\}), P\{ \mathrm{succ} \}).\end{align*}

• • (N-Subst) It is clear that the equation $\{N\}_{{\mathrm{!}} \Gamma}\{ \phi \} = \{N\}_{{\mathrm{!}} \Delta}$ holds.

• • ( $\mathcal{R}^{N}$ -Subst) Finally, by the definition of $\mathcal{R}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}})$ , we clearly have the equation

  \begin{equation*}\mathcal{R}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}}) \{ \phi_N^+ \} = \mathcal{R}^{N}_{P\{ \phi_N^+ \}}(c_{\mathrm{z}}\{ \phi \}, c_{\mathrm{s}}\{ \phi_{N, P}^{++} \})\end{equation*}

(or alternatively we can show $\mathcal{R}^{N}_{P}(c_{\mathrm{z}}, c_{\mathrm{s}})_n \{ \phi_N^+ \} = \mathcal{R}^{N}_{P\{ \phi_N^+ \}}(c_{\mathrm{z}}\{ \phi \}, c_{\mathrm{s}}\{ \phi_{N, P}^{++} \})_n$ for all $n \in \mathbb{N}$ by induction on n so that the above equation holds), which completes the proof.

4.5.4 Game semantics of the One and the Zero types

Next, we interpret the One and the Zero types. Since it is trivial to interpret them, we only sketch a proof. See Hofmann (1997) for the semantic type formers for these types.

Theorem 4.5.4.1 (game semantics of the One and the Zero types). The CwF $\mathbb{WPG}_{\mathrm{!}}$ has the One (in the strict sense) and the Zero types.

Proof (sketch). We interpret the One and the Zero types by the constant dependent p-games at the terminal p-game T and the empty p-game 0, respectively (Example 3.1.5).

The essence of the interpretation of the One type is that there is only the trivial term $\{ \boldsymbol{\epsilon} \} \in \mathbb{WPG}_{\mathrm{!}}(\Gamma, \{ T \})$ for any $\Gamma \in \mathbb{WPG}_{\mathrm{!}}$ , so we can interpret all the rules of the One type.

Finally, the gist of the interpretation of the Zero type is the elimination rule: Given a type $A \in \mathscr{D}^{\mathrm{w}}(\Sigma(\Gamma, \{ 0 \}))$ and a term $\zeta \in \mathbb{WPG}_{\mathrm{!}}(\Gamma, \{ 0 \})$ , we must construct a term $\mathcal{R}^{0}_A(\zeta) \in \mathbb{WPG}_{\mathrm{!}}(\Gamma, A\{ \langle \mathrm{id}_\Gamma, \zeta \rangle \})$ . We define $\mathcal{R}^{0}_A(\zeta)$ to be the one obtained from $\zeta$ by replacing the unique first move q of 0 in $\zeta$ with those of $|A|$ if any, and $\mathcal{R}^{0}_A(\zeta) := \{ \boldsymbol{\epsilon} \}$ otherwise.

4.5.5.1 Game semantics of Id types

Let us next present our game semantics of Id types. Again, we first review the general semantics of Id types in an arbitrary CwF:

Definition 4.5.5.1 (CwFs with Id types (Hofmann 1997)). A CwF $\mathcal{C}$ has Id types if

• • (Id-Form) Given an object $\Gamma \in \mathcal{C}$ and a type $A \in \mathrm{Ty}(\Gamma)$ , there is a type $\mathrm{Id}_A \in \mathrm{Ty}(\Gamma . A . A^+)$ , where $A^+ := A\{\mathrm{p}_A \} \in \mathrm{Ty}(\Gamma . A)$ ;

• • (Id-Intro) There is a morphism $\mathrm{Refl}_A : \Gamma . A \rightarrow \Gamma . A . A^+ . \mathrm{Id}_A$ in $\mathcal{C}$ that satisfies the equation $\mathrm{p}_{\mathrm{Id}_A} \circ \mathrm{Refl}_A = \overline{\mathrm{v}_A} : \Gamma . A \rightarrow \Gamma . A . A^+$ , where $\overline{\mathrm{v}_A} := \langle \mathrm{id}_{\Gamma . A}, \mathrm{v}_{A} \rangle$ ;

• • (Id-Elim) Given a type $B \in \mathrm{Ty}(\Gamma . A . A^+ . \mathrm{Id}_A)$ and a term $\beta \in \mathrm{Tm}(\Gamma . A, B\{\mathrm{Refl}_A\})$ , there is a term $\mathcal{R}^{\mathrm{Id}}_{A,B}(\beta) \in \mathrm{Tm}(\Gamma . A . A^+ . \mathrm{Id}_A, B)$ ;

• • (Id-Comp) $\mathcal{R}^{\mathrm{Id}}_{A,B}(\beta)\{\mathrm{Refl}_A\} = \beta$ ;

• • (Id-Subst) $\mathrm{Id}_A\{\phi_{A, A^+}^{++}\} = \mathrm{Id}_{A\{\phi\}} \in \mathrm{Ty}(\Delta . A\{\phi\} . A\{\phi\}^+)$ ( $\Delta \in \mathcal{C}$ , $\phi : \Delta \to \Gamma$ );

• • (Refl-Subst) $\mathrm{Refl}_A \circ \phi_A^+ = \phi_{A, A^+, \mathrm{Id}_A}^{+++} \circ \mathrm{Refl}_{A\{\phi\}} : \Delta . A\{\phi\} \to \Gamma . A . A^+ . \mathrm{Id}_A$ , where $\phi_{A, A^+, \mathrm{Id}_A}^{+++} := (\phi_{A, A^+}^{++})^+_{\mathrm{Id}_A} : \Delta . A\{\phi\} . A^+\{\phi^+\} . \mathrm{Id}_{A\{\phi\}} \to \Gamma . A . A^+ . \mathrm{Id}_A$ ;

• • ( $\mathcal{R}^{\mathrm{Id}}$ -Subst) $\mathcal{R}^{\mathrm{Id}}_{A,B}(\beta)\{\phi_{A, A^+, \mathrm{Id}_A}^{+++}\} = \mathcal{R}^{\mathrm{Id}}_{A\{\phi\}, B\{\phi_{A, A^+, \mathrm{Id}_A}^{+++}\}}(\beta\{\phi_A^+\})$ .

Id types are modelled in a CwF that has Id types (Hofmann 1997). Then, let us present our game semantics of Id types, which is essentially the same as the interpretation of Id types by Abramsky et al. (2015), Vákár et al. (2018):

Theorem 4.5.5.2 (game semantics of Id types) The CwF $\mathbb{WPG}_{\mathrm{!}}$ has Id types.

Proof. Let $\Gamma \in \mathbb{WPG}_{\mathrm{!}}$ , $A \in \mathscr{D}^{\mathrm{w}}(\Gamma)$ and $B \in \mathscr{D}^{\mathrm{w}}(\Sigma(\Sigma(\Sigma(\Gamma, A), A^+), \mathrm{Id}_A))$ .

• • (Id-Form) Let T’ be the flat game $\mathrm{flat}(\{ \mathbin{\surd} \})$ (Example 2.2.5), where $\{ \mathbin{\surd} \}$ is an arbitrarily fixed singleton set. We then define the type $\mathrm{Id}_A \in \mathscr{D}^{\mathrm{w}}(\Sigma(\Sigma(\Gamma, A), A^+))$ by $|\mathrm{Id}_A| := \mathscr{P}(T')$ and $\mathrm{Id}_A(\langle \langle \gamma_0, \alpha_0 \rangle, \alpha_0' \rangle^\dagger) := \begin{cases} (\mathscr{P}(T'), \kappa_{\mathscr{P}(T')}) &\text{if $\alpha_0 = \alpha_0'$;} \\ (\mathscr{P}(T'), \kappa_{0}) &\text{otherwise} \end{cases}$ for all $\langle \langle \gamma_0, \alpha_0 \rangle, \alpha_0' \rangle^\dagger \in \mathbb{WPG}_{\mathrm{!}}({\mathrm{!}} \Sigma(\Sigma(\Gamma, A), A^+))$ , where $\kappa_{X}$ is the constant family at X;

• • (Id-Intro) Let $\mathrm{Refl}_A := \langle \overline{\mathrm{v}_A}, \mathrm{refl}_A \rangle \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Gamma, A), \Sigma(\Sigma(\Sigma(\Gamma, A), A^+), \mathrm{Id}_A))$ , where $\mathrm{refl}_A \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Gamma, A), \mathrm{Id}_A\{ \overline{\mathrm{v}_A} \})$ is $\underline{\surd} : \mathscr{P}(T')$ (Example 2.5) up to ‘tags.’ Note that $\mathrm{refl}_A$ is well-defined since its codomain is always the p-game $\mathscr{P}(T')$ .

• • (Id-Elim) Given a term $\beta \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Gamma, A), B\{\mathrm{Refl}_A\})$ , there is a term $\mathcal{R}^{\mathrm{Id}}_{A,B}(\beta) \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Sigma(\Sigma(\Gamma, A_{[0]}), A_{[1]}^+), \mathrm{Id}_A), B)$ that makes the first P-move q in $\mathrm{Id}_A$ , and if O plays there by $\surd$ , then it plays as $\beta$ between $\Sigma(\Gamma, A_{[0]})$ and B in the rest of the play. Since there is the evident bijection $\mathbb{WPG}_{\mathrm{!}}(\Sigma(\Gamma, A)) \cong \mathbb{WPG}_{\mathrm{!}}(\Sigma(\Sigma(\Sigma(\Gamma, A), A^+), \mathrm{Id}_A))$ thanks to the definition of $\mathrm{Id}_A$ , $\mathcal{R}^{\mathrm{Id}}_{A,B}(\beta)$ can play as $\beta$ after the initial two moves.

Having gone through the detailed proofs of Theorems 4.5.1.4 and 4.5.2.2, now it is a routine to verify Id-Comp, Id-Subst and Refl-Subst. Also, essentially the same interpretation of Id types is given by Abramsky et al. (2015). Thus, we leave the details to the reader.

4.6 Intensionality

We next show the intensionality of our game semantics. The aim is to exhibit the unique intensionality that distinguishes our game semantics from other semantics of MLTT such as realisability (Streicher 2012) and domains (Palmgren and Stoltenberg-Hansen 1990).

This section focuses on the part of the CwF $\mathbb{WPG}_{\mathrm{!}}$ definable by MLTT with the One, the Zero, the N, Pi, Sigma and Id types (see Hofmann (1997) for the interpretation) and formulates some type-theoretic principles in $\mathbb{WPG}_{\mathrm{!}}$ . We fix an arbitrary CwF $\mathcal{C}$ with the aforementioned types, and assume $\Gamma \in \mathcal{C}$ , $A \in \mathrm{Ty}(\Gamma)$ and $B \in \mathrm{Ty}(\Gamma . A)$ .

Equality reflection Equality reflection (Martin-Löf 1975) states that two propositionally equal terms are judgmentally equal: $\alpha = \alpha' \in \mathrm{Tm}(\Gamma, A)$ if $\mathrm{Tm}(\Gamma, \mathrm{Id}_A\{\langle \langle \mathrm{id}, \alpha \rangle, \alpha' \rangle\}) \neq \emptyset$ .

Equality reflection fails in our game semantics: The strategies $N \mathbin{\&} 0 \stackrel{\pi_1}{\rightarrow} N$ and $N \mathbin{\&} 0 \stackrel{\mathrm{succ}}{\rightarrow} N \mathbin{\&} 0 \stackrel{\pi_1}{\rightarrow} N$ are two different definable terms in $\mathbb{WPG}_{\mathrm{!}}(\Sigma(N, \{0\}), \{ N \})$ , but the elimination rule on the Zero type gives a definable one $\rho \in \mathbb{WPG}_{\mathrm{!}}(\Sigma(N, \{0\}), \mathrm{Id}_N\{ \langle \langle \mathrm{id}, \pi_1 \bullet \mathrm{succ} \rangle, \pi_1 \rangle \})$ .

Recall that $\rho$ is the strategy that makes, after the initial move q on the codomain is made by O, the move q in 0 on the domain (see the proof of Theorem 4.5.4.1).

Function extensionality Function extensionality (Univalent Foundations Program 2013) postulates that if two terms of a Pi type are propositionally equal as functions, then they are propositionally equal too, i.e., $\Pi(A, \mathrm{Id}_B\{ \langle \langle \mathrm{id}, \mathrm{App}(\psi\{ \mathrm{p} \}, \mathrm{v}) \rangle, \mathrm{App}(\psi'\{ \mathrm{p} \}, \mathrm{v}) \rangle \}) \Rightarrow \mathrm{Id}_{\Pi(A, B)}\{ \langle \langle \mathrm{id}, \psi \rangle, \psi' \rangle \} \in \mathrm{Ty}(\Gamma) \neq \emptyset$ for all $\psi, \psi' \in \mathrm{Tm}(\Gamma, \Pi(A, B))$ .

Our game semantics refutes function extensionality since terms $\psi \in \mathbb{WPG}_{\mathrm{!}}(\Gamma, A)$ are in general not completely specified by their extensions $(\gamma : {\mathrm{!}} \Gamma) \mapsto \phi \circ \gamma$ . In order to see this point closely, consider, e.g., the two terms $\underline{0}, \underline{0}' \in \mathbb{WPG}_{\mathrm{!}}(T, \Pi(\{ N_{[0]} \}, \{ N_{[1]} \}))$ defined respectively by $\underline{0} := \mathrm{Pref}(\{ \, q_{[1]}q_{[0]}n_{[0]}0_{[1]} \mid n \in \mathbb{N} \, \})^{\mathrm{Even}}$ and $\underline{0}' := \mathrm{Pref}(\{ q_{[1]}0_{[1]} \})^{\mathrm{Even}}$ . They are both definable in MLTT by the introduction and the elimination rules of the N type. For the reason mentioned above, the function extensionality on these terms fails.

Criteria of intensionality There are Criteria of Intensionality given by given by Streicher (1993):

1. (1) $\mathrm{v}\{ \mathrm{p} \circ \mathrm{p} \} \neq \mathrm{v}\{ \mathrm{p} \} \in \mathrm{Tm}(\Gamma . A . A^+ . \mathrm{Id}_A, A\{ \mathrm{p} \circ \mathrm{p} \circ \mathrm{p} \})$ ;

2. (2) $B\{ \langle \mathrm{p} \circ \mathrm{p} \circ \mathrm{p}, \mathrm{v}\{ \mathrm{p} \circ \mathrm{p} \rangle \} \} \neq B\{ \langle \mathrm{p} \circ \mathrm{p} \circ \mathrm{p}, \mathrm{v}\{ \mathrm{p} \} \rangle \} \in \mathrm{Tm}(\Gamma . A . A^+ . \mathrm{Id}_A)$ ;

3. (3) If $\mathrm{Tm}(T, \mathrm{Id}_S\{ \langle \langle \mathrm{id}_T, \sigma \rangle, \sigma' \rangle \})$ is inhabited, then $\sigma = \sigma' \in \mathrm{Tm}(T, S)$ ,

for all $\Gamma \in \mathcal{C}$ , $A \in \mathrm{Ty}(\Gamma)$ , $B \in \mathrm{Ty}(\Gamma . A)$ , $S \in \mathrm{Ty}(T)$ and $\sigma, \sigma' \in \mathrm{Tm}(T, S)$ .

Our game semantics satisfies the first criterion. For example, let $\Gamma := T$ , $A := \{ N \}_{{\mathrm{!}} T}$ and $B := \{ N \}_{{\mathrm{!}} \Sigma(T, \{ N \})}$ . Then, the strategies $\mathrm{v}\{ \mathrm{p} \circ \mathrm{p} \} = (T \mathbin{\&} N \mathbin{\&} N \mathbin{\&} \mathrm{Id}_{\{ N \}} \stackrel{\pi_1}{\rightarrow} T \mathbin{\&} N \mathbin{\&} N \stackrel{\pi_1}{\rightarrow} T \mathbin{\&} N \stackrel{\pi_2}{\rightarrow} N)$ and $\mathrm{v}\{ \mathrm{p} \} = (T \mathbin{\&} N \mathbin{\&} N \mathbin{\&} \mathrm{Id}_{\{ N \}} \stackrel{\pi_1}{\rightarrow} T \mathbin{\&} N \mathbin{\&} N \stackrel{\pi_2}{\rightarrow} N)$ are clearly different.

In contrast, our game semantics does not satisfy the second criterion since dependent p-games are indexed by winning strategies: Any term $\tau \in \mathbb{WPG}_{\mathrm{!}}({\mathrm{!}} \Sigma(\Sigma(\Sigma(\Gamma, A), A^+), \mathrm{Id}_A))$ must be of the form $\tau = \langle \langle \langle \gamma_0, \alpha_0 \rangle, \alpha_0' \rangle, \underline{\surd} \rangle^\dagger$ such that $\alpha_0 = \alpha_0'$ . In other words, our game semantics of dependent types is extensional as opposed to that of terms.

Last but not least, our game semantics satisfies the third criterion: Any term $\rho \in \mathbb{WPG}_{\mathrm{!}}(T, \mathrm{Id}_S\{ \langle \langle \mathrm{id}_T, \sigma \rangle, \sigma' \rangle \})$ must be $\underline{\surd}$ (up to ‘tags’) since it is winning, so $\sigma = \sigma'$ .

Uniqueness of identity proofs Let us finally analyse uniqueness of identity proofs (UIP) (Hofmann and Streicher 1998), which states that any two identity proofs of an Id type are propositionally equal. At this point, we leave its precise formulation to the reader.

Our game semantics validates UIP as follows. If the context contains the Zero type, then the validation is trivial as in the case of equality reflection. Hence, assume that the Zero type does not occur in the context. Even in this case, by the trivial interpretation of Id types (Theorem 4.5.5.2), our game semantics validates UIP.

Summary We have seen the intensionality of our game semantics in terms of some of the well-known type-theoretic principles. Let us summarise these observations and compare our game semantics with other computational semantics of MLTT (similarly to the table in (similarly to the table in Abramsky et al. 2015, Section 1):

Our game semantics exhibits its intensionality in terms of the type-theoretic principles except the criterion (2) and UIP. Recall that the failure of the criterion (2) is because we index a dependent p-game by winning strategies, while Abramsky et al. (2015) satisfies it because their indexing is by general (i.e., not necessarily winning) strategies. As explained in the paragraph that follows Notation 4.1.2, however, the indexing of a dependent p-game by winning strategies makes sense in light of the game semantics of universes (Yamada 2022). In addition, the game semantics of universes describes the intensional computations underlying dependent p-games; i.e., it exhibits the intensionality of dependent p-games. We thus believe that the failure of the criterion (2) does not matter much.

On the other hand, our game semantics, similarly to Abramsky et al. (2015), validates UIP due to the trivial interpretation of Id types. We leave it as future work to refine the interpretation of Id types in a more intensional way so that it refutes UIP.

Finally, the above table shows the unique intensionality of the game semantics of MLTT that distinguishes it from other computational semantics of MLTT such as realisability and domains. In the next section, we illustrate the utility of this intensionality for the meta-theoretic study of MLTT.

4.7 Independence of Markov’s principle

Markov’s principle (Markov 1962) is a subtle principle studied in the fields of constructive mathematics (Troelstra and van Dalen 1988) and computability theory (Rogers 1967), where it depends on a school of constructive mathematics whether Markov’s principle is regarded as constructive. Roughly, Markov’s principle postulates that, if it is impossible that there is no natural number $n \in \mathbb{N}$ such that $f(n) = 0$ for a given function $f : \mathbb{N} \rightarrow \mathbb{N}$ , then there is a natural number $n_0 \in \mathbb{N}$ such that $f(n_0) = 0$ .

We can formulate Markov’s principle in MLTT as the type

(7) \begin{equation}\mathrm{f : N \Rightarrow N \vdash \neg \neg \Sigma_{x:N}Id_N(f(x), \underline{0}) \Rightarrow \Sigma_{y:N}Id_N(f(y), \underline{0}) \ type},\end{equation}

where $\neg \mathrm{A}$ abbreviates the implication A 0 for each type A, and 0, N, $\Rightarrow$ , ${\Pi}$ , ${\Sigma}$ and Id_N are the Zero, the N, implication, Pi, Sigma and Id types, respectively.

To see the subtlety of Markov’s principle, note that Markov’s principle forms an instance of the law of double negation elimination, which is admissible in classical logic but not in intuitionistic logic (Troelstra and Schwichtenberg 2000). Thus, at first glance, Markov’s principle appears to be non-constructive. On the other hand, Markov described an algorithm that validates the principle within his recursive school of constructive mathematics (Troelstra and van Dalen 1988, Section 4.5). In this way, it indeed depends on a school of constructive mathematics if one accepts Markov’s principle. For this reason, it is interesting to see if Markov’s principle is independent from MLTT, and why in either case.

Mannaa and Coquand (2017) proved that Markov’s principle is independent; i.e., there is no term of the type (7) in MLTT. Their proof of this independence result is syntactic.

However, even representative computational models of MLTT such as the effective topos (Hyland 1982) validate Markov’s principle. Besides, the model by Blot and Laird (2018) validates it too though this is hardly surprising as their model admits classical reasoning (Blot and Laird 2018, Section 8). In other words, there is a gap between MLTT and these models.

In this context, we illustrate the precision of our game semantics of MLTT by:

Corollary 4.7.1 (game semantics refutes Markov’s principle). There is no game-semantic term on the interpretation of the type (7) in the CwF $\mathbb{WPG}_{\mathrm{!}}$ . Hence, the game semantics of MLTT in $\mathbb{WPG}_{\mathrm{!}}$ (Sections 4.4–4.5) implies that Markov’s principle is independent from MLTT.

Proof. Assume for a contradiction that there is a game-semantic term on the interpretation of the type (7) in $\mathbb{WPG}_{\mathrm{!}}$ , which is the p-game

(8) \begin{equation}\Pi\Big(N_{[0]} \Rightarrow N_{[1]}, \Big(\Big(\Sigma(N_{[2]}, \mathrm{Id}_N\{ \langle \mathrm{App}(\pi_1, \pi_2), \underline{0} \rangle \}_{[3]}) \Rightarrow 0_{[4]}\Big) \Rightarrow 0_{[5]}\Big) \Rightarrow \Sigma(N_{[6]}, \mathrm{Id}_N\{ \langle \mathrm{App}(\pi_1, \pi_2), \underline{0} \rangle \}_{[7]})\{ \mathrm{p} \} \Big),\end{equation}

where we omit the terminal p-game T and the bracket $\{ \_ \}$ for constant dependent p-games; e.g., we write N for $T . \{ N \}$ . We call $\Sigma(N_{[6]}, \mathrm{Id}_N\{ \langle \mathrm{App}(\pi_1, \pi_2), \underline{0} \rangle \}_{[7]})\{ \mathrm{p} \}$ the codomain, and $N_{[0]} \Rightarrow N_{[1]}$ and $\big(\Sigma(N_{[2]}, \mathrm{Id}_N\{ \langle \mathrm{App}(\pi_1, \pi_2), \underline{0} \rangle \}_{[3]}) \Rightarrow 0_{[4]}\big) \Rightarrow 0_{[5]}$ the outer and the inner domains of the p-game (8), respectively. We write $\langle \phi, \psi \rangle$ for the assumed term.

We proceed by the following case analysis. Assume that there are total input strategies $\varphi^\dagger : {\mathrm{!}} (N_{[0]} \Rightarrow N_{[1]})$ and $\langle \underline{n}, \underline{\surd} \rangle^\dagger : {\mathrm{!}} \Sigma(N_{[2]}, \mathrm{Id}_N\{ \langle \mathrm{App}(\pi_1, \pi_2), \underline{0} \rangle \}_{[3]})$ on which $\phi$ eventually makes a P-move $n'_\varphi$ in $N_{[6]}$ if O begins a play in $N_{[6]}$ . If $\varphi \bullet \underline{n'_\varphi} \neq \underline{0}$ for some of these $\varphi$ and n, and O plays by them, then $\mathrm{Id}_N\{ \langle \mathrm{App}(\pi_1, \pi_2), \underline{0} \rangle \}_{[7]}$ can be the empty p-game 0, and $\psi$ plays on the domains forever, contradicting its noetherianity. If $\varphi \bullet \underline{n'_\varphi} = \underline{0}$ for all $\varphi$ and n, then $\phi$ is strict ¹⁹ since otherwise $n'_\varphi$ would be the same even if O changes $\varphi$ so that $\varphi \bullet \underline{n'_\varphi} \neq \underline{0}$ , a contradiction; thus, $\phi$ is strict and answers the question in $N_{[6]}$ yet with no answer to the question in $0_{[4]}$ , contradicting the well-bracketing of $\phi$ . Thus, we conclude that, given any total inputs $\varphi^\dagger$ and $\langle \underline{n}, \underline{\surd} \rangle^\dagger$ , $\phi$ does not make a P-move in $N_{[6]}$ . Similarly to the case of $\psi$ , however, this contradicts the noetherianity of $\phi$ .

This game-semantic proof explains why Markov’s principle is independent from MLTT in a syntax-independent, non-inductive fashion, which is very different from the syntactic, inductive proof given by Mannaa and Coquand (2017). In this sense, our method sheds new light on Markov’s principle and more broadly on constructive mathematics.

Moreover, our game-semantic reasoning will remain valid even when the present game semantics of MLTT is extended to new types. Consequently, when the game semantics of MLTT has been extended to new types, the independence result will be automatically extended to those types as well. This advantage makes game semantics a powerful tool for the meta-theoretic study of MLTT. In contrast, the syntactic proof given by by Mannaa and Coquand (2017), for instance, does not have such a modular property because an extension of MLTT may invalidate their syntactic, inductive reasoning.

4.8 Game semantics of subtyping on dependent types

Finally, let us prove that p-games enable us to interpret subtyping on dependent types for the purpose of illustrating another utility of the novel mathematical structure of p-games. In particular, we show that the liveness ordering $\preccurlyeq$ underlying p-games elegantly captures subtyping on dependent types; e.g., see the proof of Lemma 4.8.4.

Recall that the subtyping relation between types is something like the subset relation between sets, and it is mainly to ensure that, if $\alpha$ is a term of a type A, and A is a subtype of a type B, then $\mathrm{coe}(\alpha)$ is a term of B that computes in the same way as $\alpha$ , where coe is an operation on terms, called coercion. Therefore, subtyping has a pragmatic importance because it ensures reusability of terms in different types. In some cases, coe is just the identity map; in the following, we assume for simplicity that coe is the identity map.

Let us first formulate a subtyping relation between dependent types in CwFs:

Definition 4.8.1 (CwFs with subtyping). A CwF $\mathcal{C}$ with the One, Pi and Sigma types has subtyping (on the One, Pi and Sigma types) if it is equipped with a partial order on $\mathrm{Ty}(\Gamma)$ for each $\Gamma \in \mathcal{C}$ that satisfies

1. (1) ;

2. (2) ;

3. (3) ;

4. (4) .

The first axiom requires the reusability of terms. Besides, for the compositionality of mathematical semantics, the other axioms require that constructions on types preserve the partial order . Note that the last axiom implicitly requires that $B, B' \in \mathrm{Ty}(\Gamma . A')$ implies $B, B' \in \mathrm{Ty}(\Gamma . A)$ . The order between A and A’ is flipped in Pi types in the last axiom since fewer morphisms can take more inputs (Amadio and Curien 1998, p. 419).

We then define game semantics of subtyping based on Definition 3.1.1:

Definition 4.8.2 (predicate liveness ordering) The predicate (p-) liveness ordering is a partial order

between p-games $\Gamma$ and $\Delta$ defined by

and lifted to the one

between linearly dependent p-games L and R over $\Gamma$ by

It is easy to see that the p-liveness orderings and are partial orders since so is the liveness ordering $\preccurlyeq$ (Chroboczek 2000, Theorem 9). Besides, the p-liveness ordering clearly satisfies the second and the third axioms of Definition 4.8.1, where $1 = \{ T \}$ .

Moreover, if $\gamma : \Gamma$ and , then $\gamma : \Delta$ since $\gamma : |\Gamma| = |\Delta|$ and $\overline{\gamma}_{|\Delta|} = \overline{\gamma}_{|\Gamma|} \preccurlyeq \Gamma(\gamma) \preccurlyeq \Delta(\gamma)$ . This observation shows that also satisfies the first axiom:

Lemma 4.8.3 (preservation of linear typing under predicate liveness ordering). Let L and R be linearly dependent p-games over a p-game $\Gamma$ such that .

1. (1) If $\psi : \Pi_\ell(\Gamma, L)$ , then $\psi : \Pi_\ell(\Gamma, R)$ ;

2. (2) If $\psi : \Pi_\ell(\Gamma, L)$ is winning (respectively, well-bracketed), then so is $\psi : \Pi_\ell(\Gamma, R)$ .

Further, satisfies the last axiom as well:

Lemma 4.8.4 (preservation of predicate liveness ordering). If and , then , , and . Moreover, if and , then and . (N.b., strictly speaking, the pair $(|B|, \|B\| \upharpoonright \Gamma . A)$ , where $\|B\| \upharpoonright \Gamma . A$ is the restriction of $\| B \|$ to $\mathrm{st}(\Gamma . A) \subseteq \mathrm{st}(\Gamma . A')$ , not B itself, is an element of $\mathscr{D}(\Gamma . A)$ , and similarly for B’.)

Proof. For the first part, we focus on linear implication $\multimap$ as the cases of the other constructions are simpler. First, observe $|\Delta' \multimap \Gamma| = |\Delta'| \multimap |\Gamma| = |\Delta| \multimap |\Gamma'| = |\Delta \multimap \Gamma'|$ . Next, let $\phi : |\Delta' \multimap \Gamma|$ ; it remains to show $(\Delta' \multimap \Gamma)(\phi) \preccurlyeq (\Delta \multimap \Gamma')(\phi)$ , but it follows from and by induction on the lengths of positions, where the symmetry (between O and P) of the liveness ordering $\preccurlyeq$ is crucial. We show the second part in the same vein.

Hence, we have finally shown:

Corollary 4.8.5 (game semantics of subtyping) The CwF $\mathbb{WPG}_{\mathrm{!}}$ has subtyping.

5. Conclusion and Future Work

We have given novel game semantics of MLTT equipped with the One, the Zero, the N, Pi, Sigma and Id types. This game semantics interprets Sigma types in a direct, non-inductive fashion that inherits the additive nature of product on games, overcoming the shortcomings of the previous attempts (Abramsky et al. 2015; Blot and Laird 2018; Vákár et al. 2018). In particular, although the indirect, inductive interpretation of Sigma types by Abramsky et al. (2015), Vákár et al. (2018) makes it impossible to interpret universes (Martin-Löf 1975), our approach is extendable to universes (Yamada 2022).

We have also illustrated the utility of our game semantics by showing that it provides a new proof of the independence of Markov’s principle from MLTT. By its syntax-free, non-inductive nature, this proof sheds new light on why the independence holds. Moreover, this game-semantic method will be readily applicable to other types as soon as the game semantics has been extended to the types.

Unlike Blot and Laird (2018), our game semantics inherits the flagship advantages of game semantics such as the linear decomposition of function types and the characterisation of effects by constraints on strategies. Based on the insights given by this game semantics, we shall achieve the syntax and the semantics of MLTT combined with linear logic and/or effects. We would also like to extend our game semantics to other types such as Martin-Löf’s well-founded tree (W) types (Martin-Löf 1982). The resulting game semantics will be a very powerful semantic foundation of constructive mathematics; for instance, it will interpret Aczel’s constructive set theory (CZF) (Aczel 1986) since CZF is translatable into MLTT equipped with universes and W types. Moreover, the present game-semantic method for the meta-theoretic study of MLTT will be also available to W types.