Given UoPLIs $\lambda :: A \multimap B$, $\gamma :: C \multimap D$, $\eta :: A \multimap C$ and $\epsilon :: \oc A \multimap B$ between p-games, we obtain UoPLIs $\lambda \otimes \gamma :: A \otimes C \multimap B \otimes D$, $\langle \lambda, \eta \rangle :: A \multimap B \mathbin{\&} C$ and $\epsilon^\dagger :: \oc A \multimap \oc B$.

Thanks to these lemmata, the underlying FoPLI $\Phi$ on each UoPLI $\phi$, i.e., $\phi = \bigcup \Phi$, does not matter, and we may simply apply the constructions on t-skeletons to those on UoPLIs without referring to underlying FoPLIs.

Furthermore, the constructions on t-skeletons such as tensor $\otimes$, composition $\circ$, pairing $\langle \_, \_ \rangle$ and promotion $(\_)^\dagger$ all respect identifications on t-skeletons <cit.>, and so we simply define the corresponding constructions on p-strategies in terms those on t-skeletons, i.e., $\mathrm{Sat}(\psi) \circ \mathrm{Sat}(\phi) \colonequals \mathrm{Sat}(\psi \circ \phi)$, $\mathrm{Sat}(\varphi)^\dagger\colonequals \mathrm{Sat}(\varphi^\dagger)$, etc.

Let us proceed to recall one of the most basic t-skeletons: copy-cat t-skeletons.
As the name suggests, they simply `copy-cat' the last O-moves:

The copy-cat tree (t-) skeleton on a p-game $G$ is the t-skeleton $\mathrm{tcp}_G :: G \multimap G$ defined by

\begin{equation*}
\mathrm{tcp}_G \colonequals \{ \boldsymbol{s} \in P_{G^{[0]} \multimap G^{[1]}} \mid \forall \boldsymbol{t} \preceq{\boldsymbol{s}}. \ \mathrm{Even}(\boldsymbol{t}) \Rightarrow \boldsymbol{t} \upharpoonright G^{[0]} = \boldsymbol{t} \upharpoonright G^{[1]} \ \! \},
\end{equation*}

where the superscripts $(\_)^{[i]}$ on $G$ are to distinguish the two copies of $G$, and $\boldsymbol{t} \upharpoonright G^{[i]}$ is the j-subsequence of $\boldsymbol{t}$ that consists of moves in $G^{[i]}$ ($i = 0, 1$).

Let us also recall a relative of copy-cat t-skeletons:

The $\boldsymbol{i}^{\text{th}}$ dereliction tree (t-) skeleton ($i \in \mathbb{N}$) on a game $G$ is the t-skeleton $\mathrm{tder}_G^{(i)} :: G \Rightarrow G$ defined by

\begin{equation*}
\mathrm{tder}_G^{(i)} \colonequals \{ \boldsymbol{s} \in P_{\oc G \multimap G} \mid \forall \boldsymbol{t} \preceq \boldsymbol{s} . \, \mathrm{Even}(\boldsymbol{t}) \Rightarrow (\boldsymbol{t} \upharpoonright \oc G) \upharpoonright i = \boldsymbol{t} \upharpoonright G \, \}.
\end{equation*}

That is, the $i^{\text{th}}$ dereliction t-skeleton $\mathrm{tder}_G^{(i)}$ for each $i \in \mathbb{N}$ plays essentially in the same way as the copy-cat t-skeleton $\mathrm{tcp}_G$, where $\mathrm{tder}_G^{(i)}$ employs specifically the `tag' $(\_, i)$ on the domain $\oc G$.
Of course, any choice of $i \in \mathbb{N}$ should not matter, which illustrates the point that t-skeletons are not abstract enough for modeling terms in type theories.
This point motivates us to introduce predicative (p-) strategies:

The original definition of p-strategies given in <cit.> are different from yet equivalent to the one given below.
The modification is just for brevity.

A predicative (p-) strategy on a p-game $G$ is the saturation $\mathrm{Sat}(\sigma) \colonequals \{ \sigma' :: G \mid \sigma \simeq_G \sigma' \, \} \subseteq P_G$, written $\mathrm{Sat}(\sigma) : G$, of an arbitrary t-skeleton $\sigma :: G$ that satisfies validity: $\sigma \simeq_G \sigma$.
Given $\sigma' :: G$, we write $\sigma' \propto \mathrm{Sat}(\sigma)$ and say that $\sigma'$ implements $\mathrm{Sat}(\sigma)$ if $\sigma \simeq_G \sigma'$.

Without the universal identification $\simeq_{\mathscr{U}}$ (Definition <ref>), we would have to equip each p-strategy with an identification.

However, it would be mathematically cumbersome, and not properly generalize the relation between games and strategies.
This is the main reason why the part I <cit.> introduces the universal one $\simeq_{\mathscr{U}}$.

