Corresponds¡—¿ Dashto dashdash¿ Equals=====

# Game semantics of universes

Norihiro Yamada

<EMAIL_ADDRESS>
School of Mathematics
University of Minnesota

###### Abstract

This work extends the present author’s computational game semantics of Martin-
Löf type theory to the cumulative hierarchy of _universes_. This extension
completes game semantics of all standard types of Martin-Löf type theory for
the first time in the 30 years history of modern game semantics.111More
extensional, domain and realisability semantics of universes has been
established though [Pal93, Str12, BL18]. As a result, the powerful
combinatorial reasoning of game semantics becomes available for the study of
universes and types generated by them. A main challenge in achieving game
semantics of universes comes from a _conflict_ between identity types and
universes: Naive game semantics of the encoding of an identity type by a
universe induces a decision procedure on the equality between functions, a
contradiction to a well-known fact in recursion theory. We overcome this
problem by novel games for universes that encode games for identity types
_without deciding the equality_.

###### Contents

  1. 1 Introduction
    1. 1.1 Martin-Löf type theory and the meaning explanation
    2. 1.2 Game semantics of Martin-Löf type theory
    3. 1.3 Examples of games and strategies
    4. 1.4 Martin-Löf’s universes
    5. 1.5 The problem: how to encode games for identity types by strategies
    6. 1.6 Our solution: encoding without deciding
    7. 1.7 Lifting to the cumulative hierarchy of universes
    8. 1.8 Main results
    9. 1.9 Our contributions and related work
    10. 1.10 The structure of the present article
  2. 2 Review: game semantics of Martin-Löf type theory
    1. 2.1 Games and strategies
    2. 2.2 Game semantics of Martin-Löf type theory
  3. 3 Game semantics of universes
    1. 3.1 Universe predicate games
    2. 3.2 Computational game semantics of the cumulative hierarchy of universes
  4. 4 Corollaries
    1. 4.1 Effectivity of game semantics
    2. 4.2 Independence of equality reflection
    3. 4.3 Independence of Markov’s principle
  5. 5 Conclusion and future work

##  1 Introduction

For this introduction, we assume that the reader is familiar with the syntax
of dependent type theories and universes [Hof97], but not with game semantics
[A+97, Hyl97].

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

On the one hand, _formal systems_ [Sho67] are a class of symbolic or
_syntactic_ formalisations of mathematics, and _constructive mathematics_
[TvD88] is a family of computational or _constructive_ schools in mathematics.
On the other hand, _semantics_ of a formal system is an assignment of syntax-
free objects to syntactic objects of the formal system, where the former
serves as the ‘meaning’ or _interpretation_ of the latter.

_Martin-Löf type theory (MLTT)_ [ML75, ML84, ML98] is a prominent formal
system for constructive mathematics, and it is comparable to axiomatic set
theory [Zer08, Fra22] for classical mathematics. The fundamental idea of MLTT
is to regard (mathematical) objects and proofs in constructive mathematics
uniformly as _computations_ in an informal sense, and MLTT is a syntactic
formalisation of this beautiful idea [ML82]. Hence, objects and proofs in MLTT
are unified into _terms_ , where formulas are called _types_. This standard
yet informal semantics of MLTT is called the _meaning explanation_ [DP16, §5].

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

###  1.2 Game semantics of Martin-Löf type theory

This problem calls for _mathematical_ semantics [Gun92] of MLTT that
faithfully formalises the meaning explanation, abstracting the inessential
syntactic details, and advances the meta-theoretic study of MLTT. Motivated in
this way, the present author has established _game semantics of MLTT_ [Yam22].

_Game semantics_ [A+97, Hyl97] is a class of mathematical semantics that
interprets types by _games_ between _Player_ (or a mathematician) and
_Opponent_ (or an oracle), and terms by _strategies_ for Player on how to play
on games. Games are a class of rooted directed forests, and strategies are
algorithms for Player on how to walk on (or play) games alternately with
Opponent in such a way that it is Player’s _win_.

We write a walk or _play_ in a game by a potentially infinite sequence of
finite sequences

$\bm{\epsilon},m_{1},m_{1}m_{2},m_{1}m_{2}m_{3},\dots,$

where $\bm{\epsilon}$ is the empty sequence, each element or _move_ $m_{i}$ is
a vertex of the game, and each sequence or _position_ $m_{1}m_{2}\dots m_{n}$
is a finite path from the root in the game. By convention, the first move
$m_{1}$ is always made by Opponent, and then Player and Opponent alternately
make moves. Thus, the moves $m_{2i+1}$ are made by Opponent, and the other
ones $m_{2i}$ by Player ($i\in\mathbb{N}$). Because a strategy describes the
next move to be made by Player, if any, we describe its computational step by
the partial function

$m_{1}\mapsto m_{2},m_{1}m_{2}m_{3}\mapsto m_{4},\dots.$

The game semantics of MLTT formalises the meaning explanation _syntax-
independently_ and _intuitively_ by interpreting terms as strategies or
_interactive computations_ between Player and Opponent. In addition, the game
semantics turns out to be a highly effective tool for the meta-theoretic study
of MLTT; e.g., it verifies the _independence of Markov’s principle_ [Yam22],
which is not possible by most other mathematical semantics of MLTT such as
Hyland’s _effective topos_ [Hyl82]. The point is that game semantics is unique
in its interpretation of terms by strategies or _intensional processes_ ,
while other mathematical semantics interprets terms by extensional objects
such as functions. Because terms are also intensional objects, computing in a
step-by-step fashion, game semantics achieves a very tight correspondence
between terms and strategies, which makes itself an exceptionally powerful
tool for the study of formal systems.

###  1.3 Examples of games and strategies

In the following, let us see some simple examples of games and strategies as a
preparation for §1.5. For instance, the game $N$ of natural numbers is the
rooted tree (which is infinite in width) in which a play starts with
Opponent’s move or question $q$ (‘What is your number?’) and ends with
Player’s move or answer $n\in\mathbb{N}$ (‘My number is $n$!’). This natural
number game $N$ is not very different from the set $\mathbb{N}$ of all natural
numbers, and there is a much more intensional game for natural numbers
[Yam19]. However, the game $N$ is simpler and suffices for our purpose. A
strategy $\underline{7}$ on $N$, written $\underline{7}:N$, corresponding to
the number $7\in\mathbb{N}$ for instance, is the map $q\mapsto 10$. In the
rest of this introduction, we describe games by listing their positions. For
example, the set of all positions of $N$ is
$\\{\bm{\epsilon},q\\}\cup\\{\,qn\mid n\in\mathbb{N}\,\\}$.

There is a binary construction $\&$ on games, called _product_ , which forms
binary product in the category of games and strategies. The product
$A\mathbin{\&}B$ of games $A$ and $B$ are simply the disjoint union of $A$ and
$B$. In other words, a position of $A\mathbin{\&}B$ is either a position of
$A$ or $B$. For instance, a maximal position of the product $N\mathbin{\&}N$
of the game $N$ and itself is either of the following forms222The diagrams are
only to make it explicit which component game each move belongs to; the two
positions are just finite sequences $q_{[0]}n_{[0]}$ and $q_{[1]}m_{[1]}$.:
$N_{[0]}$ $\&$ $N_{[1]}$ $N_{[0]}$ $\&$ $N_{[1]}$ $q_{[0]}$ $q_{[1]}$
$n_{[0]}$ $m_{[1]}$ where $n,m\in\mathbb{N}$, and the subscripts $(\\_)_{[i]}$
($i=0,1$) are arbitrary _tags_ to distinguish the two copies of $N$. We often
omit the tags $(\\_)_{[i]}$ when it does not bring confusion. We write
$\langle\underline{n},\underline{m}\rangle$ for the strategy on
$N\mathbin{\&}N$ that plays as in the above diagrams, which forms the
_pairing_ of the strategies $\underline{n},\underline{m}:N$.

Another central construction $\multimap$, called _linear implication_ ,
captures the notion of _linear functions_ , i.e., functions that consume
exactly one input to produce an output. A position of the linear implication
$A\multimap B$ between $A$ and $B$ is an interleaving mixture of a position of
$A$ and a position of $B$ such that

  1. 1.

The first element of the position must be a move of $B$;

  2. 2.

A change of the $AB$-parity in the position must be made by Player.

For example, a typical position of the linear implication $N\multimap N$ is
$N_{[0]}$ $\multimap$ $N_{[1]}$ $q_{[1]}$ $q_{[0]}$ $n_{[0]}$ $m_{[1]}$ where
$n,m\in\mathbb{N}$, which can be read as follows:

  1. 1.

Opponent’s question $q_{[1]}$ for an output (‘What is your output?’);

  2. 2.

Player’s question $q_{[0]}$ for an input (‘Wait, what is your input?’);

  3. 3.

Opponent’s answer, say, $n_{[0]}$, to $q_{[0]}$ (‘OK, here is an input $n$.’);

  4. 4.

Player’s answer, say, $m_{[1]}$, to $q_{[1]}$ (‘Alright, the output is then
$m$.’).

This play corresponds to any linear function $\mathbb{N}\rightarrow\mathbb{N}$
that maps $n\mapsto m$. The strategy $\mathrm{succ}$ on $N\multimap N$ for the
successor function is the map $q_{[1]}\mapsto
q_{[0]},q_{[1]}q_{[0]}n_{[0]}\mapsto n+1_{[1]}$, or diagrammatically
$N_{[0]}$ $\stackrel{{\scriptstyle\mathrm{succ}}}{{\multimap}}$ $N_{[1]}$
$q_{[1]}$ $q_{[0]}$ $n_{[0]}$ $n+1_{[1]}$

Let us remark here that the following play, which corresponds to a _constant_
linear function that maps $x\mapsto m$ for all $x\in\mathbb{N}$, is also
possible: $q_{[1]}\mapsto m_{[1]}$. Thus, strictly speaking, $A\multimap B$ is
the game of _affine functions_ from $A$ to $B$, but we follow the standard
convention to call $\multimap$ linear implication.

However, the linear implication $N\mathbin{\&}N\multimap N$ cannot accommodate
strategies that compute binary functions such as addition because maximal
positions of this game are either of the following forms:  $N$ $\&$ $N$
$\multimap$ $N$ $q$ $q$ $n$ $m$ $N$ $\&$ $N$ $\multimap$ $N$ $q$ $q$ $n$ $m$
$N$ $\&$ $N$ $\multimap$ $N$ $q$ $m$

The unary construction $\oc$ on games, called _exponential_ , addresses this
problem by defining the desired game $A\Rightarrow B$ for ordinary (not
necessarily linear) functions from $A$ to $B$ by $A\Rightarrow
B\colonequals\oc A\multimap B$. This idea comes from _linear logic_ [Gir87]. A
position of the exponential $\oc A$ is an interleaving mixture of a finite
number of positions of $A$ such that a switch between different copies of
positions of $A$ inside $\oc A$ must be made by Opponent. For instance, the
exponential $\oc(N\mathbin{\&}N)$ accommodates the positions  $\oc(N$ $\&$
$N)$ $q$ $n$ $q$ $m$ $\oc(N$ $\&$ $N)$ $q$ $n$ $q$ $m$ so that there is are
strategies  $N$ $\&$ $N$
$\stackrel{{\scriptstyle\mathrm{add}}}{{\Rightarrow}}$ $N$ $q$ $q$ $n$ $q$ $m$
$n+m$ $N$ $\&$ $N$
$\stackrel{{\scriptstyle\mathrm{add}^{\prime}}}{{\Rightarrow}}$ $N$ $q$ $q$
$n$ $q$ $m$ $n+m$ both of which compute addition of natural numbers. These
strategies both implement addition, but their algorithms are slightly
different, which illustrates the _intensional_ nature of game semantics.

At this point, let us consider the game $(N\Rightarrow N)\Rightarrow N$ of
_higher-order_ functions, which is higher-order because the domain
$N\Rightarrow N$ is the game of functions. Note that the domain is the
exponential $\oc(N\Rightarrow N)$, so a strategy $\phi$ on the game
$(N\Rightarrow N)\Rightarrow N$ may interact with an input strategy $f$ on
$\oc(N\Rightarrow N)$ given by Opponent _any finite number of times_. Each
interaction between $\phi$ and $f$ reveals an input-output pair of $f$, but
this process will never collect the complete information about $f$ because
there are infinitely many input-output pairs of $f$. For instance, the
strategy $\mathrm{pazo}:(N\Rightarrow N)\Rightarrow N$ that computes the sum
$f(0)+f(1)$ for a given function $f:\mathbb{N}\Rightarrow\mathbb{N}$ plays by
$\oc(\oc N_{[0]}$ $\multimap$ $N_{[1]})$
$\stackrel{{\scriptstyle\mathrm{pazo}}}{{\multimap}}$ $N_{[2]}$ $q_{[2]}$
$q_{[1]}$ $q_{[0]}$ $0_{[0]}$ $n_{[1]}$ $q_{[1]}$ $q_{[0]}$ $1_{[0]}$
$m_{[1]}$ $n+m_{[2]}$ This play can be read as follows:

  1. 1.

Opponent’s question $q_{[2]}$ for an output (‘What is your output?’);

  2. 2.

Player’s question $q_{[1]}$ for an input function (‘Wait, your first output
please!’);

  3. 3.

Opponent’s question $q_{[0]}$ for an input (‘What is your first input then?’);

  4. 4.

Player’s answer, say, $0_{[0]}$, to the question $q_{[0]}$ (‘Here is my first
input $0$.’);

  5. 5.

Opponent’s answer, say, $n_{[1]}$, to the question $q_{[1]}$ (‘OK, then here
is my first output $n$.’);

  6. 6.

Player’s question $q_{[1]}$ for an input function (‘Your second output
please!’);

  7. 7.

Opponent’s question $q_{[0]}$ for an input (‘What is your second input
then?’);

  8. 8.

Player’s answer, say, $1_{[0]}$, to the question $q_{[0]}$ (‘Here is my second
input $1$.’);

  9. 9.

Opponent’s answer, say, $m_{[1]}$, to the question $q_{[1]}$ (‘OK, then here
is my second output $m$.’);

  10. 10.

Player’s answer, say, $n+m_{[2]}$, to the question $q_{[2]}$ (‘Alright, my
output is then $n+m$.’).

In this play, the strategy $\mathrm{pazo}$ has only revealed the two input-
output pairs $(0,n)$ and $(1,m)$ of $f$.

Finally, let us recall the _composition_ $\psi\bullet\phi:A\Rightarrow C$ of
strategies $\phi:A\Rightarrow B$ and $\psi:A\Rightarrow C$. For an
illustration, consider the strategies
$\mathrm{succ},\mathrm{double}:N\Rightarrow N$ (n.b., $\mathrm{succ}$ this
time is not on $N\multimap N$):  $N_{[0]}$
$\stackrel{{\scriptstyle\mathrm{succ}}}{{\Rightarrow}}$ $N_{[1]}$ $q_{[1]}$
$q_{[0]}$ $m_{[0]}$ $m+1_{[1]}$ $N_{[2]}$
$\stackrel{{\scriptstyle\mathrm{double}}}{{\Rightarrow}}$ $N_{[3]}$ $q_{[3]}$
$q_{[2]}$ $n_{[3]}$ $2n_{[2]}$ The composition
$\mathrm{double}\bullet\mathrm{succ}:N\Rightarrow N$ is calculated as follows.
First, we have to define the _promotion_ $\mathrm{succ}^{\dagger}:\oc
N_{[0]}\multimap\oc N_{[1]}$ of $\mathrm{succ}$, which computes just as
$\mathrm{succ}:\oc N_{[0]}\multimap N_{[1]}$ for each position of $\oc
N_{[0]}\multimap N_{[1]}$ occurring inside $\oc N_{[0]}\multimap\oc N_{[1]}$.
A typical position played by the promotion therefore looks like  $\oc N_{[0]}$
$\stackrel{{\scriptstyle\mathrm{succ}^{\dagger}}}{{\multimap}}$ $\oc N_{[1]}$
$q_{[1]}$ $q_{[0]}$ $m_{[0]}$ $m+1_{[1]}$ $q_{[1]}$ $q_{[0]}$
$m^{\prime}_{[0]}$ $m^{\prime}+1_{[1]}$ $q_{[1]}$ $q_{[0]}$
$m^{\prime\prime}_{[0]}$ $m^{\prime\prime}+1_{[1]}$

Next, we _synchronise_ $\mathrm{succ}^{\dagger}$ and $\mathrm{double}$ via the
codomain $\oc N_{[1]}$ of $\mathrm{succ}^{\dagger}$ and the domain $\oc
N_{[2]}$ of $\mathrm{double}$, for which Player also plays the role of
Opponent in $\oc N_{[1]}$ and $\oc N_{[2]}$ by copying her last moves,
resulting in  $\oc N_{[0]}$
$\stackrel{{\scriptstyle\mathrm{succ}^{\dagger}}}{{\multimap}}$ $\oc N_{[1]}$
$\oc N_{[2]}$ $\stackrel{{\scriptstyle\mathrm{double}}}{{\multimap}}$
$N_{[3]}$ $q_{[3]}$ $q_{[2]}$ $q_{[1]}$ $q_{[0]}$ $n_{[0]}$ $n+1_{[1]}$
$n+1_{[2]}$ $2\cdot(n+1)_{[3]}$ where moves made for the synchronisation are
marked by the square boxes just for clarity. Importantly, it is assumed that
Opponent plays on the _external game_ $N_{[0]}\Rightarrow N_{[3]}$, seeing
only moves of $\oc N_{[0]}$ or $N_{[3]}$.

The resulting play is to be read as follows:

  1. 1.

Opponent’s question $q_{[3]}$ for an output in $\oc N_{[0]}\multimap N_{[3]}$
(‘What is your output?’);

  2. 2.

Player’s question $q_{[2]}$ by $\mathrm{double}$ for an input in $\oc
N_{[2]}\multimap N_{[3]}$ (‘Wait, what is your input?’);

  3. 3.

$q_{[2]}$ in turn triggers the question $q_{[1]}$ for an output in $\oc
N_{[0]}\multimap\oc N_{[1]}$ (‘What is your output?’);

  4. 4.

Player’s question $q_{[0]}$ by $\mathrm{succ}^{\dagger}$ for an input in $\oc
N_{[0]}\multimap\oc N_{[1]}$ (‘Wait, what is your input?’);

  5. 5.

Opponent’s answer, say, $n_{[0]}$, to $q_{[0]}$ in $\oc N_{[0]}\multimap\oc
N_{[3]}$ (‘Here is an input $n$.’);

  6. 6.

Player’s answer $n+1_{[1]}$ to $q_{[1]}$ by $\mathrm{succ}^{\dagger}$ in $\oc
N_{[0]}\multimap\oc N_{[1]}$ (‘The output is then $n+1$.’);

  7. 7.

$n+1_{[1]}$ in turn triggers the answer $n+1_{[2]}$ to $q_{[2]}$ in $\oc
N_{[2]}\multimap N_{[3]}$ (‘Here is the input $n+1$.’);

  8. 8.

Player’s answer $2\cdot(n+1)_{[3]}$ to $q_{[3]}$ by $\mathrm{double}$ in $\oc
N_{[0]}\multimap N_{[3]}$ (‘The output is $2\cdot(n+1)$!’).

Finally, we hide or delete all moves with the square boxes from the play,
resulting in the strategy $\mathrm{double}\bullet\mathrm{succ}:N\Rightarrow N$
for the function $n\mapsto 2\cdot(n+1)$ as expected:  $N_{[0]}$
$\stackrel{{\scriptstyle\mathrm{double}\bullet\mathrm{succ}}}{{\Rightarrow}}$
$N_{[3]}$ $q_{[3]}$ $q_{[0]}$ $n_{[0]}$ $2\cdot(n+1)_{[3]}$ The category of
games and strategies has games as objects, and strategies $\phi:A\Rightarrow
B$ as morphisms $A\rightarrow B$, and the composition of strategies just
sketched forms the categorical composition.

