\documentclass[11pt]{article}
\usepackage{graphicx}
\usepackage{amscd, amssymb}

\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}




\begin{document}
%
\parskip = 2mm
\begin{center}
{\bf\Large Notes on type systems}

{\bf Vladimir Voevodsky}

{Started September 08, 2009}  
\end{center}


\paragraph{Free systems of expressions.} Let $M$ be a set and let $T(M)$ be the set of finite rooted trees whose vertices (including the root) are labeled by elements of $M$ and such that for any vertex the set of edges leaving this vertex is ordered. Note that such ordered trees have no symmetries. We will use the following notations. For $T\in T(M)$ let $Vrtx(T)$ be the set of vertices of $T$ and for $v\in Vrtx(T)$ let $lbl(v)=lbl(v)_T\in M$ be the label on $v$. We will sometimes write $v\in T$ instead of $v\in Vrtx(T)$. For $v\in Vrtx(T)$ let $[v]=[v]_T\in T(M)$ be the subtree in $T$ which consists of $v$ and all the vertices under $v$. Let $val(v)$ be the valency of $v$ i.e. the number of edges leaving $v$ and $ch_1(v),\dots,ch_{val(v)}(v)\in Vrtx(T)$ be the "children" of $v$ i.e. the end points of these edges. Let further $br_i(v)=[ch_i(v)]$ be the branches of $[v]$. We write $v\le w$ (resp. $v<w$) if $v\in [w]$ (resp. $v\in [w]-w$). We say that two vertices $v$ and $w$ are independent if $v\notin [w]$ and $w\notin [v]$.  

For three sets $A, B$ and $Cont$ let 
%
$$AllExp(A,B;Con)=T(A\amalg B\amalg (Con\times (\amalg_{n\ge 0} B^n)))$$
%
Elements of $AllExp(A,B;Con)$ are called expressions over the alphabet $Con$ (or with a set of constructors $Con$), free variables from $A$ and bound variables from $B$. 

An expression is called unambiguous if it satisfies the following conditions:
%
\begin{enumerate}
\item if $lbl(v)\in A\amalg B$ then $val(v)=0$,
\item 
%
\begin{enumerate}
\item if  $v< v'$, $lbl(v)=(c;x_1,\dots,x_n)$ and $lbl(v')=(c';x_1',\dots,x_{n'}')$ then\\ $\{x_1,\dots,x_n\}\cap \{x_1',\dots,x_{n'}'\}=\emptyset$,
\item if $lbl(v)=(c;x_1,\dots,x_n)$ then $x_i\ne x_j$ for $i\ne j$,
\end{enumerate}
\item if $lbl(v)=(c;x_1,\dots,x_n)$ and $lbl(v')\in \{x_1,\dots,x_n\}$ then $v'\in [v]$.
\end{enumerate}
%
The first conditions says that a vertex labeled by a variable is a leaf. The second one is equivalent to saying that if the same variable is bound at two different vertices $v,v'$ then these vertices are independent i.e. $[v]\cap [v']=\emptyset$ and that a vertex can not bind the same variable twice.  The third one says that all the leaves labeled by a bound variable lie under the vertex where it is boud. We let $UAExp(A,B;Con)$ denote the subset of unambiguous expressions in $AllExp(A,B;Con)$.  Note that for for any $T\in UAExp(A,B;Con)$ and $v\in Vrtx(T)$ there is a subset $Ext(v)\subset B$ such that 
%
$$[v]\in UAExp(A\amalg Ext(v),B\backslash Ext(v);Con)$$

Any triple of maps $f_{Con}:A\sr A'$, $f_B:B\sr B'$, $f_{Con}:Con\sr Con'$ define a map 
%
$$f_*=(f_A,f_B,f_{Con})_*:AllExp(A,B;Con)\sr AllExp(A',B';Con')$$
%
which changes labels in the obvious way. If $f_B$ is  injective then $f_*$ maps unambiguous expressions to unambiguous ones. 

An element $T$ of $UAExp(A,B;Con)$ is said to be strictly unambiguous if for any $v\ne v'$ in $Vrtx(T)$ such that $lbl(v)=(c;x_1,\dots,x_n)$ and $lbl(v')=(c';x_1',\dots,x_{n'}')$ one has $\{x_1,,\dots,x_n\}\cap \{x_1',\dots,x_{n'}'\}=\emptyset$ i.e. if the names of all bound variables are different. We let $SUAExp(A,B;Con)$ denote the subset of strictly unambiguous expressions in $UAExp(A,B;Con)$. 

An element $T$ of $UAExp(A,B;Con)$ is said to be $\alpha$-equivalent to an element $T'$ of $UAExp(A,B';Con)$ if there is a set $B''$ , an element $T''\in UAExp(A,B'';Con)$ and two maps $f:B''\sr B$, $f':B''\sr B'$ such that $T=(Id,f,Id)_*(T'')$ and $T'=(Id,f',Id)_*(T'')$. The following lemma is straightforward:
%
\begin{lemma}
\llabel{2009.09.08.l1}
For any two sets $A$ and $Con$ one has:
%
\begin{enumerate}
\item $\alpha$-equivalence is an equivalence relation,
\item for any set $B$ and any element $T\in UAExp(A,B;Con)$ there exists an element\\ $T'\in UAExp(A,\nn;Con)$ such that $T\alphaeq T'$ and $T'$ is strictly unambiguous, 
\item fwo strictly unambiguous elements $T,T'\in UAExp(A,B;Con)$ are $\alpha$-equivalent if and only if there exists a permutation $f:B\sr B$ such that $(Id,f,Id)_*(T)=T'$.
\end{enumerate}
\end{lemma}
%
We let $Exp_{\alpha}(A;Con)$ denote the set of $\alpha$-equivalence classes in $\amalg_{B} UAExp(A,B;Con)$. In view of Lemma \ref{2009.09.08.l1} this set is well defined and can be also defined as the set of equivalence classes in $SUAExp(A,\nn;Con)$ modulo the equivalence relation generated by the permutations on $\nn$. 

Note that for two $\alpha$-equivalent expressions $T_1,T_2$ and a vertex $v\in V(T_1)=V(T_2)$ the expressions $[v]_{T_1}$ and $[v]_{T_2}$ need not be $\alpha$-equivalent since some of the variables which are bound in $T_1$ may be free in $[v]$. 

The maps $(f_A,f_B,f_{Con})_*$ respect $\alpha$-equivalence. Therefore for any $f_A:A\sr A'$ and $f_{Con}:Con\sr Con'$ there is a well defined map
%
$$(f_A,f_{Con})_{*}:Exp_{\alpha}(A;Con)\sr Exp(A';Con')$$
%
which make $Exp_{\alpha}(-;-)$ into a covariant functors from pairs of sets to sets. In addition there is a well defined notion of substitution on $Exp_{\alpha}(-;Con)$ which may be considered as a collection of maps of the form:
%
$$Exp_{\alpha}(A;Con)\times (\prod_{a\in A} Exp_{\alpha}(X_a;Con))\sr Exp_{\alpha}(\amalg_{a\in A} X_a;Con)$$
%
given for all pairs $(A;\{X_a\}_{a\in A})$ where $A$ is a set and $\{X_a\}_{a\in A}$ a family of sets parametrized by $A$. Alternatively, the substitution structure can be seen as a collection of maps
%
$$Exp_{\alpha}(Exp_{\alpha}(A;Con);Con)\sr Exp_{\alpha}(A;Con)$$
%
given for all $A$ and $Con$. These maps make the functor $Exp_{\alpha}(-;Con)$ into a monad (triple) on the category of sets which functorially depends on the set $Con$. 

%
\begin{example}\rm
\llabel{lambda}
The mapping which sends a set $X$ to the set of $\alpha$-equivalence classes of terms of the untyped $\lambda$-calculus with free variables from $X$ is a sub-triple of $Exp_{\alpha}(-;Con)$ where $Con=\{\lambda, ev\}$. Elements $T$ of $UAExp(X,\nn;\{\lambda,ev\})$ which belong to this sub-triple are characterized by the following "local" conditions:
%
\begin{enumerate}
\item for each $v\in T$, $lbl(v)\in X\amalg \nn\amalg \{ev\}\amalg \{\lambda\}\times \nn$
\item if $lbl(v)\in \{\lambda\}\times \nn$ then $val(v)=1$
\item if $lbl(v)=ev$ then $val(v)=2$.
\end{enumerate}
%
\end{example}
%
\begin{example}\llabel{propositional}\rm
The mapping which sends a set $X$ to the set of  terms of the propositional calculus with free variables from $X$ is a sub-triple of $Exp_{\alpha}(-;C_0)$ where $C_0=\{\vee,\wedge,\urcorner,\Rightarrow\}$.  Elements $T$ of $UAExp(X,\nn;C_0)$ which belong to this sub-triple are characterized by the following "local" conditions:
%
\begin{enumerate}
\item for all $v\in T$, $lbl(v)\in X\amalg C_0$
\item if $lbl(v)\in \{\vee,\wedge,\Rightarrow\}$ then $val(v)=2$
\item if $lbl(v)=\urcorner$ then $val(v)=1$.
\end{enumerate}
%
\end{example}
%%
\begin{example}\rm
\llabel{multisorted}
Consider first order logic with several sorts $GS=\{S_1,\dots,S_n\}$. Let $GP$ be the set of generating predicates and $GF$ the set of generating functions. Let $C_1=C_0\amalg \{\forall,\exists\}$ and $C_2=C_1\amalg GP\amalg GF\amalg GS$. We can identify the $\alpha$-equivalence classes of formulas of the first order language defined by $GS$ and $GF$ with free variables from a set $X$  with a subset in $Exp_{\alpha}(X,\nn;C_2)$. Vertices which are labeled by $(\forall;x)$ and $(\exists;x)$ have valency two. For such a vertex $v$, the first branch of $[v]$ is one vertex labeled by an element of $GS$ giving the sort over which the quantification occurs and the second branch is the expression which is quantified.  Now however, these subsets do not form a sub-triple of $Exp_{\alpha}$ since not all substitutions are allowed. By allowing all substitutions irrespectively of the sort we get (for each $X$) a subset in $Exp_{\alpha}(X;C_2)$ whose elements will be called pseudo-formulas. 
\end{example}
%

The following operations on expressions are well defined up to the $\alpha$-equivalence:
%
\begin{enumerate}
\item If  ${T}_1,\dots,{T}_m\in Exp_{\alpha}(A;Con)$, $a_1,\dots,a_n$ are pair-wise different elements of $A$ and $M\in Con$ we will write 
$(M,a_1,\dots,a_n)({T}_1,\dots,{T}_m)$ for the expression whose root $v$ is labeled by $(M,a_1,\dots,a_n)$, $val(v)=n$ and $br_i(v)={T}_i$.
%
\item For $T_1,T_2\in Exp_{\alpha}(A;Con)$ and $v\in T_1$ we let $T_1(T_2/[v])$ be the  expression obtained by replacing $[v]$ in $T_1$ with $T_2'$ where $T_2'$ is obtained from $T_2$ by the change of bound variables such that the bound variables of $T_2'$  do not conflict with the variables of $T_1$.
%  
\item For $T,R_1,\dots,R_n\in Exp_{\alpha}(A;Con)$ and $y_1,\dots,y_n\in A$ we let $T(R_1/y_1,\dots,R_n/y_n)$ denote the expression obtained by changing $R_i$'s by $\alpha$-equivalent $R_i'$ such that $bnd(R_i')\cap bnd(R_j)'=\emptyset$ for $i\ne j$, changing $T$ to an $\alpha$-equivalent $T'$ such that $bnd(T')\cap(var(R_1')\cup\dots\cup var(R_n'))=\emptyset$ and then replacing all the leaves of $T'$ marked by $y_i$ by  $R_i'$. 
\end{enumerate}
%
In all the examples considered above, these operations correspond to the usual operations on formulas. The first operation can be used to directly associate expressions in our sense with the formulas. For example, the expression associated with the formula $\forall x:S.P(x,y)$ in a multi-sorted predicate calculus is $(\forall,x)(S,P(x,y))$ where as was mentioned above we use the same notation for an element of $A\amalg B\amalg (Con\times (\amalg_{n\ge 0} B^n))$ and the one vertex tree with the corresponding label. 

Note: about representing elements of $AllExp(A,B;Con)$ by linear sequences of elements of $A\amalg B\amalg ??$. 


