%!TEX encoding = UTF-8 Unicode
\documentclass[12pt]{article}
%\usepackage{graphicx}
\usepackage{amscd, amssymb}
\usepackage{enumerate}
\usepackage[utf8]{inputenc}
\usepackage{fontspec}
%\usepackage[T1]{fontenc} 
\usepackage{hyperref}

%
\textwidth = 6.5 in
\textheight = 9 in
\oddsidemargin = 0.0 in
\evensidemargin = 0.0 in
\topmargin = 0.0 in
\headheight = 0.0 in
\headsep = 0.0 in
\parindent = 0.0in

%\renewcommand{\thesubsection}{\arabic{subsection}}
%
%
\newenvironment{eq}{\begin{equation}}{\end{equation}}
%
\newenvironment{proof}{{\bf Proof}:}{\vskip 5mm }
\newenvironment{rem}{{\bf Remark}:}{\vskip 5mm }
\newenvironment{remarks}{{\bf Remarks}:\begin{enumerate}}{\end{enumerate}}
\newenvironment{examples}{{\bf Examples}:\begin{enumerate}}{\end{enumerate}}  
%
\newtheorem{proposition}{Proposition}[subsection]
\newtheorem{lemma}[proposition]{Lemma}
\newtheorem{definition}[proposition]{Definition}
\newtheorem{theorem}[proposition]{Theorem}
\newtheorem{cor}[proposition]{Corollary}
\newtheorem{conjecture}{Conjecture}
\newtheorem{pretheorem}[proposition]{Pretheorem}
\newtheorem{hypothesis}[proposition]{Hypothesis}
\newtheorem{example}[proposition]{Example}
\newtheorem{remark}[proposition]{Remark}
\newtheorem{ex}[proposition]{Exercise}
\newtheorem{cond}[proposition]{Conditions}
\newtheorem{cons}[proposition]{Construction}
%
%
%\newcommand{\C}[4]{\left[\begin{array}{rcl}&#1\\#3&\dw\dw&#4\\&#2\end{array}\right]}
\newcommand{\llabel}[1]{\label{#1}[{\bf #1}]}
%\newcommand{\llabel}[1]{\label{#1}}
\newcommand{\comment}[1]{}
\newcommand{\sr}{\rightarrow}
\newcommand{\lr}{\longrightarrow}
\newcommand{\xr}{\xrightarrow}
\newcommand{\dw}{\downarrow}
\newcommand{\bdl}{\bar{\Delta}}
\newcommand{\zz}{{\bf Z\rm}}
\newcommand{\zq}{{\bf Z}_{qfh}}
\newcommand{\nn}{{\bf N\rm}}
\newcommand{\qq}{{\bf Q\rm}}
\newcommand{\nq}{{\bf N}_{qfh}}
\newcommand{\oo}{\otimes}
\newcommand{\uu}{\underline}
\newcommand{\ih}{\uu{Hom}}
\newcommand{\af}{{\bf A}^1}
\newcommand{\wt}{\widetilde}
\newcommand{\gm}{{\bf G}_m}
\newcommand{\dsr}{\stackrel{\sr}{\scriptstyle\sr}}
%\newcommand{\PP}{$P_{\infty}$}
\newcommand{\tp}{\tilde{D}}
\newcommand{\HH}{$H_{\infty}$}
\newcommand{\ii}{\stackrel{\scriptstyle\sim}{\sr}}
\newcommand{\BB}{_{\bullet}}
\newcommand{\D}{\Delta}
\newcommand{\colim}{{\rm co}\hspace{-1mm}\lim}
\newcommand{\cf}{{\it cf} }
\newcommand{\msf}{\mathsf }
\newcommand{\mcal}{\mathcal }
\newcommand{\ep}{\epsilon}
\newcommand{\tl}{\widetilde}
\newcommand{\ub}{\mbox{\rotatebox{90}{$\in$}}}
\newcommand{\ssp}{\,\,\,\,\,\,\,\,}
\newcommand{\red}{\twoheadrightarrow}
\newcommand{\eqg}{\stackrel{\Gamma}{\approx}}
\newcommand{\alphaeq}{\stackrel{\alpha}{\sim}}
\newcommand{\rtr}{\triangleright}
%
\newcommand{\piece}{\vskip 3mm\noindent\refstepcounter{proposition}{\bf
\theproposition}\hspace{2mm}}
\newcommand{\subpiece}{\vskip 3mm\noindent\refstepcounter{equation}{\bf\theequation}
\hspace{2mm}}{\vskip
3mm}

\newcommand{\ev}{{\bf ev}}
\newcommand{\TT}{{\bf Type0}}
\newcommand{\PP}{{\bf Prop}}
\newcommand{\cc}{{\bf c}}
\newcommand{\rect}{{\bf rect}}
\newcommand{\eqd}{\stackrel{d}{=}}



\newcommand{\cu}{{u}}
\newcommand{\Eu}{{\cal U}}
\newcommand{\JJ}[2]{{J(#1,#2)\,}}
\newcommand{\J}[1]{{J(#1)\,}}
\newcommand{\jj}[3]{{j(#1,#2,#3)\,}}
\newcommand{\jr}[2]{{jr(#1, #2)\,}}
\newcommand{\jl}[2]{{jl(#1, #2)\,}}
\newcommand{\UU}[1]{{UU(#1)}}
\newcommand{\rd}{\succ}
\newcommand{\rde}{\succeq}
\newcommand{\rdA}{\rd_{\AA}}
\newcommand{\brd}{\equiv}
\newcommand{\ind}{Ind\,\,}
\newcommand{\erd}[1]{\equiv_{{\AA},#1}}
\newcommand{\spc}{{\,\,\,\,\,\,\,}}
\renewcommand{\AA}{{\cal A}}
%
\begin{document}
%

\parskip = 2mm
\begin{center}
{\bf\Large A universe polymorphic type system}

{\bf Vladimir Voevodsky}

{Started January 11, 2012. Work in progress.}  
\end{center}




Notes from discarded attempts: 

1. Jan. 21, 2012 Without distinguishing types and terms whose type is a universe (i.e. without $El$ constructor ) and without type cumulativity  necessarily leads to a system where 

a. one has to introduce explicit functions going both ways between the types represented by a term of $U_n$ and its image in $U_{n+1}$ together with additional reduction rules for making these functions strict isomorphisms,

b. one will have a proliferation of non-equal but strictly isomorphic types sometimes having the same universe level as for example $X\sr Y$ and $X\sr j\, Y$ for $X:U_{n+1}$, $Y:U_n$. 

2. Jan. 27, 2012. In a system with T- and o-expressions one can not restrict oneself to $forall$ operators acting only between terms of the same universe level since it leads to the loss of confluence for the reduction related to the interaction of $forall$ and $j$ and the reduction related to the interaction of two $j$'s.

3. The introduction of resizing rules rr0 and rr1 leads naturally to a situation where definitional equality is no more determined as combination of $\equiv_{\AA}$ with the equivalence relation generated by reductions. While reductions and associated notion of non-reducible terms (which exist conjecturally) remain, two non-reducible terms may be definitionally equal in a "non-trivial" way.  

4. An example of a derivable term $E$ with a sub-term $f$ such that replacing $f$ be $f'$ which is connected to $f$ by an object of $Id f f'$ makes the resulting term $E[f'/f]$ non-derivable. One takes $f:Bool \sr \sum t:\Eu, [El](T)$ (where $\Eu$ is a universe) given by $f(true)=(T_0, a)$, $f(false)=(T_0,b)$. Then $E=Id\, T_0, [pr2](f\,true), [pr2](f\,false)$. If $f'$ is a function connected by an object of $Id$ to $f$ and such that $[pr1](f'\, true)$ is not definitionally equal to $T_0$ then $E[f'/f]$ is not derivable. There should be even more elementary examples. 

5. Aug. 17, 2012. Started to re-write the specification using the definition of a type system based on four classes of "sentences": contexts, T-terms equalities in a context, judgements and o-terms equalities in a type in a context.    

\tableofcontents


\section{Introduction}
%
We will work on the semi-syntactic level with named variables. We have three classes of variables - o-variables which can be substituted by o-expressions (see below), T-variables which can be substituted by T-expressions (see below) and u-level variables. Semi-syntactic means here that we are going to define expressions or pre-terms as planar trees with vertices marked either by a name of a variable or by a u-level expression (see below) or by a sequence of the form $(S;x_1,\dots,x_n)$ where $S$ is a special symbol (from the given set of allowed special symbols), $n\ge 0$  and $x_1,\dots,x_n$ are names of o-variables. The occurrences of variables named in the node label in the nodes below are considered to be bound. All expressions are considered up to $\alpha$-equivalence i.e. the renaming of bound variables and since the problems related to the possible conflict of variable names are the usual ones we ignore them in this exposition. 

This level of formalization is an intermediate one between the syntactic (linear) presentation of expressions on the one hand and nameless presentation (using some version of de Brujin indexes) on the other. The choice of a particular syntactic representation which is necessary at the level of the user interface and of a particular nameless representation which is necessary for the internal manipulation of expressions by the system can vary and are left for the next stage of concretization. 

We describe several systems here by starting with the simplest one and later adding more and more features. Common to all the systems defined in this paper is that they are fully universe polymorphic. In particular there is a class of expressions which are called u-level expressions which are used to specify the level of universes and which can contain u-variables. They also come with their own concept of equality $\equiv_{\AA}$ modulo a given set of universe constraints ${\AA}$. Note that what we describe at each step is not an individual type system but a family of type systems parametrized by "universe contexts" - the lists of permitted universe variables and required constraints between these variables and by lists of T-variables. To each universe context and a list of T-variables there corresponds a type system in the sense of \ref{notes} and in particular a contextual category. 

We will also discuss transformations between universe contexts and lists of type variables which lead to functors between the corresponding contextual categories or, on the more practical level, to automatic translations of definitions, theorems and proofs built in one universe context and with one list of type variables into similar objects built in  another universe context and/or with another list of type variables.  

In each of the systems we define first terms, T-terms and o-terms. These are expressions which satisfy certain simple local conditions. For a given universe context and a sequence of T-variables, the derivable terms of the corresponding type system which "denote" types will always be T-terms and the derivable terms which "denote" objects of types will always be o-terms. The concepts of contexts as sequences of the form $(x_1:E_1,\dots, x_n:E_n)$  where $E_i$ is a T-term with free o-variables from the set $\{x_1,\dots,x_{i-1}\}$ and judgements as  sequences of the form $(x_1:E_1,\dots, x_n:E_n; o:T)$  where $(E_1,\dots, E_i)$ is a context, $T$ is a T-expression with free o-variables from $\{x_1,\dots,x_n\}$ and $o$ is an o-expression with free o-variables from $\{x_1,\dots,x_n\}$ are standard. 

The terms are introduced in such a way that for any context $\Gamma=(x_1:E_1,\dots, x_n:E_n)$ and any o-term $o$ with free variables from $\{x_1,\dots,x_n\}$ there is an easily computable T-term $\tau_{\Gamma}(o)$ which in the case when both the $\Gamma$  and $o$  are derivable gives a canonical form for the type of $o$. To have this typing function defined on all o-terms we had to introduce some unusual features into the syntax. For example evaluation node in our system is a quantifier of the form $[ev;x](o_1,o_2,T)$ where $T$ is the target type of the function $o_1$ and $x$ is the "dependent variable" in $T$. For derivable terms this extra arguments can be reconstructed from the other data. Whether it makes sense to keep those arguments in the implementations or not is a question which should be considered separately.  

We further consider the equivalence relation $\sim_{\AA}$ on terms. It is based on another  important concept of essential and non-essential nodes and sub-terms of a term. Two terms $E_1$ and $E_2$ are $\sim_{\AA}$ equivalent if the  expressions $Ess(E_1)$ and $Ess(E_2)$ obtained from $E_1$ and $E_2$ by the removal of all non-essential sub-expressions are $\equiv_{\AA}$ equivalent. 

Both $\equiv_{\AA}$ and $\sim_{\AA}$ are shown to be decidable and in practice are expected to be very easily decidable i.e. to have low  complexity of the decision procedure.   

The next structure which we define for each type system is the set of reduction rules which are also defined on all terms. The reduction rules depend on the universe context and especially on the set of universe constraints of this context ${\AA}$ and we denote the transitive version of reducibility relative to ${\AA}$ by $\rd_{\AA}$ and the transitive reflexive version by $\rde_{\AA}$. We only consider reductions which occur at the essential nodes of a term. While our reduction rules can be equally applied to non-essential nodes it is not clear whether that such an extended notion has any practical uses. 

Definitional equality of a given type system is the third member of a sequence of equivalence relation $\equiv_{\AA}$, $\sim_{\AA}$ and finally $\eqd_{\AA}$. As mentioned above, the relation $\equiv_{\AA}$ is the relation of equality between u-level subexpressions which was mentioned above. The relation $\sim_{\AA}$ is $\equiv_{\AA}$ between the essential sub-expressions of the corresponding terms. Finally, definitional equality is defined as the equivalence relation generated by $\rde_{\AA}$ and $\sim_{\AA}$.  

To verify that our reduction rules are consistent we show local confluence (i.e. confluence of two one step reductions) in each system modulo $\sim_{\AA}$ i.e. for $E\rd_{\AA} E_1$ and $E\rd_{\AA} E_2$ where both reductions are one-step ones we show the existence of $E_1'$ and $E_2'$ such that $E_1\rde_{\AA} E_1'$, $E_2\rde_{\AA} E_2'$ and $E_1\sim_{\AA} E_1'$. The confluence holds in most cases for general terms but in some exceptional cases it is expected to hold only for derivable terms. 

We then describe the derivation rules in the context/judgement form.  A slight difference between our form for derivation rules and the usual ones is that the rules for the formation of new type expressions are written directly as rules for adding a new component to a context i.e. we write $\Gamma, x : T \vdash$ where one would usually write $\Gamma\vdash T : Type$. 

For practical implementation of a type system in the style in which Coq is written one has to be able to deal with a situation when a user-written proof tactic produces a term whose correctness needs to be verified by an independent type-checker. Since the derivation steps of such a term are not supplied by the tactic there must be an algorithm which, given a context $\Gamma$ or a judgement $\Gamma\vdash t :T$ is able to determined whether or not the context or the judgement is derivable.  

(???) There is a more or less obvious algorithm of this sort for each of our type systems. The correctness and termination properties of these algorithms depend on a number of properties of each system which are usually summed up under the name of meta-theory. We prove some of these theorems and formulate others as conjectures for the future work. This choice is a consequences of three circumstances. Firstly, one can start to work on the implementation of a proof assistant based on the systems introduced here having just the syntax and the type checking algorithms. Secondly, the consistency of the proposed type systems can be verified by model construction which does not require most of the meta-theory results. Thirdly, due to the relative complexity of even the first of our type systems it appears to be unreasonable to try to prove more complex meta-theorems  "by hand" and one should probably start by formalizing the definitions we give in one of the accepted proof assistants such as Coq and then proceed to giving formal proof of the meta-theorems. (???)

The last system (called simply TS) described here represents the first layer of the system which I hope will eventually be implemented in the new proof assistant. The second layer is formed by "quasi-constructive" features such as functional extensionality, ctf-terms and univalence axiom. The difference here lies in the nature of the algorithms which are required for computations in the fully constructive first layer and quasi-constructive second. We expect that an appropriate version of strong normalization holds for TS  and that any object of type $\nn$ (natural numbers) which is in the normal form is a numeral. Therefore, computation on terms of this layer can be done by a normalization algorithm. 

The property that any object of type $\nn$ normalizes to a numeral is known to become false when one adds quasi-constructive features. However, it is expected that a weaker property which is still sufficient for computation holds. Namely, it is expected that there is a terminating algorithm which, given a derivable object $o$ of type $\nn$ (in any context) which uses quasi-constructive features, produces a derivable object $o'$ of the same type which is build without the use of these features and an object of the identity type between $o$ and $o'$. This property should generalize to other "datatypes".

On notations and conventions: If $E$ is a labelled tree, $S$ is a branch of $E$ and $S'$ is another labelled tree we write $E[S'/S]$ for the labelled tree obtained by the direct substitution of the branch $S'$ instead of $S$.  If $E$, $S$ are expressions with free variables from a set $Fv$ and $x\in Fv$ we write $E[S/x]$ for the expression obtained by the substitution of all the occurrences of $x$ by $S$ with a possible renaming of bound variables such as to avoid name conflicts.  

We will write $\vec{a}$ for a sequence $a_1,\dots,a_n$ and let $dim(\vec{a})$ denote the number of items in the sequence.  

We assume three alphabets for variables one for u-level variables, one for T-variables and one for o-variables. Unless otherwise indicated variables named $x,y,z$ (with or without diacritics) are o-variables, variables named  $X,Y,Z$ (with or without diacritics) and the ones named $p,q,r$ are u-level variables (see below). The letters $i,j,k,l,m,n$ are reserved for numerals (e.g. in indexes). 

We write $[L](B_1,\dots,B_n)$ for a labelled (planar i.e. with ordered branches) tree with the root node labelled by $L$ and branches $B_1,\dots,B_n$. We also abbreviate $[L]([L'](B_1,\dots,B_n))$ as $[L][L'](B_1,\dots,B_n)$. 

We will use the following lemma which holds for systems of expressions with any choice of labels:

\begin{lemma}
\llabel{sublemma}
Let $E, o_1, o_2$ be expressions with free variables from a set $F$. Let $x,y\in F$ where $x\ne y$. Assume that $o_1$ does not depend on $y$. Then one has $(E[o_2/y])[o_1/x]=(E[o_1/x])[o_2[o_1/x]/y]$.
\end{lemma}
%
\begin{proof}
Easy induction by the depth of $E$ with the cases when $E=[x]$, $E=[y]$ and $E=[L](B_1,\dots,B_n)$ where $L\ne x, y$ to be considered separately.
\end{proof}
%

\section{Universe contexts}

\begin{definition} 
\llabel{d21a}
A u-level expression is either a numeral or a u-level variable or an expression of the form $M+n$ where $M$ is a u-level expression and $n$ is a numeral or an expression of the form $max(M_1,M_2)$ where $M_1,M_2$ are two u-level expressions.
\end{definition}
%
Note that u-level expressions are exactly "linear" function of u-level variables in the tropical (max-plus) semi-ring. 
%
\begin{definition}
\llabel{d21b}
Let $Fu$ be a finite set. A subset ${\AA}$ of $\nn^{Fu}$ is called admissible if it is defined by a system of equations of the form $M_i=N_i$ where $M_i,N_i$ are u-level expressions in variables from $Fu$. 
\end{definition}
%
\begin{lemma}
\llabel{uld}
Let ${\AA}$ be an admissible subset of $Fu$ and $M,N$ are u-level expressions with variables from $Fu$. Then the condition "for all $\vec{n}\in {\AA}$ one has  $M(\vec{n})=N(\vec{n})$" is decidable.
\end{lemma}
%
\begin{proof}
The condition considered in the lemma can be expressed in Presburger arithmetic which is decidable. For a further discussion see \cite{???}. 
\end{proof}

Since $M(\vec{n})\ge N(\vec{n})$ is equivalent to $M(\vec{n})=max(M(\vec{n}),N(\vec{n}))$, Lemma \ref{uld} implies that conditions of the form "for all $\vec{n}\in {\AA}$ one has  $M(\vec{n})\ge N(\vec{n})$" is also decidable.  

\begin{remark}\rm
Note also that any u-level expression can be re-written in the form $M=max(n_0, u_1+n_1,\dots,u_l+n_l)$ where $u_i$ are u-level variables and $n_i\in\nn$. By choosing a linear ordering on $Fu$ and replacing $max(u+n, u+n')$ by $u+ max(n,n')$ we can further assume that in our representation $u_i<u_{i+1}$ according to our ordering. This effectively provides us with a normal form of a u-level expression. 

However as will be seen below we will be mostly interested in equality of u-level expressions not on the whole of $\nn^{Fu}$ but on a given admissible subset of $\nn^{Fu}$. 
 \end{remark}

\begin{definition}
\llabel{uc}
A universe context $UC$ is a pair $(Fu,{\AA})$ where $Fu$ is a finite sequence of u-level variables and ${\AA}$ an admissible domain in $\nn^{Fu}$.
\end{definition}






\section{System TS0} 
%
We first describe the system $TS0$ which has only elements related to universes and dependent products and later add the elements related to other constructions.
%
%
\subsection{TS0-terms and the typing function}
%
\begin{definition}
\llabel{d01}
The following labels are permitted in the expressions of $TS0$ : names of o-variables, names of T-variables, u-level expressions, $\Eu$, $El$, $(\prod;x)$, $\cu$, $j$, $(ev;x)$, $(\lambda;x)$, $(forall;x)$.
\end{definition}
%
\begin{definition}
\llabel{d02}
We distinguish three classes of expressions:
%
\begin{enumerate}
\item u-level expressions,
\item T-expressions are the ones with the root node $[X]$ where $X$ is the name of a T-variable, $[\Eu]$, $[El]$ or $[\prod;x]$,
\item o-expressions are the ones with the root $[x]$ where $x$ is the name of an o-variable, $[\cu]$, $[j]$, $[ev;x]$, $[\lambda;x]$ or $[forall;x]$.
\end{enumerate}
\end{definition}
%
%
\begin{definition}
\llabel{d03}
A TS0-term is a T-expression or an o-expression (with labels from the set described in Definition \ref{d01}) which satisfies the following conditions: 
%
\begin{enumerate}
\item any node of the form $[M]$ where $M$ is a u-level expression has valency $0$ (i.e. is a leaf),
%
\item any node of the form $[X]$ where $X$ is the name of a T-variable has valency $0$ (i.e. is a leaf),
\item any node of the form $[\Eu]$ has valency $1$ and its only branch is a node labelled by a u-level expression,
\item any node of the form $[El]$ has valency $1$ with its only branch being an o-expression,
\item any node of the form $[\prod;x]$ has valency $2$, both of its branches are T-expressions and the first branch does not contain $[x]$,
%
\item any node of the form $[x]$ where $x$ the name of an o-variable has valency $0$ (i.e. is a leaf),
\item any node of the form $[\cu]$ has valency $1$ and its only branch is a node labelled by a u-level expression,
\item any node of the form $[j]$ has valency $2$ and both of its branches are nodes labelled by u-level expressions,
\item any node of the form $[ev;x]$ has valency $3$ its first two branches are o-expressions which do not contain $[x]$ and the third branch is a T-expression,
\item any node of the form $[\lambda;x]$ has valency $2$, its first branch is a T-expression which does not contain $[x]$ and its second branch is an o-expression,
\item any node of the form $[forall;x]$ has valency $4$, its first two branches are nodes labelled by u-level expressions and last two branches are o-expressions and the third branch does not contain $[x]$.
\end{enumerate}
%
\end{definition}
%
We define o-terms as terms which are o-expression and T-terms as terms which are T-expressions. 
Intuitively, T-terms correspond to types and o-terms correspond to objects of types.

For $x\in Fv$ (resp. $X\in FV$) we will often write $x$ instead of $[x]$ (resp. $X$ instead of $[X]$). We will abbreviate $[\Eu][M]$ as $\Eu_M$, $[\cu][M]$ as $\cu_M$, $[j]([M_1],[M_2])$ as $j_{M_1,M_2}$ and $[forall;x]([M_1],[M_2],o_1,o_2)$ as $[forall_{M_1,M_2};x](o_1,o_2)$. 

\begin{definition}
\llabel{d04}
Let $E$ be a TS0-term. A node is called non-essential if it belongs to the subexpression $T$ of a subexpression of the form $[ex;x](o_1,o_2,T)$. Otherwise a node is called essential. A subexpression is called non-essential (resp. essential) if its root node is non-essential (resp. essential).

For a term $E$ we let $Ess(E)$ denote the subexpression of $E$ (which is not a term anymore) which is obtained by removing all non-essential subexpressions from $E$
\end{definition}
% 
Note that the root node of any term is essential, therefore $Ess(E)$ is always non-empty and therefore an expression. 






%
\begin{remark}\rm
There is a similarity in our description of TS0 to the description of the Calculus of Constructions which is given in \cite{Streicher}. In \cite{Streicher}, T-terms are the ones which start with $[\prod;x]$, $[Prop]$ (analog of our $\Eu_0$) or $[Proof]$ (analog of our $[El]$) and o-terms are the ones which start with $[x]$, $[\lambda;x]$, $[App]$ (the analog of our $[ev;x]$ - see remark below) or $[\forall;x]$. The later is an analog of our $[forall_{0,0};x]$ and $[forall_{1,0};x]$ which in the case of CC coincide due to the impredicativity of $Prop$. For the same reason the first node of $[\forall;x]$ is a T-term which is analogous to $[El](o_1)$ in $[forall_{M,0}](o_1,o_2)$ with $M=0,1$. 

It should be easy to describe a subset of TS0-terms which can be directly mapped to CC-terms while preserving all the main constructions. 
\end{remark}   
%
\begin{remark}\rm
In our description the evaluation node $[ev;x]$ is a quantifier i.e. it bounds a variable. This is due to the fact that we want to include the target type of function being evaluated as the third branch of the evaluation expression and this type may include, in dependent cases, an additional variable. This allows us to define the typing function on all terms before we proceed to the notions of definitional equality and derivable.

It might also be convenient to have our third argument of evaluation present on the level of implementations as an implicit argument. While, due to the expected properties of normalization in the system, it can always be inferred up do definitional equality from other arguments, this inference may require computation which can be avoided by providing an explicit value of this argument.
\end{remark}
%





We let $TS0$ denote the set of TS0-terms and $TT0$ and $oT0$ denote the subsets of T-terms and o-terms.

According to the general rule stated above, variable $x$ appearing under the nodes $[\prod,x]$, $[ev;x]$, $[\lambda,x]$ and $[forall;x]$ is called bound.  Variables which are not bound are called free. We will write $TS0(Fu,FV,Fv)$, $TT0(Fu,FV,Fv)$ and $oT0(Fu,FV,Fv)$ for the sets of terms, T-terms and o-terms respectively with u-level variables from the set $Fu$, free T-variables from the set $FV$ and free o-variables from the set $Fv$.

%
\begin{lemma} 
\llabel{l02}
One has:
%
\begin{enumerate} 
\item Any branch of a TS0-term is a TS0-term or a u-level expression,
\item For $E\in TS0(Fu,FV,Fv)$ (resp. $TT0(Fu,FV,Fv)$, $oT0(Fu,FV,Fv)$), $X\in FV$ and $o\in oT0(Fu,FV,Fv)$ one has $E[o/x]\in TS0(Fu,FV,Fv)$ ( resp. $E[o/x]\in TT0(Fu,FV,Fv)$, $E[o/x]\in oT0(Fu,FV,Fv)$),
\item For $E\in TS0(Fu,FV,Fv)$ (resp. $TT0(Fu,FV,Fv)$, $oT0(Fu,FV,Fv)$), $x\in Fv$ and $o\in oT0(Fu,FV,Fv)$ one has $E[o/x]\in TS0(Fu,FV,Fv)$ ( resp. $E[o/x]\in TT0(Fu,FV,Fv)$, $E[o/x]\in oT0(Fu,FV,Fv)$).
\end{enumerate}
\end{lemma}
%
\begin{proof}
Straightforward.
\end{proof}
%
The correctness of the following definition follows from Lemma \ref{l02}(3).
%
\begin{definition}
\llabel{dtau0}
For any finite set $Fv$ and any function $\Gamma:Fv\sr TT0(Fu,FV,Fv)$ we define the typing function $\tau=\tau_{\Gamma}: oT0(Fu,FV,Fv)\sr TT0(Fu,FV,Fv)$ relative to $\Gamma$ inductively (by induction on the number of nodes in the term) as follows:
%
\begin{enumerate}
\item For $x\in Fv$, $\tau([x])=\Gamma(x)$,
\item $\tau([\cu_M])=\Eu_{M+1}$,
\item $\tau([j_{M_1,M_2}])=[\prod;x](\Eu_{M_1},\Eu_{M_2})$,
\item $\tau([ev;x](o_1,o_2,T))=T[o_2/x]$,
\item $\tau([\lambda;x](T,o))=[\prod;x](T,\tau_{\Delta}(o))$ where $\Delta$ is the function on on $Fv\amalg \{x\}$ which equals $\Gamma$ on $Fv$ and $T$ on $x$.
\item $\tau([forall_{M_1,M_2};x](o_1,o_2))=\Eu_{max(M_1,M_2)}$.
\end{enumerate}
\end{definition}
%
%??? make the text more readable by resolving the fact that what is should be denoted by $\Gamma(i)$ according to the idea that $\Gamma$ is a function has no special notation later and, usually, is described as $T_i$ where $\Gamma=\dots$. 
%
\begin{proposition}
\llabel{tausub0}
Let $\Gamma:Fv\sr TT0(Fu,FV,Fv)$ be a function, $o,s\in oT0(Fu,FV,Fv)$ and $x\in Fv$. Assume that the following conditions hold:
%
\begin{enumerate}
\item $s$ does not depend on $x$,
\item $\Gamma(x)$ does not depend on $x$,
\item $\tau_{\Gamma}(s)=\Gamma(x)$. 
\end{enumerate}
%
Then one has
%
$$(\tau_{\Gamma}(o))[s/x]=\tau_{\Gamma[s/x]}(o[s/x])$$
%
where $\Gamma[s/x]$ is the function $x'\mapsto \Gamma(x')[s/x]$.
\end{proposition}
%
\begin{proof}
Let us proceed by induction on the depth of $o$. We have to consider the various options for the structure of $o$ listed in Definition \ref{dtau0}.
%
\begin{enumerate}
\item $o=[x']$ for $x'\in Fv$. We have two sub-cases
%
\begin{enumerate}
\item if $x'\ne x$ we have 
%
$$(\tau_{\Gamma}(o))[s/x]=(\tau_{\Gamma}([x']))[s/x]=\tau_{\Gamma[s/x]}([x'])=\tau_{\Gamma[s/x]}(o[s/x])$$
%
where the middle equality holds by definition of $\Gamma[s/x]$,
%
\item if $x'=x$ we have 
%
$$(\tau_{\Gamma}(o))[s/x]=(\tau_{\Gamma}([x])[s/x]=(\Gamma(x))[s/x]=\Gamma(x)$$
%
where the last equality holds by condition (2) of the proposition and
%
$$\tau_{\Gamma[s/x]}(o[s/x])=\tau_{\Gamma[s/x]}(s)=\tau_{\Gamma}(s)$$
%
where the last equality holds by condition (1) of the proposition. Together with condition (3) these equalities imply the assertion of the proposition for $o=[x]$.
\end{enumerate}
%
\item $o=[\cu_M]$. Then $\tau_{\Gamma}(o)[s/x]=\Eu_{M+1}=\tau_{\Gamma[s/x]}(o[s/x])$.
%
\item $o=[j_{M_1,M_2}]$. Then $\tau_{\Gamma}(o)[s/x]=[\prod;y](\Eu_{M_1},\Eu_{M_2})=\tau_{\Gamma[s/x]}(o[s/x])$.
%
\item $o=[ev;y](o_1,o_2,T)$. Then
%
$$\tau_{\Gamma}(o)[s/x]=(T[o_2/y])[s/x]$$
%
and
$$\tau_{\Gamma[s/x]}(o[s/x])=(T[s/x])[(o_2[s/x])/y]$$
%
Since $s$ does not depend on $y$ these two expressions are equal by Lemma \ref{sublemma}.
%
\item $o=[\lambda;y](T,o')$. We have
%
$$(\tau_{\Gamma}(o))[s/x]=([\prod;y](T,\tau_{\Delta}(o')))[s/x]=[\prod;y](T[s/x],\tau_{\Delta}(o')[s/x])$$
%
and
%
$$\tau_{\Gamma[s/x]}(o[s/x])=\tau_{\Gamma[s/x]}([\lambda;y](T[s/x],o'[s/x]))=[\prod;y](T[s/x],\tau_{\Delta'}(o'[s/x]))$$
%
where $\Delta'$ equals $\Gamma[s/x]$ on $Fv$ and $T[s/x]$ on y. Therefore, $\Delta'=\Delta[s/x]$. The conditions (1)-(3) still hold for $\Delta$ and the depth of $o'$ is strictly less than the depth of $o$. Therefore by the inductive assumption $\tau_{\Delta}(o')[s/x]=\tau_{\Delta[s/x]}(o'[s/x])$. 
%
\item $o=[forall_{M_1,M_2};y](o_1,o_2)$. We have $\tau_{\Gamma}(o)[s/x]=\Eu_{max(M_1,M_2)}$ and 
%
$$\tau_{\Gamma[s/x]}(o[s/x])=\tau_{\Gamma[s/x]}([forall_{M_1,M_2};y](o_1[s/x],o_2[s/x]))=\Eu_{max(M_1,M_2)}.$$
%
\end{enumerate}
\end{proof}
%



\subsection{Equivalence relations $\equiv_{\AA}$ and $\sim_{\AA}$ on TS0-terms}
\llabel{sim0}
%
Let $UC=(Fu,{\AA})$ be a universe context and $FV$ a sequence of T-variables. In this section we define two simple equivalence relations on TS0-terms with u-variables from $Fu$ and T-variables from $FV$ which depend on ${\AA}$. Recall that we always consider expressions up to the $\alpha$-equivalence (renaming of bound variables). 

For $E\in TS0(Fu,FV,Fv)$ and an element $\vec{n}\in \nn^{Fu}$ we write $E[\vec{n}]$ for the TS0-term obtained by evaluating all of the u-level expressions in $E$ on $\vec{n}$.
%
\begin{definition}
\llabel{dequivA0}
Define an equivalence relation $\equiv_{\AA}$ on $TS0(Fu,FV,Fv)$ for all $Fv$ by the condition that $E_1\equiv_{\AA} E_2$ iff for all $\vec{n}\in {\AA}$ one has $E_1[\vec{n}]=E_2[\vec{n}]$.
\end{definition}
%
\begin{lemma}
\llabel{lequivA0}
The equivalence relation $\equiv_{\AA}$ is decidable.
\end{lemma}
%
\begin{proof}
It follows immediately from Lemma \ref{uld}.
\end{proof}
%
Note that $E_1\equiv_{\emptyset} E_2$ iff $E_1$ and $E_2$ differ only in their u-level subexpressions.
%
\begin{lemma}
\llabel{equivsub01}
In the notations used above let $E,E'\in TS0(Fu,FV,Fv)$ and $E\equiv_{\AA} E'$ then one has:
%
\begin{enumerate}
\item for $x\in Fv$ and $s\in oT0(Fu,FV,Fv)$ one has $E[s/x]\equiv_{\AA} E'[s/x]$,
\item for $X\in FV$ and $T\in TT0(Fu,FV,Fv)$ one has $E[T/X]\equiv_{\AA} E'[T/X]$. 
\end{enumerate}
\end{lemma}
%
\begin{proof}
Straightforward by induction on the number of nodes in $E$ and $E'$. 
\end{proof}
%
\begin{lemma}
\llabel{equivsub02}
Let $E$ be an term of the form $E=[L](B_1,\dots,B_n)$. Suppose further that for each $i=1,\dots,n$ one has $B_i\equiv_{\AA} B_i'$. Then $E\equiv_{\AA} [L](B_1',\dots,B_n')$.
\end{lemma}
%
\begin{proof}
Straightforward.
\end{proof}
%
\begin{lemma}
\llabel{redsub03}
In the notations used above let $E\in TS0(Fu,FV,Fv)$ then one has:
%
\begin{enumerate}
\item Let $s,s'\in oT0(Fu,FV,Fv)$ such that $s\equiv_{\AA} s'$ and $x\in Fv$, then $E[s/x]\equiv_{\AA} E[s'/x]$.
\item Let $T,T'\in TT0(Fu,FV,Fv)$ such that $T\equiv_{\AA} T'$ and $X\in FV$, then $E[T/X]\equiv_{\AA} E[T'/x]$.
\end{enumerate}
\end{lemma}
%
\begin{proof}
Straightforward.   
\end{proof}
%

\begin{definition}
\llabel{dsimA0}
Define an equivalence  relation $\sim_{\AA}$ on $TS0(Fu,FV,Fv)$ for all $Fv$ by the condition that $E\sim_{\AA} E'$ iff $Ess(E)\equiv_{\AA} Есс(Е')$\end{definition}
%
%
\begin{lemma}
\llabel{Beqdec0}
The equivalence relation $\sim_{\AA}$ is decidable.
\end{lemma}
%
\begin{proof}
Follows easily from Lemma \ref{lequivA0}.
\end{proof}
%
\begin{lemma}
\llabel{simsub01}
In the notations used above let $E,E'\in TS0(Fu,FV,Fv)$ and $E\sim_{\AA} E'$ then one has:
%
\begin{enumerate}
\item for $x\in Fv$ and $s\in oT0(Fu,FV,Fv)$ one has $E[s/x]\sim_{\AA} E'[s/x]$,
\item for $X\in FV$ and $T\in TT0(Fu,FV,Fv)$ one has $E[T/X]\sim_{\AA} E'[T/X]$. 
\end{enumerate}
\end{lemma}
%
\begin{proof}
Straightforward. 
\end{proof}
%
%
\begin{lemma}
\llabel{simsub02}
Let $E$ be an term of the form $E=[L](B_1,\dots,B_n)$. Suppose further that for each $i=1,\dots,n$ one has $B_i\sim_{\AA} B_i'$. Then $E\sim_{\AA} [L](B_1',\dots,B_n')$.
\end{lemma}
%
\begin{proof}
Straightforward.
\end{proof}
%
\begin{lemma}
\llabel{simsub03}
In the notations used above let $E\in TS0(Fu,FV,Fv)$ then one has:
%
\begin{enumerate}
\item Let $s,s'\in oT0(Fu,FV,Fv)$ such that $s\sim_{\AA} s'$ and $x\in Fv$, then $E[s/x]\sim_{\AA} E[s'/x]$.
\item Let $T,T'\in TT0(Fu,FV,Fv)$ such that $T\sim_{\AA} T'$ and $X\in FV$, then $E[T/X]\sim_{\AA} E[T'/x]$.
\end{enumerate}
\end{lemma}
%
\begin{proof}
Straightforward.   
\end{proof}
%


\subsection{Derivation trees}
%
Notes:

\begin{definition}
\llabel{cuttingsrface}
For a rooted tree $E$ a "cutting surface" $S$ is a set of vertices such that the path from each leave of the tree to the root passes through exactly one vertex in $S$.  
\end{definition}
%
For example the sets of all leaves or the set consisting only of the root are cutting surfaces.
%
\begin{definition}
\llabel{csdepth}
A depth of a rooted tree $E$ relative to a cutting surface $S$ is the maximal distance (number of edges one has to cross) from elements of $S$ to the root of the tree. 
\end{definition}
%
For example the depth of a tree relative to $S=\{root\}$ is $0$ and the depth relative to the set of all leaves is the depth of the tree. 
%
\begin{lemma}
\llabel{surface}
Let $S$ be any subset of vertices of a rooted tree $E$ such that the path from any leaf to the root passes through at least one element of $S$. Let further $S_0$ be the subset of $S$ which is defined by the condition that $v\in S_0$ if an only if $v\in S$ and the path from $v$ to the root does not contain any other elements of $S$. Then $S_0$ is a cutting surface.
\end{lemma}
%
\begin{proof}
For any leaf $l$ of $E$ let $S(l)$ be the set of elements of $S$ which lie on the path from $l$ to the root. Then $S(l)\cap S_0$ consists of exactly one element, namely the element in $S(l)$ which is closest to the root.
\end{proof}
%
%
Given two cutting surfaces $S_1$, $S_2$ we say that $S_1\ge S_2$ if the path from any element of $S_1$ to the root contains an element of $S_2$. We will write $inf(S_1,S_2)$ for the cutting surface constructed according to Lemma \ref{surface} from the set of vertices $S_1\cup S_2$. 
Note that $inf(S_1,S_2)$ is indeed the greatest lower bound of the set $\{S_1,S_2\}$. 
%
\begin{enumerate}
%
\item Each derivation tree is rooted and each branch of a derivation tree is a derivation tree.
%
\item Each derivation tree defines a derivable sentence. In particular there are five kinds of derivation trees - the ones which define four kinds of sentences and the ones which define u-level expressions. 
%
\item Each vertex of a derivation tree is labelled by the (number or name of) the corresponding derivation rule. The kind of the branch corresponding to a given vertex is completely determined by the label of the vertex. 
%
\item Each derivation rule defines the following data structure:
%
\begin{enumerate}
\item the number of premises (each premise being a sentence),
\item the kind of each of the premises,
\item a "pattern matching" condition which the premises should satisfy.
\end{enumerate}
%
\item The correctness of a derivation tree is determined by the condition that at every vertex the number and kinds of branches are the ones which are prescribed by the label and that the corresponding pattern matching condition holds.
\end{enumerate}


\subsection{Derivation rules of TS0}
%
As was mentioned in the introduction the systems which we described are not type systems but families of type systems parametrized by universe contexts and sequences of T-variables. 

We are going to describe now the derivation rules for sentences of the type system $TS0_{UC,FV}$ associated with a given universe context $UC=(Fu,{\AA})$ and a sequence of T-variables $FV$. The description is given in the usual type-theoretic notation. It is assumed that new names of variables which appear in the derivation rules do not conflict with the previously existing ones. Everywhere below we use the letter $M$ with or without diacritics to denote a u-level expression in variables from $Fu$. The letter $\Gamma$ with or without diacritics is used to denote a derivable context. By $l(\Gamma)$ we denote the "length" of $\Gamma$ i.e. $l(x_1:T_1,\dots,x_n:T_n)=n$. 

According to \cite{NTP} a type system over a system of expressions is given by sets of {\em derivable} sentences of four kinds. In the sequent notation the sentences of each of the four kinds have the form
%
$$\Gamma\vdash$$
$$\Gamma\vdash o:T$$
$$\Gamma\vdash T=T'$$
$$\Gamma\vdash o=o':T$$
%
Derivable sentences are those which can be obtained by the derivation rules given below. Since precise derivation trees for sentences are going to be important to us it is convenient to have relatively small number of different derivation rules. Normally, one would include 
%
$$\frac{\Gamma\vdash}{\Gamma, x:\Eu_M\vdash}$$
%
as a family of derivation rules one for each well-formed u-level expression $M$. This is however inconvenient in particular because different u-level expressions can be equivalent and we do not want to deal with equivalence relations on the set of the derivation rules. Because of that we include in our consideration a fifth class of sentences which we write simply as $M$ with the meaning of such a sentence being that $M$ is a well-formed u-level expression in variables from $Fu$. From the abstract point of view it means that our four classes of derivable sentences are actually defined  by an inductive procedure which also involves a fifth class but later the fifth class is not considered as a part of the resulting type system.  

Note that even with this addition we actually have infinitely many derivation rules due to the issue with the "rule"
%
$$\frac{\Gamma,x:T,\Gamma'\vdash}{\Gamma,x:T,\Gamma'\vdash x:T}$$
%
which is actually a family of infinitely many derivation rules parametrized by natural numbers $i$ with $i=l(\Gamma)$ being a condition of the rule.
%
%????That's where we should use $\Gamma(i)$ expression.??? And then the condition is actually $i\le l(\Gamma)$. Tomorrow. 
%
\begin{enumerate}
\item for each $u\in Fu$ 
$$\frac{}{u}$$
\item 
$$\frac{M}{M+1}$$
\item 
$$\frac{M_1\spc M_2}{max(M_1,M_2)}$$
\item 
$$\frac{}{\vdash}$$
\item for each $X\in FV$, 
$$\frac{\Gamma\vdash}{\Gamma, x:X\vdash}$$
\item for each $i\in\nn$
$$\frac{\Gamma, x:T, \Gamma'\vdash\spc where\,\,l(\Gamma)=i}{\Gamma, x:T, \Gamma'\vdash x:T}$$
\item 
$$\frac{\Gamma, x:T\vdash\spc \Gamma, x:T'\vdash\spc T\sim_A T'}{\Gamma\vdash T\eqd T'}$$
\item 
$$\frac{\Gamma\vdash T_1\eqd T_2}{\Gamma\vdash T_2\eqd T_1}$$
\item 
$$\frac{\Gamma\vdash T_1\eqd T_2\spc\Gamma\vdash T_2\eqd T_3}{\Gamma\vdash T_1\eqd T_3}$$
\item 
$$\frac{\Gamma\vdash o:T\spc\Gamma\vdash o':T\spc o\sim_A o'}{\Gamma\vdash o\eqd o':T}$$
\item 
$$\frac{\Gamma\vdash o_1\eqd o_2:T}{\Gamma\vdash o_2\eqd o_1:T}$$
\item 
$$\frac{\Gamma\vdash o_1\eqd o_2:T\spc\Gamma\vdash o_2\eqd o_3:T}{\Gamma\vdash o_1\eqd o_3:T}$$
\item 
$$\frac{\Gamma\vdash o:T\spc \Gamma\vdash T\eqd T'}{\Gamma\vdash o:T'}$$
\item 
$$\frac{\Gamma\vdash o\eqd o':T\spc \Gamma\vdash T\eqd T'}{\Gamma\vdash o\eqd o':T'}$$
\item 
$$\frac{\Gamma\vdash\spc M}{\Gamma, x:\Eu_M\vdash}$$
\item 
$$\frac{\Gamma\vdash\spc M}{\Gamma\vdash  u_M:\Eu_{M+1}}$$
\item 
$$\frac{\Gamma\vdash o:\Eu_M}{\Gamma, x: [El](o)\vdash}$$
\item 
$$\frac{\Gamma\vdash\spc M}{\Gamma\vdash [El](u_M)\eqd \Eu_M}$$
\item 
$$\frac{\Gamma\vdash o\eqd o':\Eu_M}{\Gamma\vdash [El](o)\eqd [El](o')}$$
\item 
$$\frac{\Gamma\vdash o:\Eu_M\spc\Gamma\vdash o':\Eu_M\spc\Gamma\vdash [El](o)\eqd [El](o')}{\Gamma\vdash o\eqd o':\Eu_M}$$
\item 
$$\frac{\Gamma, x:T_1, y:T_2\vdash}{\Gamma, y:[\prod;x](T_1,T_2)\vdash}$$
\item 
$$\frac{\Gamma\vdash T_1\eqd T_1'\spc\Gamma, x:T_1\vdash T_2\eqd T_2'}{\Gamma\vdash [\prod;x](T_1,T_2)\eqd [\prod;x](T_1',T_2')}$$
\item 
$$\frac{\Gamma, x : T_1\vdash o: T_2}{\Gamma\vdash [\lambda;x](T_1,o):[\prod;x](T_1,T_2)}$$
\item 
$$\frac{\Gamma\vdash T_1\eqd T_1'\spc\Gamma, x:T_1\vdash o\eqd o':T_2}{\Gamma\vdash [\lambda;x](T_1,o)\eqd [\lambda;x](T_1',o'):[\prod;x](T_1,T_2)}$$
\item 
$$\frac{\Gamma\vdash f:[\prod;x](T_1,T_2)\spc \Gamma\vdash o:T_1}{\Gamma\vdash [ev;x](f,o,T_2):T_2[o/x]}$$
\item 
$$\frac{
\begin{array}{l}
\Gamma\vdash T_1\eqd T_1'\\
\Gamma, x:T_1\vdash T_2\eqd T_2'
\end{array}
\spc
\begin{array}{l}
\Gamma\vdash f\eqd f':[\prod;x](T_1,T_2)\\
\Gamma\vdash o\eqd o':T_1
\end{array}
}{\Gamma\vdash [ev;x](f,o,T_2)\eqd [ev;x](f',o',T_2'): T_2[o/x]}$$ 
\item 
$$\frac{\Gamma\vdash o_1:T_1\spc \Gamma, x:T_1\vdash o_2:T_2}{\Gamma\vdash [ev;y]([\lambda;x](T_1,o_2),o_1,T_2)\eqd o_2[o_1/x]:T_2[o_1/x]}$$
\item 
$$\frac{\Gamma\vdash f:[\prod;x](T_1,T_2)}{\Gamma\vdash [\lambda;x](T_1, [ev;y](f,x,T_2[y/x]))\eqd f:[\prod;x](T_1,T_2)}$$ 
\item 
$$\frac{\Gamma\vdash \spc M_1\spc M_2\spc M_1\le_{\AA} M_2}{\Gamma\vdash j_{M_1,M_2}:[\prod;x](\Eu_{M_1},\Eu_{M_2})}$$
\item 
$$\frac{\Gamma\vdash o:\Eu_{M_1}\spc M_2\spc M_1\le_{\AA} M_2}{\Gamma\vdash [El][ev;x](j_{M_1,M_2},o,\Eu_{M_2})\eqd [El](o)}$$
\item 
$$\frac{\Gamma\vdash o_1:\Eu_{M_1}\spc \Gamma, x:[El](o_1)\vdash o_2:\Eu_{M_2}}{\Gamma\vdash [forall_{M_1,M_2};x](o_1,o_2):\Eu_{max(M_1,M_2)}}$$
\item 
$$\frac{\Gamma\vdash o_1:\Eu_{M_1}\spc \Gamma, x:[El](o_1)\vdash o_2:\Eu_{M_2}}{\Gamma\vdash [El][forall_{M_1,M_2};x](o_1,o_2)\eqd [\prod;x]([El](o_1),[El](o_2))}$$
\end{enumerate}







\subsection{TS0(UC,FV) are type systems}
\llabel{ts0aretypesystems}
%
Given a system of expressions such as the one given by TS0 terms relative to a given universe context $UC=(Fu,\AA)$ and a sequence of T-variables $FV$ one defines a type system over this system of expressions as four classes of sentences of the forms $\Gamma\vdash$, $\Gamma\vdash o:T$, $\Gamma\vdash T=T'$ and $\Gamma\vdash o=o':T$ which satisfy a number of technical conditions listed in \cite{NTP}. In this section we will show that  these conditions hold for the classes of derivable sentences of TS0.

In what follows we fix a universe context $UC$ and a sequence of T-variables $FV$ and consider all the notions relative to this context and this sequence.





%
\begin{lemma}
\llabel{dertree}
Any derivation tree for sequent of one of the following forms:
%
$$\Gamma,\Gamma'\vdash$$
$$\Gamma,\Gamma'\vdash o:T$$
$$\Gamma,\Gamma'\vdash T=T'$$
$$\Gamma,\Gamma'\vdash o=o':T$$
%
has (a unique) smallest cutting surface whose elements represent contexts of the form $\Gamma\vdash$ and u-level expressions. There is at least one element representing $\Gamma\vdash$ in this cutting surface.
\end{lemma}
%
\begin{proof}
It is easy to see from the shape of the derivation rules that there can be no cutting surface for any of the four main kinds of sentences which contains only u-level expressions. Therefore the second assertion of the lemma is automatically satisfied.

Since the the greatest lower bound of any two cutting surfaces is defined and is contained (as a subset) in the union of these surfaces, it is sufficient to show that that in each of the four cases for any derivation tree there exists at least one cutting surface satisfying  the conditions of the lemma. 

We proceed by induction on the depth of the derivation tree. 

Looking at the derivation rules we see that each of the premises for any derivation rule for a context of the form $\Gamma,\Gamma'\vdash$ where $\Gamma'$ is non-empty has either the same form or of the form $\Gamma,\Gamma'\vdash o:T$ or equals $\Gamma\vdash$. 

Each of the premises for any derivation rule for a judgement of the form  $\Gamma,\Gamma'\vdash o:T$ is either of the same form or of the form $\Gamma,\Gamma'\vdash T=T'$, or of the form $\Gamma,\Gamma'\vdash$ where $\Gamma'$ is non-empty or equals $\Gamma\vdash$.

Each of the premises for any derivation rule for a judgement of the form  $\Gamma,\Gamma'\vdash T=T'$ is either of the same form or of the form $\Gamma,\Gamma'\vdash o:T$, or of the form $\Gamma,\Gamma'\vdash o=o':T$,  or of the form $\Gamma,\Gamma'\vdash$ where $\Gamma'$ is non-empty or equals $\Gamma\vdash$.

Each of the premises for any derivation rule for a judgement of the form  $\Gamma,\Gamma'\vdash o:T$ is either of the same form or of the form $\Gamma,\Gamma'\vdash T=T'$, or of the form $\Gamma,\Gamma'\vdash o=o':T$,  or of the form $\Gamma,\Gamma'\vdash$ where $\Gamma'$ is non-empty or equals $\Gamma\vdash$.

Combining these properties of our derivation rules with the induction on the depth of the derivation tree we obtain the assertion of the lemma.
\end{proof} 
%
\begin{remark}\rm
Note that the assertion of Lemma \ref{dertree} is not tautological and really depends on the form of the derivation rules which one chooses in the definition of a type system. For example, if we included the rule
%
$$\frac{\Gamma\vdash}{\Gamma, x:X\vdash x:X}$$
%
for $X\in FV$ into our list of the generating derivation rules then Lemma \ref{dertree} would become false. Indeed then one would have a derivation tree for $x:X\vdash x:X$ which has only one edge terminating in the empty context $\vdash$ and in particular no vertices corresponding to the context $x:X\vdash$. 
\end{remark}
%
\begin{definition}
\llabel{derdepthgamma}
For a sentence of one of the forms listed in Lemma \ref{dertree} we define its derivation depth relative to $\Gamma$ as the minimum over all its derivation trees of the depth of this tree relative to the cutting surface defined in Lemma \ref{dertree}.
\end{definition}
%
Note that the derivation depth relative to $\Gamma$ is $0$ only for $\Gamma\vdash$. Note also that for any sentence of the form considered in Lemma \ref{dertree} whose derivation depth relative to $\Gamma$ is greater than $0$ there exists a derivation rule which generates this sentence such that all its premises are again of the same form and their derivation depth relative to $\Gamma$ is strictly less than of the original sentence.

As an immediate corollary of Lemma \ref{dertree} we get the following result.
%
\begin{lemma}
\llabel{dertree0}
For any derivable sequent of one of the following forms
%
$$\Gamma,\Gamma'\vdash$$
$$\Gamma,\Gamma'\vdash o:T$$
$$\Gamma,\Gamma'\vdash T=T'$$
$$\Gamma,\Gamma'\vdash o=o':T$$
%
the sequent $\Gamma\vdash$ is derivable. 
\end{lemma}
%



\begin{lemma}
\llabel{dertree1}
One has the following derivation rules:
%
\begin{enumerate}
\item $$\frac{\Gamma, x_1:T_1\vdash\spc \Gamma,\Gamma'\vdash}{\Gamma, x_1:T_1,\Gamma'\vdash}$$
\item $$\frac{\Gamma, x_1:T_1\vdash\spc \Gamma, \Gamma'\vdash o:T}{\Gamma, x_1:T_1,\Gamma'\vdash o:T}$$
\item $$\frac{\Gamma, x_1:T_1\vdash\spc \Gamma, \Gamma'\vdash T=T'}{\Gamma, x_1:T_1,\Gamma'\vdash T=T'}$$
\item $$\frac{\Gamma, x_1:T_1\vdash\spc \Gamma, \Gamma'\vdash o=o':T}{\Gamma, x_1:T_1,\Gamma'\vdash o=o':T}$$
\end{enumerate}
%
\end{lemma}
%
\begin{proof}
We prove that for any derivable sentence $St$ of one of the four main kinds which starts with $\Gamma$ the sentence obtained from $St$ by replacing $\Gamma$ with $\Gamma, x:T$ is derivable if $\Gamma, x:T\vdash$ itself is derivable. We proceed by induction on the derivation depth of $S$ relative to $\Gamma$. We now have to consider case by case each of the generating derivation rule families which produce a sentence of a main kind. Since $\Gamma, x:T\vdash$ is derivable we may assume that $\Gamma'$ is nonempty or that $S$ of the three later kinds. The verification is straightforward.
\end{proof}
%
\begin{remark}\rm
The key to the validity of the proof of Lemma \ref{dertree1} is that for any of the derivation rules one of the following possibilities holds:
%
\begin{enumerate}
\item the product sentence of the derivation rule is of the three later kinds and changing its context part $\Gamma$ with $\Gamma, x:T$ both in the  product and in the premises again produces a derivation rule,
\item the product sentence is of the first kind i.e. of the form $\Gamma\vdash$ where $\Gamma=\Gamma_1,\Gamma_2$ with $l(\Gamma_2)\le 1$ and replacing $\Gamma_1$ with $\Gamma_1, x:T$ both in the  product and in the premises again produces a derivation rule.
\end{enumerate}
%
These conditions would not hold if we had a generating derivation rule with the product of the form $\Gamma_1,\Gamma_2\vdash$ where $l(\Gamma_2)>1$ and $\Gamma_2$ does not directly appear in the premise e.g. a rule such as 
%
$$\frac{\Gamma\vdash\spc M}{\Gamma, x:\Eu_M, o:[El](x)\vdash}$$
%
or if we had a generating derivation rule with the product of one of the three later kinds of the form $\Gamma_0,\Gamma_1\vdash{\cal J}$ where $\Gamma_1$ is nonempty and does not directly appear in the premises e.g. a rule such as 
%
$$\frac{\Gamma\vdash f:[\prod;x](T_1,T_2)}{\Gamma, y:T_1\vdash [ev;x](f,y,T_2):T_2[y/x]}$$
%
\end{remark}






%
\begin{lemma}
\llabel{dertree2}
One has the following derivation rules:
%
\begin{enumerate}
\item $$\frac{\Gamma,\Gamma''\vdash\spc \Gamma,\Gamma'\vdash}{\Gamma,\Gamma',\Gamma''\vdash}$$
\item $$\frac{\Gamma,\Gamma''\vdash \spc \Gamma,\Gamma'\vdash a:T}{\Gamma,\Gamma',\Gamma''\vdash a:T}$$
\item $$\frac{\Gamma,\Gamma''\vdash \spc \Gamma,\Gamma'\vdash T=T'}{\Gamma,\Gamma',\Gamma''\vdash T=T'}$$
\item $$\frac{\Gamma,\Gamma''\vdash \spc \Gamma,\Gamma'\vdash o=o':T}{\Gamma,\Gamma',\Gamma''\vdash o=o':T}$$
\end{enumerate}
%
\end{lemma}
%
\begin{proof}
By induction on the length of $\Gamma''$ using Lemma \ref{dertree1}.
\end{proof}
%
\begin{lemma}
\llabel{dertree3}
One has the following derivation rules:
%
$$\frac{\Gamma\vdash a:S\spc \Gamma, x:S, \Gamma'\vdash}{\Gamma, \Gamma'[a/x]\vdash}$$
$$\frac{\Gamma\vdash a:S\spc \Gamma, x:S, \Gamma'\vdash o:T}{\Gamma, \Gamma'[a/x]\vdash o[a/x]:T[a/x]}$$
$$\frac{\Gamma\vdash a:S\spc \Gamma, x:S, \Gamma'\vdash T=T'}{\Gamma, \Gamma'[a/x]\vdash T[a/x]=T'[a/x]}$$
$$\frac{\Gamma\vdash a:S\spc \Gamma, x:S, \Gamma'\vdash o=o':T}{\Gamma, \Gamma'[a/x]\vdash o[a/x]=o'[a/x]:T[a/x]}$$
%
\end{lemma}
%
\begin{proof}
???
\end{proof} 
%
\begin{lemma}
\llabel{dertree4}
One has the following derivation rules:
%
$$\frac{\Gamma\vdash o:T}{\Gamma, x:T\vdash}$$
$$\frac{\Gamma\vdash T=T'}{\Gamma, x:T\vdash}$$
$$\frac{\Gamma\vdash o=o':T}{\Gamma\vdash o:T}$$
%
\end{lemma}
%
\begin{proof}
???
\end{proof}
%
Recall from \cite{NTP} that subsets in the sets of all contexts and  judgements in a given system of expressions form a type system i.e. define a contextual subcategory in the contextual category defined by the underlying system of expressions iff they satisfy the following conditions:
%
\begin{center}

$$\frac{}{\vdash}$$
$$\frac{x_1:E_1,\dots,x_{n}:E_{n}\vdash}{x_1:E_1,\dots,x_{n-i}:E_{n-i}\vdash} \,\,\,(i\le n) \,\,\,\,\,\,\,\,\,\, 
\frac{x_1:E_1,\dots,x_n:E_n\vdash t:T}{x_1:E_1,\dots,x_n:E_n, x:T\vdash} \,\,\,(n\ge 0)$$

$$\frac{x_1:E_1,\dots,x_n:E_n\vdash t:T\,\,\,\,\,\,\,x_1:E_1,\dots,x_i:E_i, y:F\vdash}{x_1:E_1,\dots,x_i:E_i, y:F, x_{i+1}:E_{i+1},\dots,x_n:E_n\vdash t:T},\,\,\,i=0,\dots,n$$

$$\frac{x_1:E_1,\dots,x_n:E_n\vdash t:T\,\,\,\,\,\,\,x_1:E_1,\dots,x_i:E_i\vdash r:E_{i+1}}
{x_1:E_1,\dots,x_i:E_i,x_{i+2}:E_{i+2}[r/x_{i+1}],\dots,x_n:E_n[r/x_{i+1}]\vdash t[r/x_{i+1}]:T[r/x_{i+1}]}$$
%
$$i=0,\dots,n-1$$

$$\frac{x_1:E_1,\dots,x_n:E_n\vdash}{x_1:E_1,\dots,x_n:E_n\vdash x_n:E_n}$$

\end{center}
%
Combining the lemmas proved above we get the following result.
%
\begin{theorem}
\llabel{mainth1}
For any given universe context $UC$ and a sequence of T-variables $FV$ the derivable sentences form a type system.
\end{theorem}
%
\begin{lemma}
\llabel{lm02a}
One has the following derivation rules in TS6:
%
\begin{enumerate}
\item $$\frac{\Gamma, x:T'\vdash\spc \Gamma, x:T, \Gamma'\vdash \spc T'\rd_{\AA} T}{\Gamma, x:T', \Gamma'\vdash}$$
\item $$\frac{\Gamma, x:T'\vdash\spc \Gamma, x:T, \Gamma'\vdash a:T'' \spc T'\rd_{\AA} T}{\Gamma, x:T', \Gamma'\vdash a:T''}$$
\end{enumerate}
%
\end{lemma}
%
\begin{proof}
By the induction on the derivation depth of $\Gamma, x:T, \Gamma'\vdash$ and $\Gamma, x:T, \Gamma'\vdash a:T''$ relative to $\Gamma, x:T\vdash$. If the derivation depth is $0$ then we are in the first case and the assertion is obvious. For the inductive step consider the derivation rules one by one. There are three cases to be considered for the first reduction rule. The other reduction rules are straightforward.
\end{proof}
%
\begin{lemma}
\llabel{lm02b}
One has the following derivation rules in TS6:
%
\begin{enumerate}
\item $$\frac{\Gamma, x:T'\vdash\spc \Gamma, x:T, \Gamma'\vdash \spc T\rd_{\AA} T'}{\Gamma, x:T', \Gamma'\vdash}$$
\item $$\frac{\Gamma, x:T'\vdash\spc \Gamma, x:T, \Gamma'\vdash a:T'' \spc T\rd_{\AA} T'}{\Gamma, x:T', \Gamma'\vdash a:T''}$$
\end{enumerate}
%
\end{lemma}
%
\begin{proof}
Same as for Lemma \ref{lm02a}.
\end{proof}
%
\begin{lemma}
\llabel{lm02c}
One has the following derivation rules in TS6:
%
\begin{enumerate}
\item $$\frac{\Gamma, x:T'\vdash\spc \Gamma, x:T, \Gamma'\vdash \spc T\equiv_{\AA} T'}{\Gamma, x:T', \Gamma'\vdash}$$
\item $$\frac{\Gamma, x:T'\vdash\spc \Gamma, x:T, \Gamma'\vdash a:T'' \spc T\equiv_{\AA} T'}{\Gamma, x:T', \Gamma'\vdash a:T''}$$
\end{enumerate}
%
\end{lemma}
%
\begin{proof}
Same as for Lemmas \ref{lm02a} and \ref{lm02b}.
\end{proof}








\begin{lemma}
\llabel{lm1}
Let $\Gamma, x:[El](o)\vdash$ be a derivable context.  Then there exists a u-level expression $M$ such that $\Gamma\vdash o :\Eu_M$ is derivable.
\end{lemma}
%
\begin{proof}
There is a unique derivation rule which produces contexts of the form $\Gamma, x:[El](o)\vdash$ and the premise of this rule is of the form $\Gamma\vdash o:\Eu_M$.
\end{proof}  
%
\begin{theorem}
\llabel{th1}
Let $\Gamma, x:T\vdash$ be a derivable context. Then there is a derivable context of the form $\Gamma, x:[El](o)\vdash$ such that $[El](o)\rde_{\AA} T$ and all the reductions involved are from the following list: Elforall, Eltotal, Elcoprod, Elpaths. 
\end{theorem}
%
\begin{proof}
By induction on the derivation depth of $\Gamma, x:T\vdash$ relative to $\Gamma$. Since $T$ is a T-term it has one of the following forms $[El](o)$, $[\prod;x](T_1,T_2)$, $[\sum;x](T_1,T_2)$, $[\amalg](T_1,T_2)$, $[Id](T, o_1,o_2)$. If $T=[El](o)$  we take $T'=T$. 

If $T=[\prod;x](T_1,T_2)$ then $\Gamma, x:T_1, y:T_2\vdash$ is derivable as the premise of the only derivation rule which generates $[\prod;x]$-terms. By Lemma \ref{lm00}(1), $\Gamma, x:T_1\vdash$ is also derivable. By induction there are derivable contexts $\Gamma, x:T_1, y:[El](o_2)\vdash$ and $\Gamma, x:[El](o_1)\vdash$ such that $[El](o_1)\rd_{\AA} T_1$ and $[El](o_2)\rd_{\AA} T_2$ through reductions from the list in the conditions of the theorem.  We then take $o=[forall_{M_1,M_2};x](o_1,o_2)$ and apply Lemma \ref{lm02a}. 

The cases of $[\sum;x]$ and $[\amalg](T_1,T_2)$ are similar to the case of $[\prod;x]$. Finally the case of $[Id]$ is similar with the use of Lemma \ref{lm00}(2) instead of Lemma \ref{lm00}(1).
\end{proof}
































\section{Abbreviations, conventions and definitions}
\llabel{abb0}
%
In order to make our definitions more readable we introduce the following conventions. We write them here in the context of TS0 terms but they will be applied in the same way to the terms of the other systems considered in this paper. 
%
\begin{enumerate} 
% 
\item Let $E\in TS0(Fu,FV,Fv)$ where $Fu (u_1,\dots,u_k)$, $FV=(X_1,\dots,X_m)$. Let $Fu'=(u'_1,\dots,u'_{k'})$, $FV'=(X'_1,\dots,X'_{m'})$ and $Fv'=(x'_1,\dots,x'_n)$. Let  $M_1,\dots,M_k$ be u-level expressions in variables from $Fu'$ and $T_1,\dots,T_m\in TT(Fu',FV',Fv)$. We will then write 
%
$$E\, M_1\dots M_k\,T_1\dots T_m$$ 
%
for 
%
$$E'=E[M_1/u_1,\dots,M_k/u_k,T_1/X_1,\dots,T_m/X_m]$$
%
considered as an element of $TS0(Fu',FV',Fv)$. 
%
\item  We will write $\prod x:T_1, T_2$ for $[\prod;x](T_1,T_2)$ and $\lambda x:T_1, o_1$ for $[\lambda;x](T_1,o_1)$. When $Y$ does not depend on $x$ we will write $X \sr Y$ for $\prod x:X, Y$. We will also write $\prod (x_1:T_1)\dots(x_n:T_n),T$ for 
%
$$\prod x_1:T_1,\prod x_2:T_2,\dots,\prod x_n:T_n,T$$
%
and $X_1\sr\dots\sr X_n$ for $X_1\sr (X_2\sr \dots ( X_{n-1}\sr X_n)\dots )$. 
%
\item We will write $*t$ for $[El](t)$
%
\item Let $\Gamma$ be a context. We will write $f a$ for $[ev;x](f,a,T_2)$ if $\tau_{\Gamma}(f)=\prod x:T_1, T_2$. Note that $=$ here means the equality of expressions (up to the $\alpha$-equivalence). In particular $T_2$ is well defined (again up to the $\alpha$-equivalence) by this condition as the second branch of $\tau_{\Gamma}(f)$. 
%
\item We will write:
%
$$Def.\spc D(u_1,\dots,u_k;{\AA})(X_1,\dots,X_m:Type)(x_1:T_1)\dots(x_n:T_n):=T$$
%
where $D$ is a name (identifier) and $T\in TT0(Fu,\{X_1,\dots,X_m\},\{x_1,\dots,x_n\})$ to signify the assertion that the context
%
$$x_1:T_1,\dots,x_n:T_n,x:T\vdash$$
%
is derivable in TS0 relative to the universe context $(u_1,\dots,u_k;{\AA})$ and the sequence of T-variables $(X_1,\dots,X_m)$ and that we will use $D$ as a notation for the term $T$.  

???Proofs of such assertions should be provided where necessary wince they will form the basis for our annotation language.

%
\item We will write:
%
$$Def.\spc D(u_1,\dots,u_k;{\AA})(X_1,\dots,X_m:Type)(x_1:T_1)\dots(x_n:T_n):=o:T$$
%
where $D$ is a name (identifier) and 
%
$$T\in TT0(\{u_1,\dots,u_k\},\{X_1,\dots,X_m\},\{x_1,\dots,x_n\})$$
$$o\in TT0(\{u_1,\dots,u_k\},\{X_1,\dots,X_m\},\{x_1,\dots,x_n\})$$
%
to signify the assertion that the judgement
%
$$x_1:T_1,\dots,x_n:T_n\vdash o:T$$
%
is derivable in TS0 relative to the universe context $(u_1,\dots,u_k;{\AA})$ and the sequence of T-variables $(X_1,\dots,X_m)$ and that we will use $D$ as the notation for the term $\lambda (x_1:T_1)\dots (x_n:T_n) o$. 

??? Note on proofs of such assertions in the annotation language.

Similarly we will write
%
$$Def.\spc D (u_1,\dots,u_k;{\AA})(X_1,\dots,X_m:Type)(x_1:T_1)\dots(x_n:T_n):=o$$
%
for
%
$$Def.\spc D (u_1,\dots,u_k;{\AA})(X_1,\dots,X_m:Type)(x_1:T_1)\dots(x_n:T_n):=o:\tau_{\Gamma}(o)$$
%
where $\Gamma=(x_1:T_1,\dots,x_n:T_n)$. 
%
\item We will write
%
$$Th.\spc D (u_1,\dots,u_k;{\AA})(X_1,\dots,X_m:Type)(x_1:T_1)\dots(x_n:T_n):T$$
%
where $D$ is a name (identifier) and 
%
$$T\in TT0(Fu,\{X_1,\dots,X_m\},\{x_1,\dots,x_n\})$$
$$o\in TT0(Fu,\{X_1,\dots,X_m\},\{x_1,\dots,x_n\})$$
%
To signify that there is a derivable judgement of the form 
%
$$x_1:T_1,\dots,x_n:T_n\vdash o:T$$
%
in TS0 relative to to the universe context $(u_1,\dots,u_k;{\AA})$ and the sequence of T-variables $(X_1,\dots,X_m)$ and that we will use $D$ as the notation for $o$. 

???? Unlike $Def.$ which is verified mechanically $Th.$ requires a proof i.e. an actual construction of $o$. We will nevertheless use this notation below without providing an explicit form of $o$ in some cases when we know that such an $o$ can be constructed from existing Coq proofs but writing it explicitly would take to much space. 


%
\item We will use $\{\dots\}$ instead of $(\dots)$ for arguments of definitions which can be uniquely reconstructed under the assumption that the definition produces a derivable context or judgement. Such arguments need not be specified in definition "applications". We will also use obvious abbreviations of the notations introduced above in cases when $k,m$ or $n$ equals $0$ or when ${\AA}$ is an empty set of conditions.  
\end{enumerate} 
%






\comment{
\subsection{Criterion of derivability for TS0 contexts and judgements}
%
In this section we provide a conjectural algorithm which determines whether a given context or judgement is derivable in a given universe context $UC=(Fu,{\AA})$ where ${\AA}\ne \emptyset$. We formulate this algorithm as a pre-theorem which provides the necessary and sufficient conditions of derivability in the form which is easily converted into a recursive algorithm.
%
\begin{pretheorem}
\llabel{alg0}
Let $UC=(Fu,{\AA})$ be a universe context such that ${\AA}\ne \emptyset$. Then one has:
%
\begin{enumerate}
\item A context $\Gamma=(x_1:E_1,\dots,x_n:E_n)$ is derivable (in $UC$) if and only if one has:
%
\begin{enumerate}
\item The context $\Gamma'=(x_1:E_1,\dots,x_{n-1}:E_{n-1})$ is derivable in $UC$.
\item One of the following holds:
%
\begin{enumerate}
\item $E_n=[El](o)$ where $\Gamma'\vdash s:\tau_{\Gamma'}(o)$ is derivable and the normal form of $\tau_{\Gamma'}(o)$ is of the form $\Eu_M$ for some $M$. 
\item $E_n=[\prod;x](T_1,T_2)$ where $\Gamma', x:T_1, y:T_2\vdash$ is derivable.
\end{enumerate}
\end{enumerate}
%
\item A judgement $\Gamma\vdash o : T$ is derivable (in $UC$) if and only if one has:
%
\begin{enumerate}
\item The context $\Gamma, x:T\vdash$ is derivable.
\item One of the following conditions holds:
%
\begin{enumerate}
\item $N(o)=[x_i]$ where $x_i:E_i$ is one of the variables declared in $\Gamma$ and $T=_{\AA} E_i$,
\item $N(o)=[\cu_M]$ and $T=_{\AA} \Eu_{M+1}$,
\item $N(o)=[j_{M_1,M_2}]$ where for all $\vec{n}\in {\AA}$ one has $M_1(\vec{n})\le M_2(\vec{n})$ and $T=_{\AA} [\prod;x](\Eu_{M_1},\Eu_{M_2})$,
\item $N(o)=[ev;x](o_1,o_2,T')$ where $\Gamma\vdash o_1:[\prod;x](\tau_{\Gamma}(o_2),T')$ and $\Gamma\vdash o_2:\tau_{\Gamma}(o_2)$ are derivable and $T=_{\AA} T'[o_2/x]$.
\item $N(o)=[\lambda;x](T',o)$ where $\Gamma, x:T'\vdash o:\tau_{\Gamma, x:T'}(o)$ is derivable and $T=_{\AA} [\prod;x](T',\tau_{\Gamma, x:T'}(o))$.
\item $N(o)=[forall_{M_1,M_2};x][o_1,o_2]$ where $\Gamma\vdash o:\Eu_{M_1}$ and $\Gamma, x:[El](o_1)\vdash o_2:\Eu_{M_2}$ are derivable and $T=_{\AA} \Eu_{max(M_1,M_2)}$.
\end{enumerate}
\end{enumerate}
\end{enumerate}
%
\end{pretheorem}
%

}
















\subsection{Reducibility relation on TS0 terms}
%
%
\begin{definition}
\llabel{drd0}
Let $UC=(Fu,{\AA})$ be universe context and $FV$ a sequence of T-variables. Define a relation $\rd_{\AA}$ on $TS0(Fu,FV,Fv)$ for each $Fv$ as the transitive closure of the union of the following reduction relations:
%
\begin{enumerate}
\item Elu-reduction. An essential subterm of the form $[El][\cu_M]$ reduces to $\Eu_M$. 
\item Elj-reduction. An essential  subterm of the form $[El][ev;y]([j_{M_1,M_2}], o, T)$ reduces to $[El](o)$, 
%
\item Elforall-reduction. An essential subterm of the form  $[El][forall_{M_1,M_2};x](o_1,o_2)$  reduces to $[\prod;x]([El](o_1),[El](o_2))$,
%
\item jMM-reduction. An essential subterm of the form  $[j_{M_1,M_2}]$ such that $M_1\equiv_{{\AA}} M_2$, reduces to $[\lambda;x](\Eu_{M_1},[x])$ where $x$ is a new, relative to the whole term, name of a variable,
%
\item beta-reduction. An essential subterm of the form $[ev;z]([\lambda;x](T_1,o_1),o_2,T_2)$ reduces to $o_1[o_2/x]$,
%
\item jj-reduction. An essential subterm of the form  $[ev;z]([j_{M_2',M_3}], [ev;y]([j_{M_1,M_2}], o_1, T_1), T_2)$ such that $M_2'\equiv_{\AA} M_2$ reduces to $[ev;z]([j_{M_1,M_3}], o_1, T_2)$,
%
%
\item eta-reduction. An essential subterm of the form $[\lambda;x](X, [ev;y](f,[x],Y))$ where $f$ does not depend on $x$ reduces to $f$.
%
\item forallj-reductions: 
\begin{enumerate}
\item forallja-reduction. An essential subterm of the form 
%
$$[forall_{M_1,M_2};x]([ev;z]([j_{M_0,M_1'}], o_1, T), o_2)$$
%
such that $M_1'\equiv_{\AA} M_1$, reduces to 
%
$$[ev;z]([j_{max(M_0,M_2), max(M_1,M_2)}], [forall_{M_0,M_2};x](o_1,o_2), \Eu_{max(M_1,M_2)})$$
%
\item foralljb-reduction. An essential subterm of the form 
%
$$[forall_{M_1,M_3};x](o_1, [ev;z]([j_{M_2,M_3'}], o_2, T) )$$
%
such that  $M_3'\equiv_{\AA} M_3$ reduces to
%
$$[ev;z]([j_{max(M_1,M_2),max(M_1,M_3)}], [forall_{M_1,M_2};x](o_1,o_2), \Eu_{max(M_1,M_3)})$$
%
\end{enumerate}
%
\end{enumerate}
\end{definition}
%
\begin{remark}\rm
One verifies easily that a reduction of a TS0-term is again a TS0-term and that reductions preserve the subsets of T-terms and o-terms.
\end{remark}
%
Let $\rde_{\AA}$ be the transitive and reflexive closure of $\rd_{\AA}$. 
%
\begin{lemma}
\llabel{redsub01}
In the notations used above let $E,E'\in TS0(Fu,FV,Fv)$ and $E\rd_{\AA} E'$ then one has:
%
\begin{enumerate}
\item for $x\in Fv$ and $s\in oT0(Fu,FV,Fv)$ one has $E[s/x]\rd_{\AA} E'[s/x]$,
\item for $X\in FV$ and $T\in TT0(Fu,FV,Fv)$ one has $E[T/X]\rd_{\AA} E'[T/X]$.
\end{enumerate} 
\end{lemma}
%
\begin{proof}
It is sufficient to consider one step reductions. Of all reductions of Definition \ref{drd0} the only non-trivial case is that of the beta-reduction. It follows from Lemma \ref{sublemma}. 
\end{proof}
%
\begin{lemma}
\llabel{redsub02}
Let $E$ be an term of the form $E=[L](B_1,\dots,B_n)$ and suppose that $B_i$ are essential if and only if $i\in I$. Suppose further that for each $i\in I$ one has $B_i\rde_{\AA} B_i'$ and let $B_i'=B_i$ for $i\notin I$. Then $E\rde_{\AA} [L](B_1',\dots,B_n')$.
\end{lemma}
%
\begin{proof}
Straightforward.
\end{proof}
%
In the following lemma we let $E[s'/x]_{ess}[s/x]_{ness}$ denote the expression obtained by the substitution of $s'$ for all essential occurrences of $x$ and $s$ for all non-essential occurrences of $x$ and use the notation for the substitutions of T-variables.
%
\begin{lemma}
\llabel{redsub03}
In the notations used above let $E\in TS0(Fu,FV,Fv)$ then one has:
%
\begin{enumerate}
\item Let $s,s'\in oT0(Fu,FV,Fv)$ such that $s\rd_{\AA} s'$ and $x\in Fv$, then 
%
$$E[s/x]\rde_{\AA} E[s'/x]_{ess}[s/x]_{ness}$$
%
\item Let $T,T'\in TT0(Fu,FV,Fv)$ such that $T\rd_{\AA} T'$ and $X\in FV$, then 
%
$$E[T/X]\rde_{\AA} E[T'/x]_{ess}[T/x]_{ness}$$
%
\end{enumerate}
\end{lemma}
%
\begin{proof}
Straightforward by induction on the number of nodes in $E$ using Lemma \ref{redsub02}.   
\end{proof}
%
\begin{lemma}
\llabel{lequivsimred0}
In the notations used above let $E\rde_{\AA} E'$ and $F\equiv_{\AA} E$ (resp. $F\sim_{\AA} E$). Then there is an term $F'$ such that $F\rde_{\AA} F'$ and $F'\equiv_{\AA} E'$ (resp. $F'\sim_{\AA} E'$).
\end{lemma}
%
\begin{proof}
It follows easily from the fact that all our reducibility conditions are invariant under both $\equiv_{\AA}$ and $\sim_{\AA}$.
\end{proof}
%
\begin{remark}\rm
Note that the analog of Lemma \ref{lequivsimred0} with $F'\equiv_{\AA} E'$ does not hold. Indeed, in the case of $\beta$-reduction the substitution may produce a term with many copies of the same u-level expression and replacing some but not all of these copies by an equivalent u-level expression may produce $F'$ which can not be obtained by reduction of any $F$. 
\end{remark}
%






\subsection{Local confluence for general terms of TS0}
%

The following theorem asserts "local" confluence for one step reductions except for one special case. The confluence in this special case is expected to hold for derivable terms (see below).  

%
\begin{theorem}
\llabel{lc0}
Let $UC=(Fu,{\AA})$ be a universe context and $FV$ a sequence of T-variables. Let $E\in TS0(Fu,FV,Fv)$. Let further $E \rd_{\AA} E_1$ and $E\rd_{\AA} E_2$ be two one-step reductions. Then there exists a TS0-terms $E'_1$, $E_2'$ from $TS0(Fu,FV,Fv)$ such that $E_1\rde_{\AA} E_1'$, $E_2\rde_{\AA} E_2'$ and $E_1'\sim_{\AA} E_2'$ unless $E_1$ is obtained by eta-reduction of a subterm of the form $[\lambda;x](T_1,[ev;y]([\lambda;z](T_2,o),[x],T_3))$ to $[\lambda;z](T_2,o)$ and $E_2$ is obtained by beta-reduction of this subterm at the node $[ev;y]$ to $[\lambda;x](T_1,o[x/z])$. In this cases confluence is expected for derivable terms (see below). 
\end{theorem}
%
\begin{proof}
It is sufficient to consider the case when the first reduction is relative to subterm $S=E$ i.e. occurs at the root. 
%
\begin{enumerate}
\item Elu-reduction at the root. $E=[El][\cu_M]$. Then no other reductions may occur in $E$ and therefore there are no confluence issues.  
\item Elj-reduction at the root. $E=[El][ev;y]([j_{M_1,M_2}], o, T)$ and 
%
$$E_1=[El](o).$$
%
If the second reduction occurs inside $o$ or $T$ then the statement is obvious. It remains to consider possible second reductions occurring at the "exposed" nodes $[El]$, $[ev;y]$ and $[j_{M_1,M_2}]$. This leads to the following actual cases:
%
\begin{enumerate}
%
\item jMM-reduction at $[j_{M_1,M_2}]$. Then $M_1\equiv_{\AA} M_2$, 
%
$$E_1=[El](o)=E_1'$$
$$E_2=[El][ev;y]([\lambda;x](\Eu_{M_1},[x]), o, T)\rd [El](o)=E_2'$$
%
\item jj-reduction at $[ev;y]$. Then $o=[ev;z]([j_{M_0,M_1'}],o',T')$ where $M_1'\equiv_{\AA} M_1$  and
%
$$E_1=[El][ev;z]([j_{M_0,M_1'}],o', T')\rd [El](o')=E_1'$$
$$E_2=[El][ev;y]([j_{M_0,M_2}],o', T)\rd [El](o')=E_2'$$
%
\end{enumerate}
%
\item Elforall-reduction at the root. $E=[El][forall_{M_1,M_2};x](o_1,o_2)$ and 
%
$$E_1=[\prod;x]([El](o_1),[El](o_2)).$$
%
Exposed nodes where second reduction may occur are $[El]$ and $[forall_{M_1,M_2};x]$ with the following actual cases:
%
\begin{enumerate}
\item forallja-reduction at $[forall_{M_1,M_2};x]$. Then $o_1=[ev;z]([j_{M_0,M_1'}], o_1',T')$ where $M_1'\equiv_{\AA} M_1$ and
%
$$E_1= [\prod;x]([El][ev;z]([j_{M_0,M_1'}], o_1',T'),[El](o_2))\rd$$
$$ [\prod;x]([El](o_1'),[El](o_2))=E_1'$$
$$E_2= [El][ev;z]([j_{max(M_0,M_2),max(M_1,M_2)}], [forall_{M_0,M_2};x](o_1',o_2), \Eu_{max(M_1,M_2)}) \rd$$ 
$$[El][forall_{M_0,M_2};x](o_1',o_2) \rd [\prod;x]([El](o_1'), [El](o_2))=E_2'$$
%
\item foralljb-reduction at $[forall_{M_1,M_2};x]$. Then $o_2=[ev;z](j_{M_3,M_2'},o_2',T')$ where $M_2'\equiv_{\AA} M_2$ and 
%
$$E_1=[\prod;x]([El](o_1),[El][ev;z](j_{M_3,M_2'},o_2',T'))\rd$$
$$[\prod;x]([El](o_1),[El](o_2'))=E_1'$$
$$E_2= [El][ev;z]([j_{max(M_1,M_3),max(M_1,M_2)}], [forall_{M_1,M_3};x](o_1,o_2'), \Eu_{max(M_1,M_2)})\rd $$
$$[El][forall_{M_1,M_3};x](o_1,o_2') \rd [\prod;x]([El](o_1),[El](o_2'))=E_2'$$
%
\end{enumerate}
%
\item jMM-reduction at the root. $E=[j_{M_1,M_2}]$ such that $M_1\equiv_{\AA} M_2$ and
%
$$E_1=[\lambda;x](\Eu_{M_1},[x])$$ 
%
There are exposed nodes where second reduction may occur. 
%
\item beta-reduction at the root. $E=[ev;z]([\lambda;x](T_1,o_1),o_2,T_2)$ and 
%
$$E_1=o_1[o_2/x].$$
%
Exposed nodes where second reduction may occur  are $[ev;z]$ and $[\lambda;x]$ with the only actual case of the eta-reduction at $[\lambda;x](X,Y)$. Then $Y=[ev;y](o,[x],T)$ where $o$ does not depend on $x$ and
%
$$E_1=[ev;y](o,o_2,T[o_2/x])=E_1'$$
$$E_2=[ev;z](o,o_2,T_2)=E_2'$$
%
\item jj-reduction at the root. $E=[ev;z]([j_{M_2',M_3}], [ev;y]([j_{M_1,M_2}], o, T), T')$ such that $M_2'\equiv_{\AA} M_2$ and
%
$$E_1=[ev;z]([j_{M_1,M_3}], o, T')$$
%
Exposed nodes where second reduction may occur  are $[ev;z]$, $[j_{M_2',M_3}]$, $[ev;y]$ and $[j_{M_1,M_2}] $ with the following actual cases:
%
\begin{enumerate}
\item jMM-reduction at $[j_{M_2',M_3}] $. Then $M_2'\equiv_{\AA} M_3$ and
%
$$E_1=[ev;z]([j_{M_1,M_3}], o, T')=E_1'$$
$$E_2=[ev;z]([\lambda;x](\Eu_{M_2'},[x]), [ev;y]([j_{M_1,M_2}], o, T), T')\rd$$
$$[ev;y]([j_{M_1,M_2}], o, T)=E_2'$$
%
\item jj-reduction at $[ev;y]$. Then $o=[ev;t]([j_{M_0,M_1'}], o', T)$ where $M_1'\equiv_{\AA} M_1$ and 
%
$$E_1=[ev;z]([j_{M_1,M_3}], [ev;t]([j_{M_0,M_1'}], o', T), T')\rd $$
$$[ev;z]([j_{M_0,M_3}],o', T')=E_1'$$
$$E_2=[ev;z]([j_{M_2',M_3}], [ev;y]([j_{M_0,M_2}], o', T), T')\rd $$
$$ [ev;z]([j_{M_0,M_3}], o', T')=E_2'$$
%
\item jMM-reduction at $[j_{M_1,M_2}] $. Then $M_1\equiv_{\AA} M_2$ and
%
$$E_1=[ev;z]([j_{M_1,M_3}], o, T)=E_1'$$
$$E_2=[ev;z]([j_{M_2',M_3}], [ev;y]([\lambda;x](\Eu_{M_1},[x]), o, T'), T)\rd$$
$$[ev;z]([j_{M_2',M_3}], o ,T)=E_2'$$
%
\end{enumerate}
%
\item eta-reduction at the root. $E=[\lambda;x](T_1, [ev;y](o ,[x], T_2))$ such that $o$ does not depend on $x$ and 
%
$$E_1=o$$
%
Exposed nodes where second reduction may occur  are $[\lambda;x]$ and $[ev;y]$ with the only actual case being beta-reduction at $[ev;y]$. This is the exceptional case from the condition of the theorem.
%
\item forallj-reductions at the root:
\begin{enumerate}
\item forallja-reduction at the root. $E=[forall_{M_1,M_2};x]([ev;z]([j_{M_0,M_1'}], o_1, T), o_2)$ such that $M_1'\equiv_{\AA} M_1$ and
%
$$E_1=[ev;z]([j_{max(M_0,M_2), max(M_1,M_2)}], [forall_{M_0,M_2};x](o_1,o_2), \Eu_{max(M_1,M_2)})$$
%
Exposed nodes where second reduction may occur  are $[forall_{M_1,M_2};x]$, $[ev;z]$ and $[j_{M_0,M_1'}]$ with the following actual cases:
%
\begin{enumerate}
\item foralljb-reduction at $[forall_{M_1,M_2};x]$. Then $o_2=[ev;z']([j_{M_3,M_2'}], o_2', T')$ where $M_2'\equiv_{\AA} M_2$ and 
%
$$E_1=[ev;z]([j_{max(M_0,M_2), max(M_1,M_2)}], $$
$$[forall_{M_0,M_2};x](o_1, [ev;z']([j_{M_3,M_2'}], o_2', T')), \Eu_{max(M_1,M_2)})\rd$$
$$[ev;z]([j_{max(M_0,M_2), max(M_1,M_2)}], $$
$$ [ev;z']([j_{max(M_0,M_3),max(M_0,M_2')}], [forall_{M_0,M_3};x](o_1,o_2'), \Eu_{max(M_0,M_2')}),$$
$$ \Eu_{max(M_1,M_2)} )\rd$$
$$[ev;z]([j_{max(M_0,M_3),max(M_1,M_2)}], [forall_{M_0,M_3};x](o_1,o_2'), \Eu_{max(M_1,M_2)})=E_1'$$
%
$$E_2=[ev;z']([j_{max(M_1,M_3), max(M_1,M_2)}], $$
$$ [forall_{M_1,M_3};x]([ev;z]([j_{M_0,M_1'}], o_1, T), o_2'), \Eu_{max(M_1,M_2)})\rd$$
$$[ev;z']([j_{max(M_1,M_3), max(M_1,M_2)}], $$
$$ [ev;z]([j_{max(M_0,M_3),max(M_1,M_3)}], [forall_{M_0,M_3};x](o_1,o_2'), \Eu_{max(M_1,M_3)}) ,$$
$$ \Eu_{max(M_1,M_2)})\rd$$
$$[ev;z']([j_{max(M_0,M_3),max(M_1,M_2)}], [forall_{M_0,M_3};x](o_1,o_2'), \Eu_{max(M_1,M_2)})=E_2'$$
%
\item jj-reduction at $[ev;z]$. Then $o_1=[ev;z']([j_{M_3,M_0'}],o_1',T')$ where $M_0'\equiv_{\AA} M_0$  and 
%
$$E_1=[ev;z]([j_{max(M_0,M_2), max(M_1,M_2)}],$$
$$ [forall_{M_0,M_2};x]( [ev;z']([j_{M_3,M_0'}], o_1', T'), o_2), \Eu_{max(M_1,M_2)})\rd$$
$$[ev;z]([j_{max(M_0,M_2), max(M_1,M_2)}], $$
$$ [ev;z']([j_{max(M_3,M_2),max(M_0,M_2)}], [forall_{M_3,M_2};x](o_1',o_2), \Eu_{max(M_0,M_2)}), $$
$$ \Eu_{max(M_1,M_2)})\rd$$
$$[ev;z]([j_{max(M_3,M_2),max(M_1,M_2)}], [forall_{M_3,M_2};x](o_1',o_2), \Eu_{max(M_1,M_2)})=E_1'$$
%
$$E_2=[forall_{M_1,M_2};x]([ev;z]([j_{M_3,M_1'}], o_1', T), o_2)\rd$$
$$[ev;z]([j_{max(M_3,M_2), max(M_1,M_2)}], [forall_{M_3,M_2};x](o_1',o_2), \Eu_{max(M_1,M_2)})=E_2'$$
%
\item jMM-reduction at $[j_{M_0,M_1'}]$. Then $M_0\equiv_{\AA} M_1'$ and 
%
$$E_1=[ev;z]([j_{max(M_0,M_2), max(M_1,M_2)}], [forall_{M_0,M_2};x](o_1,o_2), \Eu_{max(M_1,M_2)})\rd$$
$$[ev;z]([\lambda;x](\Eu_{max(M_0,M_2)},[x]), [forall_{M_0,M_2};x](o_1,o_2), \Eu_{max(M_1,M_2)})\rd$$
$$[forall_{M_0,M_2};x](o_1,o_2)=E_1'$$
%
$$E_2=[forall_{M_1,M_2};x]([ev;x]([\lambda;x](\Eu_{M_0},[x]), o_1, T), o_2)\rd$$
$$[forall_{M_1,M_2};x](o_1,o_2)=E_2'$$
\end{enumerate}




%
\item foralljb-reduction at the root. $E=[forall_{M_1,M_3};x](o_1, [ev;z]([j_{M_2,M_3'}], o_2, T) )$ such that $M_3'\equiv_{\AA} M_3$ and
%
$$E_1=[ev;z]([j_{max(M_1,M_2),max(M_1,M_3)}], [forall_{M_1,M_2};x](o_1,o_2), \Eu_{max(M_1,M_3)}),$$
%
Exposed nodes where second reduction may occur are $[forall_{M_1,M_3};x]$, $[ev;z]$ and $[j_{M_2,M_3''}]$ with the following actual cases:
%
\begin{enumerate}
\item forallja-reduction at $[forall_{M_1,M_3};x]$. Then $o_1=[ev;z']([j_{M_0,M_1'}], o_1', T')$ where $M_1'\equiv_{\AA} M_1$ and 
%
$$E_1=[ev;z]([j_{max(M_1,M_2), max(M_1,M_3)}], $$
$$[forall_{M_1,M_2};x]([ev;z']([j_{M_0,M_1'}], o_1', T'), o_2), \Eu_{max(M_1,M_3)})\rd$$
$$[ev;z]([j_{max(M_1,M_2), max(M_1,M_3)}], $$
$$ [ev;z']([j_{max(M_0,M_2),max(M_1,M_2)}], [forall_{M_0,M_2};x](o_1',o_2), \Eu_{max(M_0,M_2)}),$$
$$ \Eu_{max(M_1,M_3)})\rd$$
$$[ev;z]([j_{max(M_0,M_2),max(M_1,M_3)}], [forall_{M_0,M_2};x](o_1',o_2), \Eu_{max(M_1,M_3)} )=E_1'$$
%
$$E_2=[ev;z']([j_{max(M_0,M_3), max(M_1,M_3)}], $$
$$ [forall_{M_0,M_3};x](o_1', [ev;z]([j_{M_2,M_3'}], o_2, T), \Eu_{max(M_1,M_3)})\rd$$
$$[ev;z']([j_{max(M_0,M_3), max(M_1,M_3)}], $$
$$ [ev;z]([j_{max(M_0,M_2),max(M_0,M_3)}], [forall_{M_0,M_2};x](o_1',o_2), \Eu_{max(M_0,M_3)}) ,$$
$$ \Eu_{max(M_1,M_3)})\rd$$
$$[ev;z']([j_{max(M_0,M_2),max(M_1,M_3)}], [forall_{M_0,M_2};x](o_1',o_2), \Eu_{max(M_1,M_3)})=E_2'$$
%
\item jj-reduction at $[ev;z]$. Then $o_2=[ev;z']([j_{M_0,M_2'}],o_2',T')$ where $M_2'\equiv_{\AA} M_2$ and 
%
$$E_1=[ev;z]([j_{max(M_1,M_2), max(M_1,M_3)}],$$
$$ [forall_{M_1,M_2};x]( o_1 ,[ev;z']([j_{M_0,M_2'}],o_2',T') ), \Eu_{max(M_1,M_3)})\rd$$
$$[ev;z]([j_{max(M_1,M_2), max(M_1,M_3)}], $$
$$ [ev;z']([j_{max(M_1,M_0),max(M_1,M_2)}], [forall_{M_1,M_0};x](o_1,o_2'), \Eu_{max(M_1,M_2)}), $$
$$ \Eu_{max(M_1,M_3)})\rd$$
$$[ev;z]([j_{max(M_1,M_0),max(M_1,M_3)}], [forall_{M_1,M_0};x](o_1,o_2'), \Eu_{max(M_1,M_3)})=E_1'$$
%
$$E_2=[forall_{M_1,M_3};x](o_1, [ev;z]([j_{M_0,M_3'}], o_1', T))\rd$$
$$[ev;z]([j_{max(M_1,M_0), max(M_1,M_3)}], [forall_{M_1,M_0};x](o_1,o_2'), \Eu_{max(M_1,M_3)})=E_2'$$
%
\item jMM-reduction at $[j_{M_2,M_3'}]$. Then $M_2\equiv_{\AA} M_3'$ and 
%
$$E_1=[ev;z]([j_{max(M_1,M_2), max(M_1,M_3)}], [forall_{M_1,M_2};x](o_1,o_2), \Eu_{max(M_1,M_3)})\rd$$
$$[ev;z]([\lambda;x](\Eu_{max(M_1,M_2)},[x]), [forall_{M_1,M_2};x](o_1,o_2), \Eu_{max(M_1,M_3)})\rd$$
$$[forall_{M_1,M_2};x](o_1,o_2)=E_1'$$
%
$$E_2=[forall_{M_1,M_3};x](o_1, [ev;x]([\lambda;x](\Eu_{M_2},[x]), o_2, T))\rd$$
$$[forall_{M_1,M_3};x](o_1,o_2)=E_2'$$
\end{enumerate}
\end{enumerate}
\end{enumerate}
\end{proof}


%??? say something about:
%
\comment{


$$\frac{\Gamma\vdash o:T\spc \Gamma, x:T'\vdash\spc T\rd_{\AA} T'}{\Gamma\vdash o:T'} \spc \frac{\Gamma\vdash o:T\spc \Gamma, x:T'\vdash\spc T'\rd_{\AA} T}{\Gamma\vdash o:T'}$$


}



\newpage





\section{Adding the unit $pt$ - system TS2}
%

\subsection{TS2 terms and typing function}

\begin{definition}
\llabel{d21}
The following labels are permitted in the expressions of TS2 - the labels permitted in TS1, $pt$ and $(pt_r;x)$
\end{definition}
%
The notions of u-level expressions, T- and o- terms in TS2 are defined as follows:
%
\begin{definition}
\llabel{d22}
\begin{enumerate}
\item expressions with the root node caring a TS1-label is an u-level expression, o-expression or a T-expression according to the rules of Definition \ref{d13},
\item expressions with the root of the form $[pt]$ or $[pt_r;x]$ are o-expressions.
\end{enumerate}
\end{definition}
%
%
\begin{definition}
\llabel{d23}
A TS2-term is a TS2-expression such that:
%
\begin{enumerate}
\item any node caring one of the TS1-labels satisfies the conditions of Definition \ref{d13},
\item any node of the form $[pt]$ has valency $0$, 
\item any node of the form $[pt_r;x]$ has valency $2$, its first branch is an o-expression which does not contain $[x]$ and its second branch is a T-expression. 
\end{enumerate}
\end{definition}
%
\begin{definition}
\llabel{d24}
A node in TS2 term is called non-essential if it satisfies the conditions of Definition \ref{d14}. The same applies to the definition of essential nodes, essential and non-essential subexpressions and of $Ess(E)$ is extended to TS2-terms in the obvious way. 
\end{definition}
%
We let $TS2$ denote the set of TS2-terms and $TT2$ and $oT2$ denote the subsets of T-terms and o-terms.
The obvious analog of Lemma \ref{l02} holds for TS1-expressions. We extend to TS2 the abbreviations introduced for TS1-expressions and also abbreviate $[El][pt]$ as $[Pt]$. 
%
\begin{definition}
\llabel{dtau2}
Under the assumptions of Definition \ref{dtau0} we extend the typing function $\tau_{\Gamma}$ to o-terms of TS2 as follows:
%
\begin{enumerate}
\item the value of $\tau_{\Gamma}$ on an o-term whose root node carries a TS1-label is computed according to the rules of Definition \ref{dtau1}.
\item $\tau_{\Gamma}([pt])=\Eu_0$,
\item $\tau_{\Gamma}([pt_r;x](o,T))=[\prod;x](Pt,T)$.
\end{enumerate}
\end{definition}
%
We have the obvious analog of Proposition \ref{tausub0} for TS2.
%
\begin{remark}
\rm\llabel{unitpos}
The obvious idea to introduce $pt$ not through the eliminators $[pt_{r,M}]$ but by the condition that $Pt$ has one distinguished term $tt$ and any other term $a\ne tt$ reduces to $tt$ leads to a system without confluence since 
%
$$[pair;x]([pr1;y](Pt,T,c),[pr2;y](Pt,c,T),T[x/y])$$
%
reduces both to $c$ and to $[pair;x](tt, [pr2;y](Pt,c,T),T[x/y])$ and these two terms can not be reduced to a common term (cf. \cite{Lambek}[Exercise p.88]). Of the other reductions which are supported by the univalent model namely:
%
$$[\prod;x](Pt,T)\rd_{\AA} T\spc [\prod;x](T,Pt)\rd_{\AA} Pt$$
$$[\sum;x](Pt,T)\rd_{\AA} T\spc [\sum;x](T,Pt)\rd_{\AA} T$$
%
the first two lead to  derivable terms whose types are changed by $\beta$-reduction:
%
\begin{enumerate}
\item $o=[ev;x]([\lambda;y](Pt,o_1),o_2,T_2)\rd o_1[o_2/y]=o'$ where $o_1:[\prod;x](T_1,T_2)$, $o_2:T_1$ and $\tau_{\Gamma}(o)=T_2[o_2/x]$, $\tau_{\Gamma}(o')=[\prod;x](T_1,T_2)$.
\item $o=[ev;x]([\lambda;y](T_1,o_1),o_2,Pt)\rd o_1[o_2/y]=o'$ where $o_1:T_2$, $o_2:[\prod;y](T_1,T_2)$ and $\tau_{\Gamma}(o)=Pt$, $\tau_{\Gamma}(o')=T_2[o_2/y]$. 
\end{enumerate}
%
and the other two seem to lead to similar problems with sum-related reductions.
%???
\end{remark}


\subsection{Equivalence relations $\equiv_{\AA}$ and $\sim_{\AA}$ on TS2-terms}
%
The relations $\equiv_{\AA}$ and $\sim_{\AA}$ are extended to TS2-terms in the obvious way. We also have obvious analogs of all the statements of Section \ref{sim0}.



\subsection{Reducibility relation on TS2 terms}
%

\begin{definition}
\llabel{drd2}
Let $UC=(Fu,{\AA})$ be universe context and $FV$ a sequence of T-variables. Define a relation $\rd_{\AA}$ on $TS2(Fu,FV,Fv)$ for any $Fv$ as the transitive closure of the union of the following reduction relations:
%
\begin{enumerate}
\item Reductions of Definition \ref{drd1}.
%
\item iotapt-reduction. An essential subterm of the form $[ev;x]([pt_r;y](o,T),tt,T')$ where $T[x/y]\sim_{\AA} T'$ reduces to $o$.  
\end{enumerate}
\end{definition}
%
The obvious analogs of Lemmas \ref{redsub01}-\ref{lequivsimred0} hold for TS2.
 


\subsection{Local confluence for general terms of TS2}
%
The local confluence theorem for TS2 has exactly the same form as Theorem \ref{lc1} and the same proof since there are no non-trivial confluence dependencies between the new reduction rule of Definition \ref{drd2} and the reduction rules of Definition \ref{drd1}. 


\subsection{Derivation rules of TS2}
%
The derivation rules for contexts and judgements of TS2 are the derivation rules for TS1 together with the following additional ones:

$$\frac{\Gamma\vdash}{\Gamma\vdash pt:\Eu_0}\spc \frac{\Gamma\vdash}{\Gamma\vdash tt:Pt}$$

$$\frac{\Gamma, x:Pt, y:T\vdash \spc \Gamma \vdash o:T[tt/x]}{\Gamma\vdash [pt_r;x](o,T):[\prod;x](Pt,T)}$$


\comment{
\subsection{Criterion of derivability for TS2 contexts and judgements}
%
\begin{pretheorem}
\llabel{alg2}
Let $UC=(Fu,{\AA})$ be a universe context such that ${\AA}\ne \emptyset$. Then one has:
%
\begin{enumerate}
\item A context $\Gamma=(x_1:E_1,\dots,x_n:E_n)$ is derivable (in $UC$) if and only if one has:
%
\begin{enumerate}
\item The context $\Gamma'=(x_1:E_1,\dots,x_{n-1}:E_{n-1})$ is derivable in $UC$.
\item The root label of $E_n$ belongs to the set of labels of TS1 and the corresponding condition of Pretheorem \ref{alg1} holds.
\end{enumerate}
%
\item A judgement $\Gamma\vdash o : T$ is derivable (in $UC$) if and only if one has:
%
\begin{enumerate}
\item The context $\Gamma, x:T\vdash$ is derivable.
\item One of the following conditions holds:
%
\begin{enumerate}
\item the root label of $o$ belongs to the set of labels of TS1 and the corresponding condition of Pretheorem \ref{alg0} holds.
\item $o=_{\AA}pt$ and $T=_{\AA} \Eu_0$,
\item $o=_{\AA}[pt_r;x](o',T')$ where $\Gamma, x:Pt, y:T'\vdash$ and $\Gamma\vdash o': T'[tt/x]$ are derivable and $T=_{\AA} [\prod;x](Pt,T')$.
\end{enumerate}
\end{enumerate}
\end{enumerate}
%
\end{pretheorem}
%
}








\section{Adding dependent sums - system TS1}

\subsection{TS1 terms and typing function}
%

\begin{definition}
\llabel{d11}
The following labels are permitted in the expressions of TS1 - the labels permitted in TS0, $(\sum;x)$, $(pair;x)$, $(pr1;x)$, $(pr2;x)$, $(total;x)$.
\end{definition}
%
The notions of u-level expressions, T- and o- terms in TS1 are defined as follows:
%
\begin{definition}
\llabel{d12}
\begin{enumerate}
\item expressions with the root node caring a TS0-label is an u-level expression, o-expression or a T-expression according to the rules of Definition \ref{d02},
\item expressions with the root of the form $[\sum;x]$ are T-expressions,
\item expressions with the root node of the form $[pair;x]$, $[pr1;x]$, $[pr2;x]$ and $[total;x]$ are o-expressions.
\end{enumerate}
\end{definition}
%
%
\begin{definition}
\llabel{d13}
A TS1-term is a TS1-expression such that:
%
\begin{enumerate}
\item any node caring one of the TS0-labels satisfies the conditions of Definition \ref{d03},
\item any node of the form $[\sum;x]$ has valency $2$, both its branches are T-expressions and the first one does not contain $[x]$,
\item any node of the form $[pair;x]$ has valency $3$, its first two branches are o-expressions which do not contain $[x]$ and the third branch a T-expression,
\item any node of the form $[pr1;x]$ has valency $3$, its first branch is a T-expression which does not contain on $[x]$, its second branch a T-expression and the third branch an o-expression,
\item any node of the form $[pr2;x]$ has valency $3$, its first branch is a T-expression which does not contain on $[x]$, its second branch a T-expression and the third branch an o-expression,
\item any node of the form $[total;x]$ has valency $4$ and its first two branches are u-level expressions and the last two are o-expressions of which the first one does not contain $[x]$. 
\end{enumerate}
\end{definition}
%
\begin{definition}
\llabel{d14}
A node in TS1 term is called non-essential if it satisfies the conditions of Definition \ref{d04} or if it belongs to the subexpression $T_1$ of a subexpression of the form $[pr1;x](T_1,T_2,o)$ or if it belongs to subexpression $T_1$ of a subexpression of the form $[pr2;x](T_1,T_2,o)$. The definition of essential nodes, essential and non-essential subexpressions and of $Ess(E)$ is extended to TS1-terms in the obvious way. 
\end{definition}
%
We let $TS1$ denote the set of TS1-terms and $TT1$ and $oT1$ denote the subsets of T-terms and o-terms.
The obvious analog of Lemma \ref{l02} holds for TS1-expressions. We extend to TS1 the abbreviations introduced for TS0-expressions and abbreviate $[total;x](M_1,M_2,o_1,o_2)$ to $[total;x]_{M_1,M_2}(o_1,o_2)$ and $[\sum;x](T_1,T_2)$ to $\sum x:T_1,T_2$. We also write $T_1\times T_2$ for $\sum x:T_1, T_2$ when $T_2$ does not depend on $x$ and use the notation $\sum (x_1:T_1)\dots (x_n:T_n),T$ for $\sum x_1:T_1,\sum x_2:T_2,\dots,\sum x:T_n, T$.  We will write $[pair;x](T_2,o_1,o_2)$ for $[pair;x](\tau_{\Gamma}(o_1),T_2,o_1,o_2)$.
%
\begin{definition}
\llabel{dtau1}
Under the assumptions of Definition \ref{dtau0} we extend the typing function $\tau_{\Gamma}$ to o-terms of TS1 as follows:
%
\begin{enumerate}
\item the value of $\tau_{\Gamma}$ on an o-term whose root node carries a TS0-label is computed according to the rules of Definition \ref{dtau0}.
\item $\tau_{\Gamma}([pair;x](o_1,o_2,T))=[\sum;x](\tau_{\Gamma}(o_1), T)$,
\item $\tau_{\Gamma}([pr1;x](T_1,T_2,o))=T_1$,
\item $\tau_{\Gamma}([pr2;x](T_1,T_2,o))=T_2[[pr1;x](T_1,T_2,o)/x]$,
\item $\tau_{\Gamma}([total;x]_{M_1,M_2}(o_1,o_2))=\Eu_{max(M_1,M_2)}$.
%
\end{enumerate}
\end{definition}
%
\begin{remark}\rm
As is seen from Definition \ref{dtau1} it is not necessary to include $T_2$ into the $pr1$ expressions and, therefore, not necessary to make $pr1$ into a quantifier in order to define $\tau_{\Gamma}$.The reason for the inclusion of $T_2$ into $pr1$ lies in the proof of Theorem \ref{lc1} below. Without this information it is impossible to define reductions on TS1-terms in a way which preserves (local) confluence. A particular case of the problem can be seen in the case of iotatotal2-reduction at the root combined with etatotal-reduction at $pair$. See proof of Theorem \ref{lc1}.
\end{remark}
%
We have the obvious analog of Proposition \ref{tausub0} for TS1.


\subsection{Equivalence relations $\equiv_{\AA}$ and $\sim_{\AA}$ on TS1-terms}
\llabel{sim1}
%
The relations $\equiv_{\AA}$ and $\sim_{\AA}$ are extended to TS1-terms in the obvious way. We also have obvious analogs of all the statements of Section \ref{sim0}.







\subsection{Reducibility relation on TS1 terms}
\llabel{red1}
%

\begin{definition}
\llabel{drd1}
Let $UC=(Fu,{\AA})$ be universe context and $FV$ a sequence of T-variables. Define a relation $\rd_{\AA}$ on $TS1(Fu,FV,Fv)$ for each $Fv$ as the union of the transitive closures of the following reduction relations:
%
\begin{enumerate}
\item Reductions of Definition \ref{drd0}.
%
\item Eltotal-reduction. An essential subterm of the form  $[El][total_{M_1,M_2};x](o_1,o_2)$  reduces to $[\sum;x]([El](o_1),[El](o_2))$.
%
\item iotatotal1-reduction. An essential subterm of the form $[pr1;x](T_1,T_2,[pair;y](o_1,o_2,T_2'))$ such that $T_2[y/x]\sim_{\AA} T_2'$  reduces to $o_1$.
\item iotatotal2-reduction. An essential subterm of the form $[pr2;x](T_1,T_2,[pair;y](o_1,o_2,T_2'))$ such that $T_2[y/x]\sim_{\AA} T_2'$ reduces to $o_2$.
%
\item etatotal-reduction. An essential subterm of the form 
%
$$[pair;x]([pr1;y](T_1',T_2',a'), [pr2;y](T_1'',T_2'',a''), T_2)$$
%
such that $a'\sim_{\AA} a''$ and $T_2'[x/y]\sim_{\AA} T_2\sim_{\AA} T_2''[x/y]$ reduces to $a'$. 
%
\item totalj-reductions: 
\begin{enumerate}
\item totalja-reduction. An essential subterm of the form 
%
$$[total_{M_1,M_2};x]([ev;z]([j_{M_0,M_1'}], o_1, T), o_2)$$
%
such that $M_1'\equiv_{\AA} M_1$, reduces to 
%
$$[ev;z]([j_{max(M_0,M_2), max(M_1,M_2)}], [total_{M_0,M_2};x](o_1,o_2), \Eu_{max(M_1,M_2)})$$
%
\item totaljb-reduction. An essential subterm of the form 
%
$$[total_{M_1,M_3};x](o_1, [ev;z]([j_{M_2,M_3'}], o_2, T) )$$
%
such that  $M_3'\equiv_{\AA} M_3$ reduces to
%
$$[ev;z]([j_{max(M_1,M_2),max(M_1,M_3)}], [total_{M_1,M_2};x](o_1,o_2), \Eu_{max(M_1,M_3)})$$
%
\end{enumerate}
%
\end{enumerate}
\end{definition}
%
\begin{remark}\rm
\llabel{etatotal1}
The condition that $T_2'[x/y]\equiv_{\AA} T_2$ is does not follow automatically for derivable terms. Indeed, if a term is derivable then one would expect that $T_2'[o_1/y]$ is convertible to $T_2[o_1/x]$ which does not imply that $T_2'[x/y]$ is convertible to $T_2$.
\end{remark}
%
Let $\rde_{\AA}$ be the transitive and reflexive closure of $\rd_{\AA}$. The obvious analogs of Lemmas \ref{redsub01}-\ref{lequivsimred0} hold for TS1.


\subsection{Local confluence for general terms of TS1}
%


%
\begin{theorem}
\llabel{lc1}
Let $UC=(Fu,{\AA})$ be a universe context and $FV$ a sequence of T-variables. Let $E\in TS1(Fu,FV,Fv)$. Let further $E \rd_{\AA} E_1$ and $E\rd_{\AA} E_2$ be two one-step reductions. Then there exists a TS1-terms $E'_1$, $E_2'$ from $TS1(Fu,FV,Fv)$ such that $E_1\rde_{\AA} E_1'$, $E_2\rde_{\AA} E_2'$ and $E_1'\sim_{\AA} E_2'$ unless the exceptional case of Theorem \ref{lc0} occurs.
\end{theorem}
%
\begin{proof}
It is sufficient to consider the case when the first reduction is relative to subterm $S=E$ i.e. occurs at the root. It is further sufficient to consider cases when one of the two reductions belongs to the list of new items in Definition \ref{drd1}. 
%
\begin{enumerate}
\item Elj-reduction at the root. $E=[El][ev;y]([j_{M_1,M_2}], o, T)$ and 
%
$$E_1=[El](o).$$
%
No new exposed nodes where second reduction may occur compared to TS0. 
%
\item Elforall-reduction at the root. $E=[El][forall_{M_1,M_2};x](o_1,o_2)$ and 
%
$$E_1=[\prod;x]([El](o_1),[El](o_2)).$$
%
No new exposed nodes where second reduction may occur compared to TS0. 
%
\item jMM-reduction at the root. $E=[j_{M_1,M_2}]$ such that $M_1\equiv_{\AA} M_2$ and
%
$$E_1=[\lambda;x](\Eu_{M_1},[x])$$ 
%
No new exposed nodes where second reduction may occur compared to TS0. 
%
\item beta-reduction at the root. $E=[ev;z]([\lambda;x](T_1,o_1),o_2,T_2)$ and 
%
$$E_1=o_1[o_2/x].$$
%
No new exposed nodes where second reduction may occur compared to TS0. 
%??? insert a reference on the relevant reduction-substitution results
%
\item jj-reduction at the root. $E=[ev;z]([j_{M_2',M_3}], [ev;y]([j_{M_1,M_2}], o, T), T')$ such that $M_2'\equiv_{\AA} M_2$ and
%
$$E_1=[ev;z]([j_{M_1,M_3}], o, \Eu_{M_3})$$
%
No new exposed nodes where second reduction may occur compared to TS0. 
%
\item eta-reduction at the root. $E=[\lambda;x](T_1, [ev;y](o ,[x], T_2))$ such that $o$ does not depend on $x$ and 
%
$$E_1=o$$
%
No new exposed nodes where second reduction may occur compared to TS0. 
%
\item forallj-reductions at the root:
\begin{enumerate}
\item forallja-reduction at the root. $E=[forall_{M_1,M_2};x]([ev;z]([j_{M_0,M_1'}], o_1,T), o_2)$ such that $M_1'\equiv_{\AA} M_1$ and
%
$$E_1=[ev;z]([j_{max(M_0,M_2), max(M_1,M_2)}], [forall_{M_0,M_2};x](o_1,o_2), \Eu_{max(M_1,M_2)})$$
%
No new exposed nodes where second reduction may occur compared to TS0. 

%
\item foralljb-reduction at the root. $E=[forall_{M_1,M_3};x](o_1, [ev;z]([j_{M_2,M_3'}], o_2, T) )$ such that $M_3'\equiv_{\AA} M_3$ and
%
$$E_1=[ev;z]([j_{max(M_1,M_2),max(M_1,M_3)}], [forall_{M_1,M_2};x](o_1,o_2), \Eu_{max(M_1,M_3)}),$$
%
No new exposed nodes where second reduction may occur compared to TS0. 
\end{enumerate}
%
\item Eltotal-reduction at the root. $E=[El][total_{M_1,M_2};x](o_1,o_2)$ and 
%
$$E_1=[\sum;x]([El](o_1),[El](o_2)).$$
%
The node where second reduction may occur is $[total_{M_1,M_2};x]$ with the following actual cases:
%
\begin{enumerate}
\item totalja-reduction at $[total_{M_1,M_2};x]$. Then $o_1=[ev;z]([j_{M_0,M_1'}], o_1',T)$ where $M_1'\equiv_{\AA} M_1$ and
%
$$E_1= [\sum;x]([El][ev;z]([j_{M_0,M_1'}], o_1', T),[El](o_2))\rd$$
$$ [\sum;x]([El](o_1'),[El](o_2))=E_1'$$
$$E_2= [El][ev;z]([j_{max(M_0,M_2),max(M_1,M_2)}], [total_{M_0,M_2};x](o_1',o_2), \Eu_{max(M_1,M_2)}) \rd$$ 
$$[El][total_{M_0,M_2};x](o_1',o_2) \rd [\sum;x]([El](o_1'), [El](o_2))=E_2'$$
%
\item foralljb-reduction at $[total_{M_1,M_2};x]$. Then $o_2=[ev;z](j_{M_3,M_2'},o_2',T)$ where $M_2'\equiv_{\AA} M_2$ and 
%
$$E_1=[\sum;x]([El](o_1),[El][ev;z](j_{M_3,M_2'},o_2',T))\rd$$
$$[\sum;x]([El](o_1),[El](o_2'))=E_1'$$
$$E_2= [El][ev;z]([j_{max(M_1,M_3),max(M_1,M_2)}], [total_{M_1,M_3};x](o_1,o_2'), \Eu_{max(M_1,M_2)})\rd $$
$$[El][forall_{M_1,M_3};x](o_1,o_2') \rd [\sum;x]([El](o_1),[El](o_2'))=E_2'$$
%
\end{enumerate}
%
\item iotatotal1-reduction at the root. $E=[pr1;x](T_1,T_2,[pair;y](o_1,o_2,T_2'''))$ where $T_2[y/x]\sim_{\AA} T_2'''$ and
%
$$E_1=o_1.$$
%
The exposed node where second reduction may occur is $[pair;y]$ with the only actual case being
%
\begin{enumerate}
\item etatotal-reduction at $[pair;y]$. Then 
%
$$E=[pr1;x](T_1,T_2,[pair;y]([pr1;z'](T_1',T_2',a'),[pr2;z''](T_1'',T_2'',a'')),T_2'''))$$
%
where $a'\sim_{\AA} a''$ and $T_2'[y/z']\sim_{\AA} T_2'''\sim_{\AA} T_2''[y/z'']$. Then 
%
$$E_1=[pr1;z'](T_1',T_2',a')$$
$$E_2=[pr1;x](T_1,T_2,a')$$
%
\end{enumerate}
%
\item iotatotal2-reduction at the root. $E=[pr2;x](T_1,T_2,[pair;y](o_1,o_2,T_2'''))$ where $T_2[y/x]\sim_{\AA} T_2'''$ and
%
$$E_1=o_2.$$
%
The exposed node where second reduction may occur is $[pair;y]$ with the only actual case being
%
\begin{enumerate}
\item etatotal-reduction at $[pair;y]$. Then 
%
$$E=[pr2;x](T_1, T_2,[pair;y]([pr1;z'](T_1',T_2',a'), [pr2;z''](T_1'',T_2'',a'')))$$
%
where $a\equiv_{\AA} a'$ and $T_2'[y/z']\sim_{\AA} T_2'''\sim_{\AA} T_2''[y/z'']$. Then 
%
$$E_1=[pr2;z''](T_1'',T_2'',a'')$$
$$E_2=[pr2;z](T_1',T_2',a')$$
%
\end{enumerate}
%
\item etatotal-reduction at the root. $E=[pair;x]([pr1;y](T_1',T_2',a'), [pr2;y](T_1'',T_2'',a''),T_2)$ where $a\sim_{\AA} a'$, $T_2'[x/y]\sim_{\AA} T_2\sim_{\AA} T_2''[x/y]$ and
%
$$E_1=a.$$
%
The exposed nodes where second reduction may occur are $[pr1;y]$ and $[pr2;y]$ the actual cases being
%
\begin{enumerate}
\item iotatotal1-reduction at $[pr1;y]$. Then 
%
$$E=[pair;x]([pr1;y](T_1', T_2', [pair;z'](o_1',o_2',T_2''')), [pr2;y](T_1'',T_2'', [pair;z''](o_1'',o_2'',T_2'''')), T_2)$$
%
where $o_1'\sim_{\AA} o_1''$, $o_2'\sim_{\AA} o_2''$, $T_2'''[z''/z']\sim_{\AA} T_2''''$, $T_2'[z'/y]\sim_{\AA} T_2'''$ and
%
$$E_1=[pair;z'](o_1',o_2',T_2''')=E_1'$$
$$E_2=[pair;x](o_1', [pr2;y](T_1'', T_2'', [pair;z''](o_1'',o_2'',T_2'''')), T_2)\rd_{\AA} $$ $$\rd_{\AA} [pair;x](o_1',o_2'',T_2)=E_2'$$
%
\item iotatotal2-reduction at $[pr2;y]$. Then 
%
$$E=[pair;x]([pr1;y](T_1', T_2', [pair;z'](o_1',o_2',T_2''')), [pr2;y](T_1'',T_2'',[pair;z''](o_1'',o_2'',T_2'''')), T_2)$$
%
where $o_1'\sim_{\AA} o_1''$, $o_2'\sim_{\AA} o_2''$, $T_2'''[z''/z']\sim_{\AA} T_2''''$, $T_2''[z''/y]\sim_{\AA} T_2''''$ and
%
$$E_1=[pair;z'](o_1',o_2',T_2''')=E_1'$$
$$E_2=[pair;x]([pr1;y](T_1', T_2', [pair;z'](o_1',o_2',T_2''')), o_2'', T_2)\rd_{\AA} $$ $$\rd_{\AA} [pair;x](o_1', o_2'', T_2)=E_2'$$
%
\end{enumerate}
%
\item totalj-reductions at the root:
%
\begin{enumerate}
\item totalja-reduction at the root. $E=[total_{M_1,M_2};x]([ev;z]([j_{M_0,M_1'}], o_1, T), o_2)$ such that $M_1'\equiv_{\AA} M_1$ and
%
$$E_1=[ev;z]([j_{max(M_0,M_2), max(M_1,M_2)}], [total_{M_0,M_2};x](o_1,o_2), \Eu_{max(M_1,M_2)})$$
%
Exposed nodes where second reduction may occur are $[total_{M_1,M_2};x]$, $[ev;z]$ and $[j_{M_0,M_1'}]$ with the following actual cases:
%
\begin{enumerate}
\item totaljb-reduction at $[total_{M_1,M_2};x]$. Then $o_2=[ev;z']([j_{M_3,M_2'}], o_2', T')$ where $M_2'\equiv_{\AA} M_2$ and 
%
$$E_1=[ev;z]([j_{max(M_0,M_2), max(M_1,M_2)}], $$
$$[total_{M_0,M_2};x](o_1, [ev;z']([j_{M_3,M_2'}], o_2', T')), \Eu_{max(M_1,M_2)})\rd$$
$$[ev;z]([j_{max(M_0,M_2), max(M_1,M_2)}], $$
$$ [ev;z']([j_{max(M_0,M_3),max(M_0,M_2')}], [total_{M_0,M_3};x](o_1,o_2'), \Eu_{max(M_0,M_2')}),$$
$$ \Eu_{max(M_1,M_2)} )\rd$$
$$[ev;z]([j_{max(M_0,M_3),max(M_1,M_2)}], [total_{M_0,M_3};x](o_1,o_2'), \Eu_{max(M_1,M_2)})=E_1'$$
%
$$E_2=[ev;z']([j_{max(M_1,M_3), max(M_1,M_2)}], $$
$$ [total_{M_1,M_3};x]([ev;z]([j_{M_0,M_1'}], o_1, T), o_2'), \Eu_{max(M_1,M_2)})\rd$$
$$[ev;z']([j_{max(M_1,M_3), max(M_1,M_2)}], $$
$$ [ev;z]([j_{max(M_0,M_3),max(M_1,M_3)}], [total_{M_0,M_3};x](o_1,o_2'), \Eu_{max(M_1,M_3)}) ,$$
$$ \Eu_{max(M_1,M_2)})\rd$$
$$[ev;z']([j_{max(M_0,M_3),max(M_1,M_2)}], [total_{M_0,M_3};x](o_1,o_2'), \Eu_{max(M_1,M_2)})=E_2'$$
%
\item jj-reduction at $[ev;z]$. Then $o_1=[ev;z']([j_{M_3,M_0'}],o_1', T')$ where $M_0'\equiv_{\AA} M_0$  and 
%
$$E_1=[ev;z]([j_{max(M_0,M_2), max(M_1,M_2)}],$$
$$ [total_{M_0,M_2};x]( [ev;z']([j_{M_3,M_0'}], o_1', T'), o_2), \Eu_{max(M_1,M_2)})\rd$$
$$[ev;z]([j_{max(M_0,M_2), max(M_1,M_2)}], $$
$$ [ev;z']([j_{max(M_3,M_2),max(M_0,M_2)}], [total_{M_3,M_2};x](o_1',o_2), \Eu_{max(M_0,M_2)}), $$
$$ \Eu_{max(M_1,M_2)})\rd$$
$$[ev;z]([j_{max(M_3,M_2),max(M_1,M_2)}], [total_{M_3,M_2};x](o_1',o_2), \Eu_{max(M_1,M_2)})=E_1'$$
%
$$E_2=[total_{M_1,M_2};x]([ev;z]([j_{M_3,M_1'}], o_1', T), o_2)\rd$$
$$[ev;z]([j_{max(M_3,M_2), max(M_1,M_2)}], [total_{M_3,M_2};x](o_1',o_2), \Eu_{max(M_1,M_2)})=E_2'$$
%
\item jMM-reduction at $[j_{M_0,M_1'}]$. Then $M_0\equiv_{\AA} M_1'$ and 
%
$$E_1=[ev;z]([j_{max(M_0,M_2), max(M_1,M_2)}], [total_{M_0,M_2};x](o_1,o_2), \Eu_{max(M_1,M_2)})\rd$$
$$[ev;z]([\lambda;x](\Eu_{max(M_0,M_2)},[x]), [total_{M_0,M_2};x](o_1,o_2), \Eu_{max(M_1,M_2)})\rd$$
$$[total_{M_0,M_2};x](o_1,o_2)=E_1'$$
%
$$E_2=[total_{M_1,M_2};x]([ev;x]([\lambda;x](\Eu_{M_0},[x]), o_1, T), o_2)\rd$$
$$[total_{M_1,M_2};x](o_1,o_2)=E_2'$$
\end{enumerate}




%
\item totaljb-reduction at the root. $E=[total_{M_1,M_3};x](o_1, [ev;z]([j_{M_2,M_3'}], o_2, T) )$ such that $M_3'\equiv_{\AA} M_3$ and
%
$$E_1=[ev;z]([j_{max(M_1,M_2),max(M_1,M_3)}], [total_{M_1,M_2};x](o_1,o_2), \Eu_{max(M_1,M_3)}),$$
%
Exposed nodes where second reduction may occur  are $[total_{M_1,M_3};x]$, $[ev;z]$ and $[j_{M_2,M_3'}]$ with the following actual cases:
%
\begin{enumerate}
\item totalja-reduction at $[total_{M_1,M_3};x]$. Then $o_1=[ev;z']([j_{M_0,M_1'}], o_1', T')$ where $M_1'\equiv_{\AA} M_1$ and 
%
$$E_1=[ev;z]([j_{max(M_1,M_2), max(M_1,M_3)}], $$
$$[total_{M_1,M_2};x]([ev;z']([j_{M_0,M_1'}], o_1', T'), o_2), \Eu_{max(M_1,M_3)})\rd$$
$$[ev;z]([j_{max(M_1,M_2), max(M_1,M_3)}], $$
$$ [ev;z']([j_{max(M_0,M_2),max(M_1,M_2)}], [total_{M_0,M_2};x](o_1',o_2), \Eu_{max(M_0,M_2)}),$$
$$ \Eu_{max(M_1,M_3)})\rd$$
$$[ev;z]([j_{max(M_0,M_2),max(M_1,M_3)}], [total_{M_0,M_2};x](o_1',o_2), \Eu_{max(M_1,M_3)} )=E_1'$$
%
$$E_2=[ev;z']([j_{max(M_0,M_3), max(M_1,M_3)}], $$
$$ [total_{M_0,M_3};x](o_1', [ev;z]([j_{M_2,M_3'}], o_2, T'), \Eu_{max(M_1,M_3)})\rd$$
$$[ev;z']([j_{max(M_0,M_3), max(M_1,M_3)}], $$
$$ [ev;z]([j_{max(M_0,M_2),max(M_0,M_3)}], [total_{M_0,M_2};x](o_1',o_2), \Eu_{max(M_0,M_3)}) ,$$
$$ \Eu_{max(M_1,M_3)})\rd$$
$$[ev;z']([j_{max(M_0,M_2),max(M_1,M_3)}], [total_{M_0,M_2};x](o_1',o_2), \Eu_{max(M_1,M_3)})=E_2'$$
%
\item jj-reduction at $[ev;z]$. Then $o_2=[ev;z']([j_{M_0,M_2'}],o_2',T')$ where $M_2'\equiv_{\AA} M_2$ and 
%
$$E_1=[ev;z]([j_{max(M_1,M_2), max(M_1,M_3)}],$$
$$ [total_{M_1,M_2};x]( o_1 ,[ev;z']([j_{M_0,M_2'}],o_2',T') ), \Eu_{max(M_1,M_3)})\rd$$
$$[ev;z]([j_{max(M_1,M_2), max(M_1,M_3)}], $$
$$ [ev;z']([j_{max(M_1,M_0),max(M_1,M_2)}], [total_{M_1,M_0};x](o_1,o_2'), \Eu_{max(M_1,M_2)}), $$
$$ \Eu_{max(M_1,M_3)})\rd$$
$$[ev;z]([j_{max(M_1,M_0),max(M_1,M_3)}], [total_{M_1,M_0};x](o_1,o_2'), \Eu_{max(M_1,M_3)})=E_1'$$
%
$$E_2=[total_{M_1,M_3};x](o_1, [ev;z]([j_{M_0,M_3'}], o_1', T'))\rd$$
$$[ev;z]([j_{max(M_1,M_0), max(M_1,M_3)}], [total_{M_1,M_0};x](o_1,o_2'), \Eu_{max(M_1,M_3)})=E_2'$$
%
\item jMM-reduction at $[j_{M_2,M_3'}]$. Then $M_2\equiv_{\AA} M_3'$ and 
%
$$E_1=[ev;z]([j_{max(M_1,M_2), max(M_1,M_3)}], [total_{M_1,M_2};x](o_1,o_2), \Eu_{max(M_1,M_3)})\rd$$
$$[ev;z]([\lambda;x](\Eu_{max(M_1,M_2)},[x]), [total_{M_1,M_2};x](o_1,o_2), \Eu_{max(M_1,M_3)})\rd$$
$$[total_{M_1,M_2};x](o_1,o_2)=E_1'$$
%
$$E_2=[total_{M_1,M_3};x](o_1, [ev;x]([\lambda;x](\Eu_{M_2},[x]), o_2, T'))\rd$$
$$[total_{M_1,M_3};x](o_1,o_2)=E_2'$$
\end{enumerate}
\end{enumerate}
%
\end{enumerate}
\end{proof}




\subsection{Derivation rules of TS1}
%
The derivation rules for contexts and judgements of TS1 are the derivation rules for TS0 together with the following additional ones:

$$\frac{\Gamma, x:T_1, y:T_2\vdash}{\Gamma, y:[\sum;x](T_1,T_2)}$$

$$\frac{\Gamma, x : T_1, y:T_2\vdash\spc \Gamma\vdash o_1:T_1\spc\Gamma\vdash o_2:T_2[o_1/x]}{\Gamma\vdash [pair;x](o_1,o_2,T_2):[\sum;x](T_1,T_2)}$$

$$\frac{\Gamma\vdash a:[\sum;x](T_1,T_2)}{\Gamma\vdash [pr1;x](T_1,T_2,a):T_1}\spc \frac{\Gamma\vdash a:[\sum;x](T_1,T_2)}{\Gamma\vdash [pr2;x](T_1,T_2,a):T_2[[pr1;x](T_1,T_2,a)/x]}$$

$$\frac{\Gamma\vdash o_1:\Eu_{M_1}\spc \Gamma, x:[El](o_1)\vdash o_2:\Eu_{M_2}}{\Gamma\vdash [total_{M_1.M_2};x](o_1,o_2):\Eu_{max(M_1,M_2)}}$$

\begin{remark}
\rm\llabel{sumelim}
Note that our derivation and reduction rules for the dependent sum allow one to define "eliminators" which one would have if one introduced dependent sums as particular cases of inductive definitions as it is done in Coq. For $\Gamma, x:T_1, y:T_2\vdash$ the eliminator for the corresponding dependent sum is a family of terms $I_M$  of type (we use the standard abbreviation $\sr$ for non-dependent product)
%
$$[\prod;P](([\sum;x](T_1,T_2)\sr \Eu_M),$$
$$ [\prod; s0]([\prod;s1](T_1, [\prod;s2](T_2, [ev;a](P, [pair;x](s1,s2,T_2), \Eu_M))),$$
$$ [\prod;c]([\sum;x](T_1,T_2), [ev;a](P,c,\Eu_M))))$$
%
which one defines as
%
$$[\lambda;P](([\sum;x](T_1,T_2)\sr \Eu_M),$$
$$[\lambda;s0]([\prod;s1](T_1, [\prod;s2](T_2, [ev;a](P, [pair;x](s1,s2,T_2), \Eu_M))),$$
$$[\lambda;c]([\sum;x](T_1,T_2), [ev;s2]([ev;s1](P, [pr1](c,T_1),_), [pr2;x](T_1,c,T_2)),\_)))$$
%
which is well-typed since $[pair;x]([pr1](T_1,c),[pr2;x](T_1,c,T_2))=_{\AA} c$. 
\end{remark}


\comment{
\subsection{Criterion of derivability for TS1 contexts and judgements}
%
In this section we provide a conjectural algorithm which determines whether a given context or judgement composed of TS1 terms is derivable in a given universe context $UC=(Fu,{\AA})$ where ${\AA}\ne \emptyset$. We formulate this algorithm as a pre-theorem which provides the necessary and sufficient conditions of derivability in the form which is easily converted into a recursive algorithm.
%
\begin{pretheorem}
\llabel{alg1}
Let $UC=(Fu,{\AA})$ be a universe context such that ${\AA}\ne \emptyset$. Then one has:
%
\begin{enumerate}
\item A context $\Gamma=(x_1:E_1,\dots,x_n:E_n)$ is derivable (in $UC$) if and only if one has:
%
\begin{enumerate}
\item The context $\Gamma'=(x_1:E_1,\dots,x_{n-1}:E_{n-1})$ is derivable in $UC$.
\item One of the following holds:
%
\begin{enumerate}
\item the root label of $E_n$ belongs to the set of labels of TS0 and the corresponding condition of Pretheorem \ref{alg0} holds.
\item $N(E_n)=[\sum;x](T_1,T_2)$ and $\Gamma', x:T_1, y:T_2\vdash$ is derivable.
\end{enumerate}
\end{enumerate}
%
\item A judgement $\Gamma\vdash o : T$ is derivable (in $UC$) if and only if one has:
%
\begin{enumerate}
\item The context $\Gamma, x:T\vdash$ is derivable.
\item One of the following conditions holds:
%
\begin{enumerate}
\item the root label of $o$ belongs to the set of labels of TS0 and the corresponding condition of Pretheorem \ref{alg0} holds.
\item $o=[pair;x](o_1,o_2,T_2)$ where $\Gamma, o_1:\tau_{\Gamma}(o_1)$, $\Gamma,x:\tau_{\Gamma}(o_1),y:T_2\vdash$ and $\Gamma\vdash o_2:T_2[o_1/x]$ are derivable and $T=_{\AA} T_2[o_1/x]$.
\item $o=[pr1](T_1,o)$ where $\Gamma\vdash o:\tau_{\Gamma}(o)$ is derivable, the normal form of $\tau_{\Gamma}(o)$ is of the form $[\sum;x](N(T_1),T_2)$ for some $T_2$ where $N(T_1)$ is the normal form of $T_1$ and $T=_{\AA} T_1$.
\item $o=[pr2;x](T_1,o,T_2)$ where $\Gamma\vdash o:[\sum;x](T_1,T_2)$ is derivable and $T=_{\AA} T_2[[pr1](T_1,o)/x]$.
\item $o=[total_{M_1,M_2};x][o_1,o_2]$ where $\Gamma\vdash o:\Eu_{M_1}$ and $\Gamma, x:[El](o_1)\vdash o_2:\Eu_{M_2}$ are derivable and $T=_{\AA} \Eu_{max(M_1,M_2)}$.
\end{enumerate}
\end{enumerate}
\end{enumerate}
%
\end{pretheorem}
%
}


\section{Adding pairwise disjoint unions - system TS3}
%

\subsection{TS3 terms and typing function}
%
\begin{definition}
\llabel{d31}
The following labels are permitted in the expressions of TS3 - the labels permitted in TS2, $\amalg$, $coprod$, $ii1$, $ii2$ and $[sum;x]$, $[\amalg;x_1,x_2]$.
\end{definition}
%
The notions of u-level expressions, T- and o- terms in TS3 are defined as follows:
%
\begin{definition}
\llabel{d32}
\begin{enumerate}
\item expressions with the root node caring a TS2-label is an u-level expression, o-expression or a T-expression according to the rules of Definition \ref{d22},
\item expressions with the root of the form $\amalg$ and $[\amalg;x_1,x_2]$ are T-expressions,
\item expressions with the root of the form $coprod$, $ii1$, $ii2$ and $sum$.  are o-expressions.
\end{enumerate}
\end{definition}
%
%
\begin{definition}
\llabel{d33}
A TS3-term is a TS3-expression such that:
%
\begin{enumerate}
\item any node caring one of the TS2-labels satisfies the conditions of Definition \ref{d23},
\item any node of the form $[\amalg]$ has valency $2$ and its two branches are T-expressions, 
\item any node of the form $[\amalg;x_1,x_2]$ has valency $5$, its first four branches are T-expressions and the fifth branch is an o-expression, its first, second and fifths branches do not depend on $x_1,x_2$, its third branch does not depend on $x_2$ and its fourth branch does not depend on $x_1$,
\item any node of the form $[coprod]$ has valency $4$, its first two branches are u-level expressions and the last two branches are o-expressions, 
\item any node of the form $[ii1]$ has valency 3 and its first two branches are T-expressions and the third one is an o-expression,
\item any node of the form $[ii2]$ has valency 3 and its first two branches are T-expressions and the third one is an o-expression.\item any node of the form $[sum;x]$ has valency 6, its first two branches are T-expressions next three are o-expressions all of which do not contain $x$ and the last branch is a T-expression.
\end{enumerate}
\end{definition}
%
%
\begin{definition}
\llabel{d34}
A node in TS3 term is called non-essential if it satisfies the conditions of Definition \ref{d14}. The same applies to the definition of essential nodes, essential and non-essential subexpressions and of $Ess(E)$ is extended to TS3-terms in the obvious way. 
\end{definition}
%
We let $TS3$ denote the set of TS3-terms and $TT3$ and $oT3$ denote the subsets of T-terms and o-terms.
The obvious analog of Lemma \ref{l02} holds for TS3-expressions. We extend to TS3 the abbreviations introduced for TS2-expressions, abbreviate $[coprod](M_1,M_2,o_1,o_2)$ as $[coprod_{M_1,M_2}](o_1,o_2)$ and write $T_1\amalg T_2$ for $[\amalg](T_1,T_2)$. 
%
\begin{definition}
\llabel{dtau3}
Under the assumptions of Definition \ref{dtau0} we extend the typing function $\tau_{\Gamma}$ to o-terms of TS3 as follows:
%
\begin{enumerate}
\item the value of $\tau_{\Gamma}$ on an o-term whose root node carries a TS2-label is computed according to the rules of Definition \ref{dtau2}.
\item $\tau_{\Gamma}([coprod_{M_1,M_2}](o_1,o_2))=\Eu_{max(M_1,M_2)}$,
\item $\tau_{\Gamma}([ii1](T_1,T_2,o))= [\amalg](T_1,T_2)$,
\item $\tau_{\Gamma}([ii2](T_1,T_2,o))= [\amalg](T_1,T_2)$,
\item $\tau_{\Gamma}([sum;x](T_1,T_2,s_1,s_2,o,S))=S[o/x]$.
\end{enumerate}
\end{definition}
%
We have the obvious analog of Proposition \ref{tausub0} for TS3.


\subsection{Equivalence relations $\equiv_{\AA}$ and $\sim_{\AA}$ on TS3-terms}
%
The relations $\equiv_{\AA}$ and $\sim_{\AA}$ are extended to TS1-terms in the obvious way. We also have obvious analogs of all the statements of Section \ref{sim0}.
%


\subsection{Reducibility relation on TS3 terms}
%

\begin{definition}
\llabel{drd3}
Let $UC=(Fu,{\AA})$ be universe context and $FV$ a sequence of T-variables. Define a relation $\rd_{\AA}$ on $TS3(Fu,FV,Fv)$ for any $Fv$ as the transitive closure of the union of the following reduction relations:
%
\begin{enumerate}
\item Reductions of Definition \ref{drd2}.
%
\item Elcoprod-reduction. An essential subterm of the form $[El][coprod_{M_1,M_2}](o_1,o_2)$ reduces to $[\amalg]([El](o_1),[El](o_2))$.
\item amalg-reductions. 
%
\begin{enumerate}
\item amalg1-reduction. An essential sub term of the form 
%
$$[\amalg;x_1,x_2](T_1,T_2,S_1,S_2,[ii1](T_1',T_2',o))$$
%
such that $T_1\sim_{\AA} T_1'$ and $T_2\sim_{\AA} T_2'$ reduces to $S_1[o/x_1]$.
%
\item amalg1-reduction. An essential sub term of the form 
%
$$[\amalg;x_1,x_2](T_1,T_2,S_1,S_2,[ii2](T_1',T_2',o))$$
%
such that $T_1\sim_{\AA} T_1'$ and $T_2\sim_{\AA} T_2'$ reduces to $S_2[o/x_2]$.
\end{enumerate}
%
\item sum-reductions. 
%
\begin{enumerate}
\item sum1-reduction. An essential  subterm of the form 
%
$$[sum;x](T_1,T_2,s_1,s_2, [ii1](T_1',T_2',o))$$
%
such that  $T_1\sim_{\AA} T_1'$ and $T_2\sim_{\AA} T_2'$  reduces to $[ev;x](s_1,o, [\amalg](T_1,T_2))$.
%
\item sum2-reduction. An essential  subterm of the form 
%
$$[sum;x](T_1,T_2,s_1,s_2, [ii2](T_1',T_2',o))$$
%
such that  $T_1\sim_{\AA} T_1'$ and $T_2\sim_{\AA} T_2'$ reduces to $[ev;x](s_2,o, [\amalg](T_1,T_2))$.
\end{enumerate}
%
\item coprodj-reductions:
%
\begin{enumerate}
\item coprodj1-reduction. An essential subterm of the form 
%
$$[coprod_{M_1,M_2}]([ev;z]([j_{M_0,M_1'}],o_1, T),o_2)$$
%
where $M_1\equiv_{\AA} M_1'$ reduces to 
%
$$[ev;z]([j_{max(M_0,M_2), max(M_1,M_2)}], [coprod_{M_0,M_2}](o_1,o_2), \Eu_{max(M_1,M_2)})$$
%
\item coprodj2-reduction. An essential subterm of the form 
%
$$[coprod_{M_1,M_3}](o_1, [ev;z]([j_{M_2,M_3'}],o_2,T))$$
%
where $M_3\equiv_{\AA} M_3'$ reduces to 
%
$$[ev;z]([j_{max(M_1,M_2), max(M_1,M_3)}], [coprod_{M_1,M_2}](o_1,o_2), \Eu_{max(M_1,M_3)})$$
%
\end{enumerate}
\end{enumerate}
\end{definition}
%
The obvious analogs of Lemmas \ref{redsub01}-\ref{lequivsimred0} hold for TS3.





\subsection{Local confluence for general terms of TS3}
%
There are eight new confluence situations associated with disjoint union. They are:
%
\begin{enumerate}
\item Elcoprod-reduction at the root with:
%
\begin{enumerate}
\item coprodj1-reduction at $[coprod]$.
\item coprod2-reduction at $[coprod]$.
\end{enumerate}
%
\item coprodj1-reduction at the root with:
%
\begin{enumerate}
\item coprodj2-reduction at $[coprod]$.
\item jj-reduction at $[ev;z]$.
\item jMM-reduction at $[j]$.
\end{enumerate}
%
\item coprodj2-reduction at the root with:
%
\begin{enumerate}
\item coprodj1-reduction at $[coprod]$.
\item jj-reduction at $[ev;z]$.
\item jMM-reduction at $[j]$.
\end{enumerate}
\end{enumerate}
%
which are handled in exactly the same way as similar confluence situations for $[forall]$ and $[total]$.






\subsection{Derivation rules of TS3}
%
The derivation rules for contexts and judgements of TS3 are the derivation rules for TS2 together with the following additional ones:

$$\frac{\Gamma\vdash o_1:\Eu_{M_1}\spc \Gamma\vdash o_1:\Eu_{M_2}}{\Gamma\vdash [coprod_{M_1,M_2}]:\Eu_{max(M_1,M_2)}}$$

$$\frac{\Gamma, x_1:T_1\vdash\spc \Gamma, x_2:T_2\vdash}{\Gamma, x:[\amalg](T_1,T_2)\vdash}$$

$$\frac{\Gamma\vdash a: [\amalg](T_1,T_2)\spc
\begin{array}{l}
\Gamma, x_1:T_1, s_1:S_1\vdash\\
\Gamma, x_2:T_2, s_2:S_2\vdash
\end{array}}{\Gamma, s:[\amalg;x_1,x_2](T_1,T_2,S_1,S_2,a)\vdash}$$

$$\frac{\Gamma\vdash o_1:T_1\spc \Gamma, x_2:T_2\vdash}{\Gamma\vdash [ii1](T_1,T_2,o_1):[\amalg](T_1,T_2)}$$

$$\frac{\Gamma, x_1:T_1\vdash \spc \Gamma\vdash  o_2:T_2}{\Gamma\vdash [ii2](T_1,T_2,o_2):[\amalg](T_1,T_2)}$$

$$\frac{\Gamma, x: [\amalg](T_1,T_2), y : S \vdash\spc 
%
\begin{array}{c}
\Gamma\vdash s_1:[\prod;x_1](T_1, S[[ii1](T_1,T_2,x_1)/o])\\
\Gamma\vdash s_2:[\prod;x_2](T_2, S[[ii2](T_1,T_2,x_2)/o])
\end{array}
%
\spc \Gamma \vdash o : [\amalg](T_1,T_2)}{\Gamma\vdash [sum;x](T_1,T_2,s_1,s_2,o,S):S[o/x]}$$
%


\comment{
\subsection{Criterion of derivability for TS3 contexts and judgements}
%
\begin{pretheorem}
\llabel{alg3}
Let $UC=(Fu,{\AA})$ be a universe context such that ${\AA}\ne \emptyset$. Then one has:
%
\begin{enumerate}
\item A context $\Gamma=(x_1:E_1,\dots,x_n:E_n)$ is derivable (in $UC$) if and only if one has:
%
\begin{enumerate}
\item The context $\Gamma'=(x_1:E_1,\dots,x_{n-1}:E_{n-1})$ is derivable in $UC$.
%
\item One of the following conditions holds:
%
\begin{enumerate}
\item The root label of $E_n$ belongs to the set of labels of TS2 and the corresponding condition of Pretheorem \ref{alg2} holds.
\item One has $E_n=_{\AA}[\amalg](T_1,T_2)$ and $\Gamma,x_1:T_1\vdash$, $\Gamma, x_2:T_2\vdash$ are derivable. 
\end{enumerate}
\end{enumerate}
%
\item A judgement $\Gamma\vdash o : T$ is derivable (in $UC$) if and only if one has:
%
\begin{enumerate}
\item The context $\Gamma, x:T\vdash$ is derivable.
\item One of the following conditions holds:
%
\begin{enumerate}
\item the root label of $o$ belongs to the set of labels of TS1 and the corresponding condition of Pretheorem \ref{alg0} holds.
\item $o=pt$ and $T=_{\AA} \Eu_0$,
\item $o=[pt_r;x](P,o)$ where $\Gamma, x:Pt, y:P\vdash$ and $\Gamma\vdash o: P[tt/x]$ are derivable and $T=_{\AA} [\prod;x](Pt,P)$.
\end{enumerate}
\end{enumerate}
\end{enumerate}
%
\end{pretheorem}
%
}



\section{Adding the empty type - system TS4}
%

\subsection{TS4 terms and typing function}
%
\begin{definition}
\llabel{d41}
The following labels are permitted in the expressions of TS4 - the labels permitted in TS3,  $empty$, $empty_r$.
\end{definition}
%
The notions of u-level expressions, T- and o- terms in TS4 are defined as follows:
%
\begin{definition}
\llabel{d42}
\begin{enumerate}
\item expressions with the root node caring a TS3-label is an u-level expression, o-expression or a T-expression according to the rules of Definition \ref{d32},
\item expressions with the root of the form $[empty]$ and $[empty_r]$ are o-expressions,
\end{enumerate}
\end{definition}
%
%
\begin{definition}
\llabel{d43}
A TS4-term is a TS4-expression such that:
%
\begin{enumerate}
\item any node caring one of the TS3-labels satisfies the conditions of Definition \ref{d33},
\item any node of the form $[empty]$ has valency $0$, 
\item any node of the form $[empty_r]$ has valency $2$, its first branch is a T-expression and its second branch an o-expression. \end{enumerate}
\end{definition}
%
\begin{definition}
\llabel{d44}
A node in TS4 term is called non-essential if it satisfies the conditions of Definition \ref{d14}. The same applies to the definition of essential nodes, essential and non-essential subexpressions and of $Ess(E)$ is extended to TS4-terms in the obvious way. 
\end{definition}
%
We let $TS4$ denote the set of TS4-terms and $TT4$ and $oT4$ denote the subsets of T-terms and o-terms.
The obvious analog of Lemma \ref{l02} holds for TS4-expressions. We extend to TS4 the abbreviations introduced for TS3-expressions and also abbreviate $[El][empty]$ as $\emptyset$. 
%
\begin{definition}
\llabel{dtau4}
Under the assumptions of Definition \ref{dtau0} we extend the typing function $\tau_{\Gamma}$ to o-terms of TS4 as follows:
%
\begin{enumerate}
\item the value of $\tau_{\Gamma}$ on an o-term whose root node carries a TS3-label is computed according to the rules of Definition \ref{dtau3}.
\item $\tau_{\Gamma}([empty])=\Eu_0$,
\item $\tau_{\Gamma}([empty_r](T,o)=T$
\end{enumerate}
\end{definition}
%
We have the obvious analog of Proposition \ref{tausub0} for TS3.


\subsection{Equivalence relations $\equiv_{\AA}$ and $\sim_{\AA}$ on TS4-terms}
%
The relations $\equiv_{\AA}$ and $\sim_{\AA}$ are extended to TS1-terms in the obvious way. We also have obvious analogs of all the statements of Section \ref{sim0}.


\subsection{Reducibility relation on TS4 terms}
%

There are no new reductions for TS4 compared to TS3. The obvious analogs of Lemmas \ref{redsub01}-\ref{lequivsimred0} hold for TS4.







\subsection{Local confluence for general terms of TS4}
%
There are no new confluence situations for TS4 compared with TS3. 



\subsection{Derivation rules of TS4}
%
The derivation rules for contexts and judgements of TS4 are the derivation rules for TS3 together with the following additional ones:

$$\frac{\Gamma\vdash}{\Gamma\vdash empty:\Eu_0}$$

$$\frac{\Gamma, x : T \vdash\spc \Gamma\vdash o : \emptyset}{\Gamma\vdash empty_r(T,o):T}$$

This derivations rules show in particular correctness of the following definition
%
$$Def.\spc fromempty (T:Type):=\lambda\, x:\emptyset, [empty_r](T,x):\prod x:\emptyset, T$$
%


\section{Adding generalized $W$-types - system TS5}
%



\subsection{TS5 terms and typing function}
%
\begin{definition}
\llabel{d51}
The following labels are permitted in the expressions of TS5 - the labels permitted in TS4, $[IC;x,y,z]$, $[c;x,y,z]$, $[IC_{r};x,y,z,x',v]$, $[ic;x,y,z]$.
\end{definition}
%
The notions of u-level expressions, T- and o- terms in TS5 are defined as follows:
%
\begin{definition}
\llabel{d52}
\begin{enumerate}
\item expressions with the root node caring a TS4-label is an u-level expression, o-expression or a T-expression according to the rules of Definition \ref{d42},
\item expressions with the root of the form $[IC;x,y,z]$ are T-expressions,
\item expressions with the root of the form $[c;x,y,z]$, $[IC_{r};x,y,z,x',v]$ and $[ic;x,y,z]$ are o-expressions.
\end{enumerate}
\end{definition}
%
%
\begin{definition}
\llabel{d53}
A TS5-term is a TS5-expression such that:
%
\begin{enumerate}
\item any node caring one of the TS4-labels satisfies the conditions of Definition \ref{d33},
\item any node of the form $[IC;x,y,z]$ has valency $5$, its first branch, third and fourth branches are T-expressions and second and fifths branches are o-expressions, the first and second branch do not depend on $x,y,z$, the third branch does not depend on $y,z$  and the fourth branch does not depend on $z$,  
\item any node of the form $[c;x,y,z]$ has valency $7$ with the same conditions on the first five branches as for $[IC;x,y,z]$, the sixth and seventh branches are o-expressions which do not depend on $x,y$ and $z$,
\item any node of the form $[IC_{r};x,y,z,x',v]$ has valency $8$ with the same conditions on the first five branches as for $[IC;x,y,z]$ and additional condition that they do not depend on $x',v$, its sixth and eighths branches are o-expressions, its seventh branch is a T-expression, the sixth and eighths branches do not depend on $x,y,z,x',v$, the seventh branch does not depend on $x,y,z$,
\item any node of the form $[ic;x,y,z]$ has valency $8$, its first three branches are u-level expressions and the last five branches are o-expressions,  the fourth and fifth branches do not depend on $x,y,z$, the sixth branch does not depend on $y,z$ and the seventh branch does not depend on $z$.
\end{enumerate}
\end{definition}
%
\begin{definition}
\llabel{d54}
A node in TS5 term is called non-essential if it satisfies the conditions of Definition \ref{d14}. The same applies to the definition of essential nodes, essential and non-essential subexpressions and of $Ess(E)$ is extended to TS5-terms in the obvious way. 
\end{definition}
%
We let $TS5$ denote the set of TS5-terms and $TT5$ and $oT5$ denote the subsets of T-terms and o-terms.
The obvious analog of Lemma \ref{l02} holds for TS5-expressions. We extend to TS5 the abbreviations introduced for TS4-expressions. 
%
\begin{definition}
\llabel{dtau5}
Under the assumptions of Definition \ref{dtau0} we extend the typing function $\tau_{\Gamma}$ to o-terms of TS5 as follows:
%
\begin{enumerate}
\item the value of $\tau_{\Gamma}$ on an o-term whose root node carries a TS4-label is computed according to the rules of Definition \ref{dtau4}.
\item $\tau_{\Gamma}([c;x,y,z](A,a,B,D,q,b,f))=[IC;x,y,z](A,a,B,D,q)$,
\item $\tau_{\Gamma}([IC_{r};x,y,z,x',v](A,a,B,D,q,i,S,t))=S[a/x',i/v]$,
\item $\tau_{\Gamma}([ic;x,y,z](M_1,M_2,M_3,o_A,a,o_B,o_D,q))=\Eu_{max(M_1,M_2,M_3)}$.
\end{enumerate}
\end{definition}
%
We have the obvious analog of Proposition \ref{tausub0} for TS5.


\subsection{Equivalence relations $\equiv_{\AA}$ and $\sim_{\AA}$ on TS5-terms}
%
The relations $\equiv_{\AA}$ and $\sim_{\AA}$ are extended to TS5-terms in the obvious way. We also have obvious analogs of all the statements of Section \ref{sim0}.



\subsection{Reducibility relation on TS5 terms}
%

\begin{definition}
\llabel{drd5}
Let $UC=(Fu,{\AA})$ be universe context and $FV$ a sequence of T-variables. Define a relation $\rd_{\AA}$ on $TS5(Fu,FV,Fv)$ for all $Fv$ as the transitive closure of  the union of the following reduction relations:
%
\begin{enumerate}
\item Reductions of Definition \ref{drd3}.
%
\item Elic-reduction. An essential sub term of the form $[El][ic;x,y,z](M_1,M_2,M_3,o_A,a,o_B,o_D,q)$ reduces to $[IC;x,y,z]([El](o_A),a,[El](o_B),[El](o_D),q)$.
%
\item ICiota-reduction. An essential subterm of the form 
%
$$[IC_{r};x,y,z,x',v](A,a,B,D,[c;x,y,z](A',a',B',D',q,b,f),S,t)$$
%
where $A\sim_{\AA} A'$, $a\sim_{\AA} a'$, $B\sim_{\AA} B'$ and $D\sim_{\AA} D'$ reduces to
%
$$t\,\,a\,\,b\,\,f\,\,[\lambda;d](D[a/x,b/y],[IC_{r};x,y,z,x',v](A, q[a/x,b/y,d/z],B,D,q, (f\,\,d)))$$
%
\end{enumerate}
\end{definition}
%

The obvious analogs of Lemmas \ref{redsub01}-\ref{lequivsimred0} hold for TS5.

\subsection{Recursive equality in TS5}
%
In the following two rules we use the notation $qd=q[a/x,b/y,z/d]$.
%
$$\frac{
\begin{array}{l}
\Gamma, x:A, y:B, z:D\vdash q:A\\
\Gamma, a:A, i:[IC;x,y,z](A,a,B,D,q),t_1:T_1\vdash\\
\Gamma, a:A, i:[IC;x,y,z](A,a,B,D,q),t_2:T_2\vdash\\
(\Gamma, a:A, b:B[a/x], d:D[a/x,b/y], i:[IC;x,y,z](A,qd,B,D,q)\vdash T_1[qd/a]=_{\AA}T_2[qd/a])\Rightarrow\\
\spc\spc(\Gamma, a:A, i:[IC;x,y,z](A,a,B,D,q)\vdash T_1=_{\AA} T_2)
\end{array} 
}{\Gamma, a:A, i:[IC;x,y,z](A,a,B,D,q)\vdash \, T_1=_{\AA}T_2}$$
%
$$\frac{
\begin{array}{l}
\Gamma, x:A, y:B, z:D\vdash q:A\\
\Gamma, a:A, i:[IC;x,y,z](A,a,B,D,q)\vdash f:T\\
\Gamma, a:A, i:[IC;x,y,z](A,a,B,D,q)\vdash g:T\\
(\Gamma, a:A, b:B[a/x], d:D[a/x,b/y], i:[IC;x,y,z](A,qd,B,D,q)\vdash f[qd/a]=_{\AA}g[qd/a])\Rightarrow\\
\spc\spc(\Gamma, a:A, i:[IC;x,y,z](A,a,B,D,q)\vdash f=_{\AA} g)
\end{array} 
}{\Gamma, a:A, i:[IC;x,y,z](A,a,B,D,q)\vdash \, f=_{\AA}g}$$
%








\subsection{Local confluence for general terms of TS5}
%
There are no new confluence situations for TS5 compared with TS5. 



\subsection{Derivation rules of TS5}
%
The derivation rules for contexts and judgements of TS5 are the derivation rules for TS4 together with the following additional ones:
%
$$\frac{\Gamma\vdash a:A\spc \Gamma, x:A, y:B, z:D\vdash q:A}{\Gamma, w:[IC;x,y,z](A,a,B,D,q)\vdash}$$

$$\frac{\Gamma\vdash o_A:\Eu_{M_1}\spc\Gamma\vdash a:[El](o_A)\spc
%
\begin{array}{l}
\Gamma, x:[El](o_A)\vdash o_B:\Eu_{M_2}\\
\Gamma, x:[El](o_A), y:[El](o_B)\vdash o_D:\Eu_{M_3}\\
\Gamma, x:[El](o_A), y:[El](o_B), z:[El](o_D)\vdash q:[El](o_A)
\end{array}}{\Gamma\vdash [ic;x,y,z](o_A,a,o_B,o_D,q):\Eu_{max(M_1,M_2,M_3)}}$$



%
$$\frac{\Gamma\vdash a:A\spc \Gamma, x:A, y:B, z:D\vdash q:A\spc \Gamma\vdash b:B[a/x]\spc \Gamma\vdash f: [\prod; z'](D[a/x,b/y], ICqa)}{\Gamma\vdash [c;x,y,z](A,a,B,D,q,b,f): [IC;x,y,z](A,a,B,D,q)}$$
%
where
%
$$ICqa:=[IC;x,y,z](A,q[a/x,b/y,z'/z],B,D,q)$$
%
and
%
$$\frac{
\begin{array}{l}
\Gamma\vdash a:A\\
\Gamma, x:A, y:B, z:D\vdash q:A\\
\Gamma\vdash i:[IC;x,y,z](A,a,B,D,q)\\
\Gamma, x':A, v: ICx', s:S\vdash \\
\Gamma\vdash t:\prod (x':A)(y':B[x'/x])(w: [\prod;z'](D[x'/x,y'/y],ICq')),\\
{}[\prod;d](D[x'/x,y'/y], S[q[x'/x,y'/y,d/z]/x', (w\,d)/v])\sr S [(cx'y'w)/v]
\end{array}
}{\Gamma\vdash [IC_{r};x,y,z,x',v](A,a,B,D,q,i,S,t):S[a/x',i/v]}$$
%
where
%
$$ICx':=[IC;x,y,z](A,x',B,D,q)$$
$$ICq':=[IC;x,y,z](A,q[x'/x,y'/y,z'/z],B,D,q)$$
$$cx'y'w:=[c;x,y,z](A,x',B,D,q,y',w)$$

%
\begin{remark}\rm
Our inductive type $[IC;x,y,z](A,a,B,D,q)$ corresponds to the following inductive definition in Coq:

Inductive IC(A:Type)(a:A)(B:A->Type)(D:forall x:A, ( B x -> Type ))(q:forall x:A, forall y:B x, forall z: D x y, A):= c: forall b:B a, forall f : (forall d: D a b, IC A (q a b d) B D q), IC A a B D q .

with $[IC_{r};\dots]$ being a direct analog of the eliminator $IC_{r}$ and the reduction rule the direct analog of the iota-reduction for this inductive type. 

\end{remark}



\section{Datatypes}
%
The basic constructions of TS5 allow one to define various "datatypes" i.e. types with associated eliminators and computation rules which in Coq are introduced by strictly positive inductive definitions without pseudo-parameters. In this section we consider only natural numbers and binary trees but it should be possible to write down a simple algorithm which would translate a general strictly positive inductive definition without pseudo-parameters into the language of TS5. 
%
\subsection{Natural numbers}
%
The object of type $\Eu_0$ corresponding to natural numbers is defined as follows:
%
$$Def.\spc nat:=[ic;x,y,z](o_A,tt,o_B,o_D,tt):\Eu_0$$
%
where 
%
$$o_A:=pt\spc o_B:=[coprod_{0,0}](pt,pt)$$
$$o_D:=[sum;y'](Pt,Pt,(\lambda\, z':Pt, empty),(\lambda\,z':Pt, pt),y,\Eu_0)$$
% 
We will write $\nn$ for $[El](nat)$. The two standard constructors for $\nn$ are defined as:
%
$$Def.\spc O:=[c;x,y,z](A,tt,B,D,tt,[ii1](Pt,Pt,tt), (fromempty\, \nn)):\nn $$
%
$$Def.\spc S:=\lambda\, n:\nn, [c;x,y,z](A,tt,B,D,tt,[ii2](Pt,Pt,tt),  (\lambda\,t:Pt, n)): \nn\sr\nn$$
%
where
%
$$A:=[El](o_A)=Pt\spc B:=[El](o_B)=Pt\amalg Pt\spc D=[El](o_D)$$
%
The eliminator associated with natural numbers is defined as:
%
$$[nat_{r};v](v:\nn, v':T\vdash)(o_O:T[O/v])(o_S:\prod (v:\nn)(y:T), T[(S\,v)/v])(n:\nn) :=$$ $$= [IC_r;x,y,z,x',v](A,tt,B,D,tt,n,T,t): T[n/v]$$
%
where 
%
$$t:\prod (x':Pt)(y':Pt\amalg Pt)(w:D[y'/y]\sr \nn)(s:\prod d:D[y'/y], T[(w\,d)/v]),$$ $$ T([c;x,y,z](A,x',B,D,tt,y',w)/v)$$
%
using eliminators for $Pt$ and $Pt\amalg Pt$ we see that it is sufficient to describe $t\,tt\,[ii1](tt)$ and $t\,tt\,[ii2](tt)$ whose types are
%
$$t\,tt\,[ii1](tt):\prod (w:\emptyset \sr \nn)(s:\prod d:\emptyset , T[(w\,d)/v]), T([c;x,y,z](A,tt,B,D,tt,[ii1](tt),w)/v)$$
%
and
%
$$t\,tt\,[ii2](tt):\prod (w:Pt \sr \nn)(s:\prod d:Pt, T[(w\,d)/v]), T([c;x,y,z](A,tt,B,D,tt,[ii2](tt),w)/v)$$
% 





$$=\lambda (x:Pt)(y:Pt\amalg Pt)(w:\prod z':D,\nn)(s:\prod d:D,T[w\,d/v]), [sum;y'](Pt,Pt,f_1,f_2,y,(\prod (d:D[y'/y])(v':\nn), T))$$













\section{Adding the identity types - system TS6}
%

\subsection{TS6 terms and typing function}
%
\begin{definition}
\llabel{d61}
The following labels are permitted in the expressions of TS6 - the labels permitted in TS5,  $Id$, $paths$, $refl$, $[J;x,e]$.
\end{definition}
%
The notions of u-level expressions, T- and o- terms in TS6 are defined as follows:
%
\begin{definition}
\llabel{d62}
\begin{enumerate}
\item expressions with the root node caring a TS5-label is an u-level expression, o-expression or a T-expression according to the rules of Definition \ref{d52},
\item expressions with the root of the form $[Id]$ are T-expressions,
\item expressions with the root of the form $[paths]$, $[relf]$ and $[J;x,e]$ are o-expressions,
\end{enumerate}
\end{definition}
%
%
\begin{definition}
\llabel{d63}
A TS6-term is a TS6-expression such that:
%
\begin{enumerate}
\item any node caring one of the TS5-labels satisfies the conditions of Definition \ref{d53},
\item any node of the form $[Id]$ has valency $3$, its first branch is a T-expression and the last two branches are o-expressions,
\item any node of the form $[paths]$ has valency $4$, its first branch is a u-level expression and the following three branches are o-expressions, 
\item any node of the form $[refl]$ has valency $2$, its first branch is a T-expression and its second branch is an o-expression,
\item any node of the form $[J;x,e]$ has valency $6$, its first branch is a T-expression, the following 4 branches are o-expressions all of them do not contain $x,e$ and the last branch is a T-expression.
\end{enumerate}
\end{definition}
%
\begin{definition}
\llabel{d64}
A node in TS6 term is called non-essential if it satisfies the conditions of Definition \ref{d14}. The same applies to the definition of essential nodes, essential and non-essential subexpressions and of $Ess(E)$ is extended to TS6-terms in the obvious way. 
\end{definition}
%
We let $TS6$ denote the set of TS6-terms and $TT6$ and $oT6$ denote the subsets of T-terms and o-terms.
The obvious analog of Lemma \ref{l02} holds for TS6-expressions. We extend to TS6 the abbreviations introduced for TS5-expressions, abbreviate $[paths](M,t,o_1,o_2)$ as $[paths_M](t,o_1,o_2)$, $[Id](T, o_1,o_2)$ as $Id\,T\,o_1\,o_2$ and write $Id\,x\,y$ for $Id\,\tau_{\Gamma}(x)\,x\,y$ and $refl\, o$ for $[refl](\tau_{\Gamma}(o),o)$.
%
\begin{definition}
\llabel{dtau6}
Under the assumptions of Definition \ref{dtau0} we extend the typing function $\tau_{\Gamma}$ to o-terms of TS6 as follows:
%
\begin{enumerate}
\item the value of $\tau_{\Gamma}$ on an o-term whose root node carries a TS5-label is computed according to the rules of Definition \ref{dtau5}.
\item $\tau_{\Gamma}([paths_M](t,o_1,o_2))=\Eu_M$,
\item $\tau_{\Gamma}([refl](T,o))=[Id](T,o,o)$,
\item $\tau_{\Gamma}([J;x,e](T,a,b,q,i,S))=S[o_1/x,o_2/y,o_3/e]$
\end{enumerate}
\end{definition}
%
We have the obvious analog of Proposition \ref{tausub0} for TS6.


\subsection{Equivalence relations $\equiv_{\AA}$ and $\sim_{\AA}$ on TS6-terms}
%
The relations $\equiv_{\AA}$ and $\sim_{\AA}$ are extended to TS1-terms in the obvious way. We also have obvious analogs of all the statements of Section \ref{sim0}.



\subsection{Reducibility relation on TS6 terms}
%

\begin{definition}
\llabel{drd6}
Let $UC=(Fu,{\AA})$ be universe context and $FV$ a sequence of T-variables. Define a relation $\rd_{\AA}$ on $TS6(Fu,FV,Fv)$ for all $Fv$ as the transitive closure of the union of the following reduction relations:
%
\begin{enumerate}
\item Reductions of Definition \ref{drd3}.
%
\item Elpaths-reduction An essential subterm of the form $[El][paths_M](t,o_1,o_2)$ reduces to $[Id]([El](t),o_1,o_2)$,
\item pathsj-reduction An essential subterm of the form $[paths_{M_2}]([ev;x]([j_{M_1,M_2'}],t, Т),o_1,o_2)$ such that $M_2\equiv_{\AA} M_2'$ reduces to $[ev;x]([j_{M_1,M_2'}], [paths_{M_1}](t,o_1,o_2),M_2')$,
\item Jiota-reduction. An essential subterm of the form $[J;x,e](T,a,a',q,[refl](T',a''),S)$ such that $a\sim_{\AA} a'\sim_{\AA} a''$ and $T\sim_{\AA} T'$ reduces to $q$,
\end{enumerate}
\end{definition}
%

The obvious analogs of Lemmas \ref{redsub01}-\ref{lequivsimred0} hold for TS6.




\subsection{Local confluence for general terms of TS6}
%
There are the following new confluence situations in TS6 compared with TS5:
%
\begin{enumerate}
\item Elpaths-reduction at the root and pathsj-reduction at $[paths]$,
\item pathsj-reduction at the root and
%
\begin{enumerate}
\item jj-reduction at $[ev;x]$,
\item jMM-reduction at [j].
\end{enumerate}
\end{enumerate}
%
These cases are dealt with in the same way as similar cases for $[forall]$, $[total]$ etc. 


\subsection{Derivation rules of TS6}
%
The derivation rules for contexts and judgements of TS6 are the derivation rules for TS5 together with the following additional ones:
%

$$\frac{\Gamma\vdash t :\Eu_M\spc \Gamma\vdash o_1:[El][t]\spc \Gamma\vdash o_2:[El][t]}{\Gamma\vdash [paths_M](t,o_1,o_2):\Eu_M}$$

$$\frac{\Gamma\vdash o_1:T \spc \Gamma\vdash o_2:T}{\Gamma, y: [Id](T,o_1,o_2)\vdash}$$

$$\frac{\Gamma\vdash o : T}{\Gamma\vdash [refl](T,o):[Id](T,o,o)}$$

$$\frac{\Gamma\vdash a:T\spc 
%
\begin{array}{c}
\Gamma, x:T, e: [Id](T,a,x), z:S\vdash\\
\Gamma\vdash q:S[a/x,[refl](T,a)/e]
\end{array} 
%
\begin{array}{c}
\Gamma\vdash b:T\\
\Gamma\vdash i:[Id](T,a,b)
\end{array}
%
}{\Gamma\vdash [J;x,e](T,a,b,q,i,S):S[b/x,i/e]}$$










\newpage





\section{Adding resizing rules RR0 and RR1 - system TS7}
%
In order to introduce the resizing rules we will need the folioing definitions:
%
\begin{enumerate}
\item $Def.\spc Iscontr(X:Type):=\sum x:X, \prod y:X, Id\, y\, x$
\item $Def.\spc Hfiber\{X, Y:Type\}( f: X\sr Y)(y:Y):=\sum x:X, Id\,(f\,x)\, y$
\item $Def.\spc Isweq\{X\, Y\:Type\}(f:X\sr Y):=\prod y:Y, Iscontr (Hfiber\,f\,y)$
\item $Def.\spc Weq(X\,Y\,:Type):=\sum f:X\sr Y, Isweq\,f$
\item $Def.\spc Isaprop(X:Type):=\prod x:X,\prod x':X,Iscontr (Id\,x\,x')$
\item $Def.\spc Isaset(X:Type):=\prod x:X,\prod x':X, Isaprop(Id\,x\,x')$
\item $Def.\spc idfun(X:Type):=\lambda x:X, x$
\item $Th.\spc idisweq(X:Type):Isweq\, X$
\item $Def.\spc idweq(X:Type):=[pair;f](Isweq\,f,idfun\,X,idisweq\,X):Weq\,X\,X$
\end{enumerate} 
%







\subsection{TS7 terms and typing function}
%
\begin{definition}
\llabel{d71}
The following labels are permitted in the expressions of TS7 - the labels permitted in TS6,  $rr0$, $rr1$.
\end{definition}
%
The notions of u-level expressions, T- and o- terms in TS7 are defined as follows:
%
\begin{definition}
\llabel{d72}
\begin{enumerate}
\item expressions with the root node caring a TS5-label is an u-level expression, o-expression or a T-expression according to the rules of Definition \ref{d62},
\item expressions with the root of the form $rr0$ and $rr1$ are o-expressions,
\end{enumerate}
\end{definition}
%
%
\begin{definition}
\llabel{d73}
A TS7-term is a TS7-expression such that:
%
\begin{enumerate}
\item any node caring one of the TS6-labels satisfies the conditions of Definition \ref{d63},
\item any node of the form $[rr0]$ has valency $5$, its first two branches are u-level expressions and the last three are o-expressions, 
\item any node of the form $[rr1]$ has valency $3$, its first branch is an u-level expression and the last two branches are o-expressions,
\end{enumerate}
\end{definition}
%
\begin{definition}
\llabel{d74}
A node in TS7 term is called non-essential if it satisfies the conditions of Definition \ref{d14} or if it belongs to the subexpression $t$ or $e$ of a subexpression of the form $[rr0](M_1,M_2,s,t,e)$ or if it belongs to subexpression $p$ of a subexpression of the form $[rr1](M,a,p)$.

The definition of essential nodes, essential and non-essential subexpressions and of $Ess(E)$ is extended to TS6-terms in the obvious way. 
\end{definition}
%

We let $TS7$ denote the set of TS7-terms and $TT7$ and $oT7$ denote the subsets of T-terms and o-terms.
The obvious analog of Lemma \ref{l02} holds for TS7-expressions. We extend to TS7 the abbreviations introduced for TS6-expressions and also abbreviate $[rr0](M_2,M_1,s,t,e)$ as $[rr0_{M_2,M_1}](s,t,e)$ and $[rr1](M,a,p)$ as $[rr1_M](a,p)$. 
%
\begin{definition}
\llabel{dtau7}
Under the assumptions of Definition \ref{dtau0} we extend the typing function $\tau_{\Gamma}$ to o-terms of TS7 as follows:
%
\begin{enumerate}
\item the value of $\tau_{\Gamma}$ on an o-term whose root node carries a TS6-label is computed according to the rules of Definition \ref{dtau6}.
\item $\tau_{\Gamma}([rr0_{M_2,M_1}](s,t,e))=\Eu_{M_1}$,
\item $\tau_{\Gamma}([rr1_M](a,p))=\Eu_0$,
\end{enumerate}
\end{definition}
%
We have the obvious analog of Proposition \ref{tausub0} for TS7.


\subsection{Equivalence relations $\equiv_{\AA}$ and $\sim_{\AA}$ on TS7-terms}
%
The relations $\equiv_{\AA}$ and $\sim_{\AA}$ are extended to TS7-terms in the obvious way. We also have obvious analogs of all the statements of Section \ref{sim0}.


\subsection{Reducibility relation on TS7 terms}
%

\begin{definition}
\llabel{drd7}
Let $UC=(Fu,{\AA})$ be universe context and $FV$ a sequence of T-variables. Define a relation $\rd_{\AA}$ on $TS7(Fu,FV,Fv)$ for all $Fv$ as the transitive closure of the union of the following reduction relations:
%
\begin{enumerate}
\item Reductions of Definition \ref{drd6}.
%
\item Elrr0-reduction. An essential subterm of the form $[El][rr0_{M_2,M_1}](s,t,e)$ reduces to $[El](s)$.
%
\item forallrr0a-reduction. An essential subterm $S=[forall_{M_1,M_2};x]([rr0_{M_3,M_1'}](s,t,e),o_2)$ such that $M_1\equiv_{\AA} M_1'$ and $M_1'\le_{\AA} M_3$ reduces to
%
$$[rr0_{max(M_3,M_2),max(M_1,M_2)}]([forall_{M_3,M_2};x](s,o_2), S, idweq\, S)$$
%
\item forallrr0b-reduction. An essential subterm $S=[forall_{M_1,M_2};x](o_1,[rr0_{M_3,M_2'}](s,t,e))$ such that $M_2\equiv_{\AA} M_2'$ and $M_2'\le_{\AA} M_3$ reduces to
%
$$[rr0_{max(M_1,M_3),max(M_1,M_2)}]([forall_{M_1,M_3};x](o_1,s), S, idweq\, S)$$
%
\item totalrr0a-reduction. An essential subterm $S=[total_{M_1,M_2};x]([rr0_{M_3,M_1'}](s,t,e),o_2)$ such that $M_1\equiv_{\AA} M_1'$ and $M_1'\le_{\AA} M_3$ reduces to
%
$$[rr0_{max(M_3,M_2),max(M_1,M_2)}]([total_{M_3,M_2};x](s,o_2), S, idweq\, S)$$
%
\item totalrr0b-reduction. An essential subterm $S=[total_{M_1,M_2};x](o_1,[rr0_{M_3,M_2'}](s,t,e))$ such that $M_2\equiv_{\AA} M_2'$ and $M_2'\le_{\AA} M_3$ reduces to
%
$$[rr0_{max(M_1,M_3),max(M_1,M_2)}]([total_{M_1,M_3};x](o_1,s), S, idweq\, S)$$
%
\item coprodrr0a-reduction. An essential subterm $S=[coprod_{M_1,M_2}]([rr0_{M_3,M_1'}](s,t,e),o_2)$ such that $M_1\equiv_{\AA} M_1'$ and $M_1'\le_{\AA} M_3$ reduces to
%
$$[rr0_{max(M_3,M_2),max(M_1,M_2)}]([coprod_{M_3,M_2}](s,o_2), S, idweq\, X)$$
%
\item coprodrr0b-reduction. An essential subterm $S=[coprod_{M_1,M_2}](o_1,[rr0_{M_3,M_2'}](s,t,e))$ such that $M_2\equiv_{\AA} M_2'$ and $M_2'\le_{\AA} M_3$ reduces to
%
$$[rr0_{max(M_1,M_3),max(M_1,M_2)}]([coprod_{M_1,M_3}](o_1,s), S, idweq\, S)$$
%
\item pathsrr0-reduction. An essential subterm $S=[paths_{M_1}]([rr0_{M_2,M_1'}](s,t,e),o_1,o_2)$ such that $M_1\equiv_{\AA} M_1'$ and $M_1'\le_{\AA} M_2$ reduces to
%
$$[rr0_{M_2,M_1}]([paths_{M_2}](s,o_1,o_2), S, idweq\, S)$$
%






%
\item rr1rr0-reduction. An essential subterm of the form $[rr1_M](a,p)$ reduces to 
%
$$[rr0_{M,0}](a, [rr1_M](a,p), idweq\,[rr1_M](a,p)).$$
%
\item jrr0j-reduction. An essential subterm of the form $j_{M_1',M_3}\,[rr0_{M_2,M_1}](s,t,e)$ such that $M_1'\equiv_{\AA} M_1$ and $M_1\le_{\AA} M_2\le_{\AA} M_3$ reduces to $j_{M_2,M_3}\,s$.
\item jrr0rr0-reduction. An essential subterm of the form $j_{M_1',M_2}\,[rr0_{M_3,M_1}](s,t,e)$ such that $M_1'\equiv_{\AA} M_1$ and $M_1\le_{\AA} M_2\le_{\AA} M_3$ reduces to $[rr0_{M_3,M_2}](s, j_{M_1,M_2}\,t,e)$.
\item rr0jj-reduction. An essential subterm of the form $[rr0_{M_2,M_1}]((j_{M_0,M_2'}\,s), t, e)$ such that $M_2\equiv_{\AA} M_2'$ and $M_0\le_{\AA} M_1\le_{\AA} M_2$ reduces to $j_{M_0,M_1}\,s$.
\item rr0jrr0-reduction. An essential subterm of the form $[rr0_{M_3,M_1}]((j_{M_2,M_3'}\,s), t, e)$ such that $M_3\equiv_{\AA} M_3'$ and $M_0\le_{\AA} M_1\le_{\AA} M_2$ reduces to $[rr0_{M_2,M_1}](s,t,e)$.
\item rr0rr0-reduction. An essential subterm of the form $[rr0_{M_2,M_1}]([rr0_{M_3,M_2'}](s,t_2,e_2),t_1,e_1)$ such that $M_2\equiv_{\AA} M_2'$ and $M_1\le_{\AA} M_2\le_{\AA} M_3$ reduces to $[rr0_{M_3,M_1}](s,t_1,e_1)$.
%
\item rr0MM-reduction. An essential subterm of the form $[rr0_{M,M'}](s,t,e)$ such that $M\equiv_{\AA} M'$ reduces to $s$. 
%
\end{enumerate}
\end{definition}
%
The obvious analogs of Lemmas \ref{redsub01}-\ref{lequivsimred0} hold for TS7.





\subsection{Local confluence for general terms of TS7}
%
There are, if I have not missed anything, 91 new confluence cases related to the addition of resizing rules RR0 and RR1. We consider them below by naming the corresponding root reduction and the reduction at an exposed essential sub-term. The proofs in all cases seem to be straightforward. 
%
\begin{enumerate}
\item Elj-reduction at the root.
%
\begin{enumerate}
\item jrr0j.
\item jrr0rr0.
\end{enumerate}
%
\item Elforall-reduction at the root.
%
\begin{enumerate}
\item forallrr0a.
\item forallrr0b.
\end{enumerate}
%
\item jj-reduction at the root.
%
\begin{enumerate}
\item jrr0j.
\item jrr0rr0.
\end{enumerate}
%
\item forallja-reduction at the root.
%
\begin{enumerate}
\item jrr0j.
\item jrr0rr0. 
\end{enumerate}
%
\item foralljb-reduction at the root.
%
\begin{enumerate}
\item jrr0j.
\item jrr0rr0.
\end{enumerate}
%
\item Eltotal-reduction at the root.
%
\begin{enumerate}
\item totalrr0a.
\item totalrr0b.
\end{enumerate}
%
\item totalja-reduction at the root.
%
\begin{enumerate}
\item jrr0j.
\item jrr0rr0.
\end{enumerate}
%
\item totaljb-reduction at the root.
%
\begin{enumerate}
\item jrr0j.
\item jrr0rr0.
\end{enumerate}
%
\item Elcoprod-reduction at the root.
%
\begin{enumerate}
\item coprodrr0a.
\item coprodrr0b.
\end{enumerate}
%
\item coprodja-reduction at the root.
%
\begin{enumerate}
\item jrr0j.
\item jrr0rr0.
\end{enumerate}
%
\item coprodjb-reduction at the root.
%
\begin{enumerate}
\item jrr0j.
\item jrr0rr0.
\end{enumerate}
%
\item Elpaths-reduction at the root.
%
\begin{enumerate}
\item pathsrr0.
\end{enumerate}
%
\item pathsj-reduction at the root.
%
\begin{enumerate}
\item jrr0j.
\item jrr0rr0.
\end{enumerate}
%
\item Elrr0-reduction at the root.
%
\begin{enumerate}
\item rr0jj.
\item rr0jrr0.
\item rr0rr0.
\item rr0MM.
\end{enumerate}
%
\item forallrr0a/forallrr0b-reductions at the root.
%
\item forallrr0a-reduction at the root.
%
\begin{enumerate}
\item rr0jj.
\item rr0jrr0.
\item rr0rr0.
\item rr0MM.
\end{enumerate}
%
\item forallrr0b-reduction at the root.
%
\begin{enumerate}
\item rr0jj.
\item rr0jrr0.
\item rr0rr0.
\item rr0MM.
\end{enumerate}
%
\item totalrr0a/totalrr0b-reductions at the root.
%
\item totalrr0a-reduction at the root.
%
\begin{enumerate}
\item rr0jj.
\item rr0jrr0.
\item rr0rr0.
\item rr0MM.
\end{enumerate}
%
\item totalrr0b-reduction at the root.
%
\begin{enumerate}
\item rr0jj.
\item rr0jrr0.
\item rr0rr0.
\item rr0MM.
\end{enumerate}
%
\item coprodrr0a/coprodrr0b-reductions at the root.
%
\item coprodrr0a-reduction at the root.
%
\begin{enumerate}
\item rr0jj.
\item rr0jrr0.
\item rr0rr0.
\item rr0MM.
\end{enumerate}
%
\item coprodrr0b-reduction at the root.
%
\begin{enumerate}
\item rr0jj.
\item rr0jrr0.
\item rr0rr0.
\item rr0MM.
\end{enumerate}
%
\item pathsrr0-reduction at the root.
%
\begin{enumerate}
\item rr0jj.
\item rr0jrr0.
\item rr0rr0.
\item rr0MM.
\end{enumerate}
%
\item jrr0j-reduction at the root.
%
\begin{enumerate}
\item rr0jj.
\item rr0jrr0.
\item rr0rr0.
\item rr0MM.
\end{enumerate}
%
\item jrr0rr0-reduction at the root.
%
\begin{enumerate}
\item jrr0j.
\item rr0jj.
\item rr0jrr0.
\item rr0rr0.
\item rr0MM.
\end{enumerate}
%
\item rr0jj-reduction at the root.
%
\begin{enumerate}
\item jrr0j.
\item jrr0rr0.
\item rr0jrr0.
\item rr0MM.
\end{enumerate}
%
\item rr0jrr0-reduction at the root.
%
\begin{enumerate}
\item jrr0j.
\item jrr0rr0.
\item rr0jj.
\item rr0MM.
\end{enumerate}
%
\item rr0rr0-reduction at the root.
%
\begin{enumerate}
\item rr0jj.
\item rr0jrr0.
\item rr0rr0.
\item rr0MM(a).
\item rr0MM(b).
\end{enumerate}
%
\item rr0MM-reduction at the root.
%
\begin{enumerate}
\item rr0jj.
\item rr0jrr0.
\item rr0rr0.
\end{enumerate}
%
\end{enumerate}





\subsection{Derivation rules of TS7}
%
\begin{enumerate}
\item $$\frac{\Gamma\vdash s:\Eu_{M_2}\spc\Gamma\vdash t:\Eu_{M_1}\spc M_1\le_{\AA} M_2\spc \Gamma\vdash e:Weq\,*s\,*t}{\Gamma\vdash [rr0_{M_2,M_1}](s,t,e):\Eu_{M_1}}$$
\item $$\frac{\Gamma\vdash a:\Eu_M\spc \Gamma\vdash p:Isaprop\,*a}{\Gamma\vdash [rr1](a,p):\Eu_0}$$ 
\end{enumerate}
%






\subsection{Main meta-theorems and conjectural meta-theorems for TS6}
%
In what follows we fix a universe context $UC$ and a sequence of T-variables $FV$ and consider all the notions relative to this context and this sequence.
%
\begin{lemma}
\llabel{lm000}
In TS6 one has:
%
\begin{enumerate}
\item Any derivation tree for a context of the form $\Gamma,\Gamma'\vdash$ has a rooted sub-tree whose leaves are contexts of the form $\Gamma\vdash$.
\item Any derivation tree for a judgement of the form $\Gamma,\Gamma'\vdash o:T$ has a rooted sub-tree whose leaves are contexts of the form $\Gamma$.
\end{enumerate}
\end{lemma}
%
\begin{proof}
Induction on the length of the derivation tree. In the first case if $\Gamma'$ is empty then there is nothing to prove. Looking at the derivation rules we see that the premises for any derivation rule for a context of the form $\Gamma,\Gamma'\vdash$ where $\Gamma'$ is non-empty has either the same form or of the form $\Gamma,\Gamma'\vdash o:T$ or equals $\Gamma\vdash$. The premises for any derivation rule for a judgement of the form  $\Gamma,\Gamma'\vdash o:T$ is either of the same form or of the form $\Gamma,\Gamma'\vdash$ where $\Gamma'$ is non-empty or equals $\Gamma\vdash$.
\end{proof} 
%
\begin{definition}
\llabel{d000}
For a context of the form $\Gamma,\Gamma'\vdash$ or a judgement of the form $\Gamma,\Gamma'\vdash o:T$ the derivation depth relative to $\Gamma$ is the minimum over all derivation trees of the depth of the smallest sub-tree with all leaves equal $\Gamma\vdash$.
\end{definition}
%
Note that the derivation depth relative to $\Gamma$ is $0$ only for $\Gamma\vdash$. Note also that for any context or judgement of the form considered in Definition \ref{d000} there exists a derivation rule which produce this context or judgement such that all the premises are again of the same form and their derivation depth relative to $\Gamma$ is strictly less than for the original context or judgement. 
%
\begin{lemma}
\llabel{lm00}
One has:
%
\begin{enumerate}
\item Let $x_1:T_1,\dots,x_n:T_n \vdash$ be a derivable context in TS6. Then for any $i\le n$ the context $x_1:T_1,\dots, x_i:T_i\vdash$ is derivable.
\item Let $x_1:T_1,\dots,x_n:T_n\vdash o:T$ be a derivable judgement in TS6. Then for any $i\le n$ the context $x_1:T_1,\dots, x_i:T_i\vdash$ is derivable.
\end{enumerate}
\end{lemma}
%
\begin{proof}
The statements:
%
\begin{enumerate}
\item Let $x_1:T_1,\dots,x_n:T_n \vdash$ be a derivable context in TS6 of derivation depth $\le N$. Then for any $i\le n$ the context $x_1:T_1,\dots, x_i:T_i\vdash$ is derivable.
\item Let $x_1:T_1,\dots,x_n:T_n\vdash o:T$ be a derivable judgement in TS6 of derivation depth $\le N$. Then for any $i\le n$ the context $x_1:T_1,\dots, x_i:T_i\vdash$ is derivable.
\end{enumerate}
%
are immediately provable by induction on $N$ from the form of the derivation rules. 
\end{proof}
%


\subsection{Main conjectural meta-theorems for TS0}
%
Let us fix a universe context $UC=(Fu,{\AA})$ and a sequence of T-variables $FV$. 

\begin{definition}
\llabel{bnd}
A term $E$ is said to be bounded relative to ${\AA}$ if there exists $d\in\nn$ such that for any sequence of the form $E\rd_{\AA} E_1\rd_{\AA} E_2\rd_{\AA}\dots \rd_{\AA} E_n$ one has $n\le d$. The smallest $d$ satisfying this property is called the reduction depth of $E$. 
\end{definition}
%
\begin{definition}
\llabel{nf}
A term $E'$ is said to be a normal form of a term $E$ relative to ${\AA}$ if there is a sequence of the form $E\rd_{\AA} E_1\rd_{\AA}\dots\rd_{\AA} E_d=E'$ and the reduction depth of $E'$ is $0$. A term is said to be in the normal form if it is a normal form of itself. 
\end{definition}
%
In our system there is no chance for the actual uniqueness of the normal form. Instead the normal form of derivable terms (see below) is expected to be unique up to $\equiv_{\AA}$. 


%
\begin{definition}
\llabel{derivable}
A T-term $T$ is called derivable (relative to $UC$) if there is a derivable context of the form $\Gamma, x:T\vdash$. An o-term $o$ is called derivable if there is a derivable judgement of the form $\Gamma\vdash o:T$.
\end{definition}
%
\begin{conjecture}
\llabel{c1}
If $E$ is a derivable term then any subterm of $E$ is derivable.
\end{conjecture}
%
\begin{conjecture}
\llabel{c5}
If $\Gamma\vdash o:T$ is derivable then $\Gamma\vdash o:\tau_{\Gamma}(o)$ is derivable.
\end{conjecture}
%
\begin{conjecture}
\llabel{c2}
If $E$ is a derivable term and $E\rd_{\AA} E'$ then $E'$ is derivable.
\end{conjecture}
%
\begin{conjecture}
\llabel{c3}
If $E$ is a derivable term, $E\rd_{\AA} E_1$, $E\rd_{\AA} E_2$ then there exist $E_1'$, $E_2'$ such that $E_1'\equiv_{\AA} E_2'$ and $E_1\rde_{\AA} E_1'$, $E_2\rde_{\AA} E_2'$.
\end{conjecture}
%
\begin{conjecture}
\llabel{c4}
If ${\AA}\ne \emptyset$ and $E$ is a derivable term then $E$ is bounded.
\end{conjecture}
%
The following pre-theorems are theorems modulo the conjectures stated above.
%
\begin{pretheorem}
\llabel{pt1}
Let ${\AA}\ne \emptyset$, $E$ be a derivable term and $E\rde_{\AA} E_1$, $E\rd_{\AA} E_2$ then there exist $E_1'$, $E_2'$ such that $E_1'\equiv_{\AA} E_2'$ and $E_1\rde_{\AA} E_1'$, $E_2\rde_{\AA} E_2'$.
\end{pretheorem}
%
\begin{proof}
???
\end{proof}
%
\begin{pretheorem}
\llabel{pt2}
Let ${\AA}\ne\emptyset$ and $E$ be a derivable term. Then $E$ has a normal form $N(E)$ and for any two normal fors $N_1(E)$, $N_2(E)$ of $E$ one has $N_1(E)\equiv_{\AA} N_2(E)$.
\end{pretheorem}
%
\begin{proof}
???
\end{proof}

\begin{definition}
\llabel{deq}
Let ${\AA}\ne \emptyset$ and $E$, $E'$ be derivable terms. We say that $E=_{\AA} E'$ if for normal forms $N(E)$, $N(E')$ of $E$ and $E'$ respectively one has $N(E)\equiv_{\AA} N(E')$.
\end{definition}
%
Note that our pre-theorems imply that if ${\AA}\ne \emptyset$ then $=_{\AA}$ is a decidable equivalence relation on derivable terms.







\newpage


\section{Appendix A. Complete list of derivation rules}

\begin{enumerate}

\item $$\frac{}{\vdash}$$

\item $$\frac{\Gamma}{\Gamma, x:X\vdash\spc for\spc X\in FV}$$

\item $$\frac{\Gamma, x:T, \Gamma'\vdash}{\Gamma, x:T, \Gamma'\vdash x:T}$$

\item $$\frac{\Gamma\vdash o:T\spc \Gamma, x:T'\vdash\spc T\rd_{\AA} T'}{\Gamma\vdash o:T'}$$

\item $$\frac{\Gamma\vdash o:T\spc \Gamma, x:T'\vdash\spc T'\rd_{\AA} T}{\Gamma\vdash o:T'}$$

\item $$\frac{\Gamma\vdash o:T\spc T\sim_{\AA} T'}{\Gamma\vdash o:T'}$$

\item $$\frac{\Gamma, x:T, x':T'\vdash}{\Gamma, x'':[\prod;x](T,T')\vdash}$$

\item $$\frac{\Gamma\vdash o:\Eu_M}{\Gamma, x: [El](o)\vdash}$$

\item $$\frac{\Gamma\vdash}{\Gamma\vdash  u_M:\Eu_{M+1}}$$

\item $$\frac{\Gamma, x : T_1\vdash o: T_2}{\Gamma\vdash [\lambda;x](T_1,o):[\prod;x](T_1,T_2)}$$

\item $$\frac{\Gamma\vdash o_1:[\prod;x](T_1,T_2)\spc \Gamma\vdash o_2:T_1}{\Gamma\vdash [ev;x](o_1,o_2,T_2):T_2[o_2/x]}$$

\item $$\frac{\Gamma\vdash \spc M_1\le_{\AA} M_2}{\Gamma\vdash [j_{M_1,M_2}]:[\prod;x](\Eu_{M_1},\Eu_{M_2})}$$

\item $$\frac{\Gamma\vdash o_1:\Eu_{M_1}\spc \Gamma, x:[El](o_1)\vdash o_2:\Eu_{M_2}}{\Gamma\vdash [forall_{M_1,M_2};x](o_1,o_2):\Eu_{max(M_1,M_2)}}$$

\item $$\frac{\Gamma, x:T_1, y:T_2\vdash}{\Gamma, y:[\sum;x](T_1,T_2)\vdash}$$

\item $$\frac{\Gamma, x : T_1, y:T_2\vdash\spc \Gamma\vdash o_1:T_1\spc\Gamma\vdash o_2:T_2[o_1/x]}{\Gamma\vdash [pair;x](o_1,o_2,T_2):[\sum;x](T_1,T_2)}$$

\item $$\frac{\Gamma\vdash a:[\sum;x](T_1,T_2)}{\Gamma\vdash [pr1;x](T_1,T_2,a):T_1}$$

\item $$\frac{\Gamma\vdash a:[\sum;x](T_1,T_2)}{\Gamma\vdash [pr2;x](T_1,T_2,a):T_2[[pr1;x](T_1,T_2,a)/x]}$$

\item $$\frac{\Gamma\vdash o_1:\Eu_{M_1}\spc \Gamma, x:[El](o_1)\vdash o_2:\Eu_{M_2}}{\Gamma\vdash [total_{M_1.M_2};x](o_1,o_2):\Eu_{max(M_1,M_2)}}$$

\item $$\frac{\Gamma\vdash}{\Gamma\vdash pt:\Eu_0}$$

\item $$\frac{\Gamma\vdash}{\Gamma\vdash tt:Pt}$$

\item $$\frac{\Gamma, x:Pt, y:T\vdash \spc \Gamma \vdash o:T[tt/x]}{\Gamma\vdash [pt_r;x](o,T):[\prod;x](Pt,T)}$$

\item $$\frac{\Gamma\vdash o_1:\Eu_{M_1}\spc \Gamma\vdash o_1:\Eu_{M_2}}{\Gamma\vdash [coprod_{M_1,M_2}](o_1,o_2):\Eu_{max(M_1,M_2)}}$$

\item $$\frac{\Gamma, x_1:T_1\vdash\spc \Gamma, x_2:T_2\vdash}{\Gamma, x:[\amalg](T_1,T_2)\vdash}$$

\item $$\frac{\Gamma\vdash o_1:T_1\spc \Gamma, x_2:T_2\vdash}{\Gamma\vdash [ii1](T_1,T_2,o_1):[\amalg](T_1,T_2)}$$

\item $$\frac{\Gamma, x_1:T_1\vdash \spc \Gamma\vdash  o_2:T_2}{\Gamma\vdash [ii2](T_1,T_2,o_2):[\amalg](T_1,T_2)}$$

\item $$\frac{\Gamma, x: [\amalg](T_1,T_2), y : S \vdash\spc 
%
\begin{array}{c}
\Gamma\vdash s_1:[\prod;x_1](T_1, S[[ii1](T_1,T_2,x_1)/o])\\
\Gamma\vdash s_2:[\prod;x_2](T_2, S[[ii2](T_1,T_2,x_2)/o])
\end{array}
%
\spc \Gamma \vdash o : [\amalg](T_1,T_2)}{\Gamma\vdash [sum;x](T_1,T_2,s_1,s_2,o,S):S[o/x]}$$
%


\item $$\frac{\Gamma\vdash}{\Gamma\vdash empty:\Eu_0}$$

\item $$\frac{\Gamma, x : T \vdash\spc \Gamma\vdash o : \emptyset}{\Gamma\vdash empty_r(T,o):T}$$

\item $$\frac{\Gamma\vdash}{\Gamma\vdash nat:\Eu_0}$$
%
\item $$\frac{\Gamma\vdash}{\Gamma\vdash O:\nn}$$
%
\item $$\frac{\Gamma\vdash}{\Gamma\vdash S:[\prod;x](\nn,\nn)}$$
%
\item $$\frac{\Gamma, x:\nn, y:T\vdash\spc 
%
\begin{array}{c}
\Gamma\vdash o_1:T[O/x]\\
\Gamma\vdash o_2:[\prod;x](\nn, [\prod;y](T, T[[ev;z](S,x,\nn)/x]))
\end{array}
%
\spc \Gamma\vdash n:\nn}{\Gamma \vdash [nat_r;x](o_1,o_2,n,T):T[n/x]}$$


\item $$\frac{\Gamma\vdash t :\Eu_M\spc \Gamma\vdash o_1:[El][t]\spc \Gamma\vdash o_2:[El][t]}{\Gamma\vdash [paths_M](t,o_1,o_2):\Eu_M}$$

\item $$\frac{\Gamma\vdash o_1:T \spc \Gamma\vdash o_2:T}{\Gamma, y: [Id](T,o_1,o_2)\vdash}$$

\item $$\frac{\Gamma\vdash o : T}{\Gamma\vdash [refl](T,o):[Id](T,o,o)}$$

\item $$\frac{\Gamma\vdash a:T\spc 
%
\begin{array}{c}
\Gamma, x:T, e: [Id](T,a,x), z:S\vdash\\
\Gamma\vdash q:S[a/x,[refl](T,a)/e]
\end{array} 
%
\begin{array}{c}
\Gamma\vdash b:T\\
\Gamma\vdash i:[Id](T,a,b)
\end{array}
%
}{\Gamma\vdash [J;x,e](T,a,b,q,i,S):S[b/x,i/e]}$$
%
\item $$\frac{\Gamma\vdash s:\Eu_{M_2}\spc\Gamma\vdash t:\Eu_{M_1}\spc M_1\le_{\AA} M_2\spc \Gamma\vdash e:Weq\,*s\,*t}{\Gamma\vdash [rr0_{M_2,M_1}](s,t,e):\Eu_{M_1}}$$
%
\item $$\frac{\Gamma\vdash a:\Eu_M\spc \Gamma\vdash p:Isaprop\,*a}{\Gamma\vdash [rr1_M](a,p):\Eu_0}$$ 

\end{enumerate}


\newpage

\section{Appendix B. Complete list of reductions}

\begin{enumerate}

\item Elforall-reduction. $$[El][forall_{M_1,M_2};x](o_1,o_2)\rd_{\AA} [\prod;x]([El](o_1),[El](o_2))$$

\item Eltotal-reduction. $$[El][total_{M_1,M_2};x](o_1,o_2)\rd_{\AA} [\sum;x]([El](o_1),[El](o_2))$$

\item Elcoprod-reduction. $$[El][coprod_{M_1,M_2}](T_1,T_2)\rd_{\AA} [\amalg]([El](o_1),[El](o_2))$$

\item Elpaths-reduction.  $$[El][paths_M](t,o_1,o_2)\rd_{\AA} [Id]([El](t),o_1,o_2)$$

\item Elj-reduction $$[El][ev;y]([j_{M_1,M_2}],o,T)\rd_{\AA} [El](o)$$


\item jMM-reduction. $$[j_{M_1,M_2}]\rd_{\AA} [\lambda;x](\Eu_{M_1},[x])\spc iff \spc M_1\equiv_{\AA} M_2$$

\item beta-reduction. $$[ev;z]([\lambda;x](T_1,o_1),o_2,T_2)\rd_{\AA} o_1[o_2/x]$$

\item jj-reduction. $$[ev;z]([j_{M_2',M_3}], [ev;y]([j_{M_1,M_2}],o_1,T),T')\rd_{\AA} [ev;z]([j_{M_1,M_3}],o_1,T')$$ $$ iff\spc M_2'\equiv_{\AA} M_2$$

\item eta-reduction. $$[\lambda;x](T_1,[ev;y](o,[x],T_2))\rd_{\AA} o\spc iff\, f\, and\, T\, do\, not\, depend\, on\, x$$

\item forallja-reduction. $$[forall_{M_1,M_2};x]([ev;z]([j_{M_0,M_1'}],o_1,T),o_2)\rd_{\AA} $$ $$ [ev;z]([j_{max(M_0,M_2),max(M_1,M_2)}], [forall_{M_0,M_2};x](o_1,o_2),\Eu_{max(M_1,M_2)})$$ $$\spc iff\spc M_1'\equiv_{\AA} M_1$$

\item foralljb-reduction. $$[forall_{M_1,M_3};x](o_1, [ev;z]([j_{M_2,M_3'}],o_2,T))\rd_{\AA} $$ $$ [ev;z]([j_{max(M_1,M_2),max(M_1,M_3)}], [forall_{M_1,M_2};x](o_1,o_2),\Eu_{max(M_1,M_3)})$$ $$\spc iff\spc M_3'\equiv_{\AA} M_3$$

\item iotatotal1-reduction. $$[pr1;y](T_1,T_2,[pair;x](o_1,o_2,T_2'))\rd_{\AA} o_1\spc iff\spc T_2[y/x]\sim_{\AA} T_2'$$

\item iotatotal2-reduction. $$[pr2;x](T_1,T_2',[pair;y](o_1,o_2,T_2'))\rd_{\AA} o_2\spc iff\spc T_2[y/x]\sim_{\AA} T_2'$$

\item etatotal-reduction. $$[pair;x]([pr1;y](T_1',T_2',o'),[pr2;y](T_1'',T_2'',o''),T_2)\rd_{\AA} o' $$ $$iff\spc o\equiv_{\AA} o'\spc and\spc T_2'[x/y]\sim_{\AA} T_2\sim_{\AA} T_2''[x/y]$$

\item totalja-reduction. $$[total_{M_1,M_2}]([ev;z]([j_{M_0,M_1'}],o_1,T),o_2)\rd_{\AA}$$ $$[ev;z]([j_{max(M_0,M_2),max(M_1,M_2)}], [total_{M_0,M_2};x](o_1,o_2),\Eu_{max(M_1,M_2)})$$ $$\spc iff\spc M_1'\equiv_{\AA} M_1$$

\item totaljb-reduction. $$[total_{M_1,M_3}](o_1,[ev;z]([j_{M_2,M_3'}],o_2,T))\rd_{\AA}$$ $$[ev;z]([j_{max(M_1,M_2),max(M_1,M_3)}], [total_{M_1,M_2};x](o_1,o_2),\Eu_{max(M_1,M_3)})$$ $$\spc iff\spc M_3'\equiv_{\AA} M_3$$

\item iotapt-reduction. $$[ev;x]([pt_r;y](o;T),tt,T')\rd_{\AA} o\spc iff\spc T'\sim_{\AA} T[x/y]$$

\item sum1-reduction. $$[sum;x](T_1,T_2,s_1,s_2,[ii1](T_1',T_2',o))\rd_{\AA} [ev;x](s_1,o,[\amalg](T_1,T_2))$$

\item sum2-reduction. $$[sum;x](T_1,T_2,s_1,s_2,[ii2](T_1',T_2',o))\rd_{\AA} [ev;x](s_2,o,[\amalg](T_1,T_2))$$

\item coprodja-reduction. $$[coprod_{M_1,M_2}]([ev;z]([j_{M_0,M_1}],o_1,T),o_2)\rd_{\AA} $$ $$[ev;z]([j_{max(M_0,M_2),max(M_1,M_2)}],[coprod_{M_0,M_2}](o_1,o_2),\Eu_{max(M_1,M_2)})$$ $$\spc iff\spc M_1\equiv_{\AA} M_1'$$

\item coprodjb-reduction. $$[coprod_{M_1,M_3}](o_1, [ev;z]([j_{M_2,M_3'}],o_2,T))\rd_{\AA} $$ $$[ev;z]([j_{max(M_1,M_2),max(M_1,M_3)}],[coprod_{M_1,M_2}](o_1,o_2),\Eu_{max(M_1,M_3)})$$ $$\spc iff\spc M_3\equiv_{\AA} M_3'$$

\item natO-reduction. $$[nat_r;x](o_1,o_2,O,T)\rd_{\AA} o_1$$

\item natS-reduction. $$[nat_r;x](o_1,o_2,[ev;y](S,n,\nn),T)\rd_{\AA} [ev;x]([ev;y](o_2, n, \nn), [nat_r;x](o_1,o_2,n,T), T)$$

\item pathsj-reduction. $$[paths_{M_2}]([ev;x]([j_{M_1,M_2'}],t,T),o_1,o_2)\rd_{\AA} [ev;x]([j_{M_1,M_2'}], [paths_{M_1}](t,o_1,o_2),T)$$ $$\spc iff\spc M_2\equiv_{\AA} M_2'$$

\item Jiota-reduction. $$[J;x,e](T,a,a',q,[refl](T',a''),S)\rd_{\AA} q\spc iff\spc a\equiv_{\AA} a'\equiv_{\AA} a''\spc and\spc T\sim_{\AA} T'$$

\item Elrr0-reduction.  $$[El][rr0_{M_2,M_1}](s,t,e)\rd_{\AA} [El](s)$$
%
\item forallrr0a-reduction. $$S=[forall_{M_1,M_2};x]([rr0_{M_3,M_1'}](s,t,e),o_2)$$ such that $M_1\equiv_{\AA} M_1'$ and $M_1'\le_{\AA} M_3$ reduces to
%
$$[rr0_{max(M_3,M_2),max(M_1,M_2)}]([forall_{M_3,M_2};x](s,o_2), S, idweq\, S)$$
%
\item forallrr0b-reduction. $$S=[forall_{M_1,M_2};x](o_1,[rr0_{M_3,M_2'}](s,t,e))$$ such that $M_2\equiv_{\AA} M_2'$ and $M_2'\le_{\AA} M_3$ reduces to
%
$$[rr0_{max(M_1,M_3),max(M_1,M_2)}]([forall_{M_1,M_3};x](o_1,s), S, idweq\, S)$$
%
\item totalrr0a-reduction. $$S=[total_{M_1,M_2};x]([rr0_{M_3,M_1'}](s,t,e),o_2)$$ such that $M_1\equiv_{\AA} M_1'$ and $M_1'\le_{\AA} M_3$ reduces to
%
$$[rr0_{max(M_3,M_2),max(M_1,M_2)}]([total_{M_3,M_2};x](s,o_2), S, idweq\, S)$$
%
\item totalrr0b-reduction. $$S=[total_{M_1,M_2};x](o_1,[rr0_{M_3,M_2'}](s,t,e))$$ such that $M_2\equiv_{\AA} M_2'$ and $M_2'\le_{\AA} M_3$ reduces to
%
$$[rr0_{max(M_1,M_3),max(M_1,M_2)}]([total_{M_1,M_3};x](o_1,s), S, idweq\, S)$$
%
\item coprodrr0a-reduction. $$S=[coprod_{M_1,M_2}]([rr0_{M_3,M_1'}](s,t,e),o_2)$$ such that $M_1\equiv_{\AA} M_1'$ and $M_1'\le_{\AA} M_3$ reduces to
%
$$[rr0_{max(M_3,M_2),max(M_1,M_2)}]([coprod_{M_3,M_2}](s,o_2), S, idweq\, X)$$
%
\item coprodrr0b-reduction. $$S=[coprod_{M_1,M_2}](o_1,[rr0_{M_3,M_2'}](s,t,e))$$ such that $M_2\equiv_{\AA} M_2'$ and $M_2'\le_{\AA} M_3$ reduces to
%
$$[rr0_{max(M_1,M_3),max(M_1,M_2)}]([coprod_{M_1,M_3}](o_1,s), S, idweq\, S)$$
%
\item pathsrr0-reduction. $$S=[paths_{M_1}]([rr0_{M_2,M_1'}](s,t,e),o_1,o_2)$$ such that $M_1\equiv_{\AA} M_1'$ and $M_1'\le_{\AA} M_2$ reduces to
%
$$[rr0_{M_2,M_1}]([paths_{M_2}](s,o_1,o_2), S, idweq\, S)$$
%
\item rr1rr0-reduction. $$[rr1_M](a,p)\rd_{\AA} [rr0_{M,0}](a, [rr1_M](a,p), idweq\,[rr1_M](a,p))$$
%
\item jrr0j-reduction. $$j_{M_1',M_3}\,[rr0_{M_2,M_1}](s,t,e)\rd_{\AA} j_{M_2,M_3}\,s$$ $$iff\spc M_1'\equiv_{\AA} M_1\spc and \spc M_1\le_{\AA} M_2\le_{\AA} M_3$$ 
\item jrr0rr0-reduction. $$j_{M_1',M_2}\,[rr0_{M_3,M_1}](s,t,e)\rd_{\AA} [rr0_{M_3,M_2}](s, j_{M_1,M_2}\,t,e)$$ $$iff\spc M_1'\equiv_{\AA} M_1\spc and\spc M_1\le_{\AA} M_2\le_{\AA} M_3$$
\item rr0jj-reduction. $$[rr0_{M_2,M_1}]((j_{M_0,M_2'}\,s), t, e)\rd_{\AA} j_{M_0,M_1}\,s$$ $$iff\spc M_2\equiv_{\AA} M_2'\spc and\spc M_0\le_{\AA} M_1\le_{\AA} M_2$$.
\item rr0jrr0-reduction. $$[rr0_{M_3,M_1}]((j_{M_2,M_3'}\,s), t, e)\rd_{\AA} [rr0_{M_2,M_1}](s,t,e)$$  $$iff\spc M_3\equiv_{\AA} M_3'\spc and \spc M_0\le_{\AA} M_1\le_{\AA} M_2$$
\item rr0rr0-reduction. $$[rr0_{M_2,M_1}]([rr0_{M_3,M_2'}](s,t_2,e_2),t_1,e_1)\rd_{\AA} [rr0_{M_3,M_1}](s,t_1,e_1)$$  $$iff\spc M_2\equiv_{\AA} M_2'\spc and \spc M_1\le_{\AA} M_2\le_{\AA} M_3$$
%
\item rr0MM-reduction. $$[rr0_{M,M'}](s,t,e)\rd_{\AA} s\spc iff\spc M\equiv_{\AA} M'$$ 
%


\end{enumerate}
















































































\comment{

\section{Expressions well formed relative to a parametrized relation}
%





\subsection{Main definitions}


Let $nn(E)$ be the number of nodes of an expression $E$.  We fix a finite set of u-level variables $Fu$ and an admissible subset ${\AA}$ of $\nn^{Fu}$.   We also fix an infinite linearly ordered set $Fv=\{v_1,\dots,v_n,\dots\}$ and let $Fv_n$ denote the subset $\{v_i\,|\,i\le n\}$ of $Fv$.

\begin{definition}
\llabel{cdef}
\begin{enumerate}
\item For $n\in nn$, a context $\Gamma$ of length $n$ is a sequence $\Gamma(1),\dots,\Gamma(n)$ where $\Gamma(i)\in TT0(Fu,FV,Fv_{i-1})$,
\item for a context $\Gamma$ of length $n$ and $i\le n$ we let $\Gamma_{\le i}$ denote the obvious truncation of $\Gamma$ to a context of length $i$,
\item for a context $\Gamma$ of length $n$ and $T\in TT0(Fu,FV,Fv_n)$ we let $\Gamma+T$ denote the context of length $n+1$ which equals $\Gamma$ on $1,\dots,n$ and $T$ on $n+1$.   
\end{enumerate}
\end{definition}
% 

In what follows we will consider families of relations $Q_{*,*}$ on $TS0(Fu,FV,Fv_*)$ parametrized by pairs $(n,\Gamma)$ where $n\ge 0$ and $\Gamma$ is a context of length $n$. We will call such families "parametrized relations" without mentioning specifically the parametrizing set.


%
\begin{definition}
\llabel{strwellf}
Let ${\AA}$ be an admissible subset and $Q_{*,*}$ be a family of relations parametrized by contexts as above. We define the family of subsets $W_{*,*}=WF(Q)_{*,*}$ which we call the subsets of terms well formed in $\Gamma$ relative to $Q_{*,*}$, by induction on $nn(E)$ as follows:
%
\begin{enumerate}
\item For any $(n,\Gamma)$ and a u-level expression $M$ one has $M\in W_{n,\Gamma}$.
%
\item For any $(n,\Gamma)$ one has $[El](s)\in W_{n,\Gamma}$ iff $s\in W_{n,\Gamma}$ and $(\tau_{\Gamma}(s), \Eu_M)\in Q_{n,\Gamma}$.
\item For any $(n,\Gamma)$ one has $[\prod;x](T_1,T_2)\in W_{n,\Gamma}$ iff: 
%
\begin{enumerate}
\item $T_1\in W_{n,\Gamma}$, 
\item $T_2[v_{n+1}/x]\in W_{n+1,\Gamma+T_1}$.
\end{enumerate}
%
\item For any $(n,\Gamma)$ and $i=1,\dots,n$ one has $[v_i]\in W_{n,\Gamma}$.
%
\item For any $(n,\Gamma)$ one has $[\cu_M]\in W_{n,\Gamma}$.
\item For any $(n,\Gamma)$ one has $[j_{M_1,M_2}]\in W_{n,\Gamma}$ iff for all $\vec{n}\in {\AA}$ one has $M_1(\vec{n})\le M_2(\vec{n})$.
%
\item For any $(n,\Gamma)$ one has $[ev;x](o_1,o_2,T)\in W_{n,\Gamma}$  iff:
%
\begin{enumerate}
\item $o_1, o_2\in W_{n,\Gamma}$, 
\item $T[v_{n+1}/x]\in W_{n+1,\Gamma+\tau_{\Gamma}(o_2)}$,
\item $(\tau_{\Gamma}(o_1), [\prod;x](\tau_{\Gamma}(o_2),T))\in Q_{n,\Gamma}$.
\end{enumerate}
% 
\item For any $(n,\Gamma)$ one has $[\lambda;x](T,o)\in W_{n,\Gamma}$ iff:
%
\begin{enumerate}
\item $T\in W_{n,\Gamma}$, 
\item $o[v_{n+1}/x]\in W_{n+1,\Gamma+T}$.
\end{enumerate}
%
\item For any $(n,\Gamma)$ one has $[forall_{M_1,M_2};x][o_1,o_2]\in W_{n,\Gamma}$ iff:
%
\begin{enumerate}
\item $o_1\in W_{n,\Gamma}$ and $(\tau_{\Gamma}(o_1),  \Eu_{M_1})\in Q_{n,\Gamma}$,
\item $o_2[v_{n+1}/x]\in W_{n+1,\Delta}$ where $\Delta=\Gamma+[El](o_1)$ and $(\tau_{\Delta}(o_2), \Eu_{M_2})\in Q_{n+1,\Delta}$.
\end{enumerate}
\end{enumerate}
\end{definition}
%


\begin{definition}
\llabel{wfcon}
A context $\Gamma$ of length $n$ is said to be well formed relative to a parametrized relation $Q_{*,*}$ if for each $j=1,\dots,n$ the term $\Gamma(j)$ is well formed in $\Gamma_{\le j-1}$ relative to $Q_{*,*}$.
\end{definition}
%










\subsection{Substitution invariant parametrized relations}
%

In this section we mainly consider properties of a fixed parametrized relation $Q_{*,*}$ and the notion of being well formed is always assumed to be relative to this relation.


\begin{lemma}
\llabel{contsub}
Let $\Gamma$ be a context of length $n$, $i=1,\dots,n$ and $s\in oT0(Fu,FV,Fv_i)$. Then the sequence $\Gamma(1)[s/v_i],\dots, \Gamma(n)[s/v_i]$ is again a context of length $n$ which we will denote by $\Gamma[s/v_i]$. In addition we have $(\Gamma[s/v_i])_{\le i}=\Gamma_{\le i}$.
\end{lemma}
%
\begin{proof}
Straightforward.
\end{proof}
%

%
\begin{definition}
\llabel{subinv}
A family of relations $Q_{*,*}$ on $TS0(Fu,FV,Fv_*)$  is called substitution invariant if for any $n$, any context $\Gamma$ of length $n$, any $(E,E')\in Q_{n,\Gamma}$, any $i\le n$, and any $s\in oT0(Fu,FV,Fv_i)$ which is well formed in $\Gamma_{\le i}$ and such that $\tau_{\Gamma_{\le i}}(s)=\Gamma(i)$, one has $(E[s/v_i], E'[s/v_i])\in Q_{n,\Gamma[s/v_i]}$.
\end{definition}
%

%
\begin{lemma}
\llabel{equivAinv}
For any admissible ${\AA}$ the family of relations $Q_{n,\Gamma}=(\equiv_{\AA})$ is substitution invariant.
\end{lemma}
%
\begin{proof}
Straightforward by induction on the number of nodes in an expression.
\end{proof}
% 
 
%
\begin{proposition}
\llabel{wfexpsub}
Let $Q_{*,*}$ be a parametrized relation which is substitution invariant. Then for any $(n,\Gamma)$, any $E$ which is well formed in $\Gamma$, any $i\le n$, and any $s\in oT0(Fu,FV,Fv_i)$ which is well formed in $\Gamma_{\le i}$ and satisfies the condition $\tau_{\Gamma_{\le i}}(s)=\Gamma(i)$, one has that $E[s/v_i]$ is well formed in $\Gamma[s/v_i]$.
\end{proposition}
%
\begin{proof}
Let $W_{n,\Gamma}$ be the subset of terms well formed in $\Gamma$ in $TS0(Fu,FV,Fv_n)$. Let $(n,\Gamma)$ be as above, $E\in W_{n,\Gamma}$, $i\le n$, $s\in oT0(Fu,FV,Fv_i)\cap W_{i,\Gamma_{\le i}}$ and $\tau_{\Gamma_{\le i}}(s)=\Gamma(i)$. We need to check that  $E[s/v_i]$ is well formed in $\Gamma[s/v_i]$ relative to $Q_{*,*}$. Proceed by induction on $nn(E)$. Let us consider the cases of Definition \ref{strwellf}:
%
\begin{enumerate}
\item If $E$ is a u-level expression then $E[s/v_i]=E$ is a u-level expression which is well formed in any context.
\item If $E=[El](o)$ then $E[s/v_i]=[El](o[s/v_i])$ where $o[s/v_i]\in W_{n,\Gamma[s/v_i]}$ by the inductive assumption. It remains to check that $(\tau_{\Gamma[s/v_i]}(E[s/v_i]), \Eu_M)\in Q_{n,\Gamma[s/v_i]}$. This follows from Lemma \ref{tausub0} and our condition on $Q_{*,*}$. 
\item If $E=[\prod;x](T_1,T_2)$ then $E[s/v_i]=[\prod;x](T_1[s/v_i],T_2[s/v_i])$ where by the inductive assumption $T_1[s/v_i]\in W_{n,\Gamma[s/v_i]}$ and 
%
$$(T_2[s/v_i])[v_{n+1}/x]=(T_2[v_{n+1}/x])[s/v_i]\in W_{n+1,(\Gamma+T_1)[s/v_i]}=W_{n+1,\Gamma[s/v_i]+T_1[s/v_i]}.$$
%
and we conclude that $E[s/v_i]\in W_{n,\Gamma[s/v_i]}$.
\item If $E=[v_j]$ then $E$ is well formed in any context.
%
\item Obvious.
\item Obvious.
\item If $E=[ev;x](o_1,o_2,T)$ and $i$, $s$ are as above we have by induction $o_1[s/v_i], o_2[s/v_i]\in W_{n,\Gamma[s/v_i]}$ and by induction and Lemma \ref{tausub0} we have
%
$$(T[s/v_i])[v_{n+1}/x]=(T[v_{n+1}/x])[s/v_i]\in W_{n+1,(\Gamma+\tau_{\Gamma}(o_2))[s/v_i]}=W_{n+1, \Gamma[s/v_i]+\tau_{\Gamma[s/v_i]}(o_2[s/v_i])}$$
% 
It remains to check that 
%
$$(\tau_{\Gamma[s/v_i]}(o_1[s/v_i]),[\prod;x](\tau_{\Gamma}(o_2[s/v_i]),T[s/v_i]))\in Q_{n,\Gamma[s/v_i]}$$
%
which follows from Lemma \ref{tausub0} and our condition on $Q_{*,*}$.
\item Same argument as in the case of $E=[\prod;x](\_,\_)$.
\item Similar to previous cases. 
\end{enumerate}
%
\end{proof}
%

\begin{cor}
\llabel{wfconsub}
Let $\Gamma$ be a context of length $n$ which is well formed relative to a substitutionally invariant parametrized relation $Q_{*,*}$. Let $i\le n$ and $s\in oT0(Fu,FV,Fv_i)\cap W_{i,\Gamma_{\le i}}$ be such that $\tau_{\Gamma_{\le i}}(s)=\Gamma(i)$. Then $\Gamma[s/v_i]$ is a well formed context relative to $Q_{*,*}$.
\end{cor}
%
\begin{proof}
We need to verify that for any $j=1,\dots,n$ we have $(\Gamma(j))[s/v_i]\in W_{j-1,(\Gamma_{\le j-1})[s/v_i]}$. By definition of a well formed context we have $\Gamma(j)\in W_{j-1,\Gamma_{\le j-1}}$. For $j\le i$, $\Gamma(j)$ does not contain $v_i$ and the assertion is obvious. For $i\le j-1$ the result follows from the definition of a substitution invariance of parametrized subsets applied to $(j-1,\Gamma_{\le j-1})$ and Proposition \ref{wfexpsub}.
\end{proof}


\begin{proposition}
\llabel{wftau}
Let $Q_{*,*}$ be a substitution invariant parametrized relation, $\Gamma$ a context of length $n$ well formed relative to $Q_{*,*}$ and $o\in oT0(Fu,FV,Fv_n)$ an term well formed in $\Gamma$ relative to $Q_{*,*}$. Then $\tau_{\Gamma}(o)$ is well formed in $\Gamma$ relative to $Q_{*,*}$.
\end{proposition}
%
\begin{proof}
We proceed by induction on the number of nodes in $o$ considering each of the cases of Definition \ref{dtau0} separately.
%
\begin{enumerate}
\item If $o=[v_i]$ then $\tau_{\Gamma}(o)=\Gamma(i)$ and our assertion follows from the definition of a well formed context.
\item If $o=[\cu_M]$ the assertion is obvious.
\item If $o=[j_{M_1,M_2}]$ the assertion is obvious.
\item If $o=[ev;x](o_1,o_2,T)$ then $\tau_{\Gamma}(o)=T[o_2/x]=(T[v_{n+1}/x])[o_2/v_{n+1}]$. By our assumption $T[v_{n+1}/x]$ is well formed in the context  $\Gamma+\tau_{\Gamma}(o_2)$ therefore by Proposition \ref{wfexpsub} $\tau_{\Gamma}(o)$ is well formed in $(\Gamma+\tau_{\Gamma}(o_2))[o_2/v_{n+1}]=\Gamma+\tau_{\Gamma}(o_2)$ and since $\tau_{\Gamma}(o)$ does not contain $v_{n+1}$ it is well formed in $\Gamma$. 
\item If $o=[\lambda;x](T,o')$ then $\tau_{\Gamma}(o)=[\prod;x](T,\tau_{\Gamma+T}(o'))$. We conclude that $\tau_{\Gamma}(o)$ is well formed since $T$ is well formed and $\tau_{\Gamma+T}(o')$ is well formed by the inductive assumption.
\item If $o=[forall_{M_1,M_2};x](o_1,o_2)$ then $\tau_{\Gamma}(o)=\Eu_{max(M_1,m_2)}$ which is well formed.
\end{enumerate}
%
Proposition is proved.
\end{proof}
%

\begin{lemma}
\llabel{equivAandQ}
Let $Q_{*,*}$ be a parametrized relation which is transitive and which contains $\equiv_{\AA}$. Then for any $\Gamma$, any $E$ which is well formed in $\Gamma$ relative to $Q_{*,*}$ and any $E'$ such that $E\equiv_{\AA} E'$ one has that $E'$ is well formed in $\Gamma$ relative to $Q_{*,*}$.
\end{lemma}
%
\begin{proof}
Straightforward, case by case of Definition \ref{strwellf}.
\end{proof}
%





\subsection{$\prod$-regular parametrized relations}
%
%
\begin{definition}
\llabel{prodreg}
A parametrized relation $Q_{*,*}$ is called $\prod$-regular if
%
\begin{enumerate}
\item for any $(n,\Gamma)$, any $(T_1,T_1')\in Q_{n,\Gamma}$ and any $(T_2,T_2')\in Q_{n+1,\Gamma+T_1}$ such that $\Gamma$ is well formed, $T_1$ is well formed in $\Gamma$ and $T_2$ is well formed in $\Gamma+T_1$, one has 
%
$$([\prod;x](T_1,T_2[x/v_{n+1}]), [\prod;x'](T_1',T_2'[x'/v_{n+1}]))\in Q_{n,\Gamma}$$
%
\item for any $(n, \Gamma)$ and any $T_1,T_1'\in oT0(Fu,FV,Fv_n)$, $T_2, T_2'\in oT0(Fu,FV,Fv_{n+1})$ such that $\Gamma$ is well formed, $T_1$ is well formed in $\Gamma$ and $T_2$ is well formed in $\Gamma+T_1$ and
%
$$([\prod;x](T_1,T_2[x/v_{n+1}]), [\prod;x'](T_1',T_2'[x'/v_{n+1}])\in Q_{n,\Gamma}$$
%
one has $(T_1,T_1')\in Q_{n,\Gamma}$ and $(T_2,T_2')\in Q_{n+1,\Gamma+T_1}$.
\end{enumerate}
\end{definition}
%
For contexts $\Gamma,\Gamma'$ of length $n$ and a parametrized relation $Q_{*,*}$ we will write $(\Gamma,\Gamma')\in Q$ if  for any $i\le n$ one has $(\Gamma(i),\Delta'(i))\in Q_{i-1,\Gamma_{\le i-1}}$.
%
\begin{lemma}
\llabel{newlemma}
Let $Q_{*,*}$ be a reflexive parametrized relation which satisfies the first part of Definition \ref{prodreg}. 
Then for any $n$, any contexts $\Gamma$, $\Gamma'$ of length $n$ such that $(\Gamma,\Gamma')\in Q$ and $\Gamma$ is well formed and any $E\in TS0(Fu,FV,Fv_{n})$ which is well formed in $\Gamma$, one has $(\tau_{\Gamma}(E), \tau_{\Gamma'}(E))\in Q_{n,\Gamma}$.
\end{lemma}
%
\begin{proof}
By induction on the number of nodes in $E$ considering the cases of Definition \ref{dtau0}.
%
\begin{enumerate}
\item $E=[v_i]$, follows from the assumption that $(\Gamma,\Gamma')\in Q$ since $(\tau_{\Gamma}(E),\tau_{\Gamma'}(E))=(\Gamma(i),\Gamma'(i))$.
\item $E=[\cu_M]$, obvious since $\tau_{\Gamma}(E)$ does not depend on $\Gamma$.
\item $E=[j_{M_1,M_2}]$, obvious since $\tau_{\Gamma}(E)$ does not depend on $\Gamma$.
\item $E=[ev;x](o_1,o_2,TT)$, obvious since $\tau_{\Gamma}(E)$ does not depend on $\Gamma$. 
\item $E=[\lambda;x](TT,o)$. Then 
%
$$\tau_{\Gamma}(E)=[\prod;x](TT, (\tau_{\Gamma+TT}(o[v_{n+1}/x]))[x/v_{n+1}])$$
$$\tau_{\Gamma'}(E)=[\prod;x](TT, (\tau_{\Gamma'+TT}(o[v_{n+1}/x]))[x/v_{n+1}])$$ 
%
Since $E$ is well formed in $\Gamma$ we know that $TT$ is well formed in $\Gamma$ and $o[v_{n+1}/x]$ is well formed in $\Gamma+TT$.  Since $\Gamma$ is well formed Proposition \ref{wftau} implies that $\tau_{\Gamma+TT}(o[v_{n+1}/x])$ is well formed in $\tau_{\Gamma+TT}$. By the inductive assumption $(\tau_{\Gamma+TT}(o[v_{n+1}/x]), \tau_{\Gamma'+TT}(o[v_{n+1}/x]))\in Q_{n+1,\Gamma+TT}$. Therefore the first case of Definition \ref{prodreg} applies and we conclude that $(\tau_{\Gamma}(E), \tau_{\Gamma'}(E))\in Q_{n,\Gamma}$.
%
\item $E=[forall_{M_1,M_2}](o_1,o_2)$, obvious since $\tau_{\Gamma}(E)$ does not depend on $\Gamma$.
\end{enumerate}
Lemma \ref{newlemma} is proved. 
\end{proof}
%
\begin{lemma}
\llabel{newlemma2}
Let $Q_{*,*}$ be a parametrized equivalence relation which satisfies the first part of Definition \ref{prodreg} and such that for any $n$, any contexts $\Gamma$, $\Gamma'$ of length $n$ such that $(\Gamma,\Gamma')\in Q$ and $\Gamma$, $\Gamma'$ are well formed, and any $(E,E')\in Q_{n,\Gamma}$ such that $E$ is well formed in $\Gamma$, one has $(E,E')\in Q_{n,\Gamma'}$. 

Then for any $\Gamma$, $\Gamma'$ as above and $E\in TS0(Fu,FV,Fv_{n})$ which is well formed in $\Gamma$ one has that $E$ is well formed in $\Gamma'$.
\end{lemma}
%
\begin{proof}
Proceed by induction on $nn(E)$. If $nn(E)=1$ then there are only two possibilities:
%
\begin{enumerate}
\item $E$ is a u-level term which is well formed in any context,
\item $E=[v_i]$ for some $i=1,\dots,n$ which is well formed in any context.
\end{enumerate}
%
Consider now the cases of Definition \ref{strwellf} corresponding to the case $nn(E)=N>1$:
%
\begin{enumerate}
\item $E=[El](s)$ where $s$ is well formed in $\Gamma$ and $(\tau_{\Gamma}(s),\Eu_M)\in Q_{n,\Gamma}$. We have $nn(s)=N-1$ and by the inductive assumption $s$ is well formed in $\Gamma'$. 

By Proposition \ref{wftau}, $\tau_{\Gamma}(s)$ is well formed in $\Gamma$ and Lemma \ref{newlemma} implies that $(\tau_{\Gamma}(s),\tau_{\Gamma'}(s))\in Q_{n,\Gamma}$. By our condition on $Q$ we conclude that  $(\tau_{\Gamma}(s),\tau_{\Gamma'}(s))\in Q_{n,\Gamma'}$. 
On the other hand $(\tau_{\Gamma}(s), \Eu_M)\in Q_{n,\Gamma}$ implies by the same condition that $(\tau_{\Gamma}(s), \Eu_M)\in Q_{n,\Gamma'}$. Using the fact that $Q_{n,\Gamma'}$ is an equivalence  we conclude that $(\tau_{\Gamma'}(s),\Eu_M)\in Q_{n,\Gamma'}$ and therefore $[El](s)$ is well formed in $\Gamma'$.
%
\item If $E=[prod;x](T_1,T_2)$ then by the inductive assumption $T_1$ is well formed in $\Gamma'$ and $T_2$ is well formed in $\Gamma'+T_1$. Therefore $E$ is well formed in $\Gamma'$.
%
\item If $E=[v_i]$ then $E$ is well formed in any context.
\item If $E=[\cu_M]$ then $E$ is well formed in any context.
\item If $E=[j_{M_1,M_2}]$ then the condition that $E$ is well formed does not depend on the context.
%
\item Let $E=[ev;x](o_1,o_2,T)$. By the inductive assumption $o_1$ and $o_2$ are well formed in $\Gamma'$. By Lemma \ref{newlemma} we have 
%
%
\begin{eq}
\llabel{eq1}
(\tau_{\Gamma}(o_1),\tau_{\Gamma'}(o_1))\in Q_{n,\Gamma}
\end{eq}
%
\begin{eq}
\llabel{eq2}
(\tau_{\Gamma}(o_2),\tau_{\Gamma'}(o_2))\in Q_{n,\Gamma}
\end{eq}
%
In particular, $(\Gamma+\tau_{\Gamma}(o_2), \Gamma'+\tau_{\Gamma'}(o_2))\in Q$ and by the inductive assumption $T[v_{n+1}/x]$ is well formed in $\Gamma'+\tau_{\Gamma'}(o_2)$. 

It remains to check that $(\tau_{\Gamma'}(o_1),[\prod;x](\tau_{\Gamma'}(o_2),T))\in Q_{n,\Gamma'}$. We do it in several steps:
%
\begin{enumerate}
\item $(\tau_{\Gamma}(o_1),\tau_{\Gamma'}(o_1))\in Q_{n,\Gamma}$ implies since $\tau_{\Gamma}(o_1)$ is well formed in $\Gamma$ that $(\tau_{\Gamma}(o_1),\tau_{\Gamma'}(o_1))\in Q_{n,\Gamma'}$ implies since $Q_{n,\Gamma'}$ is symmetric that   $(\tau_{\Gamma'}(o_1),\tau_{\Gamma}(o_1))\in Q_{n,\Gamma'}$. 
\item $(\tau_{\Gamma}(o_2),\tau_{\Gamma'}(o_2))\in Q_{n,\Gamma}$ implies since $\Gamma$ is well formed, $\tau_{\Gamma}(o_2)$ is well formed in $\Gamma$  and $T$ is well formed in $\Gamma+\tau_{phi}(o_2)$ that 
%
$$([\prod;x](\tau_{\Gamma}(o_2),T),[\prod;x](\tau_{\Gamma'}(o_2),T))\in Q_{n,\Gamma}$$
%
Since $[\prod;x](\tau_{\Gamma}(o_2),T)$ is well formed in $\Gamma$ we have
%
$$([\prod;x](\tau_{\Gamma}(o_2),T),[\prod;x](\tau_{\Gamma'}(o_2),T))\in Q_{n,\Gamma'}$$
%
\item Since $E$ is well formed in $\Gamma$ we have
%
$$(\tau_{\Gamma}(o_1),[\prod;x](\tau_{\Gamma}(o_2),T))\in Q_{n,\Gamma}$$
%
Since $\tau_{\Gamma}(o_1)$ is well formed we conclude that
%
$$(\tau_{\Gamma}(o_1),[\prod;x](\tau_{\Gamma}(o_2),T))\in Q_{n,\Gamma'}$$
%
Together with the previous two results and the fact that $Q_{n,\Gamma'}$ is  an equivalence relation we conclude that that $(\tau_{\Gamma'}(o_1),[\prod;x](\tau_{\Gamma'}(o_2),T))\in Q_{n,\Gamma'}$.  
\end{enumerate}
%
\item Let $E=[\lambda;x](T,o)$ where $T$ is well formed in $\Gamma$ and $o$ is well formed in $\Gamma+T$. By the inductive assumption we conclude that $o$ is well formed in $\Gamma'$. Furthermore, $\Gamma+T$ and $\Gamma'+T$ are both well formed and we conclude that $o$ is well formed in $\Gamma'+T$ by the inductive assumption. 
\item Let $E=[forall_{M_1,M_2};x](o_1,o_2)$ where $o_1$ is well formed in $\Gamma$,  $(\tau_{\Gamma}(o_1),\Eu_{M_1})\in Q_{n,\Gamma}$, $o_2[v_{n+1}/x]$ is well formed in $\Gamma+[El](o_1)$ and 
%
$$(\tau_{\Gamma+[El](o_1)}(o_2 [v_{n+1}/x]),\Eu_{M_2})\in Q_{n+1,\Gamma+[El](o_1)}$$
%
We need to check that all of these conditions hold with the replacement of $\Gamma$ by $\Gamma'$. We have that $o_1$ is well formed in $\Gamma'$ by the inductive assumption. By Lemma \ref{newlemma} we have
%
\begin{eq}
\llabel{eq3}
(\tau_{\Gamma}(o_1),\tau_{\Gamma'}(o_1))\in Q_{n,\Gamma}
\end{eq}
%
Since $Q_{n,\Gamma}$ is an equivalence we have $(\Eu_{M_1}, \tau_{\Gamma'}(o_1))\in Q_{n,\Gamma}$ and since $\Eu_{M_1}$ is well formed in $\Gamma$ we have $(\Eu_{M_1}, \tau_{\Gamma'}(o_1))\in Q_{n,\Gamma'}$ and by the symmetry $(\tau_{\Gamma'}(o_1), \Eu_{M_1})\in Q_{n,\Gamma'}$. 

By the inductive assumption  $[El](o_1)$ is well formed in $\Gamma'$. Therefore $\Gamma'+[El](o_1)$ is well formed and we conclude again by the inductive assumption that $o_2[v_{n+1}/x]$ is well formed in $\Gamma'+[El](o_1)$. 

It remains to check that
%
\begin{eq}
\llabel{eq5}
(\tau_{\Gamma'+[El](o_1)}(o_2[v_{n+1}/x]),\Eu_{M_2})\in Q_{n+1,\Gamma'+[El](o_1)}
\end{eq}
%
Since $\Gamma+[El](o_1)$ and $\Gamma'+[El](o_1)$ are both well formed and $o_2[v_{n+1}/x]$ is well formed in the first of these contexts we conclude that
%
$$(\tau_{\Gamma+[El](o_1)}(o_2[v_{n+1}/x]), \tau_{\Gamma'+[El](o_1)}(o_2[v_{n+1}/x]))\in Q_{n+1, \tau_{\Gamma+[El](o_1)}}$$
%
Since $\tau_{\Gamma+[El](o_1)}(o_2[v_{n+1}/x)$ is well formed in $\tau_{\Gamma+[El](o_1)}$ we conclude that
%
$$(\tau_{\Gamma+[El](o_1)}(o_2[v_{n+1}/x]), \tau_{\Gamma'+[El](o_1)}(o_2[v_{n+1}/x]))\in Q_{n+1, \tau_{\Gamma'+[El](o_1)}}$$
%
On the other hand since $\tau_{\Gamma+[El](o_1)}(o_2[v_{n+1}/x])$ is well formed in $\Gamma+[El](o_1)$ we conclude that
%
$$(\tau_{\Gamma+[El](o_1)}(o_2[v_{n+1}/x]),\Eu_{M_2})\in Q_{n+1,\Gamma'+[El](o_1)}$$
%
which implies (\ref{eq5}) since $Q_{n+1,\Gamma'+[El](o_1)}$ is an equivalence. 
\end{enumerate}
%
Lemma \ref{newlemma2} is proved.
\end{proof}
%






\subsection{Parametrized relations and reductions}
%

\begin{proposition}
\llabel{taured}
Let $Q_{*,*}$ be a parametrized equivalence relation satisfying the following conditions:
%
\begin{enumerate}
\item $Q_{*,*}$ contains $\equiv_{\AA}$,
\item $Q_{*,*}$ is substitution invariant,
\item $Q_{*,*}$ is $\prod$-regular,
\item if $\Gamma$ is well formed, $E$ is well formed in $\Gamma$ and $E\rde_{\AA} E'$ then $(E,E')\in Q_{n,\Gamma}$,
\end{enumerate}
%
Let $\Gamma$ be a well formed context, $E$ be an o-term well formed in $\Gamma$ and $E'$ an term obtained from $E$ by a one-step reduction. Then $(\tau_{\Gamma}(E),\tau_{\Gamma}(E'))\in Q_{n,\Gamma}$.
\end{proposition}
%
\begin{proof}
We proceed by induction on the number of nodes in $E$. Consider the cases of Definition \ref{dtau0} separately:
%
\begin{enumerate}
\item $E=[v_i]$. The $E'=E$ and the statement follows from reflexivity of $Q_{n,\Gamma}$.
\item $E=[\cu_M]$. Same as above.
\item $E=[j_{M_1,M_2}]$. The only non-trivial reduction is the jMM-reduction to $E'=[\lambda;x](\Eu_{M_1},[x])$. Then $\tau_{\Gamma}(E)\equiv_{\AA} \tau_{\Gamma}(E')$.
\item $E=[ev;x](o_1,o_2,T)$ where $o_1$, $o_2$ are well formed in $\Gamma$, $T[v_{n+1}/x]$ is well formed in $\Gamma+\tau_{\Gamma}(o_2)$  and $(\tau_{\Gamma}(o_1),[\prod;x](\tau_{\Gamma}(o_2),T))\in Q_{n,\Gamma}$. We have 
%
$$\tau_{\Gamma}(E)=T[o_2/x].$$
%
There are the following possibilities:
%
\begin{enumerate}
\item Reduction occurs in $o_1$. Then $\tau_{\Gamma}(E)=\tau_{\Gamma}(E')$.
\item Reduction occurs in $o_2$. Then $\tau_{\Gamma}(E)\rde_{\AA} \tau_{\Gamma}(E')$ by Lemma \ref{redsub03} and the claim follows by our condition on $Q_{*,*}$. 
\item Reduction occurs in $T$. Then $\tau_{\Gamma}(E)\rde_{\AA} \tau_{\Gamma}(E')$ by Lemma \ref{redsub01} and the claim follows by our condition on $Q_{*,*}$. 
\item Beta-reduction at the root. Then $o_1=[\lambda;y](T',o_1')$ and we have
%
$$\tau_{\Gamma}(o_1)=[\prod;y](T', \tau_{\Gamma+T'}(o_1'[v_{n+1}/y])[y/v_{n+1}])$$
$$\tau_{\Gamma}(E')=\tau_{\Gamma}(o_1'[o_2/y])$$
%
Since $Q$ is symmetric we have $([\prod;x](\tau_{\Gamma}(o_2),T), \tau_{\Gamma}(o_1))\in Q_{n,\Gamma}$. Since $Q_{*,*}$ is $\prod$-regular, $\Gamma$ is well formed, $\tau_{\Gamma}(o_2)$ is well formed in $\Gamma$ and $T[v_{n+1}/x]$ is well formed in $\Gamma+\tau_{\Gamma}(o_2)$ we have:
%
$$(\tau_{\Gamma}(o_2), T')\in Q_{n,\Gamma}$$
$$(T[v_{n+1}/x], \tau_{\Gamma+T'}(o_1'[v_{n+1}/y]))\in Q_{n+1,\Gamma+\tau_{\Gamma}(o_2)}$$
%
and since $Q_{*,*}$ is substitution invariant we have
%
$$(T[o_2/x], (\tau_{\Gamma+T'}(o_1'[v_{n+1}/y])[o_2/v_{n+1}]))\in Q_{n,\Gamma}$$
%
On the other hand by Lemma \ref{newlemma} and symmetry we have 
%
$$(\tau_{\Gamma+\tau_{\Gamma}(o_2)}(o_1'[v_{n+1}/y]), \tau_{\Gamma+T'}(o_1'[v_{n+1}/y]))\in Q_{n+1,\Gamma+\tau_{\Gamma}(o_2)}$$
%
and by substitution invariance:
% 
$$(\tau_{\Gamma}(o_1'[o_2/y]), (\tau_{\Gamma+T'}(o_1'[v_{n+1}/y]))[o_2/v_{n+1}])\in Q_{n,\Gamma}$$
%
and using symmetry and transitivity we conclude that
%
$$(T[o_2/x], \tau_{\Gamma}(o_1'[o_2/y])\in Q_{n,\Gamma}$$
%
\item jj-reduction at the root. Then $o_1=[j_{M_2',M_3}]$, $o_2=[ev;y]([j_{M_1,M_2}],o,\Eu_{M_2''})$ and 
%
$$\tau_{\Gamma}(E')=\tau_{\Gamma}([ev;x]([j_{M_1,M_3}],o,\Eu_{M_3'}))=\Eu_{M_3'}=\tau_{\Gamma}(E).$$ 
%
\end{enumerate}
%
\item $E=[\lambda;x](T,o)$, $\tau_{\Gamma}(E)=[\prod;x](T,\tau_{\Gamma+T}(o[v_{n+1}/x])[x/v_{n+1}])$. There are the following possibilities:
%
\begin{enumerate}
\item Reduction occurs inside $T$ i.e. $E'=[\lambda;x](T',o)$ where $T\rde_{\AA} T'$. Then 
%
$$\tau_{\Gamma}(E')=[\prod;x](T',\tau_{\Gamma+T'}(o[v_{n+1}/x])[x/v_{n+1}])$$
%
By our condition on $Q$ we have $(T,T')\in Q_{n,\Gamma}$. Therefore, by Lemma \ref{newlemma} we have 
%
$$(\tau_{\Gamma+T}(o[v_{n+1}/x]), \tau_{\Gamma+T'}(o[v_{n+1}/x]))\in Q_{n+1,\Gamma+T}$$
%
By the first part of $\prod$-regularity of $Q_{*,*}$ we conclude that 
%
$$([\prod;x](T,\tau_{\Gamma+T}(o[v_{n+1}/x])[x/v_{n+1}]), [\prod;x](T',\tau_{\Gamma+T'}(o[v_{n+1}/x])[x/v_{n+1}]))\in Q_{n,\Gamma}$$
%
\item Reduction occurs inside $o$ i.e. $E'=[\lambda;x](T,o')$ where $o\rde_{\AA} o'$.  Then 
%
$$\tau_{\Gamma}(E')=[\prod;x](T,\tau_{\Gamma+T}(o'[v_{n+1}/x])[x/v_{n+1}]))$$
%
By the inductive assumption $(\tau_{\Gamma+T}(o[v_{n+1}/x]),\tau_{\Gamma+T}(o'[v_{n+1}/x]))\in Q_{n+1,\Gamma+T}$ and by the first part of $\prod$-regularity of $Q_{*,*}$ we conclude that $(\tau_{\Gamma}(E),\tau_{\Gamma}(E'))\in Q_{n,\Gamma}$.
\item eta-reduction at the root i.e. $E=[\lambda;x](T, [ev;y](o', [x], T'))$ where $o'$ and $T'$ do not depend on $x$. Then 
%
$$\tau_{\Gamma}(E)=[\prod;x](T,T'[x/y])$$
$$\tau_{\Gamma}(E')=\tau_{\Gamma}(o')$$
%
By the condition that $E$ s well formed we have that $[ev;y](o', [x], T')$ is well formed in $\Gamma+T$. In particular,
%
$$(\tau_{\Gamma}(o'), [\prod;y](T, T'))\in Q_{n,\Gamma}$$
%
which implies the statement in this case.
\end{enumerate}
%
\item $E=[forall_{M_1,M_2};x](o_1,o_2)$, $\tau_{\Gamma}(E)=\Eu_{max(M_1,M_2)}$. There are the following possibilities:
%
\begin{enumerate}
\item Reduction occurs inside $o_1$ or $o_2$. Then $\tau_{\Gamma}(E)$ does not change.
\item forallja-reduction at the root. Then $\tau_{\Gamma}(E)$ does not change.
\item foralljb-reduction at the root. Then $\tau_{\Gamma}(E)$ does not change.
\end{enumerate}
\end{enumerate}
%
Proposition \ref{taured} is proved. 
\end{proof}



\begin{proposition}
\llabel{wftowf}
Let $Q_{*,*}$ be as in Proposition \ref{taured} and such that for any $n$, any contexts $\Gamma$, $\Gamma'$ of length $n$ such that $\Gamma$, $\Gamma'$ are well formed and $(\Gamma,\Gamma')\in Q$, and any $(E,E')\in Q_{n,\Gamma}$ such that $E$ is well formed in $\Gamma$ one has $(E,E')\in Q_{n,\Gamma'}$.  

Then for any well formed $\Gamma$,  any $E$ which is well formed in $\Gamma$ and any $E'$ such that $E\rde_{\AA} E'$, one has that $E'$ is well formed in $\Gamma$.
\end{proposition}
%
\begin{proof}
It is clearly sufficient to consider the one step reductions. We proceed by induction on the number of nodes in $E$ considering the possible root nodes of $E$ separately.
%
\begin{enumerate}
\item $E=M$ is an u-level expression. Then $E'=E$ and the statement is obvious.
\item $E=[El](s)$ where $s$ is well formed and $(\tau_{\Gamma}(s), \Eu_M)\in Q_{n,\Gamma}$. There are the following cases:
%
\begin{enumerate}
\item Reduction occurs inside $s$. Then $E'=[El](s')$ where $s\rde_{\AA} s'$. By the inductive assumption $s'$ is well formed in $\Gamma$. It remains to check that 
$(\tau_{\Gamma}(s'),\Eu_M)\in Q_{n,\Gamma}$. It follows from the symmetry and transitivity of $Q$ and Proposition \ref{taured}. 
\item Elj-reduction at the root. Then  $E=[El]([ev;x]([j_{M_0,M'}],o,\Eu_{M''}))$ where $M'\equiv_{\AA} M\equiv_{\AA} M''$ and $E=[El](o)$. We need to check that $(\tau_{\Gamma}(o), \Eu_{M_0})\in Q_{n,\Gamma}$. Since $E$ is well formed we have 
%
$$([\prod;x](\Eu_{M_0},\Eu_{M'}), [\prod;x](\tau_{\Gamma}(o),\Eu_{M''}))\in Q_{n,\Gamma}$$
%
and we conclude by the symmetry and the second part of $\prod$-regularity of $Q_{*,*}$. 
%
\item Elforall-reduction at the root. Then $E=[El][forall_{M_1,M_2};x](o_1,o_2)$ where $M\equiv_{\AA} max(M_1,M_2)$ and $E'=[\prod;x]([El](o_1),[El](o_2))$. The fact that $E'$ is well formed follows immediately from the fact that $[forall_{M_1,M_2};x](o_1,o_2)$ is well formed.
\end{enumerate}
%
\item $E=[\prod;x](T_1,T_2)$ where $T_1$ is well formed in $\Gamma$ and $T_2$ in $\Gamma+T_1$. There are the following cases:
%
\begin{enumerate}
\item Reduction occurs inside $T_1$ i.e. $E'=[\prod;x](T_1',T_2)$ where $T_1\rde_{\AA} T_1'$. By the inductive assumption $T_1'$ is well formed. We need to verify that $T_2$ is well formed in $\Gamma+T'$. This follows from Lemma \ref{newlemma2}.
%
\item Reduction occurs inside $T_2$. The statement follows from the inductive assumption. 
\end{enumerate}
%
\item $E=[v_i]$. Then $E'=E$ and the statement is obvious. 
\item $E=[\cu_M]$. Then $E'=E$ and the statement is obvious.
\item $E=[j_{M_1,M_2}]$. The only possible reduction is jMM-reduction at the root. Then $E'=[\lambda;x](\Eu_{M_1},[x])$ which is well formed.
%
\item $E=[ev;x](o_1,o_2,T)$ where $o_1$, $o_2$ are well formed in $\Gamma$, $T[v_{n+1}/x]$ is well formed in $\Gamma+\tau_{\Gamma}(o_2)$ and 
%
$$(\tau_{\Gamma}(o_1), [\prod;x](\tau_{\Gamma}(o_2),T))\in Q_{n,\Gamma}$$
%
There are the following possibilities:
%
\begin{enumerate}
\item $o_1\rde_{\AA} o_1'$. Then $o_1'$ is well formed by the inductive assumption, $o_2$ is well well formed and $T[v_{n+1}/x]$ is well formed in  $\Gamma+\tau_{\Gamma}(o_2)$. By Lemma \ref{taured} we have $(\tau_{\Gamma}(o_1),\tau_{\Gamma}(o_1'))\in Q_{n,\Gamma}$ and $(\tau_{\Gamma}(o_1'), [\prod;x](\tau_{\Gamma}(o_2),T)\in Q_{n,\Gamma}$ follows. 
%
\item $o_2\rde_{\AA} o_2'$. Then $o_1$ is well formed, $o_2'$ is well well formed by the inductive assumption. By Lemma \ref{taured} we have $(\tau_{\Gamma}(o_2),\tau_{\Gamma}(o_2'))\in Q_{n,\Gamma}$. Therefore $(\Gamma+\tau_{\Gamma}(o_2),\Gamma+\tau_{\Gamma}(o_2'))\in Q$ and $T[v_{n+1}/x]$ is well formed in $\Gamma+\tau_{\Gamma}(o_2')$ by Lemma \ref{newlemma2}. 

On the other hand, by the first part of $\prod$-regularity of $Q$ we conclude that $([\prod;x](\tau_{\Gamma}(o_2),T),[\prod;x](\tau_{\Gamma}(o_2'),T))\in Q_{n,\Gamma}$ and by transitivity of $Q_{n,\Gamma}$ we get that $(\tau_{\Gamma}(o_1), [\prod;x](\tau_{\Gamma}(o_2'),T)\in Q_{n,\Gamma}$.
%
\item $T\rde_{\AA} T'$. Then $o_1$, $o_2$ are well formed. and $T'$ is well formed by the inductive assumption.  The condition $(\tau_{\Gamma}(o_1), [\prod;x](\tau_{\Gamma}(o_2),T)\in Q_{n,\Gamma}$ follows from the first part of the $\prod$-regularity of $Q$.
%
\item Beta-reduction at the root. Then $o_1=[\lambda;y](T',o_1')$ and we have $E'=o_1'[o_2/y]$. Since $E$ is well formed so is $o_1$ and therefore $o_1'[v_{n+1}/x]$ is well formed in $\Gamma+T'$. By Proposition \ref{wfexpsub} it is sufficient to show that $o_1'[v_{n+1}/x]$ is well formed in $\Gamma+\tau_{\Gamma}(o_2)$. 

Since $E$ is well formed and $Q$ is symmetric we have $([\prod;x](\tau_{\Gamma}(o_2),T), \tau_{\Gamma}(o_1))\in Q_{n,\Gamma}$. Since $Q_{*,*}$ is $\prod$-regular we have $(\tau_{\Gamma}(o_2), T')\in Q_{n,\Gamma}$. Therefore $o_1'[v_{n+1}/x]$ is well formed in $\Gamma+\tau_{\Gamma}(o_2)$ by Lemma \ref{newlemma2}.
%
\item jj-reduction at the root. Then $o_1=[j_{M_2',M_3}]$, $o_2=[ev;y]([j_{M_1,M_2}],o,\Eu_{M_2''})$ and 
%
$$E'=[ev;x]([j_{M_1,M_3}],o,\Eu_{M_3'})$$ 
%
We need to check that $o$ is well formed and $([\prod;x](\Eu_{M_1},\Eu_{M_3}), [\prod;x](\tau_{\Gamma}(o), \Eu_{M_3'})\in Q_{n,\Gamma}$. This follows from $\prod$-regularity of $Q$ (both parts) and the assumption that $o_2$ is well formed.
\end{enumerate}
%
\item $E=[\lambda;x](T,o)$ where $T$ is well formed in $\Gamma$ and $o$ is well formed in $\Gamma+T$. There are the following possibilities:
%
\begin{enumerate}
\item $T\rde_{\AA} T'$. By the inductive assumption $T'$ is well formed in $\Gamma$. Hence both $\Gamma+T$ and $\Gamma+T'$ are well formed. Thus by Lemma \ref{newlemma2} we conclude that $o$ is well formed in $\Gamma+T'$. 
%
\item $o\rde_{\AA} o'$.  The result follows from the inductive assumption. 
%
\item eta-reduction at the root i.e. $E=[\lambda;x](T, [ev;y](o', [x], T'))$ where $o'$ and $T'$ do not depend on $x$. Then $E'=o'$ which is well formed by the assumptions. 
\end{enumerate}
%
\item $E=[forall_{M_1,M_2};x](o_1,o_2)$ where $o_1$ is well formed in $\Gamma$, $o_2[v_{n+1}/x]$ is well formed in $\Delta=\Gamma+[El](o_1)$ and $(\tau_{\Gamma}(o_1),\Eu_{M_1})\in Q_{n,\Gamma}$, $(\tau_{\Delta}(o_2),\Eu_{M_2})\in Q_{n,\Delta}$. There are the following possibilities:
%
\begin{enumerate}
\item $o_1\rde_{\AA} o_1'$. Then $o_1'$ is well formed in $\Gamma$ by the inductive assumption. We also see easily that $[El](o_1')$is well formed in $\Gamma$. Then  $\Gamma+[El](o_1')$ is well formed and $o_2$ is well formed in $\Gamma+[El](o_1')$ by Lemma \ref{newlemma2}.
\item $o_2\rde_{\AA} o_2'$. Then $\tau_{\Gamma}(E)$ does not change.
\item forallja-reduction at the root. Then $\tau_{\Gamma}(E)$ does not change.
\item foralljb-reduction at the root. Then $\tau_{\Gamma}(E)$ does not change.
\end{enumerate}
\end{enumerate}
%
Proposition \ref{wftowf} is proved. 
\end{proof}




\section{Definitional equality}
%

\subsection{Main definitions}

\begin{definition}
\llabel{qnphi}
Define a sequence of parametrized equivalence relations $Q_{n,\Gamma}^r$ by induction on $r$ as follows:
%
\begin{enumerate}
\item for any $(n,\Gamma)$, $Q^0_{n,\Gamma}$ is the relation $\equiv_{\AA}$ on $TS0(Fu,FV,Fv_n)$,
\item $Q^{r+1}_{*,*}$ is the smallest parametrized equivalence relation satisfying the following conditions:
%
\begin{enumerate}
\item for any $n$, $\Gamma$ one has $Q^r_{n,\Gamma}\subset Q^{r+1}_{n,\Gamma}$,
\item for any $n$, any $\Gamma$ which is well formed relative to $Q^r$, any $E\in TS0(Fu,FV,Fv_n)$ which is well formed in $\Gamma$ relative to $Q^r$ and any $E'$ such that $E\rde_{\AA} E'$ one has $(E,E')\in Q^{r+1}_{n,\Gamma}$,
\end{enumerate}
\end{enumerate}
\end{definition}
%





\begin{proposition}
\llabel{qrsubinv}
For any $r\ge 0$ the parametrized relation $Q^r_{*,*}$ is substitution invariant. 
\end{proposition}
%
\begin{proof}
We proceed by induction on $r$. For $r=0$ this is shown in Lemma \ref{equivAinv}.

Let $R^{r+1}_{*,*}$ be the parametrized relation where $(E,E')\in R^{r+1}_{n,\Gamma}$ iff $(E,E')\in Q^{r+1}_{n,\Gamma}$ and for any $i\le n$, and any $s\in oT0(Fu,FV,Fv_i)$ such that $s$ is well formed in $\Gamma_{\le i}$ relative to $Q^{r+1}_{*,*}$ and $\tau_{\Gamma_{\le i}}(s)=\Gamma(i)$, one has $(E[s/v_i], E'[s/v_i])\in Q^{r+1}_{n,\Gamma[s/v_i]}$. We need to show that $R^{r+1}_{*,*}$ satisfies the defining conditions of $Q^{r+1}_{*,*}$. The reflexivity, symmetry and transitivity are obvious. 

To verify the reduction rule for $R^{r+1}_{*,*}$ we need to show that for any $n$, any $\Gamma$ which is well formed relative to $Q^r$, any $E$ which is well formed in $\Gamma$ relative to $Q^r$, any $E'$ such that $E\rde_{\AA} E'$, any $i\le n$, and any $s\in oT0(Fu,FV,Fv_i)$ which is well formed in $\Gamma_{\le i}$ relative to $Q^{r+1}$ and such that $\tau_{\Gamma_{\le i}}(s)=\Gamma(i)$, one has $(E[s/v_i], E'[s/v_i])\in Q^{r+1}_{n,\Gamma[s/v_i]}$.

By the inductive assumption $Q^r_{*,*}$ is substitution invariant and therefore by Proposition \ref{wfexpsub} we conclude that $E[s/v_i]$ is well formed in $\Gamma[s/v_i]$ relative to $Q^r$.  In view of the reduction rule for $Q^{r+1}_{*,*}$ it remains to verify that $E[s/v_i]\rde_{\AA} E'[s/v_i]$ which follows from Lemma \ref{redsub01}.
\end{proof}
%

\begin{lemma}
\llabel{qrsimpl}
Let $r\ge 1$ and $(E,E')\in Q^r_{n,\Gamma}$. Then one of the following two possibilities occurs:
%
\begin{enumerate}
\item $E\equiv_{\AA} E'$,
\item there are terms $F$, $F'$ such that $F$ is well formed in $\Gamma$ relative to $Q^{r-1}$ and $F\rde_{\AA} F'\equiv_{\AA} E'$
\end{enumerate}
\end{lemma}
%
\begin{proof}
If $(E,E')\in Q^r_{n,\Gamma}$ then there is a chain of the form $E_1,\dots,E_l$ where $E_1=E$, $E_l=E'$ and for each $i=2,\dots,l$ one of the following holds:
%
\begin{enumerate}
\item $E_{i-1}\equiv_{\AA} E_{i}$,
\item $E_{i-1}$ is well formed in $\Gamma$ relative to $Q^{r-1}$ and $E_{i-1}\rde_{\AA} E_{i}$,
\item $E_{i}$ is well formed in $\Gamma$ relative to $Q^{r-1}$ and $E_{i}\rde_{\AA} E_{i-1}$.
\end{enumerate}
%
Proceed by induction on $l$. For $l=1$ we have $E=E'$. For $l\ge 2$ consider the two cases which may occur for the chain $E_1,\dots,E_{l-1}$:
%
\begin{enumerate}
\item $E_1\equiv_{\AA} E_{l-1}$. Consider the possible forms of the link $(E_{l-1},E_l)$. If $E_{l-1}\equiv_{\AA} E_l$ then $E_1\equiv_{\AA} E_l$. If the second case occurs then we set $F=E_{l-1}$, $F'=E_l$. If the third case occurs we set $F=F'=E_l$. 
%
\item Let $F_0, F'_0$ be the terms which satisfy the conditions of the lemma for the chain $E_1,\dots,E_{l-1}$. Consider the possible forms of the link $(E_{l-1},E_l)$. If the first of the three possibilities listed above occurs for $(E_{l-1},E_{l})$ we take $F=F_0$ and $F'=F_0'$.  If the second one occurs we take $F=E_{l-1}$ and $F'=E'$. If the third one occurs we take $F=F'=E_l$.
\end{enumerate}
\end{proof}
%



%??? many a mess below

\begin{theorem}
\llabel{tauequiv}
The following holds for any $r\ge 0$:
%
\begin{enumerate}
\item If $E$ is well formed in $\Gamma$ relative to $Q^r$ then $\tau_{\Gamma}(E)$ is well formed in $\Gamma$ relative to $Q^r$,
\item If $(E,E')\in Q^r_{n,\Gamma}$ then $(\tau_{\Gamma}(E),\tau_{\Gamma}(E'))\in Q^r_{n,\Gamma}$.
\end{enumerate}
%
\end{theorem}
%
\begin{proof}
We proceed by induction on $r$. Consider first the case $r=0$. 

The first assertion is the conclusion of Lemma \ref{wfeqA}.

Let $\Gamma$ be a context of length $n$ and $E\in oT0(Fu,FV,Fv_n)$ be such that $E$ is  well formed in $\Gamma$ relative to $\equiv_{\AA}$. We want to show that $\tau_{\Gamma}(E)$ is well formed in $\Gamma$ relative to  $\equiv_{\AA}$. Proceed by induction on $nn_{\Gamma}(E)$. Consider various cases of Definition \ref{dtau0}:
%
\begin{enumerate}
\item $E=[v_i]$ for $i\le n$. Then $\tau_{\Gamma}(E)=\Gamma(i)$ which is well formed by Definition \ref{strwellf}(4).
\item $E=[\cu_M]$. Then $\tau_{\Gamma}(E)=\Eu_{M+1}$ which is well formed in any $\Gamma$ relative to any family of reflexive relations,
\item $E=[j_{M_1,M_2}]$. Again $\tau_{\Gamma}(E)$ is well formed in any $\Gamma$ relative to  any family of reflexive relations.
\item $E=[ev;x](o_1,o_2,T)$. Then $\tau_{\Gamma}(E)=T[o_2/x]$. Since $E$ is well formed in $\Gamma$ relative to $\equiv_{\AA}$ we have $\tau_{\Gamma}(o_1)\equiv_{\AA} [\prod;x](\tau_{\Gamma}(o_2),T)$. By the inductive assumption (on $nn_{\Gamma}(E)$) $\tau_{\Gamma}(o_1)$ is well formed in $\Gamma$ relative to $\equiv_{\AA}$. 

By the first assertion we conclude that $[\prod;x](\tau_{\Gamma}(o_2),T)$ is well formed in $\Gamma$ relative to $\equiv_{\AA}$. 

By definition this implies that $T[v_{n+1}/x]$ is well formed relative to $\equiv_{\AA}$ and the context $\Delta$ which coincide with $\Gamma$ on $1,\dots,n$ and such that $\Delta(n+1)=\tau_{\Gamma}(o_2)$. Then $T[o_2/x]=(T[v_{n+1}/x])[o_2/v_{n+1}]$ which we conclude to be well formed relative to $\Gamma$ by Lemmas \ref{winvifqinv} and \ref{equivAinv} and the fact that $o_2$ does not depend on $x$. 
\item $E=[\lambda;x](T,o)$. Then $\tau_{\Gamma}(E)=[\prod;x](T,\tau_{\Delta}(o))$. We have that $T$ is well formed by the assumption that $E$ is well formed and $\tau_{\Delta}(o)$ is well formed by the assumption that $E$ is well formed and by the inductive assumption on $nn_{*}(*)$. 
\item $E=[forall_{M_1,M_2};x](o_1,o_2)$. Then $\tau_{\Gamma}(E)=\Eu_{max(M_1,M_2)}$ which is obviously well formed.
\end{enumerate}
%
The third assertion for $n=0$ is straightforward.

Let us consider now the case $r+1$. In view of Lemma \ref{intl2} and the inductive assumption 



it is sufficient to show that if $E$ is well formed relative to $Q^{r+1}_{*,*}$ and $\Gamma$ and $E'$ is such that $E\rde_{\AA} E'$ then $E'$ is well formed relative to $Q^{r+1}_{*,*}$ and $\Gamma$. It is clearly sufficient to consider the case when $E\rde_{\AA} E'$ is one of the one step reductions of Definition \ref{drd0}. We proceed by induction on $nn_{\Gamma}(E)$ and consider the cases presented by the possible roots of $E$:
%
\begin{enumerate}
\item If $E$ is a u-level expression then $E'=E$ and there is nothing to prove.
\item Let $E=[El](o)$. We have the following cases:
%
\begin{enumerate}
\item Reduction occurs inside $o$. Then $o\rde_{\AA} o'$ and by induction on $nn_*(*)$ we know that $X'$ is well formed relative to $\Gamma$ and $Q^{r+1}_{*,*}$


\end{enumerate}
\end{enumerate} 

\end{proof}



We let $\erd{\Gamma}$ denote the union of relations $Q^r_{n,\Gamma}$ for given $Fu$ and ${\AA}$. We will say that $E$ is well formed relative to $\Gamma$ if it is well formed relative to $\erd{*}$ and $\Gamma$. 
%
\begin{lemma}
\llabel{wfeq}
Let $n$, $\Gamma$ and $E$ be such that $E$ is well formed relative to $\Gamma$ (and $\erd{*}$). Then there exists $r$ such that $E$ is well formed relative to $\Gamma$ and $Q^r_{*,*}$.
\end{lemma}
%
\begin{proof}
Straightforward by induction on $nn_{\Gamma}(E)$ and case-by-case verification for each of the possibilities of Definition \ref{strwellf}.
\end{proof}
%
\begin{lemma}
\llabel{erdprop}
The relations $\erd{*}$ have the following properties:
%
\begin{enumerate}
\item they are reflexive, symmetric and transitive,
\item for any $(n,\Gamma)$, any $E$ which is well formed relative to $\Gamma$ and $\erd{*}$, and any $E'$ such that $E\rde_{\AA} E'$ one has $E\erd{\Gamma} E'$,
\end{enumerate}
\end{lemma}
%
\begin{proof}
The first assertion is straightforward. The second is straightforward with the use of Lemma \ref{wfeq}.
\end{proof}
%
\begin{lemma}
\llabel{eqsubinv}
The parametrized relation $\erd{*}$ is substitution invariant.
\end{lemma}
%


























}


\comment{


\newpage


such that the square
%
$$
\begin{CD}
\uu{Hom}_U(\tilde{U},\uu{U}\times \tilde{U}) @>\Lambda>> \tilde{U}\\
@VVV @VVV\\
\uu{Hom}_U(\tilde{U},\uu{U}\times U) @>\Pi>> U
\end{CD}
$$
%
where the left vertical morphism is defined by the display map $\tilde{U}\sr U$, is a pull-back square. 
%
In the context when there are universes $\UU n$ for various $n$ the proper behavior 

For our purposes we need to have a notation for the type expression generated by a given "inductive definition". We will write 
%
\begin{eq}
\llabel{eq2}
\ind\, X : (\vec{a}:\vec{A})||(\vec{pa}:\vec{PA}), \UU n ||\{ C^{(1)}| \dots C^{(nc)}\}
\end{eq}
%
for the inductive type defined by (\ref{eq1}). Note that $X$ is a bound variable in this expression so that it can be used inside Coq code in the form
%
$$Definition\,\,\, Y := Ind\, X : (\vec{a}:\vec{A})||(\vec{pa}:\vec{PA}) \UU n ||\{ C^{(1)}| \dots |C^{(nc)}\}.$$
%

}
















\section{Adding the natural numbers - system TS5}
%

\subsection{TS5 terms and typing function}
%
\begin{definition}
\llabel{d51}
The following labels are permitted in the expressions of TS5 - the labels permitted in TS4,  $nat$, $O$, $S$, $nat_r$.
\end{definition}
%
The notions of u-level expressions, T- and o- terms in TS5 are defined as follows:
%
\begin{definition}
\llabel{d52}
\begin{enumerate}
\item expressions with the root node caring a TS4-label is an u-level expression, o-expression or a T-expression according to the rules of Definition \ref{d42},
\item expressions with the root of the form $[nat]$, $O$, $S$ and $[nat_r;x]$ are o-expressions,
\end{enumerate}
\end{definition}
%
%
\begin{definition}
\llabel{d53}
A TS5-term is a TS5-expression such that:
%
\begin{enumerate}
\item any node caring one of the TS4-labels satisfies the conditions of Definition \ref{d33},
\item any node of the form $[nat]$ has valency $0$, 
\item any node of the form $[O]$ has valency $0$,
\item any node of the form $[S]$ has valency $0$,
\item any node of the form $[nat_r]$ has valency $4$, its first three branches are o-expressions which do not contain $x$ and the fourth branch a T-expression.
\end{enumerate}
\end{definition}
%
\begin{definition}
\llabel{d54}
A node in TS5 term is called non-essential if it satisfies the conditions of Definition \ref{d14}. The same applies to the definition of essential nodes, essential and non-essential subexpressions and of $Ess(E)$ is extended to TS5-terms in the obvious way. 
\end{definition}
%
We let $TS5$ denote the set of TS5-terms and $TT5$ and $oT5$ denote the subsets of T-terms and o-terms.
The obvious analog of Lemma \ref{l02} holds for TS5-expressions. We extend to TS5 the abbreviations introduced for TS4-expressions and also abbreviate $[El][nat]$ as $\nn$. 
%
\begin{definition}
\llabel{dtau5}
Under the assumptions of Definition \ref{dtau0} we extend the typing function $\tau_{\Gamma}$ to o-terms of TS5 as follows:
%
\begin{enumerate}
\item the value of $\tau_{\Gamma}$ on an o-term whose root node carries a TS4-label is computed according to the rules of Definition \ref{dtau4}.
\item $\tau_{\Gamma}([nat])=\Eu_0$,
\item $\tau_{\Gamma}([O])=\nn$,
\item $\tau_{\Gamma}([S])=[\prod;x](\nn,\nn)$,
\item $\tau_{\Gamma}([nat_r;x](o_1,o_2,o_3,T))=T$.
\end{enumerate}
\end{definition}
%
We have the obvious analog of Proposition \ref{tausub0} for TS5.


\subsection{Equivalence relations $\equiv_{\AA}$ and $\sim_{\AA}$ on TS5-terms}
%
The relations $\equiv_{\AA}$ and $\sim_{\AA}$ are extended to TS1-terms in the obvious way. We also have obvious analogs of all the statements of Section \ref{sim0}.



\subsection{Reducibility relation on TS5 terms}
%

\begin{definition}
\llabel{drd5}
Let $UC=(Fu,{\AA})$ be universe context and $FV$ a sequence of T-variables. Define a relation $\rd_{\AA}$ on $TS5(Fu,FV,Fv)$ for all $Fv$ as the transitive closure of  the union of the following reduction relations:
%
\begin{enumerate}
\item Reductions of Definition \ref{drd3}.
%
\item natO-reduction. An essential subterm of the form $[nat_r;x](o_1,o_2,O,T)$ reduces to $o_1$,
\item natS-reduction. An essential subterm of the form $[nat_r;x](o_1,o_2,[ev;y](S,n,\nn),T)$ reduces to $[ev;x]([ev;y](o_2, n, \nn), [nat_r;x](o_1,o_2,n,T), T)$.
\end{enumerate}
\end{definition}
%

The obvious analogs of Lemmas \ref{redsub01}-\ref{lequivsimred0} hold for TS5.






\subsection{Local confluence for general terms of TS5}
%
There are no new confluence situations for TS5 compared with TS5. 



\subsection{Derivation rules of TS5}
%
The derivation rules for contexts and judgements of TS5 are the derivation rules for TS4 together with the following additional ones:
%
$$\frac{\Gamma\vdash}{\Gamma\vdash nat:\Eu_0}$$
%
$$\frac{\Gamma\vdash}{\Gamma\vdash O:\nn}$$
%
$$\frac{\Gamma\vdash}{\Gamma\vdash S:[\prod;x](\nn,\nn)}$$

$$\frac{\Gamma, x:\nn, y:T\vdash\spc 
%
\begin{array}{c}
\Gamma\vdash o_1:T[O/x]\\
\Gamma\vdash o_2:[\prod;x](\nn, [\prod;y](T, T[[ev;z](S,x,\nn)/x]))
\end{array}
%
\spc \Gamma\vdash n:\nn}{\Gamma \vdash [nat_r;x](o_1,o_2,n,T):T[n/x]}$$





\bibliography{../../../alggeom}
\bibliographystyle{plain}



\end{document}








\section{Introduction}