Moreover, one can compose strategies $\alpha:A$ and $\phi:A\Rightarrow B$ in
the same vein, obtaining the composition $\phi\bullet\alpha:B$. For instance,
we have the composition $\mathrm{double}\bullet\underline{n}=\underline{2n}$
for all $n\in\mathbb{N}$. Alternatively, recall the _terminal game_ $T$, which
has no move. Hence, we have the isomorphism $A\cong T\Rightarrow A$, and we do
not distinguish strategies on $A$ and $T\Rightarrow A$ since they are
essentially the same. As a result, the composition $\phi\bullet\alpha:B$ can
be recasted as the ordinary composition $\phi\bullet\alpha:T\Rightarrow B$ of
$\alpha:T\Rightarrow A$ and $\phi:A\Rightarrow B$.

We have seen that strategies interact with each other in a _step-by-step,
finitary_ fashion. This unique, _intensional computation_ distinguishes game
semantics from other mathematical semantics.

###  1.4 Martin-Löf’s universes

One can extend MLTT by a ‘types of (smaller) types’ or _universe_ introduced
by Martin-Löf [ML75]. The universe enables MLTT to expand its realm of
constructive mathematics significantly. For instance, the elimination rule of
the natural number (N-) type with respect to the universe generates
_infinitely_ indexed dependent types such as the type of finite lists of
natural numbers by mathematical induction.

Besides, the power of the universe is greatly increased when it is combined
with Martin-Löf’s _well-founded tree (W-) types_ [ML82]. For instance, MLTT
together with the universe and W-types interprets Aczel’s constructive set
theory [Acz86]. Moreover, the combination of the universe and W-types offers
MLTT a high proof-theoretic strength among constructive formal systems [Set93,
GR94].

###  1.5 The problem: how to encode games for identity types by strategies

For these significant roles of the universe in MLTT and constructive
mathematics, it is a natural aim to extend game semantics to the universe so
that its powerful combinatorial reasoning becomes available for the study of
the universe and types generated by the universe. However, it is a challenge
to achieve game semantics of the universe, and it has not been established in
the 30 years history of game semantics.333Blot and Laird [BL18] interpret
universes, but this interpretation is by domain theory, not by game semantics.

Specifically, the challenge is _how to encode games for identity (Id-) types
by strategies_. To see this point, recall first that the game semantics
[Yam22] interprets each dependent type $\mathsf{\Gamma\vdash A\ type}$ roughly
by a family $A=(A(\gamma))_{\gamma:\Gamma}$ of games $A(\gamma)$ indexed by
strategies $\gamma$ on the game $\Gamma$ that interprets the context
$\mathsf{\Gamma}$. Also, recall that the introduction rule of each universe
$\mathsf{\Gamma\vdash U\ type}$ _encodes_ the dependent type
$\mathsf{\Gamma\vdash A\ type}$ by a term $\mathsf{\Gamma\vdash En(A):U}$ in
such a way that the computation rule $\mathsf{\Gamma\vdash El(En(A))=A\ type}$
holds, where the dependent type $\mathsf{x:U\vdash El(x)\ type}$ embodies the
elimination rule of the universe by the substitution $\mathsf{\Gamma\vdash
u:U}\mapsto\mathsf{\Gamma\vdash El(u)\ type}$. Note that each universe is a
_constant_ dependent type, and therefore the game semantics [Yam22] should
interpret it by a _constant_ family of games, which is in turn identified by a
single game in the evident way. Hence, we have to define not only a game
$\mathcal{U}$ that interprets the universe $\mathsf{U}$ but also the
corresponding encoding of the family $A$ of games by a strategy
$\mathrm{En}(A)$ on the function game $\Gamma\Rightarrow\mathcal{U}$ from
$\Gamma$ to $\mathcal{U}$, which interprets the introduction rule, and a
family $\mathrm{El}=(\mathrm{El}(\mu))_{\mu:\mathcal{U}}$ of games
$\mathrm{El}(\mu)$, which interprets the elimination rule, that satisfies
$\mathrm{El}(\mathrm{En}(A)\bullet\gamma)=A(\gamma)$ for all $\gamma:\Gamma$,
which interprets the computation rule. Recall that a strategy on the game
$\Gamma\Rightarrow\mathcal{U}$ is a certain kind of an _algorithm_ that
outputs a strategy on the codomain $\mathcal{U}$ from a given input strategy
on the domain $\Gamma$.

Now, let us take $\mathrm{A}$ to be the Id-type $\mathsf{f:N\Rightarrow
N,g:N\Rightarrow N\vdash Id_{N\Rightarrow N}(f,g)\ type}$ on the function type
$\mathsf{N\Rightarrow N}$ from N-type $\mathsf{N}$ to itself. Then, the game
semantics [Yam22] has to interpret the encoding term $\mathsf{f:N\Rightarrow
N,g:N\Rightarrow N\vdash\mathrm{En}(Id_{N\Rightarrow N}(f,g)):U}$ for this Id-
type by a strategy $\mathrm{En}(\mathrm{Id}_{N\Rightarrow N}):(N\Rightarrow
N)\mathbin{\&}(N\Rightarrow N)\Rightarrow\mathcal{U}$ that satisfies
$\mathrm{El}(\mathrm{En}(\mathrm{Id}_{N\Rightarrow N})\bullet\langle
f,g\rangle)=\mathrm{Id}_{N\Rightarrow N}(\langle f,g\rangle)$ for all
$f,g:N\Rightarrow N$, where $\mathrm{Id}_{N\Rightarrow N}$ is the family of
games that interprets the Id-type [Yam22]. Crucially, the game
$\mathrm{Id}_{N\Rightarrow N}(\langle f,g\rangle)$ depends on the equation
$f=g$. Thus, the composition $\mathrm{En}(\mathrm{Id}_{N\Rightarrow
N})\bullet\langle f,g\rangle$ _must vary over the cases $f=g$ and $f\neq g$_.

Accordingly, the strategy $\mathrm{En}(\mathrm{Id}_{N\Rightarrow N})$ seems to
be an algorithm that decides whether the equation $f=g$ holds for all
$f,g:N\Rightarrow N$, a contradiction to a well-known fact in recursion theory
[RR67]. This corresponds, in game semantics, to that the strategy
$\mathrm{En}(\mathrm{Id}_{N\Rightarrow N})$ can learn about only _finite_
input-output pairs of $f$ and $g$, so it cannot decide if the equation $f=g$
holds, as illustrated by the diagram

$(N$ | $\stackrel{{\scriptstyle f}}{{\Rightarrow}}$ | $N)$ | $\&$ | $(N$ | $\stackrel{{\scriptstyle g}}{{\Rightarrow}}$ | $N)$ | $\stackrel{{\scriptstyle\mathrm{En}(\mathrm{Id}_{N\Rightarrow N})}}{{\Rightarrow}}$ | $\mathcal{U}$
---|---|---|---|---|---|---|---|---
|  |  |  |  |  |  |  | $u_{1}$
|  | $q$ |  |  |  |  |  |
$q$ |  |  |  |  |  |  |  |
$n$ |  |  |  |  |  |  |  |
|  | $f(n)$ |  |  |  |  |  |
|  |  |  |  |  | $q$ |  |
|  |  |  | $q$ |  |  |  |
|  |  |  | $n^{\prime}$ |  |  |  |
|  |  |  |  |  | $f(n^{\prime})$ |  |
|  |  |  |  |  |  | $\vdots$ |
|  |  |  |  |  |  | $\wn$ |

Let us see more concretely that the following naive method fails due to the
problem just sketched. Let us assign a natural number $\sharp(A)$ to the game
$A$ that interprets each type $\mathsf{\Gamma\vdash A\ type}$ along the
inductive construction of $\mathrm{A}$, and define a game $\mathcal{U}$ in
such a way that maximal positions in $\mathcal{U}$ are of the form
$q.\sharp(A)$.  $\mathcal{U}$ $q$ $\sharp(A)$ Intuitively, the initial element
$q$ is Opponent’s question ‘What is your game?’, and the second one
$\sharp(\mathrm{A})$ is Player’s answer ‘My game is $A$!’. Further, let
$\mathrm{En}(A):\Gamma\Rightarrow\mathcal{U}$ be the strategy that encodes the
family $A$ of games by playing $q\mapsto\sharp(A)$ without ever computing on
the domain $\Gamma$. For this game $\mathcal{U}$, the strategy
$\mathrm{En}(\mathrm{Id}_{N\Rightarrow N})$ would decide if $f=g$ (even
without interacting with $f$ or $g$), which is clearly impossible.  $\Gamma$
$\stackrel{{\scriptstyle\mathrm{En}(A)}}{{\not\Rightarrow}}$ $\mathcal{U}$ $q$
$\sharp(\mathrm{Id}_{N\Rightarrow N}(\langle f,g\rangle))$

######  Remark.

This naive method does not exploit any intrinsic feature of game semantics,
but it actually works for encoding all standard dependent types except Id-
types. Hence, one may say that our main contribution is game semantics of the
universe that subsumes the encoding of Id-types.

###  1.6 Our solution: encoding without deciding

A key observation behind our solution to the problem described in §1.5 is that

> The game semantics [Yam22] allows the decoding function $\mathrm{El}$ to be
> _uncomputable_ without sacrificing the algorithmic nature of
> strategies.444This is because the game semantics of Pi-types (Definition
> 2.29) reveals the type dependency _only gradually_ so that it is not
> necessary to compute the value of the function $\mathrm{El}$ in one go. We
> shall come back to this point in Example 2.36. In particular, the strategy
> $\mathrm{En}(\mathrm{Id}_{N\Rightarrow N})\bullet\langle f,g\rangle$ _does
> not have to decide_ the equality $f=g$; it only has to encode the game
> $\mathrm{Id}_{N\Rightarrow N}(\langle f,g\rangle)$.

This leads us to the following solution. Let
$\sharp(1),\sharp(0),\sharp(N),\sharp(\Pi),\sharp(\Sigma),\sharp(\mathrm{Id})\in\mathbb{N}$
be arbitrarily fixed pairwise distinct natural numbers. We then define the
game $\mathcal{U}$ in such a way that

> The strategy $\mathrm{En}(\mathrm{Id}_{N\Rightarrow N})\bullet\langle
> f,g\rangle:\mathcal{U}$ plays first by computing
> $q\mapsto\sharp(\mathrm{Id})$ (indicating that it encodes an Id-type) and
> then, depending on the next move by Opponent, by playing as the strategy
> $\mathrm{En}(N\Rightarrow N)$ (indicating that the encoded Id-type is on the
> type $\mathsf{N\Rightarrow N}$) or by merely _copy-catting $f$ and $g$_
> given by Opponent in the step-by-step fashion (indicating that the encoded
> Id-type is between $f$ and $g$) _without necessarily detecting what $f$ or
> $g$ is_.

The point is that this method allows the strategy
$\mathrm{En}(\mathrm{Id}_{N\Rightarrow N})$ to encode the family
$\mathrm{Id}_{N\Rightarrow N}$ without sacrificing its algorithmic nature: The
copy-cat of Opponent’s strategies $f$ and $g$ is trivially computable, while
the potentially infinite plays by $\mathrm{En}(\mathrm{Id}_{N\Rightarrow
N})\bullet\langle f,g\rangle:\mathcal{U}$ faithfully encode whether or not
$f=g$.

In general, positions in $\mathcal{U}$ consist of symbols $\sharp(X)$ that
encode type constructions $X$ and ordinary (i.e., not necessarily symbolic)
strategies. In the following, let us sketch the definition of $\mathcal{U}$.

First, we have to encode _the base cases_ , i.e., the games $1$, $0$ and $N$
that interpret One-, Zero- and N-types, respectively, by strategies on the
game $\Gamma\Rightarrow\mathcal{U}$. For this reason, $\mathcal{U}$ subsumes
the positions  $\mathcal{U}$ $q$ $\sharp(1)$ $\mathcal{U}$ $q$ $\sharp(0)$
$\mathcal{U}$ $q$ $\sharp(N)$ so that there are strategies
$\mathrm{En}(1),\mathrm{En}(0),\mathrm{En}(N):\Gamma\Rightarrow\mathcal{U}$
that compute respectively by En(1) : q ↦♯(1) En(0) : q ↦♯(0) En(N) : q ↦♯(N).

Next, we consider the inductive step to encode Pi- and Sigma-types. Assume
that a family $A=(A(\gamma))_{\gamma:\Gamma}$ of games $A(\gamma)$ interprets
a type $\mathsf{\Gamma\vdash A\ type}$, and a strategy
$\mathrm{En}(A):\Gamma\Rightarrow\mathcal{U}$ interprets the encoding
$\mathsf{\Gamma\vdash En(A):U}$. For simplicity, let $\mathsf{\Gamma}$ be the
empty context; thus, $\Gamma$ is the terminal game $T$ that has only the
trivial strategy, and $A$ is identified with a game. Assume further that a
family $B=(B(\alpha))_{\alpha:A}$ of games $B(\alpha)$ interprets a type
$\mathsf{x:A\vdash B\ type}$, and a strategy
$\mathrm{En}(B):A\Rightarrow\mathcal{U}$ interprets the encoding
$\mathsf{x:A\vdash En(B):U}$. Recall that the game semantics [Yam22]
interprets the Pi-type $\mathsf{\vdash\Pi(A,B)\ type}$ and the Sigma-type
$\mathsf{\vdash\Sigma(A,B)\ type}$ by (the singleton families of) the games
$\Pi(A,B)$ and $\Sigma(A,B)$, respectively. Then, there must be strategies
$\mathrm{En}(\Pi(A,B)),\mathrm{En}(\Sigma(A,B)):T\Rightarrow\mathcal{U}\cong\mathcal{U}$
that respectively encode these families. For this reason, the game
$\mathcal{U}$ also subsumes the positions  $\mathcal{U}$ $q$ $\sharp(\Pi)$
$a_{1}$ $a_{2}$ $\vdots$ $\mathcal{U}$ $q$ $\sharp(\Pi)$ $b_{1}$ $b_{2}$
$\vdots$ $\mathcal{U}$ $q$ $\sharp(\Sigma)$ $a_{1}$ $a_{2}$ $\vdots$
$\mathcal{U}$ $q$ $\sharp(\Sigma)$ $b_{1}$ $b_{2}$ $\vdots$ where
$a_{1}a_{2}\dots$ are moves played by the strategy
$\mathrm{En}(A):\mathcal{U}$, and $b_{1}b_{2}\dots$ by the strategy
$\mathrm{En}(B):A\Rightarrow\mathcal{U}$. In other words, we define the
strategy $\mathrm{En}(\Pi(A,B))$ to be the pairing
$\langle\mathrm{En}(A),\mathrm{En}(B)\rangle:\mathcal{U}\mathbin{\&}(A\Rightarrow\mathcal{U})$
prefixed by the moves $q.\sharp(\Pi)$, and similarly for the strategy
$\mathrm{En}(\Sigma(A,B))$. In this way, the game $\mathcal{U}$ enables the
encodings of the games $\Pi(A,B)$ and $\Sigma(A,B)$. Note, however, that the
ambient games $\mathcal{U}$ and $A\Rightarrow\mathcal{U}$ for the positions
$a_{1}a_{2}\dots$ and $b_{1}b_{2}\dots$, respectively, contain the game
$\mathcal{U}$ itself. In particular, the game $A\Rightarrow\mathcal{U}$ is not
the game $\mathcal{U}$ itself but the function game from $A$ to $\mathcal{U}$.
Accordingly, this idea necessitates a nontrivial _recursive_ definition of the
game $\mathcal{U}$. Our main technical achievement is to realise such a
definition, subsuming the general case where the game $\Gamma$ can be
different from the trivial one $T$.

Finally, there must be a strategy
$\mathrm{En}(\mathrm{Id}_{A}(\langle\alpha,\alpha^{\prime}\rangle)):\mathcal{U}$
for each pair $\alpha,\alpha^{\prime}:A$ of strategies that encodes (the
singleton family of) the game
$\mathrm{Id}_{A}(\langle\alpha,\alpha^{\prime}\rangle)$. For this reason, we
further add the positions  $\mathcal{U}$ $q$ $\sharp(\mathrm{Id})$ $a_{1}$
$a_{2}$ $\vdots$ $\mathcal{U}$ $q$ $\sharp(\mathrm{Id})$ $c_{1}$ $c_{2}$
$\vdots$ $\mathcal{U}$ $q$ $\sharp(\mathrm{Id})$ $c^{\prime}_{1}$
$c^{\prime}_{2}$ $\vdots$ where the moves $a_{1}a_{2}\dots$ are played by the
strategy $\mathrm{En}(A):\mathcal{U}$, the moves $c_{1}c_{2}\dots$ by the
strategy $\alpha:A$ and the moves $c^{\prime}_{1}c^{\prime}_{2}\dots$ by the
strategy $\alpha^{\prime}:A$. In other words, we define the strategy
$\mathrm{Id}_{A}(\langle\alpha,\alpha^{\prime}\rangle)$ to be the pairing
$\langle\mathrm{En}(A),\langle\alpha,\alpha^{\prime}\rangle\rangle:\mathcal{U}\mathbin{\&}(A\mathbin{\&}A)$
prefixed by the moves $q.\sharp(\mathrm{Id})$. It is easy to see how this can
be lifted to the general case, where the game $\Gamma$ can be different from
the trivial one $T$, and the strategies $\alpha,\alpha^{\prime}$ are on the
game $\Pi(\Gamma,A)$ for Pi-types. This generalisation is illustrated in the
next paragraph.

Now, let us see how this idea solves the problem sketched in §1.5. Instead of
the trivial assumption $\Gamma=T$, take $\Gamma=(N\Rightarrow
N)\mathbin{\&}(N\Rightarrow N)$, and further let $A$ be the singleton family
$\\{N\Rightarrow N\\}$, together with the projections
$\alpha=\pi_{1}:(N\Rightarrow N)\mathbin{\&}(N\Rightarrow
N)\rightarrow(N\Rightarrow N)$ and $\alpha^{\prime}=\pi_{2}:(N\Rightarrow
N)\mathbin{\&}(N\Rightarrow N)\rightarrow(N\Rightarrow N)$. Then, we define
the strategy $\mathrm{En}(\mathrm{Id}_{N\Rightarrow
N}(\langle\pi_{1},\pi_{2}\rangle)):(N\Rightarrow N)\mathbin{\&}(N\Rightarrow
N)\rightarrow\mathcal{U}$ to play in either of the following ways illustrated
in Figure 1, depending on the moves played by Opponent.

$(N\stackrel{{\scriptstyle f}}{{\Rightarrow}}N)$ | $\&$ | $(N\stackrel{{\scriptstyle g}}{{\Rightarrow}}N)$ | $\stackrel{{\scriptstyle\mathrm{En}(\mathrm{Id}_{N\Rightarrow N}(\langle\pi_{1},\pi_{2}\rangle))}}{{\rightarrow}}$ |  |  |  | $\mathcal{U}$ |  |
---|---|---|---|---|---|---|---|---|---
|  |  |  |  |  |  | $q$ |  |
|  |  |  |  |  |  | $\sharp(\mathrm{Id})$ |  |
|  |  |  |  | $q$ |  |  |  |
|  |  |  |  | $\sharp(\Pi)$ |  |  |  |
|  |  |  | $q$ |  |  |  |  |
|  |  |  | $\sharp(N)$ |  |  |  |  |