\paragraph{Reduction structures.} Another component of the structure present in systems of expressions used in formal systems is the reduction relation. It is very important for our approach to type systems that the reduction relation is defined on all pseudo-formulas and is compatible with the substitution structure even when not all psedu-formulas are well formed formulas. In what follows we will consider, instead of a particular syntactic system, a pair $(S,\rtr)$ where $S$ is a continuous triple on the category of sets and $\rtr$ is a reduction structure on $S$ i.e. a collection of relations $\rtr_X$ on $S(X)$ given for all finite sets $X$ satisfying the following two conditions:
%
\begin{enumerate}
\item if $E\in S(\{x_1,\dots,x_n\})$, $f_1,\dots, f_n, f_i'\in S(\{y_1,\dots, y_m\})$ and $f_i\rtr_{\{y_1,\dots,y_m\}} f_i'$ then 
%
$$E(f_1/x_1,\dots,f_i/x_i,\dots f_n/x_n)\rtr_{\{x_1,\dots,x_n\}}E(f_1/x_1,\dots,f'_i/x_i,\dots f_n/x_n),$$
%
\item if $E, E'\in S(\{x_1,\dots,x_n\})$, $f_1,\dots, f_n\in S(\{y_1,\dots, y_m\})$ and $E\rtr_{\{x_1,\dots,x_n\}} E'$ then 
%
$$E(f_1/x_1,\dots, f_n/x_n)\rtr_{\{x_1,\dots,x_n\}}E'(f_1/x_1,\dots, f_n/x_n).$$
%
\end{enumerate}
%
The following two results are obvious but important.
%
\begin{proposition}
\llabel{2009.10.17.prop1}
Let $S$ be a continuous triple on $Sets$ and $\rtr_{\alpha}$ be a family of reduction structures on $S$. Then the intersection $\cap_{\alpha}\rtr_{\alpha}:X\mapsto \cap_{\alpha}\rtr_{\alpha,X}$ is a reduction structure on $S$.
\end{proposition}
%
\begin{cor}
\llabel{2009.10.17.cor1}
For any family $(X_{\alpha},pre_{\alpha})$ of pairs of the form $(X,pre)$ where $X$ is a set and 
$pre$ is a relation on $S(X)$ (i.e. a subset of $S(X)\times S(X)$) there exists the smallest reduction structure $\rtr=\rtr(X_{\alpha},pre_{\alpha})$ on $S$ such that for each $\alpha$ and each $(f,g)\in pre_{\alpha}$ one has $f\rtr g$.
\end{cor}
%




\paragraph{Contextual categories.}
From this point on it will be important for us to distinguish two notions of a category. What is understood by a category by most practicing mathematicians i.e. a category up to an equivalence, will be called, when an explicit distinction is needed, a category of level 1. A category as a combinatorial object i.e. a category up to an isomorphism will be called a set-level category.  A set-level category $C$ is a pair of sets $Mor(C)$ and $Ob(C)$ with an additional structure. The structure is given by four maps
%
$$\partial_0,\partial_1:Mor(C)\sr ob(C)$$
$$Id:ob(C)\sr Mor(CC)$$
%
and the composition map
%
$$\circ:Mor(CC)_{\partial_1}\times_{\partial_0} Mor(CC)\sr Mor(CC)$$
%
which satisfy the well known conditions.  

A contextual category is a set-level category with the following additional structure (\cite[Def. 1.2, p.47]{Streicher}):
%
\begin{enumerate}
\item a function $lngth:ob(CC)\sr \nn$ such that there is a unique object $pt$ with $lngth(pt)=0$ and this object is a final object,
\item a map $fthr: Ob(C)\sr Ob(C)$ such that $lngth(fthr(X))=max(lngth(X)-1,0)$, 
\item for each $X\in Ob(C)$ a morphism $p_X:X\sr fthr(X)$,
\item for each $X\in Ob(C)\backslash \{pt\}$ and each morphism $f:Y\sr fthr(X)$ a pull-back square of the form
%
\begin{eq}
\llabel{2009.10.14.eq1}
\begin{CD}
f^*X @>q(f,X)>> X\\
@Vp_{f^*X}VV @VVp_XV\\
Y @>f>> fthr(X)
\end{CD}
\end{eq}
\end{enumerate}
%
such that the squares (\ref{2009.10.14.eq1}) satisfy the obvious conditions for $f=Id_{fthr(X)}$ and $f= f_1\circ f_2$. (Note that in the squares (\ref{2009.10.14.eq1}) one has $fthr(f^*X)=Y$ since the codomain of the morphism $p_{f^*X}$ is necessarily $fthr(f^*X)$). 

Note that this structure is given by maps of the form
%
$$lngth(ob(C))\sr\nn$$
$$fthr:ob(C)\sr ob(C)$$
$$p_{\_}:ob(C)\sr Mor(C)$$
%
and
%
$$(^*,q):Mor(C)_{\partial_1}\times_{fthr} Ob(C)\sr Ob(C)\times Mor(C)$$
%
This view of the contextual structure will be important below when we consider quotients of contextual categories by equivalence relations.











\paragraph{Contextual subcategories.} A subcategory $CC'$ of a contextual category $CC$ is called contextual subcategory if it is closed, in the obvious sense under the operations which define the contextual structure on $CC$ and such that the canonical squares which belong to $CC'$ are pull-back squares in $CC'$. A contextual subcategory is called non-triviial if it contains at least one other element than $pt$. A contextual subcategory of a contextual category is itself a contextual category with respect to the induced structure. The following elementary result plays a key role in many constructions of type theory:
%
\begin{proposition}
\llabel{2009.10.15.prop1}
Let $CC$ be a contextual category. Then for any family $CC_{\alpha}$ of contextual subcategories of $CC$, the intersection $CC'=\cap_{\alpha} CC_{\alpha}$ is a contextual sub-category.
\end{proposition}
%
\begin{proof}
The only condition to check is that a canonical square which belongs to $CC'$ is a pull-back square in $CC'$. This follows from the definition of pull-back squares and the fact that fiber products of sets commute with intersections of sets.
\end{proof}
%
\begin{cor}
\llabel{2009.10.15.cor1}
Let $CC$ be a contextual category, $C_0$ a set of objects of $CC$ and $C_1$ a set of morphisms of $CC$. Then there exists the smallest contextual subcategory $[C_1,C_0]$ which contains $C_0$ and $C_1$. It is called the contextual subcategory generated by $C_0$ and $C_1$. 
\end{cor}
%

Let $CC$ be a contextual category. Let $ob(CC)$ be as usually the set of objects of $CC$ and let $\wt{ob}(CC)$ be the set of pairs of the form $(X,s)$ where $X\in ob(CC)$ and $s:fthr(X)\sr X$ is a section of the canonical morphism $p_X:X\sr fthr(X)$. 
%
\begin{lemma}
\llabel{2009.10.15.l1}
Let $CC$ be a contextual category and $CC'$, $CC''$ be two contextual subcategories such that $ob(CC')=ob(CC'')$ (as subsets of $ob(CC)$) and $\wt{ob}(CC')=\wt{ob}(CC'')$ (as subsets of $\wt{ob}(CC)$). Then $CC'=CC''$.
\end{lemma}
%
\begin{proof}
For any contextual category we have a canonical decomposition $ob(CC)=\amalg_n ob_n(CC)$ such that $ob_0(CC)=\{pt\}$ is the distinguished final object and for $\Gamma\in ob_n$ and $n>0$, $fthr(\Gamma)\in ob_{n-1}$. 

Let $f:Y\sr X$ be a morphism in $CC'$. We want to show that it belongs to $CC''$. Proceed by induction on $m$ where $X\in ob_m$. For $m=0$ the assertion is obvious. Suppose that $m>0$. Since $CC$ is a contextual category we have a commutative diagram
%
\begin{eq}
\llabel{2009.11.07.oldeq1}
\begin{CD}
Y @>s_f>> (p_{X}f)^*X @>q(p_{X}f,X)>> X\\
@V=VV @VVp'V @VVpV\\
Y @>=>> Y @>p_{X}f>> fthr(X)
\end{CD}
\end{eq}
%
such that $f= q(p_{X}f,X)\,s_f$. Since the right hand side square is a canonical one, $((p_{X}f)^*\Gamma',s_f)\in \wt{ob}(CC)$ and $fthr(X)\in ob_{m-1}(CC)$, the inductive assumption implies that $f\in CC''$. 
\end{proof}
%
\begin{remark}\rm
In Lemma \ref{2009.10.15.l1}, it is sufficient to assume that $\wt{ob}(CC')=\wt{ob}(CC'')$. The condition $ob(CC')=ob(CC'')$ is then also satisfied. Indeed, let $X\in ob(CC')$. Then $p_X^*X$ is the product $X\times X$ in $CC$. Consider the diagonal section $\Delta_X:X\sr p_X^*X$ of $p_{p_X^*(X)}$. Since $CC'$ is assumed to be a contextual subcategory we conclude that $\Delta_X\in \wt{ob}(CC')=\wt{ob}(CC'')$ and therefore $X\in ob(CC'')$. It is however more convenient to think of contextual subcategories in terms of both subsets $ob$ and $\wt{ob}$.
\end{remark}
%




Let $CC$ be a contextual category. Let us say that a pair of subsets $C\subset ob(CC)$, $\wt{C}\subset \wt{ob}(CC)$ is saturated if there exists a contextual subcategory $CC'$ such that $C=ob(CC')$ and $\wt{C}=\wt{ob}(CC')$. By Lemma \ref{2009.10.15.l1} we have a bijection between contextual subcategories of $CC$ and saturated pairs $(C,\wt{C})$. 

Let us introduce the following notations. Let $X\in ob(CC)$ and $i\ge 0$. Denote by $p_{X,i}$ the composition of the canonical projections $X\sr fthr(X)\sr\dots\sr fthr^i(X)$ such that $p_{X,0}=Id_X$ and $p_{X,1}=p_X$. For $f:Y\sr fthr^i(X)$ denote by $q(f,X,i):f^*(X,i)\sr X$ the morphism defined inductively by the rule 
%
$$f^*(X,0)=Y\,\,\,\,\,\,\,\,\,q(f,X,0)=f,$$
$$f^*(X,i+1)=q(f,fthr(X),i)^*(X)\,\,\,\,\,\,\,\,\,q(q(f,fthr(X),i), X).$$
%
In other words, $q(f,X,i)$ is the canonical pull-back of the morphism $f:Y\sr fthr^i(X)$ with respect to  the sequence of canonical projections $X\sr fthr(X)\sr\dots\sr fthr^i(X)$. 

Let $s:fthr(X)\sr X$ be an element of $\wt{ob}(CC)$ and let $f:Y\sr X$ be a morphism. Denote by $f^*(s)$ the element of $\wt{ob}(CC)$ of the form $f^*(s):Y\sr f^*(X)$ which is the pull-back of $s$ with respect $f$. 




%
\begin{proposition}
\llabel{2009.10.15.prop2}
A pair $(C,\wt{C})$ is saturated if and only if it satisfies the following conditions:
%
\begin{enumerate}
\item $pt\in C$,
\item if $X\in C$ then $fthr(X)\in C$,
\item if $(s:fthr(X)\sr X)\in \wt{C}$ then $X\in C$,
%\item if $X,X'\in C$, $i\ge 1$ and $fthr^i(X)=fthr(X')$ then $p_{X'}^*(X,i)\in C$,
\item if $(s:fthr(X)\sr X)\in \wt{C}$, $X'\in C$, $i\ge 1$ and $fthr^i(X)=fthr(X')$ then $q(p_{X'},fthr(X),i-1)^*(s)\in \wt{C}$,
%\item if $X\in C$, $i\ge 1$ and $(s:Y\sr fthr^i(X))\in\tilde{C}$ then $s^*(X,i)\in C$,
\item if $(s_1:fthr(X)\sr X)\in \wt{C}$, $i\ge 1$ and $(s_2:fthr^{i+1}(X)\sr fthr^i(X))\in\tilde{C}$ then $q(s_2,fthr(X),i-1)^*(s_1)\in \wt{C}$,
\item if $X\in C$ then the diagonal $s_{id_X}:X\sr (p_X)^*(X)$ is in $\wt{C}$. 
\end{enumerate}
%
\end{proposition}
%
Conditions (4) and (5) are illustrated by the following diagrams:
%
$$
\begin{CD}
p_{X'}^*(fthr(X),i-1) @>q(p_{X'},fthr(X),i-1)>> fthr(X)\\
@VVq(p_{X'},fthr(X),i-1)^*(s)V @VVsV\\
p_{X'}^*(X,i) @>q(p_{X'},X,i)>> X\\
@VVV @VVp_XV\\
p_{X'}^*(fthr(X),i-1) @>q(p_{X'},fthr(X),i-1)>> fthr(X)\\
@VVV @VVV\\
\dots @. \dots\\
@VVV @VVV\\
X' @>p_{X'}>> fthr^i(X)
\end{CD}
\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,
\begin{CD}
s_2^*(fthr(X),i-1) @>q(s_2,fthr(X),i-1)>> fthr(X)\\
@VVq(s_2,fthr(X),i-1)^*(s_1)V @VVs_1V\\
s_2^*(X,i) @>q(s_2,X,i)>> X\\
@VVV @VVp_XV\\
s_2^*(fthr(X),i-1) @>q(s_2,fthr(X),i-1)>> fthr(X)\\
@VVV @VVV\\
\dots @. \dots\\
@VVV @VVV\\
fthr^{i+1}(X) @>s_2>> fthr^i(X)
\end{CD}$$
%
\begin{proof}
The "only if" part of the proposition is straightforward. Let us prove that for any $(C,\wt{C})$ satisfying the conditions of the proposition there exists a contextual subcategory $CC'$ of $CC$ such that $C=ob(CC')$ and $\wt{C}=\wt{ob}(CC')$. 

For a morphism $f:Y\sr X$ let $fthr(f)=p_Xf:Y\sr fthr(X)$.  Any morphism $f:Y\sr X$ in $CC$ has a canonical representation of the form $Y\stackrel{s_f}{\sr} X_f \stackrel{q_f}{\sr} X$ where $X_f=fthr(f)^*(X)$, $q_f=q(fthr(f),X)$ and $s_f:Y\sr X_f$ is the section of the canonical projection $X_f\sr Y$ corresponding to $f$. 

Define a candidate subcategory $CC'$ setting $ob(CC')=C$ and defining the set $Mor(CC'
)$ of morphisms of $CC'$ inductively by the conditions:
%
\begin{enumerate}
\item $Y\sr pt$ is in $Mor(CC')$ if and only if $Y\in C$,
\item $f:Y\sr X$ is in $Mor(CC')$  if and only if $X\in ob(C)$, $fthr(f)\in Mor(CC')$ and $s_f\in \wt{C}$.
\end{enumerate}
%
(note that the for $(f:Y\sr X)\in Mor(CC')$ one has $Y\in C$ since $s_f:Y\sr X_f$).

Let us show that if the condition of the proposition are satisfied then $(ob(CC'), Mor(CC'))$ form a contextual subcategory of $CC$. 

The subset $ob(CC')$ contains $pt$ and is closed under $fthr$ map by the first two conditions. The following lemma shows that $Mor(CC')$ contains identities and the compositions of canonical projections.
%
\begin{lemma}
\llabel{2009.10.16.l1}
Under the assumptions of the proposition, if $X\in C$ and $i\ge 0$ then $p_{X,i}:X\sr fthr^i(X)$ is in $Mor(CC')$.
\end{lemma}
%
\begin{proof}
By definition of contextual categories there exists $n$ such that $fthr^n(X)=pt$. Then $p_{X,n}\in Mor(CC')$ by the first constructor of $Mor(CC')$. By induction it remains to show that if $X\in C$ and $p_{X,i}\in Mor(CC')$ then $p_{X,i-1}\in Mor(CC')$. We have $fthr(p_{X,i-1})=p_{X,i}$ and $s_{p_{X,i-1}}$ is the pull-back of the diagonal $fthr^{i-1}(X)\sr (p_{fthr^{i-1}(X)})^*(fthr^{i-1}(X))$ with respect to the canonical morphism $X\sr fthr^{i-1}(X)$. The diagonal is in $\wt{C}$ by condition (6) and therefore $s_{p_{X,i-1}}$ is in $\wt{C}$ by repeated application of condition (4). 
\end{proof}
%
\begin{lemma}
\llabel{2009.10.16.l3}
Under the assumptions of the proposition, let $X\in C$, $(s:fthr(X)\sr X)\in \wt{C}$, $i\ge 0$,  and $(f:Y\sr fthr^i(X))\in Mor(CC')$. Then $q(f,fthr(X),i-1)^*(s):fthr(f^*(X,i))\sr f^*(X,i)$ is in $Mor(CC')$. 
\end{lemma}
%
\begin{proof}
Suppose first that $fthr^i(X)=pt$. Then $f=p_{Y,n}$ for some $n$ and the statement of the lemma follows from repeated application of condition (4). Suppose that the lemma is proved for all morphisms to objects of length $j-1$ and let the length of $fthr^i(X)$ be $j$. Consider the canonical decomposition $f=q_fs_f$. The morphism $q_f$ is the canonical pull-back of $fthr(f)$ and therefore the pull-back of $s$ relative to $q_f$ coincides with its pull-back relative to $fthr(f)$ which is $\wt{C}$ by the inductive assumption. The pull-back of an element of $\wt{C}$ with respect to $s_f$ is in $\wt{C}$ by condition (5). 
\end{proof}
%
\begin{lemma}
\llabel{2009.10.16.l4}
Under the assumptions of the proposition, let $g:Z\sr Y$ and $f:Y\sr X$ be in $Mor(CC')$. then $fg\in Mor(CC')$. 
\end{lemma}
%
\begin{proof}
If $X=pt$ the the statement is obvious. Assume that it is proved for all $f$ whose codomain is of length $<j$ and let $X$ be of length $j$. We have $fthr(fg)=fthr(f)g$ and therefore $fthr(fg)\in Mor(CC')$ by the inductive assumption. It remains to show that  $s_{fg}\in \wt{C}$. We have the following diagram whose squares are canonical pull-back squares
%
$$
\begin{CD}
X_{fg} @>>> X_f @>>> X\\
@VVV @VVV @VVp_XV\\
Z @>g>> Y @>fthr(f)>> fthr(X)
\end{CD}
$$
%
which shows that $s_{fg}=g^*(s_f)$. Therefore, $s_{fg}\in Mor(CC')$ by Lemma \ref{2009.10.16.l3}.
\end{proof}
%
\begin{lemma}
\llabel{2009.10.16.l5}
Under the assumptions of the proposition, let $X\in C$ and let $f:Y\sr fthr(X)$ be in $Mor(CC')$, then $f^*(X)\in C$ and $q(f,X)\in Mor(CC')$.
\end{lemma}
%
\begin{proof}
Consider the diagram
%
$$
\begin{CD}
f^*(X) @>q(f,X)>> X \\
@Vs_{q(f,X)}VV @VVs_{Id_X}V\\
q(f,X)^*(X) @>>> p_X^*(X) @>>> X\\
@VVV @VVV @VVV\\
f^*(X) @>q(f,X)>> X @>>> fthr(X)\\
@Vp_{f^*(X)}VV  @VVp_XV @.\\
Y @>f>> fthr(X)
\end{CD}
$$ 
%
where the squares are canonical. By condition (6) we have $s_{Id}\in \wt{C}$. Therefore, by Lemma \ref{2009.10.16.l3}, we have $s_{q(f,X)}\in \wt{C}$. In particular, $q(f,X)^*(X)\in C$ and therefore $f^*(X)=fthr(q(f,X)^*(X))\in C$. The fact that $q(f,X)\in Mor(CC')$ follows from the fact that $s_{q(f,X)}\in \wt{C}$ and $fthr(q(f,X))=f\circ p_{f^*(X)}$ is in $Mor(CC')$ by previous lemmas.
\end{proof}
%
\begin{lemma}
\llabel{2009.10.16.l6}
Under the assumptions of Lemma \ref{2009.10.16.l5}, the square
%
$$
\begin{CD}
f^*(X) @>q(f,X)>> X\\
@Vp_{f^*(X)}VV @VVp_XV\\
Y @>f>> fthr(X)
\end{CD}
$$
is a pull-back square in $CC'$.
\end{lemma}
%
\begin{proof}
We need to show that for a morphism $g:Z\sr f^*(X)$ such that $p_{f^*(X)}g$ and $q(f,X)g$ are in $Mor(CC')$ one has $g\in Mor(CC')$. We have $fthr(g)=p_{f^*(X)}g$, therefore by definition of $Mor(CC')$ it remains to check that $s_g\in \wt{C}$. The diagram
%
$$
\begin{CD}
(f^*Y)_g @>>> f^*Y @>q(f,X)>> X\\
@VVV @VVV @VVV\\
Z @>fthr(g)>> Y @>f>> fthr(X)
\end{CD}
$$
%
shows that $s_g=s_{q(f,X)g}$ and therefore $s_g\in Mor(CC')$.
\end{proof}
%
To finish the proof of the proposition it remains to show that $ob(CC')=C$ and $\wt{ob}(CC')=\wt{C}$. The first assertion is tautological. The second one follows immediately from the fact that for $(s:fthr(X)\sr X)\in \wt{ob}(CC)$ one has $fthr(s)=Id_{fthr(X)}$ and $s_s=s$. 
\end{proof}


\paragraph{Subcategories generated by rules.}
%
Let $CC$ be a contextual category. We will write $Seq_0$ for its set of obejcts and $Seq_1$ for its set of standard sections. For a contextual subcategory $CC'$ we will write $Seq_0(CC')$ for the subset of objects which belong to $CC'$ and $Seq_1(CC')$ for the subset of standard sections which belong to $CC'$. We will further write $Seq$ for $Seq_0\amalg Seq_1$.
%
\begin{definition}
\llabel{2009.11.11.def1}
A rule of valency $n$ on $CC$ is a subset $R\subset Seq^n\times Seq$.
\end{definition}
%
\begin{definition}
\llabel{2009.11.11.def2}
A subset $Sq\subset Seq$ is said to satisfy a rule $R$ if for any $(S_1,\dots,S_n;S')\in R$ such that $S_1,\dots,S_n\in Sq$ one has $S'\in Sq$.
\end{definition}
%
Let ${\cal R}$ be a set of rules on $CC$. We say that $Sq\subset Seq(CC)$ satisfies $\cal R$ if it satisfies all the rules from $\cal R$.  The intersection of all the subsets in $Seq$ which satisfy $\cal R$ is the smallest subset which satisfies $\cal R$ and we denote it by $Seq({\cal R})$. We will also write $Seq_0({\cal R})$ and $Seq_1({\cal R})$ for the intersections of $Seq({\cal R})$ with $Seq_0$ and $Seq_1$ respectively. 

Let us consider the condition on $\cal R$ which are required for the pair of subsets $(Seq_0({\cal R}), Seq_1({\cal R}))$ to be saturated i.e. to correspond to a contextual subcategory. 






%
Let $CC'$ be a contextual subcategory of $CC$. We say that $CC'$ satisfies $\cal R$ if $Seq(CC')$ satisfies $\cal R$ as a subset of $Seq(CC)$.
%
\begin{lemma}
\llabel{2009.11.11.l1}
Let $CC$ be a contextual category and ${\cal R}$ be a set of rules on $CC$. Then there exists the smallest contextual subcategory $CC({\cal R})$ which satisfies ${\cal R}$.
\end{lemma}
%
\begin{proof}
The whole $CC$ clearly satisfy all possible rules. Consider the intersection of all contextual subcategories which satisfy $\cal R$. It is a contextual subcategory by Proposition \ref{2009.10.15.prop1}. Since  the intersection of any family of subcategories satisfying a rule  $R$ obviously satisfies this rule as well, we conclude that this subcategory satisfies ${\cal R}$. Since it is clearly the smallest possible subcategory satisfying ${\cal R}$ this proves the lemma. 
\end{proof}
%
The contextual subcategory $CC({\cal R})$ is called the subcategory generated by the set of rules ${\cal R}$.
%
\begin{definition}
\llabel{2009.11.11.def2}
Let ${\cal R}$ be a collection of rules on $CC$ and $Sq\subset Seq(CC)$.  Denote by ${\cal R}_n$ the subset of rules of valency $n$ in $\cal R$. A parsing scheme on $Sq$ relative to $\cal R$ is a map
%
$$Par:Sq\sr \amalg_{n\ge 0}Seq^n\times {\cal R}_n$$
%
which satisfies the following two conditions:
%
\begin{enumerate}
\item  if $Rar(S)=(S_1,\dots,S_n; R)$ then $(S_1,\dots,S_n;S)\in R$,
\item for each $S\in Sq$ the parsing tree defined by iterated application of $Par$ is finite.
\end{enumerate}
\end{definition}
%
\begin{lemma}
\llabel{2009.11.11.l3}
Let $CC$ and $\cal R$ be as above. Let $CC'$ be a subcategory satisfying $\cal R$. Suppose that there exists a parsing scheme on $Seq_0(CC')\amalg Seq_1(CC')$ relative to $\cal R$. Then $CC'$ is generated by $\cal R$.
\end{lemma}
%
\begin{proof}
Using induction on the length of the parsing tree from $S\in Seq_0(CC')\amalg Seq_1(CC')$ one can easily see that any such $S$ belongs to the subcategory generated by $\cal R$.
\end{proof}
%

Let $\cal R$ be a collection of rules and let $Seq({\cal R})$ be the smallest subset in $Seq$ which satisfies ${\cal R}$. 







\paragraph{The sequent axiomatics of contextual categories.} Proposition \ref{2009.10.15.prop2} suggests that a contextual category $CC$ can be reconstructed from the sets $ob(CC)$ and $\wt{ob}(CC)$ together with the structures on these sets which correspond to the conditions of the proposition. Let us show that it is indeed the case. Let $B=ob(CC)$ and $\wt{B}=\wt{ob}(CC)$. We will further write $B_n$ for $ob(CC)_n$ such that $B_0=\{pt\}$,  $ft:B_n\sr B_{n-1}$ for the $fthr$ map and $ft^i:B_n\sr B_{n-i}$ for the $i$-th iteration of $ft$.  Let $\partial:\wt{B}\sr B$ be the map which assigns to a pair $(X,s:fthr(X)\sr X)\in \wt{ob}(CC)$ the object $X$. It takes values in $B_{\ge 1}=\amalg_{n\ge 1}B_n$. Let $\delta:B_{\ge 1}\sr \wt{B}$ be the map which sends $X$ to the diagonal section of the projection $p_X^*X\sr X$. We will also write $\wt{B}_{i}$ for $(X,s)$ such that $X\in B_i$ with the obvious meaning assigned to $\wt{B}_{\ge i}$ etc. 

In addition let us consider the following maps:
%
\begin{enumerate}
\item $T_i: (B_{\ge 1})_{ft}\times_{ft^i} (B_{\ge i})\sr B_{\ge i+1}$, $i\ge 1$ which sends $(Y,X)$ such that $fthr(Y)=fthr^i(X)$ to  $p_Y^*(X,i)$,
\item $\wt{T}_i:(B_{\ge 1})_{ft}\times_{ft^i\partial} (\wt{B}_{\ge i})\sr \wt{B}_{\ge i+1}$, $i\ge 1$ which sends $(Y, (X,s))$ such that $fthr(Y)=fthr^i(X)$ to $(p_Y^*(X,i), q(p_Y,fthr(X),i-1)^*(s))$,
\item $S_i: (\wt{B})_{\partial}\times_{ft^i} (B_{\ge i})\sr B_{\ge i-1}$, $i\ge 1$ which sends $((Y,s),X)$ such that $Y=fthr^i(X)$ to $s^*(X,i)$,
\item $\wt{S}_i: (\wt{B})_{\partial}\times_{ft^i\partial} (\wt{B}_{\ge i})\sr \wt{B}_{\ge i-1}$, $i\ge 1$ which sends $((Y,s_2),(X,s_1))$ such that $Y=fthr^i(X)$ to $q(s_2,fthr(X),i-1)^*(s_1)$.
\end{enumerate}
%
We will also write $T_0$ for the map $(Y,X)\mapsto Y$ defined on pairs such that $X=ft(Y)$  and $S_0$ for the map $((Y,s),X)\mapsto Y)$ defined on pairs  such that $X=Y$. The maps $\wt{T}_0$ and $\wt{S}_0$ are not defined. 

Note that we have
%
\begin{eq}
\begin{array}{ll}
ft(T_i(Y,X))=T_{i-1}(Y,ft(X))&\partial(\wt{T}_i(Y,(X,s))=T_i(X,Y)\\\\
ft(S_i((Y,s),X))=S_{i-1}((Y,s),ft(X))& \partial(\wt{S}_i((Y,s),X))=S_i((Y,s),X)
\end{array}
\end{eq}
%
Let us denote by 
%
$$T_i^j:(B_{\ge j})_{ft^j}\times_{ft^i} (B_{\ge i})\sr B_{\ge i+j}$$
$$\wt{T}_i^j:(B_{\ge j})_{ft^j}\times_{ft^i\partial} (\wt{B}_{\ge i})\sr \wt{B}_{\ge i+j}$$
%
the maps which are defined inductively by 
%
\begin{eq}
T_i^j(Y,X)=\left\{
\begin{array}{ll}
X&\mbox{\rm if $j=0$}\\
T_i(Y,X)&\mbox{\rm if $j=1$}\\
T_i^{j-1}(ft(Y),X))&\mbox{\rm if $j>1$}
\end{array}
\right.
\,\,\,\,\,\,\,\,\,\,\,\,
\wt{T}_i^j(Y,(X,s))=\left\{
\begin{array}{ll}
(X,s)&\mbox{\rm if $j=0$}\\
\wt{T}_i(Y,(X,s))&\mbox{\rm if $j=1$}\\
\wt{T}_i^{j-1}(ft(Y),(X,s)))&\mbox{\rm if $j>1$}
\end{array}
\right.
\end{eq}
%

Let $f:Y\sr X$ be a morphism such that $Y\in B_n$ and $X\in B_m$. Define a sequence $(s_1(f),\dots,s_m(f))$ of elements of $\wt{B}_{n+1}$ inductively by the rule 
%
$$(s_1(f),\dots,s_m(f))=(s_1(ft(f)),\dots,s_{m-1}(ft(f)),s_f)=(s_{ft^{m-1}(f)},\dots,s_{ft(f)},s_f)$$
%
where $ft(f)=p_X f$, $s_f$ is defined by the diagram (\ref{2009.11.07.oldeq1}) and for $m=0$ we start with the empty sequence. This construction can be illustrated by the following diagram for $f:Y\sr X$ where $X\in B_4$:
%
\begin{eq}
\begin{CD}
Y @>s_4(f)>>   Z_{4,3} @>>> Z_{4,2} @>>> Z_{4,1} @>>> T_4^n(Y,X) @>>> X\\
@. @VVV @VVV  @VVV @VVV @VVV\\
{} @. Y @>s_{3}(f)>> Z_{3,2} @>>> Z_{3,1} @>>> T_{3}^n(Y,ft(X))@>>> ft(X)\\
@. @. @VVV @VVV @VVV @VVV\\
{} @. {} @.  Y @>s_{2}(f)>> Z_{2,1}@>>> T_2^n(Y,ft^2(X)) @>>>  ft^2(X)\\
@. @. @.  @VVV @VVV @VVV\\
{} @. {} @. {} @. Y @>s_1(f)>>  T_1^n(Y,ft^{3}(X)) @>>>  ft^{3}(X)\\
@. @. @.  @. @VVV @VVV\\
{} @. {} @. {} @.  @.  Y @>>>  pt\\
\end{CD}
\end{eq}
%
which is completely determined by the condition that the squares are the canonical ones and the composition of morphisms in the $i$-th arrow from the top is $ft^i(f)$. For the objects $Z_i^j$ we have:
%
\begin{eq}
\begin{array}{lll}
Z_{4,1}=S_3(s_1(f), T_4^n(Y,X))&Z_{4,2}=S_2(s_2(f),Z_{4,1})&Z_{4,3}=S_1(s_3(f),Z_{4,2})\\\\
Z_{3,1}=S_2(s_1(f),T_3^n(Y,ft(X)))&Z_{3,2}=S_1(s_2(f),Z_{3,1})&\\\\
Z_{2,1}=S_1(s_1(f),T_2^n(Y,ft^2(X)))&&\\
\end{array}
\end{eq}

A simple inductive argument similar to the one in the proof of Lemma \ref{2009.10.15.l1} show that if $f,f':Y\sr X$ are two morphisms such that $X\in B_m$ and $s_i(f)=s_i(f')$ for $i=1,\dots,m$ then $f=f'$.  Therefore, we may consider the set $Mor(CC)$ of morphisms of $CC$ as a subset in $\amalg_{n,m\ge 0} B_n\times B_m\times \wt{B}_{n+1}^m$. 


Let us show how to describe this subset in terms of the operations introduced above. 
%
\begin{lemma}
\llabel{2009.11.07.l1}
An element $(Y,X,s_1,\dots,s_m)$ of $B_n\times B_m\times \wt{B}_{n+1}^m$ corresponds to a morphism if and only if the element $(Y,ft(X),s_1,\dots,s_{m-1})$ corresponds to a morphism and $\partial(s_m)=Z_{m,m-1}$ where $Z_{m,i}$ is defined inductively by the rule:
%
$$Z_{m,0}=T_m^n(Y,X)\,\,\,\,\,\,\,\,\,\,Z_{m,i+1}=S_{m-i-1}(s_{i+1}(f),Z_{m,i})$$
%
\end{lemma}
%
\begin{proof}
Straightforward from the example considered above. 
\end{proof}
%
Let us show now how to identify the canonical morphisms $p_{X,i}:X\sr ft^i(X)$ and in particular the identity morphisms. 
%
\begin{lemma}
\llabel{2009.11.10.l1}
Let $X\in B_m$ and $0\le i\le m$. Let $p_{X,i}:X\sr ft^i(X)$ be the canonical morphism. Then one has:
%
$$s_j(p_{X,i})=\wt{T}_1^{m-j}(X,\delta_{ft^{m-j}(X)})\,\,\,\,\,\,\,\,\,\,    j=1,\dots, m-i $$
%
\end{lemma}
%
\begin{proof}
Let us proceed by induction on $m-i$. For $i=m$ the assertion is trivial. Assume the lemma proved for $i+1$.  Since $ft(p_{X,i})=p_{X,i+1}$ we have $s_j(p_{X,i})=s_j(p_{X,i+1})$ for $j=1,\dots, m-i-1$. It remains to show that
%
\begin{eq}
\llabel{2009.11.10.eq1}
s_{m-i}(p_{X,i})=\wt{T}_1^{i}(X,\delta_{ft^{i}(X)})
\end{eq}
%
By definition $s_{m-i}(p_{X,i})=s_{p_{X,i}}$ and (\ref{2009.11.10.eq1}) follows from the commutative diagram:
%
$$
\begin{CD}
X @>>> ft^i(X)\\
@Vs_pVV @VV\delta_{ft^i(X)}V\\
p_{X,i+1}^*(ft^i(X)) @>>> p_{ft^i(X)}^*(ft^i(X)) @>>> ft^i(X)\\
@VVV @VVV @VVp_{ft^i(X)}V\\
 X @>>> ft^i(X) @>>> ft^{i+1}(X)
\end{CD}
$$
%
where $p=p_{X,i}$.
\end{proof}
%
\begin{lemma}
\llabel{2009.11.10.l2}
Let $(X,s)\in \wt{B}_{m+1}$, $Y\in B_n$ and $f:Y\sr ft(X)$. Define inductively
$(f,i)^*(s)\in \wt{B}_{n+m+1-i}$ by the rule
%
$$(f,0)^*(s)=\wt{T}^n_{m+1}(Y,s)$$
$$(f,i+1)^*(s)=\wt{S}_{m-i}(s_{i+1}(f), (f,i)^*(s))$$
%
Then $f^*(s)=(f,m)^*(s)$.
\end{lemma}
%
\begin{proof}
It follows from the diagram:
%
$$
\begin{CD}
Y @>s_m(f)>> * @>>> \dots @>>>* @>>> * @>>> ft(X)\\
@Vf^*(s)VV @VV(f,m-1)^*(s)V @. @VV(f,1)^*(s)V @VV(f,0)^*(s)V @VVsV\\
* @>>> * @>>> \dots @>>>* @>>> * @>>> X\\
@VVV @VVV @. @VVV @VVV @VVV\\
Y @>s_m(f)>> * @>>> \dots @>>>* @>>> * @>>> ft(X)\\
@. @VVV @. @VVV @VVV @VVV\\
{} @. Y  @>s_{m-1}(f)>> \dots @>>> * @>>> * @>>> ft^2(X)\\
@. @. @. @VVV @VVV @VVV\\
{} @. {} @. {} @. \dots @. \dots @. \dots \\
@. @. @. @VVV @VVV @VVV\\
 {} @. {} @. {} @. Y @>s_1(f)>> * @>>> ft^{m-1}(X)\\
@. @. @. @. @VVV @VVV\\
 {} @. {} @. {} @. {} @. Y @>>> pt
\end{CD}
$$
%
\end{proof}
%
\begin{lemma}
\label{2009.11.10.l3}
Let $g:Z\sr Y$, $f:Y\sr X$ and $X\in B_m$. Then $s_i(fg)=g^*s_i(f)$.
\end{lemma}
%
\begin{proof}
It follows immediately from the equations $s_{fg}=g^*s_f$ and $ft(fg)=ft(f)g$.
\end{proof}
%
\begin{lemma}
\llabel{2009.11.10.l4}
Let $f:Y\sr ft(X)$ be a morphism, $Y\in B_n$ and $X\in B_{m+1}$. Define $(f,i)^*(X)$ inductively by the rule:
%
$$(f,0)^*(X)=T_{m+1}^n(Y,X)$$
$$(f,i+1)^*(X)=S_{m-i}(s_{i+1}(f),(f,i)^*(X))$$
%
Then $f^*(X)=(f,m)^*(X)$.
\end{lemma}
%
\begin{proof}
Similar to the proof of Lemma \ref{2009.11.10.l2}.
\end{proof}
%
\begin{lemma}
\llabel{2009.11.10.l4}
Let $f:Y\sr ft(X)$ be a morphism, $Y\in B_n$ and $X\in B_{m+1}$. 
Then 
%
$$s_i(q(f,X))=\left\{
\begin{array}{ll}
\wt{T}_1(f^*X,s_i(f))&\mbox{\rm if $i\le m$}\\\\
\wt{T}_1(f^*X,\delta_X)&\mbox{\rm if $i=m+1$}
\end{array}
\right.
$$
%
\end{lemma} 
%
\begin{proof}
We have $s_i(q(f,X))=s_{ft^{m+1-i}(q(f,X))}$. For $i\le m$ we have $ft^{m+1-i}(q(f,X))=ft^{m-i}(f)p_{f^*X}$. Therefore,
%
$$s_{ft^{m+1-i}(q(f,X))}=s_{ft^{m-i}(f)p_{f^*X}}=p_{f^*X}^*s_{ft^{m-i}(f)}=\wt{T}_1(f^*X,s_i(f))$$
%
and for $i=m+1$ we have 
%
$$s_i(q(f,X))=s_{q(f,X)}=p_{f^*X}^*(\delta_X)=\wt{T}_1(f^*X,\delta_X).$$
%
\end{proof}
%
The lemmas proved above show that a contextual category can be reconstructed from the pair of sets $B, \wt{B}$ connected by the maps $ft$, $\partial$, $\delta$, $T_i$, $\wt{T}_i$, $S_i$ and $\wt{S}_i$. While this way of encoding contextual categories may be less convenient than their encoding as a pair of sets $Ob$ and $Mor$ connected by the maps $\partial_0$, $\partial_1$, $c$ (composition), $id$, $ft$ and $qpb:(f,X)\mapsto q(f,X)$, this fact has the following  important corollary. 
%
\begin{proposition}
\llabel{2009.11.10.prop1}
Let $CC$, $CC'$ be two contextual categories. Then there is a natural bijection between contextual functors $F:CC\sr CC'$ and pairs of maps $F_0:ob(CC)\sr {ob}(CC')$, $F_1:\wt{ob}(CC)\sr \wt{ob}(CC')$ which commute in the obvious sense with $ft$, $\partial$, $\delta$, $T_i$, $\wt{T}_i$, $S_i$ and $\wt{S}_i$.
\end{proposition}
%









\paragraph{Contextual categories $CC({\cal C},p)$.}
%
Let $C$ be a set level category, $pt\in ob(C)$ a final object of $C$, $p:\wt{U}\sr U$ a morphism in $C$ and suppose that for any $f:X\sr U$ in $C$ we  are given a pull-back square
%
$$
\begin{CD}
(X,f) @>Q(f)>> \wt{U}\\
@Vp_{(X,f)}VV @VVpV\\
X @>f>> U
\end{CD}
$$
%
In what follows we will write $(X,f_1,\dots,f_n)$ for $(\dots((X,f_1),f_2)\dots,f_n)$. 
For such a quadruple define a contextual category $CC=CC(C,p)$ as follows. Objects of $CC$ are sequences of the form $(F_1,\dots,F_n)$ where $F_1\in Hom_{C}(pt, U)$ and $F_{i+1}\in Hom_C((pt,F_1,\dots,F_i),U)$.  Morphisms from $(G_1,\dots,G_n)$ to $(F_1,\dots,F_m)$ are given by
%
$$Hom_{CC}((G_1,\dots,G_n),(F_1,\dots,F_m))=Hom_C((pt,G_1,\dots,G_n),(pt,F_1,\dots,F_m))$$
%
such that the mapping $(F_1,\dots,F_n)\sr (pt,F_1,\dots,F_n)$ is a full embedding of the underlying category of $CC$ to $C$. The image of this embedding consists of objects $X$ for which the canonical morphism $X\sr pt$ is a composition of morphisms which are (canonical) pull-backs of $p$. We will denote this embedding by $int$.

The final object of $CC$ is the empty sequence $()$. The map $fthr$ sends $(F_1,\dots,F_n)$ to $(F_1,\dots,F_{n-1})$. The canonical morphism $p_{(F_1,\dots,F_n)}$ is the projection 
%
$$p_{((pt,F_1,\dots,F_{n-1}),F_n)}:((pt,F_1,\dots,F_{n-1}),F_n)\sr (pt,F_1,\dots,F_{n-1})$$
%
For an object $(F_1,\dots,F_{m+1})$ and a morphism $f:(G_1,\dots,G_n)\sr (F_1,\dots,F_m)$ the canonical pull-back square is of the form
%
\begin{eq}
\llabel{2009.10.26.eq3}
\begin{CD}
(G_1,\dots,G_n,F_{m+1}f) @>q(f)>> (F_1,\dots,F_{m+1})\\
@Vp_GVV @VVp_FV\\
(G_1,\dots,G_n) @>f>> (F_1,\dots,F_{m})
\end{CD}
\end{eq}
%
where $int(p_F)=p((pt,F_1,\dots,F_{n-1}),F_n)$, $int(p_G)=p((pt,G_1,\dots,G_{n-1}),F_{m+1}\circ f)$ and $q(f)$ is the morphism such that $p_Fq(f)=fp_G$ and $Q(F_{m+1})int(q(f))=Q(F_{m+1}f)$.
 The unity and composition axioms for the canonical squares follow immediately from the unit and associativity axioms for compositions of morphisms in $C$. 

Let $(C,p)$ and $(C',p')$ be two sets of data as above. Let $\Phi:C\sr C'$ be a functor which takes distinguished squares in $C$ to pull-back squares in $C'$, $\phi:\Phi(U)\sr U'$, $\wt{\phi}:\Phi(\wt{U})\sr \wt{U}'$ be two morphisms such that 
%
$$
\begin{CD}
\Phi(\wt{U}) @>\phi>> \wt{U}'\\
@V\Phi(p)VV @VVp'V\\
\Phi(U) @>\phi>> U'
\end{CD}
$$
%
is a pull-back square and $\psi$ an isomorphism $\psi:pt_{C'}\sr \Phi(pt_C)$. 

Define a functor $H=H(\Phi,\phi,\wt{\phi})$ from $CC(C,p)$ to $CC(C',p')$ as follows. We define by induction on $n$ objects  $H(F_1,\dots,F_n)\in CC(C',p')$ and isomorphisms 
%
$$\psi_{(F_1,\dots,F_n)}:int'(H(F_1,\dots,F_n))\sr \Phi(int(F_1,\dots F_n))$$
%
where $int$ and $int'$ are the canonical functors $CC(C,p)\sr C$ and $CC(C',p')\sr C'$ respectively. 

For $n=0$ we set $H(pt)=pt$ and $\psi_{()}=\psi$. For $n>0$ let
%
$$(F'_1,\dots,F'_{n-1})=H(F_1,\dots,F_{n-1})$$
%
and let $F_n:int(F_1,\dots,F_{n-1})\sr U$. Define $F_n'$ as the composition
%
\begin{eq}
\llabel{2009.10.26.eq5}
F_n':int'(F_1',\dots,F_{n-1}')\stackrel{\psi_{(F_1,\dots,F_{n-1})}}{\longrightarrow} \Phi(int(F_1,\dots,F_{n-1})) \stackrel{\Phi(F_n)}{\sr} \Phi(U)\stackrel{\phi}{\sr} U'
\end{eq}
%
and let $H(F_1,\dots,F_n)=(F_1',\dots,F_{n-1}',F_n')$. Then
%
$$int'(H(F_1,\dots,F_n))=(int'(H(F_1,\dots,F_n)), F_n')$$
%
To define 
%
$$\psi_{(F_1,\dots,F_n)}:int'(H(F_1,\dots,F_n))\sr \Phi(int(F_1,\dots,F_{n}))$$
%
observe that by our conditions on $\phi,\wt{\phi}$ and $\Phi$ the squares of the diagram 
%
$$
\begin{CD}
\Phi(int(F_1,\dots,F_{n})) @>\Phi(Q(F_n))>> \Phi(\wt{U}) @>>>  \wt{U}'\\
@VVV @VVV @VVV\\
\Phi(int(F_1,\dots,F_{n-1})) @>\Phi(F_n)>>  \Phi(U) @>\phi>> U'
\end{CD}
$$
%
are pull-back. Therefore there is a unique morphism $\psi_{(F_1,\dots,F_n)}$ such that the diagram 
%
\begin{eq}
\llabel{2009.10.26.eq2}
\begin{CD}
int'(H(F_1,\dots,F_n)) @>\psi_{(F_1,\dots,F_n)}>> \Phi(int(F_1,\dots,F_{n})) @>\wt{\phi}\Phi(Q(F_n))>>  \wt{U}'\\
@VVV @VVV @VVV\\
int'(H(F_1,\dots,F_{n-1})) @>\psi_{(F_1,\dots,F_{n-1})}>> \Phi(int(F_1,\dots,F_{n-1})) @>\phi\Phi(F_n)>>  U'
\end{CD}
\end{eq}
%
commutes and  
%
\begin{eq}
\llabel{2009.10.26.eq7}
\wt{\phi}\Phi(Q(F_n))\psi_{(F_1,\dots,F_n)}=Q(\phi\Phi(F_n)\psi_{(F_1,\dots,F_{n-1})})
\end{eq}
%
and this morphism is an isomorphism. 

To define $H$ on morphism we use the fact that morphisms $\psi_{(F_1,\dots,F_n)}$ are isomorphisms and for $f:(F_1,\dots,F_n)\sr (G_1,\dots,G_m)$ we set
%
\begin{eq}
\llabel{2009.10.26.eq6}
H(f)=\psi_{(G_1,\dots,G_m)}^{-1}\Phi(f)\psi_{(F_1,\dots,F_n)}
\end{eq}
%
The fact that this construction gives a functor i.e. satisfies the unity and composition axioms is straightforward. 

It remains to verify that this functor respects the contextual structure. 
It is clear that it respects the length function and the $fthr$ maps. The fact that it takes the canonical projections to canonical projections is equivalent to the commutativity of the left hand side square in (\ref{2009.10.26.eq2}). 

Consider a canonical square of the form (\ref{2009.10.26.eq3}). Its image is a square of the form
%
\begin{eq}
\llabel{2009.10.26.eq4}
\begin{CD}
(G_1',\dots,G'_n,G_{n+1}') @>H(q(f))>> (F_1',\dots,F_{m+1}')\\
@VH(p_G)VV @VVH(p_F)V\\
(G_1',\dots,G_n') @>H(f)>> (F_1',\dots,F_{m}')
\end{CD}
\end{eq}
%
We already know that the vertical arrows are canonical projections. Therefore, in order to prove that (\ref{2009.10.26.eq4})  is a canonical square in $CC(C',p')$ we have to show that $G_{n+1}'=F_{m+1}'int(H(f))$ and 
%
\begin{eq}
\llabel{2009.10.26.eq8}
Q(F_{m+1}')int(H(q(f)))=Q(F_{m+1}'int(H(f)))
\end{eq}
%
By (\ref{2009.10.26.eq5}) we have
%
$$G_{n+1}'=\phi\Phi(F_{m+1}f)\psi_{(G_1,\dots,G_n)}$$
$$F_{m+1}'=\phi\Phi(F_{m+1})\psi_{(F_1,\dots,F_{m})}$$
%
and by (\ref{2009.10.26.eq6})
%
$$int(H(f))=\psi^{-1}_{(F_1,\dots,F_m)}\Phi(f)\psi_{(G_1,\dots,G_n)}$$
$$int(H(q(f)))=\psi^{-1}_{(F_1,\dots,F_{m+1})}\Phi(q(f))\psi_{(G_1,\dots,G_n, F_{m+1}f)}$$
%
Therefore the relation $G_{n+1}'=F_{m+1}'int(H(f))$ follows immediately and the relation (\ref{2009.10.26.eq8}) follows by application of (\ref{2009.10.26.eq7}). 

Our construction of $H$ shows that if $\Phi$ is a full embedding and $\phi$ and $\wt{\phi}$ are isomorphisms then $H$ is an isomorphism of contextual categories. This implies in particular that considered up to a canonical isomorphism $CC(C,p)$ depends only on the equivalence class of the pair $(C,p)$ i.e. that our construction maps level 1 pairs $(C,p)$ to contextual categories which are set level.





Note: for $p:\wt{U}\sr U$ for which pull-backs exist the notion of a $p$-small object - an object $X$ such that $X\sr pt$ is a composition of morphisms which are pull-backs of $p$. 





\paragraph{$\Pi$ and $\Sigma$ universes in lcc categories.} 
%
\begin{definition}
\llabel{2009.11.1.def1}
Let $\cal C$ be a (level 1) category. A pre-universe in $\cal C$ is a morphism $p:\wt{U}\sr U$ together with for any $f:X\sr U$ a pull-back square 
%
$$
\begin{CD}
[f] @>Q(f)>>  \wt{U}\\
@Vp(f)VV  @VVpV\\
X @>f>> U
\end{CD}
$$
%

A morphism $q:Y\sr X$ in $\cal C$ is called a $p$-fibration if there a pull-back square of the form 
%
$$
\begin{CD}
Y @>>> \wt{U}\\
@VqVV @VVV\\
X @>>> U
\end{CD}
$$
%
A morphism $q$ is called $p$-small if it is a finite composition of $p$-fibrations.
\end{definition}
%
If $\cal C$ is a set-level category then we will say that a morphism $f:Y\sr X$ is a strict $p$-fibration if it is of the form $p(f)$. 



Recall that a (level 1) category $\cal C$ is called a lcc (locally Cartesian closed) category if it has fiber products and all the over-categories ${\cal C}/X$ have internal Hom-objects. 
%
\begin{definition}
\llabel{2009.10.27.def1}
Let $\cal C$ be an lcc category and let $p_i:\wt{U}_i\sr U_i$, $i=1,2,3$ be three morphisms in $\cal C$. A $\Pi$-structure on $(p_1,p_2,p_3)$ is a Cartesian square of the form
%
$$
\begin{CD}
\uu{Hom}_{U_1}(\wt{U}_1,U_1\times \wt{U_2}) @>>> \wt{U}_3\\
@Vp_2'VV @VVp_3V\\
\uu{Hom}_{U_1}(\wt{U}_1,U_1\times U_2) @>\Pi>> U_3
\end{CD}
$$
such that $p_2'$ is the natural morphism defined by $p_2$. A $\Pi$-structure on $p:\wt{U}\sr U$ is a $\Pi$-structure on $(p,p,p)$.
\end{definition}
%
A $\Pi$-structure on $(p_1,p_2,p_3)$ corresponds to the rule
%
$$\frac{\Gamma, X:U_1,f:X\sr U_2\vdash}{\Gamma, X:U_1,f:X\sr U_2\vdash \prod x:X. ev(f, x):U_3}$$
%



\begin{definition}
\llabel{2009.10.27.def2}
Let $\cal C$ be an lcc category and $p_i:\wt{U}_i\sr U_i$, $i=1,2,3$ be three morphisms in $\cal C$. A $\Sigma$-structure on $(p_1,p_2,p_3)$ is a diagram of the form
%
$$
\begin{CD}
\wt{U}_2 @<<< Fam_{\BB}(U_1,U_2) @>>> \wt{U}_3\\
@Vp_2VV @VVV\\
U_2 @<pr_{U_2}eval<< \wt{U_1}\times_{U_1}\uu{Hom}_{U_1}(\wt{U}_1,U_1\times U_2) @. @VVp_3V\\
@. @VVprV\\
{} @. \uu{Hom}_{U_1}(\wt{U}_1,U_1\times U_2) @>\Sigma>> U_3\\
\end{CD}
$$
%
such that $p_2'$ is the natural morphism defined by $p_2$, $eval$ is the canonical evaluation morphism and both the square and the vertical rectangle are Cartesian. A $\Sigma$-structure on $p:\wt{U}\sr U$ is a $\Sigma$-structure on $(p,p,p)$.
\end{definition}
%

A $\Sigma$-structure on $(p_1,p_2,p_3)$ corresponds to the rule
%
$$\frac{\Gamma, X:U_1,f:X\sr U_2\vdash}{\Gamma, X:U_1,f:X\sr U_2\vdash \sum x:X. ev(f, x):U_3}$$
%

\begin{definition}
\llabel{2009.11.2.def1}
Let $\cal C$ be an lcc category and $p:\wt{U}\sr U$ be a morphism. A $Prop$-structure on $p$ is a collection of data of the following form:
%
\begin{enumerate}
\item two pull-back squares 
%
$$
\begin{CD}
P @>>> \wt{U}\\
@VVV @VVpV\\
pt @>>> U
\end{CD}
\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,
\begin{CD}
\wt{P} @>>> \wt{U}\\
@Vp_0VV @VVpV\\
P @>>> U
\end{CD}
$$
%
\item a $\Pi$-structure on $(p,p_0,p_0)$.
\end{enumerate}
%
\end{definition}
%
A $Prop$-structure on $p$ corresponds to the rules:
%
$$\frac{}{x:P\vdash}\,\,\,\,\,\,\,\, \frac{}{x:P, y:x\vdash}\,\,\,\,\,\,\,\,\,\frac{\Gamma, f:X\sr P\vdash}{\Gamma, f:X\sr P\vdash \prod x:X. ev(f,x):P}$$





\paragraph{Contextual categories defined by a triple.}
Let $S$ be a continuous triple on $Sets$. Let $S-cor$ be the full subcategory of the Kleisli category of $S$ whose objects are finite sets. Recall, that the set of morphisms from $X$ to $Y$ in $S-cor$ is the set of maps from $X$ to $S(Y)$ i.e. $S(Y)^X$ (in other words, $S-cor$ is the 
category of free, finitely generated $S$-algebras).   We will construct two contextual categories $C(S)$ and $CC(S)$which are based on $(S-cor)^{op}$. 
%

\begin{examples}\rm
\item If $S=Id$ i.e. $S(X)=X$ the $S-cor=FSets$ is the category of finite sets. It is easy to see that the category of finite sets is the free category with finite coproducts generated by one object. Therefore, $(FSets)^{op}$ can be thought of the free category with finite products generated by one object.
\item Let $S$ be given by $S(X)=X\amalg A$ where $A$ is a set. This corresponds to the system of expressions where all expressions are either variables or constants and the set of constants is $A$. The category $(S-cor)^{op}$ can be though of as the free category with finite products generated by an object $U$ and the set $A$ of morphisms $pt\sr U$.
\end{examples}
%

The categories of sets, finite sets or even the category of finite linearly ordered sets and their isomorphisms are all level 1 categories and so is the category $S-cor$. We can get a set-level model $C(S)$ for $(S-cor)^{op}$ by setting  $ob(C(S))=\nn$ and $Hom_{C(S)}(n,m)=S(\{1,\dots,n\})^m$.  

The category $C(S)$ has a  contextual structure which is defined as follows. The final object is $0$. The map $fthr$ is given by 
%
$$fthr(n)=\left\{
\begin{array}{ll}
0&\mbox{\rm if $n=0$}\\
n-1&\mbox{\rm if $n>0$}
\end{array}
\right.
$$
%
The canonical projection $n\sr n-1$ is given by the sequence $(1,\dots,n-1)$. For $f=(f_1,\dots,f_{m}):n\sr m$ the canonical square build on $f$ and the canonical projection $m+1\sr m$ is of the form
%
$$
\begin{CD}
n+1 @>(f_1,\dots,f_m,n+1)>> m+1\\
@VVV @VVV\\
n @>(f_1,\dots,f_m)>> m
\end{CD}
$$
%
Any morphism of triples $S\sr S'$ defines a contextual functor $C(S)\sr C(S')$.
Non-trivial contextual subcategories of $C(S)$ are in one-to-one correspondence with continuous sub-triples of $S$. 

Note: add notes that a continuous sub-triple of $S$ is exactly the same as a subcategory in $S-cor$ which contains all (isomorphism classes of) objects. Intersection of two sub-triples is a sub-triple which allows us to speak of sub-triples (systems of expressions etc.) generated by a set of expressions. For the construction of type systems the category $S-cor$ is replaced by the contextual category $CC(S,X)$.

Note: that continuous triples on $Sets$ are the same as category structures on $\nn$ which extend the a category structure of finite sets and where the addition remains to be coproduct. 



Let now $CC(S)$ be the set-level category whose set of objects is $ob(CC(S))=\amalg_{n\ge 0} ob_n$ where 
%
$$ob_n=S(\emptyset)\times\dots\times S(\{1,\dots,n-1\})$$
%
and the set of morphisms is
%
$$mor(CC(S))=\coprod_{n,m\ge 0} ob_n\times ob_m\times S(\{1,\dots,n\})^m$$
%
with the obvious domain and codomain maps. The composition of morphisms is defined in the same way as in $C(S)$ such that the mapping $ob(CC(S))\sr \nn$ which sends all elements of $ob_n$ to $n$, is a functor. The associativity of compositions follows immediately from the associativity of compositions in $S-cor$. 

Note that if $S(\emptyset)=\emptyset$ then $CC(S)=\emptyset$ and otherwise the functor $CC(S)\sr (S-cor)^{op}$ is an equivalence, so that in the second case $C(S)$ and $CC(S)$ are indistinguishable as level 1 categories. However, as set level categories they are quite different. 

The category $CC(S)$ is given a contextual structure as follows. The final object is the only element of $ob_0$, the map $fthr$ is defined by the rule
%
$$fthr(T_1,\dots,T_n)=(T_1,\dots,T_{n-1}).$$
%
The canonical pull-back square defined by an object $(T_1,\dots,T_{m+1})$ and a morphism $(f_1,\dots,f_{m})\in S(\{1,\dots,n\})^{m}$ from $(R_1,\dots,R_n)$ to $(T_1,\dots,T_{m})$ is of the form
%
\begin{eq}
\llabel{2009.11.05.oldeq1}
\begin{CD}
(R_1,\dots,R_n,T_{m+1}(f_1/1,\dots, f_{m}/m)) @>(f_1,\dots,f_{m},n+1)>> (T_1,\dots,T_{m+1})\\
@VVV @VVV\\
(R_1,\dots,R_n) @>(f_1,\dots,f_{m})>> (T_1,\dots,T_{m})
\end{CD}
\end{eq}
%
%
\begin{proposition}
\llabel{2009.10.01.prop2}
With the structure defined above $CC(S)$ is a contextual category.
\end{proposition}
%
\begin{proof}
Straightforward.
\end{proof}
%

Note that the natural projection $CC(S)\sr C(S)$ is a contextual functor. It's contextual sections are in one-to-one correspondence with $S(\emptyset)$ such that $U\in S(\emptyset)$ corresponds to the section which takes the object $n$ of $C(S)$ to the object $(U,\dots,U)$ of $CC(S)$. 

Any morphism of triples $S\sr S'$ defines a contextual functor $CC(S)\sr CC(S')$. Contextual subcategories of $CC(S)$, which are discussed in more detail below, provide an important class of type systems over $S$. 


There is another construction of a category from a continuous triple $S$ which takes as an additional parameter a set $Var$ which is called the set of variables. Let $F_n(Var)$ be the set of sequences of length $n$ of pair-wise distinct elements of $Var$. Define the category $CC(S,Var)$ as follows. The set of objects of $CC(S,Var)$ is 
%
$$ob(CC(S,Var))= \amalg_{n\ge 0} \amalg_{(x_1,\dots,x_n)\in F_n(Var)} S(\emptyset)\times\dots\times S(\{x_1,\dots,x_{n-1}\})$$
%
For notational compatibility with the traditional type theory we will write the elements of $ob(CC(S,X))$ as sequences of the form $x_1:E_1,\dots,x_n:E_n$. The set of morphisms is given by
%
$$Hom_{CC(S,,Var)}((x_1:E_1,\dots,x_n:E_n),(y_1:T_1,\dots,y_m:T_m))=S(\{x_1,\dots,x_n\})^m$$
%
The composition is defined in such a way that the projection 
%
$$(x_1:E_1,\dots,x_n:E_n)\mapsto (E_1,E_2(1/x_1),\dots,E_n(1/x_1,\dots,n-1/x_{n-1}))$$
%
is a functor from $CC(S,X)$ to $CC(S)$. This functor is clearly an equivalence. There is an obvious final object and $frth$ map on $CC(S,X)$. There is however a real problem in making it into a contextual category which is due to the following. Consider an object $(y_1:T_1,\dots,y_{m+1}:T_{m+1})$ and a morphism $(f_1,\dots,f_m):(x_1:R_1,\dots,x_n:R_n)\sr (y_1:T_1,\dots,y_{m}:T_{m})$. In order for the functor to $CC(S)$ to be a contextual functor the canonical square build on this pair should have the form
%
$$
\begin{CD}
(x_1:R_1,\dots,x_n:R_n,x_{n+1}:T_{m+1}(f_1/1,\dots, f_{m}/m)) @>(f_1,\dots,f_{m},n+1)>> (y_1:T_1,\dots,y_{m+1}:T_{m+1})\\
@VVV @VVV\\
(x_1:R_1,\dots,x_n:R_n) @>(f_1,\dots,f_{m})>> (y_1:T_1,\dots,y_m:T_{m})
\end{CD}
$$
%
where $x_{n+1}$ is an element of $X$ which is distinct from each of the elements $x_1,\dots,x_n$. Moreover, we should choose  $x_{n+1}$ in such a way the the resulting construction satisfies the contextual category axioms for $(f_1,\dots,f_{m})=Id$ and for the compositions $(g_1,\dots,g_n)\circ (f_1,\dots,f_m)$. One can easily see that no such choice is possible for a finite set $X$. At the moment it is not clear to me whether or not such it is possible for an infinite $X$.

\paragraph{Contextual subcategories of $CC(S)$.}

Let $TS$ be a contextual subcategory of $CC(S)$.  By Lemma \ref{2009.10.15.l1}, $TS$ is determined by the subsets $ob(TS)$ and $\wt{ob}(TS)$ in $ob(CC(S))$ and $\wt{ob}(CC(S))$. By definition we have
%
$$ob(CC(S))=\coprod_{n\ge 0} S(\emptyset)\times S(\{1\})\times\dots\times S(\{1,\dots,n-1\})\times S(\{1,\dots,n\})$$
%
An element of $\wt{ob}(CC(S))$ is given by a pair $(\Gamma,s)$ where $\Gamma\in ob(CC(S))$ is an object and $s:fthr(\Gamma)\sr \Gamma$ is a section of the canonical morphism $p_{\Gamma}:\Gamma\sr fthr(\Gamma)$. It follows immediately from the definition of $CC(S)$ that for $\Gamma=(E_1,\dots,E_{n+1})$, a morphism $(f_1,\dots,f_{n+1})\in S(\{1,\dots,n\})^{n+1}$ from $fthr(\Gamma)$ to $\Gamma$ is a section of $p_{\Gamma}$ if an only if $f_i=i$ for $i=1,\dots,n$. Therefore, any such section is determined by its last component $f_{n+1}$ and mapping
$((E_1,\dots,E_{n+1}), (f_1,\dots,f_{n+1}))$ to $(E_1,\dots,E_n,E_{n+1},f_{n+1})$ we get a bijection
%
\begin{eq}
\llabel{2009.10.15.eq2}
\wt{ob}(CC(S))\cong \coprod_{n\ge 0} S(\emptyset)\times S(\{1\})\times\dots\times S(\{1,\dots,n-1\})\times S(\{1,\dots,n\})^2
\end{eq}
%
Let $Seq_0(TS)=ob(TS)$ and let $Seq_1(TS)$ be the image of $\wt{ob}(TS)$ under the bijection (\ref{2009.10.15.eq2}).  Traditionally, one writes $E_1,E_2,\dots,E_n\vdash_{TS} $ if $(E_1,\dots,E_n)$ is in $Seq_0(TS)$ and $E_1,E_2,\dots,E_n\vdash_{TS} t:T$  if  $(E_1,\dots,E_n,T,t)$ is in $Seq_1(TS)$. When no confusion is possible we will write $\vdash$ instead of $\vdash_{TS}$.

The following result is an immediate corollary of Proposition \ref{2009.10.15.prop2}.
%
\begin{proposition}
\llabel{2009.10.16.prop3}
Let $S$ be a continuous triple on $Sets$.  A pair of subsets $Seq_0$, $Seq_1$ of the form 
%
\begin{eq}
\llabel{2009.10.01.eq3}
\begin{array}{c}
Seq_0(TS)\subset \coprod_{n\ge 0}  S(\emptyset)\times S(\{1\})\times\dots\times S(\{1,\dots,n-1\})\times S(\{1,\dots,n\})\\\\
Seq_1(TS)\subset \coprod_{n\ge 0}  S(\emptyset)\times S(\{1\})\times\dots\times S(\{1,\dots,n-1\})\times S(\{1,\dots,n\})^2
\end{array}
\end{eq}
%
defines a contextual subcategory of $CC(S)$  if and only if the following conditions hold:
%
\begin{enumerate}
\item $\vdash$,
\item if $E_1,\dots, E_n\vdash$ then $E_1,\dots,E_{n-1}\vdash$,
\item if $E_1,\dots, E_n\vdash t:T$ then $E_1,\dots, E_{n},T\vdash$,
\item if $E_1,\dots, E_n\vdash t:T$, $i=1,\dots,n$ and $E_1,\dots, E_i, E_{i+1}'\vdash$ then $E_1,\dots, E_i, E_{i+1}', E_{i+1},\dots, E_n(i+2/i+1,\dots, n/n-1)\vdash t(i+2/i+1,\dots,n+1/n):T(i+2/i+1,\dots,n+1/n)$,
\item if $E_1,\dots, E_n\vdash t:T$, $i=1,\dots,n$ and $E_1,\dots, E_i\vdash  r:E_{i+1}$ then  $E_1,\dots, E_i, E_{i+2}(r/i+1),\dots,E_n(r/i+1,i+1/i+2,\dots,n-2/n-1)\vdash t(r/i+1,i+1/i+2,\dots,n-2/n-1):T(r/i+1,i+1/i+2,\dots,n-2/n-1)$,
\item $E_1,\dots, E_n\vdash$ then $E_1,\dots, E_n\vdash n:E_n$.
\end{enumerate}
\end{proposition}
%
Note that conditions (4) and (5) together with condition (6) and condition (3) imply the following 
%
\begin{description}
\item[{\em 4a}] if $E_1,\dots, E_n\vdash$, $i=1,\dots,n$ and $E_1,\dots, E_i, E_{i+1}'\vdash$ then $E_1,\dots, E_i, E_{i+1}', E_{i+1},\dots, E_n(i+2/i+1,\dots, n/n-1)\vdash$,
\item[{\em 5a}] if $E_1,\dots, E_n\vdash$, $i=1,\dots,n$ and $E_1,\dots, E_i\vdash  r:E_{i+1}$ then  $E_1,\dots, E_i, E_{i+2}(r/i+1),\dots,E_n(r/i+1,i+1/i+2,\dots,n-2/n-1)\vdash$.
\end{description}
%
\begin{lemma}
\llabel{2009.11.05.l1}
Let $S$ be as above and let $Seq_0=ob(TS)$, $Seq_1\cong \wt{ob}(TS)$ be subsets corresponding to a contextual subcategory $TS$. Let further $(E_1,\dots, E_n), (T_1,\dots,T_m)\in ob(TS)$ and $(f_1,\dots,f_m)\in S(\{1,\dots,n\})^m$. Then  
%
$$(f_1,\dots,f_m)\in Hom_{TS}((E_1,\dots, E_n), (T_1,\dots,T_m))$$
%
if and only if $(f_1,\dots,f_{m-1})\in Hom_{TS}((E_1,\dots, E_n), (T_1,\dots,T_{m-1}))$ and 
%
$$(E_1,\dots,E_n,T_{m}(f_1/1,\dots,f_{m-1}/m-1), f_m)\in Seq_1$$
%
\end{lemma}
%
\begin{proof}
Straightforward using the fact that the canonical pull-back squares in $CC(S)$ are given by (\ref{2009.11.05.oldeq1}).
\end{proof}
%







Note: describe all type systems over the triple $X\mapsto X_+$. (Note that there are no non-trivial type systems over the identity triple since $Id(\emptyset)=\emptyset$.



\begin{remark}
\rm One can also define type systems as sub-quotients rather than just subobjects of $C_1(S,X)$.  This requires one to consider "type equality sequents" and "term equality sequents" in addition to the type sequents and term sequents which we consider. Some sort of syntactic equality is necessary in order to define well behaved type systems. The question is whether or not one needs to consider context dependent syntactic equalities which make it necessary to pass to equivalence classes on the level of contextual categories. The example of most of the type systems which are practically used suggests that it is sufficient to consider context-independent syntactic equalities (i.e. equivalence classes of abstract expressions) and to use equality types for the context dependent equalities. For the approach with context dependent syntactic equalities  see \cite{Streicher}.
\end{remark}


\paragraph{Type systems over $(S,\rtr)$.} Let $S$ be a continuous triple on $Sets$ and $\rtr$ a relation on $S$ (see above). One defines type systems over $(S,\rtr)$ as follows.
%
\begin{definition}
\llabel{2009.10.01.def2} Let $S$ be a continuous triple on the category of sets. A type system over $(S,\rtr)$ is a contextual subcategory $TS$ of $CC(S)$ such that 
%
\begin{enumerate}
\item if $(E_1,\dots,E_n)\in ob_n(TS)$, $i=1,\dots, n$ and $E'_i\in S(\{1,\dots,i-1\})$ is such that $E_i\rtr E'_i$ then $(E_1,\dots,E_i',\dots,E_n)\in ob_n(TS)$,
\item if $(f_1,\dots,f_m)\in Hom_{TS}((E_1,\dots,E_n),(T_1,\dots,T_m))$, $i=1,\dots,m$ and $f_i'\in S(\{1,\dots,n\})$ is such that $f_i\rtr f_i'$ then $(f_1,\dots,f_i',\dots,f_m)\in Hom_{TS}((E_1,\dots,E_n),(T_1,\dots,T_m))$,
\item if $(E_1,\dots,E_n),(T_1,\dots,T_m)\in ob(TS)$, $(f_1,\dots,f_m)\in S(\{1,\dots,n\})^m$, $i=1,\dots,n$ and $E'_i\in S(\{1,\dots,i-1\})$ is such that $E_i\rtr E'_i$ then 
%
$$(f_1,\dots,f_m)\in Hom_{TS}((E_1,\dots,E_n),(T_1,\dots,T_m))$$
%
if and only if $(f_1,\dots,f_m)\in Hom_{TS}((E_1,\dots,E_i',\dots,E_n),(T_1,\dots,T_m))$,
\item if $(E_1,\dots,E_n),(T_1,\dots,T_m)\in ob(TS)$, $(f_1,\dots,f_m)\in S(\{1,\dots,n\})^m$, $i=1,\dots,m$ and $T'_i\in S(\{1,\dots,i-1\})$ is such that $T_i\rtr T'_i$ then 
%
$$(f_1,\dots,f_m)\in Hom_{TS}((E_1,\dots,E_n),(T_1,\dots,T_m))$$
%
if and only if $(f_1,\dots,f_m)\in Hom_{TS}((E_1,\dots,E_n),(T_1,\dots,T_i',\dots,T_m))$,
%
\end{enumerate}
\end{definition}
%
We will write $TS(S,\rtr)$ for the set of type systems over $(S,\rtr)$. Type systems over $(S,=)$ are just the contextual subcategories of $CC(S)$. 





Define relations $\rtr_{TS}$ on $ob(TS)$ and on the sets $Hom_{TS}(-,-)$ 




%
\begin{proposition}
\llabel{2009.10.18.prop1}
Let $S$ be a continuous triple on $Sets$ and $\rtr$ a reduction structure on $S$. A pair of subsets 
$Seq_0$, $Seq_1$ of the form (\ref{2009.10.01.eq3}) defines a type system over $(S,\rtr)$ if and only of it satisfies the conditions of Proposition \ref{2009.10.16.prop3} together with the following additional conditions:
%
\begin{enumerate}
\item if $(E_1,\dots,E_n)\in Seq_0$, $i=1,\dots,n$ and $E_i\rtr E_i'$ then $(E_1,\dots,E_i',\dots,E_n)\in Seq_0$,
\item if $(E_1,\dots,E_{n+1},t)\in Seq_1$ and $t\rtr t'$ then $(E_1,\dots,E_{n+1},t')\in Seq_1$,
\item if $(E_1,\dots,E_{n+1},t)\in Seq_1$, $i=1,\dots,n+1$ and $E_i\rtr E_i'$ then $(E_1,\dots,E_i',\dots,E_{n+1},t)\in Seq_1$, 
\item if $(E_1,\dots,E_{n+1})\in Seq_0$, $i=1,\dots,n+1$, $E_i\rtr E_i'$ and $(E_1,\dots,E_i',\dots,E_{n+1},t)\in Seq_1$ \\
then $(E_1,\dots,E_i,\dots,E_{n+1},t)\in Seq_1$.
\end{enumerate}
%
\end{proposition}
%
\begin{proof}
Since $Seq_0=ob(TS)$ the first condition of the proposition is equivalent to the first condition of Definition  \ref{2009.10.01.def2}.

Suppose that $Seq_0$ and $Seq_1$ correspond to a contextual subcategory $TS$ satisfying the conditions of Definition \ref{2009.10.01.def2}. A sequence $(E_1,\dots,E_{n+1},t)$ is in $Seq_1$ if and only if $(1,\dots,n,t)$ is a morphism from $(E_1,\dots,E_n)$ to $(E_1,\dots,E_{n+1})$ in $TS$.  
If $(E_1,\dots,E_{n+1},t)\in Seq_1$ and $t\rtr t'$ then $(E_1,\dots,E_{n+1},t')\in Seq_1$ by condition (2) of Definition \ref{2009.10.01.def2}.  If $(E_1,\dots,E_{n+1},t)\in Seq_1$, $i=1,\dots,n$ and $E_i\rtr E_i'$ then by $(E_1,\dots,E_i',\dots,E_{n+1},t)\in Seq_1$ conditions (3) and (4) of Definition \ref{2009.10.01.def2}. If $(E_1,\dots,E_{n+1})\in Seq_0$, $i=1,\dots,n+1$, $E_i\rtr E_i'$ and $(E_1,\dots,E_i',\dots,E_{n+1},t)\in Seq_1$ 
then $(E_1,\dots,E_i,\dots,E_{n+1},t)\in Seq_1$ again by conditions (3), (4) of Definition \ref{2009.10.01.def2}.

Suppose now that the conditions (1)-(4) of the proposition are satisfied and $Seq_0$, $Seq_1$ correspond to a contextual subcategory $TS$. Let us show that $TS$ satisfies conditions (2)-(4) of Definition \ref{2009.10.01.def2}. Let  $(f_1,\dots,f_m)\in Hom_{TS}((E_1,\dots,E_n),(T_1,\dots,T_m))$, $i=1,\dots,m$ and $f_i'\in S(\{1,\dots,n\})$ is such that $f_i\rtr f_i'$.
Then $(f_1,\dots,f_i',\dots,f_m)\in Hom_{TS}((E_1,\dots,E_n),(T_1,\dots,T_m))$ by Lemma \ref{2009.11.05.l1}, the definition of the reduction structure on $S$ and conditions (2), (3) of our proposition. 

Let $(E_1,\dots,E_n),(T_1,\dots,T_m)\in ob(TS)$, $(f_1,\dots,f_m)\in S(\{1,\dots,n\})^m$, $i=1,\dots,n$ and $E'_i\in S(\{1,\dots,i-1\})$ is such that $E_i\rtr E'_i$. Then
%
$$(f_1,\dots,f_m)\in Hom_{TS}((E_1,\dots,E_n),(T_1,\dots,T_m))$$
%
if and only if $(f_1,\dots,f_m)\in Hom_{TS}((E_1,\dots,E_i',\dots,E_n),(T_1,\dots,T_m))$ by obvious induction, Lemma \ref{2009.11.05.l1} and conditions (3), (4) of the proposition. 

Similarly, if $(E_1,\dots,E_n),(T_1,\dots,T_m)\in ob(TS)$, $(f_1,\dots,f_m)\in S(\{1,\dots,n\})^m$, $i=1,\dots,m$ and $T'_i\in S(\{1,\dots,i-1\})$ is such that $T_i\rtr T'_i$ then 
%
$$(f_1,\dots,f_m)\in Hom_{TS}((E_1,\dots,E_n),(T_1,\dots,T_m))$$
%
if and only if $(f_1,\dots,f_m)\in Hom_{TS}((E_1,\dots,E_n),(T_1,\dots,T_i',\dots,T_m))$, by obvious induction, Lemma \ref{2009.11.05.l1}, the definition of reduction structure and conditions (3), (4) of the proposition. 
\end{proof}



\begin{definition}
\llabel{2009.11.4.def1}
Let $S$, $\rtr$ and $TS$ be as above. Let further $({\cal C},p)$ be a category with a pre-universe structure. A closed model of $TS$ with values in $({\cal C},p)$ is a contextual functor 
%
$$M:TS \sr CC({\cal C},p)$$
%
which is compatible with $\rtr$ i.e. such that the following conditions hold:
%
\begin{enumerate}
\item  if $(E_1,\dots,E_n)\in ob(TS)$, $i=1,\dots, n$ and $E'_i\in S(\{x_1,\dots,x_{i-1}\})$ is such that $E_i\rtr E'_i$ then $M(E_1,\dots,E_n)=M(E_1,\dots,E_i',\dots,E_n)$,
\item if $(f_1,\dots,f_m)\in Hom_{TS}((E_1,\dots,E_n),(T_1,\dots,T_m))$, $i=1,\dots,m$ and $f_i'\in S(\{1,\dots,n\})$ is such that $f_i\rtr f_i'$ then 
%
$$M((f_1,\dots,f_m);(E_1,\dots,E_n);(T_1,\dots,T_m))=M((f_1,\dots,f_i',\dots,f_m);(E_1,\dots,E_n);(T_1,\dots,T_m)$$
%
\item if $(E_1,\dots,E_n),(T_1,\dots,T_m)\in ob(TS)$, $(f_1,\dots,f_m)\in S(\{1,\dots,n\})^m$, $i=1,\dots,n$ and $E'_i\in S(\{1,\dots,i-1\})$ is such that $E_i\rtr E'_i$ then 
%
$$M((f_1,\dots,f_m);(E_1,\dots,E_n);(T_1,\dots,T_m))=M((f_1,\dots,f_m);(E_1,\dots,E_i',\dots,E_n);(T_1,\dots,T_m))$$
%
\item if $(E_1,\dots,E_n),(T_1,\dots,T_m)\in ob(TS)$, $(f_1,\dots,f_m)\in S(\{1,\dots,n\})^m$, $i=1,\dots,m$ and $T'_i\in S(\{1,\dots,i-1\})$ is such that $T_i\rtr T'_i$ then 
%
$$M((f_1,\dots,f_m);(E_1,\dots,E_n);(T_1,\dots,T_m))=M((f_1,\dots,f_m);(E_1,\dots,E_n);(T_1,\dots,T'_i,\dots,T_m))$$
%
\end{enumerate}
\end{definition}


...
are called the subset of type sequents and the subset of term sequents of a type system. By Lemma \ref{2009.10.15.l1} they uniquely determine the type system. 

Elements of $Seq_0$ are called contexts and elements of $Seq_1$ are called judgements. Proposition \ref{2009.10.16.prop3}  shows that for any type system $TS$ and any $(E_1,\dots,E_n,t,T)$  in $Seq_1(TS)$ the sequence $(E_1,\dots,E_n)$ is in $Seq_0$ i.e. the first part of a judgement should be a valid context.  

One also often uses the notation $E_1,E_2,\dots,E_n\vdash T:Type$ which is equivalent to  $E_1,E_2,\dots,E_n, T\vdash $. The meaning assigned to these subsets is as follows:
%
\begin{enumerate}
\item $E_1,E_2,\dots,E_n\vdash$ means that $E_1$ is a well formed closed type expression and for $i>1$, $E_i(1,\dots,i-1)$ is a well formed type expression in the context where variables $1,\dots,i-1$ have types $E_1,\dots,E_{i-1}$ respectively,
\item $E_1,E_2,\dots,E_n\vdash t:T$ means that $E_1,E_2,\dots,E_n, T\vdash$ and in the context where variables $1,\dots,n$ are of the types $E_1,\dots E_n$ respectively, $t(1,\dots,n)$ is a well formed term expression of type $T(1,\dots,n)$.
\end{enumerate}
%




\comment{
Let $CC$ be a contextual category. For a pair of equivalence relations $\sim_{ob}$, $\sim_{Mor}$ on $ob(CC)$ and $Mor(CC)$ respectively such that the maps $\partial_0$, $\partial_1$, $Id$ and $fthr$ are compatible with these relations, denote by
%
$$\partial_0(\sim),\partial_1(\sim):(Mor(CC)/\sim_{Mor})\sr (ob(CC)/\sim_{ob})$$
$$Id(\sim):(ob(CC)/\sim_{ob})\sr (Mor(CC)/\sim_{Mor})$$
$$fthr(\sim):(ob(CC)/\sim_{ob})\sr (ob(CC)/\sim_{ob})$$
%
the corresponding maps on the equivalence classes. 
%
\begin{definition}
\llabel{2009.10.15.def1}
A pair $(\sim_{ob},\sim_{Mor})$ is called a  contextual equivalence on $CC$ if the following conditions hold:
%
\begin{enumerate}
\item if $X\sim_{ob} X'$ then $length(X)=length(X')$,
\item the maps $\partial_0$, $\partial_1$, $Id$ and $fthr$ are compatible with $(\sim_{ob},\sim_{Mor})$,
\item the maps 
%
\begin{eq}
\llabel{2009.10.16.map1}
Mor(CC)_{\partial_1}\times_{\partial_0} Mor(CC)\sr (Mor(CC)/\sim_{Mor})_{\partial_1(\sim)}\times_{\partial_0(\sim)} (Mor(CC)/\sim_{Mor})
\end{eq}
%
\begin{eq}
\llabel{2009.10.16.map2}
Mor(CC)_{\partial_1}\times_{fthr} ob(CC)\sr (Mor(CC)/\sim_{Mor})_{\partial_1(\sim)}\times_{fthr(\sim)} (ob(CC)/\sim_{ob})
\end{eq}
%
are surjective,
\item $((ob(CC)/\sim_{ob}),(Mor(CC)/\sim_{Mor}))$ has a contextual category structure such that the natural projection is a contextual functor.
\end{enumerate}
\end{definition}
%
Note that the surjectivity condition on the maps (\ref{2009.10.16.map1}), (\ref{2009.10.16.map2}) implies that if $(\sim_{ob},\sim_{Mor})$ is a  contextual equivalence then there exists exactly one contextual category structure on $((ob(CC)/\sim_{ob}),(Mor(CC)/\sim_{Mor}))$ which makes the projection into a contextual functor. 

Given a contextual equivalence $(\sim_{ob},\sim_{Mor})$ define an equivalence relation $\sim_{\wt{ob}}$ on $\wt{ob}(CC)$ setting $s\sim_{\wt{ob}} s'$ iff $s\sim_{Mor} s'$. 
%
\begin{lemma}
\llabel{2009.10.16.l1}
Let $(\sim_{ob},\sim_{Mor})$, $(\sim'_{ob},\sim'_{Mor})$ be two contextual relations on $CC$ such that $\sim_{ob}=\sim_{ob}'$ and $\sim_{\wt{ob}}=\sim_{\wt{ob}}'$. Then $\sim_{Mor}=\sim_{Mor}'$.
\end{lemma}
%
\begin{proof}
Let us write $\sim$ for all three relations $\sim_{ob}$, $\sim_{Mor}$ and $\sim_{\wt{ob}}$ and similarly for $\sim'$. Let $f:Y\sr X$, $f':Y'\sr X'$ be such that $f\sim f'$. We want to show that $f\sim' f'$. Since $X\sim X'$ we have $j=length(X)=length(X')$. Suppose first that $j=0$. Then $X=X'=pt$ and the condition that $pt$ is a final object in the quotient category implies that $Y\sr pt$ is equivalent to $Y'\sr pt$ iff $Y$ is equivalent to $Y'$. Since $\sim$ and $\sim'$ agree on objects we conclude that in this case $f\sim' f'$. Proceed by induction on $j$. By inductive assumption we may assume that $fthr(f)\sim' fthr(f')$. Then since $\sim'$ is compatible with pull-backs we conclude that $q(f,X)\sim' q(f',X')$. On the other hand by the assumption that $\sim$ is a contextual equivalence we conclude that for $f\sim f'$ we have $s_f\sim s_{f'}$ which is equivalent to $s_f\sim' s_{f'}$. Finally, since $f=s_fq(f,X)$ and $f'=s_{f'}q(f',X')$ we conclude that $f\sim' f'$. 
\end{proof}
%
\begin{proposition}
\llabel{2009.10.15.prop4}
Let $CC$ be a contextual category. A pair of equivalence relations $(\sim_{ob},\sim_{\wt{ob}})$ on $ob(CC)$ and $\wt{ob}(CC)$ respectively corresponds to a contextual equivalence on $CC$ if and only if the following conditions hold:
%
\begin{enumerate}
\item
\end{enumerate}
%
\end{proposition}
%
\begin{proof}


\end{proof}

}




\bibliography{alggeom}
\bibliographystyle{plain}



\end{document}





