leftovers.tex

% 1. Это более общее определение морфизмов алгебраических теорий.
% Оно мне пока не нужно, а определение более сложное, чем для теорий с фиксированными сортами.
% Поэтому я решил его пока не включать, но потом может пригодиться.

There are several equivalent ways of defining essentially algebraic theories (\cite{LPC}, \cite{GAT}, \cite{PHL}, \cite[D 1.3.4]{elephant}).
We use approach introduced in \cite{PHL} under the name of partial Horn theories since it is the most convenient one.
There is a structure of a category on partial Horn theories.
A \emph{generalized morphism} between theories $\mathbb{T}$ and $\mathbb{T}'$ is a model of $\mathbb{T}$ in $\mathcal{C}_{\mathbb{T}'}$,
where $\mathcal{C}_{\mathbb{T}'}$ is the classifying category for $\mathbb{T}'$.
We will define another notion of morphisms between theories, which is more explicit.

\subsection{Morphisms of partial Horn theories}

Let $\mathbb{T}$ be a partial Horn theory.
A \emph{restricted term} of $\mathbb{T}$ is a term $t$ together with a formula $\varphi$.
We denote such a restricted term by $t|_\varphi$.
A \emph{derived sort} of $\mathbb{T}$ is a sequence of sorts $s_1, \ldots s_k$ together with a formula $\varphi$ succh that $FV(\varphi) \subseteq \{ x_1 : s_1, \ldots x_k : s_k \}$.

We will use the following abbreviations:
\begin{align*}
R(t_1|_{\varphi_1}, \ldots t_k|_{\varphi_k}) & \Longleftrightarrow R(t_1, \ldots t_k) \land \varphi_1 \land \ldots \land \varphi_k \\
t|_\varphi = s|_\psi & \Longleftrightarrow t = s \land \varphi \land \psi \\
t|_\varphi\!\downarrow & \Longleftrightarrow t\!\downarrow\!\land \varphi \\
\chi \sststile{}{V} t|_\varphi \cong s|_\psi & \Longleftrightarrow \chi \land t|_\varphi\!\downarrow\,\sststile{}{V} t = s \land \psi \text{ and } \chi \land s|_\psi\!\downarrow\,\sststile{}{V} t = s \land \varphi
\end{align*}

We define morphisms of theories $\mathbb{T}$ and $\mathbb{T}'$ as equivalence classes of functions $h$ satisfying the following conditions:
\begin{enumerate}
\item For every sort $s$ of $\mathbb{T}$, it determines a derived sort $h(s)$ of $\mathbb{T}'$,
\item For every predicate symbol $P : s_1 \times \ldots \times s_k$ of $\mathbb{T}$, it determines a formula $h(P)$ of $\mathbb{T}'$
such that $FV(h(P)) = \{ x^1_1 : s^1_1, \ldots x^{n_1}_1 : s^{n_1}_1, \ldots x^1_k : s^1_k, \ldots x^{n_k}_k : s^{n_k}_k \}$
and the sequent $h(P) \sststile{}{FV(h(P))} \varphi_1 \land \ldots \land \varphi_k$ is derivable,
where $\varphi_i$ are the formulas that correspond to the derived sorts $h(s_i)$ and $FV(\varphi_i) = \{ x^{n_i}_i, \ldots x^{n_i}_i \}$.
\item For every function symbol $\sigma : s_1 \times \ldots \times s_k \to s$ of $\mathbb{T}$,
it determines a sequence of restricted terms $h(\sigma)_1$, \ldots $h(\sigma)_m$ of $\mathbb{T}'$
such that $FV(h(\sigma)_i) = \{ x^1_1 : s^1_1, \ldots x^{n_1}_1 : s^{n_1}_1, \ldots x^1_k : s^1_k, \ldots x^{n_k}_k : s^{n_k}_k \}$
and the sequents $h(\sigma)_i\!\downarrow\ \sststile{}{FV(h(\sigma)_i)} \varphi^i_1 \land \ldots \land \varphi^i_k$
and $\bigwedge_{1 \leq i \leq m} h(\sigma)_i\!\downarrow\ \sststile{}{FV(h(\sigma)_i)} \psi[h(\sigma)_1/y_1, \ldots h(\sigma)_m/y_m]$ are derivable,
where $\varphi_i$ are the formulas that correspond to the derived sorts $h(s_i)$ and $FV(\varphi_i) = \{ x^{n_i}_i, \ldots x^{n_i}_i \}$
and $\psi$ is the formula that correspond to the derived sort $h(s)$ and $FV(\psi) = \{ y_1, \ldots y_m \}$.
\item For every axiom $S$ of $\mathbb{T}$, the sequent $h(S)$ is derivable in $\mathbb{T}'$.
\end{enumerate}

We will say that functions $h$ and $h'$ as described above are equivalent if the following conditions hold:
\begin{enumerate}
\item For every sort $s$ of $\mathbb{T}$, the sequences of sorts that correspond to $h(s)$ and $h'(s)$ are equal
and the formulas $\varphi$ and $\psi$ that correspond to $h(s)$ and $h'(s)$ are equivalent;
that is, the sequents $\varphi \ssststile{}{FV(\varphi) \cup FV(\psi)} \psi$ are derivable.
\item For every predicate symbol $P : s_1 \times \ldots \times s_k$ of $\mathbb{T}$, the formulas $h(P)$ and $h'(P)$ are equivalent.
\item For every function symbol $\sigma : s_1 \times \ldots \times s_k \to s$ of $\mathbb{T}$, restricted terms $h(\sigma)_i$ and $h'(\sigma)_i$ are equivalent for every $i$;
that is, the sequents $\sststile{}{FV(h(\sigma)_i)} h(\sigma)_i \cong h'(\sigma)_i$ are derivable.
\end{enumerate}

The identity morphism is defined in the obvious way.
To define the composition of morphisms, we need to extend the definition of a function $h : \mathbb{T} \to \mathbb{T}'$ to terms and formulas.
Let $t$ be a term of $\mathbb{T}$ of sort $s$ with free variables $x_1 : s_1$, \ldots $x_k : s_k$.
Suppose that $h(s)$ is a sequence $s_1$, \ldots $s_m$ together with a formula $\psi$
and $h(s_i)$ is a sequence $s^1_i$, \ldots $s^{n_i}_i$ together with a formula $\varphi_i$.
Then, by induction on $t$, we define a sequence of restricted terms $h(t)_1$, \ldots $h(t)_m$ of $\mathbb{T}'$
with free variables $x^1_1 : s^1_1, \ldots x^{n_1}_1 : s^{n_1}_1, \ldots x^1_k : s^1_k, \ldots x^{n_k}_k : s^{n_k}_k$.
If $t = x$ is a variable, then let $h(x)_i = x^i$.
% Это я не закончил.

% 2. Это раздел про partial Horn theories из моей старой версии статьи про алгебраические теории типов.
% В основном это шлак, но там есть пара интересных лемм, например про мономорфизмы.

\section{Partial Horn theories}
\label{sec:PHT}

There are several equivalent ways of defining essentially algebraic theories (\cite{LPC}, \cite{GAT}, \cite{PHL}, \cite[D 1.3.4]{elephant}).
We use approach introduced in \cite{PHL} under the name of partial Horn theories since it is the most convenient one.
We define morphisms of partial Horn theories in terms of morphisms of monads and left modules over them.
In this section we review necessary for our development parts of the theory of monads, left modules over them and partial Horn theories.
We also define algebraic dependent type theories as certain partial Horn theories.

\subsection{Monads and left modules over them}

We recall definitions of monads and left modules over a monad.
For our purposes the following definitions (see \cite{manes-algebraic-theories}) will be more convenient than the ordinary ones.
\begin{defn}
A \emph{monad} $(T,\eta,(-)^*)$ on a category $\C$ consists of a function $T : Ob(\C) \to Ob(\C)$,
a function $\eta$ that to each $A \in Ob(\C)$ assign a morphism $\eta_A : A \to T(A)$,
and a function that to each $A,B \in Ob(\C)$ assigns a function $(-)^* : Hom_\C(A,T(B)) \to Hom_\C(T(A),T(B))$, satisfying the following conditions:
\begin{itemize}
\item $\eta_A^* = id_{T(A)}$.
\item For every $\rho : A \to T(B)$, $\rho^* \circ \eta_A = \rho$.
\item For every $\rho : A \to T(B)$, $\sigma : B \to T(C)$, $\sigma^* \circ \rho^* = (\sigma^* \circ \rho)^*$.
\end{itemize}

A \emph{left module} $(M,(-)^\circ)$ over a monad $(T,\eta,(-)^*)$ with values in a category $\D$ consists of a function $M : Ob(\C) \to Ob(\D)$
and a function that to each $A,B \in Ob(\C)$ assigns a function $(-)^\circ : Hom_\C(A,T(B)) \to Hom_\D(M(A),M(B))$, satisfying the following conditions:
\begin{itemize}
\item $\eta_A^\circ = id_{M(A)}$.
\item For every $\rho : A \to T(B)$, $\sigma : B \to T(C)$, $\sigma^\circ \circ \rho^\circ = (\sigma^* \circ \rho)^\circ$.
\end{itemize}
\end{defn}
These data and axioms imply that $T$ and $M$ are functorial: if $f : A \to B$, then we can define $T(f)$ as $(\eta_B \circ f)^*$ and $M(f)$ as $(\eta_B \circ f)^\circ$.
Moreover, $\eta$, $(-)^*$ and $(-)^\circ$ are natural.

\begin{defn}
A morphism of monads $(T,\eta,(-)^*)$ and $(T',\eta',(-)^{*'})$ on $\C$ is a function $\alpha$ that to each $A \in Ob(\C)$ assigns a morphism $\alpha_A : T(A) \to T'(A)$,
satisfying the following conditions:
\begin{itemize}
\item $\alpha_A \circ \eta_A = \eta'_A$.
\item For every $\rho : A \to T(B)$, $\alpha_B \circ \rho^* = (\alpha_B \circ \rho)^{*'} \circ \alpha_A$.
\end{itemize}

Let $(M,(-)^\circ)$ and $(M',(-)^{\circ'})$ be left modules with values in $\D$ over monads $(T,\eta,(-)^*)$ and $(T',\eta',(-)^{*'})$ respectively.
A morphism between them is a pair of functions $(\alpha,\beta)$, where $\alpha$ is a morphism of monads $T$ and $T'$,
and $\beta$ assigns to each $A \in Ob(\C)$ a morphism $\beta_A : M(A) \to M'(A)$,
such that, for every $\rho : A \to T(B)$, $\beta_B \circ \rho^\circ = (\alpha_B \circ \rho)^{\circ'} \circ \beta_A$.
\end{defn}
These data and axioms imply that $\alpha$ and $\beta$ are natural.

Let $\mathcal{S}$ be a set of sorts, and let $(T,\eta,(-)^*)$ be a monad on the category of $\mathcal{S}$-sets.
We think of elements of $T(V)_s$ as terms of sort $s$ with free variables in $V$.
Given $t \in T(V)_s$ and $\rho : V \to T(V')$, we will write $t[\rho] \in T(V')_s$ for $\rho^*(t)$.
Let $(F,(-)^\circ)$ be a left module over $T$ with values in $\Set$.
We think of elements of $F(V)$ as formulas with free variables in $V$.
Given $\varphi \in F(V)$ and $\rho : V \to T(V')$, we will write $\varphi[\rho] \in F(V')$ for $\rho^\circ(\varphi)$.

Let $T : \Set^\mathcal{S} \to \Set^\mathcal{S}$ be a monad.
Then \emph{a free variables structure} on $T$ is a function $FV$ that to each $t \in T(V)_s$ assigns a subset of $V$, that is $FV(t) \subseteq V$, called the set of free variables of $t$.
This function must satisfy the following conditions:
\begin{align*}
FV(\eta(x)) & = x \\
FV(t[\rho]) & = \bigcup_{x \in FV(t)} FV(\rho(x))
\end{align*}

Let $F : \Set^\mathcal{S} \to \Set$ be a left module over $T$.
Then \emph{a free variables structure} on $F$ is a function $FV$ that to each $\varphi \in F(V)$ assigns a subset of $V$, that is $FV(\varphi)$, called the set of free variables of $\varphi$.
This function must satisfy the following condition:
\[ FV(\varphi[\rho]) = \bigcup_{x \in FV(\varphi)} FV(\rho(x)) \]

\emph{A module of formulas} over $T$ is a left module $F$ over $T$ together with a function
    $\land : F(V) \times F(V) \to F(V)$ and a constant $\top \in F(V)$ for every $V \in \Set^\mathcal{S}$, satisfying the following conditions:
\begin{itemize}
\item For every $\rho : V \to T(V')$, $\top[\rho] = \top$.
\item For every $\rho : V \to T(V')$, $(\varphi \land \psi)[\rho] = \varphi[\rho] \land \psi[\rho]$.
\end{itemize}

For every monad $T$ on $\Set^\mathcal{S}$ we define a left module $E$ with values in $\Set$.
For every $V \in \Set^\mathcal{S}$, let $E(V)$ be the set of triples $(s,t,t')$, where $s \in \mathcal{S}$, and $t,t' \in T(V)_s$.
For every $\rho : V \to T(V')$ and $(s,t,t') \in E(V)$, we let $(s,t,t')[\rho] = (s,t[\rho],t'[\rho])$.
We think of $(s,t,t')$ as a formula asserting the equality of terms $t$ and $t'$.
We write $t =_s t'$ (or simply $t = t'$) for $(s,t,t')$.
\emph{A module of formulas with equality} over $T$ is a module $F$ of formulas over $T$ together with a morphism $e : E \to F$.

\begin{defn}[mon-pres]
A \emph{monadic presentation of a partial Horn theory} is a triple $(T,F,\mu)$, where
    $T : \Set^\mathcal{S} \to \Set^\mathcal{S}$ is a finitary monad with a free variables structure,
    $F : \Set^\mathcal{S} \to \Set$ is a finitary module of formulas with equality and a free variables structure, and
    $\mu_V : T(V) \times F(V) \to T(V)$ is a function such that the following conditions hold:
\begin{itemize}
\item For every $\rho : V \to T(V')$, $\mu_V(t,\varphi)[\rho] = \mu_{V'}(t[\rho],\varphi[\rho])$.
\item $\mu_V(t, \top) = t$.
\item $\mu_V(t, \varphi \land \psi) = \mu_V(\mu_V(t, \varphi), \psi)$.
\end{itemize}
A morphism of triples $(T,F,\mu)$ and $(T',F',\mu')$ is a morphism $f$ of left modules $(T,F)$ and $(T',F')$ such that $f$ preserves free variables, equality, $\top$, $\land$ and $\mu$.
The category of monadic presentations of partial Horn theories with $\mathcal{S}$ as the set of sorts is denoted by $\PMnd_\mathcal{S}$.
\end{defn}

\subsection{The category of partial Horn theories}
\label{sec:PHT-rules}

Let $\mathcal{S}$ be a set of sorts, $T : \Set^\mathcal{S} \to \Set^\mathcal{S}$ a monad with a free variables structure,
    and $\mathcal{P}$ a set of predicate symbols together with a function that to each $R \in \mathcal{P}$
    assigns its signature $R : s_1 \times \ldots \times s_n$, where $s_1, \ldots s_n \in \mathcal{S}$.

Let $\mathcal{F}$ be a set of function symbols together with a function that to each $\sigma \in \mathcal{F}$ assigns its signature $\sigma : s_1 \times \ldots \times s_n \to s$, where $s_1, \ldots s_n, s \in \mathcal{S}$.
Then we can define an example of a monad over $\Set^\mathcal{S}$.
For each $V \in \Set^\mathcal{S}$ we can define a set $Term_\mathcal{F}(V)_s$ of terms of sort $s$ inductively:
\begin{itemize}
\item If $x \in V_s$, then $x \in Term_\mathcal{F}(V)_s$.
\item If $\sigma : s_1 \times \ldots \times s_n \to s$ and $t_i \in Term_\mathcal{F}(V)_{s_i}$, then $\sigma(t_1, \ldots t_n) \in Term_\mathcal{F}(V)_s$.
\end{itemize}
If $\rho : V \to Term_\mathcal{F}(V')$, then substitution is defined as follows:
\begin{align*}
x[\rho] & = \rho(x) \\
\sigma(a_1, \ldots a_k)[\rho] & = \sigma(a_1[\rho], \ldots a_k[\rho])
\end{align*}
Thus $Term_\mathcal{F} : \Set^\mathcal{S} \to \Set^\mathcal{S}$ is a monad, which we call the standard monad (over $\mathcal{F}$).

An \emph{atomic formula} with free variables in $V$ is an expression either of the form $t_1 =_s t_2$ (we will usually omit $s$ in the notation),
    where $s \in \mathcal{S}$ and $t_1, t_2 \in T(V)_s$, or of the form $R(t_1, \ldots t_n)$, where $R \in \mathcal{P}$, $R : s_1 \times \ldots \times s_n$ and $t_i \in T(V)_{s_i}$.
A \emph{Horn formula} (over $\mathcal{P}$) with free variables in $V$ is an expression of the form $\varphi_1 \land \ldots \land \varphi_n$ where $\varphi_i$ are atomic formulas.
If $n = 0$, then we write such a formula as $\top$.
The set of Horn formulas with free variables in $V$ is denoted by $Form_\mathcal{P}(V)$.
If $\varphi \in Form_\mathcal{P}(V)$ and $\rho : V \to T(V')$, then we will write $\varphi[\rho]$ for a formula defined as follows:
\begin{align*}
(t = t')[\rho] & = (t[\rho] = t'[\rho]) \\
R(t_1, \ldots t_k)[\rho] & = R(t_1[\rho], \ldots t_k[\rho]) \\
(\varphi_1 \land \ldots \land \varphi_n)[\rho] & = \varphi_1[\rho] \land \ldots \land \varphi_n[\rho]
\end{align*}
Thus $Form_\mathcal{P}$ is a left module over $T$.
Moreover, a free variables structure on $Form_\mathcal{P}$ is defined as follows:
\begin{align*}
FV(t = t') & = FV(t) \cup FV(t') \\
FV(R(t_1, \ldots t_k)) & = FV(t_1) \cup \ldots \cup FV(t_k) \\
FV(\varphi_1 \land \ldots \land \varphi_n) & = FV(\varphi_1) \cup \ldots \cup FV(\varphi_n)
\end{align*}

A \emph{Horn sequent} is an expression of the form $\varphi \sststile{}{V} \psi$, where $\varphi$ and $\psi$ are Horn formulas with free variables in $V$.
We will often write $\varphi_1, \ldots \varphi_n \sststile{}{V} \psi_1, \ldots \psi_k$ instead of $\varphi_1 \land \ldots \land \varphi_n \sststile{}{V} \psi_1 \land \ldots \land \psi_k$.
A \emph{partial Horn theory} is a set of Horn sequents.
The rules of \emph{partial Horn logic} are listed below.
If $\mathcal{A}$ is a partial Horn theory, then a \emph{theorem} of $\mathcal{A}$ is a sequent derivable from $\mathcal{A}$ in this logic.
\begin{center}
$\varphi \sststile{}{V} \varphi$ \axlabel{b1}
\qquad
\AxiomC{$\varphi \sststile{}{V} \psi$}
\AxiomC{$\psi \sststile{}{V} \chi$}
\RightLabel{\axlabel{b2}}
\BinaryInfC{$\varphi \sststile{}{V} \chi$}
\DisplayProof
\qquad
$\varphi \sststile{}{V} \top$ \axlabel{b3}
\end{center}

\medskip
\begin{center}
$\varphi \land \psi \sststile{}{V} \varphi$ \axlabel{b4}
\qquad
$\varphi \land \psi \sststile{}{V} \psi$ \axlabel{b5}
\qquad
\AxiomC{$\varphi \sststile{}{V} \psi$}
\AxiomC{$\varphi \sststile{}{V} \chi$}
\RightLabel{\axlabel{b6}}
\BinaryInfC{$\varphi \sststile{}{V} \psi \land \chi$}
\DisplayProof
\end{center}

\medskip
\begin{center}
$\sststile{}{x} x\!\downarrow$ \axlabel{a1}
\qquad
$x = y \land \varphi \sststile{}{V,x,y} \varphi[y/x]$ \axlabel{a2}
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \psi$}
\RightLabel{, $x \in FV(\varphi)$, $t \in T(V')$ \axlabel{a3}}
\UnaryInfC{$\varphi[t/x] \sststile{}{V,V'} \psi[t/x]$}
\DisplayProof
\end{center}
\medskip
Here, $t/x$ denotes a function $\rho : V \to T(V \cup V')$ such that $\rho(x) = t$ and $\rho(y) = y$ if $y \neq x$.

Note that this set of rules is a generalization of the one described in \cite{PHL}.
If $T$ is the standard monad $Term_\mathcal{F}$, then these rules are equivalent to the rules from \cite{PHL}.
In particular, the following sequents are derivable if $x \in FV(t)$:
\begin{align*}
R(t_1, \ldots t_k) & \sststile{}{V} t_i = t_i \axtag{a4} \\
t_1 = t_2 & \sststile{}{V} t_i = t_i \axtag{a4'} \\
t[t'/x]\!\downarrow & \sststile{}{V} t' = t' \axtag{a5}
\end{align*}

We will need the following lemmas from \cite{PHL}:
\begin{lem}[cong-a]
For every $u_i,v_i \in T(V)_{s_i}$ and $t \in T(\{ x_1 : s_1, \ldots x_n : s_n\})_s$,
sequents $u_1 = v_1 \land \ldots \land u_n = v_n \sststile{}{V} t[x_i \mapsto u_i] \cong t[x_i \mapsto v_i]$ are theorems of any theory.
\end{lem}

\begin{lem}
Sequent $y = x \land \varphi[y/x] \sststile{}{V} \varphi$ is a theorem of any theory.
\end{lem}

Using the previous lemma we prove the following fact:

\begin{lem}[cong-b]
For every $u_i,v_i \in T(V)_{s_i}$ and $\varphi \in Form_\mathcal{P}(\{ x_1 : s_1, \ldots x_n : s_n\})$,
sequent $u_1 = v_1 \land \ldots \land u_n = v_n \land \varphi[x_i \mapsto u_i] \sststile{}{V} \varphi[x_i \mapsto v_i]$ is a theorem of any theory.
\end{lem}
\begin{proof}
By the previous lemma we have $y_n = x_n \land \varphi[y_n/x_n] \sststile{}{x_1 : s_1, \ldots x_n : s_n, y_n : s_n} \varphi$ is provable.
If we take $\varphi$ to be equal to $y_n = x_n \land \varphi[y_n/x_n]$, then we get sequent
$y_{n-1} = x_{n-1} \land y_n = x_n \land \varphi[y_n/x_n,y_{n-1}/x_{n-1}] \sststile{}{x_1 : s_1, \ldots x_n : s_n, y_{n-1} : s_{n-1}, y_n : s_n} y_n = x_n \land \varphi[y_n/x_n]$.
By \axref{b2} we get sequent
\[ y_{n-1} = x_{n-1} \land y_n = x_n \land \varphi[y_n/x_n,y_{n-1}/x_{n-1}] \sststile{}{x_1 : s_1, \ldots x_n : s_n, y_{n-1} : s_{n-1}, y_n : s_n} \varphi. \]
Repeating this argument we can conclude that
\[ y_1 = x_1 \land \ldots \land y_n = x_n \land \varphi[y_1/x_1, \ldots y_n/x_n] \sststile{}{x_1 : s_1, \ldots x_n : s_n, y_1 : s_1, y_n : s_n} \varphi. \]
By \axref{a3} we conclude that the required sequent is derivable.
\end{proof}

Now we define a functor $PT : \Set^\mathcal{S} \to \Set^\mathcal{S}$ of restricted terms.
We let $PT(V)_s$ to be the set of expressions $t|_\varphi$ where $t \in T(V)_s$ and $\varphi \in Form_\mathcal{P}(V)$.
If $\varphi = \top$, then we will write $t|_\varphi$ simply as $t$.
If $p \in PT(V)_s$, $p = t|_\varphi$ and $\psi \in Form_\mathcal{P}(V)$, then we will write $p|_\psi$ for $t|_{\varphi \land \psi}$.

We will use the following abbreviations:
\begin{align*}
t\!\downarrow & \Longleftrightarrow t = t \\
\varphi \sststile{}{V} t \leftrightharpoons s & \Longleftrightarrow \varphi \land t\!\downarrow \land s\!\downarrow\,\sststile{}{V} t = s \\
\varphi \sststile{}{V} t \cong s & \Longleftrightarrow \varphi \land t\!\downarrow\,\sststile{}{V} t = s \text{ and } \varphi \land s\!\downarrow\,\sststile{}{V} t = s \\
\varphi \ssststile{}{V} \psi & \Longleftrightarrow \varphi \sststile{}{V} \psi \text{ and } \psi \sststile{}{V} \varphi \\
R(t_1|_{\varphi_1}, \ldots t_k|_{\varphi_k}) & \Longleftrightarrow R(t_1, \ldots t_k) \land \varphi_1 \land \ldots \land \varphi_k \\
t|_\varphi = s|_\psi & \Longleftrightarrow t = s \land \varphi \land \psi \\
t|_\varphi\!\downarrow & \Longleftrightarrow t\!\downarrow\!\land \varphi \\
\chi \sststile{}{V} t|_\varphi \leftrightharpoons s|_\psi & \Longleftrightarrow \chi \land t|_\varphi\!\downarrow, s|_\psi\!\downarrow\,\sststile{}{V} t = s \\
\chi \sststile{}{V} t|_\varphi \cong s|_\psi & \Longleftrightarrow \chi \land t|_\varphi\!\downarrow\,\sststile{}{V} t = s \land \psi \text{ and } \chi \land s|_\psi\!\downarrow\,\sststile{}{V} t = s \land \varphi
\end{align*}

Now we define substitution functions for restricted terms.
For every $\rho : V \to PT(V')$, $t \in T(V)_s$ and $\varphi \in Form_\mathcal{P}(V)$,
we define $t[\rho] \in PT(V')_s$, $\varphi[\rho] \in Form_\mathcal{P}(V')$ and $t_\varphi[\rho] \in PT(V')_s$ as follows:
\begin{align*}
t[\rho] & = t[\rho_1]|_{\bigcup_{x \in FV(t)} \rho_2(x)} \\
R(t_1, \ldots t_k)[\rho] & = R(t_1[\rho], \ldots t_k[\rho]) \\
(\varphi_1 \land \ldots \land \varphi_n)[\rho] & = \varphi_1[\rho] \land \ldots \land \varphi_n[\rho] \\
t|_\varphi[\rho] & = t[\rho]|_{\varphi[\rho]}
\end{align*}
where if $\rho(x) = t|_\varphi$, then $\rho_1(x) = t$ and $\rho_2(x) = \varphi$.
Free variables of $t|_\varphi$ is defined as follows: $FV(t|_\varphi) = FV(t) \cup FV(\varphi)$.

Note that $PT$ is not a monad in general since this substitution does not satisfy axioms.
To fix this we introduce an equivalence relation on sets $PT(V)_s$ and $Form_\mathcal{P}(V)$.
Let $\mathbb{T}$ be a partial Horn theory.
For every $t, t' \in PT(V)_s$, $t \sim t'$ if and only if $FV(t) = FV(t')$ and $\sststile{}{V} t \cong t'$ is a theorem of $\mathbb{T}$.
For every $\varphi, \psi \in Form_\mathcal{P}(V)$, $\varphi \sim \psi$ if and only if $FV(\varphi) = FV(\psi)$ and $\varphi \ssststile{}{V} \psi$ is a theorem of $\mathbb{T}$.
Then let $P(V)_s = PT(V)_s/\!\!\sim$ and $F(V) = Form_\mathcal{P}(V)/\!\!\sim$.
For every $x \in V_s$, $\eta_V(x)$ is the equivalence class of $x|_\top$.
Substitution functions respect equivalence relations, and it is easy to see that they define a structure of a monad and of a left module over it on $T$ and $F$.
For every $t,t' \in T(V)_s$, $e(s,t,t')$ is the equivalence class of $t = t'$.
For every $t \in T(V)_s$ and $\varphi \in F(V)$, let $\mu_V(t,\varphi) = t|_\varphi$.
It is easy to see that $(P,F,\mu)$ satisfies axioms of monadic presentations.
We will call it the monadic presentation of partial Horn theory $\mathbb{T}$ and denote by $P(\mathbb{T})$.

The category of partial Horn theories over $\mathcal{S}$ has tuples $(T,\mathcal{P},\mathcal{A})$ as objects,
    where $T$ is a finitary monad with a free variables structure, $\mathcal{P}$ is a set of predicate symbols and $\mathcal{A}$ is a set of axioms.
Morphisms of partial Horn theories $\mathbb{T}$ and $\mathbb{T}'$ are morphisms of their monadic presentations.
The category of partial Horn theories over $\mathcal{S}$ is denoted by $\Th^T_\mathcal{S}$.

\begin{prop}[mor-def]
Let $\mathbb{T} = (T,\mathcal{P},\mathcal{A})$ and $\mathbb{T}' = (T',\mathcal{P}',\mathcal{A}')$ be partial Horn theories,
    and let $P(\mathbb{T}) = (P,F,\mu)$ and $P(\mathbb{T}') = (P',F',\mu')$ be their monadic presentations.
To construct a morphism of these theories, it is enough to specify the following data:
\begin{itemize}
\item A morphism of monads $\alpha : T \to P'$ that preserves free variables.
\item For every $R \in \mathcal{P}$, $R : s_1 \times \ldots \times s_k$,
    a formula $\beta(R) \in F'(\{ x_1 : s_1, \ldots x_k : s_k \})$ such that $FV(\beta(R)) = \{ x_1, \ldots x_k \}$.
\end{itemize}
Then there is a morphism of left modules $f : (T,Form_\mathcal{P}) \to (T',F')$
    such that $f(\sigma(x_1, \ldots x_k)) = \alpha(\sigma)$ and $f(R(x_1, \ldots x_k)) = \beta(R)$.
If $f$ preserves axioms of $\mathbb{T}$, then it extends to a morphism of theories.
Moreover, there is at most one morphism with these properties.
\end{prop}
\begin{proof}
Morphism $f$ is already defined on terms, and we can define it on formulas as follows:
\begin{align*}
f(a = b) & = f(a) = f(b) \\
f(R(a_1, \ldots a_k)) & = \beta(R)[x_i \mapsto f(a_i)] \\
f(\varphi_1 \land \ldots \land \varphi_n) & = f(\varphi_1) \land \ldots \land f(\varphi_n)
\end{align*}
We also can define $f$ on restricted terms:
\[ f(t|_\varphi) = f(t)|_{f(\varphi)} \]
It is easy to see that $f$ preserves substitution.
Thus to prove that $f$ extends to a morphism of theories, we only need to show that it preserves theorems of $\mathbb{T}$.
By assumption, it preserves axioms, thus we only need to check that application of $f$ preserves inference rules.
This is obvious for \axref{b1}-\axref{b6} and \axref{a1}.
For \axref{a2} and \axref{a3} it follows from the facts that $f(\varphi[t/x]) = f(\varphi)[f(t)/x]$ and $FV(f(\varphi)) = FV(\varphi)$.

Now, let us prove that $f$ is unique.
Let $f$ and $f'$ be morphisms of theories such that $f(t) = f'(t)$ for every $t \in T(V)_s$, and
    $f(R(x_1, \ldots x_k)) = f'(R(x_1, \ldots x_k))$ for every $R \in \mathcal{P}$.
Then we prove that $f = f'$.

Let us prove that $f(\varphi) = f'(\varphi)$ for every $\varphi \in Form_\mathcal{P}(V)$.
It is enough to prove this for atomic formulas $\varphi$.
If $\varphi$ equals to $t = t'$, then $f(\varphi)$ equals to $f(t) = f(t')$ and $f'(\varphi)$ equals to $f'(t) = f'(t')$.
We know that $\sststile{}{V} f(t) \cong f'(t)$ and $\sststile{}{V} f(t') \cong f'(t')$.
Thus by transitivity and symmetry we can conclude that $f(t) = f(t)' \sststile{}{V} f'(t) = f'(t')$.

If $\varphi = R(t_1, \ldots t_k)$, then $f(\varphi) = f(R(x_1, \ldots x_k))[x_i \mapsto f(t_i)]$
    and $f'(\varphi) = f'(R(x_1, \ldots x_k))[x_i \mapsto f'(t_i)]$.
We know that $f(R(x_1, \ldots x_k)) \sststile{}{x_1, \ldots x_k}$ \linebreak $f'(R(x_1, \ldots x_k))$.
Since $FV(f(R(x_1, \ldots x_k))) = \{ x_1, \ldots x_k \}$, by \axref{a3} we can conclude that $f(\varphi) \sststile{}{V} f'(R(x_1, \ldots x_k))[x_i \mapsto f(t_i)]$.
Since $f'(R(x_1, \ldots x_k))[x_i \mapsto f(t_i)] \sststile{}{V} f(t_i)\!\downarrow$, \rlem{cong-b} implies that
    $f'(R(x_1, \ldots x_k))[x_i \mapsto f(t_i)] \sststile{}{V} f'(\varphi)$.
By \axref{b2} we conclude that $f(\varphi) \sststile{}{V} f'(\varphi)$.
The same argument shows that $f'(\varphi) \sststile{}{V} f(\varphi)$.

Finally, it is easy to see that $f(t) = f'(t)$ for every $t \in PT(V)_s$.
Thus $f = f'$.
\end{proof}

Note that if $T$ is the standard monad $Term_\mathcal{F}$, then to define a morphism of monads $T \to T'$,
it is enough to specify for every $\sigma \in \mathcal{F}$, $\sigma : s_1 \times \ldots \times s_k \to s$,
a restricted term $\alpha(\sigma) \in T'(\{ x_1 : s_1, \ldots x_k : s_k \})$ such that $FV(\alpha(\sigma)) = \{ x_1, \ldots x_k \}$.
Then there is a unique morphism of monads $f : T \to T'$ such that $f(\sigma(x_1, \ldots x_k)) = \alpha(\sigma)$.

Now, let us define a category $\Th_\mathcal{S}$ of standard partial Horn theories.
Its objects are tuples $((\mathcal{S},\mathcal{F},\mathcal{P}),\mathcal{A})$, where $\mathcal{F}$ is a set of function symbols,
    $\mathcal{P}$ is a set of relation symbols, and $\mathcal{A}$ is a set of axioms over $(Term_\mathcal{F},Form_\mathcal{P})$.
Morphisms of standard partial Horn theories are morphisms of corresponding partial Horn theories.
Thus $\Th_\mathcal{S}$ is (equivalent to) a full subcategory of $\Th^T_\mathcal{S}$.

\subsection{Models of partial Horn theories}

Given a monad $T : \Set^\mathcal{S} \to \Set^\mathcal{S}$, we define a category of its partial algebras.
A \emph{partial algebra} over $T$ is a pair $(A,\alpha)$, where $A$ is an $\mathcal{S}$-set and $\alpha_V : Hom_{\PSet^\mathcal{S}}(V,A) \to Hom_{\PSet^\mathcal{S}}(T(V),A)$,
    where $\PSet$ is the category of sets and partial functions between them.
This pair must satisfy the following conditions:
\begin{itemize}
\item For every partial function $f : V \to A$, $\alpha_V(f) \circ \eta_V = f$.
\item For every total function $\rho : V \to T(V')$ and every partial function $f : V' \to A$, $\alpha_V(\alpha_{V'}(f) \circ \rho) = \alpha_{V'}(f) \circ \rho^*$.
\end{itemize}
A morphism of partial algebras $(A,\alpha)$ and $(A',\alpha')$ is a total morphism $h : A \to A'$ of $\mathcal{S}$-sets
    such that, for every partial function $f : V \to A$ and every $t \in T(V)_s$, if $\alpha_V(f)(t)$ is defined,
    then $\alpha'_V(h \circ f)(t)$ is also defined and $h(\alpha_V(f)(t)) = \alpha'_V(h \circ f)(t)$.

\begin{lem}[par-alg-str]
If $Term_\mathcal{F}$ is the standard monad, then categories of partial algebras over $Term_\mathcal{F}$
    and partial structures for signature $(\mathcal{S},\mathcal{F},\varnothing)$ as defined in \cite{PHL} are isomorphic.
\end{lem}
\begin{proof}
A partial structure for signature $(\mathcal{S},\mathcal{F},\varnothing)$ is an $\mathcal{S}$-set $A$ together with a collection of partial functions
    $A(\sigma) : A_{s_1} \times \ldots \times A_{s_n} \to A_s$ for every $\sigma \in \mathcal{F}$, $\sigma : s_1 \times \ldots \times s_n \to s$.
Given such partial structure, we define a partial algebra $F(A)$ over $Term_\mathcal{F}$ as $(A,\alpha)$, where $\alpha$ is defined as follows:
\begin{align*}
\alpha_V(f)(x) & = f(x) \\
\alpha_V(f)(\sigma(t_1, \ldots t_n)) & = A(\sigma)(\alpha_V(f)(t_1), \ldots \alpha_V(f)(t_n))
\end{align*}
For every morphism $h : A \to A'$ of partial structures, let $F(h) = h$.

For every partial algebra $(A,\alpha)$, we define a partial structure $G(A,\alpha)$.
Let $G(A,\alpha) = A$ and $G(A,\alpha)(\sigma)(a_1, \ldots a_n) = \alpha_{x_1, \ldots x_n}(x_i \mapsto a_i)(\sigma(x_1, \ldots x_n))$.
For every morphism $h : (A,\alpha) \to (A',\alpha')$ of partial algebras, let $G(h) = h$.
It is easy to see that functors $F$ and $G$ determine isomorphisms of categories.
\end{proof}

If $F : \Set^\mathcal{S} \to \Set$ is a left module of formulas over $T$, then we define a category of its partial algebras.
A \emph{partial algebra} over $(T,F)$ is a partial algebra $(A,\alpha)$ over $T$ together with a function $\beta_V : Hom_{\PSet^\mathcal{S}}(V,A) \to Hom_\Set(F(V),\Omega)$,
    where $\Omega = \{ \top, \bot \}$ is the set of truth-values.
This function must satisfy the following conditions:
\begin{itemize}
\item For every total function $\rho : V \to T(V')$ and every partial function $f : V' \to A$, $\beta_V(\alpha_{V'}(f) \circ \rho) = \beta_{V'}(f) \circ \rho^\circ$.
\item For every partial function $f : V \to A$, $\beta_V(f)(\top) = \top$.
\item For every partial function $f : V \to A$, $\beta_V(f)(\varphi \land \psi) = \beta_V(f)(\varphi) \land \beta_V(f)(\psi)$,
    where $P \land Q = \top$ if and only if $P = \top$ and $Q = \top$.
\end{itemize}
A morphism of partial algebras $(A,\alpha,\beta)$ and $(A',\alpha',\beta')$ is a morphism $h$ of partial algebras $(A,\alpha)$ and $(A',\alpha')$
    such that, for every partial function $f : V \to A$ and every $\varphi \in F(V)$, if $\beta_V(f)(\varphi) = \top$, then $\beta'_V(h \circ f)(\varphi) = \top$.

We define a function $\epsilon_V : Hom_{\PSet^\mathcal{S}}(V,A) \to Hom_\Set(E(V),\Omega)$ for the left module $E$ of equality.
Let $\epsilon_V(e(s,t,t')) = \top$ if and only if $\alpha_V(f)(t)$ and $\alpha_V(f)(t')$ are defined and equal.
If $F$ is a left module of formulas with equality over $T$, then we say that a partial algebra $(A,\alpha,\beta)$ is standard
    if, for every partial function $f : V \to A$, $e_V \circ \beta_V(f) = \epsilon_V(f)$, where $e_V : E(V) \to F(V)$.

\begin{lem}[par-alg-pred]
If $Term_\mathcal{F}$ is the standard monad and $Form_\mathcal{P}$ is the left module of Horn formulas,
    then categories of partial algebras over $(Term_\mathcal{F},Form_\mathcal{P})$ and partial structures for signature $(\mathcal{S},\mathcal{F},\mathcal{P})$ are isomorphic.
\end{lem}
\begin{proof}
A partial structure for signature $(\mathcal{S},\mathcal{F},\mathcal{P})$ is a partial structure $A$ for signature $(\mathcal{S},\mathcal{F},\varnothing)$
    together with a relation $A(R) \subseteq A_{s_1} \times \ldots \times A_{s_n}$ for every $R \in \mathcal{P}$, $R : s_1 \times \ldots \times s_n$.
Given such partial structure, we define a partial algebra $F(A)$ over $(Term_\mathcal{F},Form_\mathcal{P})$ as $(A,\alpha,\beta)$,
    where $(A,\alpha)$ is the partial algebra defined in \rlem{par-alg-str}, and $\beta$ defined as follows:
\begin{align*}
\beta_V(f)(t =_s t') & = \epsilon_V(e(s,t,t')) \\
\beta_V(f)(R(t_1, \ldots t_n)) & = \top \text{ if and only if } (\alpha_V(f)(t_1), \ldots \alpha_V(f)(t_n)) \in A(R) \\
\beta_V(f)(\varphi_1 \land \ldots \land \varphi_n) & = \beta_V(f)(\varphi_1) \land \ldots \land \beta_V(f)(\varphi_n)
\end{align*}
For every morphism $h : A \to A'$ of partial structures, let $F(h) = h$.

For every partial algebra $(A,\alpha,\beta)$, we define a partial structure $G(A,\alpha,\beta)$.
We already defined interpretation of function symbols in \rlem{par-alg-str}.
For every $R \in \mathcal{P}$, let $G(A,\alpha,\beta)(R) = \{ (a_1, \ldots a_n)\ |\ \beta_{x_1, \ldots x_n}(x_i \mapsto a_i)(R(x_1, \ldots x_n)) = \top \}$.
For every morphism $h : (A,\alpha,\beta) \to (A',\alpha',\beta')$ of partial algebras, let $G(h) = h$.
It is easy to see that functors $F$ and $G$ determine isomorphisms of categories.
\end{proof}

If $(T,F,\mu)$ is a monadic presentation, then we define a category of its partial algebras as a full subcategory of partial algebras over $(T,F)$.
A partial algebra $(A,\alpha,\beta)$ over $(T,F)$ is a partial algebra over $(T,F,\mu)$ if, for every partial function $f : V \to A$,
    every $t \in T(V)_s$ and every $\varphi \in F(V)$, $\alpha_V(f)(\mu_V(t,\varphi))$ is defined if and only if $\alpha_V(f)(t)$ is defined and $\beta_V(f)(\varphi) = \top$,
    and $\alpha_V(f)(\mu_V(t,\varphi))$ equals to $\alpha_V(f)(t)$ when it is defined.
The category of partial algebras over $(T,F,\mu)$ will be denoted by $\PAlg{(T,F,\mu)}$.

\begin{lem}
If $Term_\mathcal{F}$ is the standard monad and $\mathbb{T} = (Term_\mathcal{F},\mathcal{P},\mathcal{A})$ is a partial Horn theory,
    then categories of partial algebras over $P(\mathbb{T})$ and models of $\mathbb{T}$ as defined in \cite{PHL} are isomorphic.
\end{lem}
\begin{proof}
Using \rlem{par-alg-pred}, models of $\mathbb{T}$ can be described as partial algebras $(A,\alpha',\beta')$ over $(Term_\mathcal{F},Form_\mathcal{P})$
    such that, for every derivable sequent $\varphi \ssststile{}{V} \psi$ of $\mathbb{T}$ and every partial function $f : V \to A$, $\beta'_V(f)(\varphi) = \beta'_V(f)(\psi)$.

Let $(A,\alpha,\beta)$ be a partial algebra over $P(\mathbb{T})$.
Then we define a partial algebra $F(A,\alpha,\beta)$ over $(Term_\mathcal{F},Form_\mathcal{P})$.
Let $F(A,\alpha,\beta) = (A,\alpha',\beta')$, where $\alpha'_V(f)(t) = \alpha_V(f)([t|_\top]_\sim)$ and $\beta'_V(f)(\varphi) = \alpha_V(f)([\varphi]_\sim)$,
    where $[t|_\top]_\sim$ and $[\varphi]_\sim$ are equivalence classes of $t_\top$ and $\varphi$ in $P(V)$ and $F(V)$ respectively.
Then $F(A,\alpha,\beta)$ is a model of $\mathbb{T}$.
Indeed, if $\varphi \ssststile{}{V} \psi$ is a theorem of $\mathbb{T}$, then $\varphi' \ssststile{}{V} \psi'$
    is also a theorem of $\mathbb{T}$, where $\varphi' = \varphi \land x_1 \land \ldots \land x_n$, $\psi' = \psi \land y_1 \land \ldots \land y_k$,
    $x_1, \ldots x_n$ is the set of free variables of $\psi$, and $y_1, \ldots y_k$ is the set of free variables of $\varphi$.
It follows that $[\varphi']_\sim = [\psi']_\sim$; hence $\beta'_V(f)(\varphi') = \beta'_V(f)(\varphi')$.
But $\beta'_V(f)(\varphi) = \beta'_V(f)(\varphi')$ and $\beta'_V(f)(\psi) = \beta'_V(f)(\psi')$; hence $F(A,\alpha,\beta)$ is a model of $\mathbb{T}$.
If $h$ is a morphism of partial algebras over $P(\mathbb{T})$, then let $F(h) = h$.

Let $(A,\alpha',\beta')$ be a model of $\mathbb{T}$.
Then we define a partial algebra $G(A,\alpha',\beta')$ over $P(\mathbb{T})$.
Let $G(A,\alpha',\beta') = (A,\alpha,\beta)$, where $\beta_V(f)([\varphi]_\sim) = \beta'_V(f)(\varphi)$, and $\alpha_V(f)([t|_\varphi]_\sim)$ is defined
    if and only if $\alpha'_V(f)(t)$ is defined and $\beta'_V(f)(\varphi) = \top$, and in this case $\alpha_V(f)([t|_\varphi]_\sim) = \alpha'_V(f)(t)$.
These definitions do not depend on the choice of a representative of the equivalence classes.
Indeed, if $\varphi \sim \psi$, then $\varphi \ssststile{}{V} \psi$ is a theorem of $\mathbb{T}$,
    and in this case $\beta'_V(f)(\varphi) = \beta'_V(f)(\psi)$ since $A$ is a model of $\mathbb{T}$.
The same argument shows that the definition of $\alpha$ does not depend on the choice of a representative of $[t|_\varphi]_\sim$.
If $h$ is a morphism of models, then let $G(h) = h$.
It is easy to see that functors $F$ and $G$ determine isomorphisms of categories.
\end{proof}

Finally, we prove a proposition which shows that if $\mathbb{T}'$ is a partial Horn theory under $\mathbb{T}$,
    then we can think of models of $\mathbb{T}'$ as models of $\mathbb{T}$ with additional structure.

\begin{prop}[func-mod]
For every morphism of monadic presentations $f : (P,F,\mu) \to (P',F',\mu')$, there is a faithful functor $f^* : \PAlg{(P',F',\mu')} \to \PAlg{(P,F,\mu)}$
    such that $id_{(P,F,\mu)}^*$ is the identity functor and $(g \circ f)^* = f^* \circ g^*$.
\end{prop}
\begin{proof}
If $(A,\alpha,\beta)$ is a partial algebra over $(P',F',\mu')$, then let $f^*(A,\alpha,\beta) = (A, e \mapsto \alpha_V(e) \circ f_V, e \mapsto \beta_V(e) \circ f_V)$.
If $h : (A,\alpha,\beta) \to (A',\alpha',\beta')$ is a morphism of partial algebras, then let $f^*(h) = h$.
It is easy to see that these definitions satisfy all required conditions.
\end{proof}

\subsection{Properties of the category of theories}
\label{sec:prop}

Now we prove a few properties of the category of theories.
We begin with a proof of the existence of colimits.

\begin{prop}[th-cocomplete]
Category $\Th_\mathcal{S}$ is cocomplete.
\end{prop}
\begin{proof}
First, let $\{ \mathbb{T}_i \}_{i \in S} = \{ ((\mathcal{S},\mathcal{F}_i,\mathcal{P}_i),\mathcal{A}_i) \}_{i \in S}$ be a set of theories.
Then we can define its coproduct $\coprod\limits_{i \in S} \mathbb{T}_i$ as the theory with $\coprod\limits_{i \in S} \mathcal{F}_i$ as the set of function symbols and $\coprod\limits_{i \in S} \mathcal{A}_i$ as the set of axioms.
Morphisms $f_i : \mathbb{T}_i \to \coprod\limits_{i \in S} \mathbb{T}_i$ are defined in the obvious way.
If $g_i : \mathbb{T}_i \to X$ is a collection of morphisms, then \rprop{mor-def} implies that there is a unique morphism $g : \coprod\limits_{i \in S} \mathbb{T}_i \to X$
    satisfying $g(\sigma(x_1, \ldots x_n)) = g_i(\sigma(x_1, \ldots x_n))$ and $f(R(x_1, \ldots x_n)) = f_i(R(x_1, \ldots x_n))$
    for every $\sigma \in \mathcal{F}_i$ and $R \in \mathcal{P}_i$.

Now, let $f,g : \mathbb{T}_1 \to \mathbb{T}_2$ be a pair of morphisms of theories.
Then we can define their coequalizer $\mathbb{T}$ as the theory with the same set of function and predicate symbols as $\mathbb{T}_2$ and the set of axioms which consists of the axioms of $\mathbb{T}_2$
together with $\sststile{}{x_1, \ldots x_n} f(\sigma(x_1, \ldots x_n)) \cong g(\sigma(x_1, \ldots x_n))$ for each function symbols $\sigma$ of $\mathbb{T}_1$
and $f(R(x_1, \ldots x_n)) \ssststile{}{x_1, \ldots x_n} g(R(x_1, \ldots x_n))$ for each predicate symbols $R$ of $\mathbb{T}_1$.
Then we can define $e : \mathbb{T}_2 \to \mathbb{T}$ as identity function on terms and formulas.
By \rprop{mor-def}, $e \circ f = e \circ g$.
If $h : \mathbb{T}_2 \to X$ is such that $h \circ f = h \circ g$, then it extends to a morphism $\mathbb{T} \to X$ since additional axioms are preserved by the assumption on $h$.
This extension is unique since $e$ is an epimorphism.
\end{proof}

Now we give a characterization of monomorphisms.

\begin{prop}[mono]
A morphism of theories $f : \mathbb{T}_1 \to \mathbb{T}_2$ is a monomorphism if and only if, for every sequent $\varphi \sststile{}{V} \psi$ of $\mathbb{T}_1$,
if $f(\varphi) \sststile{}{V} f(\psi)$ is a theorem of $\mathbb{T}_2$, then $\varphi \sststile{}{V} \psi$ is a theorem of $\mathbb{T}_1$.
\end{prop}
\begin{proof}
First, let us prove the ``if'' part.
Let $g,h : \mathbb{T} \to \mathbb{T}_1$ be a pair of morphisms such that $f \circ g = f \circ h$.
If $t \in RTerm_\Sigma(V)_s$, then $\sststile{}{V} f(g(t)) \cong f(h(t))$; hence $\sststile{}{V} g(t) \cong h(t)$.
If $\varphi \in Form_\mathcal{P}(V)$, then $f(g(\varphi)) \ssststile{}{V} f(h(\varphi))$; hence $g(\varphi) \ssststile{}{V} h(\varphi)$.
Thus $g = h$.

Now, let us prove the ``only if'' part.
Suppose that $f$ is a monomorphism.
Let $\varphi \sststile{}{V} \psi$ be a sequent of $\mathbb{T}_1$ such that $f(\varphi) \sststile{}{V} f(\psi)$ is a theorem of $\mathbb{T}_2$.
Let $\mathbb{T}$ be a theory which consists of a single predicate symbol $R : s_1 \times \ldots \times s_n \times s'_1 \times \ldots \times s'_k$
where $s_1, \ldots s_n$ are sorts of variables in $FV(\varphi)$ and $s'_1, \ldots s'_k$ are sorts of variables in $FV(\psi)$.
Let $g : \mathbb{T} \to \mathbb{T}_1$ be a morphism defined by $g(R(x_1, \ldots x_n, y_1, \ldots y_k)) = \varphi \land y_1\!\downarrow \land \ldots \land y_k\!\downarrow$ and
let $h : \mathbb{T} \to \mathbb{T}_1$ be a morphism defined by $h(R(x_1, \ldots x_n, y_1, \ldots y_k)) = \varphi \land \psi$.
By \rprop{mor-def}, $f \circ g = f \circ h$, hence $g = h$ which implies that $\varphi \sststile{}{V} \psi$.
\end{proof}

Let $\mathbb{T} = ((\mathcal{S},\mathcal{F},\mathcal{P}),\mathcal{A})$ and $\mathbb{T}' = ((\mathcal{S}',\mathcal{F}',\mathcal{P}'),\mathcal{A}')$ be a pair of theories.
Then we say that $\mathbb{T}'$ is a \emph{subtheory} of $\mathbb{T}$ if $\mathcal{S}' \subseteq \mathcal{S}$, $\mathcal{F}' \subseteq \mathcal{F}$, $\mathcal{P}' \subseteq \mathcal{P}$ and $\mathcal{A}' \subseteq \mathcal{A}$.
If $\mathbb{T}'$ is a subtheory of a theory $\mathbb{T}$, then we often need to know when a theorem of $\mathbb{T}$ is a theorem of $\mathbb{T}'$.
The lemma below gives us a simple criterion for this.
First, we need to introduce a bit of notation.
Let $t$ is a term over the signature of $\mathbb{T}$ such that there is no subterm of a sort that does not belong to $\mathcal{S}'$.
Then we define a term $Ret(t)$ over the signature of $\mathbb{T}'$ as follows:
\begin{align*}
Ret(x) & = x \\
Ret(\sigma(t_1, \ldots t_n)) & = \sigma(Ret(t_1), \ldots Ret(t_n)) \text{, if $\sigma \in \mathcal{F}'$} \\
Ret(\sigma(t_1, \ldots t_n)) & = x_s \text{, if $\sigma \notin \mathcal{F}'$ and $\sigma : s_1 \times \ldots \times s_n \to s$}
\end{align*}
where $x_s$ is a variable of sort $s$ that is not a free variable of $t$.

If $\varphi$ is an atomic formula over the signature of $\mathbb{T}$, then we define a formula $Ret(\varphi)$ over the signature of $\mathbb{T}'$ as follows:
\begin{align*}
Ret(t = t') & = (Ret(t) = Ret(t')) \text{, if $Ret(t)$ and $Ret(t')$ are defined} \\
Ret(R(t_1, \ldots t_n)) & = R(Ret(t_1), \ldots Ret(t_n)) \text{, if $Ret(t_i)$ is defined for every $i$} \\
Ret(\varphi) & = \top \text{, otherwise}
\end{align*}
For an arbitrary Horn formula $\varphi$ we define $Ret(\varphi)$ as follows:
\[ Ret(\varphi_1 \land \ldots \land \varphi_n) = Ret(\varphi_1) \land \ldots \land Ret(\varphi_n) \]
For every restricted term $t|_\varphi$, let $Ret(t|_\varphi) = Ret(t)|_{Ret(\varphi)}$.
If $S$ is sequent $\varphi \sststile{}{V} \psi$ in the signature of $\mathbb{T}$,
then we define sequent $Ret(S)$ in the signature of $\mathbb{T}'$ as $Ret(\varphi) \sststile{}{V \cup FV(Ret(\varphi)) \cup FV(Ret(\psi))} Ret(\psi)$.

\begin{lem}[subtheory]
Let $\mathbb{T}'$ be a subtheory of $\mathbb{T}$.
Suppose that, for every axiom $S$ of $\mathbb{T}$, $Ret(S)$ is a theorem of $\mathbb{T}'$.
Then if a sequent in the signature of $\mathbb{T}'$ is provable in $\mathbb{T}$, then it is also provable in $\mathbb{T}'$.
\end{lem}
\begin{proof}
If $S$ is a sequent in the signature of $\mathbb{T}'$, then $Ret(S) = S$.
Thus we only need to prove that if $S$ is a theorem of $\mathbb{T}$, then $Ret(S)$ is a theorem of $\mathbb{T}'$.
For axioms this is true by assumption.
We need to check that $Ret(-)$ preserves inference rules.
This is clearly true for rules \axref{b1}-\axref{b6} and \axref{a1}.

Let us consider rule \axref{a2}.
Let $S$ equals $x = y \land \varphi \sststile{}{x:s,y:s,V} \varphi[y/x]$.
Note that $Ret(\varphi[y/x])$ is defined if and only if $Ret(\varphi)$ is defined, and in this case $Ret(\varphi[y/x]) = Ret(\varphi)[y/x]$.
Thus $Ret(S)$ is either of the form $x = y \land Ret(\varphi) \sststile{}{x:s,y:s,V,FV(Ret(\varphi))} Ret(\varphi)[y/x]$,
or of the form $x = y \sststile{}{x:s,y:s,V} \top$, or of the form $\top \sststile{}{x:s,y:s,V} \top$.
In all of these cases $Ret(S)$ is a theorem of $\mathbb{T}'$.

Finally, let us consider rule \axref{a3}.
To prove that it preserves the required property, it is enough to show that $\varphi$ is a formula of $(\mathcal{S}',\mathcal{F}',\mathcal{P}')$ if and only if $\varphi[t/x]$ is.
If $x \notin FV(\varphi)$, then $\varphi = \varphi[t/x]$.
Suppose that $x \in FV(\varphi)$ and $\varphi$ is a formula of $(\mathcal{S}',\mathcal{F}',\mathcal{P}')$.
If $x$ has sort $s$, then $s \in \mathcal{S}'$.
We need to show that a term of sort $s$ is a term of $(\mathcal{S}',\mathcal{F}',\mathcal{P}')$.
But this follows from the assumption on the set of function symbols.
\end{proof}

Sometimes it is convenient to have a sort which consists of a single element.
Let $\mathcal{S}$ be a set of sorts and let $s_0$ be a sort in $\mathcal{S}$.
Then we define a theory $\mathbb{T}_{s_0}$ which consists of a single function symbol $\emptyCtx : s_0$
    and two axioms: $\sststile{}{} \emptyCtx\!\downarrow$ and $\sststile{}{x} x = \emptyCtx$.
Then, for every theory $\mathbb{T} \in \Th_\mathcal{S}$, there is at most one morphism from $\mathbb{T}_{s_0}$ to $\mathbb{T}$.
If such morphism exists, we will say that $s_0$ is \emph{trivial} in $\mathbb{T}$.
Thus $\mathbb{T}_{s_0}/\Th_\mathcal{S}$ is (equivalent to) a full subcategory of $\Th_\mathcal{S}$.

As an application of the previous results we will prove that adding a trivial sort does not change the category of theories.
Every theory $\mathbb{T} \in \Th_\mathcal{S}$ is naturally a theory in $\Th_{\mathcal{S} \amalg \{ s_0 \}}$.
Thus we have a functor $i : \Th_\mathcal{S} \to \mathbb{T}_{s_0}/\Th_{\mathcal{S} \amalg \{ s_0 \}}$ such that $i(\mathbb{T}) = \mathbb{T} \amalg \mathbb{T}_{s_0}$.
\begin{prop}[triv-sort]
Functor $i : \Th_\mathcal{S} \to \mathbb{T}_{s_0}/\Th_{\mathcal{S} \amalg \{ s_0 \}}$ is an equivalence of categories.
\end{prop}
\begin{proof}
Let $\mathbb{T}_1,\mathbb{T}_2 \in \Th_\mathcal{S}$ be theories with $P(\mathbb{T}_i) = (T_i,F_i,\mu_i)$, $i = 1,2$.
Let $\alpha,\beta : \mathbb{T}_1 \to \mathbb{T}_2$ be morphisms such that $i(\alpha) = i(\beta)$.
Then, for every $t \in T_1$, sequent $\sststile{}{V} i(\alpha)(t) \cong i(\beta)(t)$ is a theorem of $i(\mathbb{T}_2)$.
Since $\mathbb{T}_2$ is (isomorphic to) a subtheory of $i(\mathbb{T}_2)$, by \rlem{subtheory}, sequent $\sststile{}{V} \alpha(t) \cong \beta(t)$ is a theorem of $\mathbb{T}_2$.
Analogously, we can show that $\alpha(\varphi) \ssststile{}{V} \beta(\varphi)$ is a theorem of $\mathbb{T}_2$ for every $\varphi \in F_1$.
Thus $i$ is faithful.

Let $\alpha : i(\mathbb{T}_1) \to i(\mathbb{T}_2)$ be a morphism.
For every $t \in T_1(V)_s$, let $\beta(t) = Ret(\alpha(t))$ and, for every $\varphi \in F_1(V)$, let $\beta(\varphi) = Ret(\alpha(\varphi))$.
Since $Ret$ preserves substitution, $\land$ and $\top$, this defines a morphism $\beta : \mathbb{T}_1 \to \mathbb{T}_2$.
Since $s_0$ is trivial in $i(\mathbb{T}_2)$, $Ret(t) = t$ and $Ret(\varphi) = \varphi$ for every restricted term $t$ and every formula $\varphi$.
Thus $i(\beta) = \alpha$; hence $i$ is full.

Let $\mathbb{T} \in \Th_{\mathcal{S} \amalg \{ s_0 \}}$ be a theory with trivial $s_0$.
Then we define a theory $\mathbb{T}' \in \Th_\mathcal{S}$.
It has a predicate symbol $R : s'_1 \times \ldots \times s'_n$ for every predicate symbol $R : s_1 \times \ldots \times s_n$ of $\mathbb{T}$,
    where $s'_1, \ldots s'_n$ is the subsequence of $s_1, \ldots s_n$ consisting of sorts from $\mathcal{S}$.
It has a function symbol $\sigma : s'_1 \times \ldots \times s'_n \to s$ for every function symbol
    $\sigma : s_1 \times \ldots \times s_n \to s$ of $\mathbb{T}$ such that $s \in \mathcal{S}$.
Also, for every function symbol $\sigma : s_1 \times \ldots \times s_n \to s_0$ of $\mathbb{T}$,
    there is a predicate symbol $R_\sigma : s_1' \times \ldots \times s'_n$ in $\mathbb{T}'$.

For every term $t$ of $\mathbb{T}$ of a sort from $\mathcal{S}$, we can define a term $r(t)$ of $\mathbb{T}'$.
Term $r(t)$ is obtained from $t$ by omitting subterms of sort $s_0$.
For every formula $\varphi$ of $\mathbb{T}$, we can define a formula $r(\varphi)$ of $\mathbb{T}'$:
\begin{align*}
r(t =_{s_0} t') & = \top \\
r(t =_s t') & = (r(t) =_s r(t')) \\
r(R(t_1, \ldots t_n)) & = R(r(t'_1), \ldots r(t'_n)) \\
r(\varphi_1 \land \ldots \land \varphi_n) & = r(\varphi_1) \land \ldots \land r(\varphi_n)
\end{align*}
where $t'_1, \ldots t'_n$ is the subsequence of $t_1, \ldots t_n$ consisting of the terms of sorts from $\mathcal{S}$.
Axioms of $\mathbb{T}'$ are sequents of the form $r(\varphi) \sststile{}{FV(r(\varphi)) \cup FV(r(\psi))} r(\psi)$ for every axiom $\varphi \sststile{}{V} \psi$ of $\mathbb{T}$.
It is easy to see that $i(\mathbb{T}')$ is isomorphic to $\mathbb{T}$.
Thus $i$ is essentially surjective on objects.
\end{proof}

% 3. Конструирование стабилизации что-то не пригодилось.

The construction of colimits in \rprop{th-cocomplete} implies that $L$ preserves colimits.
It follows that $\PSt_{\mathcal{S}_0}$ is cocomplete.
Since $L$ preserves colimits, the forgetful functor $\PSt_{\mathcal{S}_0} \to \mathbb{T}_{\mathcal{S}_0}/\Th_\mathcal{S}$
has a left adjoint $pst : \mathbb{T}_{\mathcal{S}_0}/\Th_\mathcal{S} \to \PSt_{\mathcal{S}_0}$, which we call the prestabilization functor.
More generally, for every $(\mathbb{T}_a,\alpha) \in \PSt_{\mathcal{S}_0}$,
we define a left adjoint $pst_{(\mathbb{T}_a,\alpha)} : \mathbb{T}_a/\Th_{\mathcal{S}} \to (\mathbb{T}_a,\alpha)/\PSt_{\mathcal{S}_0}$
to the forgetful functor $U_{(\mathbb{T}_a,\alpha)} : (\mathbb{T}_a,\alpha)/\PSt_{\mathcal{S}_0} \to \mathbb{T}_a/\Th_{\mathcal{S}}$.
Let $a : \mathbb{T}_a \to \mathbb{T}$ be an object of $\mathbb{T}_a/\Th_{\mathcal{S}}$.
Let $e : L^\infty(\mathbb{T}) \to E$ be the coequalizer of the following maps:
\[ \xymatrix{ \coprod\limits_{n \in \mathbb{N}} L^{n+1}(T_a) \ar@<+1ex>[rr]^{\coprod\limits_{n \in \mathbb{N}} L^n(f)} \ar@<-1ex>[rr]_{\coprod\limits_{n \in \mathbb{N}} L^n(g)}
    & & \coprod\limits_{n \in \mathbb{N}} L^n(L^\infty(\mathbb{T})) \ar@{^{(}->}[r]^-{i^n} & L^\infty(\mathbb{T}) } \]
where $L^\infty(X)$ is the following colimit:
\[ X \to X \amalg L(X) \to X \amalg L(X \amalg L(X)) \to \ldots \]
and $f,g : L(\mathbb{T}_a) \to L^\infty(\mathbb{T})$ are defined as follows:
$f$ is the composite $L(\mathbb{T}_a) \xrightarrow{\alpha} \mathbb{T}_a \xrightarrow{a} \mathbb{T} \hookrightarrow L^\infty(\mathbb{T})$,
and $g$ is the composite $L(\mathbb{T}_a) \xrightarrow{L(a)} L(\mathbb{T}) \hookrightarrow L^\infty(\mathbb{T})$.
Since $L$ preserves colimits, $L(E)$ is a coequalizer of $i^{n+1} \circ \coprod_{n \in \mathbb{N}} L^{n+1}(f)$ and $i^{n+1} \circ \coprod_{n \in \mathbb{N}} L^{n+1}(g)$.
By the universal property of coequalizers we have a map $\beta : L(E) \to E$.
We define $pst_{(\mathbb{T}_a,\alpha)}(a)$ as $(E,\beta)$, and morphism $(\mathbb{T}_a,\alpha) \to (E,\beta)$
as the composite $\mathbb{T}_a \xrightarrow{a} \mathbb{T} \hookrightarrow L^\infty(\mathbb{T}) \xrightarrow{e} E$.
This map is a morphism of algebras for $L$ since $e$ coequalizes $f$ and $g$.
Moreover, if $(D,\delta)$ is an object of $(\mathbb{T}_a,\alpha)/\PSt_{\mathcal{S}_0} $,
then a map $L^\infty(\mathbb{T}) \to D$ is a morphism of algebras if and only if it factors through $E$.
It follows that $pst_{(\mathbb{T}_a,\alpha)}$ is left adjoint to $U_{(\mathbb{T}_a,\alpha)}$.

The categories of stable and $c$-stable theories are cocomplete.
The inclusion functors $\St_{\mathcal{S}_0} \to \PSt_{\mathcal{S}_0}$ and $\cSt_{\mathcal{S}_0} \to \PSt_{\mathcal{S}_0}$ have left adjoints,
which are defined as the functors that add the required stability axioms.
We call these left adjoints \emph{the stabilization functors}.

% 4. Два куска про локализацию моделей и правые морфизмы.

\section{Simplicial categories corresponding to a model}

In this section we construct two simplicial categories $C_R(M)$ and $L(M)$ corresponding to a model $M$ of a dependent type theory $T$.
We prove that they are equivalent to each other and to the simplicial localization of $M$ as a category with weak equivalences.
We will use the following notation in this section: $N : \Cat \to \sSet$ is the ordinary nerve functor,
$N_\Delta : \Cat_\Delta \to \sSet$ and $\mathfrak{C}_\Delta : \sSet \to \Cat_\Delta$ are the homotopy coherent nerve functor and its left adjoint defined in \cite{lurie-topos},
and $N_T : \Mod{T} \to \sSet$ and $\mathfrak{C}_T : \sSet \to \Mod{T}$ are the nerve functor and its left adjoint constructed in section~\ref{sec:nerve}.

\subsection{Space of right morphisms}

For every quasicategory $C$ and every pair of objects $X$ and $Y$ of $C$, there is a Kan complex $Hom^R_C(X,Y)$ of right morphisms from $X$ to $Y$.
The set $Hom^R_C(X,Y)_{[n]}$ is defined as the set of simplices $s \in C_{[n+1]}$ such that $s|_{\Delta^{\{n+1\}}} = Y$ and $s|_{\Delta^{\{0, \ldots n\}}}$ is a constant simplex at $X$.
The fact that this simplicial set is a Kan complex is proved in \cite[Proposition~1.2.2.3]{lurie-topos}.

If $C$ is an arbitrary quasicategory, then there is no natural composition map $Hom^R_C(Y,Z) \times Hom^R_C(X,Y) \to Hom^R_C(X,Z)$.
But if $C = N_T(M)$, then there is such a map and it is associative and unital.
Let $(O^1,H^1) \in N_T(M)_{[n+1]}$ and $(O^2,H^2) \in N_T(M)_{[n+1]}$ be functions that represent simplices in $Hom^R_{N_T(M)}(Y,Z)$ and $Hom^R_{N_T(M)}(X,Y)$, respectively.
Then we define functions $(O,H) \in N_T(M)_{[n+1]}$ representing a simplex in $Hom^R_{N_T(M)}(X,Z)$.
There is a unique way to define $O$: $O_{n+1} = Z$ and $O_i = X$ for every $0 \leq i \leq n$.
For every $J = \{ j_1 < \ldots < j_k \} \subseteq [n+1]$, let $x : X, x_{j_2} : I, \ldots x_{j_{k-1}} : I \vdash H_J : Z$ be the term defined as $H^1_J[y \repl H^2_J]$.
It is easy to see that relation~\eqref{rel:right} holds.
Let us verify relation~\eqref{rel:left}:
\begin{align*}
H_{J \cup \{j\}}[x_j \repl left] & = \\
H^1_{J \cup \{j\}}[x_j \repl left][y \repl H^2_{J \cup \{j\}}[x_j \repl left]] & = \\
H^1_{\{j < \ldots < j_k\}}[x \repl H^1_{\{j_1 < \ldots < j\}}][y \repl H^2_{\{j < \ldots j_k\}}[x \repl H^2_{\{j_1 < \ldots < j\}}]] & = \\
H^1_{\{j < \ldots < j_k\}}[y \repl H^2_{\{j < \ldots j_k\}}] & = \\
H^1_{\{j < \ldots < j_k\}}[y \repl H^2_{\{j < \ldots < j_k\}}][x \repl H^1_{\{j_1 < \ldots j\}}[y \repl H^2_{\{j_1 < \ldots j\}}]] & = \\
H_{\{j < \ldots < j_k\}}[x \repl H_{\{j_1 < \ldots j\}}] & ,
\end{align*}
where $H^1_{\{j_1 < \ldots < j\}} = y$ and $H^2_{\{j_1 < \ldots < j\}} = x$ by assumption that $H^i$ represent simplices that are constant on the left face.
It is easy to see that $H$ also satisfies this assumption and that this function respects the face and degeneracy maps.
Thus, we have defined a map of simplicial sets $Hom^R_{N_T(M)}(Y,Z) \times Hom^R_{N_T(M)}(X,Y) \to Hom^R_{N_T(M)}(X,Z)$.
The fact that it is associative and unital follows from the fact that these properties hold for the substitution operation.

Thus, we have a fibrant simplicial category, which we denote by $C_R(M)$.

\subsection{Simplicial localization of a model}

Every model $M$ of a theory $T$ with $\Id$-types and $\Sigma$-types has the underlying fibration category $C(M)$ (see \cite{tt-fibr-cat}).
In particular, $C(M)$ is a category with weak equivalences.
In this section we prove that the homotopy coherent nerve of the simplicial localization of $C(M)$ is categorically equivalent to the quasicategory $N_T(M)$.

For every model $M$ of a theory with $\Id$-types, we define a simplicial category $L(M)$ which is weakly equivalent to $L^H C(M)$,
the usual hammock localization of $C(M)$, defined in \cite{Dwyer1980}.
First, let us define a $\Cat$-enriched category $L_C(M)$.
Its objects are contexts of $M$, that is elements of $\coprod_{n \in \mathbb{N}} M_{(ctx,n)}$.
If $\Gamma$ and $\Delta$ are contexts of $M$, then objects of $Hom(\Gamma,\Delta)$ are spans of the following form:
\[ \xymatrix{        & \Gamma' \ar[ld] \ar[rd] & \\
              \Gamma &                         & \Delta
            } \]
where the right map is any context morphism and the left map is a trivial fibration, that is, $\Gamma' = (\Gamma, x_1 : A_1, \ldots x_n : A_n)$
and the map $\Gamma' \to \Gamma$ is a weak equivalence in $C(M)$.
We will denote such a span by $(\Gamma',p,f)$, where $p : \Gamma' \to \Gamma$ and $f : \Gamma' \to \Delta$.

Morphisms between two such spans $(\Gamma_1,p_1,f_1)$ and $(\Gamma_2,p_2,f_2)$ are maps $g : E_1 \to E_2$ such that $p_2 \circ g = p_1$ and $f_2 \circ g = f_1$.
The identity morphisms and compositions are defined in the obvious way.
This construction of $Hom(\Gamma,\Delta)$ appears in \cite{cis10b} and \cite{Nikolaus2015}.
The canonical inclusion $N(Hom(\Gamma,\Delta)) \to L^H C(M)(\Gamma,\Delta)$ is a weak equivalence.
This is proved in \cite[Proposition~3.23]{cis10b} and \cite[Theorem~3.61]{Nikolaus2015}.

This construction of $L_C(M)$ works for any fibration category, but gives us only a bicategory.
If $M$ is a model of a type theory, then we can show that it is actually a strict 2-category.
The identity morphism is $(\Gamma,id_\Gamma,id_\Gamma)$.
The composition $\circ : Hom(\Delta,E) \times Hom(\Gamma,\Delta) \to Hom(\Gamma,E)$ is defined as follows:
if $(\Gamma',p_1,f_1)$ is an object of $Hom(\Gamma,\Delta)$ and $(\Delta',p_2,f_2)$ is an object of $Hom(\Delta,E)$,
then let $(\Delta',p_2,f_2) \circ (\Gamma,p_1,f_1)$ be the following pullback:
\[ \xymatrix{        &                                     & f_1^*(\Delta') \ar[dl] \ar[dr] &                                     & \\
                     & \Gamma' \ar[dl]_{p_1} \ar[dr]^{f_1} &                                & \Delta' \ar[dl]_{p_2} \ar[dr]^{f_2} & \\
              \Gamma &                                     & \Delta                         &                                     & E
            } \]
The composition is defined in the obvious way on morphisms.
Since pullbacks in models of type theories are strictly associative, this composition functor is also associative.
Analogously, the identity morphism is a strict unit for the composition.

Let $L(M)$ be the simplicial category obtained from $L_C(M)$ by appyling the nerve functor to $Hom$-categories.
Then there is a functor $L^H C(M) \to L(M)$.
This functor is defined as the identity function on objects.
If $\Gamma$ and $\Delta$ are two objects, then 0-simplices of $L^H C(M)(\Gamma,\Delta)$ are reduced diagrams of the form
$\Gamma \xleftarrow{p_1} \Gamma_1' \xrightarrow{f_1} \Gamma_2 \xleftarrow{p_2} \ldots \xrightarrow{f_{n-1}} \Gamma_n \xleftarrow{p_n} \Gamma_n' \xrightarrow{f_n} \Delta$,
where $p_i$ are trivial fibrations.
Such a diagram is reduced if all the maps in it are not identity morphisms except possibly $p_1$ and $f_n$.
For every such diagram, we define an object of $Hom(\Gamma,\Delta)$ as $(\Gamma_n',p_n,f_n) \circ \ldots \circ (\Gamma_1',p_1,f_1)$.
Morphisms of such diagrams are 1-simplices of $L^H C(M)(\Gamma,\Delta)$.
Every such morphism induces a morphism in $Hom(\Gamma,\Delta)$ between the corresponding objects.
Finally, $n$-simplices of $L^H C(M)(\Gamma,\Delta)$ are sequences of such morphisms of length $n$.
Every such sequence induces a sequence of morphisms in $Hom(\Gamma,\Delta)$.
Since such sequences correspond to simplices in $L(M)$, we obtain a map $L^H C(M)(\Gamma,\Delta) \to L(M)(\Gamma,\Delta)$.
It is easy to see that this defines a functor $L^H C(M) \to L(M)$.

The functor $L^H C(M) \to L(M)$ acts as the identity function on objects and, for every pair of objects $\Gamma$ and $\Delta$,
the map $L^H C(M)(\Gamma,\Delta) \to L(M)(\Gamma,\Delta)$ is a retraction of the canonical inclusion $L(M)(\Gamma,\Delta) \to L^H C(M)(\Gamma,\Delta)$.
In particular, it is a weak equivalence.
It follows that the functor $L^H C(M) \to L(M)$ is a weak equivalence of simplicial categories.

% 5. Кусок про симплициальные теории типов.

\section{Simplicial type theories}

In this section we define regular theory $T_\Delta$ under $coe_1$.
We prove that for every theory $T$ under $B$, the categories of models of $T$ and $T \amalg_{coe_1} T_\Delta$ are Quillen equivalent.
The advantage of theories under $T_\Delta$ is that there is a forgetful functor from the category of models of simplicial type theories to the category of simplicial categories.

Theory $T_\Delta$ is a regular theory with the following function symbols:
\begin{align*}
\Delta^n & : (ty,0) \text{, for every } n \geq 0 \\
\Delta^1_l & : (tm,0) \\
\Delta^1_r & : (tm,0) \\
\cmap{f} & : (tm,0) \to (tm,0) \text{, for every map $f$ in $\Delta$} \\
fill^n_i & : (ty,1) \times (tm,1)^n \times (tm,0) \to (tm,0) \text{, for every } n \geq 1 \text{, } 0 \leq i \leq n
\end{align*}

Theory $T_\Delta$ has the following typing axioms:
\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\RightLabel{, for every $n \geq 1$}
\UnaryInfC{$\Gamma \vdash \Delta^n\ type$}
\DisplayProof
\qquad
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \Delta^1_l : \Delta^1$}
\DisplayProof
\qquad
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \Delta^1_r : \Delta^1$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash a : \Delta^m$}
\RightLabel{, for every $f : \Delta^m \to \Delta^n$}
\UnaryInfC{$\Gamma \vdash \cmap{f}(a) : \Delta^n$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\def\extraVskip{1pt}
\Axiom$\fCenter \Gamma, x : \Delta^n \vdash A\ type$
\noLine
\UnaryInf$\fCenter \Gamma, y : \Delta^{n-1} \vdash a_j : A[x \repl \cmap{\delta^n_j}(y)] \text{, for every } 0 \leq j \leq n, j \neq i$
\noLine
\UnaryInf$\fCenter \Gamma \vdash d : \Delta^n$
\noLine
\UnaryInf$\fCenter S^n_i$
\RightLabel{, for every $0 \leq i \leq n$}
\def\extraVskip{2pt}
\UnaryInf$\fCenter \Gamma \vdash fill^n_i(x. A, y.a_0, \ldots y.a_{\hat{i}}, \ldots y.a_n, d) : A[x \repl d]$
\DisplayProof
\end{center}
\medskip
where $S^n_i$ consists of equations $\Gamma, z : \Delta^{n-2} \vdash a_j[y \repl \cmap{\delta^{n-1}_{k-1}}(z)] \deq a_k[y \repl \cmap{\delta^{n-1}_j}(z)]$
for every $0 \leq j < k \leq n$ such that $j \neq i$ and $k \neq i$.

The theory also has the following equality axioms:
\medskip
\begin{center}
\AxiomC{$\Gamma \vdash a : \Delta^n$}
\UnaryInfC{$\Gamma \vdash \cmap{id}(a) \deq a : \Delta^n$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash a : \Delta^m$}
\RightLabel{, $f : \Delta^m \to \Delta^n$, $f' : \Delta^n \to \Delta^k$}
\UnaryInfC{$\Gamma \vdash \cmap{f'}(\cmap{f}(a)) \deq \cmap{f' \circ f}(a) : \Delta^k$}
\DisplayProof
\end{center}
\medskip

Finally, for every $0 \leq i \leq n$ and $f : \Delta^m \to \Delta^n$ which factors through inclusion $\Lambda^n_i \to \Delta^n$, we have the following axiom:
\medskip
\begin{center}
\def\extraVskip{1pt}
\Axiom$\fCenter \Gamma, x : \Delta^n \vdash A\ type$
\noLine
\UnaryInf$\fCenter \Gamma, y : \Delta^{n-1} \vdash a_j : A[x \repl \cmap{\delta^n_j}(y)] \text{, for every } 0 \leq j \leq n, j \neq i$
\noLine
\UnaryInf$\fCenter \Gamma \vdash d : \Delta^m$
\noLine
\UnaryInf$\fCenter S^n_i$
\def\extraVskip{2pt}
\UnaryInf$\fCenter \Gamma \vdash fill^n_i(x.A, y.a_0, \ldots y.a_{\hat{i}}, \ldots y.a_n, \cmap{f}(d)) \deq a_k[y \repl \cmap{f'}(d)] : A[x \repl \cmap{f}(d)]$
\DisplayProof
\end{center}
where $k$ and $f'$ are such that $k \neq i$, $f = \delta^n_k \circ f'$, and $k$ is the minimal such number.

There is a morphism of theories $F : I \to T_\Delta$, which is defined as follows: $F(I) = \Delta^1$, $F(left) = \Delta^1_l$, and $F(right) = \Delta^1_r$.
This morphism has a retraction $G : T_\Delta \to I$, which is defined as follows: $G(\Delta^n) = I$, $G(\Delta^1_l) = left$, $G(\Delta^1_r) = right$, $G(\cmap{f})(a) = a$,
and $G(fill^n_i)(x.A, a_0, \ldots a_{i-1}, a_{i+1}, \ldots a_n, d) = a_k[y \repl d]$, where $k = 0$ if $i > 0$ and $k = 1$ if $i = 0$.

% 6. Более привычный синтаксис для алгебраических теорий типов.

We will give several proves by induction on a derivation of a sequent $\Gamma \vdash A \deq A'$ later in the paper.
Now, we describe another inference system in which it is easier to give such proofs.
The main problem with the system that we described is that it uses terms which contain a lot of redundant information.
The system that we are going to describe is also closer to the usual presentation of type theories.

Let $T$ be a contextual algebraic dependent type theory.
If we want to omit contexts in terms, then function symbols $ft$ and $ty$ do not make sense.
We can always infer the context of a term, but not its type, so we need an additional assumption on the theory.
We assume that, for every function symbol $\sigma : s_1 \times \ldots \times s_k \to (tm,n)$ of $T$,
there exists a term $\sigma_{ty}$ such that $ty$ does not appear in $\sigma_{ty}$ and the sequent $\sststile{}{x_1, \ldots x_k} ty(\sigma(x_1, \ldots x_k)) \cong \sigma_{ty}$ is derivable.
This is not a serious restriction since every theory is isomorphic to a theory with this property.
Indeed, we can just add a new function symbol $\sigma_{ty} : s_1 \times \ldots \times s_k \to (ty,n)$
and a new axiom $\sststile{}{x_1, \ldots x_k} ty(\sigma(x_1, \ldots x_k)) \cong \sigma_{ty}(x_1, \ldots x_k)$ for each function symbol $\sigma$ as above.

Let $\mathcal{C} = \{ ctx, tm \} \times \mathbb{N}$ be the set of sorts of $T$.
Let $Var$ be a set of variables and let $V$ be a $\mathcal{C}$-set of metavariables.
Then $Term^C_T(V)$ is the $\{ ty, tm \}$-set of (classes of $\alpha$-equivalence of) metaterms constructed inductively as follows:
\begin{enumerate}
\item If $x$ is a variable, then $x$ is a metaterm of sort $tm$.
\item If $z$ is a metavariable of sort $(tm,n)$ and $a_1, \ldots a_n$ are metaterms of sort $tm$, then $z[a_1, \ldots a_n]$ is a metaterm of sort $tm$.
\item If $z$ is a metavariable of sort $(p,n)$, $1 \leq m \leq n$, and $a_1, \ldots a_m$ are metaterms of sort $tm$, then $ft^{n-m}(e_p(z))[a_1, \ldots a_m]$ is a metaterm of sort $p$.
\item If $\sigma : (p_1,n_1) \times \ldots \times (p_k,n_k) \to (p,0)$ is a basic function symbol of $T$, $\{ A^j_i \}_{1 \leq i \leq k, 1 \leq j \leq n_i}$ are metaterm of sort $ty$,
$\{ x^j_i \}_{1 \leq i \leq k, 1 \leq j \leq n_i}$ are variables, and $b_1 : p_1, \ldots b_k : p_k$ are metaterms of the specified sorts,
then the following expression is a metaterm of sort $p$:
\[ \sigma((x^1_1 : A^1_1), \ldots (x^{n_1}_1 : A^{n_1}_1).\,b_1, \ldots ((x^1_k : A^1_k), \ldots (x^{n_k}_k : A^{n_k}_k).\,b_k) \]
\end{enumerate}
We will call metaterm of sort $ty$ \emph{types} and metaterms of sort $tm$ \emph{terms}.
We will sometimes omit metaterms in the expression $z[a_1, \ldots a_n]$.
In this case, the omitted metaterms are variables and it should be clear from the context the order of the variables (usually, this is just the order in which they appear in the context).
For example, the expression $\sigma(x y.\,A, z.\,A[x \repl z, y \repl z])$ is a shorthand for $\sigma(x y.\,A[x,y], z.\,A[x,y][x \repl z, y \repl z])$ (which equals to $\sigma(x y.\,A[x,y], z.\,A[z,z])$).

The set $FV(t)$ of free variable of a metaterm $t$ is defined as follows:
\begin{align*}
& FV(x) = \{ x \} \\
& FV(z[a_1, \ldots a_n]) = \bigcup_{1 \leq i \leq n} FV(a_i) \\
& FV(ft^{n-m}(e_p(z))[a_1, \ldots a_m]) = \bigcup_{1 \leq i \leq m} FV(a_i) \\
& FV(\sigma((x^1_1 : A^1_1), \ldots (x^{n_1}_1 : A^{n_1}_1).\,b_1, \ldots ((x^1_k : A^1_k), \ldots (x^{n_k}_k : A^{n_k}_k).\,b_k)) = \\
& \bigcup_{1 \leq i \leq k} (FV(b_i) \setminus \{ x^1_i, \ldots x^{n_i}_i \}) \cup (\bigcup_{1 \leq j \leq i} FV(A^j_i) \setminus \{ x^1_i, \ldots x^{j-1}_i \})
\end{align*}
The relation of $\alpha$-equivalence and the operation of substitution on metaterms are defined as usual.

A \emph{context} is an expression of the form $x_1 : A_1, \ldots x_n : A_n$, where $x_1, \ldots x_n$ are variables and $A_1, \ldots A_n$ are types such that $FV(A_i) \subseteq \{ x_1, \ldots x_{i-1} \}$.
We will say that a metaterm $t$ is \emph{appropriate} for a context $x_1 : A_1, \ldots x_n : A_n$ if $FV(t) \subseteq \{ x_1, \ldots x_n \}$.
A \emph{judgement} is an expression of one of the following forms:
\begin{align*}
\Gamma & \vdash A\ \type \\
\Gamma & \vdash a : A \\
\Gamma & \vdash A \deq A' \\
\Gamma & \vdash a \deq a' : A
\end{align*}
where $\Gamma$ is a context, $A$ and $A'$ are types appropriate for $\Gamma$, and $a$ and $a'$ are terms appropriate for $\Gamma$.
A \emph{formula} is a finite conjunction of judgements.

% 7. Общая лемма про объединения конфлюэнтных теорий.

\begin{lem}
Let $R_0$ and $R_1$ be two confluent term rewriting systems with the same set of terms such that the following conditions hold:
\begin{enumerate}
\item $R_1$ is stongly normalizable, that is every sequence of reductions $t_1 \Rightarrow_{R_1} t_2 \Rightarrow_{R_1} t_3 \Rightarrow_{R_1} \ldots$ is finite.
\item \label{it:red-comm} If $t \Rightarrow_{R_0}^* t_1$ and $t \Rightarrow_{R_1} t_2$, then there is a term $s$ such that $t_1 \Rightarrow_{R_1} s$ and $t_2 \Rightarrow_{R_1}^* \Rightarrow_{R_0}^* \Rightarrow_{R_1}^* s$.
\end{enumerate}
Then the union of $R_0$ and $R_1$ is confluent.
\end{lem}
\begin{proof}
For every triple of terms $t$, $t_1$, and $t_2$ together with two sequences of reductions $s_1$ and $s_2$ of the forms $t \Rightarrow_{R_0 \cup R_1}^* t_1$ and $t \Rightarrow_{R_0 \cup R_1}^* t_2$, respectively,
we define a size of quintuple $(t,t_1,t_2,s_1,s_2)$ as the pair $(l(s_1)+l(s_2),|t|)$, where $l(s)$ is the number of nontrivial blocks of the form $\Rightarrow_{R_0}^*$ separated by nontrivial blocks of the form $\Rightarrow_{R_1}^*$ in the sequence $s$
and $|t|$ is the maximum length of a reduction sequence of the form $\Rightarrow_{R_1}^*$ starting from the term $t$ (this is a well-defined function since $R_1$ is strongly normalizable).
The set of such pairs is ordered lexicographically.
We prove by induction on the size of $(t,t_1,t_2,s_1,s_2)$ that there exists term $t'$ together with sequences $s_1'$ and $s_2'$ of the forms
$t_2 \Rightarrow_{R_0 \cup R_1}^* t'$ and $t_1 \Rightarrow_{R_0 \cup R_1}^* t'$, respectively, such that $l(s_i') \leq l(s_i)$:
\[ \xymatrix@=1em{                                 & \ar[ld]_{l(s_1)} t \ar[rd]^{l(s_2)} &                                 \\
                   t_1 \ar@{-->}[rd]_{\leq l(s_2)} &                                     & t_2 \ar@{-->}[ld]^{\leq l(s_1)} \\
                                                   & t'                                  &
            } \]

If either of the sequences $s_1$ or $s_2$ is empty, then the result is obvious.
If the first nontrivial blocks in $s_1$ and $s_2$ are $\Rightarrow_{R_0}^*$, then we have the following reductions (we write the value of $l$ on the arrows):
\[ \xymatrix@=1em{                            &                                                & \ar[ld]_1 t \ar[rd]^1          &                                                &                            \\
                                              & t_1' \ar[ld]_{l(s_1)-1} \ar@{-->}[rd]_{\leq 1} &                                & t_2' \ar@{-->}[ld]^{\leq 1} \ar[rd]^{l(s_2)-1} &                            \\
                   t_1 \ar@{-->}[rd]_{\leq 1} &                                                & t' \ar@{-->}[ld] \ar@{-->}[rd] &                                                & t_2 \ar@{-->}[ld]^{\leq 1} \\
                                              & t_1'' \ar@{-->}[rd]_{\leq l(s_2)-1}            &                                & t_2'' \ar@{-->}[ld]^{\leq l(s_1)-1}            &                            \\
                                              &                                                & t''                            &                                                &
            } \]
A term $t'$ exists since $R_0$ is confluent and terms $t_1''$, $t_2''$, and $t''$ exist by the induction hypothesis since the sum of lengths of corresponding reduction sequences is less than $l(s_1) + l(s_2)$.

If the first nontrivial blocks in $s_1$ and $s_2$ are $\Rightarrow_{R_1}^*$, then we have the following reductions:
\[ \xymatrix@=1em{                     &                                       & \ar[ld]_0 t \ar[rd]^0          &                                       &                     \\
                                       & t_1' \ar[ld]_{l(s_1)} \ar@{-->}[rd]_0 &                                & t_2' \ar@{-->}[ld]^0 \ar[rd]^{l(s_2)} &                     \\
                   t_1 \ar@{-->}[rd]_0 &                                       & t' \ar@{-->}[ld] \ar@{-->}[rd] &                                       & t_2 \ar@{-->}[ld]^0 \\
                                       & t_1'' \ar@{-->}[rd]_{\leq l(s_2)}     &                                & t_2'' \ar@{-->}[ld]^{\leq l(s_1)}     &                     \\
                                       &                                       & t''                            &                                       &
            } \]
A term $t'$ exists since $R_0$ is confluent and terms $t_1''$, $t_2''$, and $t''$ exist by the induction hypothesis since the sum of lengths
of corresponding reduction sequences is less than or equal to $l(s_1) + l(s_2)$ and $|t_1'| < |t|$, $|t_2'| < |t|$, and $|t'| \leq |t_1'|$.

Finally, if the first nontrivial block in $s_1$ is $\Rightarrow_{R_0}^*$ and the first nontrivial block in $s_2$ is $\Rightarrow_{R_1}^*$, then we have the following reductions:
\[ \xymatrix@=1em{                     &                                         & \ar[ld]_1 t \ar[rd]^0          &                                              &                            \\
                                       & t_1' \ar[ld]_{l(s_1)-1} \ar@{-->}[rd]_0 &                                & t_2' \ar@{-->}[ld]^{\leq 1} \ar[rd]^{l(s_2)} &                            \\
                   t_1 \ar@{-->}[rd]_0 &                                         & t' \ar@{-->}[ld] \ar@{-->}[rd] &                                              & t_2 \ar@{-->}[ld]^{\leq 1} \\
                                       & t_1'' \ar@{-->}[rd]_{\leq l(s_2)}       &                                & t_2'' \ar@{-->}[ld]^{\leq l(s_1)-1}          &                            \\
                                       &                                         & t''                            &                                              &
            } \]
A term $t'$ exists by assumption~\eqref{it:red-comm} and terms $t_1''$, $t_2''$, and $t''$ exist by the induction hypothesis since the sum of lengths of reduction sequences starting from $t_1'$ (and also $t'$) is less than $l(s_1) + l(s_2)$,
the sum of lengths of reduction sequences starting from $t_2'$ is less than or equal to $l(s_1) + l(s_2)$, and $|t_2'| < |t|$.
\end{proof}

% 8. Это пойдет в тезис.

\section{Comparsion of algebraic and ordinary type theories}

It is well-known that standard examples of type theories (such as theories of identity types, $\Sigma$-types, and $\Pi$-types) are confluent.
Terms of algebraic type theories are similar to terms of usual type theories, but they still differ from them.
The first difference is that they have an explicit substitution operation.
Another difference is that they contain more information than ordinary terms so that the type and the context of a term can be inferred from it.
In this section we prove that it is often possible to show that an algebraic type theory is confluent if corresponding usual type theory is.

More precisely, for every contextual theory $T$, we will define a set $\Term_{T,\varphi}^s$ which can be described informally as the set of defined terms
in which function symbols $\ty_m$, $\ft_m$, and $\subst_{p,n,k}$ do not occur and in which we omit contexts in function symbols.
The precise definition of this set will be given in subsection~\ref{sec:subst}.
We also define there a reduction relation $\Rightarrow_{sf} \Rightarrow_s^\nf$ on this set.
This set corresponds to the set of terms of an ordinary type theory and the reduction relation corresponds to the usual reduction relation.
The idea is that $\Rightarrow_{sf}$ reduces one of the redexes and then $\Rightarrow_s^\nf$ evaluates all explicit substitution expressions.
Then we can prove the following theorem:

\begin{thm}[conf-comp]
Let $T$ be a contextual type theory with a reduction system in which typing rules are separated, substitution rules are stable, contexts are simple, and $\ty$-free rules preserve types.
If the abstract reduction system $(\Term_{T,\varphi}^s, \Rightarrow_{sf} \Rightarrow_s^\nf)$ is confluent for every pair $(\varphi,V) \in P_M$, then $T$ is also confluent.
\end{thm}

The technical assumptions that we put on the theory will be defined in this section.
The theorem itself follows from \rprop{ty-elim}, \rprop{ctx-elim}, and \rprop{subst-elim}.

\subsection{Typing axioms}

Let us begin by showing that a term rewriting system is confluent whenever the subsystem on terms without function symbols $\ty$ and $\ft$ is.
To do this we need to know that typing axioms are well-behaved in some sense.
\begin{defn}
A reduction rule is a \emph{typing rule} if it is of the form
\[ e_p(\sigma(x_1, \ldots x_k)) \Rightarrow s \]
where $\sigma$ is neither $\ft$ nor $\ty$ and the function symbols $\ft$ and $\ty$ are applied only to variables in $s$ (if they appear in this term).
A reduction rule $t \Rightarrow s$ is \emph{$\ty$-free (and $\ft$-free)} if the function symbols $\ft$ and $\ty$ do not appear in $t$.
We will say that a theory $T$ with a reduction system has \emph{separated typing rules} if every rule in the underlying term rewriting system of $T$ is either a typing rule or a $\ty$-free rule.
The sets of typing and $\ty$-free reduction rules will be denoted by $R^t_T$ and $R^{tf}_T$, respectively.

Let $T$ be a theory with separated typing rules.
We will say that $\ty$-free rules of $T$ \emph{preserve types} if there is a well-founded relation on the set of $\ty$-free rules of $T$ such that,
for every $\ty$-free rule $(t,s) \in R^{tf}_T$ and every substitution $\rho$ such that $t[\rho]$ is $\varphi$-defined,
terms $e_p(t[\rho])$ and $e_p(s[\rho])$ are equivalent in the system $(\Term_{T,\varphi}^d,\Rightarrow_{R^t_T \cup R^{tf'}_T, \varphi})$,
where $R^{tf'}_T$ is the set of $\ty$-free rules which are less than $(t,s)$.
\end{defn}

The main property of theories with separated typing axioms is proved in the following lemma:

\begin{lem}[types-red]
Let $T$ be a theory with separated typing axioms and let $(\varphi,V)$ be a pair in $P_M$.
Then the abstract reduction system $(\Term_{T,\varphi}^d,\Rightarrow_{R^t_T,\varphi})$ is strongly normalizing and confluent.
\end{lem}
\begin{proof}
Note that $V = \{ x_1, \ldots x_k \}$ and $e_{p_i}(x_i) \Rightarrow_\varphi s_i$ where $s_i$ is a term such that $FV(s_i) \subseteq \{ x_1, \ldots x_{i-1} \}$.
To show that the system is strongly normalizing we define, for each term $t$, an ordinal $|t|$ less than $\varepsilon_\omega$ such that if $t \Rightarrow_{R^t_T,\varphi} s$, then $|t| > |s|$.
\begin{align*}
|x_i| & = \varepsilon_{i-1} \\
|\ty(t)| = |\ft(t)| & = \omega^{|t|}\\
|\sigma(t_1, \ldots t_k)| & = |t_1| \oplus \ldots \oplus |t_k| \oplus 1
\end{align*}
where $\oplus$ is the natural sum of ordinals.

If $e_p(\sigma(t_1, \ldots t_k)) \Rightarrow_{R_T^t} s(e_{p_1}(t_1), \ldots e_{p_k}(t_k), t_1, \ldots t_k)$, then we need to show that $|e_p(\sigma(t_1, \ldots t_k))| > |s(e_{p_1}(t_1), \ldots e_{p_k}(t_k), t_1, \ldots t_k)|$.
Let $\alpha_i = |t_i|$ and let $\alpha$ be the maximum of $\alpha_1$, \ldots $\alpha_k$.
Then $|e_p(\sigma(t_1, \ldots t_k))| = \omega^{\alpha_1 \oplus \ldots \oplus \alpha_k \oplus 1} \geq \omega^{\alpha + 1}$.
Note that $\ft$ and $\ty$ do not occur in the term $s$.
It follows that
\begin{align*}
|s(e_{p_1}(t_1), \ldots e_{p_k}(t_k), t_1, \ldots t_k)| & = \omega^{\alpha_1} n_1 \oplus \ldots \oplus \omega^{\alpha_k} n_k \oplus \alpha_1 m_1 \oplus \ldots \oplus \alpha_k m_k \oplus c \\
                                                        & \leq \omega^\alpha n \oplus \alpha m \oplus c
\end{align*}
for some natural numbers $n_1$, \ldots $n_k$, $m_1$, \ldots $m_k$, $n$, $m$, and $c$.
Since $\alpha \leq \omega^\alpha$ and $1 \leq \omega^\alpha$, we have $\omega^\alpha n \oplus \alpha m \oplus c \leq \omega^\alpha (n + m + c) < \omega^{\alpha + 1}$.

If $e_p(x_i) \Rightarrow_\varphi s_i$, then $FV(s_i) \subseteq \{ x_1, \ldots x_{i-1} \}$.
It follows that $|e_p(x_i)| = \omega^{\varepsilon_{i-1}} = \varepsilon_{i-1} > |s_i|$ since $|s_i|$ involves only ordinals less than $\varepsilon_{i-1}$.
This finishes the proof that $(\Term_{T,\varphi}^d,\Rightarrow_{R^t_T,\varphi})$ is strongly normalizing.

By Newman's lemma (see \cite[Lemma~2.2.5]{ohlebusch-advanced} for a proof), to prove that a strongly normalizing system is confluent it is enough to show that it is locally confluent,
that is if $a \Rightarrow_{R^t_T} b$ and $a \Rightarrow_{R^t_T} c$, then there exists a term $d$ such that $b \Rightarrow_{R^t_T}^* d$ and $c \Rightarrow_{R^t_T}^* d$.
This is obvious in our case since the rules in $R^t_T$ do not overlap.
\end{proof}

We will need the following general lemma about term rewriting systems:

\begin{lem}[conf-nf]
Let $\Rightarrow_1$ and $\Rightarrow_2$ be abstract reduction systems on the same set $A$.
Let $A'$ be a subset of $A$ containing all $\Rightarrow_1$-normal forms and let $\Rightarrow_0$ be an abstract reduction system on it.
Suppose that the following conditions hold:
\begin{itemize}
\item The system $(A',\Rightarrow_0)$ is confluent.
\item The system $(A,\Rightarrow_1)$ is confluent and weakly normalizing.
\item If $a,b \in A$ are such that $a \Rightarrow_2 b$, then $a$ and $b$ are joinable under the relation $\Rightarrow_1^\nf \Rightarrow_0^*$.
\end{itemize}
Then any two $\Rightarrow_2$-equivalent elements $a,b \in A$ are joinable under $\Rightarrow_1^\nf \Rightarrow_0^*$.
\end{lem}
\begin{proof}
Since being joinable is a symmetric relation, we can assume that $\Rightarrow_2$ is also symmetric.
Let $a_1$, \ldots, $a_n$ be a sequence such that $a_i \Rightarrow_2 a_{i+1}$ for every $1 \leq i < n$.
We prove that $a_1$ and $a_n$ are joinable under $\Rightarrow_1^\nf \Rightarrow_0^*$ by induction on $n$.
If $n = 0$, then this follows from the fact that $(A,\Rightarrow_1)$ is weakly normalizable.
Suppose $n > 0$.
We have $a_1 \Rightarrow_1^\nf a_1'$, $a_1' \Rightarrow_0^* c_1$, $a_{n-1} \Rightarrow_1^\nf a_{n-1}'$, $a_{n-1}' \Rightarrow_0^* b$ by assumption.
We have $a_n \Rightarrow_1^\nf a_n'$, $a_n' \Rightarrow_0^* c_2$, $a_{n-1} \Rightarrow_1^\nf a_{n-1}'$, $a_{n-1}' \Rightarrow_0^* c$ by the induction hypothesis.
Since $\Rightarrow_0$ is confluent, $c \Rightarrow_0^* d$ and $c \Rightarrow_0^* d$:
\[ \xymatrix@=1em{  a_1 \ar[rr]^{\Rightarrow_2^*} \ar@{-->}[d]^{\Rightarrow_1^\nf}  &                                   & a_{n-1} \ar[rr]^{\Rightarrow_2} \ar@{-->}[d]^{\Rightarrow_1^\nf}          &                                   & a_n \ar@{-->}[d]^{\Rightarrow_1^\nf}  \\
                    a_1' \ar@{-->}[rd]_{\Rightarrow_0^*}                            &                                   & a_{n-1}' \ar@{-->}[ld]_{\Rightarrow_0^*} \ar@{-->}[rd]^{\Rightarrow_0^*}  &                                   & a_n' \ar@{-->}[ld]^{\Rightarrow_0^*}  \\
                                                                                    & b \ar@{-->}[rd]_{\Rightarrow_0^*} &                                                                           & c \ar@{-->}[ld]^{\Rightarrow_0^*} &                                       \\
                                                                                    &                                   & d                                                                         &                                   &
                 } \]
\end{proof}

Let $\Term_{T,\varphi}^t$ be the subset of $\Term_{T,\varphi}^d$ consisting of terms in which function symbols $\ty$ and $\ft$ do not occur.
Let $\Rightarrow_{R_T^t,\varphi}$ be the union of $\Rightarrow_{R^t_T}$ and $\Rightarrow_\varphi$.
Then every $\Rightarrow_{R_T^t,\varphi}$-normal form belongs to $\Term_{T,\varphi}^t$.
This implies that the relation $\Rightarrow_{R^{tf}_T} \Rightarrow_{R^t_T,\varphi}^\nf$ is an abstract reduction system on $\Term_{T,\varphi}^t$
Let us denote the relation $\Rightarrow_{R^{tf}_T} \Rightarrow_{R^t_T,\varphi}^\nf$ by $\Rightarrow_{tf}$
Now we can prove that the confluence under $\Rightarrow_{tf}$ implies the confluence under $\Rightarrow_{R_T,\varphi}$:

\begin{prop}[ty-elim]
Let $T$ be a theory with a reduction system in which typing axioms are spearated and $\ty$-free axioms preserve types.
Suppose that the abstract reduction system $(\Term_{T,\varphi}^t, \Rightarrow_{tf})$ is confluent.
Then $T$ is also confluent.
\end{prop}
\begin{proof}
If $<$ is a well-founded relation on a set $A$, then we can define a well-founded relation on the set of subset of $A$ as follows.
A subset $S$ is less than a subset $T$ if and only there is an element $a \in T$ which is greater than every element of $S$.
It is easy to see that this relation is well-founded.
Let $R^{tf'}_T$ be a subset of $R^{tf}_T$.
Then we prove by induction on $R^{tf'}_T$ that terms $t$ and $s$ are joinable under $\Rightarrow_{R_T^t,\varphi}^\nf \Rightarrow_{tf}^*$
whenever they are equivalent in the system $(\Term_{T,\varphi}^d,\Rightarrow_{R^t_T \cup R^{tf'}_T, \varphi})$.

The abstract reduction system $(\Term_{T,\varphi}^d,\Rightarrow_{R^t_T,\varphi})$ is normalizing and confluent by \rlem{types-red}.
Thus we can apply \rlem{conf-nf} with $A = \Term^d_{T,\varphi}$, $A' = \Term^t_{T,\varphi}$, $(\Rightarrow_0) = (\Rightarrow_{tf})$, $(\Rightarrow_1) = (\Rightarrow_{R^t_T,\varphi})$, and $(\Rightarrow_2) = (\Rightarrow_{R_T,\varphi})$
to show that the terms $t$ and $s$ are joinable under $\Rightarrow_{R_T^t,\varphi}^\nf \Rightarrow_{tf}^*$.
To do this, we need to prove that if $t \Rightarrow_{R^t_T \cup R^{tf'}_T, \varphi} s$, then $t$ and $s$ are joinable.

Note that $\Rightarrow_{R^t_T \cup R^{tf'}_T, \varphi}$ is the union of $\Rightarrow_{R^t_T,\varphi}$ and $\Rightarrow_{R^{tf'}_T}$.
If $t \Rightarrow_{R^t_T,\varphi} s$, then this is obvious, so let us assume that $t \Rightarrow_{R^{tf'}_T} s$.
Then $t = c[a[\rho]/x]$ and $s = c[b[\rho]/x]$ for some terms $a$, $b$, and $c$ and some substitution $\rho$ such that $(a,b) \in R^{tf'}_T$.
Since the left hand side of reduction rules in $R_T^{tf}$ does not contain function symbols $\ft$ and $\ty$,
reductions $\Rightarrow_{R_T^{tf}}$ and $\Rightarrow_{R_T^t,\varphi}$ can overlap only in a term of the form $e_p(\sigma(t_1, \ldots t_k))$ as follows:
$e_p(\sigma(t_1, \ldots t_k)) \Rightarrow_{R_T^t,\varphi} u[t_1/x_1, \ldots t_k/x_k]$ for some term $u$ and $e_p(\sigma(t_1, \ldots t_k)) \Rightarrow_{R_T^{tf}} e_p(v)$ for some term $v$.
We may assume that $\Rightarrow_{R_T^t,\varphi}$-reductions occur only in such overlappings since other $\Rightarrow_{R_T^t,\varphi}$-redexes occur inside either $c$ or $\rho$, so if we reduce them in $c[a[\rho]/x]$ and $c[b[\rho]/x]$
we will still have a reduction of the form $c'[a[\rho']/x] \Rightarrow_{R_T^{tf}}^* c'[b[\rho']/x]$ for some $c'$ and $\rho'$ such that $c \Rightarrow_{R_T^t,\varphi}^\nf c'$ and $\rho \Rightarrow_{R_T^t,\varphi}^\nf \rho'$.

Since $a$, $b$, $c'$, and $\rho'$ do not contain $\Rightarrow_{R_T^t,\varphi}$-redexes, such a redex can occur in terms $c'[a[\rho']/x]$ and $c'[b[\rho']/x]$ only when $c'$ contains subterms of the form $e_p(x)$.
So there is a sequence of natural number $n_1, \ldots n_k$, and a term $c''$ which does not contain function symbols $\ty$ and $\ft$ such that the following equations hold:
\begin{align*}
c'[a[\rho']/x] & = c''[\ft^{n_1}(e_p(a[\rho']))/y_1, \ldots \ft^{n_k}(e_p(a[\rho']))/y_k, a[\rho']/z] \\
c'[b[\rho']/x] & = c''[\ft^{n_1}(e_p(b[\rho']))/y_1, \ldots \ft^{n_k}(e_p(b[\rho']))/y_k, b[\rho']/z].
\end{align*}

Since $\ty$-free axioms of $T$ preserve types, terms $e_p(a[\rho'])$ and $e_p(b[\rho'])$ are equivalent in the system $(\Term_{T,\varphi}^d,\Rightarrow_{R^t_T \cup R^{tf''}_T, \varphi})$ for some $\mathcal{A}_{tf}'' < \mathcal{A}_{tf}'$.
It follows that $c'[a[\rho']/x]$ and $c'''$ are also equivalent in this system, where $c'''$ is the following term:
\[ c''[\ft^{n_1}(e_p(b[\rho']))/y_1, \ldots \ft^{n_k}(e_p(b[\rho']))/y_k, a[\rho']/z]. \]
Since $\mathcal{A}_{tf}'' < \mathcal{A}_{tf}'$, we can apply the induction hypothesis to conclude that these terms are joinable under $\Rightarrow_{R_T^t,\varphi}^\nf \Rightarrow_{tf}^*$.
Since $c''$ does not contain function symbols $\ty$ and $\ft$, terms $c'''$ and $c'[b[\rho']/x]$ are also joinable.
Finally, \rlem{conf-nf} implies that terms $c'[a[\rho']/x]$ and $c'[b[\rho']/x]$ are joinable.
\end{proof}

\subsection{Contexts}

In this subsection we will work with contextual theories (see \cite{alg-tt} for a definition of a contextual theory).
If $T$ is a contextual theory, then we have a set of function symbols $\mathcal{F}_0$ (which we call \emph{basic function symbols}) such that the set of function symbols of $T$ consists of the following function symbols:
\begin{align*}
* & : (\ctx,0) \\
\ft_m & : (\ty,m) \to (\ctx,m) \\
\ty_m & : (\tm,m) \to (\ty,m) \\
v_{m,i} & : (\ctx,m) \to (\tm,m) \text{, } 0 \leq i < m \\
\subst_{p,m,0} & : (\ctx,m) \times (p,0) \times (p,m) \\
\subst_{p,m,k} & : (p,k) \times (\tm,m)^k \to (p,m) \text{, } k > 0 \\
\sigma_m & : (\ctx,m) \times (p_1,n_1+m) \times \ldots \times (p_k,n_k+m) \to (p,n+m)
\end{align*}
where $\sigma : (p_1,n_1) \times \ldots \times (p_k,n_k) \to (p,n)$ is a basic function symbol, $m \in \mathbb{N}$, and $p_1, \ldots, p_k, p \in \{ \ty, \tm \}$.
Moreover, we may assume that $n = 0$ for every $\sigma \in \mathcal{F}_0$.
Note that we omit the context for function symbols $\subst_{p,m,k}$ when $k > 0$.
We can do this since it can be inferred from any of the last $k$ parameters.

Let $T$ be a contextual theory and let $\mathcal{F}_0$ be the set of its basic function symbols.
Let $\mathcal{F}_0'$ be the set consisting of elements of $\mathcal{F}_0$, function symbols $v_i$ for all $i \in \mathbb{N}$, and function symbols $\subst_{p,n,k}$.
If $t$ is a term of $T$ in which function symbols $\ft_m$ and $\ty_m$ do not occur, then we can define a term $U(t) \in \Term_{\mathcal{F}'_0}$ in the obvious way:
\begin{align*}
U(x) & = x \\
U(\sigma_m(\Gamma, t_1, \ldots t_k)) & = \sigma(U(t_1), \ldots U(t_k)) \\
U(v_{n,i}(\Gamma)) & = v_i \\
U(\subst_{p,m,0}(\Gamma,t)) & = U(t) \\
U(\subst_{p,m,k}(t, a_1, \ldots a_k)) & = \subst_{p,m,k}(U(t), U(a_1), \ldots U(a_k))
\end{align*}

Let $\Term_T^c$ be the image of $\Term_T^t$ under $U$.
We define a reduction relation $\Rightarrow_{cf}$ on $\Term_T^c$ as the image of $\Rightarrow_{tf}$ under $U$.

If $t \in \Term_T^t$, then let $C(t)$ be the set of terms discarded by $U$.
That is, $C(t)$ is defined inductively as follows:
\begin{align*}
C(x) & = \varnothing \\
C(\sigma_m(\Gamma, t_1, \ldots t_k)) & = \{ \Gamma \} \cup \bigcup_{1 \leq i \leq k} C(t_i) \\
C(v_{n,i}(\Gamma)) & = \{ \Gamma \} \\
C(\subst_{p,m,0}(t)) & = C(t) \\
C(\subst_{p,m,k}(t, a_1, \ldots a_k)) & = C(t) \cup \bigcup_{1 \leq i \leq k} C(a_i)
\end{align*}
Sometimes we need to regard $C(t)$ as a sequence in which case the order is 
There is a natural linear order on the multiset $C(t)$, so we can also think of it as a sequence of terms.

\begin{defn}[simp-ctx]
We will say that a contextual theory $T$ with separated typing axioms \emph{has simple contexts} if the following conditions hold:
\begin{enumerate}
\item For all terms $t$ and $s$ in $\Term_T^t$ such that $(t,s) \in R^{tf}_T$, the sequence $C(t)$ consists of distinct variables and the set $C(s)$ consists of strongly normalizable terms.
\item For every basic function symbol $\sigma : (p_1,n_1) \times \ldots \times (p_k,n_k) \to (p,0)$ and every $1 \leq i \leq k$,
if the sequent $\sststile{}{\Gamma, x_1, \ldots x_k} \sigma_m(\Gamma, x_1, \ldots x_k)\!\downarrow$ is derivale,
then there exists a term $A_{\sigma,i}$ such that $FV(A_{\sigma,i}) \subseteq \{ \Gamma, x_1, \ldots x_{i-1} \}$ and the sequent $\sststile{}{\Gamma, x_1, \ldots x_i} e_{p_i}(x_i) = A_{\sigma,i}$ is derivale.
\item There is a well-founded relation on the set $\Term_T^t$ such that each element of $C(s)$ is less than $t$ whenever $t \Rightarrow_{tf}^* s$.
\end{enumerate}
\end{defn}
These conditions are true for all theories that occur in practice.
The first condition is easy to verify, but the last two require some explanation.
The second condition might not hold in a reasonable theory, but every theory is isomoprhic to a theory in which it holds.
For example, we can define a theory of $\Pi$-types in which the application function symbol is defined as follows:
\[ \ft(\ft(B)) = \Gamma \land \ty(b) = B \land \ty(a) = \ft(B) \sststile{}{\Gamma,B,b,a} \app_m(\Gamma,B,b,a)\!\downarrow \]
This theory does not satisfy the second condition of \rdefn{simp-ctx}, but it is easy to modify the definition of $\app$ to fix this problem:
\[ \ft(A) = \Gamma \land \ft(B) = A \land \ty(b) = B \land \ty(a) = A \sststile{}{\Gamma,A,B,b,a} \app_m(\Gamma,A,B,b,a)\!\downarrow \]
This trick can be applied to any theory to get a theory satisfying the second condition of \rdefn{simp-ctx}.

The third condition of \rdefn{simp-ctx} holds if the underlying term rewriting system of $T$ is strongly normalizing.
Indeed, we can define a well-founded relation on the set $\Term_T^t$ as follows: $t_1 > t_2$ if $|t_1| > |t_2|$ where $|t_i|$ is the length of the longest sequence of reductions starting from $t_i$.
If $t \Rightarrow_{tf}^* s$, then $|t| > |s|$ and if $\Gamma \in C(s)$, then $\Gamma$ is a subterm of $s$, so $|s| \geq |\Gamma|$.
Many theories that occur in practice are strongly normalizing, but this property is hard to verify, so let us describe another condition on a theory which implies that it has simple contexts.

Let $T$ be a theory such that, for every pair of terms $t$ and $s$ in $\Term_T^t$ such that $(t,s) \in R^{tf}_T$, the set $C(t)$ consists of distinct variables and $C(s) \subseteq C(t)$.
This condition is easy to verify and it holds for all theories that occur in practice.
If it holds, then the first and the third conditions of \rdefn{simp-ctx} hold for $T$.
The first condition holds for obvious reasons.
To prove the third condition, we define a well-founded relation on the set $\Term_T^t$ as follows: $t_1 > t_2$ if the size of $t_1$ is greater than the size of $t_2$.
If $t \Rightarrow_{tf}^* s$, then it is easy to see that $C(s) \subseteq C(t)$.
Thus, for every $\Gamma \in C(s)$, the size of $\Gamma$ is less than the size of $t$.

A theory with simple contexts satisfies the following properties:
\begin{enumerate}
\item \label{it:red-fib} Let $t$ be a term in $\Term_T^t$ such that $U(t) \Rightarrow_{cf} s$ for some term $s$.
Then there exists a term $s'$ such that $t \Rightarrow_{tf} s'$ and $U(s') = s$.
This follows from the fact that the same reduction rule that we applied to $U(t)$ also applies to $t$ since there is no additional conditions on $t$ by the first condition of \rdefn{simp-ctx}.
\item \label{it:red-nf} $U$ preserves normal forms. This follows from the previous property.
\end{enumerate}

Now we can show that we can omit contexts if they are simple:
\begin{prop}[ctx-elim]
Let $T$ be a theory with simple contexts and let $(\varphi,V)$ be a pair in $P_M$.
Then the abstract reduction system $(\Term_{T,\varphi}^t, \Rightarrow_{tf})$ is confluent if and only if the system $(\Term_{T,\varphi}^c, \Rightarrow_{cf})$ is.
\end{prop}
\begin{proof}
If $(\Term_{T,\varphi}^t,\Rightarrow_{tf})$ is confluent, then it is easy to show that $(\Term_{T,\varphi}^c,\Rightarrow_{cf})$ is also confluent.
Indeed, if we have a term $t \in \Term_{T,\varphi}^c$ such that $t \Rightarrow_{cf}^* t_1$ and $t \Rightarrow_{cf}^* t_2$,
then there is a term $t' \in \Term_{T,\varphi}^t$ and \eqref{it:red-fib} implies that there are terms $t_1'$ and $t_2'$ such that
$t' \Rightarrow_{tf}^* t_1'$, $t' \Rightarrow_{tf}^* t_2'$, $U(t_1') = t_1'$, and $U(t_2') = t_2'$.
Since $t'$ is confluent, there exists a term $s'$ such that $t_1' \Rightarrow_{tf}^* s'$ and $t_2' \Rightarrow_{tf}^* s'$.
Hence $U(t_1') \Rightarrow_{cf}^* U(s')$ and $U(t_2') \Rightarrow_{cf}^* U(s')$.

Let us prove the converse.
Suppose that $\Rightarrow_{cf}$ is confluent.
Let $t_1$ and $t_2$ be equivalent terms in $(\Term_{T,\varphi}^t,\Rightarrow_{tf})$.
We proceed by induction on $t_1$ (using the well-founded relation from \rdefn{simp-ctx}).
Since the reduction relation on $\Term_{T,\varphi}^c$ is confluent, we have a term $s' \in \Term_{T,\varphi}^c$ such that $U(t_1) \Rightarrow_{cf}^* s'$ and $U(t_2) \Rightarrow_{cf}^* s'$.
By \eqref{it:red-fib}, there are terms $s_1$ and $s_2$ such that $t_1 \Rightarrow_{tf}^* s_1$, $t_2 \Rightarrow_{tf}^* s_2$, and $U(s_1) = U(s_2) = s'$.

To prove that $s_1$ and $s_2$ are joinable, it is enough to show that sequences $C(s_1)$ and $C(s_2)$ are equal up to equivalence.
Indeed, if this is true, then we can conclude that $j$-th elements of $C(s_1)$ and $C(s_2)$ are joinable by the induction hypothesis for every $j$.
This implies that $s_1$ and $s_2$ are also joinable.
The first elements of $C(s_i)$ are equivalent to $\ctx(s_i)$ and they are equivalent since $s_1$ and $s_2$ are.
The second condition of \rdefn{simp-ctx} implies that other elements of $C(s_i)$ are determined by the first element.
Indeed, if $\sststile{}{V} \sigma_m(\Delta, t_1, \ldots t_k)\!\downarrow$ is derivable, then $\sststile{}{V} e_{p_i}(t_i) = A_{\sigma,i}[\Delta/\Gamma, t_1/x_1, \ldots t_{i-1}/x_{i-1}]$ is also derivable.
This implies that $j$-th element of $C(s_i)$ are equivalent for all $j$.
\end{proof}

\subsection{Substitution}
\label{sec:subst}

Let $T$ be a contextual theory with simple contexts.
Evety such theory $T$ has a few $\ty$-free axioms that involve function symbols $\subst_{p,m,k}$.
Corresponding $\Rightarrow_{cf}$-reduction rules look like this:
\begin{align}
\subst_{\tm,n,k}(v_i, a_1, \ldots a_k) & \Rightarrow a_{k-i} \label{ax:v-left} \\
\subst_{p,k,k}(a, v_{k-1}, \ldots v_0) & \Rightarrow a \label{ax:v-right} \\
\subst_{p,n,m}(\sigma_m(b_1, \ldots b_k), a_1, \ldots a_m) & \Rightarrow \sigma_n(b_1', \ldots b_k') \label{ax:sigma} \\
\subst_{p,n,k}(\subst_{p,k,m}(a, a_1, \ldots a_m), b_1, \ldots b_k) & \Rightarrow \subst_{p,n,m}(a, a_1', \ldots a_m') \label{ax:assoc}
\end{align}
where $a_i' = \subst_{\tm,n,k}(a_i, b_1, \ldots b_k)$ and $b_i'$ equals to
\[ \subst_{p_i,n+n_i,m+n_i}(b_i, \wk^{n_i}_{\tm,n}(a_1), \ldots \wk^{n_i}_{\tm,n}(a_m), v_{n_i-1}, \ldots v_0), \]
where $\wk^k_{p,n}(a) = \subst_{p,n+k,n}(a, v_{n+k-1}, \ldots v_k)$.

Let $T$ be a theory with simple contexts.
A $\ty$-free rule is called a \emph{substitution rule} if it is one of the rules for $\subst_{p,n,k}$ listed above.
Other $\ty$-free rule are called \emph{$\subst$-free rules}.
The sets of substitution and $\subst$-free rules will be denoted by $R^s_T$ and $R^{sf}_T$, respectively.

The relation $\Rightarrow_{R_T^{tf}}$ is the union of relations $\Rightarrow_{R_T^s}$ and $\Rightarrow_{R_T^{sf}}$.
It follows that the relation $\Rightarrow_{cf}$ is also the union of two relations $\Rightarrow_s$ and $\Rightarrow_{sf}$.
The former consists of rules \eqref{ax:v-left}-\eqref{ax:assoc} and the latter is the image of $\Rightarrow_{R_T^{sf}} \Rightarrow_{R_T^t,\varphi}^\nf$ under $U$.
Let $\Term_{T,\varphi}^s$ be the subset of $\Term_{T,\varphi}^c$ consisting of $\Rightarrow_s$-normal forms.

\begin{lem}[subst-red]
Let $T$ be a theory with separated substitution axioms.
Then the abstract reduction system $(\Term_{T,\varphi}^c,\Rightarrow_s)$ is confluent and strongly normalizing for every $(\varphi,V) \in P_M$.
\end{lem}
\begin{proof}
Let us first prove that the system is stronly normalizing.
For each term $t$, we define a natural number $|t|_1$ greater than $1$ and an ordinal $|t|_2$ less than $\epsilon_0$ such that $(|t|_2,|t|_1)$ is less than $(|t'|_2,|t'|_1)$ in the lexicographical order whenever $t \Rightarrow_s t'$.
First, let us define $|t|_1$:
\begin{align*}
|v_i|_1 & = 2 \\
|x|_1 & = 2 \\
|\sigma_m(b_1, \ldots b_k)|_1 & = |b_1|_1 + \ldots + |b_k|_1 \\
|\subst_{p,n,m}(a, a_1, \ldots a_m)|_1 & = |a|_1 (|a_1|_1 + \ldots + |a_m|_1 + 2)
\end{align*}
This interpretation of function symbols is strictly monotone in each variable.
Let us show that if $t$ reduces to $t'$ by one of the rules \eqref{ax:v-left}, \eqref{ax:v-right}, \eqref{ax:assoc}, then $|t|_1 > |t'|_1$:
\[ |\subst_{\tm,n,k}(v_i, a_1, \ldots a_k)|_1 = 2 |a_1|_1 + \ldots + 2 |a_k|_1 + 4 > |a_{k-i}|_1, \]
\[ |\subst_{p,k,k}(a, v_{k-1}, \ldots v_0)|_1 = |a|_1 (2 k + 2) \geq 2|a|_1 > |a|_1. \]
Finally, note that
\begin{align*}
|\subst_{p,n,k}(\subst_{p,k,m}(a, a_1, \ldots a_m), b_1, \ldots b_k)|_1 & = |a|_1 (A + 2) B, \\
|\subst_{p,n,m}(a, a_1', \ldots a_m')|_1 = |a|_1 (|a_1|_1 B + \ldots |a_m|_1 B + 2) & = |a|_1 (A B + 2),
\end{align*}
where $A = |a_1|_1 + \ldots + |a_m|_1$ and $B = |b_1|_1 + \ldots + |b_k|_1 + 2$.
Since $|a|_1 > 0$ and $B > 1$, $|a|_1 (A + 2) B - |a|_1 (A B + 2) = 2 |a|_1 (B - 1) > 0$.

Now, let us define $|t|_2$:
\begin{align*}
|v_i|_2 & = 0 \\
|x|_2 & = 0 \\
|\sigma_m(b_1, \ldots b_k)|_2 & = |b_1|_2 \oplus \ldots \oplus |b_k|_2 \oplus 1 \\
|\subst_{p,n,m}(a, a_1, \ldots a_m)|_2 & = 
\left\{
\begin{array}{c l}	
     2 \otimes |a|_2 & \forall i (|a_i|_2 = 0) \\
     |a|_1 \otimes (|a_1|_2 \oplus \ldots \oplus |a_m|_2) & |a|_2 = 0, \exists i (|a_i|_2 \neq 0) \\
     \omega^{|a|_2} \otimes (|a_1|_2 \oplus \ldots \oplus |a_m|_2) & |a|_2 \neq 0, \exists i (|a_i|_2 \neq 0)
\end{array}\right.
\end{align*}
Let us check that these interpretations are strictly monotone.
This is obvious for $\sigma_m$.
Let us check this for $\subst_{p,n,m}$.
First, suppose that $|a'|_2 > |a|_2$.
If $\forall i (|a_i|_2 = 0)$, then
\[ |\subst_{p,n,m}(a', a_1, \ldots a_m)|_2 = 2 \otimes |a'|_2 > 2 \otimes |a|_2 = |\subst_{p,n,m}(a, a_1, \ldots a_m)|_2, \]
so we may assume that $\exists i (|a_i|_2 \neq 0)$.
Let $A = |a_1|_2 \oplus \ldots \oplus |a_m|_2$.
If $|a|_2 \neq 0$, then
\[ |\subst_{p,n,m}(a', a_1, \ldots a_m)|_2 = \omega^{|a'|_2} \otimes A > \omega^{|a|_2} \otimes A = |\subst_{p,n,m}(a, a_1, \ldots a_m)|_2. \]
If $|a|_2 = 0$, then
\[ |\subst_{p,n,m}(a', a_1, \ldots a_m)|_2 = \omega^{|a'|_2} \otimes A \geq \omega \otimes A > \]
\[ |a|_1 \otimes A = |\subst_{p,n,m}(a, a_1, \ldots a_m)|_2. \]
Now, suppose that $|a_j'|_2 > |a_j|_2$ for some $j$ and $|a_i'| = |a_i|$ for every $i \neq j$.
If $\exists i (|a_i|_2 \neq 0)$, then it is obvious that $|\subst_{p,n,m}(a, a_1', \ldots a_m')|_2$ is greater than $|\subst_{p,n,m}(a, a_1, \ldots a_m)|_2$,
so we may assume that $\forall i (|a_i|_2 = 0)$.
If $|a|_2 = 0$, then
\[ |\subst_{p,n,m}(a, a_1', \ldots a_m')|_2 = |a|_1 \otimes A' > 0 = |\subst_{p,n,m}(a, a_1, \ldots a_m)|_2, \]
where $A' = |a_1'|_2 \oplus \ldots \oplus |a_m'|_2$.
If $|a|_2 \neq 0$, then
\[ |\subst_{p,n,m}(a, a_1', \ldots a_m')|_2 = \omega^{|a|_2} \otimes A' \geq \omega^{|a|_2} > \]
\[ 2 \otimes |a|_2 = |\subst_{p,n,m}(a, a_1, \ldots a_m)|_2. \]
This compltes the proof that the interpretation of $\subst_{p,n,m}$ is strictly monotone.

Now, we need to show that $|t|_2 \geq |t'|_2$ whenever $t \Rightarrow_s t'$.
Moreover, we need to show that this inequality is strict whenever $t$ reduces to $t'$ by the rule \eqref{ax:sigma}.
We do not need to prove strict inequality for other rules since $|t|_1 > |t'|_1$ in this case.
This inequality is obvious for the second rule:
\[ |\subst_{p,k,k}(a, v_{k-1}, \ldots v_0)|_2 = 2 \otimes |a|_2 \geq |a|_2. \]
Let us prove that $|\subst_{\tm,n,k}(v_i, a_1, \ldots a_k)|_2 \geq |a_{k-i}|_2$.
If $|a_{k-i}|_2 = 0$, then this is obvious.
If $|a_{k-i}|_2 \neq 0$, then $|\subst_{\tm,n,k}(v_i, a_1, \ldots a_k)|_2 = 2 \otimes (|a_1|_2 \oplus \ldots \oplus |a_k|_2) \geq |a_{k-i}|_2$.

Let us consider the third rule.
Note that $|\wk^k_{p,n}(a)|_2 = 2 \otimes |a|_2$.
If $\forall i (|a_i|_2 = 0)$, then
\[ |\subst_{p,n,m}(\sigma_m(b_1, \ldots b_k), a_1, \ldots a_m)|_2 = 2 \otimes |b_1|_2 \oplus \ldots \oplus 2 \otimes |b_k|_2 \oplus 2 > \]
\[ 2 \otimes |b_1|_2 \oplus \ldots \oplus 2 \otimes |b_k|_2 \oplus 1 = |\sigma_n(b_1', \ldots b_k')|_2. \]
If $\exists i (|a_i|_2 \neq 0)$, then 
\[ |\subst_{p,n,m}(\sigma_m(b_1, \ldots b_k), a_1, \ldots a_m)|_2 = \omega^{|b_1|_2 \oplus \ldots \oplus |b_k|_2 \oplus 1} \otimes (|a_1|_2 \oplus \ldots \oplus |a_m|_2), \]
\[ |\sigma_n(b_1', \ldots b_k')|_2 = (\omega^{|b_1|_2} \oplus \ldots \oplus \omega^{|b_k|_2} \oplus c) \otimes 2 \otimes (|a_1|_2 \oplus \ldots \oplus |a_m|_2) \oplus 1 < \]
\[ (\omega^{|b_1|_2} \oplus \ldots \oplus \omega^{|b_k|_2} \oplus c \oplus 1) \otimes 2 \otimes (|a_1|_2 \oplus \ldots \oplus |a_m|_2), \]
where $c$ is some natural number.
Thus we just need to prove that
\[ (\omega^{|b_1|_2} \oplus \ldots \oplus \omega^{|b_k|_2} \oplus c \oplus 1) \otimes 2 < \omega^{|b_1|_2 \oplus \ldots \oplus |b_k|_2 \oplus 1}. \]
Let $\beta$ be the maximum of $|b_1|_2$, \ldots $|b_k|_2$.
Then
\[ (\omega^{|b_1|_2} \oplus \ldots \oplus \omega^{|b_k|_2} \oplus c \oplus 1) \otimes 2 \leq \omega^\beta 2 (k + c + 1) < \omega^{\beta + 1} \leq \omega^{|b_1|_2 \oplus \ldots \oplus |b_k|_2 \oplus 1}. \]

Finally, let us consider the fourth rule.
Let $A_1 = |a_1|_1 + \ldots + |a_m|_1$, $A_2 = |a_1|_2 + \ldots + |a_m|_2$, $B = |b_1|_2 \oplus \ldots \oplus |b_k|_2$, and $a_i' = \subst_{\tm,n,k}(a_i', b_1, \ldots b_k)$.
If $\forall i (|a_i|_2 = 0)$ and $\forall i (|b_i|_2 = 0)$, then
\[ |\subst_{p,n,k}(\subst_{p,k,m}(a, a_1, \ldots a_m), b_1, \ldots b_k)|_2 = 4 \otimes |a|_2 \geq \]
\[ 2 \otimes |a|_2 = |\subst_{p,n,m}(a, a_1', \ldots a_m')|_2. \]
If $\forall i (|a_i|_2 = 0)$, $\exists i (|b_i|_2 \neq 0)$, and $|a|_2 = 0$, then
\[ |\subst_{p,n,k}(\subst_{p,k,m}(a, a_1, \ldots a_m), b_1, \ldots b_k)|_2 = |a|_1 (A_1 + 2) \otimes B > \]
\[ |a|_1 A_1 \otimes B = |\subst_{p,n,m}(a, a_1', \ldots a_m')|_2. \]
If $\forall i (|a_i|_2 = 0)$, $\exists i (|b_i|_2 \neq 0)$, and $|a|_2 \neq 0$, then
\[ |\subst_{p,n,k}(\subst_{p,k,m}(a, a_1, \ldots a_m), b_1, \ldots b_k)|_2 = \omega^{2 \otimes |a|_2} \otimes B \geq \omega^{|a|_2} \otimes \omega \otimes B >  \]
\[ \omega^{|a|_2} \otimes A_1 \otimes B = |\subst_{p,k,m}(a, a_1', \ldots a_m')|_2. \]
If $\exists i (|a_i|_2 \neq 0)$, $\forall i (|b_i|_2 = 0)$, and $|a|_2 = 0$, then both sides equal to $2 |a|_1 \otimes A_2$.
If $\exists i (|a_i|_2 \neq 0)$, $\forall i (|b_i|_2 = 0)$, and $|a|_2 \neq 0$, then both sides equal to $2 \otimes \omega^{|a|_2} \otimes A_2$.
If $\exists i (|a_i|_2 \neq 0)$, $\exists i (|b_i|_2 \neq 0)$, and $|a|_2 = 0$, then
\[ |\subst_{p,n,k}(\subst_{p,k,m}(a, a_1, \ldots a_m), b_1, \ldots b_k)|_2 = \omega^{|a|_1 \otimes A_2} \otimes B, \]
\[ |\subst_{p,k,m}(a, a_1', \ldots a_m')|_2 = |a|_1 \otimes (\omega^{|a_1|_2 \oplus \ldots \oplus |a_m|_2} \oplus c) \otimes B, \]
where $c$ is some natural number.
Let $\alpha$ be the maximum of $|a_1|_2$, \ldots $|a_m|_2$.
Then $\omega^{|a|_1 \otimes A_2} \geq \omega^{2 \otimes \alpha} \geq \omega^{\alpha + 1} > \omega^\alpha |a|_1 (m + c) \geq |a|_1 \otimes (\omega^{|a_1|_2 \oplus \ldots \oplus |a_m|_2} \oplus c)$.
If $\exists i (|a_i|_2 \neq 0)$, $\exists i (|b_i|_2 \neq 0)$, and $|a|_2 \neq 0$, then
\[ |\subst_{p,n,k}(\subst_{p,k,m}(a, a_1, \ldots a_m), b_1, \ldots b_k)|_2 = \omega^{\omega^{|a|_2} \otimes A_2} \otimes B, \]
\[ |\subst_{p,k,m}(a, a_1', \ldots a_m')|_2 = \omega^{|a|_2} \otimes (\omega^{|a_1|_2 \oplus \ldots \oplus |a_m|_2} \oplus c) \otimes B, \]
where $c$ is some natural number.
Let $\alpha$ be the maximum of $|a_1|_2$, \ldots $|a_m|_2$.
Then $\omega^{|a|_2} \otimes (\omega^{|a_1|_2 \oplus \ldots \oplus |a_m|_2} \oplus c) \leq \omega^{|a|_2} \otimes \omega^\alpha (m + c) < \omega^{|a|_2 \oplus \alpha \oplus 1}$.
Thus we just need to show that $\omega^{|a|_2} \otimes \alpha \geq |a|_2 \oplus \alpha \oplus 1$.
If $\alpha = 1$, then $\omega^{|a|_2} > |a|_2 \oplus 2$ since $|a|_2 > 0$.
If $\alpha > 1$, then $\omega^{|a|_2} \otimes \alpha \geq \omega^{|a|_2} \oplus \alpha > |a|_2 \oplus 1 \oplus \alpha$.

This completes the proof that the system is strongly normalizing.
It follows that the system is confluent if and only if it is locally confluent and local confluence is easy to verify by considering all critical pairs.
\end{proof}

To show that we can eliminate function symbols $\subst_{p,n,m}$, we need to assume that reduction rules are well-behaved in some sense with respect to substitutions.
For example, we can assume that the only reduction rules in which function symbols $\subst_{p,n,m}$ occur on the left are the ones listed above.
But there is an example of a theory which we want to consider and which does not satisfy this condition.
Namely, the theory of the interval type with the $\sigma$ rule:
\[ \coe_1(\wk^1_{\ty,0}(A), a, i) \Rightarrow a \]
Note that this theory is not confluent as formulated since
\begin{align*}
\coe_1(\wk^1_{\ty,0}(I_0), \leftI_0, \rightI_0) & \Rightarrow \leftI_0 \\
\coe_1(\wk^1_{\ty,0}(I_0), \leftI_0, \rightI_0) & \Rightarrow \coe_1(I_1, \leftI_0, \rightI_0)
\end{align*}
and terms $\leftI_0$ and $\coe_1(I_1, \leftI_0, \rightI_0)$ are not joinable.
To fix this problem, we need to give a few definitions.
We will say that a term $t$ of sort $(p,n)$ is \emph{well-behaved} if the following conditions hold:
\begin{itemize}
\item $t$ is a $\Rightarrow_s$-normal form.
\item All variables in $t$ have sorts greater than or equal to $n$.
\item For every subterm of the form $\subst_{p,m,k}(x, t_1, \ldots t_k)$, it is true that $k \geq n$ and $t_i = v_{m-i}$ for each $i \leq n$.
\item All indices except for the ones mentioned in the previous condition are bound in $t$.
\end{itemize}
We will say that $\subst$-free rules are \emph{well-behaved} if, for every such $\subst$-free rule $(t,s)$ of sort $(p,n)$, the following conditions hold:
\begin{itemize}
\item Terms $U(t)$ and $U(\nf^t(s))$ are well-behaved, where $\nf^t(s)$ is the normal form of $s$ with respect to $\Rightarrow_{T,\varphi}^t$.
\item For every substitution $\rho$ consisting of $\Rightarrow_s$-normal forms, if $U(t)[\rho] \in \Term_{T,\varphi}^c$, then $t' (\Rightarrow_{sf} \Rightarrow_s^\nf)^* s'$,
where $t'$ and $s'$ are $\Rightarrow_s$-normal forms of $U(t)[\rho]$ and $U(\nf^t(s))[\rho]$, respectively.
\end{itemize}

\begin{example}
If $t$ and $s$ are $\Rightarrow_s$-normal forms of sort $(p,0)$ and function symbols $\subst_{p,n,k}$ do not occur in $t$, then $(t,s)$ is well-behaved.
\end{example}

\begin{example}
To make the $\sigma$ rule well-behaved, we just need to add rules of the form $\coe_1(A, a, i) \Rightarrow a$ for every term $A$ in which $0$-th index does not occur.
\end{example}

If $t$ is a well-behaved term of sort $(p,n)$, then we define a term $L^m(t)$ of sort $(p,m)$ for every $m \in \mathbb{N}$ as follows:
\begin{align*}
L^m(x) & = x \\
L^m(v_i) & = v_i \\
L^m(\sigma_l(t_1, \ldots t_k)) & = \sigma_{l-n+m}(L^m(t_1), \ldots L^m(t_k)) \\
L^m(\subst_{q,l,k}(x, v_{l-1}, \ldots v_{l-n}, t_1, \ldots t_{k-n})) & = \\
\subst_{q,l-n+m,k-n+m}(x, v_{l-n+m-1}, \ldots v_{l-n}, & L^m(t_1), \ldots L^m(t_{k-n}))
\end{align*}
The fact that $t$ is well-behaved guarantees that this is a well-defined function and the term $L^m(t)$ is also well-behaved.

\begin{lem}[lift]
For every well-behaved term $t$ of sort $(p,n)$, terms
\[ \subst_{p,m,n}(t, a_1, \ldots a_n) \]
and
\[ L^m(t)[\rho] \]
are joinable under $\Rightarrow_s$, where
\[ \rho(x) = \subst_{q,m+i,n+i}(x, \wk_{\tm,m}^i(a_1), \ldots \wk_{\tm,m}^i(a_n), v_{i-1}, \ldots v_0). \]
\end{lem}
\begin{proof}
It is easy to prove by induction on a subterm $s$ of $t$ that terms
\[ \subst_{q,m+l,n+l}(s, \wk_{\tm,m}^l(a_1), \ldots \wk_{\tm,m}^l(a_n), v_{l-1}, \ldots v_0) \]
and
\[ L^m(s)[\rho] \]
are joinable.
Since $\wk_{\tm,m}^0(a_i) \Rightarrow_s a_i$, terms $\subst_{p,m,n}(t, a_1, \ldots a_n)$ and $L^m(s)[\rho]$ are equivalent.
Since the latter term is a normal form and $\Rightarrow_s$ is confluent, it follows that the former term reduces to it.
\end{proof}

We will say that $\subst$-free rules are \emph{stable} if they are well-behaved and, for every $\subst$-free rule $(t,s)$ and every $m \in \mathbb{N}$,
there exists a $\subst$-free rule $(t',s')$ such that $U(t') = L^m(U(t))$ and $U(\nf^t(s')) = L^m(U(\nf^t(s)))$.

\begin{prop}[subst-elim]
Let $T$ be a theory with stable $\subst$-free rules and let $(\varphi,V)$ be a pair in $P_M$.
If the abstract reduction system $(\Term_{T,\varphi}^s, \Rightarrow_{sf} \Rightarrow_s^\nf)$ is confluent, then $(\Term_{T,\varphi}^c,\Rightarrow_{cf})$ is also confluent.
\end{prop}
\begin{proof}
We apply \rlem{conf-nf} to the following data:
\begin{align*}
A & = \Term_{T,\varphi}^c \\
A' & = \Term_{T,\varphi}^s \\
(\Rightarrow_0) & = (\Rightarrow_{sf} \Rightarrow_s^\nf) \\
(\Rightarrow_1) & = (\Rightarrow_s) \\
(\Rightarrow_2) & = (\Rightarrow_{cf}).
\end{align*}
The system $(A',\Rightarrow_0)$ is confluent by the assumption.
The system $(A,\Rightarrow_1)$ is confluent and strongly normalizing by \rlem{subst-red}.
Thus we just need to show that every pair of terms $t,s \in \Term_{T,\varphi}^c$ such that $t \Rightarrow_{cf} s$ is joinable under $\Rightarrow_s^\nf (\Rightarrow_{sf} \Rightarrow_s^\nf)^*$.
If $t \Rightarrow_s s$, then this is obvious, so we may assume that $t \Rightarrow_{sf} s$.

Since $t \Rightarrow_{sf} s$, there exist terms $a$, $b$, and $c$ and a substitution $\rho$ such that $(a,b) \in R_T^{sf}$, $t = U(c[a[\rho]/x])$, and $s = U(\nf^t(c[b[\rho]/x]))$.
Since $t \in \Term_{T,\varphi}^c$, the term $c$ and the substitution $\rho$ do not contain occurrences of function symbols $\ft$ and $\ty$.
Thus $s = U(c[\nf^t(b)[\rho]/x])$.
Since $U$ commutes with subsitution, $t = U(c)[U(a)[U(\rho)]/x]$ and $s = U(c)[U(\nf^t(b))[U(\rho)]/x]$.

Let $c'$ be the $\Rightarrow_s$-normal form of $U(c)$.
Note that $U(c)$ contains at most one occurrence of $x$, but $c'$ may contain several such occurrences.
Let us show that $\Rightarrow_s$-redexes in the term $c'[U(a)[U(\rho)]/x]$ that do not belong to $U(a)$ do not overlap.
To do this, note that if $c \Rightarrow_s^* c'$ and $c$ contains at most one occurrence of a variable $x$, then, for every subterm of $c'$ of the form $\subst_{p,n,k}(a, a_1, \ldots a_k)$, if $x \in FV(a)$, then $x \notin FV(a_1, \ldots a_k)$.
Indeed, this property holds for $c$ since it contains at most one occurrence of $x$ and it is easy to show that if it holds for $c$ and $c \Rightarrow_s c'$, then it also holds for $c'$.
Now, a $\Rightarrow_s$-redex in the term $c'[U(a)[U(\rho)]/x]$ either belongs to $U(a)$ or it comes from a subterm of $c'$ of the form $\subst_{p,n,k}(x, a_1, \ldots a_k)$ and the fact that we just proved implies that $a_1, \ldots a_k$ do not contain such subterms.

Since $\Rightarrow_s$-redexes in the term $c'[U(a)[U(\rho)]/x]$ do not overlap, we may consider them one at a time.
Thus we just need to prove that every pair of terms of the form $\subst_{p,n,k}(U(a)[U(\rho)], a_1, \ldots a_k)$ and $\subst_{p,n,k}(U(\nf^t(b))[U(\rho)], a_1, \ldots a_k)$ is joinable under $\Rightarrow_s^\nf (\Rightarrow_{sf} \Rightarrow_s^\nf)^*$.
We may assume that if $\rho(x)$ is defined, then $x$ is not free in terms $a_1$, \ldots $a_k$.
Then
\[ \subst_{p,n,k}(U(a)[U(\rho)], a_1, \ldots a_k) = \subst_{p,n,k}(U(a), a_1, \ldots a_k)[U(\rho)] \]
and
\[ \subst_{p,n,k}(U(\nf^t(b))[U(\rho)], a_1, \ldots a_k) = \subst_{p,n,k}(U(\nf^t(b)), a_1, \ldots a_k)[U(\rho)]. \]

By \rlem{lift}, terms $\subst_{p,n,k}(U(a), a_1, \ldots a_k)[U(\rho)]$ and $L^m(U(a))[\rho'][U(\rho)]$ and terms $\subst_{p,n,k}(U(\nf^t(b)), a_1, \ldots a_k)[U(\rho)]$ and $L^m(U(\nf^t(b)))[\rho'][U(\rho)]$ are joinable under $\Rightarrow_s$,
where $\rho'$ is the substitution defined in this lemma.
Since $\subst$-free rules are stable, there is a $\subst$-free rule $(a',b')$ such that $U(a') = L^m(U(a))$ and $U(\nf^t(b')) = L^m(U(\nf^t(b)))$.
Let $\rho''$ be the substitution consisting of $\Rightarrow_s$-normal forms of $\rho'[U(\rho)]$.
Since $\subst$-free rules are well-behaved, terms $U(a')[\rho'']$ and $U(\nf^t(b'))[\rho'']$ are joinable under $\Rightarrow_s^\nf (\Rightarrow_{sf} \Rightarrow_s^\nf)^*$.
\end{proof}

% 9. Попытка доказать, что можно работать только с нормализованными формулами. Безуспешная.

\subsection{Morita equivalences between confluent theories}

The first condition of \rlem{eq-char-fib} is usually easy to check.
In this subsection we give several lemmas that will be useful for proving the second condition of this lemma.
Let $T_I = \IdT_- + I + p_I + \wUA$, where $\IdT_-$ is the theory with identity types in which computational rule for $J$ is replaced with a propositional equality,
$\wUA$ is the weak univalence axiom, and be the theory with the following constructions:
\begin{center}
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash I\ \type$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \leftI : I$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \rightI : I$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash i : I$}
\UnaryInfC{$\Gamma \vdash p_I(i) : \Id(\leftI,i)$}
\DisplayProof
\end{center}
All the theories with the interval type that we considered before are theories under $T_I$.
% If $e_{p_j}(t) = A_j$, then we can define a term $\coe(H,t)$ such that $e_{p_j}(\coe(H,t)) = A_j'$.

\begin{lem}
Let $(\varphi, V)$ be a pair in $P_M$, where $\varphi = \bigwedge_{1 \leq i \leq n} e_{p_i}(x_i) = A_i$.
Let $A_j'$ be a term homotopic to $A_j$ for some $1 \leq j \leq n$.
Let $T_1$ be a theory under $T_I$ and let $f : T_1 \to T_2$ be a map with the weak lifting property with respect to $(\varphi', V \setminus \{ x_j \} \cup \{ x_j' \})$, where $\varphi'$ is the following formula:
\[ \bigwedge_{1 \leq i < j} e_{p_i}(x_i) = A_i \land e_{p_j}(x_j') = A_j' \land \bigwedge_{j < i \leq n} e_{p_i}(x_i) = A_i[\coe(H^{-1},x_j')/x_j]. \]
Then $f$ also has this property with respect to $(\varphi,V)$.
\end{lem}
\begin{proof}
Let $H$ be a homotopy between $A_j$ and $A_j'$.
Let $B$ and $b$ be terms such that $\varphi \sststile{T_1}{V} B\!\downarrow$ and $f(\varphi) \sststile{T_2}{V} e_p(b) = f(B)$.
Then $\varphi' \sststile{T_1}{V'} B'\!\downarrow$ and $f(\varphi') \sststile{T_2}{V'} e_p(b') = f(B')\!\downarrow$, where $B' = B[\coe(H^{-1},x_j')/x_j]$ and $b' = b[\coe(f(H)^{-1},x_j')/x_j]$.
By assumption, there exist terms $c'$ and $h$ such that $\varphi' \sststile{T_1}{V'} e_p(c') = B'$ and $h$ is a relative homotopy between $f(c')$ and $b'$.
Then $\varphi'' \sststile{T_1}{V'} e_p(c'') = B''$, where $\varphi''$ is the following formula:
\[ \bigwedge_{1 \leq i \leq j} e_{p_i}(x_i) = A_i \land \bigwedge_{j < i \leq n} e_{p_i}(x_i) = A_i[\coe(H^{-1},\coe(H,x_j))/x_j], \]
$c'' = c'[\coe(H,x_j)/x_j']$, and $B'' = B[\coe(H^{-1},\coe(H,x_j))/x_j]$.
\end{proof}

% 10. Доказательство, что в некоторых локалзациях есть индексированные произведения.

\subsection{Products and exponential objects}

In this subsection, we will prove that certain localizations of the injective structure on $\scat{C}^\scat{J}$ are Cartesian closed and locally small and have products.

The notion of a Cartesian model category is a special case of a monoidal model category \cite[Definition~A.3.1.2]{lurie-topos}, \cite[Definition~4.2.6]{hovey}, \cite[Subsection~2.5]{segal-spaces}.
We will need only a weak version of this notion:

\begin{defn}
A model category is \emph{semi-Cartesian} if, for every pair of cofibrations $f : A \to B$ and $g : C \to D$,
the canonical map $f \square g : A \times D \amalg_{A \times C} B \times C \to B \times D$ is a cofibration.
A model category is \emph{semi-Cartesian closed} if it is semi-Cartesian and Cartesian closed as a category.
\end{defn}

\begin{remark}[cartesian]
A model category is \emph{Cartesian (resp., Cartesian closed)} if it is semi-Cartesian (resp., semi-Cartesian closed), the terminal object is cofibrant, and $f \square g$ is a trivial cofibration whenever $f$ is a cofibration and $g$ is a trivial cofibration.
\end{remark}

\begin{example}
If a model category $\scat{C}$ is semi-Cartesian (resp., Cartesian, semi-Cartesian closed, Cartesian closed), then $\scat{C}^\scat{J}$ with the injective structure is also semi-Cartesian (resp., Cartesian, semi-Cartesian closed, Cartesian closed).
\end{example}

The main feature of semi-Cartesian closed model categories is that they have nice cosimplicial resolutions of objects and maps \cite[Definition~16.1.2, Definition~16.1.20]{hirschhorn}.
Let $\Delta$ be a fibrant cofibrant replacement of the terminal object of $\scat{C}^\Delta$.
That is, $\Delta$ is a functor $\Delta \to \scat{C}$ such that $\Delta^n \to 1$ is a trivial fibration for all $n$ and $\partial \Delta^n \to \Delta^n$ is a cofibration in $\scat{C}$.
Then $n \mapsto Q(X) \times \Delta^n$ is a cosimplicial resolution of $X$, where $Q(X)$ is any cofibrant replacement of $X$.
Let $f : X \to Y$ be a map and let $Q(X)$ be a cofibrant replacement of $X$.
Factor the map $Q(X) \to X \xrightarrow{f} Y$ into a cofibration $Q(f) : Q(X) \to Q(Y)$ followed by a weak equivalence $Q(Y) \to Y$.
Then $n \mapsto Q(X) \times \Delta^n \to Q(Y) \times \Delta^n$ is a cosimplicial resolution of $f$.

Let $D : \scat{C} \to \scat{C}^\scat{J}$ be the diagonal functor.
We will say that a functor $F \in \scat{C}^\scat{J}$ is \emph{anticonstant} if, for every functor $R : \scat{C}^\scat{J}$ and every constant functor $D(X) \scat{C}^\scat{J}$,
every map $F \times R \to D(X)$ factors through the projection $\pi_2 : F \times R \to R$.

\begin{lem}[anticonstant-coproduct]
If the category $\fs{el}(F)$ of elements of a functor $F : \scat{J} \to \Set$ is non-empty, then the functor $F(-) \cdot 1 : \scat{J} \to \scat{C}$ is anticonstant if and only if $\fs{el}(F)$ is connected.
\end{lem}
\begin{proof}
By the universal property of coproducts, there is a bijection between the set of maps $p : F(-) \cdot 1 \to D(X)$ and the set of collections of maps $\{ p_{j,a} : 1 \to X \}_{j \in \scat{J}, a \in F(j)}$ such that,
for every map $f : j \to j'$, it is true that $p_{j,a} = p_{j',F(f)(a)}$.
On the other hand, the set of such collections is the set of maps between constant functors on $1$ and $X$ in the category $\scat{C}^{\fs{el}(F)}$.
A map $p : F(-) \cdot 1 \to D(X)$ factors through a map $c : R \to D(X)$ if and only if $p_{j,a} = c$ for all $j$ and $a$.
Since $\fs{el}(F)$ is non-empty, a map of the form $c : 1 \to X$ exists.
The assertion follows from the fact that every map between constant functors $D(Y), D(X) : \scat{I} \to \scat{C}$ equals to $D(c)$ for some fixed $c : Y \to X$ if and only if the category $\scat{I}$ is connected.
\end{proof}

\begin{example}
If $F : \scat{J} \to \Set$ is a representable functor on an object $j \in \scat{J}$, then the functor $F(-) \cdot 1$ is anticonstant.
This follows from \rlem{anticonstant-coproduct} since the category of elements of $F$ is equivalent to the category $j/\scat{J}$ which is non-empty and connected since it has an initial object.
\end{example}

\begin{example}
If $F$ is a non-empty simplicial set, then $F(-) \cdot 1 : \Delta^\fs{op} \to \scat{C}$ is anticonstant if and only if $F$ is connected as a simplicial set.
This follows from \rlem{anticonstant-coproduct} and the fact that a simplicial set is connected if and only if its category of elements is connected.
\end{example}

\begin{lem}[anticonstant-factor]
Let $\scat{C}$ be a Cartesian closed category and let $F : \scat{J} \to \scat{C}$ be an anticonstant functor.
Then every map of the form $F \times D(X) \to D(Y)$ factors as the projection $\pi_2 : F \times D(X) \to D(X)$ followed by a map $D(g)$ for some $g : X \to Y$.
\end{lem}
\begin{proof}
First, it is easy to see that the diagonal functor $D$ preserves exponential objects.
Then a map $f : F \times D(X) \to D(Y)$ corresponds to a map $F \to D(Y^X)$.
Since $F$ is anticonstant, the latter map factors through a map $D(c)$ for some $c : 1 \to Y^X$.
The map $c$ corresponds to a map $g : X \to Y$ such that $D(g) \circ \pi_2 = f$.
\end{proof}

\begin{prop}[localized-products]
Let $\scat{C}$ be a right proper semi-Cartesian closed combinatorial type-theoretic model category in which all objects are cofibrant.
Let $\scat{J}$ be a small category and let $S$ be a class of cofibrations of $\scat{C}^\scat{J}$ such that the codomains of maps in $S$ are anticonstant.
Let $\overline{S}$ be the class of maps of the form $f \square D(i)$, where $f \in S$ and $i$ is a cofibration of $\scat{C}$.
Then $\Lambda(\overline{S}) = \overline{S}$ and $D^*(L_{\overline{S}}(\scat{C}^\scat{J}))$ has dependent products.
Moreover, products in $D^*(L_{\overline{S}}(\scat{C}^\scat{J}))$ are computed as products in $D^*(\scat{C}^\scat{J})$.
\end{prop}
\begin{proof}
The functor $D : \scat{C} \to \scat{C}^\scat{J}$ satisfies most of the conditions of \rprop{products} as discussed in \rexample{products}.
We just need to prove that $\Pi_g$ preserves fibrations for all $D$-fibrations $g$.
This is true if and only if (generating) trivial cofibrations are stable under pullbacks along $D$-fibrations.
Maps that are trivial cofibrations in the injective model structure on $\scat{C}^\scat{J}$ are stable under pullbacks since $\scat{C}$ is right proper and $D$-fibrations are objectwise fibrations.
Thus, we just need to prove that maps in $\Lambda(\overline{S})$ are stable under pullbacks along $D$-fibraions.
We will use the cosimplicial resolution of the form $X \times D(\Delta^n) \to Y \times D(\Delta^n)$,
where $\Delta^n$ is any fibrant cosimplicial resolution of the terminal object in $\scat{C}$.
This is a cosimplicial resolution since $D$ preserves colimits, $\scat{C}$ is semi-Cartesian closed, and $\pi_1 : X \times D(\Delta^n) \to X$ is a weak equivalence.
The last statement is true since, for every $j \in J$, the map $\pi_1 : X_j \times \Delta^n \to X_j$ is a trivial fibration.

The class $\Lambda(\overline{S})$ consists of the maps $(f \square D(i)) \square D(j)$, where $f \in S$, $i$ is a cofibration of $\scat{C}$ and $j : \partial \Delta^n \to \Delta^n$.
Since $\square$ is associative and $D$ preserves $\square$, the map $(f \square D(i)) \square D(j)$ is isomorphic to the map $f \square D(i \square j)$.
Since $\scat{C}$ is semi-Cartesian, $i \square j$ is a cofibration, so $f \square D(i \square j)$ belongs to $\overline{S}$.
Thus, $\Lambda(\overline{S}) = \overline{S}$.

Consider the following diagram:
\[ \xymatrix{ W \ar[r] \ar[d] \pb & X \times D(R) \amalg_{X \times D(P)} Y \times D(P) \ar[d] \\
              V \ar[r] \ar[d] \pb & Y \times D(R) \ar[d] \\
              D(B) \ar[r]_{D(p)} & D(A)
            } \]
where $p : B \twoheadrightarrow A$ is a fibration, $f : X \to Y$ is a map in $S$, and $i : P \to R$ is a cofibration of $\scat{C}$.
We need to prove that $W \to V$ belongs to $\overline{S}$.
\Rlem{anticonstant-factor} implies that the map $Y \times D(R) \to D(A)$ factor as the second projection followed by a map of the form $D(R) \to D(A)$ for some map $c : R \to A$.
Let us denote by $T$ the pullback of $p$ and $c$.
Then $V \simeq Y \times D(T)$.

Since $D$-fibrations are exponentiable and exponentiable maps are stable under pullbacks, pullbacks along the map $Y \times D(T) \to Y \times D(R)$ preserve colimits.
Thus, $W \to V$ is the following map:
\[ (X \times D(T)) \amalg_{(X \times D(T \times_R P))} (Y \times D(T \times_R P)) \to Y \times D(T). \]
That is, this map is $f \square D(j)$, where $j$ is the map $T \times_R P \to T$.
Since $i$ is a cofibration and cofibrations are stable under pullback, $j$ is also a cofibration.
Thus, $f \square D(j)$ belongs to $\overline{S}$.
\end{proof}

\begin{cor}
Let $\scat{J}$ be a small category and let $S$ be a class of cofibrations of $\sSet^\scat{J}$ such that the codomains of maps in $S$ are anticonstant.
Then $D^*(L_S(\sSet^\scat{J}))$ has dependent products which are computed as products in $D^*(\sSet^\scat{J})$.
\end{cor}
\begin{proof}
The category of simplicial sets satisfies the conditions of \rprop{localized-products}.
Thus, we just need to prove that $\Icof[\Lambda(S)] = \Icof[\overline{S}]$.
The class $\Lambda(S)$ consists of maps of the form $f \square D(i)$, where $f \in S$ and $i : \partial \Delta^n \to \Delta^n$.
Thus, $\Lambda(S) \subseteq \overline{S}$ and $\overline{S} \subseteq \Icof[\Lambda(S)]$ since maps $\partial \Delta^n \to \Delta^n$ generate all cofibrations.
\end{proof}

% 11. Кусок про системы факторизаций в контекстуально индексированных контекстуальных категориях.

\section{Factorization systems}

In this section, we describe several examples of factorization systems.
A factorization system consists of a class of dependent types called fibrations closed under identity types and a map from types to fibrations satisfying a universal property.

\begin{lem}
Let $(\scat{C},\Fib)$ be a category with fibrations.
Let $\Fib' \subseteq \Fib$ be a class of fibrations such that every map factors into a map that has the left lifting property with respect to $\Fib'$ followed by a map in $\Fib'$.
Then $\scat{C}_!$ has a factorization system with $\Fib'$ as a class of fibrations.
\end{lem}
\begin{proof}
% TODO
\end{proof}

A large class of factorization systems can be defined as the localization at a finite set of families of maps.
A family of maps is a base type $I$ together with a map indexed by it:
\[ i : I \vdash f_i : \Hom(U_i,V_i). \]

Every class of dependent types $\Fib$ gives rise to a class of maps $\Fib'$.
A map belongs to $\Fib'$ if its fibers belong to $\Fib$.
Conversely, for every class of maps $\Fib'$, we can define a class of dependent types $\Fib$.
A type $\Delta.A$ belongs to $\Fib$ if the projection map $\Sigma(\Delta,A) \to \Sigma(\Delta)$ belongs to $\Fib'$.
These constructions are mutually inverse.

Let $\scat{C}$ be a contextually indexed contextual category.
Let $S$ be a finite set of families of maps of $\scat{C}$.
We will say that a map $p : \Hom(X,Y)$ is \emph{right orthogonal} to $S$ if the following square is a pullback for every $f_i \in S$:
\[ \xymatrix{ \Hom(V_i,X) \ar[r] \ar[d] & \Hom(U_i,X) \ar[d] \\
              \Hom(V_i,Y) \ar[r]        & \Hom(U_i,Y)
            } \]
Equivalently, $p$ is right orthogonal to $S$ if the type of lifts in the following square is contractible for every $f_i \in S$ and all maps $u : \Hom(U_i,X)$ and $v : \Hom(V_i,Y)$:
\[ \xymatrix{ U_i \ar[r]^u \ar[d]_{f_i}     & X \ar[d]^p \\
              V_i \ar[r]_v \ar@{-->}[ur]    & Y
            } \]

Now, let $S$ be a finite set of families of maps of $\scat{C}$ such that the domains and codomains of maps in $S$ are exponentiable.
We will say that a map $p : \Hom(X,Y)$ is \emph{internally right orthogonal} to $S$ if the following square is a pullback for every $f_i \in S$:
\[ \xymatrix{ (V_i \to X) \ar[r] \ar[d] & (U_i \to X) \ar[d] \\
              (V_i \to Y) \ar[r]        & (U_i \to Y)
            } \]
If $\scat{C}$ has a terminal type $1$ and $p$ is internally right orthogonal to $S$, then it is also right orthogonal to $S$.
To prove this, it is enough to apply $\Hom(1,-)$ to the pullback square above.
Since $\Hom(1,-)$ preserves pullbacks and maps $A \to B$ to $\Hom(A,B)$, we see that the required square is a pullback.

We will say that a dependent type is \emph{(internally) right orthogonal} to $S$ if the corresponding map is.

\begin{lem}
The class of types (internally) right orthogonal to a set $S$ is closed under unit types, $\Sigma$-types, identity types, and substitution.
\end{lem}
\begin{proof}
Any unit type $A$ is $S$-local since types $V_i \to A$ and $U_i \to A$ are contractible.
It is easy to see that $S$-local types are closed under substitution.
Indeed, if $\sigma : E \to \Delta$ is a substitution and $e$ is a proof that $f_i^* : (V_i \to A) \to (U_i \to A)$ is an equivalence, then $e[\sigma]$ is a proof that $f_i^* : (V_i \to A[\sigma]) \to (U_i \to A[\sigma])$ is an equivalence.

Let $\Delta.A$ and $\Delta, x : A. B$ be $S$-local types.
Let us prove that $\Sigma_{x : A} B$ is also $S$-local.
\end{proof}

% 12. Модельная структура на обогащенных категориях.

Let $(\cat{V},\otimes,e)$ be a monoidal model category.
Then we will denote by $[0]_\cat{V}$ the $\cat{V}$-enriched category that has a single object $X$ such that $\Hom_{[0]_\cat{V}}(X,X) = e$.
If $V$ is an object of $\cat{V}$, we will denote by $[1]_V$ the $\cat{V}$-enriched category with two objects $X$ and $Y$ and the following maps:
\begin{align*}
\Hom_{[1]_V}(X,X) & = e \\
\Hom_{[1]_V}(Y,Y) & = e \\
\Hom_{[1]_V}(X,Y) & = V \\
\Hom_{[1]_V}(Y,X) & = 0
\end{align*}

We will say $\cat{V}$ is \emph{good} if the category of $\cat{V}$-enriched categories is a model category with the following classes of cofibrations and weak equivalences:
\begin{itemize}
\item Cofibrations are generated by the class consisting of the map $0 \to [0]_\cat{V}$ and maps $[1]_i : [1]_U \to [1]_V$ for every cofibration $i : U \to V$.
\item A map $f : C \to D$ is a weak equivalence if and only if, for all objects $X$ and $Y$ of $C$, the map $f : \Hom_C(X,Y) \to \Hom_D(f(X),f(Y)$ is a weak equivalence
and, for every object $Z$ of $D$, there is an object $Z'$ of $C$ such that $f(Z')$ is isomorphic to $Z$ in the homotopy category of $D$.
\end{itemize}

Sufficient conditions for $\cat{V}$ to be good are given in \cite[Proposition~A.3.2.4]{lurie-topos}.
Categories of simplicial and cubical sets are both good.
A \emph{simplicial (resp., cubical) category} is a category enriched in simplicial (resp., cubical) sets.
The categories of simplicial and cubical sets will be denoted by $\sSet$ and $\cSet$, respectively.
The categories of simplicial and cubical categories will be denoted by $\sCat$ and $\cCat$, respectively.

An \emph{interval object} in $\cat{V}$ is an object $I$ together with a cofibration $e \amalg e \to I$ and a weak equivalence $I \to e$ such that their composite equals $[\id_e,\id_e]$.
Categories of simplicial and cubical sets both have an interval object ($\Delta^1$ and $\square^1$, respectively).
For every monoidal category $\cat{V}$ with an interval object $I$, there is a unique monoidal functor $F_I : \cSet \to \cat{V}$ sending the interval object $\square^1$ to $I$ and commuting with colimits.
If $\cat{V}$ is a monoidal model category, this functor is a left Quillen functor.
In particular, there is a monoidal left Quillen functor $F_{\Delta^1} : \cSet \to \sSet$ sending $\square^1$ to $\Delta^1$.
This functor is a Quillen equivalence. % TODO: Find a reference for this.
It follows that $F_{\Delta^1}$ is also a Quillen equivalence \cite[Remark~A.3.2.6]{lurie-topos}.