$(N\stackrel{{\scriptstyle f}}{{\Rightarrow}}N)$ | $\&$ | $(N\stackrel{{\scriptstyle g}}{{\Rightarrow}}N)$ | $\stackrel{{\scriptstyle\mathrm{En}(\mathrm{Id}_{N\Rightarrow N}(\langle\pi_{1},\pi_{2}\rangle))}}{{\rightarrow}}$ |  |  |  | $\mathcal{U}$ |  |
---|---|---|---|---|---|---|---|---|---
|  |  |  |  |  |  | $q$ |  |
|  |  |  |  |  |  | $\sharp(\mathrm{Id})$ |  |
|  |  |  |  | $q$ |  |  |  |
|  |  |  |  | $\sharp(\Pi)$ |  |  |  |
|  |  |  |  |  | $q$ |  |  |
|  |  |  |  |  | $\sharp(N)$ |  |  |

$(N\stackrel{{\scriptstyle f}}{{\Rightarrow}}N)$ | $\&$ | $(N\stackrel{{\scriptstyle g}}{{\Rightarrow}}N)$ | $\stackrel{{\scriptstyle\mathrm{En}(\mathrm{Id}_{N\Rightarrow N}(\langle\pi_{1},\pi_{2}\rangle))}}{{\rightarrow}}$ |  | $\mathcal{U}$ |  |
---|---|---|---|---|---|---|---
|  |  |  |  | $q$ |  |
|  |  |  |  | $\sharp(\mathrm{Id})$ |  |
|  |  |  |  |  | $c_{1}$ |
$c_{1}$ |  |  |  |  |  |  |
$c_{2}$ |  |  |  |  |  |  |
|  |  |  |  |  | $c_{2}$ |
|  |  |  |  |  | $c_{3}$ |
$c_{3}$ |  |  |  |  |  |  |
$c_{4}$ |  |  |  |  |  |  |
|  |  |  |  |  | $c_{4}$ |
|  |  | $\vdots$ |  |  |  |

$(N\stackrel{{\scriptstyle f}}{{\Rightarrow}}N)$ | $\&$ | $(N\stackrel{{\scriptstyle g}}{{\Rightarrow}}N)$ | $\stackrel{{\scriptstyle\mathrm{En}(\mathrm{Id}_{N\Rightarrow N}(\langle\pi_{1},\pi_{2}\rangle))}}{{\rightarrow}}$ |  | $\mathcal{U}$ |  |
---|---|---|---|---|---|---|---
|  |  |  |  | $q$ |  |
|  |  |  |  | $\sharp(\mathrm{Id})$ |  |
|  |  |  |  |  |  | $c^{\prime}_{1}$
|  | $c^{\prime}_{1}$ |  |  |  |  |
|  | $c^{\prime}_{2}$ |  |  |  |  |
|  |  |  |  |  |  | $c^{\prime}_{2}$
|  |  |  |  |  |  | $c^{\prime}_{3}$
|  | $c^{\prime}_{3}$ |  |  |  |  |
|  | $c^{\prime}_{4}$ |  |  |  |  |
|  |  |  |  |  |  | $c^{\prime}_{4}$
|  |  | $\vdots$ |  |  |  |

Figure 1: An illustration of the strategy on the encoding of the Id-type
between functions

In the first two patterns of Figure 1, the strategy
$\mathrm{En}(\mathrm{Id}_{N\Rightarrow N}(\langle\pi_{1},\pi_{2}\rangle))$
encodes the underlying family $A=\\{N\Rightarrow N\\}$, where recall that
function $\Rightarrow$ on games is the trivial class of Pi $\Pi$ on games.
Hence, the family $A$ is encoded simply by the pairing
$\langle\mathrm{En}(N),\mathrm{En}(N)\rangle:\mathcal{U}\mathbin{\&}\mathcal{U}$
prefixed by the moves $q.\sharp(\Pi)$.

In the last two patterns of the figure, what the strategy
$\mathrm{En}(\mathrm{Id}_{N\Rightarrow N}(\langle\pi_{1},\pi_{2}\rangle))$
does is essentially to _copy-cat_ the input strategies $f$ or $g$ given by
Opponent. Hence, this strategy is trivially effective, but also its
(potentially infinite) plays collectively have the complete information about
$f$ and $g$, in particular whether or not $f=g$. In this way, we overcome the
main problem sketched in §1.5.

###  1.7 Lifting to the cumulative hierarchy of universes

The universe $\mathsf{U}$ does not have its own code since otherwise the code
$\mathsf{\Gamma\vdash En(U):U}$ leads to inconsistency known as _Girard’s
paradox_ [Gir72]. To address this problem, Martin-Löf excluded the judgement
$\mathsf{\Gamma\vdash En(U):U}$ and proposed a _cumulative hierarchy_ of
universes $(\mathsf{U_{k}})_{k\in\mathbb{N}}$ [ML75, ML84]. The first universe
$\mathsf{U}_{0}$ does not have its own code $\mathsf{En(U_{0})}$, but the
second universe $\mathsf{U_{1}}$ has. Similarly, the second universe
$\mathsf{U}_{1}$ does not have its own code $\mathsf{En(U_{1})}$, but the
third universe $\mathsf{U_{2}}$ has, and so on. The hierarchy of these
universes is _cumulative_ : If $i<j$, then the larger universe
$\mathsf{U_{j}}$ has all codes in the smaller one $\mathsf{U_{i}}$ plus the
code $\mathsf{En(U_{i})}$. In this way, the hierarchy collectively encodes
_every_ type, including the universes themselves, by a code in some universe
$\mathrm{U_{k}}$. Note that the universe $\mathsf{U}$ is identified with the
first universe $\mathsf{U_{0}}$.

Having established the game $\mathcal{U}$ for the universe $\mathrm{U}$, it is
straightforward to interpret the cumulative hierarchy
$(\mathsf{U_{k}})_{k\in\mathbb{N}}$ of universes by a cumulative hierarchy
$(\mathcal{U}_{k})_{k\in\mathbb{N}}$ of games: For the base case, we define
$\mathcal{U}_{0}\colonequals\mathcal{U}$; for the inductive step, we define
$\mathcal{U}_{k+1}$ by adding the code $\mathrm{En}(\mathcal{U}_{i})$ for
$i=0,1,\dots,k$ to $\mathcal{U}$.

###  1.8 Main results

Based on the idea just sketched, we obtain the following main results of the
present work:

######  Theorem 1.1 (computational game semantics of universes).

The game semantics of MLTT [Yam22] is extendable to the cumulative hierarchy
of universes without sacrificing its computability.

This theorem in turn extends the independence proof of the previous work
[Yam22]:

######  Corollary 1.2 (independence of Markov’s principle).

Markov’s principle is independent from MLTT equipped with the cumulative
hierarchy of universes.

This corollary illustrates a strong advantage of game semantics: The
combinatorial reasoning of game semantics such as the independence proof
remains valid _even when game semantics is extended to new types_. Hence, when
the game semantics of MLTT has been extended to other types, the meta-
theoretic results on MLTT shown by the game semantics will be automatically
extended to those types as well.

This advantage makes game semantics a quite powerful tool for the study of
MLTT. In contrast, the syntactic proof given by Coquand and Manna [MC17], for
instance, does not have such a modular property because an extension of MLTT
may invalidate their syntactic, inductive reasoning.

###  1.9 Our contributions and related work

Our main contribution is the first game semantics of universes (Theorem 1.1)
in the 30 years history of game semantics. The main challenge in achieving
game semantics of universes is how to encode games by strategies, especially
games that interpret Id-types (§1.5). We solve this problem by the novel idea
to encode games by strategies that consist of both symbolic and non-symbolic
computations (§1.6), while we allow the decoding function $\mathrm{El}$ to be
uncomputable (without sacrificing the effective nature of the game semantics
of MLTT [Yam22]). This idea in turn requires a nontrivial recursive definition
of games for interpreting universes, and our main technical contribution is to
establish such a definition.

Another contribution is to show the independence of Makov’s principle from
MLTT equipped with the cumulative hierarchy of universes (Corollary 1.2). This
result demonstrates the modular property of the game-semantic reasoning: A
meta-theoretic result on MLTT given by the game semantics of MLTT is
automatically extended to new types as soon as the game semantics is extended
to the types.

Abramsky et al. [AJV15] establishes the first intensional semantics of a
fragment of MLTT. However, they interpret Sigma-types indirectly by a list
construction, not by games, which makes an interpretation of universes
hopeless. Besides, their method is valid only for a specific class of types
[VJA18, Figure 7], which excludes, e.g., the list type. Because the list type
is constructible by the elimination rule of N-type with respect to universes,
this limitation also implies that their approach cannot interpret universes.

Blot and Laird [BL18, Table 3] also interpret a universe, for which they write
$\mathsf{\Gamma\vdash_{\mathcal{E}}\mathcal{I}\ type}$, but their
interpretation is by domain theory [GHK+03], not game semantics. Besides, they
do not interpret Id-types and instead sketch how to interpret Id-types by
finite tuples of Boolean-type [BL18, §9]; however, this method does not work
in the presence of N-type since the set $\mathbb{N}$ of all natural numbers is
unbounded.

Finally, Coquand and Manna [MC17] show the independence of Markov’s principle
from MLTT equipped with a single universe for the first time in the
literature. Their independence proof is syntactic, which stands in contrast to
our game-semantic proof. As we have mentioned in §1.8, their syntactic proof
is not straightforward to extend to other types, while our game-semantic proof
is.

###  1.10 The structure of the present article

The rest of the present article proceeds as follows. We first prepare for the
interpretation of universes by recalling the game semantics of MLTT [Yam22] in
§2. We then proceed to our main contribution in §3: game semantics of the
cumulative hierarchy of universes. We next present immediate corollaries of
this result in §4, including the independence of Markov’s principle from MLTT
equipped with the hierarchy of universes. We finally draw a conclusion and
propose some future work in §5.

######  Notation.

We use the following notations:

  * •

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

  * •

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

  * •

We write $x_{1}x_{2}\dots x_{|\bm{s}|}$ for a sequence
$\bm{s}=(x_{1},x_{2},\dots,x_{|\bm{s}|})$, where $|\bm{s}|$ is the _length_ of
$\bm{s}$, define $\bm{s}(i)\colonequals x_{i}$ ($i\in\overline{|\bm{s}|}$) and
write $a\in\bm{s}$ if $a=\bm{s}(j)$ for some $j\in\overline{|\bm{s}|}$;

  * •

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

  * •

We write $\mathrm{Even}(\bm{s})$ (resp. $\mathrm{Odd}(\bm{s})$) if $\bm{s}$ is
of even- (resp. odd-) length, and given a set $S$ of sequences and
$\mathrm{P}\in\\{\mathrm{Even},\mathrm{Odd}\\}$, we define
$S^{\mathrm{P}}\colonequals\\{\,\bm{s}\in S\mid\mathrm{P}(\bm{s})\,\\}$;

  * •

We write $\bm{s}\preceq\bm{t}$ if $\bm{s}$ is a _prefix_ of a sequence
$\bm{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)\colonequals\\{\,\bm{s}\mid\exists\bm{t}\in
S.\,\bm{s}\preceq\bm{t}\,\\}$.

##  2 Review: game semantics of Martin-Löf type theory

In this section, we recall the game semantics of MLTT given in the previous
work [Yam22]. To this end, we first recall games and strategies à la McCusker
[McC98] (with the slight modifications made by the previous work [Yam22]) that
interpret simple type theories [AM99] in §2.1 since the previous work is based
on this variant of games and strategies. We then review basic definitions and
results of the game semantics of MLTT [Yam22] in §2.2. Our exposition is
minimal; see the tutorial [AM99] and the previous work [Yam22] for more
explanations and examples.

###  2.1 Games and strategies

_Games_ are a class of directed rooted forests. For technical convenience, we
identify games with the sets of all paths from the roots, called _positions_.
The vertices of games are called _moves_ , and positions must be _legal_.
These concepts are centred around the structure of _arenas_.

######  Definition 2.1 (moves [Yam22]).

Let us fix arbitrary pairwise distinct symbols $\mathrm{O}$, $\mathrm{P}$,
$\mathrm{Q}$ and $\mathrm{A}$, and call them _labels_. A _move_ is a triple
$m^{xy}\colonequals(m,x,y)$ such that $x\in\\{\mathrm{O},\mathrm{P}\\}$ and
$y\in\\{\mathrm{Q},\mathrm{A}\\}$. We abbreviate moves $m^{xy}$ as $m$ and
instead define $\lambda(m)\colonequals xy$,
$\lambda^{\mathrm{OP}}(m)\colonequals x$ and
$\lambda^{\mathrm{QA}}(m)\colonequals y$.

We call a move $m$ 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.2 (arenas [McC98, Yam22, HO00]).

An _arena_ is a pair $G=(M_{G},\vdash_{G})$ of

  * •

A set $M_{G}$ of moves;

  * •

A subset $\vdash_{G}$ of the cartesian product $(\\{\star\\}\cup M_{G})\times
M_{G}$, where $\star$ (also written $\star_{G}$) is an arbitrarily fixed
element such that $\star\not\in M_{G}$, called the _enabling relation_ , that
satisfies

    * –

(E1) If $\star\vdash_{G}m$, then $\lambda(m)=\mathrm{OQ}$;

    * –

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

    * –

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

We call moves $m\in M_{G}$ _initial_ if $\star\vdash_{G}m$, and define the set
$M_{G}^{\mathrm{Init}}\colonequals\\{\,m\in M_{G}\mid\star\vdash_{G}m\,\\}$ of
all initial moves of $G$. An arena $G$ is _well-founded_ if the relation
$\vdash_{G}$ is well-founded, i.e., there is no sequence
$(m_{i})_{i\in\mathbb{N}}$ of moves $m_{i}\in M_{G}$ such that
$\star\vdash_{G}m_{0}$ and $m_{i}\vdash_{G}m_{i+1}$ for all $i\in\mathbb{N}$.

Strictly speaking, positions of games are sequences of moves equipped with
_pointers_ :

######  Definition 2.3 (j-sequences [HO00, Coq95, McC98]).

An _occurrence_ in a finite sequence $\bm{s}$ is a pair $(\bm{s}(i),i)$ such
that $i\in\overline{|\bm{s}|}$. A _justified (j-) sequence_ is a pair
$\bm{s}=(\bm{s},\mathcal{J}_{\bm{s}})$ of a finite sequence $\bm{s}$ of moves
and a map
$\mathcal{J}_{\bm{s}}:\overline{|\bm{s}|}\rightarrow\\{0\\}\cup\overline{|\bm{s}|-1}$
such that $0\leqslant\mathcal{J}_{\bm{s}}(i)<i$ for all
$i\in\overline{|\bm{s}|}$, called the _pointer_ of the j-sequence. An
occurrence $(\bm{s}(i),i)$ is _initial_ in $\bm{s}$ if
$\mathcal{J}_{\bm{s}}(i)=0$.

We say that the occurrence
$(\bm{s}({\mathcal{J}_{\bm{s}}(i)}),\mathcal{J}_{\bm{s}}(i))$ is the
_justifier_ of a non-initial one $(\bm{s}(i),i)$ in $\bm{s}$, and
$(\bm{s}(i),i)$ is _justified_ by
$(\bm{s}({\mathcal{J}_{\bm{s}}(i)}),\mathcal{J}_{\bm{s}}(i))$ in $\bm{s}$. A
j-sequence $\bm{s}$ is _in an arena_ $G$ if its elements are moves of $G$, and
its pointer respects the relation $\vdash_{G}$ in $G$, i.e., $\forall
i\in\overline{|\bm{s}|}.\,\big{(}\mathcal{J}_{\bm{s}}(i)=0\Rightarrow\star\vdash_{G}\bm{s}(i)\big{)}\wedge\big{(}\mathcal{J}_{\bm{s}}(i)\neq
0\Rightarrow\bm{s}({\mathcal{J}_{\bm{s}}(i)})\vdash_{G}\bm{s}(i)\big{)}$. We
write $\mathscr{J}_{G}$ for the set of all j-sequences in $G$. A _justified
(j-) subsequence_ of a j-sequence $\bm{s}$ is a j-sequence $\bm{t}$, written
$\bm{t}\sqsubseteq\bm{s}$, such that $\bm{t}$ is a subsequence of $\bm{s}$,
and $\mathcal{J}_{\bm{t}}(i)=j$ if and only if $\mathcal{J}_{\bm{s}}^{n}(i)=j$
for some $n\in\mathbb{N}_{+}$ with the occurrences
$(\bm{s}(\mathcal{J}_{\bm{s}}^{k}(i)),\mathcal{J}_{\bm{s}}^{k}(i))$ for
$k=1,2,\dots,n-1$ deleted in $\bm{t}$.

######  Convention.

We are henceforth casual about the distinction between moves and occurrences,
and by abuse of notation, we frequently keep the pointer
$\mathcal{J}_{\bm{s}}$ of each j-sequence
$\bm{s}=(\bm{s},\mathcal{J}_{\bm{s}})$ implicit since it is mostly obvious,
and abbreviate occurrences $(\bm{s}(i),i)$ in $\bm{s}$ as $\bm{s}(i)$. We
write $\mathcal{J}_{\bm{s}}(\bm{s}(i))=\bm{s}(j)$ if
$\mathcal{J}_{\bm{s}}(i)=j>0$.

######  Definition 2.4 (views [Coq95, HO00, McC98]).

The _P-view_ $\lceil\bm{s}\rceil$ and the _O-view_ $\lfloor\bm{s}\rfloor$ of a
j-sequence $\bm{s}$ are the j-subsequences of $\bm{s}$ defined by the
induction

  * •

$\lceil\bm{\epsilon}\rceil\colonequals\bm{\epsilon}$;

  * •

$\lceil\bm{s}m\rceil\colonequals\lceil\bm{s}\rceil.m$ if $m$ is a P-move;

  * •

$\lceil\bm{s}m\rceil\colonequals m$ if $m$ is initial;

  * •

$\lceil\bm{s}m\bm{t}n\rceil\colonequals\lceil\bm{s}\rceil.mn$ if $n$ is an
O-move such that $m$ justifies $n$;

  * •

$\lfloor\bm{\epsilon}\rfloor\colonequals\bm{\epsilon}$;

  * •

$\lfloor\bm{s}m\rfloor\colonequals\lfloor\bm{s}\rfloor.m$ if $m$ is an O-move;

  * •

$\lfloor\bm{s}m\bm{t}n\rfloor\colonequals\lfloor\bm{s}\rfloor.mn$ if $n$ is a
P-move such that $m$ justifies $n$.

######  Definition 2.5 (legal positions [AM99, McC98]).

A _legal position_ is a j-sequence $\bm{s}$ such that

  * •

(Alternation) If $\bm{s}=\bm{s_{1}}mn\bm{s_{2}}$, then
$\lambda^{\mathrm{OP}}(m)\neq\lambda^{\mathrm{OP}}(n)$;

  * •

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

A legal position is _in an arena_ $G$ if it is a j-sequence in $G$ (Definition
2.3). We write $\mathscr{L}_{G}$ for the set of all legal positions in $G$.

######  Definition 2.6 (games [McC98, AM99, Yam22]).

A _game_ is a set $G$ of legal positions such that

  1. 1.

$G$ is nonempty and _prefix-closed_ (i.e., $\bm{s}m\in G\Rightarrow\bm{s}\in
G$);

  2. 2.