For each p-game $G$, validity of a t-skeleton $\sigma :: G$ ensures nonemptiness of the p-strategy $\mathrm{Sat}(\sigma) : G$.
Because $\mathrm{Sat}(\sigma) = \mathrm{Sat}(\sigma')$ if and only if $\sigma \simeq_G \sigma'$ for all $\sigma, \sigma' :: G$ <cit.>, a p-strategy $\mathrm{Sat}(\sigma) : G$ is invariant with respect to a representative valid t-skeleton $\sigma :: G$ up to $\simeq_G$, which justify the arbitrary choice of $\sigma$ in Definition <ref>.

In particular, we clearly have $\mathrm{tder}_G^{(i)} \simeq_{G \Rightarrow G} \mathrm{tder}_G^{(j)}$ for any $i, j \in \mathbb{N}$, for which recall Definition <ref>.
Hence, let us select $0 \in \mathbb{N}$ without any reason and define:

The copy-cat $\mathrm{pcp}_G : G \multimap G$ and the dereliction $\mathrm{pder}_G : G \Rightarrow G$ on a p-game $G$ are the p-strategies defined by

pcp_G Sat(tcp_G)
pder_G Sat(tder^(0)_G).

Finally, let us recall constraints on p-strategies that correspond to those on t-skeletons (Definition <ref>):

A p-strategy $g : G$ is

* Total if $\forall \boldsymbol{s} m \in g^{\mathsf{Odd}} . \ \! \exists \boldsymbol{s} m n \in g$;

* Innocent if $g = \bigcup \{ \sigma :: G \mid \sigma \propto g, \text{$\sigma$ is innocent} \ \! \}$;

* Noetherian if there is no strictly increasing infinite sequence of elements in the set $\lceil g \rceil  \colonequals \{ \lceil \boldsymbol{s} \rceil \mid \boldsymbol{s} \in g \ \! \}$ of all P-views in $g$;

* Winning if it is total, innocent and noetherian.

Winning p-strategies are closed under tensor $\otimes$, pairing $\langle \_, \_ \rangle$, composition $\circ$ and promotion $(\_)^\dagger$.

A category $\mathbb{PG}$ consists of

* P-games as objects;

* P-strategies $A \Rightarrow B$ as morphisms $A \rightarrow B$;

* The p-strategy $\mathrm{Sat}(\psi) \bullet \mathrm{Sat}(\psi) \colonequals \mathrm{Sat}(\psi \circ \phi^\dagger) : A \Rightarrow C$ as the composition of morphisms $\mathrm{Sat}(\phi) : A \rightarrow B$ and $\mathrm{Sat}(\psi) : B \rightarrow C$;

* The dereliction $\mathrm{pder}_A : A \Rightarrow A$ as the identity $\mathrm{id}_A$ on each object $A$.

The lluf subcategory $\mathbb{LPG}$ of $\mathbb{PG}$ has winning p-strategies in $\mathbb{PG}$ as morphisms.

We could further impose well-bracketing on p-strategies as in <cit.>, but we do not in this article for brevity.
The categories $\mathbb{PG}$ and $\mathbb{LPG}$ are cartesian closed, where a terminal object, products and exponential objects are given by the unit p-game $\boldsymbol{1}$, product $\&$ and implication $(\_) \Rightarrow (\_) \colonequals \oc (\_) \multimap (\_)$, respectively <cit.>.
Moreover, we may enrich $\mathbb{PG}$ and $\mathbb{LPG}$ by algebraic CPOs <cit.>; see <cit.> for the details.

Given a p-game $G$, we write $\mathbb{PG}(G)$ (resp. $\mathbb{LPG}(G)$) for the set of all morphisms $\boldsymbol{1} \rightarrow G$ in $\mathbb{PG}$ (resp. $\mathbb{LPG}$), and we do not notationally distinguish strategies on $G$ and those on $\boldsymbol{1} \multimap G$ or $\boldsymbol{1} \Rightarrow G$.
Given a p-strategy $g : \oc \oc G$, we write $g^\ddagger : \oc G$ for the p-strategy that plays essentially in the same way as $g$, which is obtained from $g$ by the bijection $\langle \_, \_ \rangle : \mathbb{N} \times \mathbb{N} \stackrel{\sim}{\rightarrow} \mathbb{N}$ in the evident manner.

§.§ Game semantics of intensional Martin-Löf type theory

As the last preparation, let us sketch in this section the proof of the following main theorem of the previous work <cit.>:

The category $\mathbb{LPG}$ gives rise to a model of MLTT equipped with unit-, empty-, N-, pi-, sigma- and Id-types.

For lack of space, the part I <cit.> models only pi- and sigma-types and leaves the other types to the part II <cit.>, whose outline is given in <cit.>.

Technically, the model is given via an algebraic model of MLTT, called a category with families (CwF), equipped with semantic type formers for the types <cit.>.
For brevity, however, we do not review the game-semantic CwF with the semantic type formers in this section, leaving the details to the previous work <cit.>.
Instead, we directly sketch the game-semantic counterparts of some major type constructions.

First, the model interprets (dependent) types by:

A dependent predicative (p-) game on a p-game $\Gamma$ is a continuous map $A$ from the algebraic CPO $\mathbb{PG}(\oc \Gamma)$ to the flat CPO on $\mathsf{ob}(\mathbb{PG})$ such that the union $\bigcup_{g \in \mathbb{PG}(\oc \Gamma)} \vdash_{A(g)}$ is well-founded.

It is constant if $A(g) = A(g')$ for all $g, g' \in \mathbb{PG}(\oc \Gamma)$.

We often represent a dependent p-game $A$ on a p-game $\Gamma$ as a family $(A(g))_{g \in \mathbb{PG}(\oc \Gamma)}$ of p-games $A(g)$.
The dependent p-game $A$ is indexed by p-strategies on the exponential $\oc \Gamma$, not $\Gamma$, for allowing non-promotions as inputs of the pi $\Pi (\Gamma, A)$ (Definition <ref>), which models pi-types.
This point does not matter for Theorem <ref> since morphisms in $\mathbb{LPG}$ are all innocent; however, it is crucial for inheriting the flexibility of game semantics to systematically model effects and linear typing <cit.>.

Each dependent p-game is continuous as in the domain-theoretic model of MLTT <cit.>.
The continuity is conceptually natural particularly if we think of the game semantics of universes <cit.>.
Technically, at least monotonicity of dependent p-games is necessary for the sigma $\Sigma(\Gamma, A)$ (Definition <ref>); see <cit.> for the details.

Given p-games $\Gamma$ and $\Gamma'$, we write $\{ \Gamma' \}_\Gamma$ for the constant dependent p-game on $\Gamma$ valued at $\Gamma'$, and $\mathscr{D}\mathbb{PG}(\Gamma)$ for the set of all dependent p-games on $\Gamma$.

Let us next recall a key auxiliary construction that supports pi and sigma:

The integration of a dependent p-game $A$ on a p-game $\Gamma$ is the p-game $\int_\Gamma A$ given by

∫_ΓA DetJ(⋃_g ∈ℙ𝔾(Γ)A(g))

where $\mathrm{DetJ}(\mathcal{A}) \colonequals \{ \, \bigcup \mathcal{S} \mid \mathcal{S} \subseteq \mathcal{A}, \text{$\mathcal{S}$ is consistent and deterministic} \, \} \supseteq \mathcal{A}$ for a given set $\mathcal{A}$ of t-skeletons.

If each p-game were equipped with its own identification, then it is not obvious how to define integration $\int$ that preserves the identifications.
It is another reason why we employ the universal identification $\simeq_{\mathscr{U}}$ (Definition <ref>).

Given a dependent p-game $A$ on a p-game $\Gamma$, the integration $\int_\Gamma A$ is a well-defined p-game.

Let us just remark that $\int_\Gamma A$ is det-j complete by the operation $\mathrm{DetJ}$.

We are now ready to recall pi and sigma:

A family of dependently pointwise linear implications (FoDPLI) from a p-game $\Gamma$ to a dependent p-game $A$ on $\Gamma$ is an FoPLI $\Phi$ from $\Gamma$ to $\int_\Gamma A$ that satisfies

\begin{equation*}
\forall \gamma :: \Gamma . \, A(\mathrm{Sat}(\gamma)^\dagger) \in \mathbb{PG} \Rightarrow (\bigcup \Phi) \circ \gamma :: A(\mathrm{Sat}(\gamma)^\dagger),
\end{equation*}

where the UoPLI $\bigcup \Phi \colonequals \bigcup_{\gamma :: \Gamma}\Phi_\gamma$ on $\Phi$ is called a union of DPLIs (UoDPLI) from $\Gamma$ to $A$.
We write $\mathscr{F}(\Gamma, A)$ for the set of all FoDPLIs from $\Gamma$ to $A$

The linear-pi from a p-game $\Gamma$ to a dependent p-game $A$ on $\Gamma$ is the p-game $\ell \Pi (\Gamma, A)$ defined by

\begin{equation*}
\ell \Pi (\Gamma, A) \colonequals \{ \, \bigcup \Phi \mid \Phi \in \mathscr{F}(\Gamma, A) \, \}.
\end{equation*}

The pi from a p-game $\Gamma$ to a dependent p-game $A$ on $\Gamma$ is the p-game $\Pi (\Gamma, A)$ given by $\Pi(\Gamma, A) \colonequals \ell \Pi(\oc \Gamma, A^\ddagger)$, where $A^\ddagger \in \mathscr{D}\mathbb{PG}(\oc \Gamma)$ is given by $A^\ddagger(\hat{a}) \colonequals A(\hat{g}^{\ddagger})$ for all $\hat{g} \in \mathbb{PG}(\oc \oc \Gamma)$.

The sigma of a p-game $\Gamma$ and a dependent p-game $A$ on $\Gamma$ is the p-game $\Sigma (\Gamma, A)$ defined by

\begin{equation*}
\Sigma(\Gamma, A) \colonequals \{ \langle \gamma, \alpha \rangle :: \Gamma \mathbin{\&} \int_\Gamma A \mid A(\mathrm{Sat}(\gamma)^\dagger) \in \mathbb{PG} \Rightarrow \alpha :: B(\mathrm{Sat}(\gamma)^\dagger) \, \}.
\end{equation*}

In terms of the syntax of MLTT, pi and sigma interpret the formation rules

$\mathsf{\vdash A \ type}$
$\mathsf{x : A \vdash B \ type}$

$\mathsf{\vdash \Pi_{x : A}B \ type}$
$\mathsf{\vdash A \ type}$
$\mathsf{x : A \vdash B \ type}$

$\mathsf{\vdash \Sigma_{x : A}B \ type}$

$\{ A \, \}_{\boldsymbol{1}} \in \mathscr{D}\mathbb{PG}(\boldsymbol{1})$
$B \in \mathscr{D}\mathbb{PG}(A)$

$\{ \Pi(A, B) \}_{\boldsymbol{1}} \in \mathscr{D}\mathbb{PG}(\boldsymbol{1})$
$\{ A \, \}_{\boldsymbol{1}} \in \mathscr{D}\mathbb{PG}(\boldsymbol{1})$
$B \in \mathscr{D}\mathbb{PG}(A)$

$\{ \Sigma(A, B) \}_{\boldsymbol{1}} \in \mathscr{D}\mathbb{PG}(\boldsymbol{1})$

respectively, where note that the type $\mathsf{A}$ is simple.
The general case, where $\mathsf{A}$ may be dependent, is handled simply in the pointwise fashion; see <cit.> for the details.
Also, the game semantics models terms $\mathsf{\Gamma \vdash a : A}$ by elements $a \in \mathbb{LPG}(\Pi(\Gamma, A))$.

Next, the unity-type $\mathsf{1}$, the empty-type $\mathsf{0}$ and the natural number type $\mathsf{N}$ are modeled by the unit p-game $\boldsymbol{1}$, the empty p-game $\boldsymbol{0}$ and the natural number p-game $N$, respectively (Example <ref>); again, see <cit.> for the details.

Let us proceed to recall the game semantics of Id-types:

Given a p-game $\Gamma$ and p-strategies $g, g' \in \mathbb{LPG}(\Gamma)$, the Identity (Id) predicative (p-) game between $g$ and $g'$ is the p-game $\mathrm{Id}_\Gamma(g, g') \colonequals \begin{cases} \boldsymbol{1} &\text{if $g = g'$;} \\ \boldsymbol{0} &\text{otherwise.} \end{cases}$

Similarly to the case of pi and sigma, Id p-games interpret the formation rule

$\mathsf{\vdash A \ type}$
$\mathsf{\vdash a : A}$
$\mathsf{\vdash a' : A}$

$\mathsf{\vdash Id_A(a, a') \ type}$

$\{ A \, \}_{\boldsymbol{1}} \in \mathscr{D}\mathbb{PG}(\boldsymbol{1})$
$a, a' \in \mathbb{LPG}(\Pi(\boldsymbol{1}, \{ A \}_{\boldsymbol{1}}) \cong A)$

$\{ \mathrm{Id}_A(a, a') \}_{\boldsymbol{1}} \in \mathscr{D}\mathbb{PG}(\boldsymbol{1})$

The general case is again dealt with in the pointwise fashion <cit.>.

Finally, the game semantics of MLTT <cit.> models the $\xi$-rule as its interpretation of currying simply adjusts `tags' on moves just like game semantics of simple type theories <cit.>, which does not change p-strategies in an essential way.
On the other hand, the game semantics refutes CT due to the second axiom of Definition <ref>.

§ CONSISTENCY OF INTENSIONAL MARTIN-LÖF TYPE THEORY WITH FORMAL CHURCH'S THESIS

We have reviewed all the necessary preliminaries, and therefore let us now turn to the main content of this article: consistency of MLTT with CT.

In this section, we prove the consistency by a constructive model of MLTT plus CT as follows.
We first define recursive t-skeletons and their realizers, and fix a choice of canonical realizers for technical convenience in Section <ref>.
Next, we introduce another, `nonstandard' variant of p-games, called np-games, to accommodate disjoint unions of winning-realizer-wise linear implications (DoWRWLIs) in Section <ref>.
DoWRWLIs are t-skeletons on modified linear implication, in which O must play on the domain by a winning, recursive t-skeleton and exhibit the canonical realizer for it at his first move.

As explained in Section <ref>, DoWRWLIs implement our idea on how to validate CT.

Next, we show that a CCC $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ of well-opened np-games and winning, recursive DoWRWLIs gives rise to a CwF equipped with semantic type formers for unit-, empty-, N-, pi-, sigma- and Id-types in Section <ref>, which establishes a model of MLTT equipped with these types.
Finally, we prove that the model of MLTT in $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ (even constructively) validates CT and refutes empty-type, establishing consistency of MLTT with CT, in Section <ref>.

§.§ Recursive tree skeletons and canonical realizers

In this section, we define recursive t-skeletons and their realizers, which are based on recursion theory <cit.> similarly to Section 5.6 of the classic HO-games <cit.>.
Also, for technical convenience, we fix a canonical realizer for each recursive t-skeleton.

First, let us arbitrarily encode standard moves (Definition <ref>) by finite sequences of natural numbers, which is clearly possible <cit.>.
Next, let us recall that the pointer of each j-sequence (Definition <ref>) is a finite function on natural numbers.
It then follows from these two points that there is a recursive bijection $\mathscr{J}(\mathscr{M}) \stackrel{\sim}{\rightarrow} \mathbb{N}$ <cit.>.

Let us fix once and for all a recursive bijection $\mathscr{C} : \mathscr{J}(\mathscr{M}) \stackrel{\sim}{\rightarrow} \mathbb{N}$ and call $\mathscr{C}(\sigma) \subseteq \mathbb{N}$ the coding of t-skeletons $\sigma \subseteq \mathscr{J}(\mathscr{M})$.

The coding $\mathscr{C}$ of t-skeletons enables us to employ recursion theory for defining `constructive' or recursive t-skeletons similarly to HO-games <cit.>:

Let us fix once and for all an enumeration or Gödel numbering $\mathscr{G}_{\mathrm{PRF}} : \mathbb{N} \twoheadrightarrow \mathrm{PRF}$ on the set $\mathrm{PRF}$ of all partial recursive functions $\mathbb{N} \rightharpoonup \mathbb{N}$.

The functional representation of a t-skeleton $\sigma \subseteq \mathscr{J}(\mathscr{M})$ is the partial map $\mathrm{fun}(\sigma) : \mathscr{C}(\sigma^{\mathrm{Odd}}) \rightharpoonup \mathscr{C}(\sigma^{\mathrm{Even}})$ given by

\begin{equation*}
\mathrm{fun}(\sigma)(\mathscr{C}(\boldsymbol{s}m)) \colonequals \begin{cases} \mathscr{C}(\boldsymbol{s}mn) &\text{if there is $\boldsymbol{s}mn \in \sigma^{\mathrm{Even}}$;} \\ \uparrow &\text{otherwise} \end{cases} \quad (\boldsymbol{s}m \in \sigma^{\mathrm{Odd}}).
\end{equation*}

A realizer for a t-skeleton $\sigma \subseteq \mathscr{J}(\mathscr{M})$ is a natural number $e \in \mathbb{N}$ that realizes (the functional representation of) $\sigma$:

\begin{equation*}
\forall \boldsymbol{s}m \in \sigma^{\mathrm{Odd}} . \, \mathscr{G}_{\mathrm{PRF}}(e)(\mathscr{C}(\boldsymbol{s}m)) \simeq \mathrm{fun}(\sigma)(\mathscr{C}(\boldsymbol{s}m)),
\end{equation*}

and a t-skeleton is recursive if there is a realizer for it.

Our definition of recursive t-skeletons is the same as that of recursive strategies <cit.> except that the latter focuses on innocent strategies and their P-views.
Our choice is just for simplicity; we could follow precisely the latter formulation.

Note that a realizer $e$ for a recursive t-skeleton $\sigma$ is only concerned with positions in $\sigma$, and hence $\mathscr{G}_{\mathrm{PRF}}(e)$ may not coincide with $\mathrm{fun}(\sigma)$ as a partial map $\mathbb{N} \rightharpoonup \mathbb{N}$ (i.e., they may compute differently on natural numbers that do not code positions in $\sigma$).
Note also that $\mathscr{G}_{\mathrm{PRF}}(e)$ does not (even partially) decide odd-length positions in $\sigma$, and it only computes even-length ones from odd-length ones.
These `compromises' play a crucial role for our validation of CT (essentially because the set of all total recursive functions is not recursively enumerable <cit.>), as we shall see shortly.

From the viewpoint of recursion theory, it makes sense to also reformulate p-games as recursively enumerable sets of realizers for t-skeletons so that the initial protocols between P and J would be `effective,' and further impose that the set of the codings of all odd-length positions of a realizable t-skeleton is recursive so that P would be able to `effectively' decide if a given action by O is allowed in the t-skeleton.
However, we do not employ such more `effective' p-games and t-skeletons in this article since they are unnecessary for our consistency proof.

Let $G$ be any set of t-skeletons (so that $G$ can be an np-game (Definition <ref>) as well as a p-game).
We write $\mathcal{TS}_{\mathrm{r}}(G)$ (resp. $\mathcal{TS}_{\mathrm{wr}}(G)$) for the set of all recursive (resp. winning and recursive) t-skeletons in $G$, and $\mathscr{R}_{\mathrm{r}}(G)$ (resp. $\mathscr{R}_{\mathrm{wr}}(G)$) for the set of all realizers for recursive (resp. winning and recursive) ones in $G$.
Moreover, we write $\mathrm{tsk}_G$ or $\mathrm{tsk}$ for the surjection $\mathscr{R}_{\mathrm{r}}(G) \twoheadrightarrow \mathcal{TS}_{\mathrm{r}}(G)$ such that each natural number $e \in \mathscr{R}_{\mathrm{r}}(G)$ realizes the t-skeleton $\mathrm{tsk}_G(e) \in \mathcal{TS}_{\mathrm{r}}(G)$, i.e.,

\begin{equation*}
\mathrm{tsk}_G(e) \colonequals \{ \, \boldsymbol{s} \in \mathscr{J}(\mathscr{M}) \mid \mathscr{G}_{\mathrm{PRF}}(e)(\mathscr{C}(\boldsymbol{s})) = 1 \, \}.
\end{equation*}

Clearly, the partial recursive function $\mathscr{G}_{\mathrm{PRF}}(e)$ partially decides the set $\mathscr{C}(\mathrm{tsk}_G(e))$.

Let us then fix an arbitrary choice of a realizer for each recursive t-skeleton and call it the canonical one:

Let us fix once and for all a function $\mathscr{G}_G : \mathcal{TS}_{\mathrm{r}}(G) \rightarrow \mathscr{R}_{\mathrm{r}}(G)$ for each set $G$ of t-skeletons such that $\mathscr{G}_G(\sigma) \in \mathscr{R}_{\mathrm{r}}(G)$ realizes each $\sigma \in \mathcal{TS}_{\mathrm{r}}(G)$, and call $\mathscr{G}_G$ the canonical Gödel numbering on $G$.
We assume that canonical Gödel numberings satisfy the condition at the end of Definition <ref>.

We call the realizer $\mathscr{G}_G(\sigma)$ and the pair $(\sigma, \mathscr{G}_G(\sigma))$ the canonical realizer and the canonical pair for $\sigma$, respectively, and define

\begin{equation*}
\mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(G) \colonequals \{ \, (\sigma, \mathscr{G}_G(\sigma)) \mid \sigma \in \mathcal{TS}_{\mathrm{wr}}(G) \, \}.
\end{equation*}

For technical convenience (e.g., for Definitions <ref> and <ref>), we shall henceforth employ canonical pairs frequently.
Note that, although canonical realizers in general do not have complete information about t-skeletons, canonical pairs (trivially) do.

§.§ Cartesian closed category of well-opened nonstandard predicative games and winning, recursive, winning-realizer-wise tree skeletons

In this section, we modify a certain class of t-skeletons, called unions of pointwise linear implications (UoPLIs), on the linear implication $G \multimap H$ between p-games $G$ and $H$ <cit.>, and based on it define a modified linear implication $G \rightarrowtriangle H$.
In $G \rightarrowtriangle H$, O must play by a winning, recursive t-skeleton $\sigma$ on the domain $G$ and exhibit the canonical realizer for $\sigma$ at his first move.
This modification of linear implication implements our idea on how to model MLTT plus CT sketched in Section <ref>.

However, there arises a problem: P-games $G$ are not closed under the modified linear implication $\rightarrowtriangle$ because it does not preserve saturation of the set $P_G$ of all positions.
Note that we cannot simply discard the saturation axiom since if we do so then a t-skeleton $\sigma :: G$ may generate a p-strategy $\mathrm{Sat}(\sigma)$ that is not even a subset of $P_G$, i.e., p-strategies would be no longer `strategies on p-games' <cit.>.

On the other hand, recall that McCusker <cit.> dispenses with identification of positions and strategies by employing much simpler exponential $\hat{\oc}$ without the `tags' $(\_, i)$ such that $i \in \mathbb{N}$, which we call simplified exponential, and well-opened games for which simplified exponential $\hat{\oc}$ works.
As confessed in <cit.>, however, this simpler approach to cartesian closure of games is mathematically ad-hoc, and it is why the previous work <cit.> employs identifications of positions and p-strategies.

Nevertheless, the goal of the present work is to prove consistency of MLTT with CT, and mathematical elegance of the employed method is secondly.
Therefore, we adopt, as a solution to the above problem, McCusker's simplified exponential $\hat{\oc}$ and well-opened games.
Let us first recall these concepts plus thread-closed games:

A game $A$ is thread-closed if $\boldsymbol{s} \upharpoonright \mathscr{I} \in A$ for any position $\boldsymbol{s} \in A$ and set $\mathscr{I}$ of initial occurrences in $\boldsymbol{s}$, where $\boldsymbol{s} \upharpoonright \mathscr{I}$ is the j-subsequence of $\boldsymbol{s}$ that consists of occurrences in $\boldsymbol{s}$ hereditarily justified[An initial occurrence $m$ in a j-sequence $\boldsymbol{s}$ hereditarily justifies an occurrence $n$ in $\boldsymbol{s}$ if a finite iteration of the pointer $\mathcal{J}_{\boldsymbol{s}}$ applied to $n$ goes back to $m$ <cit.>.] by initial occurrences in $\mathscr{I}$, called the thread of $\boldsymbol{s}$ with respect to $\mathscr{I}$.

That is, a game is thread-closed if its positions are closed under taking threads.

The terminology thread-closed is not used in the original articles <cit.>.

The simplified exponential on a game $A$ is the game $\hat{\oc} A \colonequals \{ \, \boldsymbol{s} \in \mathscr{L}_{\mathrm{Arn}(A)} \mid \forall m \in M_A^{\mathrm{Init}} . \, \boldsymbol{s} \upharpoonright \{ m \} \in A \, \}$, where $\{ m \}$ ranges over the singleton set of each initial occurrence in $\boldsymbol{s}$ whose move is $m$ if there is such an initial occurrence in $\boldsymbol{s}$, and the empty set $\emptyset$ otherwise.

We want the relation $A \subseteq \hat{\oc} A$ for every game $A$ since we employ $\hat{\oc}$ as an alternative to exponential $\oc$ (Section <ref>).
Although it does not hold for games in general, it does for thread-closed ones; it is the point of the thread-closing constraint <cit.>.

As mentioned in <cit.>, however, identities (or identity morphisms) in the CCC of games, called derelictions, are not well-defined with respect to simplified exponential $\hat{\oc}$.
To remedy this problem, we have to further focus on:

A game $A$ is well-opened if the conjunction of $\boldsymbol{s} m \boldsymbol{t} \in A$ and $m \in M_A^{\mathrm{Init}}$ implies $\boldsymbol{s} = \boldsymbol{\epsilon}$.

In other words, a game is well-opened if its position contains at most one initial occurrence.
Note that well-opened games are trivially thread-closed.
Note also that well-opened games are not closed under (simplified) exponential, but it does not matter for the present work as what we need is the implication $\Rightarrow$, not (simplified) exponential itself, and well-opened games are closed under implication <cit.>.

Because simplified exponential $\hat{\oc}$ dispenses with the `tags' $(\_, i)$ such that $i \in \mathbb{N}$ on exponential $\oc$, we no longer need the universal identification $\simeq_{\mathscr{U}}$ (Definition <ref>) or relevant concepts.
Let us therefore introduce modified, `nonstandard' p-games without the nonempty, saturation or three completenesses axioms:

A nonstandard predicative (np-) game is a set of t-skeletons $\sigma$ such that $\sigma \subseteq \mathscr{J}(\mathscr{M})$.
An np-game is well-opened if so are all its elements (Definition <ref>).

We could instead call np-games generalized p-games since np-games are obtained from p-games by discarding all the axioms.
Nevertheless, we would like to emphasize that np-games are undoubtedly `nonstandard' as they do not have the domain-theoretic structures of game semantics, e.g., an np-game may be the empty set, which motivates the term np-games.

Technically, we discard in Definition <ref> the nonempty axiom on p-games for the modified linear implication $\rightarrowtriangle$ between np-games (Lemma <ref>), and the saturation and the three completenesses axioms since we no longer care for identifications of positions or orders between t-skeletons (n.b., recall that mathematical elegance of our mathematical structures is secondary).

The p-games in Example <ref> are all well-opened np-games.

We apply the notations/conventions for p-games to np-games as well.

Let us next introduce the modified linear implication $\rightarrowtriangle$ between np-games as announced above.
Because np-games are defined in terms of t-skeletons (just like p-games), we define the modified linear implication in terms of t-skeletons as follows:

A family of winning-realizer-wise linear implications (FoWRWLI) between np-games $G$ and $H$ is a family

\begin{equation*}
\phi = (\phi_{(\gamma, e)})_{(\gamma, e) \in \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(G)}
\end{equation*}

of t-skeletons $\phi_{(\gamma, e)} :: \gamma \multimap \mathrm{cod}_\phi(\gamma, e)$ that satisfies

* $\mathrm{cod}_\phi(\gamma, e) \in \mathcal{TS}_{\mathrm{wr}}(H)$;

* $\forall (\gamma, e), (\gamma', e) \in  \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(G), \boldsymbol{s}mn \in \phi_{(\gamma, e)}^{\mathrm{Even}}, \boldsymbol{s}mn' \in \phi_{(\gamma', e)}^{\mathrm{Even}} . \, \boldsymbol{s}mn = \boldsymbol{s}mn'$;

* There is a natural number $f \in \mathbb{N}$ such that $\mathscr{G}_{\mathrm{PRF}}(f)(e) = \pi^\gamma_\phi(e)$ for all $(\gamma, e) \in \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(G)$, where $\pi^\gamma_\phi : e \mapsto \mathscr{G}_H (\mathrm{cod}_\phi(\gamma, e))$ (called the realizer-map of $\phi$ at $\gamma$).

\begin{equation*}
\Phi_e \circ \mathrm{tsk}_G(e) \in \mathcal{TS}_{\mathrm{wr}}(H)
\end{equation*}

for all $e \in \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(G)$.
We define a function $\pi_\Phi : \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(G) \rightarrow \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(H)$ by

\begin{equation*}
\pi_\Phi(e) : e \in \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(G) \mapsto \mathscr{G}_H(\Phi_e \circ \mathrm{tsk}_G(e)) \in \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(H).
\end{equation*}

Given an np-game $K$ and an FoWRWLI $\psi$ between $H$ and $K$, the composition of $\phi$ and $\psi$ is the FoWRWLI $\psi \circ \phi$ between $G$ and $K$ defined by

(ψ∘ϕ)_(γ, e) ψ_(cod_ϕ(γ, e), π_ϕ^γ(e)) ∘ϕ_(γ, e)   ((γ, e) ∈ℛ^cp_wr(G)).

We write $\mathscr{F_{\mathrm{wrw}}}(G, H)$ for the set of all FoWRWLIs between $G$ and $H$.

Each realizer-map $\pi^\gamma_\phi$ is not required to be recursive (or there is $f \in \mathbb{N}$ such that $\mathscr{G}_{\mathrm{PRF}}(f)(n) \simeq \pi_\phi^\gamma(n)$ for all $n \in \mathbb{N}$) since otherwise we could not validate CT (again due to the computational hardness of the set of all total recursive functions), as we shall see shortly.
Nevertheless, even in such a weakened sense, the `effectivity' of realizer-maps is necessary for recursive DoWRWLIs (Definition <ref>) to be closed under composition (the second clause of Lemma <ref>).
Note also that the realizer-map $\pi_\phi^\gamma$ does not actually depend on the t-skeleton $\gamma \in \pi_1(\mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(G))$.

We henceforth omit the superscript $(\_)^\gamma$ on realizer-maps $\pi_\phi^\gamma$.
We write $\emptyset$ for the empty FoWRWLI, and $\{ \varphi \}$ for a singleton FoWRWLI of a t-skeleton $\varphi$.

FoWRWLIs are similar to FoPLIs (Definition <ref>) because they are both certain families of t-skeletons.
However, there are crucial differences between them.
First, FoWRWLIs are indexed by canonical realizers for realizable, winning t-skeletons, while FoPLIs by (unrestricted) t-skeletons.

Second, each component of an FoWRWLI may depend on the indexing realizer, but it is not the case for an FoPLI.
These two features of FoWRWLIs implement our idea for validating CT as we shall see.

Next, the second axiom on FoWRWLIs prohibits their components from depending on the indexing t-skeletons, which is crucial for the first clause of Lemma <ref>.

On the other hand, the components may depend on the indexing realizers, which will play a crucial role for our validation of CT, as we shall see.
However, it prohibits us from taking the union on an FoWRWLI since such a union may not be a well-defined t-skeleton.
Specifically, the union may be nondeterministic (Definition <ref>).

Therefore, we instead take the disjoint union of each FoWRWLI:

A disjoint union of winning-realizer-wise linear implications (DoWRWLI) between np-games $G$ and $H$ is the t-skeleton

\begin{equation*}
\uplus \phi \colonequals \begin{cases} \top \, (= \{ \boldsymbol{\epsilon} \}) & \text{if $\phi = \emptyset$;} \\ \bigcup_{(\gamma, e) \in \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(G)} \phi_{(\gamma, e)}^{[e]} &\text{otherwise,} \end{cases}
\end{equation*}

for an FoWRWLI $\phi$ between $G$ and $H$, where

\begin{equation*}
\phi_{(\gamma, e)}^{[e]} \colonequals \{ \, (\boldsymbol{s}(1), e) . (\boldsymbol{s}(2), e) \dots (\boldsymbol{s}(|\boldsymbol{s}|), e) \mid \boldsymbol{s} \in \phi_{(\gamma, e)} \, \},
\end{equation*}

and the `tags' $(\_, e)$ are implemented within the formalization of standard moves.

Given an np-game $K$ and a DoWRWLI $\uplus \psi$ between $H$ and $K$, the composition of $\uplus \phi$ and $\uplus \psi$ is the DoWRWLI $\uplus \psi \circ \uplus \phi$ between $G$ and $K$ defined by

\begin{equation*}
\uplus \psi \circ \uplus \phi \colonequals \uplus (\psi \circ \phi).
\end{equation*}

Alternatively, a DoWRWLI $\uplus \phi$ between np-games $G$ and $H$ can be defined by $\uplus \phi \colonequals \top$ if $\phi = \emptyset$, and $\uplus \phi \colonequals \bigcup_{e \in \pi_2(\mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(G))} \phi_{e}^{[e]}$, where $\phi_e \colonequals \bigcup_{(\gamma, e) \in \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(G)} \phi_{(\gamma, e)}$, otherwise.
This point on DoWRWLIs, which are morphisms in our category, justifies the simplification of the semantics of pi-types made in Section <ref>, as we shall see.

Henceforth, we shall frequently reason about DoWRWLIs, for which we need case analyses accordingly to how DoWRWLIs are defined.
It is, however, mostly rather trivial to handle the first case (i.e., when the underlying FoWRWLI $\phi$ of a given DoWRWLI $\uplus \phi$ is empty), and so we shall often skip it.

The rank $\mathrm{rank}(G)$ of each np-game $G$ is undefined or a natural number defined by

\begin{equation*}
\mathrm{rank}(G) \colonequals \begin{cases} 0 &\text{if $\sigma \subseteq \mathscr{J}(\mathscr{M})$ for all $\sigma \in G$;} \\ \mathrm{max}(\mathrm{rank}(D), \mathrm{rank}(C)) + 1 &\text{if $G = \{ \, \uplus \phi \mid \phi \in \mathscr{F_{\mathrm{wrw}}}(D, C) \, \}$;} \\ \uparrow &\text{otherwise.} \end{cases}
\end{equation*}

A winning-realizer-wise (w.r.w.) realizer for a t-skeleton $\phi$ on an np-game $G$ is

* A realizer $e \in \mathbb{N}$ for $\phi$ (Definition <ref>) if $\mathrm{rank}(G) = 0$;

* A family $f = (f_\gamma)_{(\gamma, e) \in \mathscr{R}_{\mathrm{wr}}^{\mathrm{cp}}(D)}$ of natural numbers $f_\gamma \in \mathbb{N}$ such that the partial map $\mathscr{G}_{\mathrm{PRF}}(f_\gamma)(\langle e, \_ \rangle) : \mathbb{N} \rightharpoonup \mathbb{N}$ is a w.r.w. realizer for $\phi_{(\gamma, e)}$ if  $\mathrm{rank}(G) > 0$.

Let $G$, $H$ and $K$ be np-games.

* Any DoWRWLI between $G$ and $H$ is a t-skeleton contained in $\mathscr{J}(\mathscr{M})$;

* DoWRWLIs (resp. winning, recursive ones) are closed under composition.

For the first clause, it suffices to remark that each DoWRWLI is deterministic thanks to the second axiom on FoWRWLIs.

For the second clause, note that each DoWRWLI uniquely determines the underlying FoWRWLI so that the composition is well-defined on DoWRWLIs (resp. winning ones).
Finally, the third axiom on FoWRWLIs or `effectivity' of realizer-maps enables us to `effectively' obtain the `intermediate' realizer $\pi_\phi(e)$ on the component $(\psi \circ \phi)_e$ of the composition $\uplus \psi \circ \uplus \phi$ of given composable DoWRWLIs $\uplus \phi$ and $\uplus \psi$ so that the composition evidently preserves recursiveness of DoWRWLIs (by the same argument for closure of recursive strategies under composition in <cit.>).

For comparison with DoWRWLIs, let us recall UoPLIs <cit.> between p-games:

A family of pointwise linear implications (FoPLI) between p-games $G$ and $H$ is a family $\varphi = (\varphi_\sigma)_{\sigma :: G}$ of standard t-skeletons $\varphi_\sigma$ that satisfies

* $\forall \sigma :: G . \, \exists \tau :: H . \, \varphi_\sigma :: \sigma \multimap \tau$;

* $\forall \sigma, \tilde{\sigma} :: G, \boldsymbol{s} m n \in \varphi_\sigma^{\mathrm{Even}}, \boldsymbol{s} m \tilde{n} \in \varphi_{\tilde{\sigma}}^{\mathrm{Even}} . \, \boldsymbol{s} m n = \boldsymbol{s} m \tilde{n}$.

We write $\mathscr{F}(G, H)$ for the set of all FoPLIs between $G$ and $H$, and call the union $\bigcup \varphi \colonequals \bigcup_{\sigma :: G}\varphi_\sigma$ the union of PLIs (UoPLI) between $G$ and $H$ (on $\varphi$).

The first axiom on an FoPLI specifies the induced UoPLI in the pointwise fashion.
On the other hand, the second axiom brings UoPLIs determinacy so that they are well-defined t-skeletons.
Moreover, the second axiom gives rise to the computational nature or domain-theoretic structures of game semantics, e.g., thanks to the axiom, the input-output pairs (or extension) of a UoPLI induce continuous functions <cit.>.

Crucially, DoWRWLIs differ from UoPLIs in the following two points:

* O in each DoWRWLI must play on the domain by a winning, recursive t-skeleton and exhibit the canonical realizer for it by the `tag' at his first move, while in each UoPLI O may play by any t-skeleton on the domain and does not have to exhibit anything other than ordinary O-moves during a play;

* A play by a DoWRWLI may depend on the realizer that O supplies, while it is not the case for a play by a UoPLI due to its second axiom.

Consequently, DoWRWLIs implement our idea on how to validate CT, which is described in Section <ref>, while UoPLIs cannot.

Next, recall that the previous work <cit.> defines the linear implication $G \multimap H$ between p-games $G$ and $H$ by $G \multimap H \colonequals \{ \, \bigcup \Phi \mid \Phi \in \mathscr{F}(G, H) \, \}$.
Similarly, we define our modified linear implication $\rightarrowtriangle$ between np-games by

The winning-realizer-wise (w.r.w.) linear implication between np-games $G$ and $H$ is the np-game

G H {   ⊎ϕ|ϕ∈ℱ_wrw(G, H)   }.

Note that $G \rightarrowtriangle H = \emptyset$ if $\mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(G) \neq \emptyset$ and $\mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(H) = \emptyset$.
It is why we allow an np-game to be the empty set (Definition <ref>).

Let us assume that the canonical realizers $f \in \mathscr{R}_{\mathrm{wr}}^{\mathrm{cp}}(G \rightarrowtriangle H)$ for t-skeletons $\uplus \phi :: G \rightarrowtriangle H$ between all np-games $G$ and $H$ are chosen in such a way that $\mathscr{G}_{\mathrm{PRF}}(f)(\langle \langle e, \pi_\phi(e) \rangle, \_ \rangle) : \mathbb{N} \rightarrow \mathbb{N}$ for each $e \in \mathscr{R}_{\mathrm{wr}}^{\mathrm{cp}}(G)$ partially decides $\phi_e$.

In Definition <ref>, `tags' for DoWRWLIs are given by standard moves, and so we may simply apply realizability of t-skeletons to DoWRWLIs.
However, because the set of all total recursive functions $\mathbb{N} \rightarrow \mathbb{N}$ is not recursively enumerable <cit.>, we could not model MLTT plus CT  if we focus on recursive DoWRWLIs.
Hence, we shall impose weakened realizability, called realizer-wise-realizability, on DoWRWLIs and based on it validate CT constructively in Section <ref>.

Np-games are closed under w.r.w. linear implication $\rightarrowtriangle$.

Immediate from the first clause of Lemma <ref>.

On the other hand, p-games are not closed under w.r.w. linear implication $\rightarrowtriangle$.
To see this point, note that the `tags' for DoWRWLIs are embedded into standard moves, and thus certain forms of standard moves determine O's play on the domain of a DoWRWLI.
Consequently, p-games are not closed under w.r.w. linear implication since it does not preserve saturation of positions.
For instance, consider the w.r.w. linear implication $\oc (\oc N \rightarrowtriangle N) \rightarrowtriangle N$, where $N$ and $\oc N$ are the natural number game and its exponential (Section <ref>) regarded as p-games.
A play in it looks like

$\oc (\oc N$     $\rightarrowtriangle$     $N)$     $\rightarrowtriangle$     $N$
$q_{\oc (\oc N \rightarrowtriangle N) \rightarrowtriangle N}$

$\uplus \phi$

chigher01 $q^{[e]}$ chigher09

chigher02 $(q, j)^{[e'], [e]}$ dhigher01

chigher03 $((q, i), j)^{[e'], [e]}$ dhigher02

dhigher03 $((n, i), j)^{[e'], [e]}$

dhigher04 $(m, j)^{[e'], [e]}$

chigher08 $(q, j')^{[e'], [e]}$ dhigher05

chigher07 $((q, i'), j')^{[e'], [e]}$ dhigher06

dhigher07 $((n', i'), j')^{[e'], [e]}$

dhigher08 $(m', j')^{[e'], [e]}$

$l^{[e]}$ dhigher09

[overlay, remember picture, yshift=.25]
[->] (pic cs:dhigher01) to (pic cs:chigher01);
[->] (pic cs:dhigher02) to (pic cs:chigher02);
[->] (pic cs:dhigher03) [bend left] to (pic cs:chigher03);
[->] (pic cs:dhigher04) [bend left] to (pic cs:chigher02);
[->] (pic cs:dhigher05) to (pic cs:chigher01);
[->] (pic cs:dhigher06) to (pic cs:chigher08);
[->] (pic cs:dhigher07) [bend left] to (pic cs:chigher07);
[->] (pic cs:dhigher08) [bend left] to (pic cs:chigher08);
[->] (pic cs:dhigher09) [bend right] to (pic cs:chigher09);

Because $e$ realizes O's play on the domain $\oc N \rightarrowtriangle N$, his choice $i \in \mathbb{N}$ is determined by $e$, where the `tag' $(\_)^{[e]}$ constitutes the moves in the diagram.
It then follows that the set $P_{\oc (\oc N \rightarrowtriangle N) \rightarrowtriangle N}$ is not saturated (as $i$ does not range over all natural numbers unless we change $e$), showing that $\oc (\oc N \rightarrowtriangle N) \rightarrowtriangle N$ is not a p-game.

We circumvent this problem by discarding identifications and the saturation axiom on p-games, and then adopting np-games and simplified exponential $\hat{\oc}$ on them:

The simplified exponential of an np-game $G$ is the np-game $\hat{\oc} G \colonequals \{ \, \hat{\oc} \sigma \mid \sigma :: G \, \}$.

We adopt the notations for exponential $\oc$ on games given at the end of Section <ref> also for simplified exponential $\hat{\oc}$ on np-games in the evident way.
It in particular implies that $\hat{\oc} \sigma = \sigma^\dagger :: \hat{\oc} G$ holds for any np-game $G$ and t-skeleton $\sigma :: G$.

The previous work <cit.> necessitates the countably infinite tensor on t-skeletons $(\sigma_i)_{i \in \mathbb{N}}$ for exponential $\oc$ on p-games in order to systematically accommodate non-innocent t-skeletons on exponentials.

In contrast, we shall use simplified exponential $\hat{\oc}$ on np-games exclusively on the domains of w.r.w. linear implications, where O must play by innocent t-skeletons which are all promotions.
Hence, it suffices to define simplified exponential on np-games as above.

Let us proceed to define other constructions on np-games:

The winning-realizer-wise (w.r.w.) implication between np-games $G$ and $H$ is the np-game $\hat{\oc} G \rightarrowtriangle H$.

The product of np-games $G$ and $H$ is the np-game $G \mathbin{\&} H \colonequals \{ \langle \sigma, \tau \rangle \mid \sigma ::, \tau :: H \, \}$.

Recall once again that McCusker <cit.> has to focus on well-opened games for the use of simplified exponential $\hat{\oc}$ on games.
For the same reason, we shall henceforth focus on well-opened np-games, which the following theorem supports:

Np-games (resp. well-opened ones) are closed under product and w.r.w. implication.

Closure of np-games (resp. well-opened ones) under product is obvious, and that under implication follows immediately from Lemma <ref>.

At this point, we can sketch how we shall validate CT as follows.
Consider the np-game $\hat{\oc} (\hat{\oc} N \rightarrowtriangle N) \rightarrowtriangle N$, which interprets the type $\mathsf{(N \Rightarrow N) \Rightarrow N}$.
We then define a t-skeleton $\uplus \mathrm{ctl} : \hat{\oc} (\hat{\oc} N \rightarrowtriangle N) \rightarrowtriangle N$ that plays as in the following diagram:

$\hat{\oc} (\hat{\oc} N$     $\rightarrowtriangle$     $N)$     $\stackrel{\uplus \mathrm{ctl}}{\rightarrowtriangle}$     $N$
$q_{\hat{\oc} (\hat{\oc} N \rightarrowtriangle N) \rightarrowtriangle N}$

$\uplus \mathrm{ctl}$

cmultimap1 $q^{[e]}$ cmultimap3000

$(e^\ddagger)^{[e]}$ dmultimap3000

[overlay, remember picture, yshift=.25]
[->] (pic cs:dmultimap3000) [bend right] to (pic cs:cmultimap3000);

Note that O must perform the first move $q^{[e]}$ in $\hat{\oc} (\hat{\oc} N \rightarrowtriangle N) \rightarrowtriangle N$, which specifies the canonical realizer $e \in \pi_2(\mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(\hat{\oc} (\hat{\oc} N \rightarrowtriangle N)))$ for his intended computation on the domain $\hat{\oc} (\hat{\oc} N \rightarrowtriangle N)$.
The computation must be by a winning, recursive t-skeleton on $\hat{\oc} (\hat{\oc} N \rightarrowtriangle N)$.
Then, the t-skeleton $\uplus \mathrm{ctl}$ directs P to `copy-cat' the given realizer $e$ as the P-move $(e^\ddagger)^{[e]}$, where $e^\ddagger$ realizes the winning, recursive t-skeleton on $\hat{\oc} N \rightarrowtriangle N$ that essentially coincides with the one realized by $e$.

In this way, the t-skeleton $\uplus \mathrm{ctl}$ models the nontrivial part of CT (<ref>), which is the main idea of the present work.

Moreover, it is straightforward to see that the t-skeleton $\uplus \mathrm{ctl}$ is recursive so that we may constructively model MLTT plus CT.
Note that the position $q^{[e]} \in \uplus \mathrm{ctl}$ is not even partially decidable since otherwise it would contradict the well-known fact that the set of all total recursive functions is not recursively enumerable; for this point, we have carefully `compromised' our notions of (the `effectivity' of) recursive t-skeletons and realizer-maps, as already remarked, so that $\uplus \mathrm{ctl}$ is recursive.

Also, let us emphasize the point that the t-skeleton $\uplus \mathrm{ctl}$ resolves the dilemma between intensionality and extensionality explained in Section <ref>.
In fact, O must exhibit the canonical realizer for his winning, recursive t-skeleton on the domain on the nose at his first move in a play in $\uplus\mathrm{ctl}$, which is very intensional like realizability à la Kleene, while $\uplus\mathrm{ctl}$ itself is just as abstract as morphisms in the game semantics <cit.> or realizability à la assemblies, i.e., extensional enough to model MLTT.

The rest of this article is dedicated to verifying this solution in detail.
Towards this end, we first modify constructions on t-skeletons on linear implication $\multimap$ <cit.> into appropriate ones on w.r.w. linear implication $\rightarrowtriangle$:

The winning-realizer-wise (w.r.w.) copy-cat on an np-game $G$ is the DoWRWLI $\uplus \mathrm{cp}_G :: G \rightarrowtriangle G$ whose component $(\mathrm{cp}_G)_{(\gamma, e)}$ for each $(\gamma, e) \in \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(G)$ is given by

\begin{equation*}
(\mathrm{cp}_G)_{(\gamma, e)} \colonequals \{ \, \boldsymbol{s} \in \gamma^{[0]} \multimap \gamma^{[1]} \mid \forall \boldsymbol{t} \preceq{\boldsymbol{s}}. \ \mathrm{Even}(\boldsymbol{t}) \Rightarrow \boldsymbol{t} \upharpoonright \gamma^{[0]} = \boldsymbol{t} \upharpoonright \gamma^{[1]} \, \},
\end{equation*}

where the superscripts $(\_)^{[i]}$ ($i = 0, 1$) are to distinguish the two copies of $\gamma$.

The winning-realizer-wise (w.r.w.) dereliction on an np-game $G$ is the DoWRWLI $\uplus \mathrm{der}_G :: \hat{\oc} G \rightarrowtriangle G$ whose component $(\mathrm{der}_G)_{(\gamma^\dagger, e')}$ for each $(\gamma^\dagger, e') \in \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(\hat{\oc} G)$ is given by

\begin{equation*}
(\mathrm{der}_G)_{(\gamma^\dagger, e')} \colonequals \{ \, \boldsymbol{s} \in \gamma^\dagger \multimap \gamma \mid \forall \boldsymbol{t} \preceq{\boldsymbol{s}}. \ \mathrm{Even}(\boldsymbol{t}) \Rightarrow \boldsymbol{t} \upharpoonright \gamma^\dagger = \boldsymbol{t} \upharpoonright \gamma \, \}.
\end{equation*}

Let $G$ be an np-game.

* The w.r.w. copy-cat $\uplus\mathrm{cp}_G$ is a winning, recursive t-skeleton on the np-game $G \rightarrowtriangle G$, and it is the unit for composition on DoWRWLIs;

* The w.r.w. dereliction $\uplus\mathrm{der}_G$ is a winning, recursive t-skeleton on the np-game $\hat{\oc} G \rightarrowtriangle G$ if $G$ is well-opened.

Similar to the case of copy-cats and derelictions given in <cit.>, where $\uplus\mathrm{cp}_G$ and $\uplus\mathrm{der}_G$ are clearly recursive, and they are the trivial t-skeleton $\top$ if $\mathscr{R}_{\mathrm{wr}}^{\mathrm{cp}}(G) = \emptyset$.

Given np-games $A$, $B$, $C$ and $D$, and DoWRWLIs $\uplus \phi :: A \rightarrowtriangle B$, $\uplus \rho :: A \rightarrowtriangle C$ and $\uplus \varphi :: \hat{\oc} A \rightarrowtriangle B$, we define

* The tensor $\uplus \phi \otimes \uplus \theta \colonequals \uplus (\phi \otimes \theta) :: A \otimes C \rightarrowtriangle B \otimes D$ of $\uplus \phi$ and $\uplus \theta$ by

(ϕ⊗θ)_(γ, e) ϕ_e ↾A ⊗θ_e ↾C
π_ϕ⊗θ(e) 𝒢_B ⊗D(tsk_B ∘π_ϕ(e ↾A) ⊗tsk_D ∘π_θ(e ↾C)) ∈ℛ^cp_wr(B ⊗D)

for each $e \in \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(A \otimes B)$, where

\begin{align*}
e \upharpoonright A &\colonequals \mathscr{G}_{A}(\mathrm{tsk}_{A \otimes C}(e) \upharpoonright A) \in \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(A); \\
e \upharpoonright C &\colonequals \mathscr{G}_{C}(\mathrm{tsk}_{A \otimes C}(e) \upharpoonright C) \in \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(C);
\end{align*}

* The pairing $\langle \uplus \phi, \uplus \rho \rangle \colonequals \uplus \langle \phi, \rho \rangle :: A \rightarrowtriangle B \mathbin{\&} C$ of $\uplus \phi$ and $\uplus \rho$ by

⟨ϕ, ρ⟩_(γ, e) ⟨ϕ_(γ, e), ρ_(γ, e) ⟩

for each $(\gamma, e) \in \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(A)$;

* The promotion $(\uplus \varphi)^\dagger \colonequals \uplus (\varphi^\dagger) :: \hat{\oc} A \rightarrowtriangle \hat{\oc} B$ of $\uplus \varphi$ by

(φ^†)_(γ^†, e') (φ_(γ^†, e'))^†

for each $(\gamma^\dagger, e') \in \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(\hat{\oc} A)$ (which allows us to write $\uplus \varphi^\dagger$ for $(\uplus \varphi)^\dagger$),

where we (can and do) assume that the corresponding constructions on realizer-maps are `effective' by an appropriate choice of canonical realizers (Definition <ref>).

We fix canonical realizers since they enable us to concisely define these constructions on DoWRWLIs in such a way that Lemma <ref> below holds.

DoWRWLIs (resp. winning, recursive ones) are closed under pairing and promotion.

Similar to the corresponding constructions on UoPLIs <cit.>, where recursive DoWRWLIs are clearly closed under pairing and promotion.

Let $A$, $B$, $C$ and $D$ be np-games, and $\uplus \phi :: \hat{\oc} A \rightarrowtriangle B$, $\uplus \psi :: \hat{\oc} B \rightarrowtriangle C$ and $\uplus \varphi :: \hat{\oc} C \rightarrowtriangle D$ DoWRWLIs.

* $\uplus \mathrm{der}_A^\dagger = \uplus \mathrm{cp}_{\hat{\oc} A} :: \hat{\oc} A \rightarrowtriangle \hat{\oc} A$ and $\uplus \mathrm{der}_B \circ \uplus \phi^\dagger = \uplus \phi :: \hat{\oc} A \rightarrowtriangle B$;

* $\uplus \varphi \circ (\uplus \psi \circ \uplus \phi^\dagger)^\dagger = (\uplus \varphi \circ \uplus \psi^\dagger) \circ \uplus \phi^\dagger :: \hat{\oc} A \rightarrowtriangle D$.

Similar to the case of UoPLIs <cit.>, where it is crucial for the first and the second clauses to fix a choice of canonical realizers (Definition <ref>).

We are now ready to define:

The category $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ consists of

* Well-opened np-games as objects;

* Winning, recursive t-skeletons on $\hat{\oc} A \rightarrowtriangle B$ as morphisms $A \rightarrow B$;

* The composition $\uplus \psi \bullet \uplus \phi : A \rightarrow C$ of morphisms $\uplus \phi : A \rightarrow B$ and $\uplus \psi : B \rightarrow C$ given by $\uplus \psi \bullet \uplus \phi \colonequals \uplus \psi \circ \uplus \phi^\dagger$;

* W.r.w. derelictions $\uplus \mathrm{der}_A : \hat{\oc} A \rightarrowtriangle A$ as identities $A \rightarrow A$.

The category $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ is well-defined by Lemmata <ref>, <ref>, <ref> and <ref>, and moreover cartesian closed (which is an immediate corollary of the theorem given later that $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ models MLTT equipped with unit-, pi- and sigma-types via a CwF and semantic type formers, and so the following proof is just a sketch):

The category $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ is cartesian closed, where a terminal object, products and exponential objects are given by the unit np-game $\boldsymbol{1}$, product $\&$ and w.r.w. implication $\hat{\oc} (\_) \rightarrowtriangle (\_)$, respectively.

By Theorem <ref> and Lemmata <ref> and <ref>, where note that t-skeletons in $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ are all winning and recursive so that $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ is closed.

Given $G \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$, we write $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(G)$ for the hom-set $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\boldsymbol{1}, G)$.
Hence, each element of $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(G)$ is of the form $\uplus \{ \gamma_0^{\hat{\oc} \boldsymbol{1}} \}$ for some $\gamma_0 \in \mathcal{TS}_{\mathrm{wr}}(G)$ (n.b., $\gamma_0 :: \Gamma$ implies $\gamma_0^{\hat{\oc} \boldsymbol{1}} :: \top^\dagger \rightarrowtriangle \Gamma$); we usually write $\uplus \gamma$ for it (i.e., $\gamma = \{ \gamma_0^{\hat{\oc} \boldsymbol{1}} \}$).

Just for convenience, we also write $\mathbb{NPG}_{\mathrm{wrw}}(H)$ for the set of all winning, recursive t-skeletons on $\hat{\oc} \boldsymbol{1} \rightarrowtriangle H$ for any (not necessarily well-opened) np-game $H$.

Similarly to the game semantics of simple type theories and the game semantics of MLTT <cit.>, the w.r.w. implications $\hat{\oc} (A \mathbin{\&} B) \rightarrowtriangle C$ and $\hat{\oc} A \rightarrowtriangle (\hat{\oc} B \rightarrowtriangle C)$ coincide up to `tags' on moves for any np-games $A$, $B$ and $C$ (n.b., t-skeletons on the w.r.w. implications are only the trivial one $\top$ if $\mathscr{R}_{\mathrm{wr}}^{\mathrm{cp}}(A) = \emptyset$ or $\mathscr{R}_{\mathrm{wr}}^{\mathrm{cp}}(B) = \emptyset$), and therefore currying is modeled in the category $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$.
In particular, it explains essentially why our model of MLTT in $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ validates the $\xi$-rule, as we shall see shortly.

§.§ Realizability model of intensional Martin-Löf type theory equipped with formal Church's thesis à la game semantics

A winningly realizerwise (w.r.) dependent predicative (p-) game on a predicative game $\Gamma$ is an continuous map $A$ from the algebraic CPO $(\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Gamma), \leqslant_\Gamma)$ to the flat CPO on $\mathsf{ob}(\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}})$ with the least element $\bot$ such that the union $\bigcup_{g \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Gamma)}\vdash_{A(g)}$ is well-founded.

In this section, we lift the CCC $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ to a category with families (CwF) <cit.>, an abstract model of MLTT, equipped with semantic type formers <cit.> for unit-, empty-, N-, pi-, sigma- and Id-types so that $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ is shown to model MLTT together with these types by soundness of the semantics of MLTT in CwFs <cit.>.

Towards this end, let us first introduce our interpretation of (dependent) types:

The CCC $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ is CPO-enriched with respect to the partial order $\leqslant_G$ between t-skeletons on each np-game $G$ defined by

\begin{equation*}
\sigma \leqslant_G \sigma' :\Leftrightarrow \sigma \asymp \sigma' \wedge \sigma \subseteq \sigma'
\end{equation*}

for all $\sigma, \sigma' :: G$, and the CPOs of np-games are algebraic whose compact elements are t-skeletons $\kappa :: G$ such that the set $\lceil \kappa \rceil$ of all its P-views is finite.

As outlined in <cit.>, where the constraint $\sigma \asymp \sigma'$ plays a key role.

A dependent nonstandard predicative (np-) game on an np-game $\Gamma$ is a family

\begin{equation*}
A = (A(\uplus \gamma))_{\uplus \gamma \in \mathbb{NPG}_{\mathrm{wrw}}(\Gamma)}
\end{equation*}

of np-games $A(\uplus \gamma)$ such that the union $\bigcup_{\uplus \gamma \in \mathbb{NPG}_{\mathrm{wrw}}(\Gamma)} \mathbin{\vdash_{A(\uplus \gamma)}}$ is well-founded.

A dependent np-game is well-opened if so are all its components.
We write $\mathscr{D}\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Gamma)$ for the set of all well-opened dependent np-games on $\Gamma$.

Every dependent np-game $A$ is required to be continuous similarly to the domain-theoretic interpretation of (partial) MLTT <cit.>.
The continuity is conceptually natural particularly if we think of universes though we do not interpret them in this article.
On the other hand, at least its monotonicity is necessary for Theorem <ref>.

Unlike the game semantics of MLTT <cit.>, the indexing t-skeletons of a dependent np-game $A$ on an np-game $\Gamma$ are on $\Gamma$, not $\hat{\oc} \Gamma$, but it does not lose any generality for our interpretation since the domain and the codomain t-skeletons of DoWRWLIs are all innocent so that we may assume that those on $\hat{\oc} \Gamma$ are all promotions.

Let us then generalize w.r.w. implication (Definition <ref>) in such a way that it captures type dependency of pi-types (Definition <ref>):

The integration of a dependent np-game $A$ on an np-game $\Gamma$ is the np-game

∫_ΓA ⋃_⊎γ∈ℕℙ𝔾_wrw(Γ)A(⊎γ)   (n.b., we often abbreviate $\int_\Gamma$ as $\int$).

The integration on dependent np-games is simpler than the corresponding one on p-games in the previous work <cit.> as ours does not have to be det-j complete.

Given a dependent np-game $A$ on a well-opened np-game $\Gamma$, the integration $\int_\Gamma A$ is a well-opened np-game.

It suffices to remark that $\int_\Gamma A$ is det-j complete by the operation $\mathrm{DetJ}$.

A family of dependently winning-realizer-wise linear implications (FoDWRWLI) from an np-game $\Gamma$ to a dependent np-game $A$ on $\Gamma$ is an FoWRWLI $\phi$ from $\Gamma$ to $\int_\Gamma A$ that satisfies

\begin{equation*}
\forall (\gamma, e) \in \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(\Gamma) . \, \mathrm{cod}_\phi(\gamma, e) :: A(\uplus \{ \gamma^{\hat{\oc} \boldsymbol{1}} \}) \quad \text{(n.b., $\gamma :: \Gamma$ implies $\gamma^{\hat{\oc} \boldsymbol{1}} :: \top^\dagger \rightarrowtriangle \Gamma$)}.
\end{equation*}

We write $\mathscr{F_{\mathrm{wrw}}}(\Gamma, A)$ for the set of all FoDWRWLIs from $\Gamma$ to $A$.

Note that the axiom on an FoDWRWLI $\phi$ from $\Gamma$ to $A$ is equivalent to

\begin{equation*}
\forall \, \mathbin{\uplus \gamma} \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Gamma) . \, \phi_{\pi_\gamma \circ \mathscr{G}_{\boldsymbol{1}}(\top)} \circ \gamma_\top :: \top \multimap A(\uplus \gamma).
\end{equation*}

The winning-realizer-wise (w.r.w.) linear-pi from an np-game $\Gamma$ to a dependent np-game $A$ on $\Gamma$ is the np-game

\begin{equation*}
\ell\Pi_{\mathrm{wrw}}(\Gamma, A) \colonequals \{ \, \uplus \phi \mid \phi \in \mathscr{F}_{\mathrm{wrw}}(\Gamma, A) \,  \},
\end{equation*}

and the winning-realizer-wise (w.r.w.) pi from $\Gamma$ to $A$ is the np-game

\begin{equation*}
\Pi_{\mathrm{wrw}}(\Gamma, A) \colonequals \ell\Pi_{\mathrm{wrw}}(\hat{\oc} \Gamma, A^\ddagger),
\end{equation*}

where $A^\ddagger$ is the dependent np-game on $\hat{\oc} \Gamma$ defined by $A^\ddagger(\uplus \gamma^\dagger) \colonequals A(\uplus \gamma)$ for each $\uplus \gamma^\dagger \in \mathbb{NPG}_{\mathrm{wrw}}(\hat{\oc} \Gamma)$.

The w.r.w. linear-pi $\ell\Pi_{\mathrm{wrw}}(\Gamma, A)$ and the w.r.w. pi $\Pi_{\mathrm{wrw}}(\Gamma, A)$ are (well-opened) np-games for any np-game $\Gamma$ and (well-opened) dependent np-game $A$ on $\Gamma$.

Immediate from Lemma <ref> and Theorem <ref>.

Let us similarly define the w.r.w. variant of sigma:

The winning-realizer-wise (w.r.w.) sigma of an np-game $\Gamma$ and a dependent np-game $A$ on $\Gamma$ is the np-game

\begin{equation*}
\Sigma_{\mathrm{wrw}}(\Gamma, A) \colonequals \{ \langle \gamma, \alpha \rangle :: \Gamma \mathbin{\&} \int_\Gamma A \mid \gamma \in \mathcal{TS}_{\mathrm{wr}}(\Gamma) \Rightarrow \alpha :: A (\uplus \{ \gamma^{\hat{\oc} \boldsymbol{1}} \}) \, \}.
\end{equation*}

The w.r.w. sigma $\Sigma_{\mathrm{wrw}}(\Gamma, A)$ is a (well-opened) np-game for any (well-opened) np-game $\Gamma$ and (well-opened) dependent np-game $A$ on $\Gamma$.

Immediate from Theorem <ref>.

Finally, let us introduce our interpretation of Id-types:

Given an np-game $\Gamma$ and t-skeletons $\gamma, \gamma' :: \Gamma$, the identity (Id) between $\gamma$ and $\gamma'$ is the np-game

\begin{equation*}
\mathrm{Id}_\Gamma(\gamma, \gamma') \colonequals \begin{cases} \boldsymbol{1} &\text{if $\gamma = \gamma'$;} \\ \boldsymbol{0} &\text{otherwise.} \end{cases}
\end{equation*}

Given an np-game $\Gamma$, the Id $\mathrm{Id}_\Gamma(\gamma, \gamma')$ between any $\gamma, \gamma' :: \Gamma$ is a well-opened np-game.

We are now ready to lift the CCC $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ to a CwF.
Let us first recall the general definition of CwFs <cit.>, where our presentation is based on <cit.>:

A category with families (CwF) is a tuple $\mathcal{C} = (\mathcal{C}, \mathrm{Ty}, \mathrm{Tm}, \_\{\_\}, T, \_.\_, \mathrm{p}, \mathrm{v}, \langle\_,\_\rangle_\_)$,

* $\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)$, called the set of all 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)$, called the set of all terms of type $A$ in the context $\Gamma$;

* To each $f : \Delta \to \Gamma$ in $\mathcal{C}$, $\_\{\_\}$ assigns a map $\_\{f\} : \mathrm{Ty}(\Gamma) \to \mathrm{Ty}(\Delta)$, called the substitution on types, and a family $(\_\{f\}_A)_{A \in \mathrm{Ty}(\Gamma)}$ of maps $\_\{f\}_A : \mathrm{Tm}(\Gamma, A) \to \mathrm{Tm}(\Delta, A\{f\})$, 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$ in $\mathcal{C}$ (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 $(f, A, g)$ of a morphism $f : \Delta \to \Gamma$ in $\mathcal{C}$, a type $A \in \mathrm{Ty}(\Gamma)$ and a term $g \in \mathrm{Tm}(\Delta, A\{f\})$, a morphism $\langle f, g \rangle_A : \Delta \to \Gamma . A$
in $\mathcal{C}$, called the extension of $f$ by $g$

that satisfies

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

* (Ty-Comp) $A \{ f \circ e \} = A \{ f \} \{ e \}$;

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

* (Tm-Comp) $h \{ f \circ e \}_A = h \{ f \}_A \{ e \}_{A\{f\}}$;

* (Cons-L) $\mathrm{p}(A) \circ \langle f, g \rangle_A = f$;

* (Cons-R) $\mathrm{v}_A \{ \langle f, g \rangle_A \} = g$;

* (Cons-Nat) $\langle f, g \rangle_A \circ e = \langle f \circ e, g \{ e \}_{A\{f\}} \rangle_A$;

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

for any $\Gamma, \Delta, \Theta \in \mathcal{C}$, $A \in \mathrm{Ty}(\Gamma)$, $f : \Delta \to \Gamma$, $e : \Theta \to \Delta$, $h \in \mathrm{Tm}(\Gamma, A)$ and $g \in \mathrm{Tm}(\Delta, A\{ f \})$.

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

\begin{align*}
\mathsf{\vdash \Gamma \ ctx} &\mapsto \llbracket \mathsf{\Gamma} \rrbracket \in \mathcal{C}; \\
\mathsf{\Gamma \vdash A \ type} &\mapsto \llbracket \mathsf{A} \rrbracket \in \mathrm{Ty}(\llbracket \mathsf{\Gamma} \rrbracket); \\
\mathsf{\Gamma \vdash a : A} &\mapsto \llbracket \mathsf{a} \rrbracket \in \mathrm{Tm}(\llbracket \mathsf{\Gamma} \rrbracket, \llbracket \mathsf{A} \rrbracket); \\
\mathsf{\vdash \Gamma = \Delta \ ctx} &\Rightarrow \llbracket \mathsf{\Gamma} \rrbracket = \llbracket \mathsf{\Delta} \rrbracket \in \mathcal{C}; \\
\mathsf{\Gamma \vdash A = B \ type} &\Rightarrow \llbracket \mathsf{A} \rrbracket = \llbracket \mathsf{B} \rrbracket \in \mathrm{Ty}(\llbracket \mathsf{\Gamma} \rrbracket); \\
\mathsf{\Gamma \vdash a = a' : A} &\Rightarrow \llbracket \mathsf{a} \rrbracket = \llbracket \mathsf{a'} \rrbracket \in \mathrm{Tm}(\llbracket \mathsf{\Gamma} \rrbracket, \llbracket \mathsf{A} \rrbracket),
\end{align*}

where $\llbracket \_ \rrbracket$ denotes the semantic map or interpretation <cit.>.
Strictly speaking, the first three maps define an interpretation $\llbracket \_ \rrbracket$ of MLTT in $\mathcal{C}$, while the last three logical implications are soundness of the interpretation $\llbracket \_ \rrbracket$.
See <cit.> for the details.

An interpretation $\llbracket \_ \rrbracket$ is applied to judgements, and thus $\llbracket \mathsf{\Gamma} \rrbracket$, $\llbracket \mathsf{A} \rrbracket$ and $\llbracket \mathsf{a} \rrbracket$ should be written, strictly speaking, as $\llbracket \mathsf{\vdash \Gamma \ ctx} \rrbracket$, $\llbracket \mathsf{\Gamma \vdash A \ type} \rrbracket$ and $\llbracket \mathsf{\Gamma \vdash a : A} \rrbracket$, respectively.
For brevity, however, we usually adopt the abbreviation whenever it does not bring any serious confusion.

Let us now turn to introducing our CwF of realizability à la game semantics:

The CwF $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ is the tuple $(\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}, \mathrm{Ty}, \mathrm{Tm}, \_\{\_\}, \boldsymbol{1}, \_.\_, \mathrm{p}, \mathrm{v}, \langle\_,\_\rangle_\_)$,

* The category $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ is the one defined in Definition <ref>, and $\boldsymbol{1} \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ is the unit np-game (Example <ref>);

* Given $\Gamma \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ and $A \in \mathscr{D}\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Gamma)$, we define $\mathrm{Ty}(\Gamma) \colonequals \mathscr{D}\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Gamma)$ and $\mathrm{Tm}(\Gamma, A) \colonequals \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Gamma, A))$;

