\section*{Introduction}
Markov's principle has a special status in constructive mathematics. One way to formulate this
principle is that if it is impossible that a given algorithm does not terminate, then it does
terminate. It is equivalent to the fact (Post's theorem) that if a set of natural number and its complement are
both computably enumerable, then this set is decidable \cite[Ch4]{vandalen}. This form is often used in recursion
theory. This principle was first formulated by Markov, who called it ``Leningrad's principle'', 
and founded a branch of constructive mathematics around this principle \cite{Margenstern1995}.

This principle is also equivalent to the fact that if a given real number is {\em not} equal to $0$
then this number is {\em apart} from $0$ (that is this number is $<-r$ or $>r$ for some 
rational number $r>0$). On this form, it was explicitly {\em refuted} by Brouwer in intuitionistic
mathematics, who gave an example of a real number (well defined intuitionistically) which is not
equal to $0$, but also not apart from $0$. (The motivation of Brouwer for this example was to show
the necessity of using {\em negation} in intuitionistic mathematics \cite{brouwer_negative}.) 
The idea of Brouwer can be represented formally using topological models \cite{vanDalen19781}.

In a neutral approach to mathematics, such as Bishop's \cite{Bishop67foundationsof}, Markov's principle is simply
left undecided. We also expect to be able to prove that Markov's principle is {\em not} provable
in formal system in which we can express Bishop's mathematics. For instance, Kreisel \cite{Kreisel1959-KREIOA} introduced {\em modified realizability} to show that Markov's principle is not derivable in the formal
system $HA^{\omega}$. Similarly, one would expect that Markov's principle is {\em not} derivable
in Martin-L\"of type theory \cite{martinloftypes}, but, as far as we know, such a result has not been 
established yet. \footnote{The paper \cite{Hyland93modifiedrealizability} presents a model of the calculus of constructions using the idea of modified
realizability, and it seems possible to use also this technique to interpret the type theory
we consider and prove in this way the independence of Markov's principle.}

We say that a statement $A$ is \emph{independent} of some formal system if $A$ cannot be derived in that system. A statement in the formal system of Martin-L\"of type theory ($\mathrm{MLTT}$) is represented by a closed type. A statement/type $A$ is derivable if it is inhabited by some term $t$ (written $\mathrm{MLTT}\vdash t\!:\! A$). This is the so-called propositions-as-types principle. Correspondingly we say that a statement $A$ (represented as a type) is independent of $\mathrm{MLTT}$ if there is no term $t$ such that $\mathrm{MLTT}\vdash t\!:\! A$.

The main result of this paper is to show that Markov's principle is independent
of Martin-L\"of type theory.\footnote{Some authors define independence in the stronger sense ``A statement is independent of a formal system if neither the statement nor its negation is provable in the system'', e.g.\ \cite{kunen}. We will also establish the independence of Markov's principle in this stronger sense.}

The main idea for proving this independence is to follow Brouwer's argument. We want to extend
type theory with a ``generic'' infinite sequence of $0$ and $1$ and establish that it is both absurd that this
generic sequence is never $0$, but also that we cannot show that it {\em has to} take the value $0$.
To add such a generic sequence is exactly like adding a {\em Cohen real} \cite{cohen} in forcing
extension of set theory. A natural attempt for doing this will be to consider a {\em topological
model} of type theory (sheaf model over Cantor space), extending the work \cite{vanDalen19781} to type
theory. However, while it is well understood how to represent universes in {\em presheaf} model
\cite{liftinggrothendieck}, it has turned out to be surprisingly difficult to represent universes
in {\em sheaf} models, see \cite{sheafuniverse}, \cite{streicher_Universe_in_toposes}. Also see \cite{CoquandMR17} for a possible solution. Our approach is here instead a purely {\em syntactical} description of a forcing extension of type theory (refining previous work of \cite{coquand2010note}),
which contains a formal symbol for the generic sequence and a proof that it is absurd that this generic
sequence is never $0$, together with a {\em normalization} theorem, from which we can deduce that we
{\em cannot} prove that this generic sequence has to take the value $0$. Since this formal system is
an extension of type theory, the independence of Markov's principle follows.

As stated in \cite{Kopylov2001}, which describes an elegant generalization of this principle in type theory,
Markov's principle is an important technical tool for proving termination of computations, and thus
can play a crucial role if type theory is extended with general recursion as in \cite{constablepartial}.


This paper is organized as follows. We first describe the rules of the version of type theory
we are considering. This version can be seen as a simplified version of type theory as represented
in the system Agda \cite{norell:thesis}, and in particular, contrary to the work \cite{coquand2010note}, we allow
$\eta$-conversion, and we express conversion as {\em judgment}. 
Markov's principle can be formulated in a natural way in this formal system.
We describe then the forcing extension of type theory, where we add a Cohen real. For proving
normalization, we follow Tait's computability method \cite{Tait1967-TAIIIO, martinloftypes}, but we have to consider an extension of this with a computability {\em relation} in order to interpret the conversion judgment.
This can be seen as a forcing extension of the technique used in \cite{abelScherer:types10}. Using this computability argument, it is then possible to show that we cannot show that the generic sequence has to take the value $0$.
We end by a refinement of this method, giving a consistent extension of type theory where the
{\em negation} of Markov's principle is provable.

\section{Type theory and forcing extension}
\label{SEC:Forcingextensionoftypetheory}


The syntax of our type theory is given by the grammar:
\begin{align*}
 t,u,A,B  \coloneqq &\, x \mid {\mathsf{rec}_{\mathsf{N}_0}} (\lambda x. A) \mid {\mathsf{rec}_{\mathsf{N}_1}} (\lambda x. A)\,t 
                  \mid {\mathsf{rec}_{\mathsf{N}_2}}(\lambda x. A)\,t\,u \mid {\mathsf{rec}_\mathsf{N}} (\lambda x. A)\,t\,u  \\
                  & \mid \mathsf{U} \mid \mathsf{N}\mid  {\mathsf{N}_0} \mid {\mathsf{N}_1}\mid {\mathsf{N}_2} \mid \mathsf{0} \mid \mathsf{1} \mid \mathsf{S}\,t
                  \mid \Pi (x\!:\! A) B \mid \lambda x. t \mid t\,u \mid \Sigma (x\!:\! A)  B\mid (t, u) \mid t.1 \mid t.2 
\end{align*}

We use the notation $\xoverline{n}$ as a short hand for the term $\mathsf{S}^n\,\mathsf{0}$, where $\mathsf{S}$ is the successor constructor. We will use the symbol $\coloneqq$ for definitional equality in the metatheory.

\subsection{Type system}
We describe a type theory with one universe \`{a} la Russell, natural numbers, functional extensionality and surjective pairing, hereafter referred to as $\mathrm{MLTT}$.\footnote{This is a type system similar to Martin-l{\"o}f's \cite{martinloftypes} except that we have $\eta$-conversion and surjective pairing.}\bigskip

 

\noindent
\textbf{Natural numbers:}
\begin{center} 	
\AxiomC{$\Gamma \vdash$ }
\UnaryInfC{$\Gamma \vdash \mathsf{N}$}
\DisplayProof
\,
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \mathsf{0} \!:\!  \mathsf{N}$}
\DisplayProof
\,
\AxiomC{$\Gamma \vdash n \!:\!  \mathsf{N}$}
\UnaryInfC{$\Gamma \vdash \mathsf{S}\, n \!:\!  \mathsf{N}$}
\DisplayProof 
\,
\AxiomC{$\Gamma \vdash n = m\!:\!  \mathsf{N}$}
\UnaryInfC{$\Gamma \vdash \mathsf{S}\, n = \mathsf{S}\, m\!:\!  \mathsf{N}$}
\DisplayProof \medskip

\begin{prooftree}
\AxiomC{$\Gamma, x\!:\! \mathsf{N} \vdash F$}
\AxiomC{$\Gamma \vdash a_0 \!:\!  F[\mathsf{0}]$}
\AxiomC{$\Gamma \vdash g\!:\!  \Pi (x\!:\! \mathsf{N}) (F[x]\rightarrow F[\mathsf{S}\,x])$}
\TrinaryInfC{$\Gamma \vdash {\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g\!:\!  \Pi (x\!:\! \mathsf{N}) F$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$\Gamma, x\!:\! \mathsf{N} \vdash F$}
\AxiomC{$\Gamma \vdash a_0 \!:\!  F[\mathsf{0}]$}
\AxiomC{$\Gamma \vdash g \!:\!  \Pi (x\!:\! \mathsf{N}) (F[x] \rightarrow F[\mathsf{S}\,x])$}
\TrinaryInfC{$\Gamma \vdash {\mathsf{rec}_\mathsf{N}} (\lambda x. F)\,a_0\, g \,\mathsf{0} = a_0 \!:\!  F[\mathsf{0}]$}
\end{prooftree}


\begin{prooftree}
\AxiomC{$\Gamma, x\!:\! \mathsf{N} \vdash F$}
\AxiomC{$\Gamma \vdash a_0 \!:\!  F[\mathsf{0}]$}
\AxiomC{$\Gamma \vdash n \!:\!  \mathsf{N}$}
\AxiomC{$\Gamma \vdash g \!:\!  \Pi (x\!:\! \mathsf{N}) (F[x] \rightarrow F[\mathsf{S} \,x])$}
\QuaternaryInfC{$\Gamma \vdash {\mathsf{rec}_\mathsf{N}} (\lambda x. F)\,a_0\, g \,(\mathsf{S}\, n) = g\,n \,({\mathsf{rec}_\mathsf{N}} (\lambda x. F)\,a_0\,g\,n) \!:\!  F[\mathsf{S}\,n]$}
\end{prooftree}

\begin{prooftree}
\AxiomC{$\Gamma, x\!:\! \mathsf{N}\vdash F = G$}
\AxiomC{$\Gamma \vdash a_0=b_0 \!:\!  F[\mathsf{0}]$}
\AxiomC{$\Gamma \vdash g=h \!:\!  \Pi (x\!:\! \mathsf{N}) (F[x] \rightarrow F[\mathsf{S} \,x])$}
\TrinaryInfC{$\Gamma \vdash {\mathsf{rec}_\mathsf{N}} (\lambda x. F)\,a_0\, g = {\mathsf{rec}_\mathsf{N}} (\lambda x. G)\,b_0\, h\!:\!  \Pi(x\!:\! \mathsf{N}) F$}
\end{prooftree}
\end{center}\medskip

\noindent
\textbf{Booleans:}

\begin{center}
\AxiomC{$\Gamma \vdash$ }
\UnaryInfC{$\Gamma \vdash {\mathsf{N}_2}$}
\DisplayProof
\,
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \mathsf{0} \!:\!  {\mathsf{N}_2}$}
\DisplayProof
\,
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \mathsf{1} \!:\!  {\mathsf{N}_2}$}
\DisplayProof \,
\AxiomC{$\Gamma, x\!:\! {\mathsf{N}_2} \vdash F$}
\AxiomC{$\Gamma \vdash a_0 \!:\!  F[\mathsf{0}]$}
\AxiomC{$\Gamma \vdash a_1 \!:\!  F[\mathsf{1}]$}
\TrinaryInfC{$\Gamma \vdash {\mathsf{rec}_{\mathsf{N}_2}}(\lambda x. F)\,a_0\, a_1\!:\!  \Pi (x\!:\! {\mathsf{N}_2}) F$}
\DisplayProof \bigskip


\AxiomC{$\Gamma, x\!:\! {\mathsf{N}_2} \vdash F$}
\AxiomC{$\Gamma \vdash a_0 \!:\!  F[\mathsf{0}]$}
\AxiomC{$\Gamma \vdash a_1 \!:\!  F[\mathsf{1}]$}
\TrinaryInfC{$\Gamma \vdash {\mathsf{rec}_{\mathsf{N}_2}} (\lambda x. F)\,a_0\, a_1 \,\mathsf{0} = a_0 \!:\!  F[\mathsf{0}]$}
\DisplayProof
\,
\AxiomC{$\Gamma, x\!:\! {\mathsf{N}_2} \vdash F$}
\AxiomC{$\Gamma \vdash a_0 \!:\!  F[\mathsf{0}]$}
\AxiomC{$\Gamma \vdash a_1 \!:\!  F[\mathsf{1}]$}
\TrinaryInfC{$\Gamma \vdash {\mathsf{rec}_{\mathsf{N}_2}} (\lambda x. F)\,a_0\, a_1 \,\mathsf{1} = a_1 \!:\!  F[\mathsf{1}]$}
\DisplayProof \bigskip

\noindent
\AxiomC{$\Gamma, x\!:\! {\mathsf{N}_2}\vdash F = G$}
\AxiomC{$\Gamma \vdash a_0=b_0 \!:\!  F[\mathsf{0}]$}
\AxiomC{$\Gamma \vdash a_1=b_1 \!:\!  F[\mathsf{1}]$}
\TrinaryInfC{$\Gamma \vdash {\mathsf{rec}_{\mathsf{N}_2}} (\lambda x. F)\,a_0\, a_1 = {\mathsf{rec}_{\mathsf{N}_2}} (\lambda x. G)\,b_0\, b_1\!:\!  \Pi(x\!:\! {\mathsf{N}_2}) F$}
\DisplayProof \bigskip
\end{center}\medskip

\noindent
\textbf{Unit Type:}

\begin{center}
\AxiomC{$\Gamma \vdash$ }
\UnaryInfC{$\Gamma \vdash {\mathsf{N}_1}$}
\DisplayProof
\,
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \mathsf{0} \!:\!  {\mathsf{N}_1}$}
\DisplayProof
\,
\AxiomC{$\Gamma, x\!:\! {\mathsf{N}_1} \vdash F$}
\AxiomC{$\Gamma \vdash a \!:\!  F[\mathsf{0}]$}
\BinaryInfC{$\Gamma \vdash {\mathsf{rec}_{\mathsf{N}_1}}(\lambda x. F)\,a\!:\!  \Pi (x\!:\! {\mathsf{N}_1}) F$}
\DisplayProof \bigskip

\noindent
\AxiomC{$\Gamma, x\!:\! {\mathsf{N}_1} \vdash F$}
\AxiomC{$\Gamma \vdash a \!:\!  F[\mathsf{0}]$}
\BinaryInfC{$\Gamma \vdash {\mathsf{rec}_{\mathsf{N}_1}} (\lambda x. F)\,a \,\mathsf{0} = a \!:\!  F[\mathsf{0}]$}
\DisplayProof
\,
\AxiomC{$\Gamma, x\!:\! {\mathsf{N}_1}\vdash F = G$}
\AxiomC{$\Gamma \vdash a=b \!:\!  F[\mathsf{0}]$}
\BinaryInfC{$\Gamma \vdash {\mathsf{rec}_{\mathsf{N}_1}} (\lambda x. F)\,a = {\mathsf{rec}_{\mathsf{N}_1}} (\lambda x. G)\,b\!:\!  \Pi(x\!:\! {\mathsf{N}_1}) F$}
\DisplayProof 
\end{center}\medskip

\noindent
\textbf{Empty type:}\smallskip

\begin{center}
\AxiomC{$\Gamma \vdash$ }
\UnaryInfC{$\Gamma \vdash {\mathsf{N}_0}$}
\DisplayProof
\,
\noindent
\AxiomC{$\Gamma, x\!:\! {\mathsf{N}_0} \vdash F$}
\UnaryInfC{$\Gamma \vdash {\mathsf{rec}_{\mathsf{N}_0}}(\lambda x. F)\!:\!  \Pi (x\!:\! {\mathsf{N}_0}) F$}
\DisplayProof
\,
\noindent
\AxiomC{$\Gamma, x\!:\! {\mathsf{N}_0}\vdash_p F = G$}
\UnaryInfC{$\Gamma \vdash  {\mathsf{rec}_{\mathsf{N}_0}}(\lambda x. F) =  {\mathsf{rec}_{\mathsf{N}_0}}(\lambda x. G)\!:\!  \Pi (x\!:\! {\mathsf{N}_0}) F$}
\DisplayProof
\end{center}
\medskip

\noindent
\textbf{Dependent functions:}\smallskip

\begin{center}
\AxiomC{$\Gamma \vdash F$ }
\AxiomC{$\Gamma, x\!:\!  F \vdash G$}
\BinaryInfC{$\Gamma \vdash \Pi (x\!:\!  F) G$}
\DisplayProof\,
\noindent
\AxiomC{$\Gamma\vdash F= H$}
\AxiomC{$\Gamma, x\!:\!  F \vdash G =E $}
\BinaryInfC{$\Gamma \vdash \Pi (x\!:\! F) G =\Pi (x\!:\! H) E$}
\DisplayProof\,
\AxiomC{$\Gamma, x \!:\!  F \vdash t \!:\!  G$ }
\UnaryInfC{$\Gamma \vdash \lambda x.t \!:\!  \Pi (x\!:\! F) G$}
\DisplayProof\bigskip

\noindent
\AxiomC{$\Gamma\vdash g \!:\!  \Pi (x\!:\! F) G$}
\AxiomC{$\Gamma\vdash a \!:\!  F$}
\BinaryInfC{$\Gamma \vdash g\,a \!:\!  G[a]$}
\DisplayProof\,
\AxiomC{$\Gamma \vdash g \!:\!  \Pi (x\!:\! F) G$}
\AxiomC{$\Gamma \vdash u =v \!:\!  F$}
\BinaryInfC{$\Gamma \vdash g\,u = g\,v \!:\!  G[u]$}
\DisplayProof
\,
\AxiomC{$\Gamma \vdash h =g \!:\!  \Pi (x\!:\! F) G$}
\AxiomC{$\Gamma \vdash u \!:\!  F$}
\BinaryInfC{$\Gamma \vdash h\,u = g\,u \!:\!  G[u]$}
\DisplayProof \bigskip

\AxiomC{$\Gamma, x\!:\! F \vdash t \!:\!  G$}
\AxiomC{$\Gamma \vdash a \!:\!  F$}
\BinaryInfC{$\Gamma \vdash (\lambda x. t) a = t[a] \!:\!  G[a]$}
\DisplayProof\,
\AxiomC{$\Gamma \vdash h \!:\! \Pi(x\!:\!  F)G$}
\AxiomC{$\Gamma \vdash g \!:\! \Pi(x\!:\!  F) G$}
\AxiomC{$\Gamma, x\!:\! F \vdash h\,x=g\,x \!:\! G[x]$}
\TrinaryInfC{$\Gamma \vdash h = g \!:\!  \Pi(x\!:\!  F)G$}
\DisplayProof \bigskip
\end{center}

\noindent
\textbf{Dependent pairs:}\smallskip
\begin{center}
\AxiomC{$\Gamma \vdash F$ }
\AxiomC{$\Gamma, x\!:\! F \vdash G $}
\BinaryInfC{$\Gamma \vdash \Sigma (x\!:\! F) G$}
\DisplayProof\,
\noindent
\AxiomC{$\Gamma\vdash F = H$}
\AxiomC{$\Gamma, x\!:\!  F \vdash G = E $}
\BinaryInfC{$\Gamma \vdash \Sigma(x\!:\! F)G =\Sigma(x\!:\! H)E$}
\DisplayProof
\,
\AxiomC{$\Gamma, x\!:\! F \vdash G$ }
\AxiomC{$\Gamma \vdash a \!:\!  F$ }
\AxiomC{$\Gamma \vdash b\!:\!  G[a]$}
\TrinaryInfC{$\Gamma \vdash (a, b) \!:\!  \Sigma (x\!:\!  F) G $}
\DisplayProof\bigskip

\AxiomC{$\Gamma\vdash t\!:\!  \Sigma (x\!:\! F) G$ }
\UnaryInfC{$\Gamma \vdash t.1 \!:\!  F$ }
\DisplayProof
\,
\AxiomC{$\Gamma\vdash t\!:\!  \Sigma (x\!:\! F) G$ }
\UnaryInfC{$\Gamma \vdash t.2 \!:\!  G[t.1]$ }
\DisplayProof\,
\AxiomC{$\Gamma, x\!:\! F\vdash G$}
\AxiomC{$\Gamma\vdash t\!:\! F$}
\AxiomC{$\Gamma\vdash u\!:\! G[t]$}
\TrinaryInfC{$\Gamma \vdash (t,u).1=t \!:\!  F$ }
\DisplayProof\bigskip

\AxiomC{$\Gamma, x\!:\! F\vdash G$}
\AxiomC{$\Gamma\vdash t\!:\! F$}
\AxiomC{$\Gamma\vdash u\!:\! G[t]$}
\TrinaryInfC{$\Gamma \vdash (t,u).2=u \!:\!  G[t]$ }
\DisplayProof\,
\AxiomC{$\Gamma \vdash t =u \!:\!  \Sigma (x\!:\! F) G$}
\UnaryInfC{$\Gamma \vdash t.1=u.1\!:\! F$}
\DisplayProof
\,
\AxiomC{$\Gamma \vdash t =u \!:\!  \Sigma (x\!:\! F) G$}
\UnaryInfC{$\Gamma \vdash t.2=u.2\!:\! G[t.1]$}
\DisplayProof \bigskip

\noindent
\AxiomC{$\Gamma\vdash t\!:\!  \Sigma(x\!:\!  F) G$}
\AxiomC{$\Gamma\vdash u\!:\!  \Sigma(x\!:\!  F) G$}
\AxiomC{$\Gamma\vdash t.1=u.1\!:\!  F$ }
\AxiomC{$\Gamma\vdash t.2=u.2\!:\!  G[t.1]$ }
\QuaternaryInfC{$\Gamma \vdash t=u \!:\!  \Sigma(x\!:\! F)G$ }
\DisplayProof
\medskip
\end{center}

\noindent
\textbf{Universe:}\smallskip

\begin{center}
\AxiomC{$\Gamma \vdash$ }
\UnaryInfC{$\Gamma \vdash \mathsf{U}$}
\DisplayProof\,
\AxiomC{$\Gamma \vdash F \!:\!  \mathsf{U}$}
\UnaryInfC{$\Gamma \vdash F$}
\DisplayProof\,
\AxiomC{$\Gamma \vdash F = G\!:\!  \mathsf{U}$}
\UnaryInfC{$\Gamma \vdash F=G$}
\DisplayProof\,
\noindent
\AxiomC{$\Gamma \vdash$ }
\UnaryInfC{$\Gamma \vdash {\mathsf{N}_0} \!:\! \mathsf{U}$}
\DisplayProof
\,
\AxiomC{$\Gamma \vdash$ }
\UnaryInfC{$\Gamma \vdash {\mathsf{N}_1} \!:\! \mathsf{U}$}
\DisplayProof
\,
\AxiomC{$\Gamma \vdash$ }
\UnaryInfC{$\Gamma \vdash {\mathsf{N}_2} \!:\! \mathsf{U}$}
\DisplayProof
\,
\AxiomC{$\Gamma \vdash$ }
\UnaryInfC{$\Gamma \vdash \mathsf{N} \!:\! \mathsf{U}$}
\DisplayProof\bigskip



\noindent
\AxiomC{$\Gamma \vdash F \!:\! \mathsf{U}$ }
\AxiomC{$\Gamma, x\!:\!  F \vdash G \!:\! \mathsf{U}$}
\BinaryInfC{$\Gamma \vdash \Pi (x\!:\!  F) G \!:\! \mathsf{U}$}
\DisplayProof\medskip
\,
\AxiomC{$\Gamma\vdash F= H \!:\! \mathsf{U}$}
\AxiomC{$\Gamma, x\!:\!  F \vdash G =E \!:\! \mathsf{U}$}
\BinaryInfC{$\Gamma \vdash \Pi (x\!:\! F) G =\Pi (x\!:\! H) E \!:\! \mathsf{U}$}
\DisplayProof\bigskip

\noindent
\AxiomC{$\Gamma \vdash F \!:\! \mathsf{U}$ }
\AxiomC{$\Gamma, x\!:\!  F \vdash G \!:\! \mathsf{U}$}
\BinaryInfC{$\Gamma \vdash \Sigma (x\!:\!  F) G\!:\!  \mathsf{U}$}
\DisplayProof\medskip
\,
\AxiomC{$\Gamma\vdash F= H \!:\! \mathsf{U}$}
\AxiomC{$\Gamma, x\!:\!  F \vdash G =E \!:\! \mathsf{U}$}
\BinaryInfC{$\Gamma \vdash \Sigma (x\!:\! F) G =\Sigma (x\!:\! H) E \!:\! \mathsf{U}$}
\DisplayProof\medskip
\end{center}
\noindent
\textbf{Congruence:}

\begin{center}
\noindent
\AxiomC{$\Gamma \vdash F$}
\UnaryInfC{$\Gamma \vdash F=F$}
\DisplayProof\,
\AxiomC{$\Gamma \vdash F=G$}
\UnaryInfC{$\Gamma \vdash G=F$}
\DisplayProof\,
\AxiomC{$\Gamma \vdash F=G$}
\AxiomC{$\Gamma \vdash G=H$}
\BinaryInfC{$\Gamma \vdash F=H$}
\DisplayProof\,
\AxiomC{$\Gamma \vdash t\!:\! F$}
\UnaryInfC{$\Gamma \vdash t=t\!:\! F$}
\DisplayProof\,
\AxiomC{$\Gamma \vdash t=u\!:\! F$}
\UnaryInfC{$\Gamma \vdash u=t\!:\! F$}
\DisplayProof\bigskip

\AxiomC{$\Gamma \vdash t=u\!:\! F$}
\AxiomC{$\Gamma \vdash u=v \!:\! F$}
\BinaryInfC{$\Gamma \vdash t=v \!:\! F$}
\DisplayProof\,
\AxiomC{$\Gamma \vdash t\!:\! F$}
\AxiomC{$\Gamma \vdash F = G$}
\BinaryInfC{$\Gamma \vdash t\!:\! G$}
\DisplayProof\,
\AxiomC{$\Gamma \vdash t=u\!:\! F$}
\AxiomC{$\Gamma \vdash F = G$}
\BinaryInfC{$\Gamma \vdash t=u\!:\! G$}
\DisplayProof \bigskip

\AxiomC{$\Gamma \vdash a\!:\! A$}
\AxiomC{$\Gamma \vdash A=B$}
\BinaryInfC{$\Gamma \vdash a \!:\! B$}
\DisplayProof
\,
\AxiomC{$\Gamma \vdash a=b\!:\! A$}
\AxiomC{$\Gamma \vdash A=B$}
\BinaryInfC{$\Gamma \vdash a=b \!:\! B$}
\DisplayProof\bigskip

\end{center}

\normalsize


\noindent
The following four rules are admissible in the this type system \cite{abelScherer:types10}, we consider them as rules of our type system:\medskip

\noindent
\AxiomC{$\Gamma \vdash a\!:\! A$}
\UnaryInfC{$\Gamma\vdash A$}
\DisplayProof
\,
\AxiomC{$\Gamma\vdash a=b \!:\! A$}
\UnaryInfC{$\Gamma\vdash a \!:\! A$}
\DisplayProof
\,
\AxiomC{$\Gamma, x\!:\! F\vdash G$}
\AxiomC{$\Gamma\vdash a=b\!:\! F$}
\BinaryInfC{$\Gamma\vdash G[a]=G[b]$}
\DisplayProof
\,
\AxiomC{$\Gamma, x\!:\! F\vdash t \!:\! G$}
\AxiomC{$\Gamma\vdash a=b\!:\! F$}
\BinaryInfC{$\Gamma\vdash t[a]=t[b] \!:\! G[a]$}
\DisplayProof\medskip
\,
\AxiomC{$\Gamma \vdash A = B$}
\UnaryInfC{$\Gamma \vdash A$}
\DisplayProo


\subsection{Markov's principle}

Markov's principle can be represented in type theory by the type 
\begin{equation*}
\mathsf{MP}\coloneqq \Pi(h\!:\! \mathsf{N}\rightarrow {\mathsf{N}_2})[\neg\neg (\Sigma (x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(h\,x)) \rightarrow \Sigma (x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(h\,x)]
\end{equation*}
where $\mathsf{IsZero}\!:\! {\mathsf{N}_2} \rightarrow \mathsf{U}$ is defined by $\mathsf{IsZero} \coloneqq \lambda y.{\mathsf{rec}_{\mathsf{N}_2}} (\lambda x. \mathsf{U})\,{\mathsf{N}_1}\,{\mathsf{N}_0}\,y$. 

Note that $\mathsf{IsZero}\,(h\,n)$ is inhabited when $h\,n = 0$ and empty when $h\,n = 1$. Thus $\Sigma(x\!:\! \mathsf{N}) \,\mathsf{IsZero}\,(h\,x)$ is inhabited if there is $n$ such that $h\,n = 0$. 

We remark that in the presence of propositional truncation $\parallel . \parallel$, Markov's principle can be alternatively formulated with weak (propositional) existential $\exists (x\!:\! A) B \coloneqq \parallel \Sigma (x\!:\! A) B\parallel$. However, the two formulations are logically equivalent \cite[Exercise 3.19]{hottbook}.

The main result of this paper is the following:

\begin{restatable}{thm}{mainresult}
\label{THM:mainResult}
There is no term $t$ such that $\mathrm{MLTT}\vdash t\!:\! \mathsf{MP}$.
\end{restatable}


An {\em extension} of $\mathrm{MLTT}$ is given by introducing new objects, judgment forms and derivation rules. This means in particular that any judgment valid in $\mathrm{MLTT}$ is valid in the extension.  A {\em consistent} extension is one in which the type ${\mathsf{N}_0}$ is uninhabited.

To show Theorem \ref{THM:mainResult} we will form a consistent extension of $\mathrm{MLTT}$ with a new constant $\vdash \mathsf{f} \!:\! \mathsf{N}\rightarrow {\mathsf{N}_2}$. We will then show that $\neg\neg (\Sigma (x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(\mathsf{f}\,x))$ is derivable while $\Sigma (x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(\mathsf{f}\,x)$ is not derivable. Thus showing that $\mathsf{MP}$ is not derivable in this extension and consequently not derivable in $\mathrm{MLTT}$. 

While this is sufficient to establish independence in the sense of non-derivability of $\mathrm{MP}$, to establish the independence of $\mathrm{MP}$ in the stronger sense one also needs to show that $\neg \mathsf{MP}$ is not derivable in $\mathrm{MLTT}$. This can achieved by reference to the work of Aczel \cite{Aczel1999} where it is shown that $\mathrm{MLTT}$ extended with $\vdash \mathsf{dne} \!:\! \Pi(A\!:\! \mathsf{U}) (\neg \neg A \rightarrow A)$ is consistent. Since $h\!:\! \mathsf{N}\rightarrow {\mathsf{N}_2}, x\!:\! \mathsf{N} \vdash \mathsf{IsZero}\,(h\,x) \!:\! \mathsf{U}$ we have $h\!:\! \mathsf{N}\rightarrow {\mathsf{N}_2}\vdash \Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(h\,x)\!:\! \mathsf{U}$. If we let $\mathsf{T}(h)\coloneqq \Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(h\,x)$ we get that $h\!:\! \mathsf{N} \rightarrow {\mathsf{N}_2} \vdash \mathsf{dne}\, \mathsf{T}(h) \!:\! \neg \neg \mathsf{T}(h) \rightarrow \mathsf{T}(h)$.
By $\lambda$ abstraction we have $\vdash \lambda h. \mathsf{dne}\,T(h) \!:\! \mathsf{MP}$. We can then conclude that there is no term $t$ such that $\mathrm{MLTT} \vdash t\!:\! \neg \mathsf{MP}$.


Finally, we will refine the result of Theorem \ref{THM:mainResult} by building a consistent extension of $\mathrm{MLTT}$ where $\neg \mathsf{MP}$ is derivable. 


\subsection{Forcing extension}

A \emph{condition} $p$ is a graph of a partial finite function from $\mathbb{N}$ to $\{\mathsf{0},\mathsf{1}\}$. We denote by $\emptyset$ the empty condition. We write $p(n)=b$ when $(n,b) \in p$. We say $q$ \emph{extends} $p$ (written $q \leqslant p$) if $p$ is a subset of $q$. A condition can be thought of as a basic compact open in Cantor space $2^\mathbb{N}$. Two conditions $p$ and $q$ are \emph{compatible} if $p\cup q$ is a condition and we write $p
q$ for $p\cup q$. If $n\notin \dom{p}$ we write $p(n\mapsto \mathsf{0})$ for $p\cup\{(n,\mathsf{0})\}$ and $p(n\mapsto \mathsf{1})$ for $p\cup\{(n,\mathsf{1})\}$. We define the notion of \emph{partition} corresponding to the notion of finite covering of a compact open in Cantor space.

\begin{defi}We write $p\vartriangleleft S$ to say that $S$ is a partition of $p$ and we define it inductively as follows:
\begin{enumerate}
\item $p \vartriangleleft \{p\}$.
\item If $n\notin \dom{p}$ and $p(n\mapsto \mathsf{0})\vartriangleleft S_0$ and $p(n\mapsto \mathsf{1})\vartriangleleft S_1 $ then $p \vartriangleleft S_0 \cup S_1$.
\end{enumerate}
\end{defi}

Note that if $p\vartriangleleft S$ then any $q\in S$ and $r\in S$ are incompatible unless $q=r$. If moreover $s \leqslant p$ then $s \vartriangleleft \{sq \mid q\in S \text{ compatible with } s\}$. 

We extend the given type theory by annotating the judgments with conditions, i.e.\ replacing each judgment $\Gamma \vdash J$ in the given type system with a judgment $\Gamma\vdash_p J$.\medskip

In addition, we add the locality rule: 
\AxiomC{$\Gamma \vdash_{p_1} J$}
\AxiomC{$\dots$}
\AxiomC{$\Gamma \vdash_{p_n} J $} 
\def1pt{1pt}
\LeftLabel{\scriptsize{\textsc{loc}}}
\RightLabel{$p \vartriangleleft \{p_1,\dots, p_n\}$}
\TrinaryInfC{$\Gamma \vdash_p J $}
\DisplayProof\smallskip

We add a term $\mathsf{f}$ for the generic point along with the introduction and conversion rules:\smallskip
\begin{center}
\AxiomC{$\Gamma \vdash_p$}
\LeftLabel{\scriptsize{\textsc{$\mathsf{f}$-I}}}
\UnaryInfC{$\Gamma \vdash_p \mathsf{f} \!:\!  \mathsf{N} \rightarrow {\mathsf{N}_2}$}
\DisplayProof\,
\AxiomC{$\Gamma \vdash_p$}
\LeftLabel{\scriptsize{\textsc{$\mathsf{f}$-eval}}}
\RightLabel{$n \in \dom{p}$}
\UnaryInfC{$\Gamma \vdash_p \mathsf{f}\,\xoverline{n} = p(n)\!:\! {\mathsf{N}_2}$}
\DisplayProof \bigskip
\end{center}

We add a term $\mathsf{w}$ and the rule: 
\begin{center}
\AxiomC{$\Gamma \vdash_p$}
\LeftLabel{\scriptsize{\textsc{$\mathsf{w}$-term}}}
\UnaryInfC{$\Gamma \vdash_p \mathsf{w}\!:\!  \neg \neg (\Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(\mathsf{f}\,x)) $}
\DisplayProo
\end{center}

Since $\mathsf{w}$ inhabits the type $\neg \neg (\Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(\mathsf{f}\,x))$, our goal is then to show that no term inhabits the type $\Sigma (x\!:\! \mathsf{N})\, \mathsf{IsZero}(\mathsf{f}\,x)$.

It follows directly from the description of the forcing extension that:
\begin{lem}
\label{LEM:extension}
If $\Gamma\vdash J$ in standard type theory then $\Gamma \vdash_{\emptyset} J$.
\end{lem}
Note that if $q\leqslant p$ and $\Gamma\vdash_p J$ then $\Gamma\vdash_q J$ (monotonicity). A statement $A$ (represented as a closed type) is derivable in this extension if $\vdash_{\emptyset} t\!:\! A$ for some $t$, which implies $\vdash_p t\!:\! A$ for all $p$. 

Similarly to \cite{coquand2010note} we can state a conservativity result for this extension. Let $\vdash g\!:\! \mathsf{N}\rightarrow {\mathsf{N}_2}$. 
 We say that $g$ is compatible with a condition $p$ if $g$ is such that $\vdash g\,\xoverline{n} = b \!:\! {\mathsf{N}_2}$ whenever $(n,b) \in p$ and $\vdash g\,\xoverline{n} = \mathsf{0}\!:\! {\mathsf{N}_2}$ otherwise. 
 We write $n_g$ for the smallest natural number such that $g\, \xoverline{n}_g = \mathsf{0}$. Let $v_g \!:\! \neg \neg (\Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(g\,x))$ be the term given by $v_g\coloneqq \lambda x. x\,(\xoverline{n}_g,\mathsf{0})\!:\! \neg \neg (\Sigma(y\!:\! \mathsf{N})\,\mathsf{IsZero}\,(g\,y))$. 
 To see that $v_g$ is well typed, note that by design $\Gamma\vdash g\,\xoverline{n}_g = \mathsf{0} \!:\! {\mathsf{N}_2}$ thus $\Gamma\vdash \mathsf{IsZero}\,(g\,\xoverline{n}_g) = {\mathsf{N}_1}$ and $\Gamma \vdash (\xoverline{n}_g,\mathsf{0}) \!:\! \Sigma(x\!:\! \mathsf{N}) \mathsf{IsZero}\,(g\,x)$. 
 We have then $\Gamma, x\!:\! \neg (\Sigma(y\!:\! \mathsf{N})\,\mathsf{IsZero}\,(g\,y))\vdash x\,(\xoverline{n}_g,\mathsf{0})\!:\! {\mathsf{N}_0}$, thus $\Gamma\vdash \lambda x. x\, (\xoverline{n}_g,\mathsf{0}) \!:\! \neg \neg (\Sigma(y\!:\! \mathsf{N})\,\mathsf{IsZero}\,(g\,y))$.
 

\begin{lem}[Conservativity]
Let $\vdash g \!:\! \mathsf{N}\rightarrow {\mathsf{N}_2}$ be compatible with some condition $p$. If $\Gamma \vdash_p J$ then $\Gamma[g/\mathsf{f},v_g/\mathsf{w}] \vdash J[g/\mathsf{f},v_g/\mathsf{w}]$, i.e.\ by replacing $\mathsf{f}$ with $g$ then $\mathsf{w}$ with $v_g$  we obtain a valid judgment in standard type theory. In particular, if we have $\Gamma\vdash_{\emptyset} J$ where neither $\mathsf{f}$ nor $\mathsf{w}$ occur in $\Gamma$ or $J$ then $\Gamma\vdash J$ is a valid judgment in standard type theory.
\end{lem}
\begin{proof}
We show that whenever the statement holds for the premise of a typing rule it holds for the conclusion. The statement will then follow by induction on the derivation tree of $\Gamma \vdash_p J$. 
 
 For the standard rules the proof is straightforward. For (\textsc{$\mathsf{f}$-eval}) we have $(\mathsf{f}\,\xoverline{n})[g/\mathsf{f}, v_g/\mathsf{w}] \coloneqq g\,\xoverline{n}$ and since $g$ is compatible with $p$ we have $\Gamma[g/\mathsf{f}, v_g/\mathsf{w}]\vdash g\,\xoverline{n}= p(n)\!:\! {\mathsf{N}_2}$ whenever $n\in \dom{p}$. For (\textsc{$\mathsf{w}$-term}) we have 
\begin{align*}
(\mathsf{w}\!:\!\neg\neg (\Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(\mathsf{f}\,x)))[g/\mathsf{f}, v_g/\mathsf{w}] &\coloneqq (\mathsf{w}\!:\!\neg\neg (\Sigma(x\!:\! \mathsf{N})\, \mathsf{IsZero}\,(g\,x)))[v_g/\mathsf{w}]\\
& \coloneqq v_g\!:\!\neg\neg (\Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero} \,(g\,x)). 
\end{align*}

For (\textsc{loc}) the statement follows from the observation that when $g$ is compatible with $p$ and $p\vartriangleleft S$ then $g$ is compatible with exactly one $q \in S$. From $\Gamma \vdash_q J$ by IH we get $\Gamma[g/\mathsf{f},v_g/\mathsf{w}] \vdash J[g/\mathsf{f},v_g/\mathsf{w}]$.
\end{proof}


\section{A Semantics of the forcing extension}
\label{SEC:semantics}

In this section we outline a semantics for the forcing extension given in the previous section. We will interpret the judgments of type theory by computability predicates and relations defined by reducibility to computable weak head normal forms.

\subsection{Reduction rules}
We extend the $\beta, \iota$ conversion with $\mathsf{f}\,\xoverline{n} \rightarrowtriangle_p b$ whenever $(n,b) \in p$. To ease the presentation of the proofs and definitions we introduce {\em evaluation contexts} following \cite{WRIGHT199438}.
\begin{align*}
\mathbb{E}\Coloneqq & [\;] \mid \mathbb{E}\, u \mid \mathbb{E}.1 \mid \mathbb{E}.2 \mid \mathsf{S}\,\mathbb{E} \mid \mathsf{f}\, \mathbb{E}\\
& {\mathsf{rec}_{\mathsf{N}_0}} (\lambda x. C)\,\mathbb{E} \mid {\mathsf{rec}_{\mathsf{N}_1}} (\lambda x. C)\,a\,\mathbb{E}
\mid {\mathsf{rec}_{\mathsf{N}_2}} (\lambda x. C)\, a_0\,a_1\,\mathbb{E}\mid {\mathsf{rec}_\mathsf{N}} (\lambda x. C)\, c_z\,g\,\mathbb{E}
\end{align*}

An expression $\mathbb{E}[e]$ is then the expression resulting from replacing the hole $[\;]$ by $e$. 

We have the following reduction rules:

\AxiomC{\vphantom{$\vdash$}}
\UnaryInfC{${\mathsf{rec}_{\mathsf{N}_1}} (\lambda x. C)\;c\;\mathsf{0} \rightarrowtriangle c $}
\DisplayProof
\,
\AxiomC{$\vphantom{\vdash}$}
\UnaryInfC{${\mathsf{rec}_{\mathsf{N}_2}} (\lambda x. C)\,c_0\,c_1\,\mathsf{0} \rightarrowtriangle c_0$}
\DisplayProof
\,
\AxiomC{$\vphantom{\vdash}$}
\UnaryInfC{${\mathsf{rec}_{\mathsf{N}_2}} (\lambda x. C)\,c_0\,c_1\,\mathsf{1} \rightarrowtriangle c_1$}
\DisplayProof\smallskip


\AxiomC{$\vphantom{\vdash}$}
\UnaryInfC{${\mathsf{rec}_\mathsf{N}} (\lambda x. C)\,c_z\,g\,\mathsf{0} \rightarrowtriangle c_z$}
\DisplayProof
\,
\AxiomC{$\vphantom{\vdash}$}
\UnaryInfC{${\mathsf{rec}_\mathsf{N}} (\lambda x. C)\,c_z\,g\,(\mathsf{S}\,\xoverline{k}) \rightarrowtriangle g\,\xoverline{k}\, ({\mathsf{rec}_\mathsf{N}} (\lambda x. C)\,c_z\,g\,\xoverline{k})$}
\DisplayProof\medskip


\AxiomC{$\vphantom{\vdash}$}
\UnaryInfC{$(\lambda x. t)\, a \rightarrowtriangle t[a/x]$}
\DisplayProof
\,
\AxiomC{\vphantom{$\vdash$}}
\UnaryInfC{$(u,v).1 \rightarrowtriangle u$}
\DisplayProof
\,
\AxiomC{\vphantom{$\vdash$}}
\UnaryInfC{$(u,v).2 \rightarrowtriangle v$}
\DisplayProof\medskip


\AxiomC{$e\rightarrowtriangle e'$}
\UnaryInfC{$e\rightarrowtriangle_p e'$}
\DisplayProof
\,
\AxiomC{$k \in \dom{p}$}
\LeftLabel{\scriptsize{\textsc{$\mathsf{f}$-red}}}
\UnaryInfC{$\mathsf{f}\,\xoverline{k} \rightarrowtriangle_p p(k)$}
\DisplayProof
\,
\AxiomC{$e\rightarrowtriangle_p e'$}
\UnaryInfC{$\mathbb{E}[e]\rightarrowtriangle_p \mathbb{E}[e']$}
\DisplayProof\medskip

Note that we reduce under $\mathsf{S}$. Also note that the relation $\rightarrowtriangle$ is monotone, that is if $q \leqslant p$ and $t \rightarrowtriangle_p u$ then $t \rightarrowtriangle_q u$. In the following we will show that $\rightarrowtriangle$ is also local, i.e.\ if $p\vartriangleleft S$ and $t\rightarrowtriangle_q u$ for all $q\in S$ then $t\rightarrowtriangle_p u$. 

\begin{lem}
\label{untypedredislocal}
If $m\notin \dom{p}$ and $t\rightarrowtriangle_{p(m\mapsto \mathsf{0})} u$ and $t\rightarrowtriangle_{p(m\mapsto \mathsf{1})} u$ then $t\rightarrowtriangle_p u$.
\end{lem}
\begin{proof}
By induction on the derivation of $t\rightarrowtriangle_{p(m\mapsto \mathsf{0})} u$. If  $t\rightarrowtriangle_{p(m\mapsto \mathsf{0})} u$ is derived by (\textsc{$\mathsf{f}$-red}) then $t\coloneqq \mathsf{f}\,\xoverline{k}$ and $u\coloneqq p(m\mapsto \mathsf{0})(k)$ for some $k\in \dom{p(m\mapsto \mathsf{0})}$. But since we also have a reduction $\mathsf{f}\,\xoverline{k}\rightarrowtriangle_{p(m\mapsto \mathsf{1})} u$,  we have $p(m\mapsto \mathsf{1})(k) \coloneqq u \coloneqq p(m\mapsto \mathsf{0})(k)$ which could only be the case if $k\in \dom{p}$. Thus we have a reduction $\mathsf{f}\,\xoverline{k} \rightarrowtriangle_p u\coloneqq p(k)$. If on the other hand we have a derivation $t\rightarrowtriangle u$, then we have $t\rightarrowtriangle_p u$ directly. If the derivation $t\rightarrowtriangle_{p(m\mapsto \mathsf{0})} u$ has the form $\mathbb{E}[e]\rightarrowtriangle_{p(m\mapsto \mathsf{0})} \mathbb{E}[e']$ then we have also $\mathbb{E}[e]\rightarrowtriangle_{p(m\mapsto \mathsf{1})} \mathbb{E}[e']$. Hence, $e\rightarrowtriangle_{p(m\mapsto \mathsf{0})} e'$ and $e\rightarrowtriangle_{p(m\mapsto \mathsf{1})} e'$. By IH $e\rightarrowtriangle_p e'$, thus $\mathbb{E}[e]\rightarrowtriangle_p \mathbb{E}[e']$.
\end{proof}


\begin{lem}
\label{reductionislevelbehaved}
Let $q\leqslant p$. If $t\rightarrowtriangle_q u$ then $t\rightarrowtriangle_p u$ or $t$ has the form $\mathbb{E}[\mathsf{f}\,\xoverline{m}]$ for some $m\in \dom{q}\setminus \dom{p}$.
\end{lem}
\begin{proof}
By induction on the derivation of $t\rightarrowtriangle_q u$. If the reduction $t\rightarrowtriangle_q u$ has the form $\mathsf{f}\,\xoverline{k} \rightarrowtriangle_q q(k)$ then either $k\notin\dom{p}$ and the statement follows or $k\in \dom{p}$ and we have $t\rightarrowtriangle_p u$. If on the other hand we have $t\rightarrowtriangle u$ then $t\rightarrowtriangle_p u$ immediately.
If $t\rightarrowtriangle_q u$ has the form $\mathbb{E}[e] \rightarrowtriangle_q \mathbb{E}[e']$ then $e\rightarrowtriangle_q e'$ and the statement follows by induction.
\end{proof}

\begin{cor}
\label{eitherreduceorstuck}
Let $t\rightarrowtriangle_{p(m\mapsto \mathsf{0})} u$ and $t\rightarrowtriangle_{p(m\mapsto \mathsf{1})} v$ for some $m\notin\dom{p}$. If $u\coloneqq v$ then $t\rightarrowtriangle_p u$; otherwise, $t$ has the form $\mathbb{E}[\mathsf{f}\,\xoverline{m}]$.
\end{cor}


Define $p\vdash t\rightarrowtriangle u \!:\! A$ to mean $t\rightarrowtriangle_p u$ and $\vdash_p t=u \!:\! A$ and write $p\vdash A\rightarrowtriangle B$ for $p\vdash A\rightarrowtriangle B\!:\! \mathsf{U}$. 

Note that it holds that if $p\vdash t\rightarrowtriangle u\!:\! \Pi(x\!:\! F) G$ and $\vdash a\!:\! F$ then $p\vdash t\,a\rightarrowtriangle u\,a \!:\! G[a]$ and if $p\vdash t\rightarrowtriangle u \!:\! \Sigma(x\!:\! F) G$ then $p\vdash t.1 \rightarrowtriangle u.1 \!:\! F$ and $p\vdash t.2 \rightarrowtriangle u.2 \!:\! G[t.1]$. 

We define a closure for this relation as follows:\medskip
\begin{center}
\AxiomC{$\vdash_p t\!:\! A$}
\UnaryInfC{$p\vdash t \red^\ast t \!:\! A$}
\DisplayProof
\,
\AxiomC{$p\vdash t \rightarrowtriangle u\!:\! A$}
\UnaryInfC{$p\vdash t \red^\ast u\!:\! A$}
\DisplayProof
\,
\AxiomC{$p\vdash t \rightarrowtriangle u \!:\! A$}
\AxiomC{$p\vdash u \red^\ast v \!:\! A$}
\BinaryInfC{$p\vdash t \red^\ast v\!:\! A$}
\DisplayProof\smallskip


\AxiomC{$\vdash_p A$}
\UnaryInfC{$p\vdash A\red^\ast A$}
\DisplayProof
\;\;\;
\AxiomC{$p\vdash A \rightarrowtriangle B$}
\UnaryInfC{$p\vdash A \red^\ast B$}
\DisplayProof
\;\;\;
\AxiomC{$p\vdash A \rightarrowtriangle B $}
\AxiomC{$p\vdash B \red^\ast C $}
\BinaryInfC{$p\vdash A \red^\ast C$}
\DisplayProof
\end{center}\smallskip


A term $t$ is {\em in} $p$-whnf if whenever $p\vdash t \red^\ast u\!:\! A$ then $t\coloneqq u$. 

A whnf is \emph{canonical} if it has one of the forms:
\begin{align*}
& \mathsf{0},\mathsf{1},\xoverline{n}, \lambda x. t, (a,b), \mathsf{f}, \mathsf{w}, {\mathsf{N}_0},{\mathsf{N}_1},{\mathsf{N}_2},\mathsf{N},\mathsf{U},\Pi(x\!:\! F) G, \Sigma(x\!:\! F) G,\\
& {\mathsf{rec}_{\mathsf{N}_0}} (\lambda x. C), {\mathsf{rec}_{\mathsf{N}_1}} (\lambda x. C)\,a, {\mathsf{rec}_{\mathsf{N}_2}} (\lambda x. C)\, a_0\,a_1, {\mathsf{rec}_\mathsf{N}} (\lambda x. C)\, c_z\,g
\end{align*}

A $p$-whnf is \emph{proper} if it is canonical or it is of the form $\mathbb{E}[\mathsf{f}\,\xoverline{k}]$ for $k\notin\dom {p}$. 

A canonical $p$-whnf has no further reduction at any $q\leqslant p$. A non-canonical proper $p$-whnf, i.e.\ of the form $\mathbb{E}[\mathsf{f}\,\xoverline{k}]$ for $k\notin\dom{p}$, have further reduction at some $q\leqslant p$, namely when $k\in \dom{q}$.

We have the following corollaries to Lemma~\ref{untypedredislocal} and Corollary~\ref{eitherreduceorstuck}.

\begin{cor}
\label{typedreduceorstuck}
Let $m\notin \dom{p}$. Let $p(m\mapsto \mathsf{0}) \vdash t\rightarrowtriangle u\!:\! A$ and $p(m\mapsto \mathsf{1})\vdash t\rightarrowtriangle v\!:\! A$. If $u\coloneqq v$ then $p\vdash t\rightarrowtriangle u \!:\! A$; otherwise $t$ has the form  $\mathbb{E}[\mathsf{f}\,\xoverline{m}]$.
\end{cor}

\begin{cor}
\label{onestepredmonolocal}
Let $p\vartriangleleft S$ and $q \vdash t\rightarrowtriangle u \!:\! A$ for all $q\in S$. We have $p\vdash t\rightarrowtriangle u \!:\! A$.
\end{cor}
\begin{proof}
By induction on $S$. If $S\coloneqq \{p\}$ the the statement follows. Assume the statement holds for $p(m\mapsto \mathsf{0})\vartriangleleft S_0$ and $p(m\mapsto \mathsf{1})\vartriangleleft S_1$ and let $S\coloneqq S_0 \cup S_1$. By IH, $p(m\mapsto \mathsf{0})\vdash t\rightarrowtriangle u\!:\! A$ and $p(m\mapsto \mathsf{1})\vdash t\rightarrowtriangle u\!:\! A$. From Lemma~\ref{untypedredislocal}, $t\rightarrowtriangle_p u$. Since $\vdash_{p(m\mapsto \mathsf{0})} t=u\!:\! A$ and $\vdash_{p(m\mapsto \mathsf{1})} t=u\!:\! A$, then $\vdash_p t=u\!:\! A$. Thus $p\vdash t\rightarrowtriangle u\!:\! A$.
\end{proof}


Note that if $q\leqslant p$ and $p\vdash t\red^\ast u \!:\! A$ then $q\vdash t\red^\ast u\!:\! A$. However if $p(m\mapsto \mathsf{0})\vdash t\red^\ast u\!:\! A$ and $p(m\mapsto \mathsf{1})\vdash t\red^\ast u\!:\! A$ it is not necessarily the case that $p\vdash t\red^\ast u\!:\! A$. E.g.\ we have that $\{(m,\mathsf{0})\}\vdash {\mathsf{rec}_{\mathsf{N}_2}} (\lambda x. \mathsf{N})\,\xoverline{n}\,\xoverline{n}\,(\mathsf{f}\,\xoverline{m}) \red^\ast \xoverline{n}\!:\! \mathsf{N}$ and $\{(m,\mathsf{1})\}\vdash {\mathsf{rec}_{\mathsf{N}_2}} (\lambda x. \mathsf{N})\,\xoverline{n}\,\xoverline{n}\,(\mathsf{f}\,\xoverline{m}) \red^\ast \xoverline{n}\!:\! \mathsf{N}$ but it is \emph{not} true that $\emptyset\vdash {\mathsf{rec}_{\mathsf{N}_2}} (\lambda x. \mathsf{N}) \,\xoverline{n}\,\xoverline{n}\,(\mathsf{f}\,\xoverline{m}) \red^\ast \xoverline{n}\!:\! \mathsf{N}$.

For a closed term $\vdash_p t\!:\! A$, we say that $t$ {\em has} a $p$-whnf if $p\vdash t\red^\ast  u \!:\! A$ and $u$ is in $p$-whnf. If $u$ is canonical, respectively proper, we say that $t$ has a canonical, respectively proper, $p$-whnf.  

Since the reduction relation is deterministic we have:

\begin{lem}
\label{LEM:uniquenessofwhnf}
A term $\vdash_p t\!:\! A$ has at most one $p$-whnf.
\end{lem}

\begin{cor}
\label{properwhnflocal}
Let $\vdash_p t\!:\! A$ and $m\notin \dom{p}$. If $t$ has proper $p(m\mapsto \mathsf{0})$-whnf and a proper $p(m\mapsto \mathsf{1})$-whnf then $t$ has a proper $p$-whnf. 
\end{cor}
\begin{proof}
Let $p(m\mapsto \mathsf{0})\vdash t\red^\ast u\!:\! A$ and $p(m\mapsto \mathsf{1})\vdash t\red^\ast v\!:\! A$ with $u$ in proper $p(m\mapsto \mathsf{0})$-whnf and $v$ in proper $p(m\mapsto \mathsf{1})$-whnf. If $t\coloneqq u$ or $t\coloneqq v$ then $t$ is already in proper $p$-whnf. Alternatively we have reductions $p(m\mapsto \mathsf{0})\vdash t\rightarrowtriangle u_1\!:\! A$ and $p(m\mapsto \mathsf{1})\vdash t\rightarrowtriangle v_1 \!:\! A$. By Corollary~\ref{typedreduceorstuck} either $t$ is in proper $p$-whnf or $u_1\coloneqq v_1$ and $p\vdash t\rightarrowtriangle u_1 \!:\! A$. It then follows by induction that $u_1$, and thus $t$, has a proper $p$-whnf.
\end{proof}

\subsection{Computability predicate and relation}
We define inductively a forcing relation $p\Vdash A$ to express that a type $A$ is computable at $p$. Mutually by recursion we define relations $p\Vdash a\!:\! A$ ($a$ computable of type $A$ at $p$), $p\Vdash A=B$ ($A$ and $B$ are computably equal at $p$), and $p\Vdash a=b \!:\! A$ ($a$ is computably equal to $b$ of type $A$ at $p$).
The definition fits the generalized mutual induction-recursion schema \cite{dybjer_inductive-recursive}\footnote{However, for the canonical proof below we actually need something weaker than an
inductive-recursive definition (arbitrary fixed-point instead of {\em least} fixed-point), reflecting
the fact that the universe is defined in an open way \cite{martinloftypes}.}.


The following rules have an implicit (hidden) premise $\vdash_p A$\medskip
\begin{center}
\AxiomC{$p\vdash A \red^\ast {\mathsf{N}_0}$}
\LeftLabel{\scriptsize{$\mathrm{F}_{\mathsf{N}_0}$}}
\UnaryInfC{$p\Vdash A$}
\DisplayProof
\,
\AxiomC{$p\vdash A \red^\ast {\mathsf{N}_1}$}
\LeftLabel{\scriptsize{$\mathrm{F}_{\mathsf{N}_1}$}}
\UnaryInfC{$p\Vdash A$}
\DisplayProof
\,
\AxiomC{$p\vdash A \red^\ast {\mathsf{N}_2}$}
\LeftLabel{\scriptsize{$\mathrm{F}_{\mathsf{N}_2}$}}
\UnaryInfC{$p\Vdash A$}
\DisplayProof
\,
\AxiomC{$p\vdash A \red^\ast \mathsf{N}$}
\LeftLabel{\scriptsize{$\mathrm{F}_\mathsf{N}$}}
\UnaryInfC{$p\Vdash A$}
\DisplayProof\medskip
\,
\AxiomC{\vphantom{$p\vdash$}}
\LeftLabel{\scriptsize{$\mathrm{F}_\mathsf{U}$}}
\UnaryInfC{$p\Vdash \mathsf{U}$}
\DisplayProof


\begin{prooftree}
\alwaysNoLine
\AxiomC{$p \Vdash F$}
\AxiomC{$p\vdash A \red^\ast \Pi (x\!:\! F) G$}
\UnaryInfC{$\forall q \leqslant p (q\Vdash a\!:\! F\Rightarrow q\Vdash G[a])$}
\AxiomC{$\forall q \leqslant p (q\Vdash a=b\!:\! F\Rightarrow q\Vdash G[a]=G[b])$}
\alwaysSingleLine
\LeftLabel{\scriptsize{$\mathrm{F}_\Pi$}}
\TrinaryInfC{$p\Vdash A$}
\end{prooftree}

\begin{prooftree}
\alwaysNoLine
\AxiomC{$p \Vdash F$}
\AxiomC{$p\vdash A \red^\ast \Sigma (x\!:\! F) G$}
\UnaryInfC{$\forall q \leqslant p (q\Vdash a\!:\! F\Rightarrow q\Vdash G[a])$}
\AxiomC{$\forall q \leqslant p (q\Vdash a=b\!:\! F\Rightarrow q\Vdash G[a]=G[b])$}
\alwaysSingleLine
\LeftLabel{\scriptsize{$\mathrm{F}_\Sigma$}}
\TrinaryInfC{$p\Vdash A$}
\end{prooftree}

\AxiomC{$p\vdash A\red^\ast \mathbb{E}[\mathsf{f}\, \xoverline{k}]$}
\AxiomC{$k\notin \dom{p}$}
\AxiomC{$p(k\mapsto \mathsf{0})\Vdash A$} 
\AxiomC{$p(k\mapsto \mathsf{1})\Vdash A$}
\LeftLabel{\scriptsize{$\mathrm{F}_\mathrm{Loc}$}}
\QuaternaryInfC{$p\Vdash A$}
\DisplayProof
\end{center}\bigskip


\begin{enumerate}
	\item Assuming $p\Vdash A$ by $\mathrm{F}_{\mathsf{N}_0}$
	\begin{enumerate}
		\item Assuming $p\Vdash B$ then $p\Vdash A=B$ if
		\begin{enumerate}
			\item $p\vdash B\red^\ast {\mathsf{N}_0}$.
			\item $p\vdash B\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]$, $k\notin \dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash A=B$ and $p(k\mapsto \mathsf{1}) \Vdash A=B$.
		\end{enumerate}
		\item $p \nVdash t\!:\! A$ for all $t$.
		\item $p\nVdash t=u\!:\! A$ for all $t$ and $u$.
	\end{enumerate}


	\item Assuming $p\Vdash A$ by $\mathrm{F}_{\mathsf{N}_1}$ 
	\begin{enumerate}
		\item Assuming $p\Vdash B$ then $p\Vdash A=B$ if
		\begin{enumerate}
			\item $p\vdash B\red^\ast {\mathsf{N}_1}$.
			\item $p\vdash B\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]$, $k\notin \dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash A=B$ and $p(k\mapsto \mathsf{1}) \Vdash A=B$.
		\end{enumerate}
		\item $p \Vdash t\!:\! A$ if
		\begin{enumerate}
			\item $p\vdash t\red^\ast \mathsf{0} \!:\! A$
			\item $p\vdash t\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]\!:\! A$, $k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash t\!:\! A$ and $p(k\mapsto \mathsf{1}) \Vdash t\!:\! A$.
		\end{enumerate}
		\item Assuming $p\Vdash t\!:\! A$ and $p\Vdash u\!:\! A$ then $p\Vdash t=u \!:\! A$ if
		\begin{enumerate}
			\item $p\vdash t\red^\ast \mathsf{0} \!:\! A$ and $p\vdash u\red^\ast \mathsf{0} \!:\! A$.
			\item $p\vdash t\red^\ast \mathsf{0} \!:\! A$ and $p\vdash u\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}] \!:\! A, k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t= u\!:\! A$.
			\item $p\vdash t\red^\ast  \mathbb{E}[\mathsf{f}\,\xoverline{k}]\!:\! A, k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t= u\!:\! A$.
		\end{enumerate}
	\end{enumerate}


	\item Assuming $p\Vdash A$ by $\mathrm{F}_{\mathsf{N}_2}$ 
	\begin{enumerate}
		\item Assuming $p\Vdash B$ then $p\Vdash A=B$ if
		\begin{enumerate}
			\item $p\vdash B\red^\ast {\mathsf{N}_2}$.
			\item $p\vdash B\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]$, $k\notin \dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash A=B$ and $p(k\mapsto \mathsf{1}) \Vdash A=B$.
		\end{enumerate}
		\item $p \Vdash t\!:\! A$ if
		\begin{enumerate}
			\item $p\vdash t\red^\ast b \!:\! A$ for some $b\in \{\mathsf{0},\mathsf{1}\}$.
			\item $p\vdash t\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]$, $k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash t\!:\! A$ and $p(k\mapsto \mathsf{1}) \Vdash t\!:\! A$.
		\end{enumerate}
		\item Assuming $p\Vdash t\!:\! A$ and $p\Vdash u\!:\! A$ then $p\Vdash t=u \!:\! A$ if
		\begin{enumerate}
			\item $p\vdash t\red^\ast b \!:\! A$ and $p\vdash u\red^\ast b \!:\! A$ for some $b\in \{\mathsf{0},\mathsf{1}\}$.
			\item $p\vdash t\red^\ast b \!:\! A$, $b\in \{\mathsf{0},\mathsf{1}\}$ and $p\vdash u\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]\!:\! A, k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t= u\!:\! A$.
			\item $p\vdash t\red^\ast  \mathbb{E}[\mathsf{f}\,\xoverline{k}]\!:\! A, k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t= u\!:\! A$.
		\end{enumerate}
	\end{enumerate}
	
	\item Assuming $p\Vdash A$ by $\mathrm{F}_\mathsf{N}$ 
	\begin{enumerate}
		\item Assuming $p\Vdash B$ then $p\Vdash A=B$ if
		\begin{enumerate}
			\item $p\vdash B\red^\ast \mathsf{N}$.
			\item $p\vdash B\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]$, $k\notin \dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash A=B$ and $p(k\mapsto \mathsf{1}) \Vdash A=B$.
		\end{enumerate}
		\item $p \Vdash t\!:\! A$ if
		\begin{enumerate}
			\item $p\vdash t\red^\ast \xoverline{n} \!:\! A$.
			\item $p\vdash t\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]$, $k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash t\!:\! A$ and $p(k\mapsto \mathsf{1}) \Vdash t\!:\! A$.
		\end{enumerate}
		\item Assuming $p\Vdash t\!:\! A$ and $p\Vdash u\!:\! A$ then $p\Vdash t=u \!:\! A$ if
		\begin{enumerate}
			\item $p\vdash t\red^\ast \xoverline{n} \!:\! A$ and $p\vdash u\red^\ast \xoverline{n} \!:\! A$.
			\item $p\vdash t\red^\ast \xoverline{n} \!:\! A$ and $p\vdash u\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]\!:\! A, k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t= u\!:\! A$.
			\item $p\vdash t\red^\ast  \mathbb{E}[\mathsf{f}\,\xoverline{k}]\!:\! A, k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t= u\!:\! A$.
		\end{enumerate}
	\end{enumerate}

	\item Assuming $p\Vdash A$ by $\mathrm{F}_\Pi$ (Let $p\vdash A\red^\ast \Pi(x\!:\! F) G$). 
	\begin{enumerate}
		\item Assuming $p\Vdash B$ and $\vdash_p A=B$ then $p\Vdash A=B$ if
		\begin{enumerate}
			\item $p\vdash B\red^\ast \Pi(x\!:\! H) E$ and $p\Vdash F=H$ and $\forall q\leqslant p (q\Vdash a\!:\! F\Rightarrow q\Vdash G[a]=E[a])$.
			\item $p\vdash B\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]$, $k\notin \dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash A=B$ and $p(k\mapsto \mathsf{1}) \Vdash A=B$.
		\end{enumerate}
		\item Assuming $\vdash_p t\!:\! A$ then $p \Vdash t\!:\! A$ if
		\begin{enumerate}
			\item[] $\forall q\leqslant p(q\Vdash a\!:\! F \Rightarrow q\Vdash t\,a \!:\! G[a])$ and $\forall q\leqslant p (q\Vdash a=b\!:\! F\Rightarrow q\Vdash t\,a = t\,b \!:\! G[a])$. 
		\end{enumerate}
		\item Assuming $p\Vdash t\!:\! A$ and $p\Vdash u\!:\! A$ and $\vdash_p t=u\!:\! A$ then $p\Vdash t=u \!:\! A$ if
		\begin{enumerate}
			\item[] $\forall q \leqslant p (q\Vdash a\!:\! F \Rightarrow q\Vdash t\, a = u\, a \!:\! G[a])$
		\end{enumerate}
	\end{enumerate}

	\item Assuming $p\Vdash A$ by $\mathrm{F}_\Sigma$ (Let $p\vdash A\red^\ast \Sigma(x\!:\! F) G$). 
	\begin{enumerate}
		\item Assuming $p\Vdash B$ and $\vdash_p A=B$ then $p\Vdash A=B$ if
		\begin{enumerate}
			\item $p\vdash B\red^\ast \Sigma(x\!:\! H) E$ and $p\Vdash F=H$ and $\forall q\leqslant p (q\Vdash a\!:\! F\Rightarrow q\Vdash G[a]=E[a])$.
			\item $p\vdash B\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]$, $k\notin \dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash A=B$ and $p(k\mapsto \mathsf{1}) \Vdash A=B$.
		\end{enumerate}
		\item Assuming $\vdash_p t\!:\! A$ then $p \Vdash t\!:\! A$ if
		\begin{enumerate}
			\item[] $p\Vdash t.1 \!:\! F$ and $p\Vdash t.2 \!:\! G[t.1]$
		\end{enumerate}
		\item Assuming $p\Vdash t\!:\! A$ and $p\Vdash u\!:\! A$ and $\vdash_p t=u\!:\! A$ then $p\Vdash t=u \!:\! A$ if
		\begin{enumerate}
			\item[] $p\Vdash t.1 = u.1 \!:\! F$ and $p\Vdash t.2 = u.2 \!:\! G[t.1]$
		\end{enumerate}
	\end{enumerate}

	\item Assuming $p\Vdash A$ by $\mathrm{F}_\mathsf{U}$ (i.e.\ $A \coloneqq \mathsf{U}$).
	\begin{enumerate}
		\item Assuming $p\Vdash B$ then $p\Vdash A=B$ if $B\coloneqq \mathsf{U}$
		\item Assuming $\vdash_p L\!:\! A$ then $p \Vdash L\!:\! A$ if
		\begin{enumerate}
			\item $p\vdash L\red^\ast M$ with $M\in \{{\mathsf{N}_0}, {\mathsf{N}_1}, {\mathsf{N}_2}, \mathsf{N}\}$
			\item $p\vdash L\red^\ast \Pi(x\!:\! F) G$ and $p\Vdash F\!:\! A$ and\\ $\forall q\leqslant p (q\Vdash a\!:\! F \Rightarrow q\Vdash G[a] \!:\! A)$ and $\forall q\leqslant p (q\Vdash a=b\!:\! F \Rightarrow q\Vdash G[a]=G[b] \!:\! A)$.
			\item $p\vdash L\red^\ast \Sigma(x\!:\! F) G$ and $p\Vdash F\!:\! A$ and\\ $\forall q\leqslant p (q\Vdash a\!:\! F \Rightarrow q\Vdash G[a] \!:\! A)$ and $\forall q\leqslant p (q\Vdash a=b\!:\! F \Rightarrow q\Vdash G[a]=G[b] \!:\! A)$
			\item $p\vdash L \red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]$, $k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash L\!:\! A$ and $p(k\mapsto \mathsf{1}) \Vdash L\!:\! A$.
		\end{enumerate}
		\item Assuming $p\Vdash L\!:\! A$ and $p\Vdash P\!:\! A$ and $\vdash_p L=P\!:\! A$ then $p\Vdash L=P \!:\! A$ if
		\begin{enumerate}
			\item $p\vdash L\red^\ast M$ and $p\vdash P\red^\ast M$ for $M\in \{{\mathsf{N}_0}, {\mathsf{N}_1}, {\mathsf{N}_2},\mathsf{N}\}$.
			\item $p\vdash L\red^\ast \Pi(x\!:\! F) G$ and $p\vdash P\red^\ast \Pi(x\!:\! H) E$ and\\ $p\Vdash F=H\!:\! A$ and $\forall q\leqslant p (q\Vdash a\!:\! F \Rightarrow q\Vdash G[a] = E[a] \!:\! A)$
			\item $p\vdash L\red^\ast \Sigma(x\!:\! F) G$ and $p\vdash P\red^\ast \Sigma(x\!:\! H) E$ and\\ $p\Vdash F=H\!:\! A$ and $\forall q\leqslant p (q\Vdash a\!:\! F \Rightarrow q\Vdash G[a] = E[a] \!:\! A)$
			\item $p\vdash L\red^\ast M$ with $M$ in canonical $p$-whnf
			and $p\vdash P\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}], k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash L=P\!:\! A$ and $(k\mapsto \mathsf{1}) \Vdash L=P\!:\! A$.
			\item $p\vdash L\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}], k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash L=P\!:\! A$ and $(k\mapsto \mathsf{1}) \Vdash L=P\!:\! A$.
		\end{enumerate}
	\end{enumerate}

	\item Assuming $p\Vdash A$ by $\mathrm{F}_\mathrm{Loc}$ (i.e.\ $p\vdash A\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}], k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash A$ and $p(k\mapsto \mathsf{1})\Vdash A$).
	\begin{enumerate}
		\item Assuming $p\Vdash B$ and $\vdash_p A= B$ then $p\Vdash A=B$ if $p(k\mapsto \mathsf{0})\Vdash A=B$ and $p(k\mapsto \mathsf{1}) \Vdash A=B$.
		\item Assuming $\vdash_p t\!:\! A$ then $p \Vdash t\!:\! A$ if $p(k\mapsto \mathsf{0})\Vdash t\!:\! A$ and $p(k\mapsto \mathsf{1}) \Vdash t\!:\! A$.
		\item Assuming $p\Vdash t\!:\! A$ and $p\Vdash u\!:\! A$ and $\vdash_p t=u\!:\! A$ then $p\Vdash t=u \!:\! A$ if $p(k\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $p(k\mapsto \mathsf{1}) \Vdash t=u\!:\! A$.
	\end{enumerate}

\end{enumerate}

Note from the definition that when $p\Vdash A=B$ then $p\Vdash A$ and $p\Vdash B$, when $p\Vdash a\!:\! A$ then $p\Vdash A$ and when $p\Vdash a=b \!:\! A$ then $p\Vdash a\!:\! A$ and $p\Vdash b\!:\! A$. It follows also from the definition that $\vdash_p J$ whenever $p\Vdash J$. 

The clause ($\mathrm{F_{Loc}}$) gives semantics to \emph{variable types}. For example,  if $p\coloneqq\{(0,\mathsf{0})\}$ and $q\coloneqq\{(0,\mathsf{1})\}$ the type $R\coloneqq {\mathsf{rec}_{\mathsf{N}_2}} (\lambda x. \mathsf{U})\,{\mathsf{N}_1}\,\mathsf{N}\,(\mathsf{f}\,\mathsf{0})$ has reductions $p\vdash R \red^\ast {\mathsf{N}_1}$ and $q\vdash R\red^\ast \mathsf{N}$. Thus $p\Vdash R$ and $q\Vdash R$ and since $\emptyset \vartriangleleft \{p,q\}$ we have $\emptyset\Vdash R$.

\begin{lem}
\label{forcedtypeslocallyreducetocanonical}
If $p\Vdash A$ then there is a partition $p\vartriangleleft S$ where $A$ has a canonical $q$-whnf for all $q\in S$. If $p\Vdash A=B$ then there is a partition $p\vartriangleleft S$ where $A$ and $B$ have similar canonical $q$-whnf for all $q\in S$, i.e.\ $q\vdash A\red^\ast A'$ and $q\vdash B\red^\ast B'$ where $(A',B')$ is of the form $({\mathsf{N}_0},{\mathsf{N}_0})$, $({\mathsf{N}_1}, {\mathsf{N}_1})$, $({\mathsf{N}_2}, {\mathsf{N}_2})$, $(\mathsf{N}, \mathsf{N})$, $(\mathsf{U}, \mathsf{U})$, $(\Pi(x\!:\! F) G, \Pi(x\!:\! H) E)$, or $(\Sigma(x\!:\! F) G, \Sigma(x\!:\! H) E)$.
\end{lem}
\begin{proof}
The statement follows from the definition by induction on the derivation of $p\Vdash A$
\end{proof}

\begin{cor}
\label{existenceofpwhnfislocal}
Let $p\vartriangleleft S$. If $q\Vdash A$ for all $q\in S$ then $A$ has a proper $p$-whnf. 
\end{cor}
\begin{proof}
Follows from Lemma~\ref{forcedtypeslocallyreducetocanonical} and Corollary~\ref{properwhnflocal} by induction.
\end{proof}


\begin{lem
	\label{LEM:BaseTypeCanonicity}
	Let $p\vdash A\red^\ast M$ with $M \in \{{\mathsf{N}_1},{\mathsf{N}_2},\mathsf{N}\}$. If $p\Vdash t\!:\! A$ then there is a partition $p\vartriangleleft S$ where $t$ has a canonical $q$-whnf for all $q\in S$. If $p\Vdash t=u\!:\! A$ then there is a partition $p\vartriangleleft S$ where $t$ and $u$ have the same canonical $q$-whnf for each $q\in S$.
\end{lem}
\begin{proof}
Follows from the definition.
\end{proof}

The rest of this section is dedicated to proving the following theorem:
\begin{thm}
\label{properties}
The following hold for the forcing relation
\begin{enumerate}
\item Monotonicity: If $q \leqslant p$ and $p\Vdash J$ then $q\Vdash J$.
\item Locality: If $p\vartriangleleft S$ and $q\Vdash J$ for all $q\in S$ then $p\Vdash J$.
\item Reflexivity: If $p\Vdash A$ then $p\Vdash A=A$ and if $p\Vdash a\!:\! A$ then $p\Vdash a=a\!:\! A$.
\item Symmetry: If $p\Vdash A=B$ then $p\Vdash B=A$ and if $p\Vdash a=b\!:\! A$ then $p\Vdash b=a\!:\! A$.
\item Transitivity: If $p\Vdash A=B$ and $p\Vdash B=C$ then $p\Vdash A=C$ and if $p\Vdash a=b \!:\! A$ and $p\Vdash b=c \!:\! A$ then $p\Vdash a=c\!:\! A$.
\item Extensionality: If $p\Vdash A=B$ then if $p\Vdash a\!:\! A$ then $p\Vdash a\!:\! B$ and if $p\Vdash a=b\!:\! A$ then $p\Vdash a=b \!:\! B$.
\end{enumerate}
\end{thm}

In the premise of any forcing $p\Vdash J$ there are a number of typing judgments. Since the type system satisfy the properties listed in Theorem~\ref{properties} we will largely ignore these typing judgments in the proofs.

\begin{lem}\label{LEM:typeIntroMonotone}
If $p\Vdash A$ and $q\leqslant p$ then $q\Vdash A$.
\end{lem}
\begin{proof}
Let $p\Vdash A$ and $q\leqslant p$. By induction on the derivation of $p\Vdash A$ 
	\begin{enumerate}
		\item (Derivation by $\for_\mathsf{N}$)
		 Let $p\vdash A\red^\ast \mathsf{N}$. Since the reduction is monotone $q\vdash A\red^\ast \mathsf{N}$, thus $q\Vdash A$. \\
		 The statement follows similarly when $p\Vdash A$ holds by $\mathrm{F}_{\mathsf{N}_0}$, $\mathrm{F}_{\mathsf{N}_1}$, $\mathrm{F}_{\mathsf{N}_2}$, $\mathrm{F}_\mathsf{N}$ or $\mathrm{F}_\mathsf{U}$.
		\item\label{typeIntroMonotonePi} (Derivation by $\mathrm{F}_\Pi$.)
		 Let $p\vdash A\red^\ast\Pi(x\!:\! F) G$. From the premise $p\Vdash F$, by IH, it follows that $q\Vdash F$. From $\forall r\leqslant p (r\Vdash a\!:\! F\Rightarrow r\Vdash G[a])$ and $\forall r\leqslant p (r\Vdash a=b\!:\! F\Rightarrow r\Vdash G[a]=G[b])$ it follows directly that $\forall s\leqslant q (s\Vdash a\!:\! F\Rightarrow s\Vdash G[a])$ and $\forall s\leqslant q (s\Vdash a=b\!:\! F\Rightarrow s\Vdash G[a]=G[b])$. Hence $q\Vdash A$.\\
		 The statement follows similarly when $p\Vdash A$ holds by $\mathrm{F}_\Sigma$
		\item (Derivation by $\mathrm{F}_\mathrm{Loc}$.) 
		 Let $p\vdash A\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{m}], m\notin \dom{p}$. If $m\in \dom{q}$ then $q\leqslant p(m\mapsto b)$ for some $b\in \{\mathsf{0},\mathsf{1}\}$. Since $p(m\mapsto b)\Vdash A$ with a derivation strictly smaller than the derivation of $p\Vdash A$ then by IH $q\Vdash A$. Alternatively, $q\vdash A\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{m}]$ but then $q(m\mapsto b)\leqslant p(m\mapsto b)$. By IH we have $q(m\mapsto \mathsf{0})\Vdash A$ and  $q(m\mapsto \mathsf{1})\Vdash A$ and thus $q\Vdash A$.\qedhere
	\end{enumerate}
\end{proof}



\begin{lem}\label{LEM:typeEqMonotone}
If $p\Vdash A=B$ and $q\leqslant p$ then $q\Vdash A=B$.
\end{lem}
\begin{proof}
Let $p\Vdash A=B$ and $q\leqslant p$. We have then that $p\Vdash A$ and $p\Vdash B$. By Lemma~\ref{LEM:typeIntroMonotone} we have that $q\Vdash A$ and $q\Vdash B$. By induction on the derivation of $p\Vdash A$
\begin{enumerate}
	 \item\label{floctypeq} Let $p\Vdash A$ by $\mathrm{F}_\mathrm{Loc}$, i.e.\ $p\vdash A\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}], k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash A=B$ and $p(k\mapsto \mathsf{1})\Vdash A=B$.  By induction on the derivation of $p\Vdash A=B$. If $k\in\dom{q}$ then $q\leqslant p(k\mapsto b)$ for some $b\in \{\mathsf{0},\mathsf{1}\}$. Since the derivation of $p(k\mapsto b)\Vdash A=B$ is strictly smaller than that of $p \Vdash A=B$,  by IH $q\Vdash A=B$. Otherwise, $k\notin \dom{q}$ and $q\vdash A\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]$ and since $q(k\mapsto b)\leqslant p(k\mapsto b)$, by IH, $q(k\mapsto \mathsf{0})\Vdash A=B$ and $q(k\mapsto \mathsf{1})\Vdash A=B$. By the definition $q\Vdash A=B$.  
	\item Let $p\Vdash A$ by $\mathrm{F}_\mathsf{N}$ (i.e.\ $p\vdash A\red^\ast \mathsf{N}$). By induction on the derivation of $p\Vdash A=B$ 
	\begin{enumerate}
		\item Let $p\vdash B\red^\ast \mathsf{N}$. We have directly that $q\Vdash A=B$ by monotonicity of the reduction.
		\item Let $p\vdash B\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}], k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash A=B$ and $p(k\mapsto \mathsf{1})\Vdash A=B$. The statement then follows similarly to (\ref{floctypeq}). 
	\end{enumerate}
	The statement follows similarly when $p\Vdash A$ holds by $\mathrm{F}_{\mathsf{N}_0}, \mathrm{F}_{\mathsf{N}_1}, \mathrm{F}_{\mathsf{N}_2}$.
	\item Let $p\vdash A\red^\ast \Pi(x\!:\! F) G$. By induction on the derivation of $p\Vdash A=B$ 
	\begin{enumerate}
		\item Let $p\vdash B\red^\ast \Pi(x\!:\! H E)$ and $p\Vdash F=H$ and $\forall r\leqslant p(r\Vdash a\!:\! F\Rightarrow r\Vdash G[a]=E[a])$. By IH $q\Vdash F=H$. Directly we have $\forall s\leqslant q(s\Vdash a\!:\! F\Rightarrow s\Vdash G[a]=E[a])$. Thus $q\Vdash A=B$.
		\item Let $p\vdash B\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}], k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash A=B$ and $p(k\mapsto \mathsf{1})\Vdash A=B$. The statement then follows similarly to (\ref{floctypeq}). 
	\end{enumerate}
	The statement follows similarly when $p\Vdash A$ holds by $\mathrm{F}_\Sigma$.
\item (Derivation by $\mathrm{F}_\mathsf{U}$) We have then that $B\coloneqq \mathsf{U}$ and thus $q\Vdash A=B$.\qedhere
\end{enumerate}
\end{proof}


\begin{lem}\label{LEM:termIntroMonotone}
If $p\Vdash t\!:\! A$ and $q\leqslant p$ then $q\Vdash t\!:\! A$.
\end{lem}
\begin{proof}
Let $p\Vdash t\!:\! A$ and $q\leqslant p$. From the definition we have that $p\Vdash A$. From Lemma \ref{LEM:typeIntroMonotone} we have that $q\Vdash A$. By induction on the derivation of $p\Vdash A$.
		\begin{enumerate}
			\item Let $p\Vdash A$ by $\mathrm{F}_\mathsf{N}$.  By induction on the derivation of $p\Vdash t\!:\! A$. 
			\begin{enumerate}
				\item Let $p\vdash t\red^\ast \xoverline{n}\!:\! A$. Then $q\vdash t\red^\ast \xoverline{n}\!:\! A$ and $q\Vdash t\!:\! A$.
				\item Let $p\vdash t\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]\!:\! A, k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash t\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t\!:\! A$. If $k\in \dom{q}$ then $q\leqslant p(k\mapsto b)$ for some $b\in \{\mathsf{0},\mathsf{1}\}$, since the derivation of $p(k\mapsto b) \Vdash t\!:\! A$ is strictly smaller than the derivation $p\Vdash t\!:\! A$, by IH,  $q\Vdash t\!:\! A$. Otherwise, $k\notin\dom{q}$ and $q\vdash t\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}] \!:\! A$. But $q(k\mapsto b) \leqslant p(k\mapsto b)$ and by IH $q(k\mapsto \mathsf{0})\Vdash t\!:\! A$ and $q(k\mapsto \mathsf{1})\Vdash t\!:\! A$. By the definition $q\Vdash t\!:\! A$. 
			\end{enumerate}
			The statement follows similarly when $p\Vdash A$ is derived by $\mathrm{F}_{\mathsf{N}_1}$ or $\mathrm{F}_{\mathsf{N}_2}$.
			
			\item Let $p\Vdash A$ by $\mathrm{F}_\mathsf{U}$. The statement follows similarly to Lemma~\ref{LEM:typeIntroMonotone}.
			\item Let $p\Vdash A$ by $\mathrm{F}_\Pi$ and let $p\vdash A\red^\ast \Pi(x\!:\! F) G$. From $\forall r\leqslant p (r\Vdash a\!:\! F \Rightarrow r\Vdash t\,a \!:\! G[a])$ and $\forall r\leqslant p (r\Vdash a=b\!:\! F\Rightarrow r\Vdash t\,a=t\,b\!:\! G[a])$ we have directly that $\forall s\leqslant q (s\Vdash a\!:\! F \Rightarrow s\Vdash t\,a \!:\! G[a])$ and $\forall s\leqslant q (s\Vdash a=b\!:\! F\Rightarrow s\Vdash t\,a=t\,b\!:\! G[a])$. Thus $q\Vdash t\!:\! A$. 
			\item Let $p\Vdash A$ by $\mathrm{F}_\Sigma$ and let $p\vdash A\red^\ast \Sigma(x\!:\! F) G$. By induction on the derivation of $p\Vdash t\!:\! A$. From $p\Vdash t.1 \!:\! F$ and $p\Vdash t.2 \!:\! G[t.1]$, by IH, $q\Vdash t.1 \!:\! F$ and $q\Vdash t.2 \!:\! G[t.1]$, thus $q\Vdash t\!:\! A$.
			\item Let $p\Vdash A$ by $\mathrm{F}_\mathrm{Loc}$ and let $p\vdash A\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}], k\notin \dom {p}$ and $p(k\mapsto \mathsf{0})\Vdash A$ and $p(k\mapsto \mathsf{1})\Vdash A$. By induction on the derivation of $p\Vdash t\!:\! A$. If $k\in\dom{q}$ then $q\leqslant p(k\mapsto b)$ for some $b\in \{\mathsf{0},\mathsf{1}\}$ from the premise $p(k\mapsto \mathsf{0})\Vdash t\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t\!:\! A$, by IH, $q\Vdash t\!:\! A$. Otherwise, $k\notin\dom{q}$ and $q\vdash A\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]$ (i.e.\ $q\Vdash A$ by $\mathrm{F}_\mathrm{Loc}$). Since $q(k\mapsto b)\leqslant p(k\mapsto b)$, by the IH, $q(k\mapsto \mathsf{0})\Vdash t\!:\! A$ and $q(k\mapsto \mathsf{1})\Vdash t\!:\! A$. By the definition $q\Vdash t\!:\! A$. \qedhere
		\end{enumerate}
\end{proof}

\begin{lem}\label{LEM:termEqMonotone}
 If $p\Vdash t=u\!:\! A$ and $q\leqslant p$ then $q\Vdash t=u\!:\! A$.
\end{lem}
\begin{proof}
Let $p\Vdash t=u \!:\! A$ and $q\leqslant p$. We have then that $p\Vdash A$, $p\Vdash t\!:\! A$, and $p\Vdash u\!:\! A$. By Lemma~\ref{LEM:typeIntroMonotone} $q\Vdash A$. By Lemma~\ref{LEM:termIntroMonotone} $q\Vdash t \!:\! A$ and $q\Vdash u \!:\! A$. By induction on the derivation $p\Vdash A$.

\begin{enumerate}
			\item Let $p\Vdash A$ by $\mathrm{F}_\mathsf{N}$.  By induction on the derivation of $p\Vdash t=u\!:\! A$.  
			\begin{enumerate}
				\item Let $p\vdash t\red^\ast \xoverline{n}\!:\! A$ and $p\vdash u\red^\ast \xoverline{n}\!:\! A$. By monotonicity of reduction $q\Vdash t=u\!:\! A$.
			\item \label{localtermeqforcingismonotone} Let $p\vdash t\red^\ast \xoverline{n}\!:\! A$ and $p\vdash t\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]\!:\! A, k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t=u\!:\! A$. If $k\in \dom{q}$ then $q\leqslant p(k\mapsto b)$ for some $b\in \{\mathsf{0},\mathsf{1}\}$, by IH,  $q\Vdash t=u\!:\! A$. Otherwise,  $q\vdash t\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]\!:\! A$. But $q(k\mapsto b) \leqslant p(k\mapsto b)$ and by IH $q(k\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $q(k\mapsto \mathsf{1}) \Vdash t=u\!:\! A$. By the definition $q\Vdash t=u\!:\! A$. 
			\item Let $p\vdash t\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]\!:\! A, k\notin\dom{p}$. The statement follows similarly to (\ref{localtermeqforcingismonotone}).
			\end{enumerate}
			The statement follows similarly for when $p\Vdash A$ holds by $\mathrm{F}_{\mathsf{N}_1}$ or $\mathrm{F}_{\mathsf{N}_2}$.
			\item Let $p\Vdash A$ by $\mathrm{F}_\mathsf{U}$. The statement follows by a proof similar to that of Lemma~\ref{LEM:typeEqMonotone}.
			\item Let $p\Vdash A$ by $\mathrm{F}_\Pi$ and let $p\vdash A\red^\ast \Pi(x\!:\! F) G$. From $\forall r\leqslant q(r\Vdash a\!:\! F\Rightarrow r\Vdash t\, a=u\, a\!:\! G[a])$ we have directly that $\forall s\leqslant q(s\Vdash a\!:\! F\Rightarrow s\Vdash t\, a=u\, a\!:\! G[a])$. Hence $q\Vdash t=u\!:\! A$.
			\item Let $p\Vdash A$ by $\mathrm{F}_\Sigma$ and let $p\vdash A\red^\ast \Sigma(x\!:\! F) G$. By induction on the derivation of $p\Vdash t=u\!:\! A$. From $p\Vdash t.1 =u.1\!:\! F$ and $p\Vdash t.2 =u.2\!:\! G[t.1]$, by IH we have $q\Vdash t.1 =u.1\!:\! F$ and $q\Vdash t.2 =u.2\!:\! G[t.1]$, thus $q\Vdash t=u\!:\! A$.
			\item Let $p\Vdash A$ by $\mathrm{F}_\mathrm{Loc}$ and let $p\vdash A\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}], k \notin\dom{p}$. By induction on the derivation of $p\Vdash t=u \!:\! A$. If $k\in \dom{q}$ then the statement follows by IH. If $k\notin\dom{q}$ then $q\vdash A\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]$ (i.e.\ $q\Vdash A$ by $\mathrm{F}_\mathrm{Loc}$) and since $q(k\mapsto b)\leqslant p(k \mapsto b)$, by IH, $q(k\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $q(k\mapsto \mathsf{1})\Vdash t=u\!:\! A$. Hence $q\Vdash t=u\!:\! A$. \qedhere
\end{enumerate}
\end{proof}


We collect the results of Lemmas~\ref{LEM:typeIntroMonotone}, \ref{LEM:termIntroMonotone}, \ref{LEM:termEqMonotone}, and \ref{LEM:typeEqMonotone} in the following corollary.
\begin{cor}[Monotonicity]
\label{COR:monotonicity}
If $p\Vdash J$ and $q\leqslant p$ then $q\Vdash J$.
\end{cor}

We write $\Vdash J$ when $\emptyset \Vdash J$. By monotonicity $\Vdash J$ iff $p\Vdash J$ for all $p$. 

\begin{lem}
\label{LEM:localitysublemma1}
Let $p\Vdash A$ and $p\Vdash B$. If $p(m\mapsto \mathsf{0})\Vdash A=B$ and $p(m\mapsto \mathsf{1})\Vdash A=B$ then $p\Vdash A=B$.
\end{lem}
\begin{proof}
By induction on the derivation of $p\Vdash A$.
\begin{enumerate}
	\item Let $p\Vdash A$ by $\mathrm{F}_\mathsf{N}$. By induction on the derivation of $p\Vdash B$
	\begin{enumerate}
		\item If $p\Vdash B$ by $\mathrm{F}_\mathsf{N}$ then $p\Vdash A=B$ immediately.
		\item \label{typeqrightloc} If $p\Vdash B$ by $\mathrm{F}_\mathrm{Loc}$.
		The statement follows similarly to~(\ref{loctypeqloc}) below.
	\end{enumerate}
	The statement follows similarly when $p\Vdash A$ is derived by $\mathrm{F}_{\mathsf{N}_0}, \mathrm{F}_{\mathsf{N}_1}$ and $\mathrm{F}_{\mathsf{N}_2}$.
	\item Let $p\Vdash A$ by $\mathrm{F}_\Pi$ and let $p\vdash A\red^\ast \Pi(x\!:\! F) G$. By induction on the derivation of $p\Vdash B$
	\begin{enumerate}
		\item Let $p\Vdash B$ by $\mathrm{F}_\Pi$ and let $p\vdash B\red^\ast \Pi(x\!:\! H) E$. Since $p\Vdash A$ and $p\Vdash B$ we have $p\Vdash F$ and $p\Vdash H$. From the premise $p(m\mapsto \mathsf{0})\Vdash F=H$ and $p(m\mapsto \mathsf{1})\Vdash F=H$ and by IH $p\Vdash F=H$.
		
		Let $q\leqslant p$ and $q\Vdash a\!:\! F$. If $q\leqslant p(m\mapsto b)$ for some $b\in \{\mathsf{0},\mathsf{1}\}$ then $q\Vdash G[a]=E[a]$. Otherwise, since $q(m\mapsto b)\leqslant p(m\mapsto b)$, by monotonicity $q(m\mapsto \mathsf{0}) \Vdash G[a]=E[a]$ and $q(m\mapsto \mathsf{1})\Vdash G[a]=E[a]$. From $p\Vdash A$ we have that $q\Vdash G[a]$ and from $p\Vdash B$ we have that $q\Vdash E[a]$. By IH $q\Vdash G[a] = E[a]$. We thus have $p\Vdash A=B$.
		\item Let $p\Vdash B$ by $\mathrm{F}_\mathrm{Loc}$. The statement then follows similarly to (\ref{loctypeqloc}) below.
	\end{enumerate}
	The statement follows similarly when $p\Vdash A$ is derived by $\mathrm{F}_\Sigma$.
	\item If $p\Vdash A$ by $\mathrm{F}_\mathsf{U}$ then $A\coloneqq B\coloneqq \mathsf{U}$ and $p\Vdash A=B$.
	\item \label{loctypeqloc} If $p\Vdash A$ by $\mathrm{F}_\mathrm{Loc}$. Let $p\vdash A\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}], k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash A$ and $p(k\mapsto \mathsf{1})\Vdash A$. 
	\begin{enumerate}
		\item If $k=m$ then we have $p\Vdash A=B$ by the definition.
		\item If $k\neq m$. By monotonicity $p(k\mapsto b)\Vdash A$ and $p(k\mapsto b)\Vdash B$ and $p(k \mapsto b) (m\mapsto \mathsf{0}) \Vdash A=B$ and $p(k\mapsto b) (m\mapsto \mathsf{1}) \Vdash A=B$ for all $b\in \{\mathsf{0},\mathsf{1}\}$. The derivation of $p(k\mapsto b)\Vdash A$ is strictly smaller than the derivation of $p\Vdash A$. By IH we have $p(k\mapsto \mathsf{0}) \Vdash A=B$ and $p(k\mapsto \mathsf{1})\Vdash A=B$. By the definition $p\Vdash A=B$.\qedhere
	\end{enumerate}
\end{enumerate}
\end{proof}

\begin{lem}\leavevmode
\label{LEM:typeIntroLocal}
If $p(m\mapsto \mathsf{0})\Vdash A$ and $p(m\mapsto \mathsf{1})\Vdash A$ for some $m\notin \dom{p}$ then $p\Vdash A$.
\end{lem}
\begin{proof}
The proof is by by induction on the derivations $p(m\mapsto \mathsf{0})\Vdash A$. Note that from $p(m\mapsto \mathsf{0})\Vdash A$ and $p(m\mapsto \mathsf{1})\Vdash A$ we have that $A$ has proper $p(m\mapsto \mathsf{0})$-whnf and $p(m\mapsto \mathsf{1})$-whnf and by Corollary~\ref{existenceofpwhnfislocal} $A$ has a proper $p$-whnf.

\begin{enumerate}
	\item Let $p(m\mapsto \mathsf{0})\Vdash A$ by $\mathrm{F}_\mathsf{N}$
	\begin{enumerate}
			\item If $A$ has a canonical $p$-whnf then $p\vdash A\red^\ast \mathsf{N}$ and $p\Vdash A$.
			\item Otherwise, $p\vdash A\red^\ast \mathbb{E}[\xoverline{k}], k\notin\dom{p}$. Since $A$ has a canonical $p(m\mapsto \mathsf{0})$-whnf we have that $k=m$ and by the definition we have $p\Vdash A$ by $\mathrm{F}_\mathrm{Loc}$
	\end{enumerate}
	The statement follows similarly when $p(m\mapsto \mathsf{0}) \Vdash A$ holds by $\mathrm{F}_{\mathsf{N}_0}$, $\mathrm{F}_{\mathsf{N}_1}$ or $\mathrm{F}_{\mathsf{N}_2}$.
	\item Let $p(m\mapsto \mathsf{0})\Vdash A$ by $\mathrm{F}_\Pi$
	\begin{enumerate}
		\item If $A$ has a canonical $p$-whnf then $p\vdash A\red^\ast \Pi(x\!:\! F) G$. From $p(m\mapsto 0)\Vdash A$ and $p(m\mapsto 1)\Vdash A$ we have $p(m\mapsto \mathsf{0})\Vdash F$ and $p(m\mapsto \mathsf{1})\Vdash F$. By IH $p\Vdash F$. Let $q\leqslant p$
		\begin{enumerate}
			\item If $m\in \dom{q}$ then $q\leqslant p(m\mapsto b)$ for some $b\in \{\mathsf{0},\mathsf{1}\}$, then $(q\Vdash a\!:\! F \Rightarrow q\Vdash G[a])$ and $(q\Vdash a=b\!:\! F\Rightarrow q\Vdash G[a]=G[b])$.
			\item If $m\notin \dom{q}$ then $q\vartriangleleft \{q(m\mapsto \mathsf{0}), q(m\mapsto \mathsf{1})\}$. Let $q\Vdash a\!:\! F$, by monotonicity $q(m\mapsto \mathsf{0}) \Vdash a\!:\! F$ and $q(m\mapsto \mathsf{1})\Vdash a\!:\! F$. Since $q(m\mapsto b)\leqslant p(m\mapsto b)$, by the definition $q(m\mapsto \mathsf{0}) \Vdash G[a]$ and $q(m\mapsto \mathsf{1})\Vdash G[a]$ and by IH $q\Vdash G[a]$. 
			
			Let $q\Vdash a=b\!:\! F$, by monotonicity $q(m\mapsto \mathsf{0})\Vdash a=b\!:\! F$ and $q(m\mapsto \mathsf{1})\Vdash a=b\!:\! F$. But then $q(m\mapsto \mathsf{0})\Vdash G[a]$ and $q(m\mapsto \mathsf{1})\Vdash G[a]$ and $q(m\mapsto \mathsf{0})\Vdash G[b]$ and $q(m\mapsto \mathsf{1})\Vdash G[b]$ and $q(m\mapsto \mathsf{0})\Vdash G[a]=G[b]$ and $q(m\mapsto \mathsf{1})\Vdash G[a]=G[b]$. By Lemma~\ref{LEM:localitysublemma1} we have $q\Vdash G[a]=G[b]$.
				\end{enumerate}
		\end{enumerate}
		The statement follows similarly when $p(m\mapsto \mathsf{0}) \Vdash A$ holds by $\mathrm{F}_\Sigma$.
	\item Let $p(m\mapsto \mathsf{0})\Vdash A$ by $\mathrm{F}_\mathsf{U}$ then $A\coloneqq \mathsf{U}$ and $p\Vdash A$.
	\item Let $p(m\mapsto \mathsf{0})\Vdash A$ by $\mathrm{F}_\mathrm{Loc}$. Since $A$ doesn't have a canonical $p(m\mapsto \mathsf{0})$-whnf $A$ doesn't have a canonical $p$-whnf. Since $A$ has a proper $p$-whnf we have $p\vdash A\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}], k\notin\dom{p}$. 	
	\begin{enumerate}
	\item If $k=m$ then by the definition we have $p\Vdash A$ by $\mathrm{F}_\mathrm{Loc}$
	\item If $k\neq m$ then $p(m\mapsto b)\vdash A\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]$. Hence $p(m\mapsto \mathsf{1})\Vdash A$ by $\mathrm{F}_\mathrm{Loc}$. We have then $p(m\mapsto \mathsf{0})(k\mapsto \mathsf{0})\Vdash A$ and $p(m\mapsto \mathsf{0})(k\mapsto \mathsf{1})\Vdash A$ and $p(m\mapsto \mathsf{1})(k\mapsto \mathsf{0})\Vdash A$ and $p(m\mapsto \mathsf{1})(k\mapsto \mathsf{1})\Vdash A$. By IH $p(k\mapsto \mathsf{0}) \Vdash A$ and $p(k\mapsto \mathsf{1})\Vdash A$. By the definition $p\Vdash A$.\qedhere
	\end{enumerate}
	\end{enumerate}
\end{proof}

\begin{lem}
\label{LEM:typeEqLocal}
If $p(m\mapsto \mathsf{0})\Vdash A=B$ and $p(m\mapsto \mathsf{1})\Vdash A=B$ for $m\notin\dom{p}$ then $p\Vdash A=B$.
\end{lem}
\begin{proof}
By the definition $p(m\mapsto \mathsf{0})\Vdash A$ and $p(m\mapsto \mathsf{1})\Vdash A$ and $p(m\mapsto \mathsf{0})\Vdash B$ and $p(m\mapsto \mathsf{1})\Vdash B$. By Lemma~\ref{LEM:typeIntroLocal} $p\Vdash A$ and $p\Vdash B$. By Lemma~\ref{LEM:localitysublemma1} $p\Vdash A=B$.
\end{proof}

\begin{lem}\leavevmode
\label{LEM:termIntroEqLocal}
\begin{enumerate}
\item If $p(m\mapsto \mathsf{0}) \Vdash t\!:\! A$ and $p(m\mapsto \mathsf{1}) \Vdash t\!:\! A$ for some $m\notin \dom{p}$ then $p\Vdash t\!:\! A$.
\item If $p(m\mapsto \mathsf{0}) \Vdash t=u\!:\! A$ and $p(m\mapsto \mathsf{1}) \Vdash t=u\!:\! A$ for some $m\notin \dom{p}$ then $p\Vdash t=u\!:\! A$.
\end{enumerate}
\end{lem}
\begin{proof}
We prove the two statements mutually by induction.
\begin{enumerate}
 \item \label{termintromontone} From $p(m\mapsto \mathsf{0})\Vdash t\!:\! A$ and $p(m\mapsto \mathsf{1})\Vdash t\!:\! A$ we have $p(m\mapsto \mathsf{0})\Vdash A$ and $p(m\mapsto \mathsf{1})\Vdash A$ and by Lemma~\ref{LEM:typeIntroLocal} $p\Vdash A$. By induction on the derivation of $p\Vdash A$.
\begin{enumerate}
	\item \label{natlocaltermforced} Let $p\Vdash A$ by $\mathrm{F}_\mathsf{N}$. Since $t$ has proper $p(m\mapsto \mathsf{0})$-whnf and $p(m\mapsto \mathsf{1})$-whnf. By Lemma~\ref{properwhnflocal} $t$ has a proper $p$-whnf. By induction on the derivation of $p(m\mapsto \mathsf{0})\Vdash t\!:\! A$.
	\begin{enumerate}	
		\item Let $p(m\mapsto \mathsf{0})\vdash t\red^\ast \xoverline{n}\!:\! A$
		\begin{enumerate}
			\item If $t$ has a canonical $p$-whnf then $p\vdash t\red^\ast \xoverline{n}\!:\! A$ and $p\Vdash t\!:\! A$ directly.
			\item Otherwise, $p\vdash t\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]\!:\! A,k\notin\dom{p}$. But then we have that $k=m$ and by the definition $p\Vdash t\!:\! A$. 
		\end{enumerate}
		\item Let $p(m\mapsto \mathsf{0})\vdash t\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}],k\notin\dom{p(m\mapsto \mathsf{0})}$ and $p(m\mapsto \mathsf{0})(k\mapsto \mathsf{0})\Vdash t\!:\! A$ and $p(m\mapsto \mathsf{0})(k\mapsto \mathsf{1})\Vdash t\!:\! A$. By monotonicity $p(m\mapsto \mathsf{1})(k\mapsto \mathsf{0})\Vdash t\!:\! A$ and $p(m\mapsto \mathsf{1})(k\mapsto \mathsf{1})\Vdash t\!:\! A$. By IH $p(k\mapsto \mathsf{0})\Vdash t\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t\!:\! A$ and by the definition $p\Vdash t\!:\! A$.
	\end{enumerate}	
	The statement follows similarly when $p\Vdash A$ by $\mathrm{F}_{\mathsf{N}_1}$ and $\mathrm{F}_{\mathsf{N}_2}$.
	
	\item \label{pilocaltermforced} Let $p\Vdash A$ by $\mathrm{F}_\Pi$ and $p\vdash A\red^\ast \Pi(x\!:\! F) G$. Let $q\leqslant p$. If $q\leqslant p(m\mapsto b)$  then we have directly $q\Vdash a \!:\! F\Rightarrow q\Vdash t\,a\!:\! G[a]$ and $q\Vdash a=b\!:\! F \Rightarrow q\Vdash t\,a = t\,b \!:\! G[a]$. Otherwise, we have $q(m\mapsto b)\leqslant p(m\mapsto b)$. Let $q\Vdash a\!:\! F$. By monotonicity $q(m\mapsto \mathsf{0})\Vdash a\!:\! F$ and $q(m\mapsto \mathsf{1})\Vdash a\!:\! F$ and we have $q(m\mapsto \mathsf{0})\Vdash t\,a\!:\! G[a]$ and $q(m\mapsto \mathsf{1})\Vdash t\,a \!:\! G[a]$. By IH we have $q\Vdash t\,a\!:\! G[a]$. Let $q\Vdash a=b\!:\! F$. By monotonicity $q(m\mapsto \mathsf{0})\Vdash a=b\!:\! F$ and $q(m\mapsto \mathsf{1})\Vdash a=b\!:\! F$ and we have $q(m\mapsto \mathsf{0})\Vdash t\,a=t\,b\!:\! G[a]$ and $q(m\mapsto \mathsf{1})\Vdash t\,a=t\,b\!:\! G[a]$. By IH (\ref{termeqlocal}) $q\Vdash t\,a =t\,b \!:\! G[a]$. Thus we have $p\Vdash t\!:\! A$.
	
	\item \label{sigmalocaltermforced} Let $p\Vdash A$ by $\mathrm{F}_\Sigma$ and let $p\vdash A\red^\ast \Sigma(x\!:\! F) G$. We have $p(m\mapsto \mathsf{0})\Vdash t.1 \!:\! F$ and $p(m\mapsto \mathsf{1})\Vdash t.1 \!:\! F$ and $p(m\mapsto \mathsf{0})\Vdash t.2 \!:\! G[t.1]$ and $p(m\mapsto \mathsf{1})\Vdash t.2 \!:\! G[t.1]$. By IH $p\Vdash t.1 \!:\! F$ and $p\Vdash t.2 \!:\! G[t.1]$. Thus $p\Vdash t\!:\! A$.
	\item Let $p\Vdash A$ by $\mathrm{F}_\mathsf{U}$. The statement then follows similarly to Lemma~\ref{LEM:typeIntroLocal}.
	\item \label{locallocaltermforced} Let $p\Vdash A$ by $\mathrm{F}_\mathrm{Loc}$ and let $p\vdash A\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}], k\notin\dom{p}$. If $k=m$ then by the definition $p\Vdash t\!:\! A$. If $k\neq m$ then by monotonicity $p(k\mapsto \mathsf{0})(m\mapsto \mathsf{0})\Vdash t\!:\! A$ and $p(k\mapsto \mathsf{0})(m\mapsto \mathsf{1})\Vdash t\!:\! A$ and $p(k\mapsto \mathsf{1})(m\mapsto \mathsf{0})\Vdash t\!:\! A$ and $p(k\mapsto \mathsf{1})(m\mapsto \mathsf{1})\Vdash t\!:\! A$. By IH $p(k\mapsto \mathsf{0})\Vdash t\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t\!:\! A$. By the definition $p\Vdash t\!:\! A$.
\end{enumerate}

\item \label{termeqlocal} From $p(m\mapsto \mathsf{0})\Vdash t=u \!:\! A$ and $p(m\mapsto \mathsf{0})\Vdash t=u\!:\! A$ we have $p(m\mapsto \mathsf{0})\Vdash t\!:\! A$ and $p(m\mapsto \mathsf{1})\Vdash t\!:\! A$ and $p(m\mapsto \mathsf{0})\Vdash u\!:\! A$ and $p(m\mapsto \mathsf{1})\Vdash u\!:\! A$ and $p(m\mapsto \mathsf{0})\Vdash A$ and $p(m\mapsto \mathsf{1})\Vdash A$. By Lemma~\ref{LEM:typeIntroLocal} $p\Vdash A$. By induction on the derivation of $p\Vdash A$.
\begin{enumerate}
	\item Let $p\Vdash A$ by $\mathrm{F}_\mathsf{N}$. By (\ref{natlocaltermforced}) we have $p\Vdash t\!:\! A$. By induction on the derivation of $p\Vdash t\!:\! A$.
	\begin{enumerate}
		\item If $p\vdash t\red^\ast \xoverline{n}\!:\! A$. By induction on the derivation of $p\Vdash u\!:\! A$
		\begin{enumerate}
			\item If $u$ has a canonical $p$-whnf then $p\vdash u\red^\ast \xoverline{n}\!:\! A$ and $p\Vdash t=u\!:\! A$.
			\item \label{natermeqlocalright} Otherwise, $p\Vdash u\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]\!:\! A, k\notin\dom{p}$. If $k=m$ then by the definition $p\Vdash t=u \!:\! A$. If $k\neq m$ then by monotonicity $p(k\mapsto \mathsf{0})(m\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $p(k\mapsto \mathsf{0})(m\mapsto \mathsf{1})\Vdash t= u\!:\! A$ and $p(k\mapsto \mathsf{1})(m\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $p(k\mapsto \mathsf{1})(m\mapsto \mathsf{1})\Vdash t= u\!:\! A$. By IH, $p(k\mapsto \mathsf{0})\Vdash t=u \!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t=u\!:\! A$. By the definition $p\Vdash t=u\!:\! A$.
		\end{enumerate}
		\item If $p\vdash t\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]\!:\! A, k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash t\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t\!:\! A$. The statement follows similarly to (\ref{natermeqlocalright}).
	\end{enumerate}
	The statement follows similarly when $p\Vdash A$ holds by $\mathrm{F}_{\mathsf{N}_1}$ and $\mathrm{F}_{\mathsf{N}_2}$.
	
	\item Let $p\Vdash A$ by $\mathrm{F}_\Pi$ and $p\vdash A\red^\ast \Pi(x\!:\! F) G$. By (\ref{pilocaltermforced}) we have $p\Vdash t\!:\! A$ and $p\Vdash u\!:\! A$. Let $q\leqslant p$. If $q\leqslant p(m\mapsto b)$ for some $b\in \{\mathsf{0},\mathsf{1}\}$ then we have $q\Vdash a \!:\! F\Rightarrow q\Vdash t\,a=u\,a\!:\! G[a]$. Otherwise, we have $q(m\mapsto b)\leqslant p(m\mapsto b)$. Let $q\Vdash a\!:\! F$. By monotonicity $q(m\mapsto \mathsf{0})\Vdash a\!:\! F$ and $q(m\mapsto \mathsf{1})\Vdash a\!:\! F$ and we have $q(m\mapsto \mathsf{0})\Vdash t\,a=u\,a\!:\! G[a]$ and $q(m\mapsto \mathsf{1})\Vdash t\,a=u\,a \!:\! G[a]$. By IH we have $q\Vdash t\,a=u\,a\!:\! G[a]$. Thus $p\Vdash t=u\!:\! A$.
	
	\item \label{sigmalocaltermforced} Let $p\Vdash A$ by $\mathrm{F}_\Sigma$ and let $p\vdash A\red^\ast \Sigma(x\!:\! F) G$. By (\ref{sigmalocaltermforced}) $p\Vdash t\!:\! A$ and $p\Vdash u\!:\! A$. We have $p(m\mapsto \mathsf{0})\Vdash t.1 = u.1 \!:\! F$ and $p(m\mapsto \mathsf{1})\Vdash t.1=u.1 \!:\! F$ and $p(m\mapsto \mathsf{0})\Vdash t.2=u.2 \!:\! G[t.1]$ and $p(m\mapsto \mathsf{1})\Vdash t.2=u.2 \!:\! G[t.1]$. By IH $p\Vdash t.1=u.1 \!:\! F$. Since we have $p(m\mapsto \mathsf{0})\Vdash u.2 \!:\! G[t.1]$ and $p(m\mapsto \mathsf{1})\Vdash u.2 \!:\! G[t.1]$ then by IH(\ref{termintromontone}) $p\Vdash u.2 \!:\! G[t.1]$. By IH we have $p\Vdash t.2 = u.2 \!:\! G[t.1]$. Thus we have $p\Vdash t=u\!:\! A$.
	\item Let $p\Vdash A$ by $\mathrm{F}_\mathsf{U}$. The statement then follows similarly to Lemma~\ref{LEM:typeEqLocal}.
	\item Let $p\Vdash A$ by $\mathrm{F}_\mathrm{Loc}$ and let $p\vdash A\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}], k\notin\dom{p}$. By (\ref{locallocaltermforced}) $p\Vdash t\!:\! A$ and $p\Vdash u\!:\! A$. If $k=m$ then by the definition $p\Vdash t=u\!:\! A$. If $k\neq m$ then by monotonicity $p(k\mapsto \mathsf{0})(m\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $p(k\mapsto \mathsf{0})(m\mapsto \mathsf{1})\Vdash t=u\!:\! A$ and $p(k\mapsto \mathsf{1})(m\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $p(k\mapsto \mathsf{1})(m\mapsto \mathsf{1})\Vdash t=u\!:\! A$. By IH $p(k\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t=u\!:\! A$. By the definition $p\Vdash t=u\!:\! A$.\qedhere
\end{enumerate}
\end{enumerate}
\end{proof}

\begin{cor}[Locality]
	\label{LEM:localCharacter}
	If $p \vartriangleleft S$ and $q \Vdash J$ for all $q\in S$ then $p\Vdash J$.
\end{cor}
\begin{proof}
Follows from Lemma~\ref{LEM:typeIntroLocal}, Lemma~\ref{LEM:termIntroEqLocal}, and Lemma~\ref{LEM:typeEqLocal} by induction.
\end{proof}

\begin{lem}
\label{LEM:equivalentTypesHaveEqualPers}
\renewcommand{\theenumi}{\alph{enumi}}
Let $p\Vdash A=B$. \begin{enumerate}
\item If $p \Vdash t \!:\!  A$ then $p\Vdash t \!:\!  B$ and if $p\Vdash u\!:\! B$ then $p\Vdash u\!:\! A$. 
\item If $p \Vdash t = u\!:\!  A$ then $p \Vdash t=u\!:\!  B$ and if $p\Vdash v=w \!:\! B$ then $p\Vdash v=w \!:\! A$.
\end{enumerate}
\end{lem}
\begin{proof}
By induction on the derivations of $p\Vdash A$, $p\Vdash B$ and $p\Vdash A=B$
\begin{enumerate}
\item Let $p\vdash A\red^\ast \mathsf{N}$ and $p\vdash B\red^\ast \mathsf{N}$
\begin{enumerate}
	\item Let $p\Vdash t\!:\! A$. By Lemma~\ref{LEM:BaseTypeCanonicity} there is a partition $p\vartriangleleft S$ where for each $q\in S$ $q\vdash t\red^\ast \xoverline{n}\!:\! A$ for some $n\in \mathbb{N}$. But then $q\vdash t\red^\ast \xoverline{n}\!:\! B$ and $q\Vdash t\!:\! B$. By locality $p\Vdash t\!:\! B$. Similarly if $p\Vdash u\!:\! B$ then $p\Vdash u\!:\! A$.
	\item Let $p\Vdash t=u\!:\! A$ then there is a partition $p\vartriangleleft S$ where for each $q\in S$ $q\vdash t\red^\ast \xoverline{n}\!:\! A$ and $q\vdash u\red^\ast \xoverline{n}\!:\! A$ for some $n\in \mathbb{N}$. But then $q\vdash t\red^\ast \xoverline{n}\!:\! B$ and $q\vdash u\red^\ast \xoverline{n}\!:\! B$ and $q\Vdash t=u\!:\! B$. By locality $p\Vdash t=u\!:\! B$. Similarly $p\Vdash v=w\!:\! A$ whenever $p\Vdash v=w\!:\! B$
\end{enumerate}
\item Let $p\vdash A\red^\ast \Pi(x\!:\! F) G$ and $p\vdash B\red^\ast \Pi(x\!:\! H) E$.
\begin{enumerate}
	\item Let $p\Vdash t\!:\! A$ and $q\leqslant p$. Let $q\Vdash a\!:\! H$. From $p\Vdash A=B$ we get $p\Vdash F=H$ and by monotonicity $q\Vdash F=H$. By IH $q\Vdash a\!:\! F$. Thus we have $q\Vdash t\,a\!:\! G[a]$. Since $q\Vdash G[a]=E[a]$, by IH $q\Vdash t\,a \!:\! E[a]$. Similarly if $q\Vdash a=b\!:\! H$ by monotonicity $q\Vdash a=b\!:\! H$ and by IH $q\Vdash a=b\!:\! F$. Thus $q\Vdash t\,a = t\,b \!:\! G[a]$ and since $q\Vdash G[a]=E[a]$. By IH $q\Vdash t\,a=t\,b \!:\! E[a]$. Similarly $p\Vdash u\!:\! A$ when $p\Vdash u\!:\! B$.
	\item Let $p\Vdash t=u\!:\! A$ and $q\leqslant p$. Let $q\Vdash a\!:\! H$. Similarly to the above we get $q\Vdash t\,a = u\,a \!:\! \!:\! E[a]$. Thus showing $q\Vdash t=u\!:\! B$. Similarly we have $q\Vdash v=w\!:\! A$ when $q\Vdash v=w\!:\! B$
\end{enumerate}
\item Let $p\vdash A\red^\ast \Sigma(x\!:\! F) G$ and $p\vdash B\red^\ast \Sigma(x\!:\! H) E$.
\begin{enumerate}
	\item Let $p\Vdash t\!:\! A$. We have $p\Vdash t.1 \!:\! F$ and $p\Vdash t.2 \!:\! G[t.1]$. From $p\Vdash A=B$ we get $p\Vdash F=H$ and by IH $p\Vdash t.1 \!:\! H$. From $p\Vdash A=B$ we get $p\Vdash G[t.1]=E[t.1]$ and by IH $p\Vdash t.2 \!:\! E[t.1]$. Thus $p\Vdash t\!:\! B$. Similarly we have $p\Vdash u\!:\! A$ when $p\Vdash u\!:\! B$.
	
	\item Let $p\Vdash t=u\!:\! A$. We have $p\Vdash t.1 =u.1 \!:\! F$ and $p\Vdash t.2 =u.2\!:\! G[t.1]$. From $p\Vdash A=B$ we get $p\Vdash F=H$ and by IH $p\Vdash t.1=u.1 \!:\! H$. From $p\Vdash A=B$ we get $p\Vdash G[t.1]=E[t.1]$ and by IH $p\Vdash t.2=u.2 \!:\! E[t.1]$. Thus $p\Vdash t=u\!:\! B$. Similarly we have $p\Vdash v=w\!:\! A$ when $p\Vdash v=w\!:\! B$.
	\end{enumerate}
	\item If either $A$ or $B$ does not reduce to a canonical $p$-whnf then by Lemma~\ref{forcedtypeslocallyreducetocanonical} we have a partition $p\vartriangleleft S$ where for each $q \in S$ both $A$ and $B$ have canonical whnf and we can show the statement for each $q\in S$ by the above. By locality the statement follows for~$p$.\qedhere
\end{enumerate}
\end{proof}

Immediately from the definition we have
\begin{lem}
If $p \Vdash A$ then $p\Vdash A=A$.
\end{lem}

\begin{lem}
If $p\Vdash A=B$ then $p\Vdash B=A$.
\end{lem}
\begin{proof}
If both $A$ and $B$ have canonical $p$-whnf then the statement follows by induction from the definition and Lemma~\ref{LEM:equivalentTypesHaveEqualPers}. Otherwise, by Lemma~\ref{forcedtypeslocallyreducetocanonical} we have a partition $p\vartriangleleft S$ where both $A$ and $B$ have canonical $q$-whnf for all $q\in S$. By monotonicity $q\Vdash A=B$ and it follows by the above that $q\Vdash B=A$. By locality $p\Vdash B=A$.
\end{proof}

\begin{lem}
\label{LEM:typeequiv_refl,symm,trans}
If $p\Vdash A=B$ and  $p\Vdash B=C$ then $p \Vdash A=C$.
\end{lem}
\begin{proof}
\leavevmode
Let $p\Vdash A=B$ and $p\Vdash B=C$. We then have that $p\Vdash A$, $p\Vdash B$ and $p\Vdash C$. Thus $A$, $B$ and $C$ have proper $p$-whnf. If any of these proper $p$-wnf is not canonical then by Lemma~\ref{forcedtypeslocallyreducetocanonical} we can find a partition $p\vartriangleleft S$ where all three have canonical $q$-whnf for all $q\in S$. By monotonicity $q\Vdash A=B$ and $q\Vdash B=C$ for all $q\in S$. If we can then show that $q\Vdash A=C$ for all $q\in S$ then by locality we will have $p\Vdash A=C$. Thus we can assume w.l.o.g that $A$, $B$ and $C$ have canonical $p$-whnf.

By induction on the derivations of $p\Vdash A$, 
\begin{enumerate}[leftmargin=10mm]
\item Let $p\Vdash A$ by $\mathrm{F}_\mathsf{N}$. Since by assumption $B$ has a canonical $p$-wnf and $p\Vdash A=B$ then $p\vdash B\red^\ast \mathsf{N}$. Similarly $p\vdash C\red^\ast \mathsf{N}$ and we have $p\Vdash A=C$

The statement follows similarly when $p\Vdash A$ holds by $\mathrm{F}_{\mathsf{N}_0}$, $\mathrm{F}_{\mathsf{N}_1}$ and $\mathrm{F}_{\mathsf{N}_2}$.

\item Let $p\Vdash A$ by $\mathrm{F}_\Pi$ and $p\vdash A\red^\ast \Pi(x\!:\! F) G$. From $p\Vdash A=B$ and since by assumption $B$ has a canonical $p$-whnf we have $p\vdash B\red^\ast \Pi(x\!:\! H) E$ and $p\Vdash F=H$ and $\forall q\leqslant p (q\Vdash a \!:\! F \Rightarrow q\Vdash G[a]=E[a])$. Since $p\Vdash B=C$ and by assumption $C$ has a canonical $p$-whnf we have $p\vdash C\red^\ast \Pi(x\!:\! T) R$ and $p\Vdash H=T$ and $\forall q\leqslant p (q\Vdash b\!:\! H \Rightarrow q\Vdash E[b]=R[b])$. 

By IH $p\Vdash F=T$. Let $q\leqslant p$ and $q\Vdash a\!:\! F$. By monotonicity $q\Vdash F=H$ and by Lemma~\ref{LEM:equivalentTypesHaveEqualPers} $q\Vdash a\!:\! H$. Thus $q\Vdash E[a]=R[a]$. But $q\Vdash G[a]=E[a]$. By IH $q\Vdash G[a]=R[a]$. Thus we have $p\Vdash A=C$.

The statement follows similarly when $p\Vdash A$ holds by $\mathrm{F}_\Sigma$. 

\item[$(\mathbf{F_\mathsf{U}})$] Since $p\Vdash A=B$ and $p\Vdash B=C$, we have $B\coloneqq \mathsf{U}$ and $C\coloneqq \mathsf{U}$ and the statements follows.\qedhere
\end{enumerate}
\end{proof}

Immediately from the definition we have the following 
\begin{lem}
If $p\Vdash t\!:\! A$ then $p\Vdash t=t\!:\! A$.
\end{lem}

\begin{lem}
If $p\Vdash t=u\!:\! A$ and then $p \Vdash u=t\!:\! A$.
\end{lem}
\begin{proof}
Let $p\Vdash t=u\!:\! A$. We have $p\Vdash t\!:\! A$, $p\Vdash u\!:\! A$ and $p\Vdash A$. By induction on the derivation of $p\Vdash A$.
\begin{enumerate}
\item Let $p\Vdash A$ by $\mathrm{F}_\mathsf{N}$. Since $p\Vdash t=u\!:\! A$ we have a partition (Lemma~\ref{LEM:BaseTypeCanonicity}) $p\vartriangleleft S$ where for each $q\in S$ we have $q\vdash t\red^\ast \xoverline{n}\!:\! A$ and $q\vdash u\red^\ast \xoverline{n}\!:\! A$ for some $n\in \mathbb{N}$. Hence $q\Vdash u=t \!:\! A$ for all $q\in S$. By locality $p\Vdash t=u\!:\! A$.

The statement follows similarly when $p\Vdash A$ is derived by $\mathrm{F}_{\mathsf{N}_1}$ and $\mathrm{F}_{\mathsf{N}_2}$.

\item Let $p\Vdash A$ by $\mathrm{F}_\Pi$ and let $p\vdash A\red^\ast \Pi(x\!:\! F) G$. Let $q\leqslant p$ and $q\Vdash a\!:\! F$ we then have $q\Vdash t\,a=u\,a \!:\! G[a]$. We have $q\Vdash G[a]$ and by IH $q\Vdash u\,a=t\,a \!:\! G[a]$. Thus $p\Vdash u=t\!:\! A$.
  
\item Let $p\Vdash A$ by $\mathrm{F}_\Sigma$ and let $p\vdash A\red^\ast \Sigma(x\!:\! F) G$. We have $p\Vdash t.1=u.1 \!:\! F$ and $p\Vdash t.2 = u.2 \!:\! G[t.1]$. Since $q\Vdash F$, by IH $p\Vdash u.1 = t.1 \!:\! F$. Since $p\Vdash A$ we have  $p\Vdash G[t.1]=G[u.1]$. By Lemma~\ref{LEM:equivalentTypesHaveEqualPers} $p\Vdash t.2 = u.2 \!:\! G[u.1]$. Since $p\Vdash G[u.1]$, by IH $p\Vdash u.2 = t.2 \!:\! G[u.1]$. Thus $p\Vdash u=t\!:\! A$.

\item Let $p\Vdash A$ by $\mathrm{F}_\mathsf{U}$. The statement then follows similarly to Lemma~\ref{LEM:typeequiv_refl,symm,trans}

\item  Let $p\Vdash A$ by $\mathrm{F}_\mathrm{Loc}$ and let $p\vdash A\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}], k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash A$ and $p(k\mapsto \mathsf{1})\Vdash A$. Since $p\Vdash t=u\!:\! A$ we have that $p(k\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t=u \!:\! A$. By IH $p(k\mapsto \mathsf{0})\Vdash u=t\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash u=t\!:\! A$. By the definition $p\Vdash u=t\!:\! A$.\qedhere
\end{enumerate}
\end{proof}

\begin{lem}
If $p\Vdash t=u\!:\! A$ and $p\Vdash u=v\!:\! A$ then $p\Vdash t=v\!:\! A$.
\end{lem}
\begin{proof}
Let $p\Vdash t=u\!:\! A$ and  $p\Vdash u=v\!:\! A$. We have $p\Vdash A$, $p\Vdash t\!:\! A$, $p\Vdash u\!:\! A$ and $p\Vdash v\!:\! A$. By induction on the derivation of $p\Vdash A$.
\begin{enumerate}
\item Let $p\Vdash A$ by $\mathrm{F}_\mathsf{N}$. By Lemma~\ref{LEM:BaseTypeCanonicity} there is a partition $p\vartriangleleft S$ where for each $q\in S$ we have $q\vdash t\red^\ast \xoverline{n}\!:\! A$, $q\vdash u\red^\ast \xoverline{n}\!:\! A$, and $q\vdash v\red^\ast \xoverline{n}\!:\! A$. Thus $q\Vdash t=v\!:\! A$ for all $q\in S$. By locality $q\Vdash t=v\!:\! A$.

The statement follows similarly when $p\Vdash A$ by $\mathrm{F}_{\mathsf{N}_1}$ and $\mathrm{F}_{\mathsf{N}_2}$

\item Let $p\Vdash A$ by $\mathrm{F}_\Pi$ and let $p\vdash A\red^\ast \Pi(x\!:\! F) G$. Let $q\leqslant p$ and $q\Vdash a\!:\! F$. We have then $q\Vdash t\,a=u\,a \!:\! G[a]$ and $q\Vdash u\,a=v\,a\!:\! G[a]$. By IH $q\Vdash t\,a = v\,a \!:\! G[a]$. Thus $p\Vdash t=v\!:\! A$.

\item Let $p\Vdash A$ by $\mathrm{F}_\Sigma$ and let $p\vdash A\red^\ast \Sigma(x\!:\! F) G$. Since $p\Vdash t=u\!:\! A$ we have that $p\Vdash t.1 = u.1 \!:\! F$ and $p\Vdash t.2 = u.2 \!:\! G[t.1]$. Similarly we have that $p\Vdash u.1 = v.1 \!:\! F$ and $p\Vdash u.2 = v.2 \!:\! G[u.1]$. Since $p\Vdash A$ we have that $p\Vdash G[t.1]=G[u.1]$ and by Lemma~\ref{LEM:equivalentTypesHaveEqualPers} $p\Vdash u.2 = v.2 \!:\! G[t.1]$. By IH we have $p\Vdash t.1 = v.1 \!:\! F$ and $p\Vdash t.2 = v.2 \!:\! G[t.1]$. We have then that $p\Vdash t= v\!:\! A$.

\item Let $p\Vdash A$ by $\mathrm{F}_\mathsf{U}$. The statement then follows similarly to Lemma~\ref{LEM:typeequiv_refl,symm,trans}.

\item Let $p\Vdash A$ by $\mathrm{F}_\mathrm{Loc}$ and let $p\vdash A\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}], k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash A$ and $p(k\mapsto \mathsf{1})\Vdash A$. We have that $p(k\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t=u \!:\! A$ and $p(k\mapsto \mathsf{0})\Vdash u=v\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash u=v\!:\! A$. By IH $p(k\mapsto \mathsf{0}) \Vdash t=v\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t=v\!:\! A$. By the definition $p\Vdash t=v\!:\! A$.\qedhere
\end{enumerate}
\end{proof}

\noindent
Theorem ~\ref{properties} then follows from the above.

\section{Soundness}
In this section we show that the type theory described in Section~\ref{SEC:Forcingextensionoftypetheory} is sound with respect to the semantics described in Section~\ref{SEC:semantics}. I.e.\ we aim to show that $p\Vdash J$ whenever $\vdash_p J$. 

\begin{lem}
\label{LEM:types_reductionimplyequiv}
If $p\vdash A \red^\ast B$ and $p\Vdash B$ then $p\Vdash A$ and $p\Vdash A=B$.
\end{lem}
\begin{proof}
Follows from the definition by induction on the derivation of $p\Vdash B$.
\end{proof}
\begin{lem}
\label{LEM:terms_onestepreductionimplyequiv}
Let $p\Vdash A$. If $p\vdash t \rightarrowtriangle u\!:\! A$ and $p\Vdash u\!:\! A$ then $p\Vdash t\!:\! A$ and $p\Vdash t=u\!:\! A$.
\end{lem}
\begin{proof
Let $p\vdash t \rightarrowtriangle u\!:\! A$ and $p\Vdash u\!:\! A$. By induction on the derivation of $p\Vdash A$.
\begin{enumerate}
\item Let $p\Vdash A$ by $\mathrm{F}_\mathsf{U}$. The statement follows similarly to Lemma~\ref{LEM:types_reductionimplyequiv}. 

\item Let $p\Vdash A$ by $\mathrm{F}_\mathsf{N}$. By induction on the derivation of $p\Vdash u\!:\! A$. If $p\vdash u\red^\ast \xoverline{n} \!:\! \mathsf{N}$ then $p\vdash t\red^\ast \xoverline{n} \!:\! \mathsf{N}$ and the statement follows by the definition. If $p\vdash u\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}]\!:\! A, k\notin \dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash u\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash u\!:\! A$ then since $p(k\mapsto b)\vdash t\rightarrowtriangle u\!:\! A$, by IH  $p(k\mapsto \mathsf{0})\Vdash t\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t\!:\! A$ and $p(k\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t= u\!:\! A$. By the definition $p\Vdash t\!:\! A$ and $p\Vdash t=u \!:\! A$. 

The statement follows similarly for $\mathrm{F}_{\mathsf{N}_1}$ and $\mathrm{F}_{\mathsf{N}_2}$.

\item Let $p\Vdash A$ by $\mathrm{F}_\Pi$ and let $p\vdash A \red^\ast \Pi(x\!:\! F)G$. Let $q\leqslant p$ and $q\Vdash a\!:\! F$. We have $q\vdash t\,a\rightarrowtriangle u\,a \!:\! G[a]$. By IH $q\Vdash t\,a \!:\! G[a]$ and $q\Vdash t\,a=u\,a \!:\! G[a]$. If $q\Vdash a=b \!:\! F$ we similarly get $q\Vdash t\,b\!:\! G[b]$ and $q\Vdash t\,b=u\,b\!:\! G[b]$. Since $q\Vdash G[a]=G[b]$, by Lemma~\ref{LEM:equivalentTypesHaveEqualPers}  $q\Vdash t\,b=u\,b\!:\! G[a]$. But $q\Vdash u\,a=u\,b\!:\! G[a]$. By symmetry and transitivity $q\Vdash t\,a = t\,b \!:\! G[a]$. Thus $p\Vdash t\!:\! A$ and $p\Vdash t=u\!:\! A$.

\item Let $p\Vdash A$ by $\mathrm{F}_\Sigma$ and let $p\vdash A \red^\ast \Sigma(x\!:\! F)G$. From $p\vdash t\rightarrowtriangle u\!:\! A$ we have $\vdash_p t\!:\! A$ and we have $p\vdash t.1 \rightarrowtriangle u.1\!:\! F$ and $p\vdash t.2\rightarrowtriangle u.2\!:\! G[u.1]$. By IH $p\Vdash t.1 \!:\! F$ and $p\Vdash t.1 = u.1 \!:\! F$. By IH $p\Vdash t.2 \!:\! G[u.1]$ and $p\Vdash t.2 = u.2 \!:\! G[u.1]$. But since $p\Vdash A$ and we have shown $p\Vdash t.1 = u.1 \!:\! F$ we get $p\Vdash G[t.1]=G[u.1]$. By Lemma~\ref{LEM:equivalentTypesHaveEqualPers} $p\Vdash t.2 \!:\! G[t.1]$ and $p\Vdash t.2=u.2\!:\! G[t.1]$. Thus $p \Vdash t\!:\! A$ and $p \Vdash t=u\!:\! A$

\item Let $p\Vdash A$ by $\mathrm{F}_\mathrm{Loc}$. Let $p\vdash A\red^\ast \mathbb{E}[\mathsf{f}\,\xoverline{k}], k\notin\dom{p}$ and $p(k\mapsto \mathsf{0})\Vdash A$ and $p(k\mapsto \mathsf{1})\Vdash A$. Since $p\Vdash u\!:\! A$ we have $p(k\mapsto \mathsf{0})\Vdash u\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash u\!:\! A$. But we have $p(k\mapsto b)\vdash t\rightarrowtriangle u\!:\! A$. By IH $p(k\mapsto \mathsf{0})\Vdash t\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t\!:\! A$ and $p(k\mapsto \mathsf{0})\Vdash t=u\!:\! A$ and $p(k\mapsto \mathsf{1})\Vdash t= u \!:\! A$. By the definition $p\Vdash t\!:\! A$ and $p\Vdash t=u \!:\! A$. \qedhere
\end{enumerate}
\end{proof}

\begin{cor}
\label{COR:terms_reductionimplyequiv}
Let $p\vdash t \red^\ast u\!:\! A$ and $p\Vdash A$. If $p\Vdash u\!:\! A$ then $p\Vdash t\!:\! A$ and $p\Vdash t=u\!:\! A$.
\end{cor}


\begin{cor}
\label{COR:genericwelltyped}
$\Vdash \mathsf{f}\!:\!  \mathsf{N}\rightarrow {\mathsf{N}_2}$. 
\end{cor}
\begin{proof}
It's direct to see that $\Vdash \mathsf{N}\rightarrow {\mathsf{N}_2}$. For an arbitrary condition $p$ let $p\Vdash n\!:\! \mathsf{N}$. By Lemma~\ref{LEM:BaseTypeCanonicity} we have a partition $p\vartriangleleft S$ where for each $q\in S$, $q\vdash n\red^\ast \xoverline{m}\!:\! \mathsf{N}$ for some $m\in\mathbb{N}$.  We have thus a reduction $q\vdash \mathsf{f}\,n\red^\ast \mathsf{f}\,\xoverline{m}\!:\! {\mathsf{N}_2}$. If $m\in \dom{q}$ then $q\vdash \mathsf{f}\,n\red^\ast \mathsf{f}\,\xoverline{m}\rightarrowtriangle q(m) \!:\! {\mathsf{N}_2}$ and by definition $q \Vdash \mathsf{f}\,n \!:\! {\mathsf{N}_2}$. If $m \notin \dom{q}$ then $q(m\mapsto \mathsf{0}) \vdash \mathsf{f}\,n\red^\ast \mathsf{f}\xoverline{m}\rightarrowtriangle \mathsf{0}\!:\! {\mathsf{N}_2}$ and $q(m_j\mapsto \mathsf{1}) \vdash \mathsf{f}\,n\red^\ast \mathsf{f}\xoverline{m}\rightarrowtriangle \mathsf{1}\!:\! {\mathsf{N}_2}$. Thus $q(m\mapsto \mathsf{0}) \Vdash \mathsf{f}\,n \!:\! {\mathsf{N}_2}$ and $q(m\mapsto \mathsf{1})\Vdash \mathsf{f}\,n \!:\! {\mathsf{N}_2}$. By the definition $q \Vdash \mathsf{f}\,n \!:\! {\mathsf{N}_2}$. We thus have that $q \Vdash \mathsf{f}\,n \!:\! {\mathsf{N}_2}$ for all $q\in S$ and by locality $p\Vdash \mathsf{f}\,n \!:\! {\mathsf{N}_2}$. 

Let $p\Vdash a=b\!:\! \mathsf{N}$. By Lemma~\ref{LEM:BaseTypeCanonicity} there is a partition $p\vartriangleleft S$ where for each $q\in S$, $q\vdash a\red^\ast \xoverline{m} \!:\! \mathsf{N}$ and $q\vdash b \red^\ast \xoverline{m}\!:\! \mathsf{N}$ for some $m\in \mathbb{N}$. We then have $q \vdash \mathsf{f}\,a \red^\ast \mathsf{f}\,\xoverline{m} \!:\! {\mathsf{N}_2}$ and $q\vdash \mathsf{f}\,b\red^\ast \mathsf{f}\,\xoverline{m}\!:\! {\mathsf{N}_2}$. If $m\in \dom{q}$ then $q \vdash \mathsf{f}\,a\red^\ast q(m)\!:\! {\mathsf{N}_2}$ and $q\vdash \mathsf{f}\,b\red^\ast q(m)\!:\! {\mathsf{N}_2}$. By Corollary~\ref{COR:terms_reductionimplyequiv}, symmetry and transitivity $q \Vdash \mathsf{f}\,a=\mathsf{f}\,b \!:\! {\mathsf{N}_2}$. If on the other hand $m \notin\dom{q}$ then $q(m\mapsto \mathsf{0}) \Vdash \mathsf{f}\,a=\mathsf{f}\,b \!:\! {\mathsf{N}_2}$ and $q(m\mapsto \mathsf{1})\Vdash \mathsf{f}\,a=\mathsf{f}\,b \!:\! {\mathsf{N}_2}$. By the definition $q \Vdash \mathsf{f}\,a=\mathsf{f}\,b\!:\! {\mathsf{N}_2}$. Thus $q \Vdash \mathsf{f}\,a=\mathsf{f}\,b\!:\! {\mathsf{N}_2}$ for all $q\in S$. By locality $p\Vdash \mathsf{f}\,a=\mathsf{f}\,b\!:\! {\mathsf{N}_2}$. Hence $\Vdash \mathsf{f}\!:\! \mathsf{N}\rightarrow {\mathsf{N}_2}$.
\end{proof}

\begin{lem}
\label{LEM:forcingTermNegation}
If $\vdash_p t\!:\! \neg A$ and $p\Vdash A$ then $p\Vdash t\!:\! \neg A$ iff for all $q\leqslant p$ there is no term $u$ such that $q\Vdash u\!:\! A$.
\end{lem}
\begin{proof}
Let $p\Vdash A$ and $\vdash_p t\!:\! \neg A$. We have directly that $p\Vdash \neg A$. Assume $p\Vdash t\!:\! \neg A$. If $q \Vdash u\!:\! A$ for some $q\leqslant p$, then $q\Vdash t\,u \!:\! {\mathsf{N}_0}$ which is impossible. Conversely, assume it is the case that for all  $q \leqslant p$ there is no $u$ for which $q\Vdash u\!:\! A$. Since $r\Vdash a\!:\! A$ and $r\Vdash a=b\!:\! A$ never hold for any $r\leqslant p$, the statements  ``$r\Vdash a\!:\! A \Rightarrow r\Vdash t\,a \!:\! {\mathsf{N}_0}$'' and ``$r\Vdash a=b \!:\! A \Rightarrow r\Vdash t\,a=t\,b \!:\! {\mathsf{N}_0}$'' hold trivially.
\end{proof}


\begin{lem}
\label{LEM:markovpremisewitnesswelltyped}
$\Vdash \mathsf{w} \!:\! \neg\neg (\Sigma(x\!:\! \mathsf{N}) \mathsf{IsZero}(\mathsf{f}\,x))$.
\end{lem}
\begin{proof}
By Lemma~\ref{LEM:forcingTermNegation} it is enough to show that for all $q$ there is no term $u$ for which $q\Vdash u\!:\! \neg (\Sigma(x\!:\! \mathsf{N}) \mathsf{IsZero}(\mathsf{f}\,x))$. Assume $q\Vdash u\!:\!\neg (\Sigma(x\!:\! \mathsf{N}) \mathsf{IsZero}(\mathsf{f}\,x))$ for some $u$. Let $m\notin\dom{q}$ we have then $q(m\mapsto \mathsf{0}) \Vdash (\overline{m},\mathsf{0}) \!:\! \Sigma(x\!:\! \mathsf{N}) \mathsf{IsZero}(\mathsf{f}\,x)$ thus $q(m\mapsto \mathsf{0}) \Vdash u\,(\xoverline{m},\mathsf{0})\!:\! {\mathsf{N}_0}$ which is impossible.\end{proof}

Let $\Gamma \coloneqq x_1\!:\! A_1\dots,x_n\!:\! A_n$ and $\rho \coloneqq a_1,\dots,a_n$. Let $A_i\rho \coloneqq A_i[a_1/x_1,\dots,a_{i-1}/x_{i-1}]$. We write $\Delta \vdash_p \rho \!:\! \Gamma$ if $\Delta \vdash_p a_i\!:\! A_i\rho$ for all $i$. Letting $\sigma=b_1,\dots,b_n$, we write $\Delta \vdash_p \rho =\sigma\!:\! \Gamma$ if $\Delta \vdash_p a_i=b_i\!:\! A_i\rho$ for all $i$. We write $p \Vdash \rho\!:\! \Gamma$ if $p\Vdash a_i\!:\! A_i\rho$ for all $i$ and $p\Vdash \rho=\sigma\!:\! \Gamma$ if $p\Vdash a_i=b_i\!:\! A_i\rho$ for all $i$.

\begin{lem}
\label{LEM:evalissub}
If $p\Vdash \rho \!:\! \Gamma$ then $\vdash_p \rho \!:\! \Gamma$. If $p\Vdash \rho = \sigma \!:\! \Gamma$ then $\vdash_p \rho = \sigma \!:\! \Gamma$.
\end{lem}
\begin{proof}
Follows from the definition.
\end{proof}

\begin{defi}\leavevmode
\begin{enumerate}
\item We write $\Gamma\vDash_p A$ if $\Gamma\vdash_p A$ and for all $q\leqslant p$ whenever $q\Vdash \rho \!:\! \Gamma$ then $q\Vdash A\rho$ and whenever $q\Vdash \rho=\sigma\!:\!\Gamma$ then $q\Vdash A\rho=A\sigma$. 
\item We write $\Gamma\vDash_p t\!:\! A$ if $\Gamma\vdash_p t\!:\! A$, $\Gamma\vDash_p A$ and for all $q\leqslant p$ whenever $q\Vdash \rho \!:\! \Gamma$ then $q\Vdash t\rho\!:\! A\rho$ and whenever $q\Vdash \rho = \sigma \!:\! \Gamma$ then $q\Vdash t\rho=t\sigma\!:\! A\rho$.
\item We write $\Gamma\vDash_p A=B$ if $\Gamma\vdash_p A=B$, $\Gamma\vDash_p A$, $\Gamma\vDash_p B$ and for all $q\leqslant p$ whenever $q\Vdash \rho \!:\! \Gamma$ then $q\Vdash A\rho = B\rho$. 
\item We write $\Gamma\vDash_p t=u\!:\! A$ if $\Gamma\vdash_p t=u\!:\! A$, $\Gamma\vDash_p t\!:\! A$, $\Gamma\vDash_p u\!:\! A$  and for all $q\leqslant p$ whenever $q\Vdash \rho \!:\! \Gamma$ then $q\Vdash t\rho = u\rho \!:\! A\rho$.
\end{enumerate}
\end{defi}

In the following we will show that whenever we have a rule 
\AxiomC{$\Gamma_1\vdash_{p_1} J_1$} 
\AxiomC{$\dots$} 
\AxiomC{$\Gamma_\ell \vdash_{p_\ell} J_\ell$} 
\TrinaryInfC{$\Gamma\vdash_p J$}
\DisplayProof
 in the type system then it holds that 
\AxiomC{$\Gamma_1\vDash_{p_1} J_1$} 
\AxiomC{$\dots$} 
\AxiomC{$\Gamma_\ell \vDash_{p_\ell} J_\ell$} 
\TrinaryInfC{$\Gamma\vDash_p J$}
\DisplayProof.
 Which is sufficient to show soundness.

\begin{lem}
\AxiomC{$\Gamma \vDash_{p_1} J$}
\AxiomC{$\dots$}
\AxiomC{$\Gamma \vDash_{p_n} J $} 
\def1pt{1pt}
\RightLabel{$p \vartriangleleft \{p_1,\dots, p_n\}$}
\TrinaryInfC{$\Gamma \vDash_p J $}
\DisplayProof\smallskip
\end{lem}
\begin{proof}
Follows from Corollary~\ref{LEM:localCharacter}.
\end{proof}

\begin{lem}\leavevmode \medskip
\label{soundPiIntro}
\AxiomC{$\Gamma \vDash_p F$ }
\AxiomC{$\Gamma, x\!:\!  F \vDash_p G$}
\BinaryInfC{$\Gamma \vDash_p \Pi (x\!:\!  F) G$}
\DisplayProof
\,
\AxiomC{$\Gamma \vDash_p F$ }
\AxiomC{$\Gamma, x\!:\!  F \vDash_p G$}
\BinaryInfC{$\Gamma \vDash_p \Sigma (x\!:\!  F) G$}
\DisplayProof
\end{lem}
\begin{proof}
Let $q\leqslant p$ and $q\Vdash \rho \!:\! \Gamma$. Let $r\leqslant q$. If $r\Vdash a\!:\! F\rho$, we have $r\Vdash (\rho,a)\!:\! (\Gamma,x\!:\! F)$, thus $r\Vdash G\rho[a]$. If moreover $r\Vdash a=b \!:\! F\rho$ then $r\Vdash (\rho,a)=(\rho,b)\!:\!(\Gamma,x\!:\! F)$ and we have $r\Vdash G\rho[a]=G\rho[b]$. Thus $q\Vdash (\Pi(x\!:\! F) G)\rho$ and $q\Vdash (\Sigma(x\!:\! F)G)\rho$

Let $q\Vdash \rho = \sigma \!:\! \Gamma$. We have that $r\Vdash F\rho=F\sigma$. If $r\Vdash a\!:\! F\rho$ then by Lemma~\ref{LEM:equivalentTypesHaveEqualPers} $r\Vdash a\!:\! F\sigma$. Thus $r\Vdash (\rho,a)=(\sigma,a)\!:\! (\Gamma,x\!:\! F)$. We have $r\Vdash G\rho[a]=G\sigma[a]$. Thus $q\Vdash (\Pi(x\!:\! F) G)\rho= (\Pi(x\!:\! F) G)\sigma$ and $q\Vdash (\Sigma(x\!:\! F)G)\rho = (\Sigma(x\!:\! F)G)\sigma$.\smallskip
\end{proof}

\begin{lem
\label{soundpieq}

\AxiomC{$\Gamma\vDash_p F= H$}
\AxiomC{$\Gamma, x\!:\!  F \vDash_p G =E $}
\BinaryInfC{$\Gamma \vDash_p \Pi (x\!:\! F) G =\Pi (x\!:\! H) E$}
\DisplayProof
\,
\AxiomC{$\Gamma\vDash_p F= H$}
\AxiomC{$\Gamma, x\!:\!  F \vDash_p G =E $}
\BinaryInfC{$\Gamma \vDash_p \Sigma (x\!:\! F) G =\Sigma (x\!:\! H) E$}
\DisplayProof
\end{lem}
\begin{proof}

Let $q\leqslant p$ and $q\Vdash \rho \!:\! \Gamma$. Similarly to Lemma~\ref{soundPiIntro}, we can show $q\Vdash (\Sigma (x\!:\! F) G)\rho$, $q\Vdash (\Sigma (x\!:\! H) E)\rho$, $q\Vdash ( \Pi (x\!:\! F) G)\rho$, and $q\Vdash (\Pi (x\!:\! H) E)\rho$. 

From  $q\Vdash F\rho = H\rho $. Let  $r\leqslant q$ and $r\Vdash a\!:\! F\rho$. We have then $r\Vdash (\rho,a)\!:\!(\Gamma,x\!:\! F)$. Thus $r\Vdash G\rho[a]=E\rho[a]$. Thus $q\Vdash (\Pi(x\!:\! F)G)\rho=(\Pi(x\!:\! H)E)\rho$ and $q\Vdash (\Sigma(x\!:\! F) G)\rho = (\Sigma(x\!:\! H)E)\rho$.
\end{proof}


\begin{lem}
\label{soundLambdaIntro}
\AxiomC{$\Gamma, x \!:\!  F \vDash_p t \!:\!  G$ }
\UnaryInfC{$\Gamma \vDash_p \lambda x.t \!:\!  \Pi (x\!:\! F) G$}
\DisplayProof
\end{lem}
\begin{proof}
Let $q\leqslant p$ and $q\Vdash \rho \!:\! \Gamma$. By Lemma~\ref{LEM:evalissub} $\vdash_q \rho \!:\! \Gamma$. Let $r\leqslant q$ and $r\Vdash d\!:\! F\rho$. Since $\Gamma, x \!:\!  F \vdash_p t \!:\!  G$ we have that $x\!:\! F\rho \vdash_r t\rho \!:\! G\rho$. Since $\vdash_r d\!:\! F\rho$ we have $\vdash_r (\lambda x. t\rho) d = t\rho[d]\!:\! G\rho[d]$. By the reduction rules $(\lambda x. t\rho)d \rightarrowtriangle t\rho[d]$. Thus $r\vdash (\lambda x. t\rho) d \rightarrowtriangle t\rho[d]\!:\! G\rho[d]$. But $r\Vdash (\rho,d)\!:\! (\Gamma,x\!:\! F)$, hence, $r\Vdash t\rho[d]\!:\! G\rho[d]$. By Lemma~\ref{LEM:terms_onestepreductionimplyequiv} we have that $r\Vdash (\lambda x. t\rho)\,d \!:\! G\rho[d]$ and $r\Vdash (\lambda x. t\rho)\,d = t\rho[d]\!:\! G\rho[d]$. 

Let $r\Vdash e=d\!:\! F\rho$ we have similarly that $r\Vdash (\lambda x. t\rho)\,e = t\rho[e]\!:\! G\rho[e]$. We have also that $r\Vdash (\rho,d)=(\rho,e)\!:\! G\rho[d]$, thus  $r\Vdash t\rho[d]=t\rho[e]\!:\! G\rho[d]$ and $r\Vdash G\rho[d]=G\rho[e]$. By Lemma~\ref{LEM:equivalentTypesHaveEqualPers} we have $r\Vdash (\lambda x. t\rho)\,e = t\rho[e]\!:\! G\rho[d]$. By symmetry and transitivity we have $r\Vdash (\lambda x. t\rho)\,d=(\lambda x. t\rho)\,e\!:\! G\rho[d]$. Thus $q\Vdash (\lambda x.t)\rho \!:\! (\Pi(x\!:\! F) G)\rho$.

Let $q\Vdash \rho=\sigma\!:\! \Gamma$. We get $q\Vdash F\rho = F\sigma$.  Similarly to the above we can show  $q\Vdash (\lambda x.t)\sigma \!:\! (\Pi(x\!:\! F) G)\sigma$. Let $r\leqslant q$ and $r\Vdash a\!:\! F\rho$. By Lemma~\ref{LEM:equivalentTypesHaveEqualPers} $r\Vdash a\!:\! F\sigma$. We then have $r\Vdash (\rho,a)=(\sigma,a)\!:\! (\Gamma,x\!:\! F)$. Thus we have $r\Vdash G\rho[a]=G\sigma[a]$. Thus $q\Vdash  (\Pi(x\!:\! F) G)\rho =  (\Pi(x\!:\! F) G)\sigma$ and by Lemma~\ref{LEM:equivalentTypesHaveEqualPers} $q\Vdash (\lambda x.t)\sigma \!:\! (\Pi(x\!:\! F) G)\rho$. We have $r\Vdash t\rho[a]=t\sigma[a]\!:\! G\rho[a]$. But $r\Vdash (\lambda x. t\rho)\,a = t\rho[a]\!:\! G\rho[a]$ and $r\Vdash (\lambda x. t\sigma) a = t\sigma[a] \!:\! G\sigma[a]$. By Lemma~\ref{LEM:equivalentTypesHaveEqualPers} $r\Vdash (\lambda x. t\sigma) a = t\sigma[a] \!:\! G\rho[a]$. By Symmetry and transitivity $r\Vdash (\lambda x. t\rho)\, a = (\lambda x. t\sigma)\,a \!:\! G\rho[a]$. Thus $q\Vdash (\lambda x. t) \rho = (\lambda x. t) \sigma \!:\! (\Pi(x\!:\! F) G)\rho$.
\end{proof}

\begin{lem}
\label{soundbeta}

\AxiomC{$\Gamma, x\!:\! F \vDash_p t \!:\!  G$}
\AxiomC{$\Gamma \vDash_p a \!:\!  F$}
\BinaryInfC{$\Gamma \vDash_p (\lambda x. t)\,a = t[a] \!:\!  G[a]$}
\DisplayProof
\end{lem}
\begin{proof}
Let $q\leqslant p$ and $q\Vdash \rho \!:\! \Gamma$. We have $q\Vdash a\rho \!:\! F\rho$. As in Lemma~\ref{soundLambdaIntro} $q\vdash ((\lambda x. t)\,a)\rho \rightarrowtriangle t[a]\rho \!:\! G[a]\rho$ which by Lemma~\ref{LEM:terms_onestepreductionimplyequiv} imply that $q\Vdash ((\lambda x. t)\,a)\rho = t[a]\rho \!:\! G\rho[a]$.
\end{proof}

\begin{lem}
\label{soundapptyp}

\AxiomC{$\Gamma\vDash_p g \!:\!  \Pi (x\!:\! F) G$}
\AxiomC{$\Gamma\vDash_p a \!:\!  F$}
\BinaryInfC{$\Gamma \vDash_p g\,a \!:\!  G[a]$}
\DisplayProof
\end{lem}
\begin{proof}
Let $q\leqslant p$ and $q\Vdash \rho \!:\! \Gamma$. We have $q\Vdash g\rho \!:\! (\Pi(x\!:\! F) G)\rho$ and  $q\Vdash a\rho \!:\! F\rho$. By the definition $q\Vdash (g\,a)\rho \!:\! G[a]\rho$.

Let $q\Vdash \rho =\sigma\!:\! \Gamma$. We have then $q\Vdash g\rho = g\sigma \!:\! (\Pi(x\!:\! F) G)\rho$ and $q\Vdash a\rho = a\sigma \!:\! F\rho$. From the definition $q\Vdash g\rho\,a\rho = g\sigma\,a\rho \!:\! G[a]\rho$. From the definition $q\Vdash g\sigma\,a\rho = g\sigma\,a\sigma \!:\! G[a]\rho$. By transitivity $q\Vdash (g\,a)\rho = (g\,a)\sigma \!:\! G[a]\rho$. 
\end{proof}

\begin{lem
\label{soundappeq}
(1) 
\AxiomC{$\Gamma \vDash_p g \!:\!  \Pi (x\!:\! F) G$}
\AxiomC{$\Gamma \vDash_p u =v \!:\!  F$}
\BinaryInfC{$\Gamma \vDash_p g\,u = g\,v \!:\!  G[u]$}
\DisplayProof\;
(2)
\AxiomC{$\Gamma \vDash_p h =g \!:\!  \Pi (x\!:\! F) G$}
\AxiomC{$\Gamma \vDash_p u \!:\!  F$}
\BinaryInfC{$\Gamma \vDash_p h\,u = g\,u \!:\!  G[u]$}
\DisplayProof 
\end{lem}
\begin{proof}
Let $q\leqslant p$ and $q\Vdash \rho \!:\! \Gamma$.  

\begin{enumerate}
\item We have $q\Vdash g\rho \!:\! (\Pi(x\!:\! F) G)\rho$ and  $q\Vdash u\rho = v\rho \!:\! F\rho$. From the definition get $q\Vdash (g\,u)\rho = (g\,v)\rho \!:\! G[u]\rho$.
\item We have  $q\Vdash h\rho = g\rho \!:\! (\Pi(x\!:\! F) G)\rho$ and  $q\Vdash u\rho \!:\! F\rho$. From the definition we get $q\Vdash (h\,u)\rho = (g\,u)\rho \!:\! G[u]\rho$.\qedhere
\end{enumerate}
\end{proof}

\begin{lem
\label{soundfunext}

\AxiomC{$\Gamma \vDash_p h \!:\! \Pi(x\!:\!  F)G$}
\AxiomC{$\Gamma \vDash_p g \!:\! \Pi(x\!:\!  F) G$}
\AxiomC{$\Gamma, x\!:\! F \vDash_p h\,x=g\,x \!:\! G[x]$}
\TrinaryInfC{$\Gamma \vDash_p h = g \!:\!  \Pi(x\!:\!  F)G$}
\DisplayProof \smallskip
\end{lem}
\begin{proof}
Let $q\leqslant p$ and $q\Vdash \rho \!:\! \Gamma$. We have $q\Vdash h\rho\!:\! (\Pi(x\!:\! F) G)\rho$ and $q\Vdash g\rho\!:\! (\Pi(x\!:\! F) G)\rho$. Let $r\leqslant q$ and $r\Vdash a\!:\! F\rho$. We have then that $r\Vdash (\rho,a)\!:\! \Gamma,x\!:\! F$. Thus $r\Vdash h\rho\,a=g\rho\,a \!:\! G\rho[a]$. By the definition $q\Vdash h\rho = g\rho \!:\! (\Pi(x\!:\! F) G)\rho$.
\end{proof}

\begin{lem}
\label{soundpairing}

\AxiomC{$\Gamma, x\!:\! F \vDash_p G$ }
\AxiomC{$\Gamma \vDash_p a \!:\!  F$ }
\AxiomC{$\Gamma \vDash_p b\!:\!  G[a]$}
\TrinaryInfC{$\Gamma \vDash_p (a, b) \!:\!  \Sigma (x\!:\!  F) G $}
\DisplayProof
\end{lem}
\begin{proof}
Let $q\leqslant p$ and $q\Vdash \rho \!:\! \Gamma$. By the typing rules $\Gamma\vdash_q (a,b).1 = a \!:\! F$ and $\Gamma\vdash_q (a,b).2 = b\!:\! F[a]$. But $\vdash_q \rho \!:\! \Gamma$. By substitution we have $\vdash_q ((a,b).1)\rho = a\rho \!:\! F\rho$ and $\vdash_q ((a,b).2)\rho = b\rho \!:\! G[a]\rho$. But $((a,b).1)\rho \rightarrowtriangle_q a\rho$ and $((a,b).2)\rho \rightarrowtriangle_q b\rho$. Thus $q\vdash ((a,b).1)\rho \rightarrowtriangle  a\rho \!:\! F\rho$ and $q\vdash ((a,b).2)\rho \rightarrowtriangle  b\rho\!:\! G[a]\rho$. From the premise $q\Vdash a\rho \!:\! F\rho$ and $q\Vdash b\rho \!:\! G[a]\rho$. By Lemma~\ref{LEM:terms_onestepreductionimplyequiv}  $q\Vdash ((a,b).1)\rho \!:\! F\rho$ and $q\Vdash ((a,b).2)\rho \!:\! G[a]\rho$. By Lemma~\ref{LEM:terms_onestepreductionimplyequiv} $q\Vdash ((a,b).1)\rho = a\rho \!:\! F\rho$, thus $q\Vdash (\rho,a\rho)=(\rho,((a,b).1)\rho)\!:\! (\Gamma,x\!:\! F)$. Hence $q\Vdash G[a]\rho = G[(a,b).1]\rho$. By Lemma~\ref{LEM:equivalentTypesHaveEqualPers} $q\Vdash ((a,b).2)\rho \!:\! G[(a,b).1]\rho$. By the definition we have then that $q\Vdash (a,b)\rho \!:\! (\Sigma(x\!:\! F) G)\rho$.

Let $q\Vdash \rho = \sigma \!:\! \Gamma$. Similarly we can show  $q\Vdash (a,b)\sigma \!:\! (\Sigma(x\!:\! F) G)\sigma$. We have that $q\Vdash a\rho = a\sigma \!:\! F\rho$ and $q\Vdash b\rho = b\sigma \!:\! G[a]\rho$. We have also $q\Vdash (\rho,a\rho)=(\sigma,a\sigma) \!:\! (\Gamma,x\!:\! F)$ we thus have $q\Vdash G[a]\rho = G[a]\sigma$. By Lemma~\ref{LEM:terms_onestepreductionimplyequiv} $q\Vdash ((a,b).2)\sigma = b\sigma \!:\! G[a]\sigma$. By Lemma~\ref{LEM:equivalentTypesHaveEqualPers} $q\Vdash ((a,b).2)\sigma = b\sigma \!:\! G[a]\rho$. But we also have by Lemma~\ref{LEM:terms_onestepreductionimplyequiv} that $q\Vdash ((a,b).2)\sigma = a\sigma \!:\! F\sigma$. Hence, by Lemma~\ref{LEM:equivalentTypesHaveEqualPers}, we have $q\Vdash ((a,b).2)\sigma=a\sigma\!:\! F\rho$. By symmetry and transitivity we then have that $q\Vdash ((a,b).1)\rho = ((a,b).1)\sigma \!:\! F\rho$ and $q\Vdash ((a,b).2)\rho = ((a,b).2)\sigma \!:\! G[(a,b).1]\rho$. Thus we have that $q\Vdash (a,b)\rho = (a,b)\sigma \!:\! (\Sigma(x\!:\! F) G)\rho$.
\end{proof}

\begin{lem
\label{soundproj} \leavevmode\\[2mm]
{\upshape (1)}
\AxiomC{$\Gamma, x\!:\! F\vDash_p G$}
\AxiomC{$\Gamma\vDash_p t\!:\! F$}
\AxiomC{$\Gamma\vDash_p u\!:\! G[t]$}
\TrinaryInfC{$\Gamma \vDash_p (t,u).1=t \!:\!  F$ }
\DisplayProof\;
{\upshape (2)}
\AxiomC{$\Gamma, x\!:\! F\vDash_p G$}
\AxiomC{$\Gamma\vDash_p t\!:\! F$}
\AxiomC{$\Gamma\vDash_p u\!:\! G[t]$}
\TrinaryInfC{$\Gamma \vDash_p (t,u).2=u \!:\!  G[t]$ }
\DisplayProof
\end{lem}
\begin{proof}
Let $q\leqslant p$ and $q\Vdash \rho \!:\! \Gamma$.

\begin{enumerate}
\item We have $\vdash_q t\rho \!:\! F\rho$ and $\vdash_q u\rho \!:\! G[t]\rho$. By substitution we get $\vdash_q ((t,u).1)\rho = t\rho \!:\! F\rho$. But $((t,u).1)\rho \rightarrowtriangle_q t\rho$, thus $q\vdash ((t,u).1)\rho \rightarrowtriangle_q t\rho \!:\! F\rho$. We have that $q\Vdash t\rho \!:\! F\rho$. Thus by Lemma~\ref{LEM:terms_onestepreductionimplyequiv} $q\Vdash ((t,u).1)\rho \!:\! F\rho$ and $q\Vdash ((t,u).1)\rho = t\rho \!:\! F\rho$. 


\item Similarly we have $q\Vdash (t,u)\rho .2 \rightarrowtriangle u\rho \!:\! G[t\rho]$. Since $q\Vdash u\rho \!:\! G[t]\rho$, by Lemma~\ref{LEM:terms_onestepreductionimplyequiv}, we have that $q\Vdash ((t,u).2)\rho \!:\! G[t]\rho$ and $q\Vdash ((t,u).2)\rho = u\rho \!:\! G[t\rho]$. \qedhere
\end{enumerate}
\end{proof}

\begin{lem}\leavevmode\medskip
\label{soundprojtypeq}
\\[2mm]
{\upshape (1) }
\AxiomC{$\Gamma\vDash_p t\!:\!  \Sigma (x\!:\! F) G$ }
\UnaryInfC{$\Gamma \vDash_p t.1 \!:\!  F$ }
\DisplayProof
\,
\AxiomC{$\Gamma\vDash_p t\!:\!  \Sigma (x\!:\! F) G$ }
\UnaryInfC{$\Gamma \vDash_p t.2 \!:\!  G[t.1]$ }
\DisplayProof
\,
{\upshape (2)}
\hspace{-2mm}
\AxiomC{$\Gamma \vDash_p t =u \!:\!  \Sigma (x\!:\! F) G$}
\UnaryInfC{$\Gamma \vDash_p t.1=u.1\!:\! F$}
\DisplayProof
\,
\AxiomC{$\Gamma \vDash_p t =u \!:\!  \Sigma (x\!:\! F) G$}
\UnaryInfC{$\Gamma \vDash_p t.2=u.2\!:\! G[t.1]$}
\DisplayProof 
\end{lem}
\begin{proof}

Let $q\leqslant p$ and $q\Vdash \rho \!:\! \Gamma$.
\begin{enumerate}
\item We have $q\Vdash t\rho \!:\! (\Sigma(x\!:\! F) G)\rho$. By the definition we have $q\Vdash (t.1)\rho \!:\! F\rho$ and $q\Vdash (t.2)\rho \!:\! G[t.1]\rho$. Let $q\Vdash \rho = \sigma \!:\! \Gamma$. We have that $q\Vdash t\rho = t\sigma \!:\! (\Sigma(x\!:\! F) G)\rho$. By the definition $q\Vdash (t.1)\rho = (t.1)\sigma \!:\! F\rho$ and $q\Vdash (t.2)\rho = (t.2)\sigma \!:\! G[t.1]\rho$. 

\item We have $q\Vdash t\rho = u\rho \!:\! (\Sigma(x\!:\! F) G))\rho$. By the definition $q\Vdash (t.1)\rho=(u.1)\rho\!:\! F\rho$ and $q\Vdash (t.2)\rho = (u.2)\rho \!:\! G[t.1]\rho$.\qedhere
\end{enumerate}
\end{proof}

\begin{lem
  \ \\[-4mm]
\label{soundpairext}
\begin{prooftree}
\AxiomC{$\Gamma\vDash_p t\!:\!  \Sigma(x\!:\!  F) G$}
\AxiomC{$\Gamma\vDash_p u\!:\!  \Sigma(x\!:\!  F) G$}
\AxiomC{$\Gamma\vDash_p t.1=u.1\!:\!  F$ }
\AxiomC{$\Gamma\vDash_p t.2=u.2\!:\!  G[t.1]$ }
\QuaternaryInfC{$\Gamma \vDash_p t=u \!:\!  \Sigma(x\!:\! F)G$ }
\end{prooftree}
\end{lem}
\begin{proof}
Let $q\leqslant p$ and $q\Vdash \rho \!:\! \Gamma$. We have $q\Vdash t\rho \!:\! (\Sigma(x\!:\! F) G)\rho$ and $q\Vdash u\rho \!:\! (\Sigma(x\!:\! F) G)\rho$. We also have $q\Vdash (t.1)\rho = (u.1) \rho \!:\! F\rho$ and $q\Vdash (t.2) \rho = (u.2) \rho \!:\! G[t.1]\rho$. By the definition $q\Vdash t\rho = u\rho \!:\! (\Sigma(x\!:\! F)G)\rho$.
\end{proof}

\begin{lem
\label{soundnat}

{\upshape (1)} \AxiomC{$\Gamma\vdash_p$}
\UnaryInfC{$\Gamma\vDash_p \mathsf{N}$}
\DisplayProof
\,
{\upshape (2)} \AxiomC{$\Gamma\vdash_p$}
\UnaryInfC{$\Gamma \vDash_p 0 \!:\!  \mathsf{N}$}
\DisplayProof
\,
{\upshape (3)} \AxiomC{$\Gamma \vDash_p n \!:\!  \mathsf{N}$}
\UnaryInfC{$\Gamma \vDash_p \mathsf{S}\, n \!:\!  \mathsf{N}$}
\DisplayProof 
\,
{\upshape (4)} \AxiomC{$\Gamma \vDash_p n=m \!:\! \mathsf{N}$}
\UnaryInfC{$\Gamma \vDash_p \mathsf{S}\,n = \mathsf{S}\, m \!:\! \mathsf{N}$}
\DisplayProof
\end{lem}
\begin{proof}
(1) and (2) follow directly from the definition while (3) and (4) follow from Lemma~\ref{LEM:BaseTypeCanonicity} and locality.
\end{proof}

\begin{lem
\label{soundnessnatrec}

\AxiomC{$\Gamma, x\!:\! \mathsf{N} \vDash_p F$}
\AxiomC{$\Gamma \vDash_p a_0 \!:\!  F[\mathsf{0}]$}
\AxiomC{$\Gamma \vDash_p g\!:\!  \Pi (x\!:\! \mathsf{N}) (F[x]\rightarrow F[\mathsf{S}\,x])$}
\TrinaryInfC{$\Gamma \vDash_p {\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g\!:\!  \Pi (x\!:\! \mathsf{N}) F$}
\DisplayProof
\end{lem}
\begin{proof}
Let $q\leqslant p$ and $q\Vdash \rho \!:\! \Gamma$. We have then that $q\vdash \rho \!:\! \Gamma$, hence, $\vdash_q ({\mathsf{rec}_\mathsf{N}} (\lambda x. F)\rho\,a_0\,g)\rho \!:\! (\Pi(x\!:\! \mathsf{N}) F)\rho$. Let $r\leqslant q$. Let $r\Vdash a \!:\! \mathsf{N}$, $r\Vdash b\!:\! \mathsf{N}$ and $r\Vdash a=b \!:\! \mathsf{N}$. By Lemma~\ref{LEM:BaseTypeCanonicity} there is a partition $r\vartriangleleft S$ such that for each $s\in S$, $s\vdash a\red^\ast \xoverline{n}\!:\! \mathsf{N}$ and $s\vdash b\red^\ast \xoverline{n}\!:\! \mathsf{N}$. In order to show that $q\Vdash ({\mathsf{rec}_\mathsf{N}} (\lambda x. F)\,a_0\,g)\rho \!:\! (\Pi(x\!:\! \mathsf{N}) F)\rho$ we need to show that $r\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,a \!:\! F\rho[a]$, $r\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,b \!:\! F\rho[b]$, and $r\Vdash {\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,a =({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,b \!:\! F\rho[a]$. By locality it will be sufficient to show that for each $s\in S$ we have $s\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,a \!:\! F\rho[a]$, $s\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,b \!:\! F\rho[b]$, and $s\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,a= ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,b\rho\!:\! F\rho[a]$.  We have that 
\begin{align*}
& s\vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,a  \red^\ast ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,\xoverline{n} \!:\! F\rho[a]\\
& s\vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,b  \red^\ast ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,\xoverline{n} \!:\! F\rho[b]
\end{align*}
Let $\xoverline{n} \coloneqq \mathsf{S}^{k}\,0$. By induction on $k$. If $k=0$ then 
\begin{align*}
& s\vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,a  \red^\ast ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,\mathsf{0}\rightarrowtriangle a_0\rho \!:\! F\rho[a]\\
& s\vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,b  \red^\ast ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,\mathsf{0}\rightarrowtriangle a_0\rho \!:\! F\rho[b]
\end{align*}
By Lemma~\ref{LEM:equivalentTypesHaveEqualPers} we have then that 
\begin{align*}
s\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,a  = a_0\rho \!:\! F\rho[a] &\hphantom{space}
s\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,b  = a_0\rho \!:\! F\rho[b]
\end{align*}

Since $s\Vdash a=b\!:\! \mathsf{N}$ we have $s\Vdash (\rho,a)=(\rho,b)\!:\! (\Gamma,x\!:\! \mathsf{N})$ and thus $s\Vdash F\rho[a]=F\rho[b]$. By Lemma~\ref{LEM:equivalentTypesHaveEqualPers}, symmetry and transitivity 
$s\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,a= ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,b\!:\! F\rho[a]$.

Assume the statement holds for $k\leq \ell$. Let $\xoverline{n} = \mathsf{S}\,\xoverline{\ell}$. We have then
\begin{align*}
& s\vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,a  \red^\ast  g\rho \,\xoverline{\ell}\, (({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,\xoverline{\ell}) \!:\! F\rho[\mathsf{S}\,\xoverline{\ell}]\\
& s\vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,b  \red^\ast  g\rho \,\xoverline{\ell}\, (({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,\xoverline{\ell}) \!:\! F\rho[\mathsf{S}\,\xoverline{\ell}]
\end{align*}
By IH $s\Vdash (({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,\xoverline{\ell}) \!:\! F\rho[\xoverline{\ell}]$. But we have $\Gamma \vDash_p g\!:\!  \Pi (x\!:\! \mathsf{N}) (F[x]\rightarrow F[\mathsf{S}\,x])$ and thus
$s\Vdash  (g\rho)\,\xoverline{\ell}\,(({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,\xoverline{\ell})\!:\! F\rho[\mathsf{S}\,\xoverline{\ell}]$. By Corollary~\ref{COR:terms_reductionimplyequiv}, symmetry and transitivity we get that $s\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,a \!:\! F\rho[\mathsf{S}\,\xoverline{\ell}]$, 
$s\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,b \!:\! F\rho[\mathsf{S}\,\xoverline{\ell}]$, and
$s\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,a = ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,b \!:\! F\rho[\mathsf{S}\,\xoverline{\ell}]$. But $s\Vdash a = \mathsf{S}\,\xoverline{\ell} \!:\! \mathsf{N}$, thus, $s\Vdash F\rho[a]=F\rho[\mathsf{S}\,\xoverline{\ell}]$. By Lemma~\ref{LEM:equivalentTypesHaveEqualPers} we get then that
$s\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,a = ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,b \!:\! F\rho[a]$.

As indicated above, this is sufficient to show $q\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho \!:\!  \Pi (x\!:\! \mathsf{N}) F\rho$. 

Given $q\Vdash \rho=\sigma\!:\! \Gamma$. Similarly we can show $q\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\sigma \!:\!  \Pi (x\!:\! \mathsf{N}) F\sigma$. 

To show that $q\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho=({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\sigma \!:\!  \Pi (x\!:\! \mathsf{N}) F\rho$ we need to show that whenever $r\Vdash a\!:\! F\rho$ for some $r\leqslant q$ we have $r\Vdash  ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,a= ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\sigma\,a\!:\! F\rho[a]$. Let $r\Vdash a\!:\! F$ for $r\leqslant q$. By Lemma~\ref{LEM:BaseTypeCanonicity} we have a partition $r\vartriangleleft S$ where for each $s\in S$ we have $s\vdash a\red^\ast \xoverline{n}\!:\! \mathsf{N}$. As  above it is  sufficient to show $s\Vdash  ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,a= ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\sigma\,a\!:\! F\rho[a]$ for all $s\in S$.

Let $\xoverline{n} \coloneqq \mathsf{S}^{k}\,\mathsf{0}$. By induction on $k$. If $k=0$ then as above
\begin{align*}
s\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,a  = a_0\rho \!:\! F\rho[a] &\hphantom{space}
s\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\sigma\,a  = a_0\sigma \!:\! F\sigma[b]
\end{align*}

Since $r\Vdash \rho =\sigma\!:\! \Gamma$ we have $s\Vdash (\rho,a)=(\sigma,a)\!:\! (\Gamma,x\!:\! \mathsf{N})$. We have then that $s\Vdash F\rho[a]=F\sigma[a]$. But we also have that $s\Vdash a_0\rho =a_0\sigma\!:\! F\rho[a]$. By Lemma~\ref{LEM:equivalentTypesHaveEqualPers}, symmetry and transitivity it then follows that $s\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,a=({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\sigma\,a\!:\! F\rho[a]$.

Assume the statement holds for $k\leq \ell$. Let $\xoverline{n} = \mathsf{S}\,\xoverline{\ell}$. As before we have that
\begin{align*}
& s\vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,a  \red^\ast  g\rho \,\xoverline{\ell}\, (({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,\xoverline{\ell}) \!:\! F\rho[\mathsf{S}\,\xoverline{\ell}]\\
& s\vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\sigma\,a  \red^\ast  g\sigma \,\xoverline{\ell}\, (({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\sigma\,\xoverline{\ell}) \!:\! F\sigma[\mathsf{S}\,\xoverline{\ell}]
\end{align*}
By IH 
$s\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,\xoverline{\ell} =({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\sigma\,\xoverline{\ell} \!:\! F\rho[\xoverline{\ell}]$.
But $s\Vdash g\rho = g\sigma \!:\! (\Pi (x\!:\! \mathsf{N}) (F[x]\rightarrow F[\mathsf{S}\,x]))\rho$, thus
 $s \Vdash g\rho\,\xoverline{\ell}\,(({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,\xoverline{\ell}) = g\sigma\,\xoverline{\ell}\,(({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\sigma\,\xoverline{\ell}) \!:\! F\rho[\mathsf{S}\,\xoverline{\ell}]$

But $s\Vdash F\rho[\mathsf{S}\,\xoverline{\ell}]=F\sigma[\mathsf{S}\,\xoverline{\ell}]$ and $r_i\Vdash F\rho[a]=F\rho[\mathsf{S}\,\xoverline{\ell}]$. By Lemma~\ref{LEM:equivalentTypesHaveEqualPers}, symmetry and transitivity we have then that 
$s\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho\,a  = ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\sigma\,a \!:\! F\rho[a]$

Which is sufficient to show 
$q\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\rho= ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\, g)\sigma \!:\! \Pi(x\!:\! \mathsf{N}) F\rho$
\end{proof}

\begin{lem}
\label{soundnatrec0}

\AxiomC{$\Gamma, x\!:\! \mathsf{N} \vdash F$}
\AxiomC{$\Gamma \vDash_p a_0 \!:\!  F[\mathsf{0}]$}
\AxiomC{$\Gamma \vDash_p g \!:\!  \Pi (x\!:\! \mathsf{N}) (F[x] \rightarrow F[\mathsf{S}\,x])$}
\TrinaryInfC{$\Gamma \vDash_p {\mathsf{rec}_\mathsf{N}} (\lambda x. F)\,a_0\, g \,\mathsf{0} = a_0 \!:\!  F[\mathsf{0}]$}
\DisplayProof
\end{lem}
\begin{proof}
Let $q\leqslant p$ and $q\Vdash \rho \!:\! \Gamma$. We have $\vdash_q \rho \!:\! \Gamma$ and thus we get that $\vdash_q ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\,g\,\mathsf{0})\rho = a_0\rho \!:\! F\rho[\mathsf{0}]$. But $({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\,g\,\mathsf{0})\rho \rightarrowtriangle a_0\rho$. Thus $q\vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\,g\,\mathsf{0})\rho \rightarrowtriangle a_0\rho\!:\! F\rho[\mathsf{0}]$. But $q\Vdash a_0\rho \!:\! F\rho[\mathsf{0}]$. By Lemma~\ref{LEM:terms_onestepreductionimplyequiv} we have $q\Vdash ({\mathsf{rec}_\mathsf{N}}(\lambda x. F)\,a_0\,g\,\mathsf{0})\rho =a_0\rho\!:\! F\rho[\mathsf{0}]$.\smallskip
\end{proof}

\begin{lem}
\label{soundnatrecsuc}
\AxiomC{$\Gamma, x\!:\! \mathsf{N} \vDash_p F$}
\AxiomC{$\Gamma \vDash_p a_0 \!:\!  F[\mathsf{0}]$}
\AxiomC{$\Gamma \vDash_p n \!:\!  \mathsf{N}$}
\AxiomC{$\Gamma \vDash_p g \!:\!  \Pi (x\!:\! \mathsf{N}) (F[x] \rightarrow F[\mathsf{S} \,x])$}
\QuaternaryInfC{$\Gamma \vDash_p {\mathsf{rec}_\mathsf{N}} (\lambda x. F)\,a_0\, g \,(\mathsf{S}\, n) = g\,n \,({\mathsf{rec}_\mathsf{N}} (\lambda x. F)\,a_0\,g\,n) \!:\!  F[\mathsf{S}\,n]$}
\DisplayProof

\end{lem}
\begin{proof}
Let $q\leqslant p$ and $q\Vdash \rho \!:\! \Gamma$. We have $q\Vdash n\rho \!:\! \mathsf{N}$. By Lemma~\ref{LEM:BaseTypeCanonicity} there is a partition $q\vartriangleleft S$ such that for each $s\in S$ there is $m\in \mathbb{N}$ and $s\vdash n\rho \red^\ast \xoverline{m}\!:\! \mathsf{N}$. Thus  $s\vdash \mathsf{S}\,n\rho \red^\ast \mathsf{S}\,\xoverline{m}\!:\! \mathsf{N}$. We have then that 
\begin{align*}
s\vdash &({\mathsf{rec}_\mathsf{N}} (\lambda x. F)\,a_0\, g \,(\mathsf{S}\, n))\rho  \red^\ast  ({\mathsf{rec}_\mathsf{N}} (\lambda x. F)\,a_0\, g)\rho\,(\mathsf{S}\, \xoverline{m})\\
&\red^\ast g\rho\,\xoverline{m}\,(({\mathsf{rec}_\mathsf{N}}\,(\lambda x. F)\,a_0\,g)\rho\,\xoverline{m})\!:\! F\rho[\mathsf{S}\,\xoverline{m}]
\end{align*}

But $s \vdash (g\,n \,({\mathsf{rec}_\mathsf{N}} (\lambda x. F)\,a_0\,g\,n))\rho \red^\ast g\rho\,\xoverline{m}\,(({\mathsf{rec}_\mathsf{N}}\,(\lambda x. F)\,a_0\,g)\rho\,\xoverline{m})\!:\! F\rho[\mathsf{S}\,\xoverline{m}]$. By Corollary~\ref{COR:terms_reductionimplyequiv}, symmetry and transitivity 
$s \Vdash ({\mathsf{rec}_\mathsf{N}} (\lambda x. F)\,a_0\, g \,(\mathsf{S}\, n))\rho =(g\,n \,({\mathsf{rec}_\mathsf{N}} (\lambda x. F)\,a_0\,g\,n))\rho \!:\! F\rho[\mathsf{S}\,\xoverline{m}]$.

Since $s\Vdash n\rho =\xoverline{m} \!:\! \mathsf{N}$ we have that $s\Vdash F\rho[\mathsf{S}\,\xoverline{m}] = F\rho[\mathsf{S}\, n\rho]$.
By Lemma~\ref{LEM:equivalentTypesHaveEqualPers} we thus have that
$ s \Vdash ({\mathsf{rec}_\mathsf{N}} (\lambda x. F)\,a_0\, g \,(\mathsf{S}\, n))\rho =(g\,n \,({\mathsf{rec}_\mathsf{N}} (\lambda x. F)\,a_0\,g\,n))\rho \!:\! F[\mathsf{S}\,n]\rho$.

By locality  
$q \Vdash ({\mathsf{rec}_\mathsf{N}} (\lambda x. F)\,a_0\, g \,(\mathsf{S}\, n))\rho =(g\,n \,({\mathsf{rec}_\mathsf{N}} (\lambda x. F)\,a_0\,g\,n))\rho \!:\! F[\mathsf{S}\,n]\rho$   
\end{proof}

\begin{lem}
\label{soundnatreccong}
\AxiomC{$\Gamma, x\!:\! \mathsf{N}\vDash_p F = G$}
\AxiomC{$\Gamma \vDash_p a_0=b_0 \!:\!  F[\mathsf{0}]$}
\AxiomC{$\Gamma \vDash_p g=h \!:\!  \Pi (x\!:\! \mathsf{N}) (F[x] \rightarrow F[\mathsf{S} \,x])$}
\TrinaryInfC{$\Gamma \vDash_p {\mathsf{rec}_\mathsf{N}} (\lambda x. F)\,a_0\, g = {\mathsf{rec}_\mathsf{N}} (\lambda x. G)\,b_0\, h\!:\!  \Pi(x\!:\! \mathsf{N}) F$}
\DisplayProof\medskip
\end{lem}
\begin{proof}
The proof follows by an argument similar to that used to prove Lemma~\ref{soundnessnatrec}.
\end{proof}


For the congruence rules, soundness follows from Theorem ~\ref{properties}. Soundness for rules of ${\mathsf{N}_0}$, ${\mathsf{N}_1}$ and ${\mathsf{N}_2}$ follow similarly to those of $\mathsf{N}$. Soundness for the rules of $\mathsf{U}$ follows similarly to soundness of typing rules. We have then the following corollary:
\begin{cor}[Soundness]
\label{LEM:soundness}
If $\Gamma \vdash_p J$ then $\Gamma\vDash_p J$
\end{cor}

\begin{thm}[Fundamental Theorem]
\label{THM:fundamentalThm}
If $\vdash_p J$ then $p\Vdash J$.
\end{thm}
\begin{proof}
Follows from Corollary~\ref{LEM:soundness}.
\end{proof}
\section{Markov's principle}
\label{SEC:markov}
Now we have enough machinery to show the independence of $\mathrm{MP}$ from type theory. The idea is that if a judgment $J$ is derivable in type theory (i.e.\ $\vdash J$) then it is derivable in the forcing extension (i.e.\ $\vdash_{\emptyset} J$) and by Theorem~\ref{THM:fundamentalThm} it holds in the interpretation (i.e.\ $\Vdash J$). It thus suffices to show that there no $t$ such that $\Vdash t\!:\! \mathsf{MP}$ to establish the independence of $\mathrm{MP}$ from type theory. First we recall the formulation of $\mathrm{MP}$.
\begin{align*}
\mathsf{MP} \coloneqq\Pi (h\!:\! \mathsf{N}\rightarrow {\mathsf{N}_2})[\neg\neg (\Sigma (x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(h\,x)) \rightarrow \Sigma (x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(h\,x)]
\end{align*}
where $\mathsf{IsZero} \!:\! {\mathsf{N}_2} \rightarrow \mathsf{U}$ is given by $\mathsf{IsZero} \coloneqq \lambda y.{\mathsf{rec}_{\mathsf{N}_2}} (\lambda x. \mathsf{U})\, {\mathsf{N}_1}\,{\mathsf{N}_0}\,y$.
 

\begin{lem}
\label{LEM:markovConclusionNoWitness}
There is no term $t$ such that $\Vdash t\!:\! \Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(\mathsf{f}\,x)$.
\end{lem}
\begin{proof}
Assume $\Vdash t\!:\! \Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(\mathsf{f}\,x)$ for some $t$. We then have $\Vdash t.1 \!:\! \mathsf{N}$ and $\Vdash t.2\!:\! \mathsf{IsZero}\,(\mathsf{f}\,t.1)$. By Lemma~\ref{LEM:BaseTypeCanonicity} one has a partition $\emptyset \vartriangleleft S$ where for each $q\in S$, $q\vdash t.1 \red^\ast \xoverline{m}\!:\! \mathsf{N}$. Hence $q\vdash \mathsf{IsZero}\,(\mathsf{f}\,t.1) \red^\ast \mathsf{IsZero}\,(\mathsf{f}\,\xoverline{m})$ and by Lemma~\ref{LEM:types_reductionimplyequiv} $q \Vdash \mathsf{IsZero}\,(\mathsf{f}\,t.1)= \mathsf{IsZero}\,(\mathsf{f}\,\xoverline{m})$. But, by definition, the partition $S$ must contain a condition, say $r$, such that $r(k) = 1$ whenever $k \in \dom{r}$ (this holds vacuously for $\emptyset\vartriangleleft \{\emptyset\}$). Let $r\vdash t.1 \red^\ast \xoverline{n}\!:\! \mathsf{N}$. Assume $n \in \dom{r}$, then $r\vdash \mathsf{IsZero}\,(\mathsf{f}\,t.1) \red^\ast \mathsf{IsZero}\,(\mathsf{f}\,\xoverline{n}) \red^\ast {\mathsf{N}_0}$. By monotonicity, from $\Vdash t.2 \!:\! \mathsf{IsZero}\,(\mathsf{f}\,t.1)$ we get $r\Vdash t.2 \!:\! \mathsf{IsZero}\,(\mathsf{f}\,t.1)$. But $r \vdash \mathsf{IsZero}\,(\mathsf{f}\,t.1) \red^\ast {\mathsf{N}_0}$ thus $r \Vdash  \mathsf{IsZero}\,(\mathsf{f}\,t.1) = {\mathsf{N}_0}$. Hence, by Lemma~\ref{LEM:equivalentTypesHaveEqualPers}, $r\Vdash t.2 \!:\! {\mathsf{N}_0}$ which is impossible, thus contradicting our assumption. If on the other hand $n \notin \dom{r}$ then, since $r\vartriangleleft\{ r(n\mapsto \mathsf{0}),r(n\mapsto \mathsf{1})\}$, we can apply the above argument with $r(n\mapsto \mathsf{1})$ instead of $r$.
\end{proof}

\begin{lem}
\label{LEM:markovNotForcible}
There is no term $t$ such that $\Vdash t\!:\! \mathsf{MP}$.
\end{lem}
\begin{proof}
Assume $\Vdash t\!:\! \mathsf{MP}$ for some $t$. From the definition, whenever $\Vdash g \!:\! \mathsf{N}\rightarrow {\mathsf{N}_2}$ we have $\Vdash t\,g \!:\! \neg \neg (\Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(g\,x))\rightarrow \Sigma (x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(g\,x)$. Since by Corollary~\ref{COR:genericwelltyped}, $\Vdash \mathsf{f} \!:\! \mathsf{N}\rightarrow {\mathsf{N}_2}$ we have $\Vdash t\,\mathsf{f} \!:\! \neg \neg (\Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(\mathsf{f}\,x))\rightarrow \Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(\mathsf{f}\,x)$. Since by Lemma~\ref{LEM:markovpremisewitnesswelltyped} $\Vdash \mathsf{w}\!:\! \neg\neg( \Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(\mathsf{f}\,x))$ we have $\Vdash (t\,\mathsf{f})\,\mathsf{w} \!:\! \Sigma (x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(\mathsf{f}\,x)$ which is impossible by Lemma~\ref{LEM:markovConclusionNoWitness}.
\end{proof}

From Theorem~\ref{THM:fundamentalThm}, Lemma~\ref{LEM:markovNotForcible}, and Lemma~\ref{LEM:extension} we can then conclude:
\mainresult*


\subsection{Many Cohen reals}

We extend the type system in Section~\ref{SEC:Forcingextensionoftypetheory} further by adding a generic point $\mathsf{f}_q$ for each condition $q$. The introduction and conversion rules for $\mathsf{f}_q$ are given by:\smallskip

\begin{center}
\AxiomC{$\Gamma\vdash_p$}
\UnaryInfC{$\Gamma\vdash_p \mathsf{f}_q \!:\! \mathsf{N}\rightarrow {\mathsf{N}_2}$}
\DisplayProof
\,
\AxiomC{$\Gamma\vdash_p$}
\RightLabel{$n\in\dom{q}$}
\UnaryInfC{$\Gamma\vdash_p \mathsf{f}_q\,\xoverline{n} = 1$}
\DisplayProof\,
\AxiomC{$\Gamma\vdash_p$}
\RightLabel{$n\notin\dom{q}, n\in \dom{p}$}
\UnaryInfC{$\Gamma\vdash_p \mathsf{f}_q\,\xoverline{n} = p(n)$}
\DisplayProof\smallskip
\end{center}

\noindent
With the reduction rules
\begin{center}
\AxiomC{$n\in \dom{q}$}
\UnaryInfC{$\mathsf{f}_q\,\xoverline{n} \rightarrow 1$}
\DisplayProof
\,
\AxiomC{$n\notin \dom{q}, n\in \dom{p}$}
\UnaryInfC{$\mathsf{f}_q\,\xoverline{n} \rightarrow_p p(n)$}
\DisplayProof\medskip
\end{center}
We observe that with these added rules the reduction relation is still monotone.
For each $\mathsf{f}_q$ we add a term:
\begin{center}
\AxiomC{$\Gamma \vdash_p$}
\UnaryInfC{$\Gamma \vdash_p \mathsf{w}_q\!:\!  \neg \neg (\Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(\mathsf{f}_q\,x)) $}
\DisplayProof\smallskip
\end{center}
Finally we add a term $\mathsf{mw}$ witnessing the negation of $\mathrm{MP}$\smallskip
\begin{center}
\AxiomC{$\Gamma \vdash_p$}
\UnaryInfC{$\Gamma \vdash_p \mathsf{mw}\!:\! \neg \mathsf{MP}$}
\DisplayProof 
\smallskip
\end{center}
By analogy to Corollary~\ref{COR:genericwelltyped} we have 
\begin{lem}
\label{LEM:qGenericPointForced}
$\Vdash \mathsf{f}_q \!:\! \mathsf{N}\rightarrow {\mathsf{N}_2}$ for all $q$.
\end{lem}

\begin{lem}
\label{LEM:qMarkovPermiseWitnessForced}
$\Vdash \mathsf{w}_q \!:\!  \neg \neg (\Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(\mathsf{f}_q\,x))$ for all $q$.
\end{lem}
\begin{proof}
Assume $p\Vdash t\!:\! \neg (\Sigma(x\!:\! \mathsf{N}) \mathsf{IsZero}\,(\mathsf{f}_q\,x))$ for some $p$ and $t$. Let $m \notin \dom{q} \cup \dom{p}$, we have $p(m\mapsto \mathsf{0})\Vdash \mathsf{f}_q\,\xoverline{m}=\mathsf{0}$. Thus $p(m \mapsto \mathsf{0})\Vdash (\xoverline{m},\mathsf{0}) \!:\!  \Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(\mathsf{f}_q\,x)$ and $p(m\mapsto \mathsf{0}) \Vdash t\,(\xoverline{m},\mathsf{0}) \!:\! {\mathsf{N}_0}$ which is impossible.
\end{proof}

\begin{lem}
\label{LEM:qMarkovConclusionNoWitness}
There is no term $t$ for which $q\Vdash t\!:\! \Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(\mathsf{f}_q\,x)$.
\end{lem}
\begin{proof}
Assume $q\Vdash t\!:\! \Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(\mathsf{f}_q\,x)$ for some $t$. We then have $q\Vdash t.1 \!:\! \mathsf{N}$ and $q\Vdash t.2\!:\! \mathsf{IsZero}\,(\mathsf{f}_q\,t.1)$. By Lemma~\ref{LEM:BaseTypeCanonicity} one has a partition $q \vartriangleleft \{q_1,\dots,q_n\}$ where for each $i$, $t.1 \red^\ast_{q_i} \xoverline{m}_i$ for some $\xoverline{m}_i \in \mathbb{N}$. Hence $q_i\vdash \mathsf{IsZero}\,(\mathsf{f}_q\,t.1) \red^\ast \mathsf{IsZero}\,(\mathsf{f}_q\,\xoverline{m}_i)$ . But any partition of $q$ contain a condition, say $q_j$, where $q_j(k) = 1$ whenever $k \notin \dom{q}$ and $k\in \dom{q_j}$. Assume $m_j \in \dom{q_j}$. If $m_j \in\dom{q}$ then $q_j\vdash \mathsf{f}_q\,m_j \rightarrowtriangle \mathsf{1}\!:\! {\mathsf{N}_2}$ and if $m_j\notin\dom{q}$ then $q_j\vdash \mathsf{f}_q\,\xoverline{m}_j\rightarrowtriangle q_j(k)\coloneqq \mathsf{1}\!:\! {\mathsf{N}_2}$. Thus $q_j\vdash \mathsf{IsZero}\,(\mathsf{f}_q\,t.1) \red^\ast {\mathsf{N}_0}$ and by Lemma~\ref{LEM:types_reductionimplyequiv} $q_j \Vdash \mathsf{IsZero}\,(\mathsf{f}\,t.1) ={\mathsf{N}_0}$. From $\Vdash t.2 \!:\! \mathsf{IsZero}\,(\mathsf{f}\,t.1)$ by monotonicity and Lemma~\ref{LEM:equivalentTypesHaveEqualPers} we have $q_j\Vdash t.2 \!:\! {\mathsf{N}_0}$ which is impossible. If on the other hand $m_j \notin \dom{q_j}$ then since $q_j\vartriangleleft \{q_j(m_j\mapsto \mathsf{0}),q_j(m_j\mapsto \mathsf{1})\}$ we can apply the above argument with $q_j(m_j\mapsto \mathsf{1})$ instead of $q_j$.
\end{proof}
\begin{lem}
$\Vdash \mathsf{mw}\!:\! \neg \mathsf{MP}$
\end{lem}
\begin{proof}
Assume $p \Vdash t\!:\! \mathsf{MP}$ for some $p$ and $t$. Thus whenever $q\leqslant p$ and $q\Vdash u \!:\! \mathsf{N}\rightarrow {\mathsf{N}_2}$ then $q\Vdash t\,u \!:\! \neg \neg (\Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(u\,x))\rightarrow (\Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(u\,x))$. But we have $q\Vdash \mathsf{f}_q \!:\! \mathsf{N}\rightarrow {\mathsf{N}_2}$ by Lemma~\ref{LEM:qGenericPointForced}. Hence $q\Vdash t\,\mathsf{f}_q \!:\! \neg \neg (\Sigma(x\!:\! \mathsf{N}) \mathsf{IsZero}\,(\mathsf{f}_q\,x))\rightarrow (\Sigma(x\!:\! \mathsf{N}) \mathsf{IsZero}\,(\mathsf{f}_q\,x))$. But $q\Vdash \mathsf{w}_q \!:\! \neg \neg (\Sigma(x\!:\! \mathsf{N}) \mathsf{IsZero}\,(\mathsf{f}_q\,x))$ by Lemma~\ref{LEM:qMarkovPermiseWitnessForced}. Thus $q\Vdash (t\,\mathsf{f}_q)\,\mathsf{w}_q \!:\! \Sigma(x\!:\! \mathsf{N})\,\mathsf{IsZero}\,(\mathsf{f}_q\,x)$ which is impossible by Lemma~\ref{LEM:qMarkovConclusionNoWitness}.
\end{proof}

We have then that this extension is sound with respect to the interpretation. Hence we have shown the following statement.

\begin{thm}
There is a consistent extension of $\mathrm{MLTT}$ where $\neg \mathsf{MP}$ is derivable.
\end{thm}

Recall that $\mathsf{dne}\coloneqq \Pi(A\!:\! \mathsf{U})(\neg\neg A\rightarrow A)$. We have then a term $\vdash t\!:\! \mathsf{dne} \rightarrow \mathsf{MP}$. Thus in this extension we have a term $\vdash_\emptyset \lambda x. \mathsf{mw}\,(t\, x)\!:\! \neg \mathsf{dne}$.

\section*{Acknowledgement}
We would like to thank Simon Huber, Thomas Streicher, Mart\'{\i}n Escard\'{o} and Chuangjie Xu.
\bibliographystyle{alpha}