$\mathrm{Arn}(G)\colonequals(M_{G},\vdash_{G})$ is an arena, where
$M_{G}\colonequals\\{\,\bm{s}(i)\mid\bm{s}\in G,i\in\overline{|\bm{s}|}\,\\}$
and $\vdash_{G}\,\colonequals\\{\,(\star,\bm{s}(j))\mid\bm{s}\in
G,\mathcal{J}_{\bm{s}}(j)=0\,\\}\cup\\{\,(\bm{s}(i),\bm{s}(j))\mid\bm{s}\in
S,\mathcal{J}_{\bm{s}}(j)=i>0\,\\}$.

A game $G$ is _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 $\bm{s}m\in G$ and $m\in M_{G}^{\mathrm{Init}}$ implies
$\bm{s}=\bm{\epsilon}$). We call elements of $G$ _(valid) positions_ in $G$. A
_subgame_ of $G$ is a game $H\subseteq G$, and
$\mathrm{sub}(G)\colonequals\\{\,H\mid\text{$H$ is a subgame of $G$}\,\\}$.

######  Example 2.7.

The simplest game is the _terminal game_ $T\colonequals\\{\bm{\epsilon}\\}$
which only has the trivial position $\bm{\epsilon}$. The _flat game_ on a
given set $S$ is the game
$\mathrm{flat}(S)\colonequals\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}}$. Consider, for instance,
the _empty game_ $0\colonequals\mathrm{flat}(\emptyset)$ and the _natural
number game_ $N\colonequals\mathrm{flat}(\mathbb{N})$. As the notation
indicates, the empty game $0$ interprets Zero-type, and the natural number
game $N$ interprets N-type (§2.2).

On the other hand, _strategies_ on a game $G$ are algorithms for Player about
how to play on $G$:

######  Definition 2.8 (strategies [McC98]).

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.,
$\bm{s}mn\in\sigma\Rightarrow\bm{s}\in\sigma$) and _deterministic_ (i.e.,
$\bm{s}mn,\bm{s}mn^{\prime}\in\sigma\Rightarrow\bm{s}mn=\bm{s}mn^{\prime}$).
We write $\mathrm{st}(G)$ for the set $\\{\,\sigma\mid\sigma:G\,\\}$ of all
strategies on $G$.

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

######  Example 2.9.

The terminal game $T$ only has the trivial strategy
$\top\colonequals\\{\bm{\epsilon}\\}$, and the flat game $\mathrm{flat}(S)$ on
a given set $S$ has strategies $\bot\colonequals\\{\bm{\epsilon}\\}$ and
$\underline{m}\colonequals\\{\bm{\epsilon},qm\\}$ for each $m\in S$.

Strategies are _unrestricted_ computations, e.g., they can be _partial_ , some
of which do not correspond to proofs in logic or formal systems. This
motivates _winning_ and _well-bracketing_ on strategies: Winning strategies
correspond to proofs in classical logic, and winning, well-bracketed ones to
proofs in intuitionistic logic. Because the underlying logic of MLTT is
intuitionistic, we achieve a tight correspondence between MLTT and game
semantics by focusing on winning, well-bracketed strategies.

######  Definition 2.10 (constraints on strategies [Coq95, Lai97, McC98,
AM99]).

A strategy $\sigma:G$ is

  * •

_Total_ if it always responds: $\forall\bm{s}\in\sigma,\bm{s}m\in
G.\,\exists\bm{s}mn\in\sigma$;

  * •

_Innocent_ if it only depends on P-views: $\forall\bm{s}mn\in\sigma,\bm{t}l\in
G.\,\lceil\bm{s}m\rceil=\lceil\bm{t}l\rceil\Rightarrow\exists\bm{t}lr\in\sigma.\,\lceil\bm{s}mn\rceil=\lceil\bm{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\colonequals\\{\,\lceil\bm{s}\rceil\mid\bm{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 $\bm{s}q\bm{t}a\in\sigma$, where
$\lambda^{\mathrm{QA}}(q)=\mathrm{Q}$, $\lambda^{\mathrm{QA}}(a)=\mathrm{A}$
and $\mathcal{J}_{\bm{s}q\bm{t}a}(a)=q$, then each question occurring in
$\bm{t^{\prime}}$, where the P-view $\lceil\bm{s}q\bm{t}\rceil$ has
$\lceil\bm{s}q\bm{t}\rceil=\lceil\bm{s}q\rceil.\bm{t^{\prime}}$ by visibility,
justifies an answer occurring in $\bm{t^{\prime}}$.

######  Example 2.11.

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.

Let us next recall standard constructions on games and strategies.

######  Convention.

For brevity and readability, we omit ‘tags’ for disjoint union $\uplus$. For
instance, we write $x\in A\uplus B$ if $x\in A$ or $x\in B$; also, given
relations $R_{A}\subseteq A\times A$ and $R_{B}\subseteq B\times B$, we write
$R_{A}\uplus R_{B}$ for the relation on $A\uplus B$ such that $(x,y)\in
R_{A}\uplus R_{B}\Leftrightarrow/(x,y)\in R_{A}\vee(x,y)\in R_{B}$.

######  Definition 2.12 (constructions on arenas [McC98]).

Given arenas $A$ and $B$, we define

  * •

$A\uplus B\colonequals(M_{A}\uplus M_{B},\vdash_{A}\uplus\vdash_{B})$;

  * •

$A\multimap B\colonequals(\\{\,a^{(x^{\bot})y}\mid a^{xy}\in M_{A}\,\\}\uplus
M_{B},\vdash_{A\multimap B})$, $\mathrm{O}^{\bot}\colonequals\mathrm{P}$,
$\mathrm{P}^{\bot}\colonequals\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)$.

######  Definition 2.13 (constructions on games [McC98]).

Given games $G$ and $H$, we define

  * •

The _tensor_ $G\otimes
H\colonequals\\{\,\bm{s}\in\mathscr{L}_{\mathrm{Arn}(G)\uplus\mathrm{Arn}(H)}\mid\forall
X\in\\{G,H\\}.\,\bm{s}\upharpoonright X\in X\,\\}$ of $G$ and $H$, where
$\bm{s}\upharpoonright X\sqsubseteq\bm{s}$ consists of occurrences of moves in
$X$;

  * •

The _exponential_ $\oc
G\colonequals\\{\,\bm{s}\in\mathscr{L}_{\mathrm{Arn}(G)}\mid\forall
i\in|\bm{s}|.\,\mathcal{J}_{\bm{s}}(i)=0\Rightarrow\bm{s}\upharpoonright\\{(\bm{s}(i),i)\\}\in
G\,\\}$ of $G$, where
$\bm{s}\upharpoonright\\{(\bm{s}(i),i)\\}\sqsubseteq\bm{s}$ consists of
occurrence in $\bm{s}$ hereditarily justified by the initial one
$(\bm{s}(i),i)$ in $\bm{s}$;

  * •

The _product_
$G\mathbin{\&}H\colonequals\\{\,\bm{s}\in\mathscr{L}_{\mathrm{Arn}(G)\mathbin{\uplus}\mathrm{Arn}(H)}\mid(\bm{s}\upharpoonright
G\in G\wedge\bm{s}\upharpoonright H=\bm{\epsilon})\vee(\bm{s}\upharpoonright
G=\bm{\epsilon}\wedge\bm{s}\upharpoonright H\in H)\,\\}$ of $G$ and $H$;

  * •

The _linear implication_ $G\multimap
H\colonequals\\{\,\bm{s}\in\mathscr{L}_{\mathrm{Arn}(G)\multimap\mathrm{Arn}(H)}\mid\bm{s}\upharpoonright
G^{\bot}\in G,\bm{s}\upharpoonright H\in H\,\\}$ from $G$ to $H$, also written
$H^{G}$, where $\bm{s}\upharpoonright G^{\bot}$ is obtained from
$\bm{s}\upharpoonright G$ by modifying all the moves $m^{(x^{\bot})y}$
occurring in $\bm{s}\upharpoonright G$ into $m^{xy}$;

  * •

The _implication_ $G\Rightarrow H\colonequals\oc G\multimap H$ from $G$ to
$H$.

Notationally, exponential $\oc$ precedes other constructions on games, while
tensor $\otimes$ and product $\mathbin{\&}$ do linear implication $\multimap$
and implication $\Rightarrow$.

######  Definition 2.14 (constructions on strategies [McC98]).

Given strategies $\phi:A\multimap B$, $\sigma:C\multimap D$, $\tau:A\multimap
C$, $\psi:B\multimap C$ and $\theta:\oc A\multimap B$, we define

  * •

The _copy-cat_ $\mathrm{cp}_{A}\colonequals\\{\,\bm{s}\in(A_{[0]}\multimap
A_{[1]})^{\mathrm{Even}}\mid\forall\bm{t}\preceq\bm{s}.\,\mathrm{Even}(\bm{t})\Rightarrow\bm{t}\upharpoonright
A_{[0]}^{\bot}=\bm{t}\upharpoonright A_{[1]}\,\\}$ on $A$;

  * •

The _dereliction_ $\mathrm{der}_{A}\colonequals\\{\,\bm{s}\in(\oc A\multimap
A)^{\mathrm{Even}}\mid\forall\bm{t}\preceq\bm{s}.\,\mathrm{Even}(\bm{t})\Rightarrow\bm{t}\upharpoonright\oc
A^{\bot}=\bm{t}\upharpoonright A\,\\}$ on $A$;

  * •

The _tensor_ $\phi\otimes\sigma\colonequals\\{\,\bm{s}\in A\otimes C\multimap
B\otimes D\mid\bm{s}\upharpoonright A,B\in\phi,\bm{s}\upharpoonright
C,D\in\sigma\,\\}$ of $\phi$ and $\sigma$, where $\bm{s}\upharpoonright
A,B\sqsubseteq\bm{s}$ (resp. $\bm{s}\upharpoonright C,D\sqsubseteq\bm{s}$)
consists of occurrences of moves in $A$ or $B$ (resp. $C$ or $D$);

  * •

The _pairing_ $\langle\phi,\tau\rangle\colonequals\\{\,\bm{s}\in A\multimap
B\mathbin{\&}C\mid(\bm{s}\upharpoonright A,B\in\phi\wedge\bm{s}\upharpoonright
C=\bm{\epsilon})\vee(\bm{s}\upharpoonright
A,C\in\tau\wedge\bm{s}\upharpoonright B=\bm{\epsilon})\,\\}$ of $\phi$ and
$\tau$;

  * •

The _composition_ $\phi;\psi\colonequals\\{\,\bm{s}\upharpoonright
A,C\mid\bm{s}\in\phi\parallel\psi\,\\}$ of $\phi$ and $\psi$ (n.b.,
$\phi;\psi$ is also written $\psi\circ\phi$), where
$\phi\parallel\psi\colonequals\\{\,\bm{s}\in\mathscr{J}\mid\bm{s}\upharpoonright
A,B_{[0]}\in\phi,\bm{s}\upharpoonright B_{[1]},C\in\psi,\bm{s}\upharpoonright
B_{[0]}^{\bot},B_{[1]}^{\bot}\in\mathrm{cp}_{B}\,\\}$,
$\mathscr{J}\colonequals\mathscr{J}_{\mathrm{Arn}(((A\multimap
B_{[0]})\multimap B_{[1]})\multimap C)}$, $\bm{s}\upharpoonright
B_{[0]}^{\bot},B_{[1]}^{\bot}$ is obtained from $\bm{s}\upharpoonright
B_{[0]},B_{[1]}$ by applying the operation $(\\_)^{\bot}:m^{xy}\mapsto
m^{x^{\bot}y}$ (Definition 2.12) on all moves $m^{xy}$;

  * •

The _promotion_ $\theta^{\dagger}\colonequals\\{\,\bm{s}\in(\oc A\multimap\oc
B)^{\mathrm{Even}}\mid\forall
i\in|\bm{s}|.\,\mathcal{J}_{\bm{s}}(i)=0\Rightarrow\bm{s}\upharpoonright\\{(\bm{s}(i),i)\\}\in\theta\,\\}$
of $\theta$.

######  Example 2.15.

The promotion $\mathrm{succ}^{\dagger}:\oc N\multimap\oc N$ of the strategy

$\mathrm{succ}\colonequals\\{\,q_{[1]}.q_{[0]}.n_{[0]}.n+1_{[1]}\mid
n\in\mathbb{N}\,\\}:N_{[0]}\Rightarrow N_{[1]}$

computes as sketched in the introduction (§1.3).

Let us summarise the present section by:

######  Definition 2.16 (categories of games [McC98, Yam22]).

The category $\mathbb{G}_{\oc}$ consists of

  * •

Well-opened games as objects;

  * •

Strategies on the implication $A\Rightarrow B$ as morphisms $A\rightarrow B$;

  * •

The composition
$\psi\bullet\phi\colonequals\psi\circ\phi^{\dagger}:A\Rightarrow C$ of
strategies as the composition of morphisms $\phi:A\rightarrow B$ and
$\psi:B\rightarrow C$;

  * •

The dereliction $\mathrm{der}_{A}$ as the identity on each object $A$.

The subcategory $\mathbb{LG}_{\oc}$ (resp. $\mathbb{WG}$) of
$\mathbb{G}_{\oc}$ consists of well-founded, well-opened games as objects, and
winning (resp. winning, well-bracketed) strategies as morphisms.

We have to focus on _well-opened_ games in these categories since otherwise
the identities would not be well-defined [McC98, pp. 42–43]. We use the
subscript $(\\_)_{\oc}$ in order to distinguish these categories from the
_linear_ ones, in which morphisms $A\rightarrow B$ are strategies on the
linear implication $A\multimap B$.

######  Notation.

We are not bothered about the distinction between strategies on games $G$ and
$T\Rightarrow G$.

###  2.2 Game semantics of Martin-Löf type theory

The previous work [Yam22] establishes game semantics of MLTT based on games
and strategies recalled in the previous section. The central idea of the
precious work is to generalise games into _predicate (p-) games_ , which
corresponds to the generalisation of simple types to dependent types:

######  Definition 2.17 (p-games [Yam22]).

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|$. It is _well-founded_ (resp. _well-
opened_) if so is $|\Gamma|$.

######  Example 2.18.

Given a game $G$, we have the p-game
$\mathscr{P}(G)\colonequals(G,\kappa_{G})$, where $\kappa_{G}$ is the constant
family at $G$. Clearly, $G$ and $\mathscr{P}(G)$ are essentially the same. 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.

Before recalling strategies on p-games, we need a few preliminary concepts:

######  Definition 2.19 (liveness ordering [Chr00]).

The _liveness ordering_ is a partial order $\preccurlyeq$ between games
[Chr00, Definition 8 and Theorem 9], which defines $G\preccurlyeq H$ to mean
that O (resp. P) is less (resp. more) restricted in $G$ than in $H$, i.e.,
they satisfy

  1. 1.

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

  2. 2.

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

######  Definition 2.20 (closures of strategies [Yam22]).

The _closure_ of a strategy $\sigma:G$ with respect to another game $H$ is the
subgame
$\overline{\sigma}_{H}\colonequals\\{\bm{\epsilon}\\}\cup\\{\,\bm{s}m\in
H^{\mathrm{Odd}}\mid\bm{s}\in\overline{\sigma}_{H}\,\\}\cup\\{\,\bm{t}lr\in\sigma\mid\bm{t}l\in\overline{\sigma}_{H}\,\\}\subseteq\sigma\cup
H$.

We see by induction that $\overline{\sigma}_{G}=\sigma\cup\\{\,\bm{s}m\in
G\mid\bm{s}\in\sigma\,\\}$ holds for all strategies $\sigma:G$. Moreover:

######  Proposition 2.21 (liveness characterisation [Yam22]).

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

This proposition enables us to define strategies on p-games as follows:

######  Definition 2.22 (strategies on p-games [Yam22]).

A _strategy_ on a p-game $\Gamma$, written $\gamma:\Gamma$, is a strategy
$\gamma:|\Gamma|$ such that
$\overline{\gamma}_{|\Gamma|}\preccurlyeq\Gamma(\gamma)$. It is _total_ (resp.
_innocent_ , _noetherian_ , _well-bracketed_) if so is
$\gamma\cap\Gamma(\gamma):\Gamma(\gamma)$.

We write $\mathrm{st}(\Gamma)$ for the set $\\{\,\gamma\mid\gamma:\Gamma\,\\}$
of all strategies on a p-game $\Gamma$ and define
$\overline{\gamma}_{\Gamma}\colonequals\overline{\gamma}_{\Gamma(\gamma)}$ for
all $\gamma:\Gamma$. A _position_ in $\Gamma$ is a prefix of a sequence
$q_{\Gamma}\gamma\bm{s}$ such that $\gamma:\Gamma$ and
$\bm{s}\in\overline{\gamma}_{\Gamma}$, where $q_{\Gamma}$ is an arbitrarily
fixed element such that $q_{\Gamma}\not\in M_{|\Gamma|}$, $q_{\Gamma}\gamma$
is called an _initial protocol_ , and $\bm{s}$ is called an _actual position_.

A play in $\Gamma$ proceeds as follows. First, _Judge_ asks Player a question
$q_{\Gamma}$ (‘What is your strategy?’) and she answers it by a strategy
$\gamma:\Gamma$ (‘It is $\gamma$!’). After this initial protocol, an ordinary
play on the game $\Gamma(\gamma)$ between Player and Opponent follows, in
which Player must use the declared one $\gamma$ restricted to
$\Gamma(\gamma)$, i.e.,
$\gamma\cap\Gamma(\gamma)=\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}}:\Gamma(\gamma)$.
Thus, $\gamma:\Gamma$ is _winning_ (resp. _well-bracketed_) if so is
$\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}}:\Gamma(\gamma)$.

Judge and the initial protocol are mere devices for requiring Player to _fix_
the strategy $\gamma:|\Gamma|$ and the game $\Gamma(\gamma)$ that _pass the
test_ $\overline{\gamma}_{\Gamma(\gamma)}^{\mathrm{Even}}:\Gamma(\gamma)$. See
the beginning of [Yam22, §3] for an illustration of how and why these strategy
filtering and fixing are necessary for an interpretation of MLTT.

We next recall basic constructions on p-games:

######  Notation.

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

Given a strategy $\sigma$ on the tensor $G_{0}\otimes G_{1}$ of games $G_{i}$
($i=0,1$), we define

$\sigma\upharpoonright G_{i}\colonequals\begin{cases}\sigma_{i}&\text{if
$\sigma=\sigma_{0}\otimes\sigma_{1}$ for (necessarily unique)
$\sigma_{0}:G_{0}$ and $\sigma_{1}:G_{1}$;}\\\ \uparrow&\text{otherwise, where
$\uparrow$ means being \emph{undefined}.}\end{cases}$ (1)

Similarly, given a strategy $\tau$ on the exponential $\oc G$ of a game $G$
and $j\in\mathbb{N}$, we define

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

Given a p-game $\Gamma$, we define the value $\Gamma(\uparrow)$ to be
_undefined_ , and the constructions $\otimes$, $\multimap$, $\&$ and $\oc$ 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 2.23 (product and tensor on p-games [Yam22]).

The _product_ of p-games $\Gamma$ and $\Delta$ is the p-game
$\Gamma\mathbin{\&}\Delta$ defined by
$|\Gamma\mathbin{\&}\Delta|\colonequals|\Gamma|\mathbin{\&}|\Delta|$ and
$(\Gamma\mathbin{\&}\Delta)(\langle\gamma,\delta\rangle)\colonequals\Gamma(\gamma)\mathbin{\&}\Delta(\delta)$
for all $\langle\gamma,\delta\rangle:|\Gamma\mathbin{\&}\Delta|$, and their
_tensor_ is the p-game $\Gamma\otimes\Delta$ defined by
$|\Gamma\otimes\Delta|\colonequals|\Gamma|\otimes|\Delta|$ and
$(\Gamma\otimes\Delta)(\sigma)\colonequals\Gamma(\sigma\upharpoonright|\Gamma|)\otimes\Delta(\sigma\upharpoonright|\Delta|)$
for all $\sigma:|\Gamma\otimes\Delta|$.