* Given $\uplus \phi : \Delta \rightarrow \Gamma$ in $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$, we define the map $\_\{\uplus \phi\} : \mathrm{Ty}(\Gamma) \to \mathrm{Ty}(\Delta)$ by

\begin{equation*}
A \{ \uplus \phi \} \colonequals (A(\uplus \phi \bullet \uplus \delta))_{\uplus \delta \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Delta)} \quad (A \in \mathrm{Ty}(\Gamma)),
\end{equation*}

and the map $\_\{\uplus \phi\}_A : \mathrm{Tm}(\Gamma, A) \to \mathrm{Tm}(\Delta, A\{\uplus \phi\})$ by

\begin{equation*}
\uplus \alpha \{ \uplus \phi \}_A \colonequals \uplus \alpha \bullet \uplus \phi \quad (\uplus \alpha \in \mathrm{Tm}(\Gamma, A));
\end{equation*}

* The comprehension $\Gamma.A$ is given by $\Gamma.A \colonequals \Sigma_{\mathrm{wrw}} (\Gamma, A)$, the first projection $\mathrm{p}(A) \colonequals \mathrm{fst}_{\Sigma_{\mathrm{wrw}}(\Gamma, A)} : \Sigma_{\mathrm{wrw}} (\Gamma, A) \to \Gamma$ is the w.r.w. dereliction $\uplus \mathrm{der}_\Gamma$ up to `tags,' the second projection $\mathrm{v}_A \colonequals \mathrm{snd}_{\Sigma_{\mathrm{wrw}}(\Gamma, A)} \in \mathrm{Tm}(\Sigma_{\mathrm{wrw}}(\Gamma, A), A\{\mathrm{p}(A)\})$ is the w.r.w. dereliction $\uplus \mathrm{der}_{\int_\Gamma A}$ up to `tags,' and the extension $\langle \uplus \phi, \uplus \alpha \rangle_A : \Delta \rightarrow \Sigma_{\mathrm{wrw}} (\Gamma, A)$ is the pairing $\langle \uplus \phi, \uplus \alpha \rangle$ of the DoWRWLIs $\uplus \phi$ and $\uplus \alpha$.