######  Definition 2.24 (countable tensor [Yam22]).

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}\colonequals\\{\,\bm{s}\in\oc H\mid\forall
j\in\mathbb{N}.\,\bm{s}\upharpoonright j\in G_{j}\,\\}\subseteq\oc H$.

######  Definition 2.25 (exponential on p-games [Yam22]).

The _exponential_ of a p-game $\Gamma$ is the p-game $\oc\Gamma$ defined by
$|\oc\Gamma|\colonequals\oc|\Gamma|$ and
$(\oc\Gamma)(\sigma)\colonequals\otimes_{i\in\mathbb{N}}\Gamma(\sigma\upharpoonright
i)$ for all $\sigma:|\oc\Gamma|$.

Hence, strategies on $\Gamma\mathbin{\&}\Delta$ are the pairings
$\langle\gamma,\delta\rangle$ of $\gamma:\Gamma$ and $\delta:\Delta$,
strategies on $\Gamma\otimes\Delta$ are the tensors $\gamma\otimes\delta$ of
$\gamma:\Gamma$ and $\delta:\Delta$, and strategies on $\oc\Gamma$ are those
$\sigma:\oc|\Gamma|$ such that $\\{\,\bm{s}\upharpoonright
i\mid\bm{s}\in\sigma\,\\}:\Gamma$ for all $i\in\mathbb{N}$.

######  Definition 2.26 (categories of p-games [Yam22]).

The category $\mathbb{PG}_{\oc}$ 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\colonequals\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}_{\oc}$ (resp. $\mathbb{WPG}_{\oc}$) of
$\mathbb{PG}_{\oc}$ consists of well-founded, well-opened p-games as objects,
and winning (resp. winning, well-bracketed) strategies as morphisms.

Because the underlying logic of MLTT is intuitionistic, the previous work
[Yam22] focuses on the category $\mathbb{WPG}_{\oc}$. It establishes game
semantics of MLTT by showing that the category $\mathbb{WPG}_{\oc}$ gives rise
to abstract semantics of MLTT, called a _category with families (CwF)_
[Dyb96]:

######  Definition 2.27 (CwFs [Dyb96, Hof97]).

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

  * •

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

  * •

$\mathrm{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$;

  * •

To each morphism $\phi:\Delta\to\Gamma$, $\\_\\{\\_\\}$ assigns 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 _substitutions 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$;

  * •

$\mathrm{p}$ (resp. $\mathrm{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$ (resp. a term
$\mathrm{v}_{A}\in\mathrm{Tm}(\Gamma.A,A\\{\mathrm{p}_{A}\\})$), called the
_first projection_ on $A$ (resp. the _second projection_ on $A$);

  * •

$\langle\\_,\\_\rangle_{\\_}$ assigns, to each triple
$(\phi,A,\check{\alpha})$ of a morphism $\phi:\Delta\to\Gamma$, a type
$A\in\mathrm{Ty}(\Gamma)$ and a term
$\check{\alpha}\in\mathrm{Tm}(\Delta,A\\{\phi\\})$, a morphism
$\langle\phi,\check{\alpha}\rangle_{A}:\Delta\to\Gamma.A$, called the
_extension_ of $\phi$ by $\check{\alpha}$,

that satisfies, for any $\Theta\in\mathcal{C}$, $\varphi:\Theta\to\Delta$ and
$\alpha\in\mathrm{Tm}(\Gamma,A)$, the equations A { id_Γ} = A A { ϕ∘φ} = A {
ϕ} { φ} α{ id_Γ}_A = αα{ ϕ∘φ}_A = α{ ϕ}_A { φ}_A{ϕ} p_A ∘⟨ϕ, ˇα ⟩_A = ϕv_A {
⟨ϕ, ˇα ⟩_A } = ˇα ⟨ϕ, ˇα ⟩_A ∘φ= ⟨ϕ∘φ, ˇα { φ}_A{ϕ} ⟩_A ⟨p_A, v_A ⟩_A = id_Γ.
A.

We sometimes write $\mathrm{Ty}_{\mathcal{C}}$, $\mathrm{Term}_{\mathcal{C}}$
and so on when we would like to emphasise the underlying CwF $\mathcal{C}$.
Roughly, judgements of MLTT are interpreted in a CwF $\mathcal{C}$ by ⊢Γ ctx
↦⟦Γ ⟧∈C Γ⊢A type ↦⟦A ⟧∈Ty(⟦Γ ⟧) Γ⊢a : A ↦⟦A ⟧∈Tm(⟦Γ ⟧, ⟦A ⟧) ⊢Γ= Δ ctx ⇒⟦Γ ⟧=
⟦Δ ⟧Γ⊢A = B type ⇒⟦A ⟧= ⟦B ⟧Γ⊢a = a’ : A ⇒⟦A ⟧= ⟦a’ ⟧, where
$\llbracket\\_\rrbracket$ denotes the _semantic map_ or _interpretation_. See
[Hof97] for the details.

In the following, we recall the additional structures on the category
$\mathbb{WPG}_{\oc}$ that lift it to a CwF. First, types in the CwF
$\mathbb{WPG}_{\oc}$ are _dependent p-games_ :

######  Definition 2.28 (dependent p-games [Yam22]).

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}_{\oc}(\Gamma)}$ of p-games
$L(\gamma_{0})$ such that $|L(\gamma_{0})|=|L|$. It is _well-opened_ (resp.
_well-founded_) if so is $|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

$L^{\star}(\gamma)\colonequals\begin{cases}L(\gamma)&\text{if
$\gamma\in\mathbb{WPG}_{\oc}(\Gamma)$;}\\\
\mathscr{P}(|L|)&\text{otherwise.}\end{cases}$ (3)

A _dependent predicate (p-) game_ over $\Gamma$ is a linearly dependent one
over the exponential $\oc\Gamma$.

######  Notation.

We write $\mathscr{D}_{\ell}(\Gamma)$ (resp.
$\mathscr{D}_{\ell}^{\mathrm{w}}(\Gamma)$) for the set of all linearly
dependent p-games (resp. well-opened, well-founded ones) over $\Gamma$, and
$\\{\Gamma^{\prime}\\}_{\Gamma}$ or $\\{\Gamma^{\prime}\\}$ for the _constant_
one at $\Gamma^{\prime}$, i.e.,
$\\{\Gamma^{\prime}\\}_{\Gamma}\colonequals(\Gamma^{\prime},\gamma:\Gamma\mapsto\Gamma^{\prime})$.
Let $\mathscr{D}(\Gamma)\colonequals\mathscr{D}_{\ell}(\oc\Gamma)$ and
$\mathscr{D}^{\mathrm{w}}(\Gamma)\colonequals\mathscr{D}^{\mathrm{w}}_{\ell}(\oc\Gamma)$.
We often write $\gamma_{0}^{\dagger}$ for an arbitrary element of
$\mathbb{WPG}_{\oc}(\oc\Gamma)$, where
$\gamma_{0}\in\mathbb{WPG}_{\oc}(\Gamma)$, since elements of
$\mathbb{WPG}_{\oc}(\oc\Gamma)$ are all _innocent_ and so promotions of
elements of $\mathbb{WPG}_{\oc}(\Gamma)$.

Next, terms in the CwF $\mathbb{WPG}_{\oc}$ are winning, well-bracketed
strategies on the following p-games:

######  Definition 2.29 (linear-pi and pi [Yam22]).

Let $L$ be a linearly dependent p-game over a p-game $\Gamma$, and $A$ be 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)|\colonequals|L|^{|\Gamma|}$ and for all
$\phi:|\Pi_{\ell}(\Gamma,L)|$

$\displaystyle\Pi_{\ell}(\Gamma,L)(\phi)$
$\displaystyle\colonequals\\{\bm{\epsilon}\\}\cup\\{\,\bm{s}m\in|\Pi_{\ell}(\Gamma,L)|^{\mathrm{Odd}}\mid\bm{s}\in\Pi_{\ell}(\Gamma,L)(\phi),\exists\gamma:\Gamma.\,\bm{s}m\in
L^{\star}(\gamma)(\phi\circ\gamma)^{\overline{\gamma}_{\Gamma}}\,\\}$
$\displaystyle\cup\\{\,\bm{t}lr\in|\Pi_{\ell}(\Gamma,L)|^{\mathrm{Even}}\mid\bm{t}l\in\Pi_{\ell}(\Gamma,L)(\phi),\forall\gamma:\Gamma.\,\bm{t}l\in
L^{\star}(\gamma)(\phi\circ\gamma)^{\overline{\gamma}_{\Gamma}}\Rightarrow\bm{t}lr\in
L^{\star}(\gamma)(\phi\circ\gamma)^{\overline{\gamma}_{\Gamma}}\,\\},$

and the _pi_ from $\Gamma$ to $A$ is the linear-pi
$\Pi(\Gamma,A)\colonequals\Pi_{\ell}(\oc\Gamma,A)$. We write
$\Gamma\Rightarrow A$ for $\Pi(\Gamma,A)$ if $A$ is constant.

Finally, comprehensions in the CwF $\mathbb{WPG}_{\oc}$ are given by:

######  Definition 2.30 (sigma [Yam22]).

The _sigma_ of a p-game $\Gamma$ and a dependent p-game $A$ over $\Gamma$ is
the p-game $\Sigma(\Gamma,A)$ defined by
$|\Sigma(\Gamma,A)|\colonequals|\Gamma|\mathbin{\&}|A|$ and
$\Sigma(\Gamma,A)(\langle\gamma,\alpha\rangle)\colonequals\Gamma(\gamma)\mathbin{\&}A^{\star}(\gamma^{\dagger})(\alpha)$
for all $\langle\gamma,\alpha\rangle:|\Sigma(\Gamma,A)|$. We write
$\Gamma\mathbin{\&}A$ for $\Sigma(\Gamma,A)$ if $A$ is constant.

We are now ready to recall:

######  Theorem 2.31 (a game-semantic CwF [Yam22]).

The category $\mathbb{WPG}_{\oc}$ gives rise to a CwF as follows:

  * •

The terminal p-game $T\in\mathbb{WPG}_{\oc}$ in Example 2.18 forms a terminal
object;

  * •

We define $\mathrm{Ty}(\Gamma)\colonequals\mathscr{D}^{\mathrm{w}}(\Gamma)$
($\Gamma\in\mathbb{WPG}_{\oc}$) and
$\mathrm{Tm}(\Gamma,A)\colonequals\mathbb{WPG}_{\oc}(\Pi(\Gamma,A))$
($A\in\mathscr{D}^{\mathrm{w}}(\Gamma)$);

  * •

Given a morphism $\phi:\Delta\rightarrow\Gamma$, we define
$\\_\\{\phi\\}:\mathrm{Ty}(\Gamma)\to\mathrm{Ty}(\Delta)$ by
$|A\\{\phi\\}|\colonequals|A|$ and
$A\\{\phi\\}(\delta_{0}^{\dagger})\colonequals
A(\phi^{\dagger}\bullet\delta_{0})$ for all $A\in\mathrm{Ty}(\Gamma)$ and
$\delta_{0}^{\dagger}\in\mathbb{WPG}_{\oc}(\oc\Delta)$, and define
$\\_\\{\phi\\}_{A}:\mathrm{Tm}(\Gamma,A)\to\mathrm{Tm}(\Delta,A\\{\phi\\})$ by
$\alpha\\{\phi\\}_{A}\colonequals\alpha\bullet\phi$ for all
$\alpha\in\mathrm{Tm}(\Gamma,A)$;

  * •

We define $\Gamma.A\colonequals\Sigma(\Gamma,A)$,
$\mathrm{p}_{A}\colonequals\mathrm{der}_{|\Gamma|}:\Sigma(\Gamma,A)\rightarrow\Gamma$,
$\mathrm{v}_{A}\colonequals\mathrm{der}_{|A|}:\Pi(\Sigma(\Gamma,A),A\\{\mathrm{p}_{A}\\})$
and
$\langle\phi,\check{\alpha}\rangle_{A}\colonequals\langle\phi,\check{\alpha}\rangle:\Delta\rightarrow\Sigma(\Gamma,A)$
($\check{\alpha}\in\mathrm{Tm}(\Delta,A\\{\phi\\})$).

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

Strictly speaking, a CwF only interprets the core part of MLTT common to all
types. For interpreting One-, Zero-, N-, Pi-, Sigma- and Id-types, we need to
equip the CwF $\mathbb{WPG}_{\oc}$ with _semantic type formers_ [Hof97] that
interpret these types. In the following, we only sketch the game-semantic type
formers on the CwF $\mathbb{WPG}_{\oc}$, leaving the general definition of
semantic type formers to Hofmann [Hof97]. Let us fix an objects
$\Delta,\Gamma\in\mathbb{WPG}_{\oc}$ and types
$A\in\mathscr{D}^{\mathrm{w}}(\Gamma)$ and
$B\in\mathscr{D}^{\mathrm{w}}(\Sigma(\Gamma,A))$.

######  Theorem 2.32 (game semantics of Pi-types [Yam22]).

$\mathbb{WPG}_{\oc}$ strictly supports Pi-types, where

  * •

($\Pi$-Form) A dependent p-game $\Pi(A,B)\in\mathscr{D}^{\mathrm{w}}(\Gamma)$
is given by $|\Pi(A,B)|\colonequals|A|\Rightarrow|B|$ and
$\Pi(A,B)(\gamma_{0}^{\dagger})\colonequals\Pi(A(\gamma_{0}^{\dagger}),B_{\gamma_{0}^{\dagger}})$
for each $\gamma_{0}^{\dagger}\in\mathbb{WPG}_{\oc}(\oc\Gamma)$, and another
dependent p-game
$B_{\gamma_{0}^{\dagger}}\in\mathscr{D}^{\mathrm{w}}(A(\gamma_{0}^{\dagger}))$
by $|B_{\gamma_{0}^{\dagger}}|\colonequals|B|$ and
$B_{\gamma_{0}^{\dagger}}(\alpha_{0}^{\dagger})\colonequals
B(\langle\gamma_{0},\alpha_{0}\rangle^{\dagger})$ for each
$\alpha_{0}^{\dagger}\in\mathbb{WPG}_{\oc}(\oc A(\gamma_{0}^{\dagger}))$. We
write $A\Rightarrow B$ for $\Pi(A,B)$ if $B_{\gamma_{0}^{\dagger}}$ is
constant for each $\gamma_{0}^{\dagger}\in\mathbb{WPG}_{\oc}(\oc\Gamma)$. Note
that the equation

$\Pi(A,B)\\{\phi\\}=\Pi(A\\{\phi\\},B\\{\phi_{A}^{+}\\})$ (4)

holds for each morphism $\phi:\Delta\rightarrow\Gamma$ ($\Pi$-Subst), where
$\phi_{A}^{+}\colonequals\langle\phi\bullet\mathrm{p},\mathrm{v}\rangle:\Delta.A\\{\phi\\}\rightarrow\Gamma.A$.

  * •

($\Pi$-Intro) Given a term $\beta\in\mathbb{WPG}_{\oc}(\Sigma(\Gamma,A),B)$,
another term $\lambda_{A,B}(\beta)\in\mathbb{WPG}_{\oc}(\Gamma,\Pi(A,B))$ is
obtained from $\beta$ by adjusting tags or _currying_ $\beta$ with respect to
the adjunction between tensor $\otimes$ and linear implication $\multimap$
[McC98] (thanks to the evident isomorphism
$|\oc\Sigma(\Gamma,A)|=\oc(|\Gamma|\mathbin{\&}|A|)\cong\oc|\Gamma|\otimes\oc|A|$).
We often omit the subscripts $(\\_)_{A,B}$ on $\lambda_{A,B}$ and the inverse
$\lambda_{A,B}^{-1}$.

  * •

($\Pi$-Elim) We define
$\mathrm{App}_{A,B}(\kappa,\alpha)\colonequals\lambda_{A,B}^{-1}(\kappa)\\{\overline{\alpha}\\}\in\mathbb{WPG}_{\oc}(\Gamma,B\\{\overline{\alpha}\\})$
for all $\kappa\in\mathbb{WPG}_{\oc}(\Gamma,\Pi(A,B))$ and
$\alpha\in\mathbb{WPG}_{\oc}(\Gamma,A)$. We often omit the subscripts
$(\\_)_{A,B}$ on $\mathrm{App}_{A,B}$.

######  Theorem 2.33 (game semantics of Sigma-types [Yam22]).

$\mathbb{WPG}_{\oc}$ strictly supports Sigma-types, where

  * •

($\Sigma$-Form) Similarly to Pi-types, we define
$\Sigma(A,B)\colonequals(|A|\mathbin{\&}|B|,(\Sigma(A(\gamma_{0}^{\dagger}),B_{\gamma_{0}^{\dagger}}))_{\gamma_{0}^{\dagger}\in\mathbb{WPG}_{\oc}(\oc\Gamma)})$.
We write $A\mathbin{\&}B$ for $\Sigma(A,B)$ if $B_{\gamma_{0}^{\dagger}}$ is
constant for each $\gamma_{0}^{\dagger}\in\mathbb{WPG}_{\oc}(\oc\Gamma)$.

  * •

($\Sigma$-Intro) By the evident bijection
$\Sigma(\Sigma(\Gamma,A),B)\cong\Sigma(\Gamma,\Sigma(A,B))$, we define a
morphism
$\mathrm{Pair}_{A,B}\colonequals\langle\mathrm{p}_{A}\bullet\mathrm{p}_{B},\langle\mathrm{v}_{A}\\{\mathrm{p}_{B}\\},\mathrm{v}_{B}\rangle\rangle:\Sigma(\Sigma(\Gamma,A),B)\stackrel{{\scriptstyle\sim}}{{\rightarrow}}\Sigma(\Gamma,\Sigma(A,B))$.

  * •

($\Sigma$-Elim) Given a term
$\rho\in\mathbb{WPG}_{\oc}(\Sigma(\Sigma(\Gamma,A),B),P\\{\mathrm{Pair}_{A,B}\\})$,
we define another term
$\mathcal{R}^{\Sigma}_{A,B,P}(\rho)\colonequals\rho\\{\mathrm{Pair}_{A,B}^{-1}\\}\in\mathbb{WPG}_{\oc}(\Sigma(\Gamma,\Sigma(A,B)),P\\{\mathrm{Pair}_{A,B}\\}\\{\mathrm{Pair}_{A,B}^{-1}\\})=\mathbb{WPG}_{\oc}(\Sigma(\Gamma,\Sigma(A,B)),P)$.

######  Theorem 2.34 (game semantics of atomic types [Yam22]).

$\mathbb{WPG}_{\oc}$ supports One-, Zero- and N-types, where their formation
rules are given by constant dependent p-gams at the terminal p-game $T$, the
empty p-game $0$ and the natural number p-game $N$, for which we write $1$,
$0$ and $N$, respectively

######  Theorem 2.35 (game semantics of Id-types [Yam22]).

$\mathbb{WPG}_{\oc}$ supports Id-types, where

  * •