We frequently omit the subscript $(\_)_A$ on $\_\{ \_ \}_A$ and $\langle \_, \_ \rangle_A$, and the one $(\_)_{\Sigma_{\mathrm{wrw}}(\Gamma, A)}$ on $\mathrm{fst}_{\Sigma_{\mathrm{wrw}}(\Gamma, A)}$ and $\mathrm{snd}_{\Sigma_{\mathrm{wrw}}(\Gamma, A)}$.

The structure $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ given in Definition <ref> forms a well-defined CwF.

We focus on substitutions on terms and extensions as other verifications are straightforward.
Let $\Gamma, \Delta \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$, $A \in \mathscr{D}\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Gamma)$, $\uplus \phi \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Delta, \Gamma)$, $\uplus \alpha \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Gamma, A))$ and $\uplus \tilde{\alpha} \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Delta, A\{ \uplus \phi \}))$, and assume that $\mathscr{R}_{\mathrm{wr}}^{\mathrm{cp}}(\Gamma) \neq \emptyset$ and $\mathscr{R}_{\mathrm{wr}}^{\mathrm{cp}}(\Delta) \neq \emptyset$, following our convention, since the other cases are trivial.

By Lemma <ref>, $\uplus \alpha \{ \uplus \phi \} = \uplus \alpha \bullet \uplus \phi$ is a winning, recursive t-skeleton on $\hat{\oc} \Delta \rightarrowtriangle \int_\Gamma A$.
Take any $\uplus \delta \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Delta)$; for proving $\uplus \alpha \{ \uplus \phi \} \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Delta, A\{ \uplus \phi \}))$, it remains to show $(\uplus \alpha \bullet \uplus \phi) \bullet \uplus \delta :: \oc \boldsymbol{1} \rightarrowtriangle A\{ \uplus \phi \}(\uplus \delta)$.
Then, we calculate

\begin{align*}
(\uplus \alpha \bullet \uplus \phi) \bullet \uplus \delta &= (\uplus \alpha \circ \uplus \phi^\dagger) \circ \uplus \delta^\dagger \\
&= \uplus \alpha \circ (\uplus \phi \circ \uplus \delta^\dagger)^\dagger \quad \text{(by Lemma~\ref{LemWRWPromotionLemma})} \\
&= \uplus \alpha \circ (\uplus \phi \bullet \uplus \delta)^\dagger :: \oc \boldsymbol{1} \rightarrowtriangle A^\ddagger((\uplus \phi \bullet \uplus \delta)^\dagger),
\end{align*}

\begin{align*}
A^\ddagger((\uplus \phi \bullet \uplus \delta)^\dagger) &= A(\uplus \phi \bullet \uplus \delta) \\
&= A\{ \uplus \phi \}(\uplus \delta).
\end{align*}

Hence, we have shown that $\uplus \alpha \{ \uplus \phi \} \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Delta, A\{ \uplus \phi \}))$ holds.

Similarly, the extension $\langle \uplus \phi, \uplus \tilde{\alpha} \rangle$ is a winning, recursive t-skeleton on $\hat{\oc} \Delta \rightarrowtriangle \Gamma \mathbin{\&} (\int_\Gamma A)$ by Lemma <ref>.
Hence, for proving $\langle \uplus \phi, \uplus \tilde{\alpha} \rangle \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Delta, \Sigma_{\mathrm{wrw}}(\Gamma, A))$, it suffices to show $\uplus \tilde{\alpha} \bullet \uplus \delta :: \oc \boldsymbol{1} \rightarrowtriangle A(\uplus \phi \bullet \uplus \delta)$ since we have $\langle \uplus \phi, \uplus \tilde{\alpha} \rangle \bullet \uplus \delta = \langle \uplus \phi \bullet \uplus \delta, \uplus \tilde{\alpha} \bullet \uplus \delta \rangle$ with $\uplus \phi \bullet \uplus \delta$ winning and recursive.
Then, we calculate

\begin{equation*}
\uplus \tilde{\alpha} \bullet \uplus \delta :: \oc \boldsymbol{1} \rightarrowtriangle A\{ \uplus \phi \}(\uplus \delta) = \oc \boldsymbol{1} \rightarrowtriangle A(\uplus \phi \bullet \uplus \delta).
\end{equation*}

Finally, let us verify the required equations:

* (Ty-Id) $A\{\mathrm{id}_\Gamma\} = (A(\uplus \mathrm{der}_\Gamma \bullet \uplus \gamma))_{\uplus \gamma \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Gamma)} = (A(\uplus \gamma))_{\uplus \gamma \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Gamma)} = A$ by Lemma <ref>;

* (Ty-Comp) Given $\Theta \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ and $\uplus \psi : \Gamma \rightarrow \Theta$ in $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$, we calculate

\begin{align*}
A\{ \uplus \psi \bullet \uplus \phi \} &= (A((\uplus \psi \bullet \uplus \phi) \bullet \uplus \delta))_{\uplus \delta \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Delta)} \\
%&= (A((g \circ f^\dagger) \circ d^\dagger))_{d \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\oc \Delta)} \\
%&= (A(g \circ (f \circ d^\dagger)^\dagger))_{d \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\oc \Delta)} \quad \text{(by Lemma~\ref{LemWRWPromotionLemma})} \\
&= (A(\uplus \psi \bullet (\uplus \phi \bullet \uplus \delta)))_{\uplus \delta \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Delta)} \quad \text{(by Lemma~\ref{LemWRWPromotionLemma})} \\
&= (A \{ \uplus \psi \} (\uplus \phi \bullet \uplus \delta))_{\uplus \delta \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Delta)} \\
&= (A \{ \uplus \psi \} \{ \uplus \phi \} (\uplus \delta))_{\uplus \delta \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Delta)} \\
&= A \{ \uplus \psi \} \{ \uplus \phi \};
\end{align*}

* (Tm-Id) $\uplus \alpha \{ \mathrm{id}_\Gamma \} = \uplus \alpha \bullet \uplus \mathrm{der}_\Gamma = \uplus \alpha \circ \uplus \mathrm{cp}_{\hat{\oc} \Gamma} = \uplus \alpha$ by Lemmata <ref> and <ref>;

* (Tm-Comp) $\uplus \alpha \{ \uplus \psi \bullet \uplus \phi \} = \uplus \alpha \bullet (\uplus \psi \bullet \uplus \phi) = (\uplus \alpha \bullet \uplus \psi) \bullet \uplus \phi = \uplus \alpha \{ \uplus \psi \} \bullet \uplus \phi = \uplus \alpha \{ \uplus \psi \} \{ \uplus \phi \}$ by Lemma <ref>;

* (Cons-L) $\mathrm{p}(A) \bullet \langle \uplus \psi, \uplus \tilde{\alpha} \rangle = \mathrm{fst} \circ \langle \uplus \psi, \uplus \tilde{\alpha} \rangle^\dagger = \mathrm{fst} \circ \langle \uplus \psi^\dagger, \uplus \tilde{\alpha}^\dagger \rangle = \uplus \psi$;

* (Cons-R) $\mathrm{v}_A \{ \langle \uplus \psi, \uplus \tilde{\alpha} \rangle \} = \mathrm{snd} \circ \langle \uplus \psi, \uplus \tilde{\alpha} \rangle^\dagger = \mathrm{snd} \circ \langle \uplus \psi^\dagger, \uplus \tilde{\alpha}^\dagger \rangle = \uplus \tilde{\alpha}$;

* (Cons-Nat) $\langle \uplus \psi, \uplus \tilde{\alpha} \rangle \bullet \uplus \phi = \langle \uplus \psi \bullet \uplus \phi, \uplus \tilde{\alpha} \bullet \uplus \phi \rangle  = \langle \uplus \psi \bullet \uplus \phi, \uplus \tilde{\alpha} \{ \uplus \phi \} \rangle$;

* (Cons-Id) $\langle \mathrm{p}(A), \mathrm{v}_A \rangle = \langle \mathrm{fst}_{\Sigma_{\mathrm{wrw}}(\Gamma, A)}, \mathrm{snd}_{\Sigma_{\mathrm{wrw}}(\Gamma, A)} \rangle = \uplus \mathrm{der}_{\Sigma_{\mathrm{wrw}}(\Gamma, A)} = \mathrm{id}_{\Gamma . A}$,

which completes the proof.

Let us then proceed to equip the CwF $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ with semantic type formers for unit-, empty-, N-, pi-, sigma- and Id-types.
We begin with pi-types (Appendix <ref>).
Recall first the semantic type former for pi-types in an arbitrary CwF:

A CwF $\mathcal{C}$ supports pi if

* ($\Pi$-Form) Given $\Gamma \in \mathcal{C}$, $A \in \mathrm{Ty}(\Gamma)$ and $B \in \mathrm{Ty}(\Gamma . A)$, there is a type $\Pi (A, B) \in \mathrm{Ty}(\Gamma)$;

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

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

* ($\Pi$-Comp) $\mathrm{App}_{A, B} (\lambda_{A, B} (b) , a) = b \{ \overline{a} \}$;

* ($\Pi$-Subst) Given $\Delta \in \mathcal{C}$ and $f : \Delta \to \Gamma$ in $\mathcal{C}$, $\Pi (A, B) \{ f \} = \Pi (A\{f\}, B\{f^+\})$, where $f^+ \colonequals \langle f \circ \mathrm{p}(A\{ f \}), \mathrm{v}_{A\{ f \}} \rangle_A : \Delta . A\{ f \} \to \Gamma . A$;

* ($\lambda$-Subst) $\lambda_{A, B} (b) \{ f \} = \lambda_{A\{f\}, B\{f^+\}} (b \{ f^+ \}) \in \mathrm{Tm} (\Delta, \Pi (A\{f\}, B\{ f^+\}))$;

* (App-Subst) $\mathrm{App}_{A, B} (k, a) \{ f \} = \mathrm{App}_{A\{f\}, B\{f^+\}} (k \{ f \}, a \{ f \}) \in \mathrm{Tm} (\Delta, B\{ \overline{a} \} \{ f \})$.

Furthermore, $\mathcal{C}$ supports pi in the strict sense if it additionally satisfies

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

Pi-types (with the $\eta$-rule) are modeled in a CwF that supports pi (in the strict sense); see Appendix <ref> for the details.

Let us now show that the CwF $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ supports pi in the strict sense:

Given $\Gamma \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$, $A \in \mathscr{D}\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Gamma)$ and $B \in \mathscr{D}\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Sigma_{\mathrm{wrw}}(\Gamma, A))$, there is a bijection

\begin{equation*}
\lambda_{A, B} : \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, A), B)) \stackrel{\sim}{\rightarrow} \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Gamma, \Pi_{\mathrm{wrw}}(A, B))),
\end{equation*}

where $\Pi_{\mathrm{wrw}}(A, B) \colonequals (\Pi_{\mathrm{wrw}}(A(\uplus \gamma), B_{\uplus \gamma}))_{\uplus \gamma \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Gamma)}$ and $B_{\uplus \gamma} \colonequals (B(\langle \uplus \gamma, \uplus \alpha \rangle)_{\uplus \alpha \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(A(\uplus \gamma))}$.

It suffices to show that there is a bijection between (not necessarily winning or recursive) t-skeletons on $\Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, A), B)$ and those on $\Pi_{\mathrm{wrw}}(\Gamma, \Pi_{\mathrm{wrw}}(A, B))$ up to finitary `tags' since such a bijection preserves winning and recursiveness.

Recall that a t-skeleton $\uplus \phi :: \Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, A), B)$ is the disjoint union on a family $\phi = (\phi_{(\sigma^\dagger, e)})_{(\sigma^\dagger, e) \in \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(\hat{\oc} \Sigma_{\mathrm{wrw}}(\Gamma, A))}$ of t-skeletons $\phi_{(\sigma^\dagger, e)} :: \sigma^\dagger \rightarrowtriangle \mathrm{cod}_\phi(\sigma^\dagger, e)$ such that $\mathrm{cod}_\phi(\sigma^\dagger, e) \in \mathcal{TS}_{\mathrm{wr}}(B(\uplus \{\sigma^{\hat{\oc}\boldsymbol{1}} \}))$, each $\phi_{(\sigma^\dagger, e)}$ does not depend on $\sigma^\dagger$, and the realizer-map $\pi_\phi$ is `effective' (Definitions <ref>, <ref>, <ref> and <ref>).

Similarly, a t-skeleton $\uplus \psi :: \Pi_{\mathrm{wrw}}(\Gamma, \Pi_{\mathrm{wrw}} (A, B))$ is the disjoint union on a family $\psi = (\psi_{(\gamma^\dagger, f)})_{(\gamma^\dagger, f) \in \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(\hat{\oc} \Gamma)}$ of t-skeletons $\psi_{(\gamma^\dagger, f)} :: \gamma^\dagger \rightarrowtriangle \mathrm{cod}_\psi(\gamma^\dagger, f)$ such that $\mathrm{cod}_\psi(\gamma^\dagger, f) \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(A, B)(\uplus \{\gamma^{\hat{\oc}\boldsymbol{1}} \}))$, each $\psi_{(\gamma^\dagger, f)}$ does not depend on $\gamma^\dagger$, and the realizer-map $\pi_\psi$ is `effective.'
Note that for each $\sigma_0^\dagger \in \mathcal{TS}_{\mathrm{wr}}(\hat{\oc}\Sigma(\Gamma, A))$ we may write $\sigma_0^\dagger = \langle \gamma_0^\dagger, \alpha_0^\dagger \rangle$ for some $\gamma_0 \in \mathcal{TS}_{\mathrm{wr}}(\Gamma)$ and $\alpha_0 \in \mathcal{TS}_{\mathrm{wr}}(A (\uplus \{ \gamma_0^{\hat{\oc}\boldsymbol{1}} \}))$.

Then, by applying the currying on skeletons in game semantics <cit.>, which simply adjusts the finitary `tags' for product and implication appropriately, to each component $\phi_{(\sigma^\dagger, e)}$ of a t-skeleton $\uplus \phi :: \Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, A), B)$ in the evident way, it is easy to see that we get a t-skeleton $\lambda_{A, B}(\uplus \phi) :: \Pi_{\mathrm{wrw}}(\Gamma, \Pi_{\mathrm{wrw}}(A, B))$.
Finally, this operation on t-skeletons has the evident inverse, which completes the proof.
Then, by adjusting `tags' appropriately, which is the standard currying operation in game semantics (<cit.>), we obtain, from the DPLI $\Phi_{\langle \gamma, \alpha \rangle} :: \langle \gamma, \alpha \rangle \multimap \beta_{\langle \gamma, \alpha \rangle}$ of $\Phi$ at each $\langle \gamma, \alpha \rangle :: \oc \Sigma (\Gamma, A)$, where $\beta_{\langle \gamma, \alpha \rangle}$ is a t-skeleton required by the first axiom on FoPLIs, a t-skeleton $\Phi'_\gamma :: \gamma \multimap (\alpha \multimap \beta_{\langle \gamma, \alpha \rangle})$.
It is easy to check that the family $\Phi' \colonequals (\Phi'_\gamma)_{\gamma :: \Gamma}$ forms an FoDPLI from $\Gamma$ to $\Pi (A, B)$, so that we obtain $\phi' \colonequals \bigcup \Phi' :: \Pi (\Gamma, \Pi (A, B))$.
We have defined the required map $\phi \mapsto \phi'$, which clearly has the inverse, completing the proof.

The proof of Lemma <ref> is essentially the same as the corresponding one given in the previous work <cit.>, and thus it explains why our realizability à la game semantics validates the $\xi$-rule just like the existing game semantics does.

The CwF $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ supports pi in the strict sense.

Let $\Gamma \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$, $A \in \mathscr{D}\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Gamma)$, $B \in \mathscr{D}\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Sigma_{\mathrm{wrw}}(\Gamma, A))$ and $\uplus \beta \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, A), B))$.

* ($\Pi$-Form) Let us define $\Pi(A, B) \colonequals (\Pi_{\mathrm{wrw}}(A(\uplus \gamma), B_{\uplus \gamma}))_{\uplus \gamma \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Gamma)}$, where $B_{\uplus \gamma} \colonequals (B(\langle \uplus \gamma, \uplus \tilde{\alpha} \rangle)_{\uplus \tilde{\alpha} \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(A(\uplus \gamma))} \in \mathscr{D}\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(A(\uplus \gamma))$.
To distinguish it from the game semantics of pi-types in <cit.>, we write $\Pi_{\mathrm{wrw}}(A, B)$ for $\Pi(A, B)$.

* ($\Pi$-Intro) We get $\lambda_{A, B} (\uplus \beta) \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Gamma, \Pi_{\mathrm{wrw}}(A, B)))$ by Lemma <ref>, where recall that $\lambda_{A, B}$ and $\lambda_{A, B}^{-1}$ simply `adjust finitary tags' on standard moves.
We often omit the subscripts $(\_)_{A, B}$ on $\lambda_{A, B}$ and $\lambda_{A, B}^{-1}$.