(Id-Form) Let $T^{\prime}\colonequals\mathrm{flat}(\\{\mathbin{\surd}\\})$
(Example 2.7), where $\mathbin{\surd}$ is any element. We define a dependent
p-game
$\mathrm{Id}_{A}\in\mathscr{D}^{\mathrm{w}}(\Sigma(\Sigma(\Gamma,A),A^{+}))$
by $|\mathrm{Id}_{A}|\colonequals T^{\prime}$ and
$\mathrm{Id}_{A}(\langle\langle\gamma_{0},\alpha_{0}\rangle,\alpha_{0}^{\prime}\rangle^{\dagger})\colonequals\begin{cases}(T^{\prime},\kappa_{T^{\prime}})&\text{if
$\alpha_{0}=\alpha_{0}^{\prime}$;}\\\
(T^{\prime},\kappa_{0})&\text{otherwise,}\end{cases}$ for all
$\langle\langle\gamma_{0},\alpha_{0}\rangle,\alpha_{0}^{\prime}\rangle^{\dagger}\in\mathbb{WPG}_{\oc}(\oc\Sigma(\Sigma(\Gamma,A),A^{+}))$,
where $\kappa_{X}$ is the constant family at a game $X$.

  * •

(Id-Intro) Let
$\mathrm{Refl}_{A}\colonequals\langle\overline{\mathrm{v}_{A}},\mathrm{refl}_{A}\rangle\in\mathbb{WPG}_{\oc}(\Sigma(\Gamma,A),\Sigma(\Sigma(\Sigma(\Gamma,A),A^{+}),\mathrm{Id}_{A}))$,
where
$\mathrm{refl}_{A}\in\mathbb{WPG}_{\oc}(\Sigma(\Gamma,A),\mathrm{Id}_{A}\\{\overline{\mathrm{v}_{A}}\\})$
is $\underline{\surd}:T^{\prime}$ (Example 2.7) up to tags.

######  Example 2.36.

Consider the interpretation of the Id-type $\mathsf{f:N\Rightarrow
N,g:N\Rightarrow N\vdash Id_{N\Rightarrow N}(f,g)\ type}$ in the CwF
$\mathbb{WPG}_{\oc}$ [Yam22], which is the p-game $\Pi((N\Rightarrow
N)\mathbin{\&}(N\Rightarrow N),\mathrm{Id}_{N\Rightarrow
N}(\pi_{1},\pi_{2}))$. The component of the codomain
$\mathrm{Id}_{N\Rightarrow N}(\pi_{1},\pi_{2})$ is in general not decidable
because any play in this p-game can observe only _finite_ information about
two input strategies on the domain. Nevertheless, this is not a problem
because the codomain component of each pi (Definition 2.29) is specified _only
gradually_ (and often incompletely) along the gradual (and often incomplete)
disclosure of input strategies on the domain by Opponent.

Accordingly, assuming a p-game $\mathcal{U}$ for the universe, a strategy
$\mathrm{En}(\mathrm{Id}_{N\Rightarrow N}(\pi_{1},\pi_{2})):(N\Rightarrow
N)\mathbin{\&}(N\Rightarrow N)\rightarrow\mathcal{U}$ that encodes the p-game
$\Pi((N\Rightarrow N)\mathbin{\&}(N\Rightarrow N),\mathrm{Id}_{N\Rightarrow
N}(\pi_{1},\pi_{2}))$, if any, only has to encode the currently possible
components of the codomain $\mathrm{Id}_{N\Rightarrow N}(\pi_{1},\pi_{2})$ at
each moment; it does not have to decide if the two input strategies on the
domain are equal. We emphasise that this _intensionality_ is highly
nontrivial, and it distinguishes game semantics from other semantics of MLTT
such as domains and realisability [Pal93, Str12, BL18]. Moreover, this
observation is the starting point of our solution to the main problem (§3) in
achieving game semantics of the universe sketched in §1.6.

##  3 Game semantics of universes

This section presents our main contribution: game semantics of the cumulative
hierarchy of universes.

To this end, we first recall the semantic type former for the cumulative
hierarchy of universes:

######  Definition 3.1 (categorical semantics of universes [Hof97]).

A CwF $\mathcal{C}$ _supports universes_ if

  * •

(U-Form) Given an object $\Gamma\in\mathcal{C}$, there is a type
$\mathcal{U}_{k}^{[\Gamma]}\in\mathrm{Ty}(\Gamma)$ for each natural number
$k\in\mathbb{N}$, called the _$(k+1)$ st universe_ in the context $\Gamma$,
where we often omit the superscript $(\\_)^{[\Gamma]}$ (when the object
$\Gamma$ is obvious) and/or the subscript $(\\_)_{k}$ (when the index $k$ is
unimportant);

  * •

(U-Intro) Given a type $A\in\mathrm{Ty}(\Gamma)$, there is a term
$\mathrm{En}_{k}(A)\in\mathrm{Tm}(\Gamma,\mathcal{U}_{k})$ for some
$k\in\mathbb{N}$, subsuming
$\mathrm{En}_{k}(\mathcal{U}_{k}^{[\Gamma]})\in\mathrm{Tm}(\Gamma,\mathcal{U}^{[\Gamma]}_{k+1})$
for each $k\in\mathbb{N}$, where we often omit the subscript $(\\_)_{k}$ on
$\mathrm{En}$;

  * •

(U-Elim) Each term $\psi\in\mathrm{Tm}(\Gamma,\mathcal{U}_{k})$ induces a type
$\mathrm{El}_{k}(\psi)\in\mathrm{Ty}(\Gamma)$, where we often omit the
subscript $(\\_)_{k}$ on $\mathrm{El}$;

  * •

(U-Comp) $\mathrm{El}(\mathrm{En}(A))=A$;

  * •

(U-Cumul) If $\psi\in\mathrm{Tm}(\Gamma,\mathcal{U}_{k})$, then
$\psi\in\mathrm{Tm}(\Gamma,\mathcal{U}_{k+1})$;

  * •

(U-Subst)
$\mathcal{U}_{k}^{[\Gamma]}\\{\phi\\}=\mathcal{U}_{k}^{[\Delta]}\in\mathrm{Ty}(\Delta)$
for each morphism $\phi:\Delta\to\Gamma$;

  * •

($\mathrm{En}$-Subst)
$\mathrm{En}(A)\\{\phi\\}=\mathrm{En}(A\\{\phi\\})\in\mathrm{Tm}(\Delta,\mathcal{U})$.

The axiom U-Cumul requires the hierarchy $(\mathcal{U}_{k})_{k\in\mathbb{N}}$
of universes $\mathcal{U}_{k}$ to be _cumulative_. For achieving game
semantics of the cumulative hierarchy of universes, it suffices to equip our
game-semantic CwF $\mathbb{WPG}_{\oc}$ with this semantic type former because
then the semantic type former will automatically induce game semantics of the
cumulative hierarchy of universes as described in Hofmann [Hof97].

###  3.1 Universe predicate games

For convenience, we employ the following reformulation
$\mathrm{Id}^{\prime}(\alpha,\alpha^{\prime})$ of Id-types that satisfy the
axiom Id’-Subst corresponding to Id-Subst. In fact, the type
$\mathrm{Id}_{A}\in\mathrm{Ty}(\Gamma.A.A^{+})$ is equivalent to the family
$(\mathrm{Id}^{\prime}_{A}(\alpha,\alpha^{\prime}))_{\alpha,\alpha^{\prime}\in\mathrm{Tm}(\Gamma,A)}$
of types
$\mathrm{Id}^{\prime}_{A}(\alpha,\alpha^{\prime})\in\mathrm{Ty}(\Gamma)$: The
former is recovered from the latter by

$\mathrm{Id}_{A}\colonequals\mathrm{Id}^{\prime}_{A}(\mathrm{v}\\{\mathrm{p}\\},\mathrm{v}),$

and the latter from the former by

$\mathrm{Id}^{\prime}_{A}(\alpha,\alpha^{\prime})\colonequals\mathrm{Id}_{A}\\{\langle\langle\mathrm{id}_{\Gamma},\alpha\rangle,\alpha^{\prime}\rangle\\}.$

We also note that the axiom Id-Subst implies the equation

$\displaystyle\mathrm{Id}^{\prime}_{A}(\alpha,\alpha^{\prime})\\{\phi\\}$
$\displaystyle=\mathrm{Id}_{A}\\{\langle\langle\mathrm{id}_{\Gamma},\alpha\rangle,\alpha^{\prime}\rangle\\}\\{\phi\\}$
$\displaystyle=\mathrm{Id}_{A}\\{\langle\langle\phi,\alpha\\{\phi\\}\rangle,\alpha^{\prime}\\{\phi\\}\rangle\\}$
$\displaystyle=\mathrm{Id}_{A}\\{\langle\langle\phi\circ\mathrm{p},\mathrm{v}\rangle\circ\mathrm{p},\mathrm{v}\rangle\\}\\{\langle\langle\mathrm{id}_{\Gamma},\alpha\\{\phi\\}\rangle,\alpha^{\prime}\\{\phi\\}\rangle\\}$
$\displaystyle=\mathrm{Id}_{A}\\{\phi_{A,A^{+}}^{++}\\}\\{\langle\langle\mathrm{id}_{\Gamma},\alpha\\{\phi\\}\rangle,\alpha^{\prime}\\{\phi\\}\rangle\\}$
$\displaystyle=\mathrm{Id}_{A\\{\phi\\}}\\{\langle\langle\mathrm{id}_{\Gamma},\alpha\\{\phi\\}\rangle,\alpha^{\prime}\\{\phi\\}\rangle\\}\quad\text{(by
{Id-Subst})}$
$\displaystyle=\mathrm{Id}^{\prime}_{A\\{\phi\\}}(\alpha\\{\phi\\},\alpha^{\prime}\\{\phi\\})$

for each terms $\alpha,\alpha^{\prime}\in\mathrm{Tm}(\Gamma,A)$ and morphism
$\phi:\Delta\rightarrow\Gamma$, which we call the axiom Id’-Subst. Conversely,
the axiom Id’-Subst implies the axiom Id-Subst because