* ($\Pi$-Elim) Given $\uplus \kappa \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}} (\Gamma, \Pi_{\mathrm{wrw}}(A, B)))$ and $\uplus \alpha \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}} (\Gamma, A))$, we define $\mathrm{App}_{A, B} (\uplus \kappa, \uplus \alpha) \colonequals  \lambda_{A, B}^{-1}(\uplus \kappa) \bullet \overline{\uplus \alpha}$.
As in the proof of Theorem <ref>, $\lambda_{A, B}^{-1}(\uplus \kappa) \bullet \overline{\uplus \alpha} :: \Pi_{\mathrm{wrw}} (\Gamma, B\{ \overline{\uplus \alpha} \})$, and so $\mathrm{App}_{A, B} (\uplus \kappa, \uplus \alpha) = \lambda_{A, B}^{-1}(\uplus \kappa) \bullet \overline{\uplus \alpha} \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Gamma, B\{ \overline{\uplus \alpha} \}))$.
We often omit the subscripts $A, B$ on $\mathrm{App}_{A, B}$.

* ($\Pi$-Comp) $\mathrm{App} (\lambda (\uplus \beta) , \uplus \alpha) = \lambda_{A, B}^{-1}(\lambda_{A, B}(\uplus \beta)) \bullet \overline{\uplus \alpha} = \uplus \beta \bullet \overline{\uplus \alpha} = \uplus \beta \{ \overline{\uplus \alpha} \}$.

* ($\Pi$-Subst) Given $\Delta \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ and $\uplus \phi \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Delta, \Gamma)$, we calculate

\begin{align*}
\textstyle \Pi_{\mathrm{wrw}} (A, B) \{ \uplus \phi \} &= (\Pi_{\mathrm{wrw}} (A(\uplus \gamma), B_{\uplus \gamma}))_{\uplus \gamma \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Gamma)} \{ \uplus \phi \} \\
&= (\Pi_{\mathrm{wrw}} (A(\uplus \phi \bullet \uplus \delta), B_{\uplus \phi \bullet \uplus \delta}))_{\uplus \delta \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Delta)} \\
%&= \textstyle \{ \ell \Pi (A\{\phi\}(\delta), B(q(\phi, A) \circ \delta)) \ \! | \ \! \delta : \Delta \} \\
&= (\Pi_{\mathrm{wrw}} (A\{ \uplus \phi \}(\uplus \delta), B\{ \uplus \phi^+ \}_{\uplus \delta}))_{\uplus \delta \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Delta)} \\
&= \Pi_{\mathrm{wrw}}(A\{ \uplus \phi \}, B\{ \uplus \phi^+ \}),
\end{align*}

where $B\{\uplus \phi^+\}_{\uplus \delta} = B_{\uplus \phi \bullet \uplus \delta}$ since for all $\uplus \alpha' \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(A(\uplus \phi \bullet \uplus \delta))$ we have

\begin{align*}
B\{\uplus \phi^+\}_{\uplus \delta} (\uplus \alpha') &= B\{\uplus \phi^+\} (\langle \uplus \delta, \uplus \alpha' \rangle) \\
&= B (\langle \uplus \phi \bullet \mathrm{p}(A \{ \uplus \phi \}), \mathrm{v}_{A\{ \uplus \phi \}} \rangle \bullet \langle \uplus \delta, \uplus \alpha' \rangle) \\
%&= B(\langle f \bullet \mathrm{fst}, \mathrm{snd} \rangle \circ \langle d, \hat{a} \rangle) \\
%&= B(\langle f^\dagger \bullet \mathrm{fst} \circ \langle d, \hat{a} \rangle, \mathrm{snd}^\dagger \circ \langle d, \hat{a} \rangle \rangle) \\
&= B(\langle \uplus \phi \bullet \uplus \delta, \uplus \alpha' \rangle) \\
&= B_{\uplus \phi \bullet \uplus \delta} (\uplus \alpha').
\end{align*}

* ($\lambda$-Subst) We calculate

\begin{align*}
\lambda (\uplus \beta) \{ \uplus \phi \} &= \lambda_{A, B} (\uplus \beta) \bullet \uplus \phi \\
&= \lambda_{A\{\uplus \phi\}, B\{\uplus \phi^+\}} (\uplus \beta \bullet \langle \uplus \phi \bullet \mathrm{fst}, \mathrm{snd} \rangle) \quad \text{(by the definition of $\lambda$)} \\
&= \lambda_{A\{\uplus \phi\}, B\{\uplus \phi^+\}} (\uplus \beta \bullet \langle \uplus \phi \bullet \mathrm{p}(A \{ \uplus \phi \}), \mathrm{v}_{A\{\uplus \phi\}} \rangle) \\
&= \lambda_{A\{\uplus \phi\}, B\{\uplus \phi^+\}} (\uplus \beta \{ \uplus \phi^+ \}).
\end{align*}

* (App-Subst) We calculate

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

* ($\lambda$-Uniq) Finally, we calculate

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

which completes the proof.

Next, we consider sigma-types (Appendix <ref>).
Again, we first recall the semantic type former for sigma-types in an arbitrary CwF:

A CwF $\mathcal{C}$ supports sigma if

* ($\Sigma$-Form) Given $\Gamma \in \mathcal{C}$, $A \in \mathrm{Ty}(\Gamma)$ and $B \in \mathrm{Ty}(\Gamma . A)$, there is a type $\Sigma (A, B) \in \mathrm{Ty}(\Gamma)$;

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

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

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

* ($\Sigma$-Subst) Given $\Delta \in \mathcal{C}$ and $f : \Delta \to \Gamma$ in $\mathcal{C}$, $\Sigma (A, B) \{ f \} = \Sigma (A\{f\}, B\{f^+\})$, where $f^+ \colonequals \langle f \circ \mathrm{p}(A\{ f \}), \mathrm{v}_{A\{f\}} \rangle_A : \Delta . A\{f\} \to \Gamma . A$;

* (Pair-Subst) $\mathrm{p}(\Sigma (A, B)) \circ \mathrm{Pair}_{A, B} = \mathrm{p}(A) \circ \mathrm{p}(B)$ and $f^\star \circ \mathrm{Pair}_{A\{f\}, B\{f^+\}} = \mathrm{Pair}_{A, B} \circ f^{++}$, where

f^⋆⟨f ∘p(Σ(A,B){f}), v_Σ(A,B){f} ⟩_Σ(A,B) : Δ. Σ(A,B){f} →Γ. Σ(A,B); f^++ ⟨f^+ ∘p(B{f^+}), v_B{f^+} ⟩_B : Δ. A{f} . B{f^+} →Γ. A . B;

* ($\mathcal{R}^{\Sigma}$-Subst) $\mathcal{R}^{\Sigma}_{A, B, P}(p) \{f^\star\} = \mathcal{R}^{\Sigma}_{A\{f\}, B\{f^+\}, P\{f^\star\}} (p \{ f^{++} \})$.

Moreover, $\mathcal{C}$ supports sigma in the strict sense if it also satisfies

* ($\mathcal{R}^{\Sigma}$-Uniq) If $p \in \mathrm{Tm}(\Gamma . A . B, P \{ \mathrm{Pair}_{A, B} \})$, $q \in \mathrm{Tm}(\Gamma . \Sigma(A, B), P)$ and $q \{ \mathrm{Pair}_{A, B} \} = p$, then $q = \mathcal{R}^{\Sigma}_{A, B, P}(p)$.

Sigma-types (with the $\eta$-rule) are modeled in a CwF that supports sigma (in the strict sense); see Appendix <ref> for the details.

Now, let us describe our interpretation of sigma-types:

The CwF $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ supports sigma in the strict sense.

Let $\Gamma, \Delta \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$, $\uplus \phi \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Delta, \Gamma)$, $A \in \mathscr{D}\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Gamma)$ and $B \in \mathscr{D}\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Sigma_{\mathrm{wrw}}(\Gamma, A))$.

* ($\Sigma$-Form) Similarly to pi, let $\Sigma (A, B) \colonequals (\Sigma_{\mathrm{wrw}} (A(\uplus \gamma), B_{\uplus \gamma}))_{\uplus \gamma \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Gamma)}$.
Again, to distinguish it from the game semantics of sigma-types given in the previous work <cit.>, we write $\Sigma_{\mathrm{wrw}}(A, B)$ for $\Sigma(A, B)$.

* ($\Sigma$-Intro) By the isomorphism $\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma,A),B) \cong \Sigma_{\mathrm{wrw}}(\Gamma, \Sigma_{\mathrm{wrw}}(A,B))$, which is similar to (and simpler than) the one in Lemma <ref> and left to the reader, let $\mathrm{Pair}_{A, B} : \Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma,A),B) \rightarrow \Sigma_{\mathrm{wrw}}(\Gamma, \Sigma_{\mathrm{wrw}}(A,B))$ be the evident w.r.w. dereliction up to `tags,' or $\mathrm{Pair}_{A, B} \colonequals \langle \mathrm{fst} \bullet \mathrm{fst}, \langle \mathrm{snd} \bullet \mathrm{fst}, \mathrm{snd} \rangle \rangle$.
Note that there is the evident inverse $\mathrm{Pair}^{-1}_{A, B} = \langle \langle \mathrm{fst}, \mathrm{fst} \bullet \mathrm{snd} \rangle, \mathrm{snd} \bullet \mathrm{snd} \rangle$.

* ($\Sigma$-Elim) We define $\mathcal{R}^{\Sigma}_{A, B, P}(\uplus \rho) \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, \Sigma_{\mathrm{wrw}} (A, B)), P))$ to be the composition $\uplus \rho \bullet \mathrm{Pair}_{A, B}^{-1}$ for any $P \in \mathscr{D}\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Sigma_{\mathrm{wrw}}(\Gamma, \Sigma_{\mathrm{wrw}}(A,B)))$ and  $\uplus \rho \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, A), B), P\{\mathrm{Pair}_{A,B}\}))$.

* ($\Sigma$-Comp) We calculate

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

* ($\Sigma$-Subst) Similar to the case of pi.

* (Pair-Subst) We calculate

\begin{align*}
\mathrm{p}(\Sigma_{\mathrm{wrw}} (A, B)) \bullet \mathrm{Pair}_{A, B} &= \mathrm{fst} \bullet \langle \mathrm{fst} \bullet \mathrm{fst}, \langle \mathrm{snd} \bullet \mathrm{fst}, \mathrm{snd} \rangle \rangle \\
&= \mathrm{fst} \bullet \mathrm{fst} \\
&= \mathrm{p}(A) \bullet \mathrm{p}(B),
\end{align*}

\begin{align*}
& {\uplus \phi}^\star \bullet \mathrm{Pair}_{A\{\uplus \phi\}, B\{\uplus \phi^+\}} \\
=& \ \langle \uplus \phi \bullet \mathrm{p}(\Sigma_{\mathrm{wrw}}(A,B)\{\uplus \phi\}), \mathrm{v}_{\Sigma_{\mathrm{wrw}}(A,B)\{\uplus \phi\}} \rangle \bullet \mathrm{Pair}_{A\{\uplus \phi\}, B\{\uplus \phi^+\}} \\
=& \ \langle \uplus \phi \bullet \mathrm{p}(\Sigma_{\mathrm{wrw}}(A\{\uplus \phi\},B\{\uplus \phi^+\})) \bullet \mathrm{Pair}_{A\{\uplus \phi\}, B\{\uplus \phi^+\}}, \mathrm{v}_{\Sigma_{\mathrm{wrw}}(A,B)\{\uplus \phi\}} \bullet \mathrm{Pair}_{A\{ \uplus \phi \}, B\{ \uplus \phi^+ \}} \rangle \\
=& \ \langle \uplus \phi \bullet \mathrm{p}(A\{ \uplus \phi \}) \bullet \mathrm{p}(B\{ \uplus \phi^+ \}), \mathrm{v}_{\Sigma_{\mathrm{wrw}}(A\{ \uplus \phi \},B\{ \uplus \phi^+ \})} \bullet \mathrm{Pair}_{A\{ \uplus \phi \}, B\{ \uplus \phi^+ \}} \rangle \\
&\text{(by the above equations)} \\
=& \ \langle \uplus \phi \bullet \mathrm{fst} \bullet \mathrm{fst}, \mathrm{snd} \bullet \langle \mathrm{fst} \bullet \mathrm{fst}, \langle \mathrm{snd} \bullet \mathrm{fst}, \mathrm{snd} \rangle \rangle \rangle \\
=& \ \langle \uplus \phi \bullet \mathrm{fst} \bullet \mathrm{fst}, \langle \mathrm{snd} \bullet \mathrm{fst}, \mathrm{snd} \rangle \rangle \\
=& \ \langle \mathrm{fst} \bullet \mathrm{fst}, \langle \mathrm{snd} \bullet \mathrm{fst}, \mathrm{snd} \rangle \rangle \bullet \langle \langle \uplus \phi \bullet \mathrm{fst} \bullet \mathrm{fst}, \mathrm{snd} \bullet \mathrm{fst} \rangle, \mathrm{snd} \rangle \\
=& \ \langle \mathrm{fst} \bullet \mathrm{fst}, \langle \mathrm{snd} \bullet \mathrm{fst}, \mathrm{snd} \rangle \rangle \bullet \langle \langle \uplus \phi \bullet \mathrm{fst}, \mathrm{snd} \rangle \bullet \mathrm{fst}, \mathrm{snd} \rangle \\
=& \ \mathrm{Pair}_{A, B} \bullet \langle \langle \uplus \phi \bullet \mathrm{p}(A\{ \uplus \phi \}), \mathrm{v}_{A\{ \uplus \phi \}} \rangle \bullet \mathrm{p}(B\{ \uplus \phi^+ \}), \mathrm{v}_{B\{ \uplus \phi^+ \}} \rangle \\
=& \ \mathrm{Pair}_{A, B} \bullet \langle \uplus \phi^+ \bullet \mathrm{p}(B\{ \uplus \phi^+ \}), \mathrm{v}_{B\{ \uplus \phi^+ \}} \rangle \\
=& \ \mathrm{Pair}_{A, B} \bullet \uplus \phi^{++}.
\end{align*}

* ($\mathcal{R}^{\Sigma}$-Subst) We calculate

\begin{align*}
\mathcal{R}^{\Sigma}_{A, B, P}(\uplus \rho) \{ \uplus \phi^\star \} &= \uplus \rho \bullet \mathrm{Pair}_{A, B}^{-1} \bullet \langle \uplus \phi \bullet \mathrm{p}(\Sigma_{\mathrm{wrw}}(A,B)\{ \uplus \phi \}, \mathrm{v}_{\Sigma_{\mathrm{wrw}}(A,B)\{ \uplus \phi \}} \rangle \\
&= \uplus \rho \bullet \langle \langle \mathrm{fst}, \mathrm{fst} \bullet \mathrm{snd} \rangle, \mathrm{snd} \bullet \mathrm{snd} \rangle \bullet \langle \uplus \phi \bullet \mathrm{fst}, \mathrm{snd} \rangle \\
&= \uplus \rho \bullet \langle \langle \uplus \phi \bullet \mathrm{fst}, \mathrm{fst} \bullet \mathrm{snd} \rangle, \mathrm{snd} \bullet \mathrm{snd} \rangle \\
&= \uplus \rho \bullet \langle \langle \uplus \phi \bullet \mathrm{fst}, \mathrm{snd} \rangle \bullet \mathrm{fst}, \mathrm{snd} \rangle \bullet \langle \langle \mathrm{fst}, \mathrm{fst} \bullet \mathrm{snd} \rangle, \mathrm{snd} \bullet \mathrm{snd} \rangle \\
&= \uplus \rho \bullet \langle \uplus \phi^+ \bullet \mathrm{fst}, \mathrm{snd} \rangle \bullet \langle \langle \mathrm{fst}, \mathrm{fst} \bullet \mathrm{snd} \rangle, \mathrm{snd} \bullet \mathrm{snd} \rangle \\
&= \uplus \rho \bullet \langle \uplus \phi^+ \bullet \mathrm{p}(B\{ \uplus \phi^+ \}), \mathrm{v}_{B\{ \uplus \phi^+ \}} \rangle \bullet \mathrm{Pair}_{A\{ \uplus \phi \}, B\{ \uplus \phi^+ \}}^{-1} \\
&= \mathcal{R}^{\Sigma}_{A\{ \uplus \phi \}, B\{ \uplus \phi^+ \}, P\{ \uplus \phi^\star \}} (\uplus \rho \bullet \langle \uplus \phi^+ \bullet \mathrm{p}(B\{ \uplus \phi^+ \}), \mathrm{v}_{B\{ \uplus \phi^+ \}} \rangle ) \\
&= \mathcal{R}^{\Sigma}_{A\{ \uplus \phi \}, B\{ \uplus \phi^+ \}, P\{ \uplus \phi^\star \}} (\uplus \rho \{ \uplus \phi^{++} \}).
\end{align*}

* ($\mathcal{R}^{\Sigma}$-Uniq) If a given t-skeleton $\uplus \varrho \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, \Sigma_{\mathrm{wrw}}(A, B)), P))$ satisfies the equation $\uplus \varrho \{ \mathrm{Pair}_{A, B} \} = \uplus \rho$ then we have

\begin{equation*}
\uplus \varrho = \uplus \rho \bullet \mathrm{Pair}_{A, B}^{-1} = \mathcal{R}^{\Sigma}_{A, B, P}(\uplus \rho),
\end{equation*}

which completes the proof.

We proceed to model N-type (Appendix <ref>).
Again, let us first recall the semantic type former for N-type in an arbitrary CwF:

A CwF $\mathcal{C}$ supports N or natural numbers if

* ($N$-Form) Given $\Gamma \in \mathcal{C}$, there is a type $N^{\Gamma} \in \mathrm{Ty}(\Gamma)$, called natural number (N-) type in $\Gamma$, which we often abbreviate as $N$;

* ($N$-Intro) There are a term and a morphism in $\mathcal{C}$

0_Γ ∈Tm(Γ, N) succ_Γ : Γ. N →Γ. N

that satisfy the equations

0_Γ { f } = 0_Δ∈Tm(Δ, N)
p(N) ∘succ_Γ = p(N) : Γ. N →Γsucc_Γ ∘⟨g, v_N ⟩_N = ⟨g, v_N{succ_Δ} ⟩_N : Δ. N →Γ. N

for any morphisms $f : \Delta \to \Gamma$ and $g : \Delta . N \to \Gamma$ in $\mathcal{C}$;

Let us define $\mathrm{zero}_\Gamma \colonequals \langle \mathrm{id}_\Gamma, \underline{0}_\Gamma \rangle_N : \Gamma \to \Gamma . N$ for each $\Gamma \in \mathcal{C}$; it then satisfies $\mathrm{zero}_\Gamma \circ f = \langle f, \underline{0}_\Delta \rangle_N = \langle f, \mathrm{v}_N \{ \mathrm{zero}_\Delta \} \rangle_N : \Delta \to \Gamma . N$ for any morphism $f : \Delta \to \Gamma$ in $\mathcal{C}$.
We often omit the subscript $(\_)_\Gamma$ on $\underline{0}_\Gamma$, $\mathrm{zero}_{\Gamma}$ and $\mathrm{succ}_{\Gamma}$.
Also, for each $n \in \mathbb{N}$, we define $\underline{n}_\Gamma \in \mathrm{Tm}(\Gamma, N)$ by

* $\underline{0}_\Gamma$ is already given;

* $\underline{n+1}_\Gamma \colonequals \mathrm{v}_N \{ \mathrm{succ}_\Gamma \circ \langle \mathrm{id}_\Gamma, \underline{n}_\Gamma \rangle \}$;

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

* ($N$-Comp) We have the equations

ℛ^N_P(z, s) { zero } = z ∈Tm(Γ, P{zero}); ℛ^N_P(z, s) { succ } = s { ⟨id_Γ. N, ℛ^N_P(z, s) ⟩_P } ∈Tm(Γ. N, P{succ});

* ($N$-Subst) $N^{\Gamma}\{f\} = N^{\Delta} \in \mathrm{Ty}(\Delta)$;

* ($\mathcal{R}^{N}$-Subst) $\mathcal{R}^{N}_{P}(z, s) \{f^+\} = \mathcal{R}^{N}_{P\{f^+\}}(z\{f\}, s\{f^{++}\}) \in \mathrm{Tm}(\Delta . N, P\{f^+\})$, where

f^+ ⟨f ∘p(N), v_N ⟩_N : Δ. N →Γ. N f^++ ⟨f^+ ∘p(P{f^+}), v_P{f^+}⟩_P : Δ. N . P{f^+} →Γ. N . P.

N-type is modeled in a CwF that supports natural numbers; see Appendix <ref> for the details.

We now propose our game semantics of N-type by basically employing the total fragment of the standard game semantics of PCF à la McCusker <cit.>:

The CwF $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ supports natural numbers.

Let $\Gamma, \Delta \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ and $\uplus \phi \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Delta, \Gamma)$, and assume that $\mathscr{R}_{\mathrm{wr}}^{\mathrm{cp}}(\Gamma) \neq \emptyset$ and $\mathscr{R}_{\mathrm{wr}}^{\mathrm{cp}}(\Delta) \neq \emptyset$ since the other cases are trivial.

* ($N$-Form) Let $N^\Gamma$ be the constant dependent np-game on $\Gamma$ valued at $N$ (Example <ref>), for which we write $\{ N \}_\Gamma$ or $\{ N \}$.

* ($N$-Intro) Let $\underline{0}_\Gamma \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Gamma, \{ N \}))$ be $\uplus \{ \underline{0} \} :: \hat{\oc}\Gamma \rightarrowtriangle N$ up to `tags,' and $\mathrm{succ}_\Gamma : \Sigma_{\mathrm{wrw}}(\Gamma, \{ N^{[0]} \}) \rightarrow \Sigma_{\mathrm{wrw}}(\Gamma, \{ N^{[1]} \})$ the pairing $\langle \mathrm{p}(\{ N \}), \uplus \mathrm{s}^\Gamma \rangle$, where the superscripts $(\_)^{[i]}$ ($i = 0, 1$) are to distinguish the two copies of $N$, and the DoWRWLI $\uplus \mathrm{s}^\Gamma :: \Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, \{ N^{[0]} \}), \{ N^{[1]} \})$ is defined by

\begin{equation*}
\mathrm{s}^\Gamma_{(\sigma^\dagger, e)} \colonequals \mathrm{Pref} (\{ q^{[1]} . q^{[0]} . n^{[0]} . (n+1)^{[1]} \}) \quad (\underline{n} \colonequals \mathrm{snd} \bullet \sigma)
\end{equation*}

up to `tags' for each $(\sigma^\dagger, e) \in \mathscr{R}_{\mathrm{wr}}^{\mathrm{cp}}(\hat{\oc} \Sigma_{\mathrm{wrw}}(\Gamma, \{ N^{[0]} \}))$.
Clearly, $\underline{0}_\Gamma \bullet \uplus \phi = \underline{0}_\Delta$ and $\uplus \mathrm{s}^\Gamma \bullet \langle \uplus \psi, \mathrm{v}_{\{N\}_\Delta} \rangle = \uplus \mathrm{s}^\Delta = \mathrm{v}_{\{N\}_\Delta}\{ \mathrm{succ}_\Delta \}$, where $\uplus \psi : \Sigma_{\mathrm{wrw}}(\Delta, \{ N \}_\Delta) \rightarrow \Gamma$ is any morphism in $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$, and therefore the required equations hold.

* ($N$-Elim) Given $P \in \mathscr{D}\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Sigma_{\mathrm{wrw}}(\Gamma, \{ N \}))$, $\uplus \zeta \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Gamma, P\{ \mathrm{zero} \}))$ and $\uplus \sigma \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, \{ N \}), P), P\{ \mathrm{succ} \circ \mathrm{p}(P)\}))$, there are

⊎ζ̃ ∈𝒯𝒮_wr(Π_wrw(Σ_wrw(Π_wrw(Σ_wrw(Γ, {N}), P), { Σ_wrw(Γ, { N }) }), P{ zero ∙fst ∙snd }))

⊎σ̃ ∈𝒯𝒮_wr(Π_wrw(Σ_wrw(Π_wrw(Σ_wrw(Γ, {N}), P), { Σ_wrw(Γ, { N }) }), P{ succ ∙pred ∙snd }))

defined respectively by

⊎ζ̃ : Π_wrw(Σ_wrw(Γ, { N }), P) & Σ_wrw(Γ, { N }) snd⟶ Σ_wrw(Γ, { N }) fst⟶ Γ⊎ζ⟶ ∫P{ zero };

⊎σ̃ : Π_wrw(Σ_wrw(Γ, {N}), P) & Σ_wrw(Γ, {N}) ⟨pred ∙snd, ev_P { ⟨fst, pred ∙snd ⟩} ⟩⟶ Σ_wrw(Γ, {N}) & ∫P ⊎σ⟶ ∫P{ succ ∘fst },

where $\mathrm{ev}_P \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, \{N\}), P), \{ \Sigma_{\mathrm{wrw}}(\Gamma, \{N\}) \}), P\{\mathrm{snd}\}))$ is the evaluation on $P$ <cit.> given by $\mathrm{ev}_P \colonequals \lambda^{-1}(\uplus \mathrm{der}_{\Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, \{ N \}), P)})$, and $\mathrm{pred} : \Sigma_{\mathrm{wrw}}(\Gamma, \{N\}) \to \Sigma_{\mathrm{wrw}}(\Gamma, \{N\})$ is the predecessor <cit.> given similarly to $\mathrm{succ}$ such that $\mathrm{pred} \bullet \mathrm{succ} = \uplus \mathrm{der}_{\Sigma_{\mathrm{wrw}}(\Gamma, \{ N \})}$ and $\mathrm{pred} \bullet \mathrm{zero} = \mathrm{zero}$.

In addition, let us define

P_z P{ zero ∙p(N) }) ∈𝒟ℕℙ𝔾_wrw^wo(Σ_wrw(Γ, {N}));

P_s P{ succ ∙pred ∙p(P_z) } ∈𝒟ℕℙ𝔾_wrw^wo(Σ_wrw(Σ_wrw(Γ, {N}), P_z)),

and then we have

\begin{equation*}
\mathrm{cond}_P \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, \{ N \}), P_{\mathrm{z}}), P_{\mathrm{s}}), P\{ \mathrm{p}(P_{\mathrm{z}}) \bullet \mathrm{p}(P_{\mathrm{s}}) \}))
\end{equation*}

that is the standard interpretation of conditionals on $P$ <cit.>: It first asks an input natural number in the component $N$ of the domain, and plays as the w.r.w. dereliction between $P_{\mathrm{z}}$ and $P\{ \mathrm{p}(P_{\mathrm{z}}) \bullet \mathrm{p}(P_{\mathrm{s}})\}$ if the answer is $\underline{0}$, and as the w.r.w. dereliction between $P_{\mathrm{s}}$ and $P\{ \mathrm{p}(P_{\mathrm{z}}) \bullet \mathrm{p}(P_{\mathrm{s}})\}$ otherwise.
Then, we define $\mathcal{F}^{N}_{P}(\uplus \zeta, \uplus \sigma) : \Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, \{N\}), P) \to \Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, \{N\}), P)$ by

\begin{equation*}
\mathcal{F}^{N}_{P}(\uplus \zeta, \uplus \sigma) \colonequals \lambda_{\{ \Sigma_{\mathrm{wrw}}(\Gamma, \{ N \}) \}, \{ P\{ \mathrm{snd} \} \}} (\mathrm{cond}_P \{ \langle \langle \mathrm{snd}, \uplus \tilde{\zeta} \rangle, \uplus \tilde{\sigma} \rangle \}).
\end{equation*}

Finally, we define $\mathcal{R}^{N}_{P}(\uplus \zeta, \uplus \sigma) \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, \{N\}), P))$ to be the least upper bound of the chain $\big(\mathcal{R}^{N}_{P}(\uplus \zeta, \uplus \sigma)_n \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, \{N\}), P))\big)_{n \in \mathbb{N}}$:

ℛ^N_P(⊎ζ, ⊎σ)_0 ⊤  (up to `tags');

ℛ^N_P(⊎ζ, ⊎σ)_n+1 ℱ^N_P(⊎ζ, ⊎σ) ∙ℛ^N_P(⊎ζ, ⊎σ)_n.

* ($N$-Comp) By the definition of $\mathcal{R}^{N}_{P}(\uplus \zeta, \uplus \sigma)$, we calculate

ℛ^N_P(⊎ζ, ⊎σ) { zero } = ⊎ζ;

ℛ^N_P(⊎ζ, ⊎σ) { succ } = ⊎σ{ ⟨⊎der_Σ(Γ, {N}), ℛ^N_P(⊎ζ, ⊎σ) ⟩}.

* ($N$-Subst) $\{N\}_{\Gamma}\{ \uplus \phi \} = \{N\}_{\Delta}$.

* ($\mathcal{R}^{N}$-Subst)
Finally, by the definition of $\mathcal{R}^{N}_{P}(\uplus \zeta, \uplus \sigma)$, we calculate

\begin{equation*}
\mathcal{R}^{N}_{P}(\uplus \zeta, \uplus \sigma) \{ \uplus \phi^+ \} = \mathcal{R}^{N}_{P\{ \uplus \phi^+ \}}(\uplus \zeta\{ \uplus \phi \}, \uplus \sigma\{ \uplus \phi^{++} \})
\end{equation*}

(or $\mathcal{R}^{N}_{P}(\uplus \zeta, \uplus \sigma)_n \{ \uplus \phi^+ \} = \mathcal{R}^{N}_{P\{ \uplus \phi^+ \}}(\uplus \zeta\{ \uplus \phi \}, \uplus \sigma\{ \uplus \phi^{++} \})_n$ for all $n \in \mathbb{N}$).

We proceed to model identity (Id-) types (Appendix <ref>).
Again, we first review the semantic type former for Id-types in an arbitrary CwF:

A CwF $\mathcal{C}$ supports Id if

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

* (Id-Intro) There is a morphism $\mathrm{Refl}_A : \Gamma . A \to \Gamma . A . A^+ . \mathrm{Id}_A$ in $\mathcal{C}$;

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

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

* (Id-Subst) $\mathrm{Id}_A\{f^{++}\} = \mathrm{Id}_{A\{f\}} \in \mathrm{Ty}(\Delta . A\{f\} . A\{f\}^+)$ for all $\Delta \in \mathcal{C}$ and $f : \Delta \to \Gamma$ in $\mathcal{C}$, where

A{f}^+ A{f}{p(A{f})} ∈Ty(Δ. A{f});
f^+ ⟨f ∘p(A{ f }), v_A{f} ⟩_A : Δ. A{f} →Γ. A;
f^++ ⟨f^+ ∘p(A^+{f^+}), v_A^+{f^+} ⟩_A^+ : Δ. A{f} . A^+{f^+} →Γ. A . A^+;

* (Refl-Subst) $\mathrm{Refl}_A \circ f^+ = f^{+++} \circ \mathrm{Refl}_{A\{f\}} : \Delta . A\{f\} \to \Gamma . A . A^+ . \mathrm{Id}_A$, where

f^+++ ⟨f^++ ∘p(Id_A{f^++}), v_Id_A{f^++} ⟩_Id_A : Δ. A{f} . A^+{f^+} . Id_A{f} →Γ. A . A^+ . Id_A;

* ($\mathcal{R}^{\mathrm{Id}}$-Subst) $\mathcal{R}^{\mathrm{Id}}_{A,B}(b)\{f^{+++}\} = \mathcal{R}^{\mathrm{Id}}_{A\{f\}, B\{f^{+++}\}}(b\{f^+\})$.

Id-types are modeled in a CwF that supports Id; see Appendix <ref> for the details.

We then equip the CwF $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ with our game-semantic Id-types:

The CwF $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ supports Id.

Let $\Gamma, \Delta \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$, $\uplus \phi \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Delta, \Gamma)$ and $A \in \mathscr{D}\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Gamma)$.

* (Id-Form) We define $\mathrm{Id}_A \in \mathscr{D}\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, A), A^+))$ by $\mathrm{Id}_A \colonequals (\mathrm{Id}_{A(\uplus \gamma)}(\uplus \alpha, \uplus \alpha'))_{\langle \langle \uplus \gamma, \uplus \alpha \rangle, \uplus \alpha' \rangle \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, A), A^+))}$.