$\displaystyle\mathrm{Id}_{A}\\{\phi_{A,A^{+}}^{++}\\}$
$\displaystyle=\mathrm{Id}^{\prime}_{A}(\mathrm{v}\\{\mathrm{p}\\},\mathrm{v})\\{\langle\phi_{A}^{+}\circ\mathrm{p},\mathrm{v}\rangle\\}$
$\displaystyle=\mathrm{Id}^{\prime}_{A\\{\phi\\}}(\mathrm{v}\\{\mathrm{p}\\}\\{\langle\phi_{A}^{+}\circ\mathrm{p},\mathrm{v}\rangle\\},\mathrm{v}\\{\langle\phi_{A}^{+}\circ\mathrm{p},\mathrm{v}\rangle\\})\quad\text{(by
{Id'-Subst})}$
$\displaystyle=\mathrm{Id}^{\prime}_{A\\{\phi\\}}(\mathrm{v}\\{\langle\phi\circ\mathrm{p}\circ\mathrm{p},\mathrm{v}\\{\mathrm{p}\\}\rangle\\},\mathrm{v})$
$\displaystyle=\mathrm{Id}^{\prime}_{A\\{\phi\\}}(\mathrm{v}\\{\mathrm{p}\\},\mathrm{v})$
$\displaystyle=\mathrm{Id}_{A\\{\phi\\}}.$

This in particular implies the equation

$\mathrm{Id}^{\prime}_{A}(\alpha,\alpha^{\prime})(\gamma_{0}^{\dagger})=\mathrm{Id}^{\prime}_{A(\gamma_{0}^{\dagger})}(\alpha\bullet\gamma_{0},\alpha^{\prime}\bullet\gamma_{0})$
(5)

for all $\gamma_{0}^{\dagger}\in\mathbb{WPG}_{\oc}$. We leave it to the reader
to reformulate the other axioms on Id-types in such a way that they correspond
to this reformulation. From now on, we simply write
$\mathrm{Id}(\alpha,\alpha^{\prime})$ for
$\mathrm{Id}^{\prime}(\alpha,\alpha^{\prime})$.

Then, as sketched in §1.6, the main idea for the construction of our game-
semantic type former for the cumulative hierarchy of universes is centred
around the following _universe p-games_ :

######  Definition 3.2 (universe p-games).

Let us fix an injection
$\sharp_{0}:\\{1,0,N,\Pi,\Sigma,\mathrm{Id}\\}\rightarrowtail\mathbb{N}$. For
each natural number $k\in\mathbb{N}$, the _$(k+1)$ st universe predicate (p-)
game_ is the constant p-game $\mathcal{U}_{k}$ on the game
$|\mathcal{U}_{k}|\colonequals\bigcup_{i\in\mathbb{N}}|\mathcal{U}_{k}^{(i)}|$
together with an arbitrarily fixed injection
$\sharp_{k}:\\{\,1,0,N,\Pi,\Sigma,\mathrm{Id}\,\\}\uplus\\{\,\mathcal{U}_{j}\mid
j<k\,\\}\rightarrowtail\mathbb{N}$ that conservatively extends $\sharp_{k-1}$,
where $\mathcal{U}_{k}^{(i)}$ is a p-game inductively defined as follows:

  1. 1.

(Base case) We define the p-game

$\mathcal{U}_{k}^{(0)}\colonequals\mathscr{P}(\mathrm{Pref}(\\{\,q^{\mathrm{OQ}}.\sharp_{k}(X)^{\mathrm{PA}}\mid
X\in\\{1,0,N,\mathcal{U}_{j}\\},j<k\,\\})),$

where $q^{\mathrm{OQ}}$ justifies $\sharp_{k}(X)^{\mathrm{PA}}$, together with
a function

$\displaystyle\mathrm{El}^{(0)}_{k}:\mathbb{WPG}_{\oc}(\oc\mathcal{U}_{k}^{(0)})$
$\displaystyle\rightarrow\mathrm{ob}(\mathbb{WPG}_{\oc})$
$\displaystyle\underline{\sharp_{k}(X)}^{\dagger}$ $\displaystyle\mapsto X.$

Abusing notation, we lift this function to a dependent p-game
$\mathrm{El}^{(0)}_{k}\in\mathscr{D}(\mathcal{U}_{k}^{(0)})$ by —El^(0)_k—
⋃_♯_k(X)^†∈WPG_(U_k^(0)) El^(0)_k(♯_k(X)^†) ∥El^(0)_k∥ :
♯_k(X)^†↦El^(0)_k(♯_k(X)^†), where recall Example 2.9 for the notation
$\underline{\sharp_{k}(X)}$. We also write $\mathcal{U}_{k}^{(0)}$ for the
constant p-game $\\{\mathcal{U}_{k}^{(0)}\\}$.

Moreover, for each object $\Gamma\in\mathbb{WPG}_{\oc}$, we further lift this
dependent p-game to a function

$\displaystyle\mathrm{El}^{(0)}_{k,\Gamma}:\mathbb{WPG}_{\oc}(\Gamma,\mathcal{U}_{k}^{(0)})$
$\displaystyle\rightarrow\mathscr{D}(\Gamma)$ $\displaystyle\psi$
$\displaystyle\mapsto\mathrm{El}^{(0)}_{k,\Gamma}(\psi),$

where the dependent p-game
$\mathrm{El}^{(0)}_{k,\Gamma}(\psi)\in\mathscr{D}(\Gamma)$ is given by
—El^(0)_k, Γ(ψ)— ⋃_γ_0^†∈WPG_(Γ) El^(0)_k(ψ∙γ_0) ∥El^(0)_k, Γ(ψ)∥ :
γ_0^†↦El^(0)_k(ψ∙γ_0). This function $\mathrm{El}^{(0)}_{k,\Gamma}$
generalises the dependent p-game $\mathrm{El}^{(0)}_{k}$ due to the evident
isomorphism $\mathrm{El}^{(0)}_{k,T}\cong\mathrm{El}^{(0)}_{k}$. We usually
omit the subscript $(\\_)_{\Gamma}$ on the function
$\mathrm{El}^{(0)}_{k,\Gamma}$ when it does not bring confusion.

  2. 2.

(Inductive step) We define the p-game

$\displaystyle\mathcal{U}_{k}^{(i+1)}\colonequals\mathscr{P}(\mathcal{U}_{k}^{(i)}$
$\displaystyle\cup\mathrm{Pref}(\\{\,q^{\mathrm{OQ}}.\sharp_{k}(Y)^{\mathrm{PA}}.\bm{s}\mid
Y\in\\{\Pi,\Sigma\\},\bm{s}\in\Sigma(\mathcal{U}_{k}^{(i)},\mathrm{El}^{(i)}_{k}\Rightarrow\mathcal{U}_{k}^{(i)})\,\\})$
$\displaystyle\cup\mathrm{Pref}(\\{\,q^{\mathrm{OQ}}.\sharp_{k}(\mathrm{Id})^{\mathrm{PA}}.\bm{t}\mid\bm{t}\in\Sigma(\mathcal{U}_{k}^{(i)},\mathrm{El}^{(i)}_{k}\mathbin{\&}\mathrm{El}^{(i)}_{k})\,\\})),$

where $q^{\mathrm{OQ}}$ justifies both $\sharp(Y)^{\mathrm{PA}}$ and
$\sharp(\mathrm{Id})^{\mathrm{PA}}$, and in turn the latter two moves justify
the initial moves in $\bm{s}$ and $\bm{t}$, respectively, together with a
function

$\displaystyle\mathrm{El}^{(i+1)}_{k}:\mathbb{WPG}_{\oc}(\oc\mathcal{U}_{k}^{(i+1)})$
$\displaystyle\rightarrow\mathrm{ob}(\mathbb{WPG}_{\oc})$
$\displaystyle\underline{\sharp_{k}(X)}^{\dagger}$ $\displaystyle\mapsto X$
$\displaystyle q.\sharp_{k}(Y).\langle\mu,\psi\rangle^{\dagger}$
$\displaystyle\mapsto
Y(\mathrm{El}^{(i)}_{k}(\mu),\mathrm{El}^{(i)}_{k}(\psi))$ $\displaystyle
q.\sharp_{k}(\mathrm{Id}).\langle\mu,\langle\alpha,\alpha^{\prime}\rangle\rangle^{\dagger}$
$\displaystyle\mapsto\mathrm{Id}_{\mathrm{El}^{(i)}_{k}(\mu)}(\mathrm{El}^{(i)}_{k}(\alpha),\mathrm{El}^{(i)}_{k}(\alpha^{\prime})),$

where
$q.a.\sigma\colonequals\mathrm{Pref}(\\{\,q^{\mathrm{OQ}}a^{\mathrm{PA}}\bm{v}\mid\bm{v}\in\sigma\,\\})^{\mathrm{Even}}$
for each question $q^{\mathrm{OQ}}$, answer $a^{\mathrm{PA}}$ and strategy
$\sigma$, and $q^{\mathrm{OQ}}$ justifies $a^{\mathrm{PA}}$, and
$a^{\mathrm{PA}}$ justifies initial moves occurring in $\bm{v}$.

Again, we lift this function $\mathrm{El}^{(i+1)}_{k}$ to a dependent p-game
$\mathrm{El}^{(i+1)}_{k}\in\mathscr{D}(\mathcal{U}_{k}^{(i+1)})$ and further
to a function
$\mathbb{WPG}_{\oc}(\Gamma,\mathcal{U}_{k}^{(i+1)})\rightarrow\mathscr{D}(\Gamma)$
for each $\Gamma\in\mathbb{WPG}_{\oc}$ in the same way as the case of
$\mathrm{El}^{(0)}_{k}$. We also write $\mathcal{U}_{k}^{(i+1)}$ for the
constant p-game $\\{\mathcal{U}_{k}^{(i+1)}\\}$ and apply the notations for
$\mathrm{El}^{(0)}_{k}$ to $\mathrm{El}^{(i+1)}_{k}$.

Given an object $\Gamma\in\mathbb{WPG}_{\oc}$, we write
$\mathcal{U}_{k}^{[\Gamma]}\in\mathscr{D}(\Gamma)$ for the constant dependent
p-game at $\mathcal{U}_{k}$ and we often omit the superscript
$(\\_)^{[\Gamma]}$ on $\mathcal{U}_{k}^{[\Gamma]}$ when it does not bring
confusion.

We finally define the injection

$\sharp\colonequals\bigcup_{k\in\mathbb{N}}\sharp_{k}:\\{\,1,0,N,\Pi,\Sigma,\mathrm{Id}\,\\}\uplus\\{\,\mathcal{U}_{j}\mid
j\in\mathbb{N}\,\\}\rightarrowtail\mathbb{N}.$

Let us emphasise that the inductive step in Definition 3.2 properly implements
our idea on how to encode game semantics of Pi-, Sigma- and Id-types by
strategies on games (§1.6) by nontrivial recursion. Specifically, our key
technique is to define each universe p-game $\mathcal{U}_{k}$ inductively in
terms of the games $\mathcal{U}_{k}^{(i)}$ ($i\in\mathbb{N}$) along with the
construction of the function $\mathrm{El}_{k}^{(i)}$. This is the highlight of
the present work.

###  3.2 Computational game semantics of the cumulative hierarchy of universes

We need one more preparation for our game semantics of universes as follows.
The axiom U-Intro (Definition 3.1) requires that every type $A$ has its
encoding $\mathrm{El}(A)$. As already indicated in §1.6, however, we define
the encoding function $\mathrm{En}$ inductively along the construction of
types. Accordingly, we have to restrict types in the CwF $\mathbb{WPG}_{\oc}$
to those freely generated by the type constructions, leading to:

######  Definition 3.3 (a subCwF $\mathbb{UPG}_{\oc}$).

Let $\mathbb{UPG}_{\oc}\hookrightarrow\mathbb{WPG}_{\oc}$ be the substructural
CwF of $\mathbb{WPG}_{\oc}$ such that

  * •

The underlying category $\mathbb{UPG}_{\oc}$ is the category
$\mathbb{WPG}_{\oc}$;

  * •

The types of $\mathbb{UPG}_{\oc}$ are inductively constructed from the atomic
dependent p-games $1$, $0$, $N$ and $\mathcal{U}_{k}$ for all $k\in\mathbb{N}$
by the constructions $\Pi$, $\Sigma$ and $\mathrm{Id}$;

  * •

The terms of $\mathbb{UPG}_{\oc}$ are given by
$\mathrm{Tm}_{\mathbb{UPG}_{\oc}}(\Gamma,A)\colonequals\mathrm{Tm}_{\mathbb{WPG}_{\oc}}(\Gamma,A)$
for all $\Gamma\in\mathbb{UPG}_{\oc}$ and
$A\in\mathrm{Ty}_{\mathbb{UPG}_{\oc}}(\Gamma)$.

######  Corollary 3.4 (well-defined $\mathbb{UPG}_{\oc}$).

The structure $\mathbb{UPG}_{\oc}$ forms a well-defined CwF that supports
One-, Zero-, N-, Pi-, Sigma- and Id-types in the same way as the CwF
$\mathbb{WPG}_{\oc}$.

###### Proof.

This corollary immediately follows from Theorem 2.31 (where the only
nontrivial point is the closure of types $\mathbb{UPG}_{\oc}$ under
substitution, but it is easily shown by induction on the types). ∎

In addition, this CwF $\mathbb{UPG}_{\oc}$ also supports the cumulative
hierarchy of universes:

######  Theorem 3.5 (game semantics of universes).

The CwF $\mathbb{UPG}_{\oc}$ supports universes.

###### Proof.

Let $\Delta,\Gamma\in\mathbb{UPG}_{\oc}$,
$A\in\mathrm{Ty}_{\mathbb{UPG}_{\oc}}(\Gamma)$ and
$\phi\in\mathbb{UPG}_{\oc}(\Delta,\Gamma)$.

  * •

(U-Form) We have $\mathcal{U}_{k}^{[\Gamma]}\in\mathscr{D}(\Gamma)$ for each
natural number $k\in\mathbb{N}$ (Definition 3.2).

  * •

(U-Intro) Because $A$ is constructed inductively, we can define a term
$\mathrm{En}(A)\in\mathrm{Tm}_{\mathbb{UPG}_{\oc}}(\Gamma,\mathcal{U}_{k(A)})$
for some natural number $k(A)\in\mathbb{N}$ inductively along the construction
of $A$ as follows:

    1. 1.

If $A$ is $1$, $0$ or $N$, then

$\mathrm{En}(A)\colonequals\underline{A}\in\mathrm{Tm}_{\mathbb{UPG}_{\oc}}(\Gamma,\mathcal{U}_{0});$

    2. 2.

If $A$ is $\mathcal{U}_{i}$ for some natural number $i\in\mathbb{N}$, then

$\mathrm{En}(\mathcal{U}_{i})\colonequals\underline{\mathcal{U}_{i}}\in\mathrm{Tm}_{\mathbb{UPG}_{\oc}}(\Gamma,\mathcal{U}_{i+1});$

    3. 3.

If $A$ is $Y(B,C)$, where $Y$ is $\Pi$ or $\Sigma$, then

$\mathrm{En}(Y(B,C))\colonequals
q^{\mathrm{OQ}}.\sharp(Y)^{\mathrm{PA}}.\langle\mathrm{En}(B),\lambda\circ\mathrm{En}(C)\rangle\in\mathrm{Tm}_{\mathbb{UPG}_{\oc}}(\Gamma,\mathcal{U}_{\max(k(B),k(C))});$

    4. 4.

If $A$ is $\mathrm{Id}_{D}(\delta,\delta^{\prime})$, then

$\mathrm{En}(\mathrm{Id}_{D}(\delta,\delta^{\prime}))\colonequals
q^{\mathrm{OQ}}.\sharp(\mathrm{Id})^{\mathrm{PA}}.\langle\mathrm{En}(D),\langle\delta,\delta^{\prime}\rangle\rangle\in\mathrm{Tm}_{\mathbb{UPG}_{\oc}}(\Gamma,\mathcal{U}_{k(D)}).$

  * •

(U-Elim) We define the function
$\mathrm{El}_{k}:\mathrm{Tm}_{\mathbb{UPG}_{\oc}}(\Gamma,\mathcal{U}_{k}^{[\Gamma]})\cong\mathbb{WPG}_{\oc}(\Gamma,\mathcal{U}_{k})\rightarrow\mathscr{D}(\Gamma)$
to be the union

$\mathrm{El}_{k}\colonequals\big{(}\bigcup_{i\in\mathbb{N}}\mathrm{El}_{k}^{(i)}\big{)}:\mathbb{WPG}_{\oc}(\Gamma,\mathcal{U}_{k})\rightarrow\mathscr{D}(\Gamma)$

up to the isomorphism
$\mathrm{Tm}_{\mathbb{UPG}_{\oc}}(\Gamma,\mathcal{U}_{k}^{[\Gamma]})\cong\mathbb{WPG}_{\oc}(\Gamma,\mathcal{U}_{k})$,
where the function
$\mathrm{El}_{k}^{(i)}:\mathbb{WPG}_{\oc}(\Gamma,\mathcal{U}_{k}^{(i)})\rightarrow\mathscr{D}(\Gamma)$
is given in Definition 3.2. Note that
$\mathrm{El}^{(0)}_{k,\Gamma}(\psi)\in\mathscr{D}(\Gamma)$ for each
$\psi\in\mathrm{Tm}_{\mathbb{UPG}_{\oc}}(\Gamma,\mathcal{U}_{k}^{[\Gamma]})$
is given by —El_k(ψ)— ⋃_γ_0^†∈WPG_(Γ) El_k(ψ∙γ_0) ∥El_k(ψ)∥ :
γ_0^†↦El_k(ψ∙γ_0).

  * •

(U-Comp) We see that the equation $\mathrm{El}(\mathrm{En}(A))=A$ holds by
induction on $A$, where we focus on the cases of $A=\Pi(B,C)$ and
$A=\mathrm{Id}_{D}(\delta,\delta^{\prime})$ since the other cases are similar
or trivial.

    1. 1.

Assume $A=\Pi(B,C)$. The dependent p-game

$\displaystyle\mathrm{El}\circ\mathrm{En}(\Pi(B,C))$
$\displaystyle=\mathrm{El}(q.\sharp(\Pi).\langle\mathrm{En}(B),\lambda\circ\mathrm{En}(C)\rangle)$

consists of the underlying p-game

$\displaystyle|\mathrm{El}\circ\mathrm{En}(\Pi(B,C))|$
$\displaystyle=|\mathrm{El}(q.\sharp(\Pi).\langle\mathrm{En}(B),\lambda\circ\mathrm{En}(C)\rangle)|$
$\displaystyle=\bigcup_{\gamma_{0}^{\dagger}\in\mathbb{UPG}_{\oc}(\oc\Gamma)}|\Pi(\mathrm{El}(\mathrm{En}(B)\bullet\gamma_{0}),\mathrm{El}(\lambda\circ\mathrm{En}(C)\bullet\gamma_{0}))|$
$\displaystyle=\bigcup_{\gamma_{0}^{\dagger}\in\mathbb{UPG}_{\oc}(\oc\Gamma)}(|\mathrm{El}(\mathrm{En}(B)\bullet\gamma_{0})|\Rightarrow|\mathrm{El}(\lambda\circ\mathrm{En}(C)\bullet\gamma_{0})|)$
$\displaystyle=\bigcup_{\gamma_{0}^{\dagger}\in\mathbb{UPG}_{\oc}(\oc\Gamma)}|\mathrm{El}(\mathrm{En}(B)\bullet\gamma_{0})|\Rightarrow\bigcup_{\gamma_{0}^{\dagger}\in\mathbb{UPG}_{\oc}(\oc\Gamma)}|\mathrm{El}(\lambda\circ\mathrm{En}(C)\bullet\gamma_{0})|$
$\displaystyle=|\mathrm{El}\circ\mathrm{En}(B)|\Rightarrow|\mathrm{El}\circ\mathrm{En}(C)|$
$\displaystyle=|B|\Rightarrow|C|\quad\text{(by the induction hypothesis)}$
$\displaystyle=|\Pi(B,C)|$

and the function

$\displaystyle\|\mathrm{El}\circ\mathrm{En}(\Pi(B,C))\|:\gamma_{0}^{\dagger}\in\mathbb{UPG}_{\oc}(\oc\Gamma)$
$\displaystyle\mapsto\mathrm{El}(q.\sharp(\Pi).\langle\mathrm{En}(B)\bullet\gamma_{0},\lambda\circ\mathrm{En}(C)\bullet\gamma_{0}\rangle)$
$\displaystyle=\Pi(\mathrm{El}(\mathrm{En}(B)\bullet\gamma_{0}),\mathrm{El}(\lambda\circ\mathrm{En}(C)\bullet\gamma_{0}))$
$\displaystyle=\Pi(\mathrm{El}\circ\mathrm{En}(B)(\gamma_{0}^{\dagger}),\mathrm{El}\circ\mathrm{En}(C)_{\gamma_{0}^{\dagger}})$
$\displaystyle=\Pi(B(\gamma_{0}^{\dagger}),C_{\gamma_{0}^{\dagger}})\quad\text{(by
the induction hypothesis)}$ $\displaystyle=\Pi(B,C)(\gamma_{0}^{\dagger}).$

Hence, we have shown the equation

$\mathrm{El}\circ\mathrm{En}(\Pi(B,C))=\Pi(B,C).$

    2. 2.

Assume $A=\mathrm{Id}_{D}(\delta,\delta^{\prime})$. The dependent p-game

$\displaystyle\mathrm{El}\circ\mathrm{En}(\mathrm{Id}_{D}(\delta,\delta^{\prime}))$
$\displaystyle=\mathrm{El}(q.\sharp(\mathrm{Id}).\langle\mathrm{En}(D),\langle\delta,\delta^{\prime}\rangle\rangle)$

consists of the underlying p-game

$\displaystyle|\mathrm{El}\circ\mathrm{En}(\mathrm{Id}_{D}(\delta,\delta^{\prime}))|$
$\displaystyle=|\mathrm{El}(q.\sharp(\mathrm{Id}).\langle\mathrm{En}(D),\langle\delta,\delta^{\prime}\rangle\rangle)|$
$\displaystyle=\bigcup_{\gamma_{0}^{\dagger}\in\mathbb{UPG}_{\oc}(\oc\Gamma)}|\mathrm{Id}_{\mathrm{El}(\mathrm{En}(D)\bullet\gamma_{0})}(\delta\bullet\gamma_{0},\delta^{\prime}\bullet\gamma_{0})|$
$\displaystyle=T^{\prime}$
$\displaystyle=|\mathrm{Id}_{D}(\delta,\delta^{\prime})|$

and the function

$\displaystyle\|\mathrm{Id}_{D}(\delta,\delta^{\prime})\|:\gamma_{0}^{\dagger}\in\mathbb{UPG}_{\oc}(\oc\Gamma)$
$\displaystyle\mapsto\mathrm{El}(q.\sharp(\mathrm{Id}).\langle\mathrm{En}(D)\bullet\gamma_{0},\langle\delta\bullet\gamma_{0},\delta^{\prime}\bullet\gamma_{0}\rangle\rangle)$
$\displaystyle=\mathrm{Id}_{\mathrm{El}(\mathrm{En}(D)\bullet\gamma_{0})}(\delta\bullet\gamma_{0},\delta^{\prime}\bullet\gamma_{0})$
$\displaystyle=\mathrm{Id}_{\mathrm{El}\circ\mathrm{En}(D)(\gamma_{0}^{\dagger})}(\delta\bullet\gamma_{0},\delta^{\prime}\bullet\gamma_{0})$
$\displaystyle=\mathrm{Id}_{D(\gamma_{0}^{\dagger})}(\delta\bullet\gamma_{0},\delta^{\prime}\bullet\gamma_{0})\quad\text{(by
the induction hypothesis)}$
$\displaystyle=\mathrm{Id}_{D}(\delta,\delta^{\prime})(\gamma_{0}^{\dagger})\quad\text{(by
the equation \ref{IdSubstBeta})}.$

Hence, we have shown the equation

$\mathrm{El}\circ\mathrm{En}(\mathrm{Id}_{D}(\delta,\delta^{\prime}))=\mathrm{Id}_{D}(\delta,\delta^{\prime}).$

  * •

(U-Cumul) By construction,
$\psi\in\mathrm{Tm}_{\mathbb{UPG}_{\oc}}(\Gamma,\mathcal{U}_{k})$ implies
$\psi\in\mathrm{Tm}_{\mathbb{UPG}_{\oc}}(\Gamma,\mathcal{U}_{k+1})$.

  * •

(U-Subst) By construction, the equation
$\mathcal{U}_{k}^{[\Gamma]}\\{\phi\\}=\mathcal{U}_{k}^{[\Delta]}\in\mathrm{Ty}(\Delta)$
holds.

  * •

($\mathrm{En}$-Subst) We see that the equation
$\mathrm{En}(A)\\{\phi\\}=\mathrm{En}(A\\{\phi\\})\in\mathrm{Tm}(\Delta,\mathcal{U})$
holds by induction on $A$, where again we focus on the cases of $A=\Pi(B,C)$
and $A=\mathrm{Id}_{D}(\delta,\delta^{\prime})$.

    1. 1.

Assume $A=\Pi(B,C)$. We have the equation

$\displaystyle\mathrm{En}(\Pi(B,C))\\{\phi\\}$
$\displaystyle=q.\sharp(\Pi).\langle\mathrm{En}(B)\bullet\phi,\lambda\circ\mathrm{En}(C)\bullet\phi\rangle$
$\displaystyle=q.\sharp(\Pi).\langle\mathrm{En}(B\\{\phi\\}),\lambda\circ\mathrm{En}(C\\{\phi_{B}^{+}\\})\rangle\quad\text{(by
the induction hypothesis)}$
$\displaystyle=\mathrm{En}(\Pi(B\\{\phi\\},C\\{\phi_{B}^{+}\\}))$
$\displaystyle=\mathrm{En}(\Pi(B,C)\\{\phi\\})\quad\text{(by the equation
\ref{PiSubst})}.$

    2. 2.

Assume $A=\mathrm{Id}_{D}(\delta,\delta^{\prime})$. We have the equation

$\displaystyle\mathrm{En}(\mathrm{Id}_{D}(\delta,\delta^{\prime}))\\{\phi\\}$
$\displaystyle=q.\sharp(\mathrm{Id}).\langle\mathrm{En}(D)\bullet\phi,\langle\delta\bullet\phi,\delta^{\prime}\bullet\phi\rangle\rangle$
$\displaystyle=q.\sharp(\mathrm{Id}).\langle\mathrm{En}(D\\{\phi\\}),\langle\delta\\{\phi\\},\delta^{\prime}\\{\phi\\}\rangle\rangle\quad\text{(by
the induction hypothesis)}$
$\displaystyle=\mathrm{En}(\mathrm{Id}_{D\\{\phi\\}}(\delta\\{\phi\\},\delta^{\prime}\\{\phi\\}))$
$\displaystyle=\mathrm{En}(\mathrm{Id}_{D}(\delta,\delta^{\prime})\\{\phi\\})\quad\text{(by
{Id'-Subst})}.$

We have verified all the required axioms, completing the proof. ∎

######  Example 3.6.

Let us consider the interpretation of the encoding

$\mathsf{f:N\Rightarrow N,g:N\Rightarrow N\vdash En_{0}(Id_{N\Rightarrow
N}(f,g)):U_{0}}$

of the Id-type discussed in §1.5. The strategy

$\psi\colonequals\mathrm{En}_{0}(\mathrm{Id}_{N\Rightarrow
N}(\pi_{1},\pi_{2})):(N\Rightarrow N)\mathbin{\&}(N\Rightarrow
N)\rightarrow\mathcal{U}_{0}$

that interprets this encoding of the Id-type plays as in Figure 2.

$(N$ | $\stackrel{{\scriptstyle f}}{{\Rightarrow}}$ | $N)$ | $\&$ | $(N$ | $\stackrel{{\scriptstyle g}}{{\Rightarrow}}$ | $N)$ | $\stackrel{{\scriptstyle\psi}}{{\rightarrow}}$ |  |  |  | $\mathcal{U}$
---|---|---|---|---|---|---|---|---|---|---|---
|  |  |  |  |  |  |  |  |  |  | $q$
|  |  |  |  |  |  |  |  |  |  | $\sharp(\mathrm{Id})$
|  |  |  |  |  |  |  |  | $q$ |  |
|  |  |  |  |  |  |  |  | $\sharp(\Pi)$ |  |
|  |  |  |  |  |  |  | $q$ |  |  |
|  |  |  |  |  |  |  | $\sharp(N)$ |  |  |

$(N$ | $\stackrel{{\scriptstyle f}}{{\Rightarrow}}$ | $N)$ | $\&$ | $(N$ | $\stackrel{{\scriptstyle g}}{{\Rightarrow}}$ | $N)$ | $\stackrel{{\scriptstyle\psi}}{{\rightarrow}}$ |  |  |  | $\mathcal{U}$
---|---|---|---|---|---|---|---|---|---|---|---
|  |  |  |  |  |  |  |  |  |  | $q$
|  |  |  |  |  |  |  |  |  |  | $\sharp(\mathrm{Id})$
|  |  |  |  |  |  |  |  | $q$ |  |
|  |  |  |  |  |  |  |  | $\sharp(\Pi)$ |  |
|  |  |  |  |  |  |  |  |  | $q$ |
|  |  |  |  |  |  |  |  |  | $\sharp(N)$ |

$(N$ | $\stackrel{{\scriptstyle f}}{{\Rightarrow}}$ | $N)$ | $\&$ | $(N$ | $\stackrel{{\scriptstyle g}}{{\Rightarrow}}$ | $N)$ | $\stackrel{{\scriptstyle\psi}}{{\rightarrow}}$ | $\mathcal{U}$ |  |  |
---|---|---|---|---|---|---|---|---|---|---|---
|  |  |  |  |  |  |  | $q$ |  |  |
|  |  |  |  |  |  |  | $\sharp(\mathrm{Id})$ |  |  |
|  |  |  |  |  |  |  |  |  |  | $q$
|  | $q$ |  |  |  |  |  |  |  |  |
$q$ |  |  |  |  |  |  |  |  |  |  |
|  |  |  |  |  |  |  |  | $q$ |  |
|  |  |  |  |  |  |  |  | $n$ |  |
$n$ |  |  |  |  |  |  |  |  |  |  |
|  | $f(n)$ |  |  |  |  |  |  |  |  |
|  |  |  |  |  |  |  |  |  |  | $f(n)$

$(N$ | $\stackrel{{\scriptstyle f}}{{\Rightarrow}}$ | $N)$ | $\&$ | $(N$ | $\stackrel{{\scriptstyle g}}{{\Rightarrow}}$ | $N)$ | $\stackrel{{\scriptstyle\psi}}{{\rightarrow}}$ | $\mathcal{U}$ |  |  |  |  |  |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---
|  |  |  |  |  |  |  | $q$ |  |  |  |  |  |
|  |  |  |  |  |  |  | $\sharp(\mathrm{Id})$ |  |  |  |  |  |
|  |  |  |  |  |  |  |  |  |  |  |  |  | $q$
|  |  |  |  |  | $q$ |  |  |  |  |  |  |  |
|  |  |  | $q$ |  |  |  |  |  |  |  |  |  |
|  |  |  |  |  |  |  |  |  |  |  | $q$ |  |
|  |  |  |  |  |  |  |  |  |  |  | $m$ |  |
|  |  |  | $m$ |  |  |  |  |  |  |  |  |  |
|  |  |  |  |  | $g(m)$ |  |  |  |  |  |  |  |
|  |  |  |  |  |  |  |  |  |  |  |  |  | $g(m)$

Figure 2: The strategy on the encoding of the Id-type between functions

######  Example 3.7.

The elimination rule of N-type with respect to a universe generates the
encodings of _transfinite_ dependent types. For instance, the encoding of the
type $\mathsf{x:N\vdash List_{N}(x)\ type}$ of finite lists of natural
numbers, which satisfies the judgemental equalities
$\mathsf{List_{N}(\underline{0})\equiv 1}$ and
$\mathsf{List_{N}(\underline{n+1})\equiv List_{N}(\underline{n})\times N}$, is
defined by applying the elimination rule of N-type to the terms ⊢En(1) : U x :
N, y : U ⊢En(El(y) ×N) : U.

Then, the strategy

$\psi^{\prime}\colonequals\mathscr{R}^{N}(\mathrm{En}(1),\mathrm{En}(\mathrm{El}(\pi_{2})\mathbin{\&}N)):N\rightarrow\mathcal{U}_{0}$

that interprets this encoding of the list type plays as in Figure 3.

$N$ | $\stackrel{{\scriptstyle\psi^{\prime}}}{{\rightarrow}}$ | $\mathcal{U}$
---|---|---
|  | $q$
$q$ |  |
$0$ |  |
|  | $\sharp(1)$

$N$ | $\stackrel{{\scriptstyle\psi^{\prime}}}{{\rightarrow}}$ |  | $\mathcal{U}$ |
---|---|---|---|---
|  |  | $q$ |
$q$ |  |  |  |
$1$ |  |  |  |
|  |  | $\sharp(\Sigma)$ |
|  | $q$ |  |
|  | $\sharp(1)$ |  |

$N$ | $\stackrel{{\scriptstyle\psi^{\prime}}}{{\rightarrow}}$ |  | $\mathcal{U}$ |
---|---|---|---|---
|  |  | $q$ |
$q$ |  |  |  |
$1$ |  |  |  |
|  |  | $\sharp(\Sigma)$ |
|  |  |  | $q$
|  |  |  | $\sharp(N)$

$N$ | $\stackrel{{\scriptstyle\psi^{\prime}}}{{\rightarrow}}$ |  |  |  | $\mathcal{U}$ |
---|---|---|---|---|---|---
|  |  |  |  | $q$ |
$q$ |  |  |  |  |  |
$2$ |  |  |  |  |  |
|  |  |  |  | $\sharp(\Sigma)$ |
|  |  | $q$ |  |  |
|  |  | $\sharp(\Sigma)$ |  |  |
|  | $q$ |  |  |  |
|  | $\sharp(1)$ |  |  |  |

$N$ | $\stackrel{{\scriptstyle\psi^{\prime}}}{{\rightarrow}}$ |  |  |  | $\mathcal{U}$ |
---|---|---|---|---|---|---
|  |  |  |  | $q$ |
$q$ |  |  |  |  |  |
$2$ |  |  |  |  |  |
|  |  |  |  | $\sharp(\Sigma)$ |
|  |  | $q$ |  |  |
|  |  | $\sharp(\Sigma)$ |  |  |
|  |  |  | $q$ |  |
|  |  |  | $\sharp(N)$ |  |

$N$ | $\stackrel{{\scriptstyle\psi^{\prime}}}{{\rightarrow}}$ |  |  |  | $\mathcal{U}$ |
---|---|---|---|---|---|---
|  |  |  |  | $q$ |
$q$ |  |  |  |  |  |
$2$ |  |  |  |  |  |
|  |  |  |  | $\sharp(\Sigma)$ |
|  |  |  |  |  | $q$
|  |  |  |  |  | $\sharp(N)$

Figure 3: The strategy on the encoding of the list type

Let us note that this list type is out of the scope of the denotational
semantics by Abramsky et al. [AJV15, VJA18], let alone its encoding, because
their interpretation is limited to _finite inductive types_ [VJA18, Figure 7];
also see [Yam22, §4.3] on this point. This argument in particular implies that
their approach cannot interpret the combination of universes and N-type.

##  4 Corollaries

This last section presents corollaries of Theorem 3.5 established in the
previous section. The first corollary is the effectivity of the game semantics
of universes (§4.1), the second one is the independence of the axiom of
equality reflection (§4.2), and the last one is the independence of Markov’s
principle (§4.3).

###  4.1 Effectivity of game semantics

Let us first show the effectivity of our interpretation of universes. Note
that strategies in the CwF $\mathbb{UPG}_{\oc}$ are the conventional ones
(§2.1), which are winning and well-bracketed. Note also that much more
unrestricted strategies that interpret terms in the higher-order functional
programming language PCF [Sco93, Plo77] are all effective or _recursive_ ; see
[AJM00, §5] and [HO00, §5.6] for the details. In essence, terms and morphisms
in $\mathbb{UPG}_{\oc}$ are winning, well-bracketed strategies in the game
semantics of PCF that satisfy the additional condition imposed by p-games
(Definition 2.22).

The definition of recursive strategies is therefore directly applicable to
terms and morphisms in $\mathbb{UPG}_{\oc}$. Roughly, assuming that moves in
games are encodable by natural numbers, a strategy is _recursive_ if its
computational steps are all computable (with respect to the encoding of moves
by natural numbers) in the standard sense of recursion theory [RR67]. We then
define:

######  Definition 4.1 (an effective subCwF
$\mathbb{UPG}_{\oc}^{\mathrm{eff}}$).

Let $\mathbb{UPG}_{\oc}^{\mathrm{eff}}\hookrightarrow\mathbb{UPG}_{\oc}$ be
the lluf substructural CwF of the CwF $\mathbb{UPG}_{\oc}$ whose terms and
morphisms are all recursive.

Because strategies in $\mathbb{UPG}_{\oc}$ that interpret terms in MLTT are
much more restricted than those that interpret terms in PCF, it is just
straightforward555Again, the point here is that our strategies are just the
conventional ones, so the arguments of the existing methods such as [AJM00,
§5] and [HO00, §5.6] are directly applicable. to verify:

######  Corollary 4.2 (effective game semantics of universes).

The CwF $\mathbb{UPG}_{\oc}^{\mathrm{eff}}$ is well-defined and supports One-,
Zero-, N-, Pi-, Sigma- and Id-types as well as the cumulative hierarchy of
universes in the same way as $\mathbb{UPG}_{\oc}$. This in particular
establishes effective game semantics of universes.

This corollary implies that our game semantics of MLTT equipped with the
aforementioned types only employs recursive strategies, i.e., the game
semantics is _computational_. Because universes are _types of types_ or _sets
of sets_ , this computational result is nontrivial.

###  4.2 Independence of equality reflection

Next, let us show the independence of the axiom of _equality reflection_
[Pal98] from MLTT: Given terms
$\psi,\psi^{\prime}\in\mathrm{Tm}(\Gamma,\mathcal{C})$, if
$\mathrm{El}(\psi)=\mathrm{El}(\psi^{\prime})\in\mathrm{Ty}(\Gamma)$, then
$\psi=\psi^{\prime}$. Then, a key observation is that, by the _intensional_
nature of our game semantics, there can be more than one term that encodes the
same type. For instance, the term
$\mathrm{En}(1)\in\mathrm{Tm}(T.N,\mathcal{U})$ that encodes One-type
$1\in\mathrm{Ty}(T.N)$ plays by  $T.N$
$\stackrel{{\scriptstyle\mathrm{En}(1)}}{{\rightarrow}}$ $\mathcal{U}$ $q$
$\sharp(1)$ while another term $\psi\in\mathrm{Tm}(T.N,\mathcal{U})$ that
plays by  $T.N$ $\stackrel{{\scriptstyle\psi}}{{\rightarrow}}$ $\mathcal{U}$
$q$ $q$ $n$ $\sharp(1)$ for all $n\in\mathbb{N}$ also encodes the same type
(n.b., this term is given by the elimination rule of N-type).

This argument together with Theorem 3.5 immediately implies:

######  Corollary 4.3 (independence of equality reflection).

The axiom of equality reflection is independent from MLTT equipped with One-,
Zero-, N-, Pi-, Sigma- and Id-types as well as universes.

We have seen that the intensional nature of strategies plays a crucial role
for this corollary, but it is not available for other computational semantics
such as domains and realisability [Pal93, Str12, BL18].

###  4.3 Independence of Markov’s principle

Finally, the previous work [Yam22, §4.7] shows that _Markov’s principle_
[Mar62] is invalid in the game semantics, which implies that the principle is
_independent_ from MLTT equipped with One-, Zero-, N-, Pi-, Sigma- and Id-
types. Markov’s principle is a well-known principle in constructive
mathematics, and it depends on the school of constructive mathematics whether
the principle is to be regarded as _constructive_. Roughly, the principle
postulates that if it is impossible that there is no natural number
$n\in\mathbb{N}$ such that $f(n)=0$ for a function
$f:\mathbb{N}\rightarrow\mathbb{N}$, then there _is_ a natural number
$n^{\prime}\in\mathbb{N}$ such that $f(n^{\prime})=0$.

The proof of this independence result given in the previous work is also valid
for the present game semantics _without any modification_. This immediately
extends the independence result to universes:

######  Corollary 4.4 (independence of Markov’s principle from universes).

Markov’s principle is independent from MLTT equipped with One-, Zero-, N-,
Pi-, Sigma- and Id-types as well as universes.

Again, this game-semantic proof [Yam22] takes advantages of the _intensional_
nature of game semantics, which is not available for other computational
semantics of MLTT.

Coquand and Manna [MC17] show the independence of Markov’s principle from MLTT
equipped with a single universe for the first time in the literature. Their
independence proof is _syntactic_ , which stands in contrast to our game-
semantic proof. As we have mentioned, their syntactic proof is not
automatically extendable to other types, and an extension can be nontrivial.
In contrast, our game-semantic reasoning is _modular_ : A meta-theoretic
result on MLTT given by our game semantics is automatically extended to new
types as soon as the game semantics is extended to the types. This is one of
the strong advantages of the game-semantic approach for the study of type
theory and constructive mathematics.

##  5 Conclusion and future work

We have established computational game semantics of the cumulative hierarchy
of universes for the first time in the literature. We have also applied this
game semantics to the meta-theoretic study of MLTT and shown that equality
reflection and Markov’s principle are both independent from MLTT equipped with
the hierarchy of universes, illustrating advantages of the game-semantic
approach.

For future work, we plan to extend the game semantics further to Martin-Löf’s
_well-founded tree (W-) types_ [ML82]. The resulting game semantics will be a
very powerful semantic foundation of constructive mathematics, e.g., it will
interpret Aczel’s constructive set theory (CZF) [Acz86] since CZF is
translatable into MLTT equipped with universes and W-types.

## References

  * [A+97] Samson Abramsky et al., _Semantics of interaction: An introduction to game semantics_ , Semantics and Logics of Computation 14 (1997), 1–31.
  * [Acz86] Peter Aczel, _The type theoretic interpretation of constructive set theory: inductive definitions_ , Studies in Logic and the Foundations of Mathematics, vol. 114, Elsevier, 1986, pp. 17–49.
  * [AJM00] Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria, _Full abstraction for PCF_ , Information and Computation 163 (2000), no. 2, 409–470.
  * [AJV15] Samson Abramsky, Radha Jagadeesan, and Matthijs Vákár, _Games for dependent types_ , Automata, Languages, and Programming, Springer, Berlin, Heidelberg, 2015, pp. 31–43.
  * [AM99] Samson Abramsky and Guy McCusker, _Game semantics_ , Computational Logic: Proceedings of the 1997 Marktoberdorf Summer School (Berlin, Heidelberg), Springer, 1999, pp. 1–55.
  * [BL18] Valentin Blot and Jim Laird, _Extensional and intensional semantic universes: A denotational model of dependent types_ , Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, ACM, 2018, pp. 95–104.
  * [Chr00] Juliusz Chroboczek, _Game semantics and subtyping_ , Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No. 99CB36332), IEEE, 2000, pp. 192–203.
  * [Coq95] Thierry Coquand, _A semantics of evidence for classical arithmetic_ , The Journal of Symbolic Logic 60 (1995), no. 1, 325–337.
  * [DP16] Peter Dybjer and Erik Palmgren, _Intuitionistic type theory_ , Stanford Encyclopedia of Philosophy (2016).
  * [Dyb96] Peter Dybjer, _Internal Type Theory_ , Types for Proofs and Programs, Springer, 1996, pp. 120–134.
  * [Fra22] Adolf Fraenkel, _Zu den grundlagen der cantor-zermeloschen mengenlehre_ , Mathematische annalen 86 (1922), no. 3-4, 230–237.
  * [GHK+03] Gerhard Gierz, Karl Heinrich Hofmann, Klaus Keimel, Jimmie D Lawson, Michael Mislove, and Dana S Scott, _Continuous lattices and domains_ , vol. 93, Cambridge university press, 2003.
  * [Gir72] Jean-Yves Girard, _Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur_ , Ph.D. thesis, Éditeur inconnu, 1972.
  * [Gir87] , _Linear logic_ , Theoretical Computer Science 50 (1987), no. 1, 1–101.
  * [GR94] Edward Griffor and Michael Rathjen, _The strength of some martin-löf type theories_ , Archive for Mathematical Logic 33 (1994), no. 5, 347–385.
  * [Gun92] Carl A Gunter, _Semantics of programming languages: Structures and techniques_ , MIT press, Cambridge, MA, 1992.
  * [HO00] J Martin E Hyland and C-HL Ong, _On full abstraction for PCF: I, II, and III_ , Information and Computation 163 (2000), no. 2, 285–408.
  * [Hof97] Martin Hofmann, _Syntax and Semantics of Dependent Types_ , Extensional Constructs in Intensional Type Theory, Springer, 1997, pp. 13–54.
  * [Hyl82] J Martin E Hyland, _The effective topos_ , Studies in Logic and the Foundations of Mathematics, vol. 110, Elsevier, 1982, pp. 165–216.
  * [Hyl97] Martin Hyland, _Game semantics_ , Semantics and Logics of Computation, vol. 14, Cambridge University Press, New York, 1997, p. 131.
  * [Lai97] James Laird, _Full abstraction for functional languages with control_ , Logic in Computer Science, 1997. LICS’97. Proceedings., 12th Annual IEEE Symposium on, IEEE, 1997, pp. 58–67.
  * [Mar62] Andrei Andreevich Markov, _On constructive mathematics_ , Trudy Matematicheskogo Instituta imeni VA Steklova 67 (1962), 8–14.
  * [MC17] Bassel Mannaa and Thierry Coquand, _The independence of markov’s principle in type theory_ , Logical Methods in Computer Science 13 (2017).
  * [McC98] Guy McCusker, _Games and full abstraction for a functional metalanguage with recursive types_ , Springer Science & Business Media, London, 1998.
  * [ML75] Per Martin-Löf, _An Intuitionistic Theory of Types: Predicative Part_ , Studies in Logic and the Foundations of Mathematics 80 (1975), 73–118.
  * [ML82] , _Constructive Mathematics and Computer Programming_ , Studies in Logic and the Foundations of Mathematics 104 (1982), 153–175.
  * [ML84] , _Intuitionistic Type Theory: Notes by Giovanni Sambin of a series of lectures given in Padova, June 1980_ , 1984.
  * [ML98] , _An Intuitionistic Theory of Types_ , Twenty-five years of constructive type theory 36 (1998), 127–172.
  * [Pal93] Erik Palmgren, _An information system interpretation of martin-löf’s partial type theory with universes_ , Information and Computation 106 (1993), no. 1, 26–60.
  * [Pal98] , _On universes in type theory_ , Twenty five years of constructive type theory (1998), 191–204.
  * [Plo77] Gordon D. Plotkin, _Lcf considered as a programming language_ , Theoretical computer science 5 (1977), no. 3, 223–255.
  * [RR67] Hartley Rogers and H Rogers, _Theory of recursive functions and effective computability_ , vol. 5, McGraw-Hill, New York, 1967.
  * [Sco93] Dana S Scott, _A type-theoretical alternative to iswim, cuch, owhy_ , Theoretical Computer Science 121 (1993), no. 1-2, 411–440.
  * [Set93] Anton Setzer, _Proof theoretical strength of martin-löf type theory with w-type and one universe_ , Ph.D. thesis, Uitgever niet vastgesteld, 1993.
  * [Sho67] Joseph R Shoenfield, _Mathematical logic_ , vol. 21, Addison-Wesley, Reading, 1967.
  * [Str12] Thomas Streicher, _Semantics of Type Theory: Correctness, Completeness and Independence Results_ , Springer Science & Business Media, 2012.
  * [TvD88] Anne Sjerp Troelstra and Dirk van Dalen, _Constructivism in mathematics. two volumes_ , NorthHolland, Amsterdam (1988).
  * [VJA18] Matthijs Vákár, Radha Jagadeesan, and Samson Abramsky, _Game semantics for dependent types_ , Information and Computation 261 (2018), 401–431.
  * [Yam19] Norihiro Yamada, _A game-semantic model of computation_ , Research in the Mathematical Sciences 6 (2019), no. 1, 3.
  * [Yam22] , _Game semantics of martin-löf type theory_ , Mathematical Structures in Computer Science, to appear (2022).
  * [Zer08] Ernst Zermelo, _Untersuchungen über die grundlagen der mengenlehre. i_ , Mathematische Annalen 65 (1908), no. 2, 261–281.