* (Id-Intro) Let $\mathrm{Refl}_A : \Sigma_{\mathrm{wrw}}(\Gamma, A^{[1]}) \rightarrow \Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, A^{[2]}), (A^{[3]})^+), \mathrm{Id}_A)$ be what plays by the w.r.w. dereliction between $\Sigma_{\mathrm{wrw}}(\Gamma, A^{[1]})$ and $\Sigma_{\mathrm{wrw}}(\Gamma, A^{[2]})$, between $\int_\Gamma A^{[1]}$ and $\int_\Gamma (A^{[3]})^+$, and trivially on $\Sigma_{\mathrm{wrw}}(\Gamma, A^{[1]}) \rightarrow \boldsymbol{1}$, where the superscripts $(\_)^{[i]}$ ($i = 1, 2, 3$) are to distinguish the three copies of $A$.
The inverse $\mathrm{Refl}_A^{-1} : \Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, A^{[2]}), (A^{[3]})^+), \mathrm{Id}_A) \to \Sigma_{\mathrm{wrw}}(\Gamma, A^{[1]})$ is the w.r.w. dereliction between $\Sigma_{\mathrm{wrw}}(\Gamma, A^{[2]})$ and $\Sigma_{\mathrm{wrw}}(\Gamma, A^{[1]})$ up to `tags.'

If we allowed a non-canonical t-skeleton on $\mathrm{Id}_A$ then $\mathrm{Refl}_A$ would have only the left inverse, being unable to satisfy Id-Elim given below, which is why we define Id np-games in the rather extensional form in Definition <ref>.

* (Id-Elim) Given $B \in \mathscr{D}\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, A^{[2]}), (A^{[3]})^+), \mathrm{Id}_A))$ and $\uplus \beta \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, A), B\{\mathrm{Refl}_A\}))$, we define

\begin{equation*}
\mathcal{R}^{\mathrm{Id}}_{A,B}(\uplus \beta) \colonequals \uplus \beta \bullet \mathrm{Refl}_A^{-1} \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}((\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, A), A^+), \mathrm{Id}_A), B)).
\end{equation*}

* (Id-Comp) We then calculate

\begin{align*}
\mathcal{R}^{\mathrm{Id}}_{A,B}(\uplus \beta)\{\mathrm{Refl}_A\} &= \mathcal{R}^{\mathrm{Id}}_{A,B}(\uplus \beta) \bullet \mathrm{Refl}_A \\
&= (\uplus \beta \bullet \mathrm{Refl}_A^{-1}) \bullet \mathrm{Refl}_A \\
&= \uplus \beta \bullet (\mathrm{Refl}_A^{-1} \bullet \mathrm{Refl}_A) \\
&= \uplus \beta \bullet \uplus \mathrm{der}_{\Sigma_{\mathrm{wrw}}(\Gamma, A)} \\
&= \uplus \beta.
\end{align*}

* (Id-Subst) We calculate

\begin{align*}
\mathrm{Id}_A\{\uplus \phi^{++}\} &= (\mathrm{Id}_{A(\uplus \gamma)}(\uplus \alpha, \uplus \alpha'))_{ \langle \langle \uplus \gamma, \uplus \alpha \rangle, \uplus \alpha' \rangle \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, A), A^+))} \{ \uplus \phi^{++} \} \\
&= (\mathrm{Id}_A(\langle \langle \uplus \gamma, \uplus \alpha \rangle, \uplus \alpha' \rangle))_{\langle \langle \uplus \gamma, \uplus \alpha \rangle, \uplus \alpha' \rangle \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Gamma, A), A^+)} \{\uplus \phi^{++}\} \\
&= (\mathrm{Id}_{A}(\uplus \phi^{++} \bullet \langle \langle \uplus \delta, \uplus \alpha \rangle, \uplus \alpha' \rangle))_{\langle \langle \uplus \delta, \uplus \alpha \rangle, \uplus \alpha' \rangle \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Delta, A\{\uplus \phi\}), A\{\uplus \phi\}^+))} \\
&= (\mathrm{Id}_{A}(\langle \uplus \phi \bullet \uplus \delta, \uplus \alpha \rangle, \uplus \alpha' \rangle))_{\langle \langle \uplus \delta, \uplus \alpha \rangle, \uplus \alpha' \rangle \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Delta, A\{\uplus \phi\}), A\{\uplus \phi\}^+))} \\
&= (\mathrm{Id}_{A(\uplus \phi \bullet \uplus \delta)}(\uplus \alpha, \uplus \alpha'))_{\langle \langle \uplus \delta, \uplus \alpha \rangle, \uplus \alpha' \rangle \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Delta, A\{\uplus \phi\}), A\{\uplus \phi\}^+))} \\
&= (\mathrm{Id}_{A\{\uplus \phi\}(\uplus \delta)}(\uplus \alpha, \uplus \alpha'))_{\langle \langle \uplus \delta, \uplus \alpha \rangle, \uplus \alpha' \rangle \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Sigma_{\mathrm{wrw}}(\Sigma_{\mathrm{wrw}}(\Delta, A\{\uplus \phi\}), A\{\uplus \phi\}^+))} \\
&= \mathrm{Id}_{A\{\uplus \phi\}},
\end{align*}

where the forth equation holds because

\begin{align*}
\uplus \phi^{++} \bullet \langle \langle \uplus \delta, \uplus \alpha \rangle, \uplus \alpha' \rangle &= \langle \uplus \phi^+ \bullet \mathrm{p}(A^+\{\uplus \phi^+\}), \mathrm{v}_{A^+\{\uplus \phi^+\}} \rangle \bullet \langle \langle \uplus \delta, \uplus \alpha \rangle, \uplus \alpha' \rangle \\
&= \langle \uplus \phi^+ \bullet \mathrm{p}(A^+\{\uplus \phi^+\}) \bullet \langle \langle \uplus \delta, \uplus \alpha \rangle, \uplus \alpha' \rangle, \mathrm{v}_{A^+\{\uplus \phi^+\}} \bullet \langle \langle \uplus \delta, \uplus \alpha \rangle, \uplus \alpha' \rangle \rangle \\
%&= \langle \langle [\phi] \bullet [\delta], [\alpha] \rangle, [\alpha'] \rangle \\
&= \langle \langle \uplus \phi \bullet \uplus \delta, \uplus \alpha \rangle, \uplus \alpha' \rangle.
\end{align*}

* (Refl-Subst) We calculate

\begin{align*}
\mathrm{Refl}_A \bullet \uplus \phi^+ &= \mathrm{Refl}_A \bullet \langle \uplus \phi \bullet \mathrm{p}(A\{ \uplus \phi \}), \mathrm{v}_{A\{ \uplus \phi \}} \rangle \\
&= \langle \langle \langle \uplus \phi \bullet \mathrm{p}(A\{ \uplus \phi \}), \mathrm{v}_{A\{ \uplus \phi \}} \rangle \bullet \mathrm{p}(A^+\{ \uplus \phi^+ \}) \bullet \mathrm{p}(\mathrm{Id}_A\{ \uplus \phi^{++} \}), \\&\mathrm{v}_{A^+\{ \uplus \phi^+ \}} \bullet \mathrm{p}(\mathrm{Id}_A\{ \uplus \phi^{++} \}) \rangle, \mathrm{v}_{\mathrm{Id}_A\{ \uplus \phi^{++} \}} \rangle \bullet \mathrm{Refl}_{A\{ \uplus \phi \}} \quad \text{(by the definition of $\mathrm{Refl}$)} \\
&= \langle \langle \uplus \phi^+ \bullet \mathrm{p}(A^+\{ \uplus \phi^+ \}), \mathrm{v}_{A^+\{ \uplus \phi^+ \}} \rangle \bullet \mathrm{p}(\mathrm{Id}_A\{ \uplus \phi^{++} \}), \mathrm{v}_{\mathrm{Id}_A\{ \uplus \phi^{++} \}} \rangle \bullet \mathrm{Refl}_{A\{ \uplus \phi \}} \\
&= \langle \uplus \phi^{++} \bullet \mathrm{p}(\mathrm{Id}_A\{ \uplus \phi^{++} \}), \mathrm{v}_{\mathrm{Id}_A\{ \uplus \phi^{++} \}} \rangle \bullet \mathrm{Refl}_{A\{ \uplus \phi \}} \\
&= \uplus \phi^{+++} \bullet \mathrm{Refl}_{A\{ \uplus \phi \}}.
\end{align*}

* ($\mathcal{R}^{\mathrm{Id}}$-Subst) We calculate

\begin{align*}
\mathcal{R}^{\mathrm{Id}}_{A,B}(\uplus \beta)\{\uplus \phi^{+++}\} &= (\uplus \beta \bullet \mathrm{Refl}_A^{-1}) \bullet \uplus \phi^{+++} \\
&= \uplus \beta \bullet (\mathrm{Refl}_A^{-1} \bullet \uplus \phi^{+++}) \\
&= \uplus \beta \bullet (\uplus \phi^+ \bullet \mathrm{Refl}_{A\{\uplus \phi\}}^{-1}) \quad \text{(by Refl-Subst)} \\
&= (\uplus \beta \bullet \uplus \phi^+) \bullet \mathrm{Refl}_{A\{\uplus \phi\}}^{-1} \\
&= \mathcal{R}^{\mathrm{Id}}_{A\{\uplus \phi\}, B\{\uplus \phi^{+++}\}}(\uplus \beta \bullet \uplus \phi^+) \\
&= \mathcal{R}^{\mathrm{Id}}_{A\{\uplus \phi\}, B\{\uplus \phi^{+++}\}}(\uplus \beta \{\uplus \phi^+\}),
\end{align*}

which completes the proof.

We next model unit-type (Appendix <ref>).
Again, let us first recall the semantic type former for unit-type:

A CwF $\mathcal{C}$ supports unit if

* (Unit-Form) Given $\Gamma \in \mathcal{C}$, there is a type $\boldsymbol{1}^{\Gamma} \in \mathrm{Ty}(\Gamma)$, called the unity type in the context $\Gamma$;

* (Unit-Intro) Given $\Gamma \in \mathcal{C}$, there is a term $\top_{\Gamma} \in \mathrm{Tm}(\Gamma, \boldsymbol{1}^\Gamma)$;

* (Unit-Elim) Given $\Gamma \in \mathcal{C}$, $A \in \mathrm{Ty}(\Gamma . \boldsymbol{1}^\Gamma)$, $a \in \mathrm{Tm}(\Gamma, A\{ \overline{\top_\Gamma} \})$ and $t \in \mathrm{Tm}(\Gamma, \boldsymbol{1}^\Gamma)$, there is a term $\mathcal{R}^{\boldsymbol{1}}_A(a, t) \in \mathrm{Tm}(\Gamma, A\{\overline{t}\})$, where

⊤ ⟨id_Γ, ⊤_Γ⟩_1^Γ : Γ→Γ. 1^Γt ⟨id_Γ, t ⟩_1^Γ : Γ→Γ. 1^Γ;

* (Unit-Comp) $\mathcal{R}^{\boldsymbol{1}}_A(a, \top_\Gamma) = a$;

* (Unit-Subst) Given $f : \Delta \to \Gamma$ in $\mathcal{C}$, $\boldsymbol{1}^{\Gamma}\{f\} = \boldsymbol{1}^{\Delta} \in \mathrm{Ty}(\Delta)$;

* ($\top$-Subst) $\top_{\Gamma}\{f\} = \top_{\Delta} \in \mathrm{Tm}(\Delta, \boldsymbol{1}^\Delta)$.

Moreover, $\mathcal{C}$ supports one in the strict sense if it additionally satisfies:

* ($\top$-Uniq)
$t = \top_\Gamma$ for all $t \in \mathrm{Tm}(\Gamma, \boldsymbol{1}^\Gamma)$.[Note that $\top$-Uniq implies Unit-Elim and Unit-Comp by defining $\mathcal{R}^{\boldsymbol{1}}_A(a, t) \colonequals a$.]

Unit-type (with the $\eta$-rule) is modeled in a CwF that supports unit (in the strict sense); see Appendix <ref> for the details.

We now propose our game semantics of unit-type:

The CwF $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ supports unit in the strict sense.

Let $\Gamma, \Delta \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ and $\uplus \phi \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Delta, \Gamma)$, and assume that $\mathscr{R}_{\mathrm{wr}}^{\mathrm{cp}}(\Gamma) \neq \emptyset$ and $\mathscr{R}_{\mathrm{wr}}^{\mathrm{cp}}(\Delta) \neq \emptyset$ since the other cases are trivial.

* (Unit-Form) Let $\boldsymbol{1}^{\Gamma}$ be the constant dependent np-game valued at the unit np-game $\boldsymbol{1}$ (Example <ref>), for which we write $\{ \boldsymbol{1} \}_\Gamma$ or $\{ \boldsymbol{1} \}$.

* (Unit-Intro) Let $\top_{\Gamma} \in \mathrm{Tm}(\Gamma, \{ \boldsymbol{1} \}_\Gamma)$ be the unique one $\uplus \{ \top \}$ up to `tags.'

* (Unit-Elim) Given $A \in \mathscr{D}\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Sigma_{\mathrm{wrw}}(\Gamma, \{ \boldsymbol{1} \}_\Gamma))$, $\uplus \alpha \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Gamma, A \{ \overline{\top_\Gamma} \}))$ and $\uplus \tau \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Gamma, \{ \boldsymbol{1} \}))$, the equation $\uplus \tau = \top_\Gamma$ clearly holds, i.e., $\top$-Uniq is satisfied, and therefore we define $\mathcal{R}^{\boldsymbol{1}}_A(\uplus \alpha, \uplus \tau) \colonequals \uplus \alpha$.

* (Unit-Comp) Clearly, $\mathcal{R}^{\boldsymbol{1}}_A(\uplus \alpha, \top_\Gamma) = \uplus \alpha$.

* (Unit-Subst) Clearly, $\{ \boldsymbol{1} \}_\Gamma\{ \uplus \phi \} = \{ \boldsymbol{1} \}_{\Delta}$.

* ($\top$-Subst) Clearly, $\top_{\Gamma} \bullet \uplus \phi = \top_{\Delta} : \Delta \to \boldsymbol{1}$,

which completes the proof.

Finally, we model empty-type (Appendix <ref>).
First, the semantic type former for empty-type is:

A CwF $\mathcal{C}$ supports empty if

* (Empty-Form) Given $\Gamma \in \mathcal{C}$, there is a type $\boldsymbol{0}^{\Gamma} \in \mathrm{Ty}(\Gamma)$, called the empty-type in the context $\Gamma$;

* Empty-Intro. For any $\Gamma \in \mathcal{C}$, there is a morphism

\begin{equation*}
\bot_{\Gamma} : \Gamma \to \Gamma . \boldsymbol{0}
\end{equation*}

that satisfies $\mathrm{p}(\boldsymbol{0}) \circ \bot_{\Gamma} = \mathrm{id}_{\Gamma}$ and $\bot_{\Gamma} \circ \phi = \langle \phi, \mathrm{v}_{\boldsymbol{0}}\{\bot_{\Delta}\} \rangle_{\boldsymbol{0}}$, where $\phi : \Delta \to \Gamma$ is any morphism in $\mathcal{C}$.
We usually omit the subscript $\Gamma$ in $\bot_{\Gamma}$;

* (Empty-Elim) Given $\Gamma \in \mathcal{C}$, $A \in \mathrm{Ty}(\Gamma . \boldsymbol{0}^\Gamma)$ and $z \in \mathrm{Tm}(\Gamma, \boldsymbol{0}^\Gamma)$, there is a term $\mathcal{R}^{\boldsymbol{0}}_A(z) \in \mathrm{Tm}(\Gamma, A\{\overline{z}\})$, where $\overline{z} \colonequals \langle \mathrm{id}_\Gamma, z \rangle_{\boldsymbol{0}^\Gamma} : \Gamma \to \Gamma . \boldsymbol{0}^\Gamma$;

* Empty-Comp. Under the same assumption,

\begin{equation*}
\mathcal{R}^{\boldsymbol{1}}_A(\tau)\{\star\} = \kappa
\end{equation*}

for any term $\kappa \in \mathrm{Tm}(\Gamma, A\{\star\})$.

* (Empty-Subst) Given $f : \Delta \to \Gamma$ in $\mathcal{C}$, $\boldsymbol{0}^{\Gamma}\{f\} = \boldsymbol{0}^{\Delta} \in \mathrm{Ty}(\Delta)$;

* ($\mathcal{R}^0$-Subst) $\mathcal{R}^{\boldsymbol{0}}_{A\{f^+\}}(z\{f\}) = \mathcal{R}^{\boldsymbol{0}}_A(z)\{ f \}$, where $f^+ \colonequals \langle f \bullet \mathrm{p}(\boldsymbol{0}^\Delta), \mathrm{v}_{\boldsymbol{0}^\Gamma} \rangle_{\boldsymbol{0}^\Gamma} : \Delta . \boldsymbol{0}^\Delta \to \Gamma . \boldsymbol{0}^\Gamma$.

Empty-type is modeled in a CwF that supports empty; see Appendix <ref> for the details.

Let us finally propose our game-semantic interpretation of empty-type:

The CwF $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ supports empty.

Let $\Gamma, \Delta \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ and $\uplus \phi \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Delta, \Gamma)$.

* (Empty-Form) $\boldsymbol{0}^\Gamma$ is the constant dependent np-game valued at the empty np-game $\boldsymbol{0}$ (Example <ref>), for which we write $\{ \boldsymbol{0} \}_{\Gamma}$ or $\{ \boldsymbol{0} \}$.

* (Empty-Elim) Let $A \in \mathscr{D}\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}(\Sigma_{\mathrm{wrw}}(\Gamma, \{ \boldsymbol{0} \}_\Gamma))$ and $\uplus \zeta \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Gamma, \{ \boldsymbol{0} \}_\Gamma))$.
Because $\mathscr{R}_{\mathrm{wr}}^{\mathrm{cp}}(\boldsymbol{0}) = \emptyset$, we have $\mathscr{R}_{\mathrm{wr}}^{\mathrm{cp}}(\Gamma) = \emptyset$ and $\zeta = \emptyset$.
Hence, it suffices to define $\mathcal{R}^{\boldsymbol{0}}_A(\uplus \zeta) \in \mathcal{TS}_{\mathrm{wr}}(\Pi_{\mathrm{wrw}}(\Gamma, A \{ \overline{\uplus \zeta} \}))$ to be the trivial one $\uplus \{ \top \}$.

* (Empty-Subst) Clearly, $\{ \boldsymbol{0} \}_{\Gamma}\{ \uplus \phi \} = \{ \boldsymbol{0} \}_{\Delta}$.

* ($\mathcal{R}^{\boldsymbol{0}}$-Subst) By the definition of the operation $\mathcal{R}^{\boldsymbol{0}}_{\_}(\_)$, we calculate

\begin{align*}
\mathcal{R}^{\boldsymbol{0}}_{A\{ \uplus \phi^+ \}}(\uplus \zeta\{ \uplus \phi \}) &= \uplus \{ \top \} \\
&= \uplus \{ \top \} \bullet \uplus \phi \quad \text{(n.b.,  $\mathscr{R}_{\mathrm{wr}}^{\mathrm{cp}}(\Delta) = \emptyset$ and $\phi = \emptyset$)} \\
%&= \mathcal{R}^{\boldsymbol{0}}_{A\{ \uplus \phi^+ \}}(\uplus \zeta \bullet \uplus \phi) \\
&= \mathcal{R}^{\boldsymbol{0}}_{A\{ \uplus \phi^+ \}}(\uplus \zeta) \bullet \uplus \phi \\
&= \mathcal{R}^{\boldsymbol{0}}_A(\uplus \zeta)\{ \uplus \phi \},
\end{align*}

which completes the proof.

§.§ Main result: consistency of intensional Martin-Löf type theory with formal Church's thesis and its constructivity

Finally, let us solve the targeted open problem, viz., consistency of MLTT with CT, in the affirmative.
For precision, we implement the T-predicate $T$ and the result-extracting function $U$ (Section <ref>) explicitly in MLTT as follows.

We first define a realizer for a given partial function $f : \mathbb{N} \rightharpoonup \mathbb{N}$ to be a realizer for a t-skeleton $\uplus \phi :: \hat{\oc} N \rightarrowtriangle N$ whose extension $\mathrm{ext}(\uplus \phi) : n \in \mathbb{N} \mapsto \mathrm{read}(\uplus \phi \bullet \underline{n}_{\boldsymbol{1}})$, where $\mathrm{read}(\uplus \{ \bot \}) \uparrow$ and $\mathrm{read}(\underline{m}_{\boldsymbol{1}}) \colonequals m$ for all $m \in \mathbb{N}$, coincides with $f$.

Then, we implement the T-predicate and the result-extracting function in MLTT with respect to the resulting realizers for total recursive functions:

* Let the T-predicate to be the type $\mathsf{x : N, y : N, z : N \vdash T(x, y, z) \ type}$ defined by $\mathsf{T(\underline{e}, \underline{n}, \underline{c}) \colonequals 1}$ if the triple $e, n, c \in \mathbb{N}$ satisfies the T-predicate with respect to the realizers just defined in the preceding paragraphs, for which we write $T(e, n, c)$, and $\mathsf{T(\underline{e}, \underline{n}, \underline{c}) \colonequals 0}$ otherwise;

* Let the result-extracting function to be the term $\mathsf{x : N \vdash U(x) : N}$ defined by $\mathsf{U(\underline{c}) \colonequals \underline{n} : N}$ if $c \in \mathbb{N}$ encodes, with respect to the realizers just defined, the computational history of a terminating computation on $\mathbb{N}$ whose output is $n \in \mathbb{N}$, and $\mathsf{U(\underline{c}) \colonequals \underline{0} : N}$ otherwise.

In practice, the T-predicate and the result-extracting function are given in MLTT by the elimination rule of N-type, which is possible because they are both primitive recursive <cit.>.
Thus, having modeled MLTT, including N-type, one may think that a model of the T-predicate and the result-extracting function has been obtained as well.
However, it is not quite the case because we need a universe to formalize the T-predicate in that way because it is a type, not a term.

For this point, we could extend our model of MLTT to a universe, but for brevity, let us skip modeling a universe in this article and instead define our interpretation of the T-predicate directly:

Let us interpret the T-predicate in the CwF $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ by the dependent np-game $\mathcal{T}$ on the product $(N \mathbin{\&} N) \mathbin{\&} N$ defined by

\begin{equation*}
\mathcal{T} (\langle \langle \uplus \sigma, \uplus \tau \rangle, \uplus \gamma \rangle) \colonequals \begin{cases} \boldsymbol{1} &\text{if $T(\mathrm{read} (\uplus \sigma), \mathrm{read}(\uplus \tau), \mathrm{read} (\uplus \gamma))$;} \\ \boldsymbol{0} &\text{otherwise.} \end{cases}
\end{equation*}

Clearly, our interpretation of the T-predicate is sound, i.e., it respects the defining judgmental equality.
Having extended our model of MLTT in the CwF $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ to the T-predicate, we are now ready to present our main theorem:

The CwF $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ validates CT, and therefore it models MLTT equipped with CT.

We have given a model of MLTT equipped with the T-predicate and unit-, empty-, N-, sigma-, pi- and Id-types in $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$.
Hence, it remains to validate CT in $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$.
Let us write $\mathcal{CT} \in \mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$ for the interpretation of CT (<ref>) in $\mathbb{NPG}_{\mathrm{wrw}}^{\mathrm{wo}}$.

As sketched in Section <ref>, we provide the t-skeleton $\uplus \mathrm{ct} :: \mathcal{CT}$ whose component $\mathrm{ct}_{(\uplus \phi^\dagger, e)}$ for each $(\uplus \phi^\dagger, e) \in \mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(\hat{\oc} (\hat{\oc} N \rightarrowtriangle N))$ is the pairing $\langle \uplus \{ \underline{e^\ddagger} \},  \mathrm{ct}' \rangle$ up to `tags,' where $e^\ddagger \in \pi_2(\mathscr{R}^{\mathrm{cp}}_{\mathrm{wr}}(\hat{\oc} N \rightarrowtriangle N))$ is the canonical realizer for $\uplus \phi$, and $\mathrm{ct}'$ is the evident DoWRWLI that essentially computes the code $c \in \mathbb{N}$ of the computational history of $\uplus \phi$ applied to a given t-skeleton $\underline{n}_{\boldsymbol{1}}$ ($n \in \mathbb{N}$), so that $T(e^\ddagger, n, c)$ and $\underline{U (c)}_{\boldsymbol{1}} = \uplus \phi \bullet \underline{n}_{\boldsymbol{1}}$ hold.
Finally, $\uplus \mathrm{ct}$ is clearly winning and recursive, which completes the proof.