homotopy-model.tex

\documentclass{amsart}

\usepackage[english,russian]{babel}
\usepackage[utf8]{inputenc}
\usepackage{amssymb}
\usepackage[all]{xy}
\usepackage{verbatim}
\usepackage{ifthen}
\usepackage{xargs}
\usepackage{bussproofs}
\usepackage{type1ec}
\usepackage{stmaryrd}

\providecommand\WarningsAreErrors{false}
\ifthenelse{\equal{\WarningsAreErrors}{true}}{\renewcommand{\GenericWarning}[2]{\GenericError{#1}{#2}{}{This warning has been turned into a fatal error.}}}{}

\newcommand{\newref}[4][]{
\ifthenelse{\equal{#1}{}}{\newtheorem{h#2}[hthm]{#4}}{\newtheorem{h#2}{#4}[#1]}
\expandafter\newcommand\csname r#2\endcsname[1]{\ref{#2:##1}}
\newenvironmentx{#2}[2][1=,2=]{
\ifthenelse{\equal{##2}{}}{\begin{h#2}}{\begin{h#2}[##2]}
\ifthenelse{\equal{##1}{}}{}{\label{#2:##1}}
}{\end{h#2}}
}

\newref[section]{thm}{Theorem}{Theorem}
\newref{lem}{Lemma}{Lemma}
\newref{prop}{Proposition}{Proposition}
\newref{cor}{Corollary}{Corollary}

\theoremstyle{definition}
\newref{defn}{Definition}{Definition}
\newref{example}{Example}{Example}

\theoremstyle{remark}
\newref{remark}{Remark}{Remark}

\newcommand{\red}{\Rightarrow}
\newcommand{\deq}{\Leftrightarrow}
\renewcommand{\ll}{\llbracket}
\newcommand{\rr}{\rrbracket}
\newcommand{\cat}[1]{\mathbf{#1}}
\renewcommand{\C}{\cat{C}}

\newcommand{\pb}[1][dr]{\save*!/#1-1.2pc/#1:(-1,1)@^{|-}\restore}
\newcommand{\po}[1][dr]{\save*!/#1+1.2pc/#1:(1,-1)@^{|-}\restore}

\numberwithin{figure}{section}

\begin{document}

\title{An interpretation of homotopy type theory}

\author{Valery Isaev}

% \begin{abstract}
% Abstract
% \end{abstract}

\maketitle

\section{Правила вывода}

\begin{table}

\medskip
\begin{center}
\AxiomC{}
\UnaryInfC{$\vdash$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash A$}
\RightLabel{, $x \notin \Gamma$}
\UnaryInfC{$\Gamma, x : A \vdash$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash A$}
\RightLabel{, $x \notin \Gamma$}
\UnaryInfC{$\Gamma, x : A \vdash x \Uparrow A$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash x \Uparrow A$}
\AxiomC{$\Gamma \vdash B$}
\RightLabel{, $y \notin \Gamma$}
\BinaryInfC{$\Gamma, y : B \vdash x \Uparrow A$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash a \Uparrow A_1$}
\AxiomC{$\Gamma \vdash A_2$}
\RightLabel{, $A_1 \deq A_2$}
\BinaryInfC{$\Gamma \vdash a \Downarrow A_2$}
\DisplayProof
\end{center}

\medskip
\caption{Правила вывода.}
\label{table:inf-rules}
\end{table}

\newpage

\section{Интерпретация}

\subsection{Контекстуальные категории}

Мы будем интерпретировать теорию в контекстуальной категории.
Такая категория состоит из следующего набора данных:
\begin{itemize}
\item Категория $\C$.
\item Градуировка объектов $Ob(\C) = \coprod_{n \in \mathbb{N}} Ob_n(\C)$.
\item Морфизмы $ft : Ob_{n+1}(\C) \to Ob_n(\C)$.
\item Для каждого $A \in Ob_{n+1}(\C)$ морфизм $\pi_A : A \to ft(A)$.
\item Для каждого $A \in Ob_{n+1}(\C)$ и $f : \Delta \to ft(A)$ объект $f^*(A)$ и морфизм $q(f, A) : f^*(A) \to A$.
\end{itemize}
удовлетворяющих следующим условиям:
\begin{itemize}
\item $Ob_0(\C)$ состоит из единственного объекта, и этот объект терминальный. Мы будем обозначать его 1.
\item Для каждого $A \in Ob_{n+1}(\C)$ и $f : \Delta \to ft(A)$ верно, что $ft(f^* A) = \Delta$ и следующий квадрат декартов:
\[ \xymatrix{ f^*(A) \ar[d]_{\pi_{f^*(A)}} \ar[r]^-{q(f, A)} & A \ar[d]^{\pi_A} \\
              \Delta \ar[r]_f & ft(A)
            } \]
\item Для каждого $A \in Ob_{n+1}(\C)$ верно, что $id^*(ft(A)) = A$, и $q(id_{ft(A), A}) = id_A$.
\item Для каждого $A \in Ob_{n+1}(\C)$, $f : \Delta \to ft(A)$ и $g : E \to \Delta$ верно, что $(f \circ g)^*(A) = g^*(f^*(A))$, и $q(f \circ g, A) = q(f, A) \circ q(g, f^*(A))$.
\end{itemize}

Если $\Gamma \in Ob_m(\C)$ и $A \in Ob_{1+m}(\C)$, то мы будем писать $\Gamma \models A$, если $ft(A) = \Gamma$.
Если $A \in Ob_{n+m}(\C)$, то мы будем обозначать $\pi^n_A : A \to ft^n(A)$ морфизм $\pi_{ft^{n-1}(A)} \circ \ldots \circ \pi_A$.
Если $\Gamma \in Ob_m(\C)$, $A \in Ob_{n+m}(\C)$ и $a \in Hom(\C)$, то мы будем писать $\Gamma \models a : A$, если $ft^n(A) = \Gamma$, и $a : \Gamma \to A$ - сечение $\pi^n_A$.

Если $f : \Delta \to \Gamma$ - некоторый морфизм, $ft(A) = \Gamma$ и $\Gamma \models a : A$, то мы будем обозначать $f^*(a)$ следующее сечение:
\[ \xymatrix{ \Delta \ar[r]^f \ar[d]_{f^*(a)} \pb                & \Gamma \ar[d]^a \\
              f^*(A) \ar[r]_-{q(f, A)} \ar[d]_{\pi_{f^*(A)}} \pb & A \ar[d]^{\pi_A} \\
              \Delta \ar[r]_f                                    & \Gamma
                 }\]

Мы предполагаем, что в категории определены различные конструкции, необходимые для интерпретации правил теории.
Часть этих конструкций ($\Sigma$-типы, $\Pi$-типы, и т.д.) мы опишем позже.
Сейчас мы опишем часть, необходимую для интерпретации гомотопий и расслоений.

Категория должна содержать интервальный тип $I' \in Ob_1(\C)$ вместе с парой морфизмов $i_0, i_1 : 1 \to I'$.
Если $!_\Gamma : \Gamma \to 1$, то $!_\Gamma^*(I')$ является декартовым произведением $\Gamma$ и $I'$, поэтому мы будем обозначать этот объект $\Gamma \times I'$.
Проекцию $\pi_{!_\Gamma^*(I')} : !_\Gamma^*(I') \to \Gamma$ мы будем обозначать как $\pi_1 : \Gamma \times I' \to \Gamma$.
Если $f : \Delta \to \Gamma$, то морфизм $q(f, !_\Gamma^*(I')) : \Delta \times I' \to \Gamma \times I'$ мы будем обозначать как $f \times I'$.
Сечения $!_\Gamma^*(i_0), !_\Gamma^*(i_1) : \Gamma \to \Gamma \times I'$ мы будем обозначать просто $i_0$ и $i_1$ соответственно.

\begin{comment}
Также в категории должен быть выбран насыщенный класс морфизмов, которые мы называем \emph{тривиальными корасслоениями}.
Морфизмы, которые имеют правое свойство поднятия по отношению к тривиальным корасслоениям, мы называем \emph{расслоениями}.
Мы требуем, чтобы для любого $\Gamma \models A$ морфизмы $\pi_A : \Gamma.A \to \Gamma$ являлись расслоениями.

Тривиальные корасслоения должны содержать морфизмы вида $i_0 : \Gamma \to \Gamma \times I'$ и
    $(\Gamma \times I' \amalg \Gamma \times I') \amalg_{\Gamma \amalg \Gamma} \Gamma \times I' \to \Gamma \times I' \times I'$, которые определяются как в следующей диаграмме:
\[ \xymatrix@-1pc{ \Gamma \amalg \Gamma \ar[rr]^{i_0 \amalg i_0} \ar[dd]_{[i_0, i_1]} & & \Gamma \times I' \amalg \Gamma \times I' \ar[dd] \ar[rddd]^{[i_0, i_1]} \\ \\
\Gamma \times I' \ar[rr] \ar[rrrd]_{i_0 \times id_{I'}} & & \po (\Gamma \times I' \amalg \Gamma \times I') \amalg_{\Gamma \amalg \Gamma} \Gamma \times I' \ar@{-->}[rd] \\
                                                                       & & & \Gamma \times I' \times I'
                 } \]
\end{comment}

Также нам потребуются следующие конструкции.
Для любых объектов $\Gamma, A$ таких, что $\Gamma \times I' \models A$ и для любого $a$ такого, что $\Gamma \models a : i_0^*(A)$ должно существовать сечение $\Gamma \times I' \models ext(A, a) : A$ такое, что $i_0^*(ext(A, a)) = a$.
Более того, мы требуем, чтобы для любого морфизма $f : \Delta \to \Gamma$ было верно, что $(f \times I')^*(ext(A, a)) = ext((f \times I')^*(A), f^*(a))$.
Для этого достаточно проверить, что следующий квадрат коммутирует:
\[ \xymatrix{ \Delta \times I' \ar[rr]^{f \times I'} \ar[d]_{ext((f \times I')^*(A), f^*(a))} & & \Gamma \times I' \ar[d]^{ext(A,a)} \\
              (f \times I')^*(A) \ar[rr]_-{q(f \times I', A)}                                 & & A
            } \]

Если $\Gamma \times I' \models H$, то $\Gamma \times I' \models Inv(H)$, $i_0^*(Inv(H)) = i_1^*(H)$, и $i_1^*(Inv(H)) = i_0^*(H)$.
Если $f : \Delta \to \Gamma$, то $(f \times I')^*(Inv(H)) = Inv((f \times I')^*(H))$.

Если $\Gamma \times I' \models H_1$, $\Gamma \times I' \models H_2$ и $i_1^*(H_1) = i_0^*(H_2)$, то $\Gamma \times I' \models Con(H_1, H_2)$, $i_0^*(Con(H_1, H_2)) = i_0^*(H_1)$, и $i_1^*(Con(H_1, H_2)) = i_1^*(H_2)$.
Если $f : \Delta \to \Gamma$, то $(f \times I')^*(Con(H_1, H_2)) = Con((f \times I')^*(H_1), (f \times I')^*(H_2))$.
Для любых $\Gamma \times I' \models H$ верно, что $Con(\pi_1^* i_0^*(H), H) = H$, и $Con(H, Inv(H)) = \pi_1^* i_0^*(H)$.

\subsection{Определение интерпретации}

Сначала определим несколько классов.
\[ Type = \{ \Gamma \models A\ |\ \Gamma, A \text{ такие, что } \Gamma \models A \} \]
\[ Sec = \{ \Gamma \models a : A\ |\ \Gamma, a, A \text{ такие, что } \Gamma \models a : A \} \]

Пусть $\Gamma \in Ob(\C)$.
Тогда определим класс $Seq_\Gamma$ как класс последовательностей $A_1, \ldots A_{2 n + 1}$ объектов $\C$ таких, что для всех $1 \leq i \leq 2 n + 1$ верно, что $ft(A_i) = \Gamma \times I'$ если $i$ - четно, и $ft(A_i) = \Gamma$ иначе, и
для любого $1 \leq i \leq n$ верно, что $i_0^*(A_{2 i}) = A_{2 i - 1}$, и $i_1^*(A_{2 i}) = A_{2 i + 1}$.
\[ Seq = \{ \Gamma \times I' \models S\ |\ \Gamma \in Ob(\C), S \in Seq_\Gamma \} \]
Если $S = (A_1, \ldots A_{2 n + 1}) \in Seq_\Gamma$, $\Gamma \times I' \models A$ и $i_1^*(A) = A_1$, то $(i_0^*(A), A, A_1, \ldots A_n) \in Seq_\Gamma$.
Мы будем обозначать эту последовательность $A * S$.

Пусть $S = (A_1, \ldots A_{2 n + 1}) \in Seq_\Gamma$ и $\rho : \Delta \to \Gamma$.
Тогда мы определим $(\rho \times I')^*(S) \in Seq_\Delta$ как последовательность $(\rho^*(A_1), (\rho \times I')^*(A_2), \rho^*(A_3), \ldots \rho^*(A_{2 n + 1}))$.

Интерпретация теории состоит из следующих отношений:
\begin{itemize}
\item Отношение $\ll - \rr = -$ на классе $Ctx \times Ob(\C)$, где $Ctx$ - множество контекстов.
\item Отношение $\ll - \vdash - \rr = -$ на классе $Ctx \times Term \times Type$, где $Term$ - множество термов.
\item Отношение $\ll - \vdash - \Uparrow - \rr = -$ на классе $Ctx \times Term \times Term \times Sec$.
\item Отношение $\ll - \vdash - \Downarrow - \rr = -$ на классе $Ctx \times Term \times Term \times Sec$.
\item Отношение $\ll - \vdash - \red - \rr = -$ на классе $Ctx \times Term \times Term \times Type$.
\item Отношение $\ll - \vdash - \red^* - \rr = -$ на классе $Ctx \times Term \times Term \times Seq$.
\item Отношение $\ll - \vdash - \red - \Downarrow - \rr = -$ на классе $Ctx \times Term \times Term \times Term \times Sec$.
\end{itemize}

Интерпретация контекстов:

\medskip
\begin{center}
\AxiomC{}
\UnaryInfC{$\ll\ \rr = 1$}
\DisplayProof
\quad
\AxiomC{$\ll \Gamma \rr = \Gamma'$}
\AxiomC{$\ll \Gamma \vdash A \rr = \Gamma' \models A'$}
\RightLabel{, $x \notin \Gamma$}
\BinaryInfC{$\ll \Gamma, x : A \rr = A'$}
\DisplayProof
\end{center}
\bigskip

Интерпретация переменных:

\medskip
\begin{center}
\AxiomC{$\ll \Gamma \vdash A \rr = \Gamma' \models A'$}
\RightLabel{, $x \notin \Gamma$}
\UnaryInfC{$\ll \Gamma, x : A \vdash x \Uparrow A \rr = A' \models a : \pi_{A'}^*(A')$}
\DisplayProof
\end{center}

где $a$ определяется как в следующей диаграме:
\[ \xymatrix@-1pc{ A' \ar[rddd]_{id_{A'}} \ar[rrrd]^{id_{A'}} \ar@{-->}[rd]_a & & & \\
                        & \pi_{A'}^*(A') \ar[rr]_-{q(\pi_{A'}, A')} \ar[dd]^{\pi_{\pi_{A'}^*(A')}} \pb & & A' \ar[dd]^{\pi_{A'}} \\
                        &                                                                              & & \\
                        & A' \ar[rr]_{\pi_{A'}}                                                        & & \Gamma'
                 }\]

\begin{center}
\AxiomC{$\ll \Gamma \vdash x \Uparrow A \rr = \Gamma' \models a : A'$}
\AxiomC{$\ll \Gamma \vdash B \rr = \Gamma' \models B'$}
\RightLabel{, $y \notin \Gamma$}
\BinaryInfC{$\ll \Gamma, y : B \vdash x \Uparrow A \rr = B' \models \pi_{B'}^*(a) : \pi_{B'}^*(A')$}
\DisplayProof
\end{center}
\bigskip

Интерпретация правила проверки типа:

\medskip
\begin{center}
\AxiomC{$\ll \Gamma \vdash a \Uparrow A_1 \rr = \Gamma' \models a' : A_1'$}
\AxiomC{$\ll \Gamma \vdash A_k \red^* B \rr = \Gamma' \times I' \models S_k$, $k \in \{ 1, 2 \}$}
\BinaryInfC{$\ll \Gamma \vdash a \Downarrow A_2 \rr = \Gamma' \models i_1^*(ext(H,a')) : A_2'$}
\DisplayProof
\end{center}

Данное правило применимо если $A_k'$ - первые элементы последовательностей $S_k$, и последние элементы последовательностей $S_1$ и $S_2$ совпадают.
Чтобы определить $H$ сначала определим объект $CI(S_1, A, S_2)$ для любых последовательностей $S_1$, $S_2$ и объекта $A$ таких, что $\Gamma' \times I' \models A$, последний элемент $S_1$ равен $i_0^*(A)$, и последний элемент $S_2$ равен $i_1^*(A)$.
Объект $CI(S_1, A, S_2)$ будет определяться индукцией по суммарной длине $S_1$ и $S_2$ и будет удовлетворять следующим совйствам: $\Gamma' \times I' \models CI(S_1, A, S_2)$, первый элемент $S_1$ равен $i_0^* CI(S_1, A, S_2)$, и первый элемент $S_2$ равен $i_1^* CI(S_1, A, S_2)$.
\begin{itemize}
\item Если $S_1 = (i_0^*(A))$, $S_2 = (i_1^*(A))$, то $CI(S_1, A, S_2) = A$.
\item Если $S_1 = (i_0^*(A))$, $S_2 = (S_2', H_2, i_1^*(A))$, \\
    то $CI(S_1, S_2) = CI(S_1, Con(A, Inv(H_2)), S_2')$.
\item Если $S_1 = (S_1', H_1, i_0^*(A))$, $S_2 = (i_1^*(A))$, \\
    то $CI(S_1, S_2) = CI(S_1', Con(H_1, A), S_2)$.
\item Если $S_1 = (S_1', H_1, i_0^*(A))$, $S_2 = (S_2', H_2, i_1^*(A))$, \\
    то $CI(S_1, S_2) = CI(S_1', Con(H_1, Con(A, Inv(H_2))), S_2')$.
\end{itemize}
Тогда $H = CI(S_1, \pi_1^*(B), S_2)$, где $B$ - последний элемент последовательностей $S_1$ и $S_2$.
Основное свойство функции $CI$: для любых $S_1$, $S_2$, $B$ и $H$ верно, что $CI((S_1, H, B), \pi_1^*(B), (S_2, H, B)) = CI(S_1, \pi_1^*(B), S_2)$.

Интерпретация правил редукций типов:

\medskip
\begin{center}
\AxiomC{$\ll \Gamma \vdash A \rr = \Gamma' \models A'$}
\UnaryInfC{$\ll \Gamma \vdash A \red^* A \rr = \Gamma' \times I' \models (A')$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\ll \Gamma \vdash A \red B \rr = \Gamma' \times I' \models H$}
\AxiomC{$\ll \Gamma \vdash B \red^* C \rr = \Gamma' \times I' \models S$}
\BinaryInfC{$\ll \Gamma \vdash A \red^* C \rr = \Gamma' \times I' \models H * S$}
\DisplayProof
\end{center}

Данное правило применимо при условии, что первый элемент последовательности $H_2$ равен $i_1^*(H_1)$.

\begin{comment}
Пусть $\Gamma.A \xrightarrow{t} P(\Gamma.A) \xrightarrow{\langle p_1, p_2 \rangle} \Gamma.A \times \Gamma.A$ - объект путей для $\Gamma.A$.

Во-первых, определим $h'_1 : \Gamma \to P(\Gamma.A)$ как композицию $p \circ i_1$, где $p$ определяется следующим образом:
\[ \xymatrix{ \Gamma \ar[r]^-a \ar[d]_{i_0} & \Gamma.A \ar[r]^-t & P(\Gamma.A) \ar[d]^{\langle p_1, p_2 \rangle} \\
              \Gamma \times I' \ar[rr]_-{\langle a \circ \pi_1, h_1 \rangle} \ar@{-->}[urr]^p & & \Gamma.A \times \Gamma.A
            }\]
Во-вторых, определим $h'_3 : \Gamma \to P(\Gamma.A)$ как композицию $q \circ i_1$, где $q$ определяется следующим образом:
\[ \xymatrix{ \Gamma \ar[rr]^{h'_1} \ar[d]_{i_0}                  & & P(\Gamma.A) \ar[d]^{\langle p_1, p_2 \rangle} \\
              \Gamma \times I' \ar[rr]_-{\langle a \circ \pi_1, h_2 \rangle} \ar@{-->}[urr]^q & & \Gamma.A \times \Gamma.A
            }\]
Теперь определим $h_3 : \Gamma \times I' \to \Gamma.A$ как композицию $p_2 \circ s$, где $s$ определяется следующим образом:
\[ \xymatrix{ \Gamma \amalg \Gamma \ar[rr]^{[t \circ a, h'_3]} \ar[d] & & P(\Gamma.A) \ar[d]^{p_1} \\
              \Gamma \times I' \ar[r]_-{\pi_1} \ar@{-->}[urr]^s & \Gamma \ar[r]_-a & \Gamma.A
            }\]
\end{comment}

\subsection{Свойства интерпретации}

Нам понадобится вспомогательное отношение $\ll - \vdash - \Uparrow - \rr = -$ на классе $Ctx \times Env \times Ctx \times Hom(\C)$, где $Env$ - множество частичных функций $Var \to Term$ с конечным носителем.
Нигде неопределенную функцию мы будем обозначать $\bot : Var \to Term$.
Если $\rho \in Env$, $x \in Var$ и $a \in Term$, то $\rho[x := a] \in Env$ - функция такая, что $\rho[x := a](x) = a$, и $\rho[x := a](y) = \rho(y)$, если $y \neq x$.
Отношение определяется индуктивно:
\begin{center}
\AxiomC{$\ll \Delta \rr = \Delta'$}
\UnaryInfC{$\ll \Delta \vdash \bot \Uparrow\ \rr =\ !_{\Delta'} : \Delta' \to 1$}
\DisplayProof
\end{center}
\medskip

\begin{center}
\AxiomC{$\ll \Delta \vdash \rho \Uparrow \Gamma \rr = \rho' : \Delta' \to \Gamma'$}
\AxiomC{$\ll \Gamma \vdash A \rr = \Gamma' \models A'$}
\AxiomC{$\ll \Delta \vdash a \Uparrow A[\rho] \rr = \Delta' \models a' : \rho'^*(A')$}
\RightLabel{, $x \notin \Delta,\Gamma$}
\TrinaryInfC{$\ll \Delta \vdash \rho[x := a] \Uparrow \Gamma, x : A \rr = q(\rho', A') \circ a' : \Delta' \to A'$}
\DisplayProof
\end{center}
\bigskip

\begin{lem}[completeness][Completeness of the interpretation of the reduction rules]
Верны следующие утверждения:
\begin{enumerate}
\item Если $\ll \Gamma \rr = \Gamma'$, то $\Gamma \vdash$.
\item Если $\ll \Gamma \vdash A \rr = \Gamma' \models A'$, то $\Gamma \vdash A$.
\item Если $\ll \Gamma \vdash a \Uparrow A \rr = \Gamma' \models a' : A'$, то $\Gamma \vdash a \Uparrow A$.
\item Если $\ll \Gamma \vdash a \Downarrow A \rr = \Gamma' \models a' : A'$, то $\Gamma \vdash a \Downarrow A$.
\item Если $\ll \Gamma \vdash A \red B \rr = \Gamma' \times I' \models H$, то $\Gamma \vdash A$, и $A \red B$.
\item Если $\ll \Gamma \vdash A \red^* B \rr = \Gamma' \times I' \models H$, то $\Gamma \vdash A$, и $A \red^* B$.
\item Если $\ll \Gamma \vdash a \red b \Downarrow A \rr = \Gamma' \times I' \models h : A'$, то $\Gamma \vdash a \Downarrow A$, и $a \red b$.
\end{enumerate}
\end{lem}
\begin{proof}
Индукцией по определению отношения интерпретации.
\end{proof}

\begin{lem}[functionality][Functionality of the interpretation]
Верны следующие утверждения:
\begin{enumerate}
\item Если $\ll \Gamma \rr = \Gamma_1$, и $\ll \Gamma \rr = \Gamma_2$, то $\Gamma_1 = \Gamma_2$.
\item Если $\ll \Gamma \vdash A \rr = \Gamma_1 \models A_1$, и $\ll \Gamma \vdash A \rr = \Gamma_2 \models A_2$, то $\Gamma_1 = \Gamma_2$, и $A_1 = A_2$.
\item Если $\ll \Gamma \vdash a \Uparrow A_1 \rr = \Gamma_1 \models a_1 : A'_1$, и $\ll \Gamma \vdash a \Uparrow A_2 \rr = \Gamma_2 \models a_2 : A'_2$, то $A_1 = A_2$, $\Gamma_1 = \Gamma_2$, $A'_1 = A'_2$, и $a_1 = a_2$.
\item Если $\ll \Gamma \vdash a \Downarrow A \rr = \Gamma_1 \models a_1 : A_1$, и $\ll \Gamma \vdash a \Downarrow A \rr = \Gamma_2 \models a_2 : A_2$, то $\Gamma_1 = \Gamma_2$, $A_1 = A_2$, и $a_1 = a_2$.
\item Если $\ll \Gamma \vdash A \red B_1 \rr = \Gamma_1 \times I' \models H_1$, и $\ll \Gamma \vdash A \red B_2 \rr = \Gamma_2 \times I' \models H_2$, то $B_1 = B_2$, $\Gamma_1 = \Gamma_2$, и $H_1 = H_2$.
\item Если $\ll \Gamma \vdash A \red^* B \rr = \Gamma_1 \times I' \models S_1$, и $\ll \Gamma \vdash A \red^* B \rr = \Gamma_2 \times I' \models S_2$, то $\Gamma_1 = \Gamma_2$, и $S_1 = S_2$.
\item Если $\ll \Gamma \vdash a \red b_1 \Downarrow A \rr = \Gamma_1 \times I' \models h_1 : A_1$, и $\ll \Gamma \vdash a \red b_2 \Downarrow A \rr = \Gamma_2 \times I' \models h_2 : A_2$, то $b_1 = b_2$, $\Gamma_1 = \Gamma_2$, $A_1 = A_2$, и $h_1 = h_2$.
\end{enumerate}
\end{lem}
\begin{proof}
Индукцией по определению отношения интерпретации.
Покажем не очевидные пункты:
\begin{itemize}
\item
\AxiomC{$\ll \Gamma \vdash a \Uparrow A_1 \rr = \Gamma' \models a' : A_1'$}
\AxiomC{$\ll \Gamma \vdash A_k \red^* B^j \rr = \Gamma' \times I' \models S^j_k$, $k \in \{ 1, 2 \}$}
\BinaryInfC{$\ll \Gamma \vdash a \Downarrow A_2 \rr = \Gamma' \models i_1^*(ext(CI(S^j_1, \pi_1^*(B'^j), S^j_2), a')) : A_2'$}
\DisplayProof
\medskip

По индукционной гипотезе $A_1$, $\Gamma'$, $a'$ и $A_1'$ однозначно определяется по $\Gamma$ и $a$.
Несложно видеть, что $A_2'$ однозначно определяется по $\Gamma$ и $A_2$.
Нам осталось показать, что $CI(S^1_1, \pi_1^*(B'^1), S^1_2) = CI(S^2_1, \pi_1^*(B'^2), S^2_2)$.
Легко видеть, что либо $\ll \Gamma \vdash B^1 \red^* B^2 \rr = \Gamma' \times I' \models T_k$, либо $\ll \Gamma \vdash B^2 \red^* B^1 \rr = \Gamma' \times I' \models T_k$, где $T_k$ - некоторые суффиксы либо $S^2_k$, либо $S^1_k$ соответственно.
Заметим, что для каждого $k \in \{ 1, 2 \}$ должен быть верен либо первый случай, либо второй одновременно, иначе по лемме~\rlem{completeness} $B^1$ редуцируется сам к себе, что противоречит сильной нормализации.
Пусть для определенности верен первый случай.
Тогда $S^2_k$ суть конкатенации $S^1_k$ и $T_k$.
По индукционной гипотезе $T_1 = T_2$, и по свойствам функции $CI$ мы получаем необходимое равенство.

\item
Пусть $\ll \Gamma \vdash A \red^* C \rr = \Gamma_1 \times I' \models S_1$, и $\ll \Gamma \vdash A \red^* C \rr = \Gamma_2 \times I' \models S_2$.
Заметим, что оба этих отношения должны выводиться по одному и тому же правилу.
Действительно, если одно из них выводится по транзитивности, а другое по рефлексивности, тогда мы получаем, что $A \red B$, $B \red^* C$, и $A = C$, что протеворечит сильной нормализации.
Случай, когда оба отношения выводится по рефлексивности элементарен.
Если оба отношения выводятся по транзитивности, то $B$ и $S_1$ однозначно определяются по $\Gamma$ и $A$, а $S_2$ однозначно определяется по $\Gamma$, $B$ и $C$.

\end{itemize}
\end{proof}

Таким образом отношения $\ll - \rr = -$ определяют частичные функции, которые мы будем обозначать $\ll - \rr$.

\begin{lem}[subst-lemma][Correctness of the substitution]
Пусть $\ll \Delta \vdash \rho \Uparrow \Gamma \rr = \rho' : \Delta' \to \Gamma'$.
Тогда верны следующие утверждения:
\begin{enumerate}
\item Если $\ll \Gamma \vdash A \rr = \Gamma' \models A'$, то $\ll \Delta \vdash A[\rho] \rr = \Delta' \models \rho'^*(A')$.
\item Если $\ll \Gamma \vdash a \Uparrow A \rr = \Gamma' \models a' : A'$, \\
    то $\ll \Delta \vdash a[\rho] \Uparrow A[\rho] \rr = \Delta' \models \rho'^*(a') : \rho'^*(A')$.
\item Если $\ll \Gamma \vdash a \Downarrow A \rr = \Gamma' \models a' : A'$, \\
    то $\ll \Delta \vdash a[\rho] \Downarrow A[\rho] \rr = \Delta' \models \rho'^*(a') : \rho'^*(A')$.
\item Если $\ll \Gamma \vdash A \red B \rr = \Gamma' \times I' \models H$, \\
    то $\ll \Delta \vdash A[\rho] \red B[\rho] \rr = \Delta' \times I' \models (\rho' \times I')^*(H)$.
\item Если $\ll \Gamma \vdash A \red^* B \rr = \Gamma' \times I' \models S$, \\
    то $\ll \Delta \vdash A[\rho] \red^* B[\rho] \rr = \Delta' \times I' \models (\rho' \times I')^*(S)$.
\item Если $\ll \Gamma \vdash a \red b \Downarrow A \rr = \Gamma' \times I' \models h : \pi_1^*(A')$, \\
    то $\ll \Delta \vdash a[\rho] \red b[\rho] \Downarrow A[\rho] \rr = \Delta' \times I' \models (\rho' \times I')^*(h) : \pi_1^* \rho'^*(A')$.
\end{enumerate}
\end{lem}
\begin{proof}
Индукцией по построению $\ll - \rr = -$.
\begin{itemize}
\item
\AxiomC{$\ll \Gamma \vdash A \rr = \Gamma' \models A'$}
\UnaryInfC{$\ll \Gamma, x : A \vdash x \Uparrow A \rr = A' \models \langle id_{A'}, id_{A'} \rangle : \pi_{A'}^*(A')$}
\DisplayProof
\medskip

Так как $\ll \Delta \vdash \rho \Uparrow \Gamma, x : A \rr = \rho' : \Delta' \to A'$, то существуют $\rho_1$ и $a$ такие, что $\ll \Delta \vdash \rho_1 \Uparrow \Gamma \rr = \rho_1' : \Delta' \to \Gamma'$, $\ll \Gamma \vdash A \rr = \Gamma' \models A'$, $\ll \Delta \vdash a \Uparrow A[\rho_1]\rr = \Delta' \models a' : \rho_1'^*(A')$, $\rho = \rho_1[x := a]$, и $\rho' = q(\rho_1', A') \circ a'$.

Нам нужно доказать, что $\ll \Delta \vdash x[\rho_1[x := a]] \Uparrow A[\rho_1[x := a]] \rr = \Delta' \models a'^* q(\rho_1', A')^*(\langle id_{A'}, id_{A'} \rangle) : a'^* q(\rho_1', A')^* \pi_{A'}^*(A')$.
Но $x[\rho_1[x := a]] = a$, и по лемме~\rlem{completeness} $\Gamma \vdash A$, следовательно $x \notin FV(A)$, следовательно $A[\rho_1[x := a]] = A[\rho_1]$.

Равенство $a'^* q(\rho_1', A')^* \pi_{A'}^*(A') = \rho_1'^*(A')$ следует из следующего равенства: $\pi_{A'} \circ q(\rho_1', A') \circ a' = \rho_1' \circ \pi_{A'} \circ a' = \rho_1'$.
Нам осталось показать, что $a'^* q(\rho_1', A')^*(\langle id_{A'}, id_{A'} \rangle) = a'$.
Сечения $\Delta' \to \rho_1'^*(A')$ определяются морфизмом $\Delta' \to A'$, но оба сечения порождают морфизм $q(\rho_1', A') \circ a'$.

\bigskip
\item
\AxiomC{$\ll \Gamma \vdash x \Uparrow A \rr = \Gamma' \models a : A'$}
\AxiomC{$\ll \Gamma \vdash B \rr = \Gamma' \models B'$}
\BinaryInfC{$\ll \Gamma, y : B \vdash x \Uparrow A \rr = B' \models \pi_{B'}^*(a) : \pi_{B'}^*(A')$}
\DisplayProof
\medskip

Так как $\ll \Delta \vdash \rho \Uparrow \Gamma, y : B \rr = \rho' : \Delta' \to B'$, то существуют $\rho_1$ и $b$ такие, что $\ll \Delta \vdash \rho_1 \Uparrow \Gamma \rr = \rho_1' : \Delta' \to \Gamma'$, $\ll \Gamma \vdash B \rr = \Gamma' \models B'$, $\ll \Delta \vdash b \Uparrow B[\rho_1]\rr = \Delta' \models b' : \rho_1'^*(B')$, $\rho = \rho_1[y := b]$, и $\rho' = q(\rho_1', B') \circ b'$.

Нам нужно доказать, что $\ll \Delta \vdash x[\rho_1[y := b]] \Uparrow B[\rho_1[y := a]] \rr = \Delta' \models b'^* q(\rho_1', B')^* \pi_{B'}^*(a) : b'^* q(\rho_1', B')^* \pi_{B'}^*(A')$.
Но $x[\rho_1[y := b]] = x$, и по лемме~\rlem{completeness} $\Gamma \vdash B$, следовательно $y \notin FV(B)$, следовательно $B[\rho_1[y := b]] = B[\rho_1]$.

Равенства $b'^* q(\rho_1', B')^* \pi_{B'}^*(a) = \rho_1'^*(a)$ и $b'^* q(\rho_1', B')^* \pi_{B'}^*(A') = \rho_1'^*(B')$ следуют из следующего равенства: $\pi_{B'} \circ q(\rho_1', B') \circ b' = \rho_1' \circ \pi_{B'} \circ b' = \rho_1'$.

\bigskip
\item
\AxiomC{$\ll \Gamma \vdash a \Uparrow A_1 \rr = \Gamma' \models a' : A_1'$}
\AxiomC{$\ll \Gamma \vdash A_k \red^* B \rr = \Gamma' \times I' \models S_k$}
\BinaryInfC{$\ll \Gamma \vdash a \Downarrow A_2 \rr = \Gamma' \models i_1^*(ext(CI(S_1, \pi_1^*(B'), S_2), a')) : A_2'$}
\DisplayProof
\medskip

По индукционной гипотезе \\
$\ll \Delta \vdash a[\rho] \Uparrow A_1[\rho] \rr = \Delta' \models \rho'^*(a') : \rho'^*(A_1') $ \\
$\ll \Delta \vdash A_k[\rho] \red^* B[\rho] \rr = \Delta' \times I' \models (\rho' \times I')^*(S_k) $ \\
Следовательно $\ll \Delta \vdash a[\rho] \Downarrow A_2[\rho] \rr =$ \\
$\Delta' \models i_1^*(ext(CI((\rho' \times I')^*(S_1), \pi_1^* \rho'^*(B'), (\rho' \times I')^*(S_2)), \rho'^*(a'))) : \rho'^*(A_2') =$ \\
$\Delta' \models i_1^*(ext((\rho' \times I')^*(CI(S_1, \pi_1^*(B'), S_2)), \rho'^*(a'))) : \rho'^*(A_2') =$ \\
$\Delta' \models \rho'^* i_1^*(ext(CI(S_1, \pi_1^*(B'), S_2), a')) : \rho'^*(A_2')$.

\bigskip
\item
\AxiomC{$\ll \Gamma \vdash A \rr = \Gamma' \models A'$}
\UnaryInfC{$\ll \Gamma \vdash A \red^* A \rr = \Gamma' \times I' \models \pi_1^*(A')$}
\DisplayProof
\medskip

По индукционной гипотезе $\ll \Delta \vdash A[\rho] \rr = \Delta' \models \rho'^*(A')$.
Следовательно $\ll \Delta \vdash A[\rho] \red^* A[\rho] \rr = \Delta' \times I' \models \pi_1^* \rho'^*(A') = \Delta' \times I' \models (\rho' \times I')^* \pi_1^*(A')$.

\bigskip
\item
\AxiomC{$\ll \Gamma \vdash A \red B \rr = \Gamma' \times I' \models H$}
\AxiomC{$\ll \Gamma \vdash B \red^* C \rr = \Gamma' \times I' \models S$}
\BinaryInfC{$\ll \Gamma \vdash A \red^* C \rr = \Gamma' \times I' \models H * S$}
\DisplayProof
\medskip

По индукционной гипотезе \\
$\ll \Delta \vdash A[\rho] \red B[\rho] \rr = \Delta' \times I' \models (\rho' \times I')^*(H)$, \\
$\ll \Delta \vdash B[\rho] \red^* C[\rho] \rr = \Delta' \times I' \models (\rho' \times I')^*(S)$. \\
Следовательно $\Delta \vdash A[\rho] \red^* C[\rho] \rr =$ \\
$\Delta' \times I' \models (\rho' \times I')^*(H) * (\rho' \times I')^*(S) = \Delta' \times I' \models (\rho' \times I')^*(H * S)$.

\end{itemize}
\end{proof}

\begin{comment}
\begin{lem}[weakening][Weakening lemma]
Пусть $\ll \Gamma_1 \vdash \Delta \rr = \Delta' \dotsb \Gamma_1'$, и $\ll \Gamma_1 \vdash \Gamma_2 \rr = \Gamma_2' \dotsb \Gamma_1'$.
Тогда верны следующие утверждения:
\begin{enumerate}
\item Если $\ll \Gamma_1, \Gamma_2 \vdash \rr = \Gamma_1'.\Gamma_2'$, то $\ll \Gamma_1, \Delta, \Gamma_2 \vdash \rr = \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$.
\item Если $\ll \Gamma_1, \Gamma_2 \vdash A \rr = A' \dotsb \Gamma_1'.\Gamma_2'$, \\
    то $\ll \Gamma_1, \Delta, \Gamma_2 \vdash A \rr = (\pi_{\Delta'}.\Gamma_2')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$.
\item Если $\ll \Gamma_1, \Gamma_2 \vdash a \Uparrow A \rr = a' : A' \dotsb \Gamma_1'.\Gamma_2'$, \\
    то $\ll \Gamma_1, \Delta, \Gamma_2 \vdash a \Uparrow A \rr = (\pi_{\Delta'}.\Gamma_2')^*(a') : (\pi_{\Delta'}.\Gamma_2')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$.
\item Если $\ll \Gamma_1, \Gamma_2 \vdash a \Downarrow A \rr = a' : A' \dotsb \Gamma_1'.\Gamma_2'$, \\
    то $\ll \Gamma_1, \Delta, \Gamma_2 \vdash a \Downarrow A \rr = (\pi_{\Delta'}.\Gamma_2')^*(a') : (\pi_{\Delta'}.\Gamma_2')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$.
\end{enumerate}
\end{lem}
\begin{proof}
Индукцией по построению $\ll - \rr = -$.
\begin{itemize}
\item Если $\Gamma_2$ - пусто, и $\ll \Gamma_1 \rr = \Gamma_1'$, то $\ll \Gamma_1, \Delta \rr = \Gamma_1'.\Delta'$.

\bigskip
\item 
\AxiomC{$\ll \Gamma_1, \Gamma_2 \vdash A \rr = A' \dotsb \Gamma_1'.\Gamma_2'$}
\UnaryInfC{$\ll \Gamma_1, \Gamma_2, x : A \vdash \rr = \Gamma_1'.\Gamma_2'.A'$}
\DisplayProof
\medskip

По индукционной гипотезе $\ll \Gamma_1, \Delta, \Gamma_2 \vdash A \rr = (\pi_{\Delta'}.\Gamma_2')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$.
Следовательно $\ll \Gamma_1, \Delta, \Gamma_2, x : A \vdash \rr = \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2').(\pi_{\Delta'}.\Gamma_2')^*(A') = \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2'.A')$.

\bigskip
\item 
\AxiomC{$\ll \Gamma_1, \Gamma_2 \vdash \rr = \Gamma_1'.\Gamma_2'$}
\UnaryInfC{$\ll \Gamma_1, \Gamma_2, x : I' \vdash \rr = \Gamma_1'.\Gamma_2' \times I'$}
\DisplayProof
\medskip

По индукционной гипотезе $\ll \Gamma_1, \Delta, \Gamma_2 \vdash \rr = \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$.
Следовательно $\ll \Gamma_1, \Delta, \Gamma_2, x : I' \vdash \rr = \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \times I' = \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2').!^*(I') = \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2'.!^*(I'))$.

\bigskip
\item Если $\Gamma_2$ - пусто, $\ll \Gamma_1 \vdash x \Uparrow A \rr = a : A' \dotsb \Gamma_1'$, то индукцией по длине $\Delta'$ легко показать, что $\ll \Gamma_1, \Delta \vdash x \Uparrow A \rr = \pi_{\Delta'}(a) : \pi_{\Delta'}(A') \dotsb \Gamma_1'.\Delta'$.

\bigskip
\item 
\AxiomC{$\ll \Gamma_1, \Gamma_2 \vdash A \rr = A' \dotsb \Gamma_1'.\Gamma_2'$}
\UnaryInfC{$\ll \Gamma_1, \Gamma_2, x : A \vdash x \Uparrow A \rr = \langle id, id \rangle : \pi_{A'}^*(A') \dotsb \Gamma_1'.\Gamma_2'.A'$}
\DisplayProof
\medskip

По индукционной гипотезе $\ll \Gamma_1, \Delta, \Gamma_2 \vdash A \rr = (\pi_{\Delta'}.\Gamma_2')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$.
Пусть $A'' = (\pi_{\Delta'}.\Gamma_2')^*(A')$.
Тогда $\ll \Gamma_1, \Delta, \Gamma_2, x : A \vdash x \Uparrow A \rr = \langle id, id \rangle : \pi_{A''}^* (\pi_{\Delta'}.\Gamma_2')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2'.A')$.
Но $\pi_{\Delta'}.\Gamma_2' \circ \pi_{A''} = \pi_{A'} \circ \pi_{\Delta'}.\Gamma_2'.A'$.
Сечение $b : \pi_{A''}^*(A'') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2'.A')$ определяется морфизмом $\Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2'.A') \to \Gamma_1'.\Gamma_2'.A'$.
Оба сечения $\langle id, id \rangle$ и $\pi_{\Delta'.\Gamma_2'.A'}^*(\langle id, id \rangle)$ порождают один и тот же морфизм $\pi_{\Delta'}.\Gamma_2'.A' : \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2'.A') \to \Gamma_1'.\Gamma_2'.A'$.
Следовательно $\ll \Gamma_1, \Delta, \Gamma_2, x : A \vdash x \Uparrow A \rr = \pi_{\Delta'.\Gamma_2'.A'}^*(\langle id, id \rangle) : (\pi_{\Delta'}.\Gamma_2'.A')^* \pi_{A'}^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2'.A')$.

\bigskip
\item 
\AxiomC{$\ll \Gamma_1, \Gamma_2 \vdash x \Uparrow A \rr = a : A' \dotsb \Gamma_1'.\Gamma_2'$}
\AxiomC{$\ll \Gamma_1, \Gamma_2 \vdash B \rr = B' \dotsb \Gamma_1'.\Gamma_2'$}
\RightLabel{, $y \notin \Gamma$}
\BinaryInfC{$\ll \Gamma_1, \Gamma_2, y : B \vdash x \Uparrow A \rr = \pi_{B'}^*(a) : \pi_{B'}^*(A') \dotsb \Gamma_1'.\Gamma_2'.B'$}
\DisplayProof
\medskip

По индукционной гипотезе
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash x \Uparrow A \rr = (\pi_{\Delta'}.\Gamma_2')^*(a') : (\pi_{\Delta'}.\Gamma_2')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$, и
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash B \rr = (\pi_{\Delta'}.\Gamma_2')^*(B') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$.
Следовательно
    $\ll \Gamma_1, \Delta, \Gamma_2, y : B \vdash x \Uparrow A \rr =$
    $\pi_{(\pi_{\Delta'}.\Gamma_2')^*(B')}^* (\pi_{\Delta'}.\Gamma_2')^*(a') : \pi_{(\pi_{\Delta'}.\Gamma_2')^*(B')}^* (\pi_{\Delta'}.\Gamma_2')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2'.B') =$
    $(\pi_{\Delta'}.\Gamma_2'.B')^* \pi_{B'}^*(a') : (\pi_{\Delta'}.\Gamma_2'.B')^* \pi_{B'}^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2'.B')$.

\bigskip
\item
\AxiomC{$\ll \Gamma_1, \Gamma_2 \vdash a \Uparrow A_1 \rr = a' : A' \dotsb \Gamma_1'.\Gamma_2'$}
\AxiomC{$\ll \Gamma_1, \Gamma_2 \vdash A_2 \rr = A' \dotsb \Gamma_1'.\Gamma_2'$}
\BinaryInfC{$\ll \Gamma_1, \Gamma_2 \vdash a \Downarrow A_2 \rr = a' : A' \dotsb \Gamma_1'.\Gamma_2'$}
\DisplayProof
\medskip

По индукционной гипотезе
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash a \Uparrow A_1 \rr = (\pi_{\Delta'}.\Gamma_2')^*(a') : (\pi_{\Delta'}.\Gamma_2')^* A' \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$, и
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash A_2 \rr = (\pi_{\Delta'}.\Gamma_2')^* A' \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$.
Следовательно $\ll \Gamma, \Delta \vdash a \Downarrow A_2 \rr = (\pi_{\Delta'}.\Gamma_2')^*(a') : (\pi_{\Delta'}.\Gamma_2')^* A' \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$.

\bigskip
\item
\AxiomC{$\ll \Gamma_1, \Gamma_2 \vdash A \rr = A' \dotsb \Gamma_1'.\Gamma_2'$}
\AxiomC{$\ll \Gamma_1, \Gamma_2 \vdash k \Uparrow I' \rr = k' : \Gamma_1'.\Gamma_2' \to \Gamma_1'.\Gamma_2' \times I'$}
\BinaryInfC{$\ll \Gamma_1, \Gamma_2 \vdash Red^*\ A\ A\ k \rr = A' \dotsb \Gamma_1'.\Gamma_2'$}
\DisplayProof
\medskip

По индукционной гипотезе
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash A \rr = (\pi_{\Delta'}.\Gamma_2')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$, и
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash k : I' \rr = (\pi_{\Delta'}.\Gamma_2')^*(k') : \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \to \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \times I'$.
Следовательно $\ll \Gamma_1, \Delta, \Gamma_2 \vdash Red^*\ A\ A\ k \rr = (\pi_{\Delta'}.\Gamma_2')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$.

\bigskip
\item
\def\extraVskip{0.5pt}
\Axiom$\fCenter \ll \Gamma_1, \Gamma_2 \vdash A \rr = i_0^*(H_1) \dotsb \Gamma_1'.\Gamma_2'$
\noLine
\UnaryInf$\fCenter \ll \Gamma_1, \Gamma_2, x : I' \vdash Red\ A\ B\ x \rr = H_1 \dotsb \Gamma_1'.\Gamma_2' \times I'$
\noLine
\UnaryInf$\fCenter \ll \Gamma_1, \Gamma_2, x : I' \vdash Red^*\ B\ C\ x \rr = H_2 \dotsb \Gamma_1'.\Gamma_2' \times I'$
\noLine
\UnaryInf$\fCenter \ll \Gamma_1, \Gamma_2 \vdash k \Uparrow I' \rr = k' : \Gamma_1'.\Gamma_2' \to \Gamma_1'.\Gamma_2' \times I'$
\def\extraVskip{2pt}
\UnaryInf$\fCenter \ll \Gamma_1, \Gamma_2 \vdash Red^*\ A\ C\ k \rr = k'^*(Con(H_1, H_2)) \dotsb \Gamma_1'.\Gamma_2'$
\DisplayProof
\medskip

По индукционной гипотезе
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash A \rr = (\pi_{\Delta'}.\Gamma_2')^* i_0^*(H_1) \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$,
    $\ll \Gamma_1, \Delta, \Gamma_2, x : I' \vdash Red\ A\ B\ x \rr = (\pi_{\Delta'}.\Gamma_2' \times I')^*(H_1) \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \times I'$,
    $\ll \Gamma_1, \Delta, \Gamma_2, x : I' \vdash Red^*\ B\ C\ x \rr = (\pi_{\Delta'}.\Gamma_2' \times I')^*(H_2) \dotsb \Gamma'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \times I'$, и
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash k \Uparrow I' \rr = (\pi_{\Delta'}.\Gamma_2')^*(k') : \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \to \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \times I'$.
Следовательно
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash Red^*\ A\ C\ k \rr =$
    $((\pi_{\Delta'}.\Gamma_2')^*(k'))^* Con((\pi_{\Delta'}.\Gamma_2' \times I')^*(H_1), (\pi_{\Delta'}.\Gamma_2' \times I')^*(H_2)) \dotsb \Gamma'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \times I' =$
    $((\pi_{\Delta'}.\Gamma_2')^*(k'))^* (\pi_{\Delta'}.\Gamma_2' \times I')^* Con(H_1, H_2) \dotsb \Gamma'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \times I' =$
    $(\pi_{\Delta'}.\Gamma_2')^* k'^* Con(H_1, H_2) \dotsb \Gamma'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \times I'$.

\bigskip
\item
\AxiomC{$\ll \Gamma_1, \Gamma_2 \vdash a \Downarrow A \rr = a' : A' \dotsb \Gamma_1'.\Gamma_2'$}
\AxiomC{$\ll \Gamma_1, \Gamma_2 \vdash k \Uparrow I' \rr = k' : \Gamma_1'.\Gamma_2' \to \Gamma_1'.\Gamma_2' \times I'$}
\BinaryInfC{$\ll \Gamma_1, \Gamma_2 \vdash red^*\ a\ a\ k \Downarrow A \rr = a' : A' \dotsb \Gamma_1'.\Gamma_2'$}
\DisplayProof
\medskip

По индукционной гипотезе
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash a \Downarrow A \rr = (\pi_{\Delta'}.\Gamma_2')^*(a') : (\pi_{\Delta'}.\Gamma_2')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}(\Gamma_2')$, и
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash k \Uparrow I' \rr = (\pi_{\Delta'}.\Gamma_2')^*(k') : \Gamma_1'.\Delta'.\pi_{\Delta'}(\Gamma_2') \to \Gamma_1'.\Delta'.\pi_{\Delta'}(\Gamma_2') \times I'$.
Следовательно
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash red^*\ a\ a\ k \Downarrow A \rr = (\pi_{\Delta'}.\Gamma_2')^*(a') : (\pi_{\Delta'}.\Gamma_2')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}(\Gamma_2')$.

\bigskip
\item
\def\extraVskip{0.5pt}
\Axiom$\fCenter \ll \Gamma_1, \Gamma_2 \vdash A \rr = A' \dotsb \Gamma_1'.\Gamma_2'$
\noLine
\UnaryInf$\fCenter \ll \Gamma_1, \Gamma_2, x : I' \vdash red\ a\ a'\ x \Downarrow A \rr = h_1 : \pi_1^*(A') \dotsb \Gamma_1'.\Gamma_2' \times I'$
\noLine
\UnaryInf$\fCenter \ll \Gamma_1, \Gamma_2, x : I' \vdash red^*\ a'\ a''\ x \Downarrow A \rr = h_2 : \pi_1^*(A') \dotsb \Gamma_1'.\Gamma_2' \times I'$
\noLine
\UnaryInf$\fCenter \ll \Gamma_1, \Gamma_2 \vdash k \Uparrow I' \rr = k' : \Gamma_1'.\Gamma_2' \to \Gamma_1'.\Gamma_2' \times I'$
\def\extraVskip{2pt}
\UnaryInf$\fCenter \ll \Gamma_1, \Gamma_2 \vdash red^*\ a\ a''\ k \Downarrow A \rr = k'^*(con(h_1, h_2)) : A' \dotsb \Gamma_1'.\Gamma_2'$
\DisplayProof
\medskip

По индукционной гипотезе
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash A \rr = (\pi_{\Delta'}.\Gamma_2')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$,
    $\ll \Gamma_1, \Delta, \Gamma_2, x : I' \vdash red\ a\ a'\ x \Downarrow A \rr = (\pi_{\Delta'}.\Gamma_2' \times I')^*(h_1) : (\pi_{\Delta'}.\Gamma_2' \times I')^* \pi_1^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \times I' =$
        $(\pi_{\Delta'}.\Gamma_2' \times I')^*(h_1) : \pi_1^* (\pi_{\Delta'}.\Gamma_2')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \times I'$,
    $\ll \Gamma_1, \Delta, \Gamma_2, x : I' \vdash red^*\ a'\ a''\ x \Downarrow A \rr = (\pi_{\Delta'}.\Gamma_2' \times I')^*(h_2) : \pi_1^* (\pi_{\Delta'}.\Gamma_2')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \times I'$, и
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash k \Uparrow I' \rr = (\pi_{\Delta'}.\Gamma_2')^*(k') : \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \to \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \times I'$.
Следовательно
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash red^*\ a\ a''\ k \Downarrow A \rr = ((\pi_{\Delta'}.\Gamma_2')^*(k'))^* con((\pi_{\Delta'}.\Gamma_2' \times I')^*(h_1), (\pi_{\Delta'}.\Gamma_2' \times I')^*(h_2)) : (\pi_{\Delta'}.\Gamma_2')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') =$
    $((\pi_{\Delta'}.\Gamma_2')^*(k'))^* (\pi_{\Delta'}.\Gamma_2' \times I')^*con(h_1, h_2) : (\pi_{\Delta'}.\Gamma_2')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') =$
    $(\pi_{\Delta'}.\Gamma_2')^* k'^* con(h_1, h_2) : (\pi_{\Delta'}.\Gamma_2')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$.

\bigskip
\item
\AxiomC{$\ll \Gamma_1, \Gamma_2 \vdash \rr = \Gamma_1'.\Gamma_2'$}
\UnaryInfC{$\ll \Gamma_1, \Gamma_2 \vdash left' \Uparrow I' \rr = i_0 : \Gamma_1'.\Gamma_2' \to \Gamma_1'.\Gamma_2' \times I'$}
\DisplayProof
\medskip

По индукционной гипотезе $\ll \Gamma_1, \Delta, \Gamma_2 \vdash \rr = \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$.
Следовательно
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash left' \Uparrow I' \rr =$
    $i_0 : \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \to \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \times I' =$
    $(\pi_{\Delta'}.\Gamma_2')^*(i_0) : \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \to \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \times I'$.

\bigskip
\item
\AxiomC{$\ll \Gamma_1, \Gamma_2 \vdash \rr = \Gamma_1'.\Gamma_2'$}
\UnaryInfC{$\ll \Gamma_1, \Gamma_2 \vdash right' \Uparrow I' \rr = i_1 : \Gamma_1'.\Gamma_2' \to \Gamma_1'.\Gamma_2' \times I'$}
\DisplayProof
\medskip

Аналогично предыдущему пункту.

\bigskip
\item
\def\extraVskip{0.5pt}
\Axiom$\fCenter \ll \Gamma_1, \Gamma_2, x : I' \vdash A \rr = A' \dotsb \Gamma_1'.\Gamma_2' \times I'$
\noLine
\UnaryInf$\fCenter \ll \Gamma_1, \Gamma_2 \vdash a \Downarrow A[x := left'] \rr = a' : i_0^*(A') \dotsb \Gamma_1'.\Gamma_2'$
\noLine
\UnaryInf$\fCenter \ll \Gamma_1, \Gamma_2 \vdash k \Uparrow I' \rr = k' : \Gamma_1'.\Gamma_2' \to \Gamma_1'.\Gamma_2' \times I'$
\def\extraVskip{2pt}
\UnaryInf$\fCenter \ll \Gamma_1, \Gamma_2 \vdash coe'\ (\lambda x. A)\ a\ k \Uparrow A[x := k] \rr = k'^*(ext(A', a')) : k'^*(A') \dotsb \Gamma_1'.\Gamma_2'$
\DisplayProof
\medskip

По индукционной гипотезе
    $\ll \Gamma_1, \Delta, \Gamma_2, x : I' \vdash A \rr = (\pi_{\Delta'}.\Gamma_2' \times I')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \times I'$,
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash a \Downarrow A[x := left'] \rr = (\pi_{\Delta'}.\Gamma_2')^*(a') : (\pi_{\Delta'}.\Gamma_2')^* i_0^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$, и
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash k \Uparrow I' \rr = (\pi_{\Delta'}.\Gamma_2')^*(k') : \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \to \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') \times I'$.
Следовательно
    $\ll \Gamma_1, \Delta, \Gamma_2 \vdash coe'\ (\lambda x. A)\ a\ k \Uparrow A[x := k] \rr =$
    $((\pi_{\Delta'}.\Gamma_2')^*(k'))^*(ext((\pi_{\Delta'}.\Gamma_2' \times I')^*(A'), (\pi_{\Delta'}.\Gamma_2')^*(a'))) : ((\pi_{\Delta'}.\Gamma_2')^*(k'))^* (\pi_{\Delta'}.\Gamma_2' \times I')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') =$
    $((\pi_{\Delta'}.\Gamma_2')^*(k'))^* (\pi_{\Delta'}.\Gamma_2' \times I')^*(ext(A', a')) : ((\pi_{\Delta'}.\Gamma_2')^*(k'))^* (\pi_{\Delta'}.\Gamma_2' \times I')^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2') =$
    $(\pi_{\Delta'}.\Gamma_2')^* k'^*(ext(A', a')) : (\pi_{\Delta'}.\Gamma_2')^* k'^*(A') \dotsb \Gamma_1'.\Delta'.\pi_{\Delta'}^*(\Gamma_2')$.

\end{itemize}
\end{proof}

\begin{lem}[correctness-subst][Correctness of the substitution]
Пусть $\ll \Gamma \vdash \rr = \Gamma'$, $\ll \Gamma \vdash a \Uparrow A \rr = a' : A' \dotsb \Gamma'$, и $\ll \Gamma, x : A \vdash \Delta \rr = \Delta' \dotsb \Gamma'.A'$.
Тогда верны следующие утверждения:
\begin{enumerate}
\item Если $\ll \Gamma, x : A, \Delta \vdash \rr = \Gamma'.A'.\Delta'$, то $\ll \Gamma, \Delta[x := a] \vdash \rr = \Gamma'.a'^*(\Delta')$.
\item Если $\ll \Gamma, x : A, \Delta \vdash B \rr = B' \dotsb \Gamma'.A'.\Delta'$, \\
    то $\ll \Gamma, \Delta[x := a] \vdash B[x := a] \rr = (a'.\Delta')^*(B') \dotsb \Gamma'.a'^*(\Delta')$.
\item Если $\ll \Gamma, x : A, \Delta \vdash b \Downarrow B \rr = b' : B' \dotsb \Gamma'.A'.\Delta'$, \\
    то $\ll \Gamma, \Delta[x := a] \vdash b[x := a] \Downarrow B[x := a] \rr = (a'.\Delta')^*(b') : (a'.\Delta')^*(B') \dotsb \Gamma.a'^*(\Delta')$.
\item Если $\ll \Gamma, x : A, \Delta \vdash b \Uparrow B \rr = b' : B' \dotsb \Gamma'.A'.\Delta'$, \\
    то $\ll \Gamma, \Delta[x := a] \vdash b[x := a] \Uparrow B[x := a] \rr = (a'.\Delta')^*(b') : (a'.\Delta')^*(B') \dotsb \Gamma.a'^*(\Delta')$.
\end{enumerate}
\end{lem}
\begin{proof}
Индукцией по построению $\ll - \rr = -$.
\begin{itemize}
\item
\AxiomC{$\ll \Gamma \vdash A \rr = A' \dotsb \Gamma'$}
\UnaryInfC{$\ll \Gamma, x : A \vdash \rr = \Gamma'.A'$}
\DisplayProof
\medskip

По предположению $\ll \Gamma \vdash \rr = \Gamma'$.

\bigskip
\item
\AxiomC{$\ll \Gamma, x : A, \Delta \vdash A_{n+1} \rr = A'_{n+1} \dotsb \Gamma'.A'.\Delta'$}
\UnaryInfC{$\ll \Gamma, x : A, \Delta, x_{n+1} : A_{n+1} \vdash \rr = \Gamma'.A'.\Delta'.A'_{n+1}$}
\DisplayProof
\medskip

По индукционной гипотезе $\ll \Gamma, \Delta[x := a] \vdash A_{n+1}[x := a] \rr = (a'.\Delta')^*(A'_{n+1}) \dotsb \Gamma'.a'^*(\Delta')$.
Следовательно $\ll \Gamma, \Delta[x := a], x_{n+1} : A_{n+1}[x := a] \vdash \rr = \Gamma'.a'^*(\Delta').(a'.\Delta')^*(A'_{n+1}) = \Gamma'.a'^*(\Delta'.A'_{n+1})$.

\bigskip
\item
\AxiomC{$\ll \Gamma \vdash A \rr = A' \dotsb \Gamma'$}
\UnaryInfC{$\ll \Gamma, x : A \vdash x \Uparrow A \rr = \langle id_{\Gamma'.A'}, id_{\Gamma'.A'} \rangle : \pi_{A'}^*(A') \dotsb \Gamma'.A'$}
\DisplayProof
\medskip

По предположению $\ll \Gamma \vdash a \Uparrow A \rr = a' : A' \dotsb \Gamma' = a'^*(\langle id_{\Gamma'.A'}, id_{\Gamma'.A'} \rangle) : a'^*(\pi_{A'}^*(A')) \dotsb \Gamma'$.

\bigskip
\item
\AxiomC{$\ll \Gamma, x : A, \Delta \vdash A_{n+1} \rr = A'_{n+1} \dotsb \Gamma'.A'.\Delta'$}
\UnaryInfC{$\ll \Gamma, x : A, \Delta, x_{n+1} : A_{n+1} \vdash x_{n+1} \Uparrow A_{n+1} \rr = \langle id, id \rangle : \pi_{A'_{n+1}}^*(A'_{n+1}) \dotsb \Gamma.A'.\Delta'.A'_{n+1}$}
\DisplayProof
\medskip

По индукционной гипотезе $\ll \Gamma, \Delta[x := a] \vdash A_{n+1}[x := a] \rr = (a'.\Delta')^*(A'_{n+1}) \dotsb \Gamma'.a'^*(\Delta')$.
Следовательно
    $\ll \Gamma, \Delta[x := a], x_{n+1} : A_{n+1}[x := a] \vdash x_{n+1} \Uparrow A_{n+1}[x := a] \rr =$
    $\langle id, id \rangle : \pi_{(a'.\Delta')^*(A'_{n+1})}^*(a'.\Delta')^*(A'_{n+1}) \dotsb \Gamma'.a'^*(\Delta').(a'.\Delta')^*(A'_{n+1}) =$
    $(a'.\Delta'.A'_{n+1})^*(\langle id, id \rangle) : (a'.\Delta'.A'_{n+1})^* \pi_{A'_{n+1}}^*(A'_{n+1}) \dotsb \Gamma'.a'^*(\Delta'.A'_{n+1})$.

\bigskip
\item
\AxiomC{$\ll \Gamma \vdash y \Uparrow B \rr = b : B' \dotsb \Gamma'$}
\AxiomC{$\ll \Gamma \vdash A \rr = A' \dotsb \Gamma'$}
\BinaryInfC{$\ll \Gamma, x : A \vdash y \Uparrow B \rr = \pi_{A'}^*(b) : \pi_{A'}^*(B') \dotsb \Gamma'.A'$}
\DisplayProof
\medskip

$\ll \Gamma \vdash y[x := a] \Uparrow B[x := a] \rr = \ll \Gamma \vdash y \Uparrow B \rr = b : B' \dotsb \Gamma' = a'^* \pi_{A'}^*(b) : a'^* \pi_{A'}^*(B') \dotsb \Gamma'$.

\bigskip
\item
\AxiomC{$\ll \Gamma, x : A, \Delta \vdash y \Uparrow B \rr = b : B' \dotsb \Gamma'.A'.\Delta'$}
\AxiomC{$\ll \Gamma, x : A, \Delta \vdash A_{n+1} \rr = A'_{n+1} \dotsb \Gamma'.A'.\Delta'$}
\BinaryInfC{$\ll \Gamma, x : A, \Delta, x_{n+1} : A_{n+1} \vdash y \Uparrow B \rr = \pi_{A'_{n+1}}^*(b) : \pi_{A'_{n+1}}^*(B') \dotsb \Gamma'.A'.\Delta'.A'_{n+1}$}
\DisplayProof
\medskip

По индукционной гипотезе
    $\ll \Gamma, \Delta[x := a] \vdash y[x := a] \Uparrow B[x := a] \rr = (a'.\Delta')^*(b) : (a'.\Delta')^*(B') \dotsb \Gamma'.a'^*(\Delta')$, и
    $\ll \Gamma, \Delta[x := a] \vdash A_{n+1}[x := a] \rr = (a'.\Delta')^*(A'_{n+1}) \dotsb \Gamma'.a'^*(\Delta')$. \\
По лемме~\rlem{weakening} $\ll \Gamma, \Delta[x := a], x_{n+1} : A_{n+1} \vdash y[x := a] \Uparrow B[x := a] \rr = \pi_{(a'.\Delta')^*(A'_{n+1})}^*(a'.\Delta')^*(b) : \pi_{(a'.\Delta')^*(A'_{n+1})}^*(a'.\Delta')^*(B') \dotsb \Gamma'.a'^*(\Delta'.A'_{n+1})$,
Теперь утверждение следует из того факта, что $a'.\Delta' \circ \pi_{(a'.\Delta')^*(A'_{n+1})} = \pi_{A'_{n+1}} \circ a'.\Delta'.A'_{n+1}$.

\bigskip
\item
\AxiomC{$\ll \Gamma, x : A, \Delta \vdash b \Uparrow B_1 \rr = b' : B' \dotsb \Gamma'.A'.\Delta'$}
\AxiomC{$\ll \Gamma, x : A, \Delta \vdash B_2 \rr = B' \dotsb \Gamma'.A'.\Delta'$}
\BinaryInfC{$\ll \Gamma, x : A, \Delta \vdash b \Downarrow B_2 \rr = b' : B' \dotsb \Gamma'.A'.\Delta'$}
\DisplayProof
\medskip

По индукционной гипотезе
    $\ll \Gamma, \Delta[x := a] \vdash b[x := a] \Uparrow B_1[x := a] \rr = (a'.\Delta')^*(b') : (a'.\Delta')^* B' \dotsb \Gamma'.a'^*(\Delta')$, и
    $\ll \Gamma, \Delta[x := a] \vdash B_2[x := a] \rr = (a'.\Delta')^* B' \dotsb \Gamma'.a'^*(\Delta')$.
Следовательно $\ll \Gamma, \Delta[x := a] \vdash b[x := a] \Downarrow B_2[x := a] \rr = (a'.\Delta')^*(b') : (a'.\Delta')^* B' \dotsb \Gamma'.a'^*(\Delta')$.

\bigskip
\item
\AxiomC{$\ll \Gamma, x : A, \Delta \vdash B \rr = B' \dotsb \Gamma'.A'.\Delta'$}
\AxiomC{$\ll \Gamma, x : A, \Delta \vdash k \Uparrow I' \rr = k' : \Gamma'.A'.\Delta' \to \Gamma'.A'.\Delta' \times I'$}
\BinaryInfC{$\ll \Gamma, x : A, \Delta \vdash Red^*\ A\ A\ k \rr = B' \dotsb \Gamma'.A'.\Delta'$}
\DisplayProof
\medskip

По индукционной гипотезе
    $\ll \Gamma, \Delta[x := a] \vdash B[x := a] \rr = (a'.\Delta')^*(B') \dotsb \Gamma'.a'^*(\Delta')$, и
    $\ll \Gamma, \Delta[x := a] \vdash k[x := a] \Uparrow I' \rr = (a'.\Delta')^*(k') : \Gamma'.a'^*(\Delta') \to \Gamma'.a'^*(\Delta') \times I'$.
Следовательно $\ll \Gamma, \Delta[x := a] \vdash Red^*\ B[x := a]\ B[x := a]\ k[x := a] \rr = (a'.\Delta')^*(B') \dotsb \Gamma'.a'^*(\Delta')$.

\bigskip
\item
\def\extraVskip{0.5pt}
\Axiom$\fCenter \ll \Gamma, x : A, \Delta \vdash B \rr = i_0^*(H_1) \dotsb \Gamma'.A'.\Delta'$
\noLine
\UnaryInf$\fCenter \ll \Gamma, x : A, \Delta, y : I' \vdash Red\ B\ C\ y \rr = H_1 \dotsb \Gamma'.A'.\Delta' \times I'$
\noLine
\UnaryInf$\fCenter \ll \Gamma, x : A, \Delta, y : I' \vdash Red^*\ C\ D\ y \rr = H_2 \dotsb \Gamma'.A'.\Delta' \times I'$
\noLine
\UnaryInf$\fCenter \ll \Gamma, x : A, \Delta \vdash k \Uparrow I' \rr = k' : \Gamma'.A'.\Delta' \to \Gamma'.A'.\Delta' \times I'$
\def\extraVskip{2pt}
\UnaryInf$\fCenter \ll \Gamma, x : A, \Delta \vdash Red^*\ B\ D\ k \rr = k'^*(Con(H_1, H_2)) \dotsb \Gamma'.A'.\Delta'$
\DisplayProof
\medskip

По индукционной гипотезе
    $\ll \Gamma, \Delta[x := a] \vdash B[x := a] \rr = (a'.\Delta')^* i_0^*(H_1) \dotsb \Gamma'.a'^*(\Delta')$,
    $\ll \Gamma, \Delta[x := a], y : I' \vdash Red\ B[x := a]\ C[x := a]\ y \rr = (a'.\Delta' \times I')^*(H_1) \dotsb \Gamma'.a'^*(\Delta' \times I')$,
    $\ll \Gamma, \Delta[x := a], y : I' \vdash Red^*\ C[x := a]\ D[x := a]\ y \rr = (a'.\Delta' \times I')^*(H_2) \dotsb \Gamma'.a'^*(\Delta' \times I')$, и
    $\ll \Gamma, \Delta[x := a] \vdash k[x := a] \Uparrow I' \rr = (a'.\Delta')^*(k') : \Gamma'.a'^*(\Delta') \to \Gamma'.a'^*(\Delta') \times I'$.
Следовательно
    $\ll \Gamma, \Delta[x := a] \vdash Red^*\ B[x := a]\ D[x := a]\ k[x := a] \rr =$
    $((a'.\Delta')^*(k'))^* Con((a'.\Delta' \times I')^*(H_1), (a'.\Delta' \times I')^*(H_2)) \dotsb \Gamma'.a'^*(\Delta') =$
    $((a'.\Delta')^*(k'))^* (a'.\Delta' \times I')^*(Con(H_1, H_2)) \dotsb \Gamma'.a'^*(\Delta') = $
    $(a'.\Delta')^* k'^*(Con(H_1, H_2)) \dotsb \Gamma'.a'^*(\Delta')$.

\bigskip
\item
\AxiomC{$\ll \Gamma, x : A, \Delta \vdash b \Downarrow B \rr = b' : B' \dotsb \Gamma'.A'.\Delta'$}
\AxiomC{$\ll \Gamma, x : A, \Delta \vdash k \Uparrow I' \rr = k' : \Gamma'.A'.\Delta' \to \Gamma'.A'.\Delta' \times I'$}
\BinaryInfC{$\ll \Gamma, x : A, \Delta \vdash red^*\ b\ b\ k \Downarrow B \rr = b' : B' \dotsb \Gamma'.A'.\Delta'$}
\DisplayProof
\medskip

По индукционной гипотезе
    $\ll \Gamma, \Delta[x := a] \vdash b[x := a] \Downarrow B[x := a] \rr = (a'.\Delta')^*(b') : (a'.\Delta')^*(B') \dotsb \Gamma.a'^*(\Delta')$, и
    $\ll \Gamma, \Delta[x := a] \vdash k[x := a] \Uparrow I' \rr = (a'.\Delta')^*(k') : \Gamma'.a'^*(\Delta') \to \Gamma'.a'^*(\Delta') \times I'$.
Следовательно $\ll \Gamma, \Delta[x := a] \vdash red^*\ b[x := a]\ b[x := a]\ k[x := a] \Downarrow B[x := a] \rr = (a'.\Delta')^*(b') : (a'.\Delta')^*(B') \dotsb \Gamma.a'^*(\Delta')$.

\bigskip
\item
\def\extraVskip{0.5pt}
\Axiom$\fCenter \ll \Gamma, x : A, \Delta \vdash B \rr = B' \dotsb \Gamma'.A'.\Delta'$
\noLine
\UnaryInf$\fCenter \ll \Gamma, x : A, \Delta, y : I' \vdash red\ b\ c\ y \Downarrow B \rr = h_1 : \pi_1^*(B') \dotsb \Gamma'.A'.\Delta' \times I'$
\noLine
\UnaryInf$\fCenter \ll \Gamma, x : A, \Delta, y : I' \vdash red^*\ c\ d\ y \Downarrow B \rr = h_2 : \pi_1^*(B') \dotsb \Gamma'.A'.\Delta' \times I'$
\noLine
\UnaryInf$\fCenter \ll \Gamma, x : A, \Delta \vdash k \Uparrow I' \rr = k' : \Gamma'.A'.\Delta' \to \Gamma'.A'.\Delta' \times I'$
\def\extraVskip{2pt}
\UnaryInf$\fCenter \ll \Gamma, x : A, \Delta \vdash red^*\ b\ d\ k \Downarrow B \rr = k'^*(con(h_1, h_2)) : B' \dotsb \Gamma'.A'.\Delta'$
\DisplayProof
\medskip

По индукционной гипотезе
    $\ll \Gamma, \Delta[x := a] \vdash B[x := a] \rr = (a'.\Delta')^*(B') \dotsb \Gamma'.a'^*(\Delta')$,
    $\ll \Gamma, \Delta[x := a], y : I' \vdash red\ b[x := a]\ c[x := a]\ y[x := a] \Downarrow B[x := a] \rr = (a'.\Delta' \times I')^*(h_1) : (a'.\Delta' \times I')^* \pi_1^*(B') \dotsb \Gamma'.a'^*(\Delta' \times I')$,
    $\ll \Gamma, \Delta[x := a], y : I' \vdash red\ c[x := a]\ d[x := a]\ y[x := a] \Downarrow B[x := a] \rr = (a'.\Delta' \times I')^*(h_2) : (a'.\Delta' \times I')^* \pi_1^*(B') \dotsb \Gamma'.a'^*(\Delta' \times I')$, и
    $\ll \Gamma, \Delta[x := a] \vdash k[x := a] \Uparrow I' \rr = (a'.\Delta')^*(k') : \Gamma'.a'^*(\Delta') \to \Gamma'.a'^*(\Delta') \times I'$.
Следовательно
    $\ll \Gamma, \Delta[x := a] \vdash red^*\ b[x := a]\ d[x := a]\ k[x := a] \Downarrow B[x := a] \rr =$
    $((a'.\Delta')^*(k'))^* con((a'.\Delta' \times I')^*(h_1), (a'.\Delta' \times I')^*(h_2)) : (a'.\Delta')^*(B') \dotsb \Gamma'.a'^*(\Delta') =$
    $((a'.\Delta')^*(k'))^* (a'.\Delta' \times I')^* con(h_1, h_2) : (a'.\Delta')^*(B') \dotsb \Gamma'.a'^*(\Delta') =$
    $(a'.\Delta')^* k'^* con(h_1, h_2) : (a'.\Delta')^*(B') \dotsb \Gamma'.a'^*(\Delta')$.

\bigskip
\item
\AxiomC{$\ll \Gamma, x : A, \Delta \vdash \rr = \Gamma'.A'.\Delta'$}
\UnaryInfC{$\ll \Gamma, x : A, \Delta \vdash left' \Uparrow I' \rr = i_0 : \Gamma'.A'.\Delta' \to \Gamma'.A'.\Delta' \times I'$}
\DisplayProof
\medskip

По индукционной гипотезе $\ll \Gamma, \Delta[x := a] \vdash \rr = \Gamma'.a'^*(\Delta')$.
Следовательно $\Gamma, \Delta[x := a] \vdash left' \Uparrow I' \rr = i_0 : \Gamma'.a'^*(\Delta') \to \Gamma'.a'^*(\Delta') \times I' = (a'.\Delta')^*(i_0) : \Gamma'.a'^*(\Delta') \to \Gamma'.a'^*(\Delta') \times I'$

\bigskip
\item
\AxiomC{$\ll \Gamma, x : A, \Delta \vdash \rr = \Gamma'.A'.\Delta'$}
\UnaryInfC{$\ll \Gamma, x : A, \Delta \vdash right' \Uparrow I' \rr = i_1 : \Gamma'.A'.\Delta' \to \Gamma'.A'.\Delta' \times I'$}
\DisplayProof
\medskip

Аналогично предыдущему пункту.

\bigskip
\item
\def\extraVskip{0.5pt}
\Axiom$\fCenter \ll \Gamma, x : A, \Delta, y : I' \vdash B \rr = B' \dotsb \Gamma'.A'.\Delta' \times I'$
\noLine
\UnaryInf$\fCenter \ll \Gamma, x : A, \Delta \vdash b \Downarrow B[y := left'] \rr = b' : i_0^*(B') \dotsb \Gamma'.A'.\Delta'$
\noLine
\UnaryInf$\fCenter \ll \Gamma, x : A, \Delta \vdash k \Uparrow I' \rr = k' : \Gamma'.A'.\Delta' \to \Gamma'.A'.\Delta' \times I'$
\def\extraVskip{2pt}
\UnaryInf$\fCenter \ll \Gamma, x : A, \Delta \vdash coe'\ (\lambda y. B)\ b\ k \Uparrow B[y := k] \rr = k'^*(ext(B', b')) : k'^*(B') \dotsb \Gamma'.A'.\Delta'$
\DisplayProof
\medskip

По индукционной гипотезе
    $\ll \Gamma, \Delta[x := a], y : I' \vdash B[x := a] \rr = (a'.\Delta' \times I')^*(B') \dotsb \Gamma'.a'^*(\Delta' \times I')$,
    $\ll \Gamma, \Delta[x := a] \vdash b[x := a] : B[y := left'][x := a] \rr = (a'.\Delta')^*(b') : (a'.\Delta')^* i_0^*(B') \dotsb \Gamma'.a'^*(\Delta')$,
    $\ll \Gamma, \Delta[x := a] \vdash k[x := a] \Uparrow I' \rr = (a'.\Delta')^*(k') : \Gamma'.a'^*(\Delta') \to \Gamma'.a'^*(\Delta') \times I'$.
Следовательно
    $\ll \Gamma, \Delta[x := a] \vdash coe'\ (\lambda y. B[x := a])\ b[x := a]\ k[x := a] \rr =$
    $((a'.\Delta')^*(k'))^*(ext((a'.\Delta' \times I')^*(B'), (a'.\Delta')^*(b'))) : ((a'.\Delta')^*(k'))^* (a'.\Delta' \times I')^*(B') \dotsb \Gamma'.a'^*(\Delta') =$
    $((a'.\Delta')^*(k'))^* (a'.\Delta' \times I')^*(ext(B', b')) : ((a'.\Delta')^*(k'))^* (a'.\Delta' \times I')^*(B') \dotsb \Gamma'.a'^*(\Delta') =$
    $(a'.\Delta')^* k'^*(ext(B', b')) : (a'.\Delta')^* k'^*(B') \dotsb \Gamma'.a'^*(\Delta')$.

\end{itemize}
\end{proof}
\end{comment}

\begin{lem}[coherence-typing][Coherence of the typing]
Верны следующие утверждения:
\begin{enumerate}
\item Если $\ll \Gamma \vdash A \rr = \Gamma' \models A'$, то $\ll \Gamma \rr = \Gamma'$.
\item Если $\ll \Gamma \vdash a \Uparrow A \rr = \Gamma' \models a : A'$, то $\ll \Gamma \vdash A \rr = \Gamma' \models A'$.
\item Если $\ll \Gamma \vdash a \Downarrow A \rr = \Gamma' \models a : A'$, то $\ll \Gamma \vdash A \rr = \Gamma' \models A'$.
\item Если $\ll \Gamma \vdash A \red B \rr = \Gamma' \times I' \models H$, то $\ll \Gamma \vdash A \rr = \Gamma' \models i_0^*(H)$, и $\ll \Gamma \vdash B \rr = \Gamma' \models i_1^*(H)$.
\item Если $\ll \Gamma \vdash A \red^* B \rr = \Gamma' \times I' \models S$, то $\ll \Gamma \vdash A \rr = A'$, и $\ll \Gamma \vdash B \rr = B'$, где $A'$, $B'$ - первый и последний элементы последовательности $S$.
\item Если $\ll \Gamma \vdash a \red b \Downarrow A\rr = \Gamma' \times I' \models h : \pi_1^*(A')$, то $\ll \Gamma \vdash a \Downarrow A \rr = \Gamma' \models i_0^*(h) : A'$, и $\ll \Gamma \vdash b \Downarrow A \rr = \Gamma' \models i_1^*(h) : A'$.
\end{enumerate}
\end{lem}
\begin{proof}
Индукцией по построению $\ll - \rr = -$.
Единственный нетривиальный случай - правила для переменных.
Для доказательства нам потребуется несколько вспомогательных утверждений.
Во-первых, если $\Gamma = x_1 : A_1, \ldots x_n : A_n$, $\ll \Gamma \rr = \Gamma'$, то для всех $1 \leq k \leq n$ верно $\ll \Gamma \vdash x_k \Uparrow A_n \rr = \Gamma' \models \langle id_{\Gamma'}, \pi^{n-k}_{\Gamma'} \rangle : (\pi^{n-k+1}_{\Gamma'})^*(ft^{n-k}(\Gamma')) $.
Это легко доказать индукцией по $n - k$.

Во-вторых, для любых $\Gamma = x_1 : A_1, \ldots x_n : A_n$, $\Gamma'$ и $0 \leq k \leq n$ таких, что $\ll \Gamma \rr = \Gamma'$, верно $\ll \Gamma \vdash id_{x_1, \ldots x_k} \Uparrow x_1 : A_1, \ldots x_k : A_k \rr = \pi^{n-k}_{\Gamma'} : \Gamma' \to ft^{n-k}(\Gamma')$, где $id_{x_1, \ldots x_k}$ - подстановка $id_{x_1, \ldots x_n}(x_i) = x_i$.
Это легко доказать индукцией по $k$, используя предыдущее замечание.

Теперь мы можем доказать неоходимое свойство.
Для этого достаточно показать, что если $\ll \Gamma \rr = \Gamma'$, $\ll \Gamma \vdash A \rr = \Gamma' \models A'$, $\ll \Gamma \vdash B \rr = \Gamma' \models B'$ и $y \notin \Gamma$, то $\ll \Gamma, y : B \vdash A \rr = B' \models \pi_{B'}^*(A')$.
Это следует из леммы~\rlem{subst-lemma}, примененной к $\ll \Gamma, y : B \vdash id_{x_1, \ldots x_n} \Uparrow \Gamma \rr = \pi_{B'} : B' \to \Gamma'$.
\end{proof}

\begin{lem}[correctness-reductions][Correctness of the interpretation of the reductions rules]
Верны следующие утверждения:
\begin{enumerate}
\item Если $\ll \Gamma \vdash A \rr = \Gamma' \models A'$, и $A \red B$, то $\ll \Gamma \vdash A \red B \rr$ определенно.
\item Если $\ll \Gamma \vdash A \rr = \Gamma' \models A'$, и $A \red^* B$, то $\ll \Gamma \vdash A \red^* B \rr$ определенно.
\item Если $\ll \Gamma \vdash a \Downarrow A \rr = \Gamma' \models a' : A'$, и $a \red b$, то $\ll \Gamma \vdash a \red b \Downarrow A \rr$ определенно.
\end{enumerate}
\end{lem}
\begin{proof}
Второй пункт элементарно следует из первого и леммы~\rlem{coherence-typing}.
Первый и третий пункты на данный момент тривиальны, так как мы не ввели пока никаких правил редукций.
\end{proof}

\begin{lem}[correctness-typing][Correctness of the interpretation of the typing rules]
Верны следующие утверждения:
\begin{enumerate}
\item Если $\Gamma \vdash$, то $\ll \Gamma \vdash \rr$ определенно.
\item Если $\Gamma \vdash A$, то $\ll \Gamma \vdash A \rr$ определенно.
\item Если $\Gamma \vdash a \Uparrow A$, то $\ll \Gamma \vdash a \Uparrow A \rr$ определенно.
\item Если $\Gamma \vdash a \Downarrow A$, то $\ll \Gamma \vdash a \Downarrow A \rr$ определенно.
\end{enumerate}
\end{lem}
\begin{proof}
Индукцией по построению $- \vdash -$, используя лемму~\rlem{coherence-typing}.
Единственный нетривиальный случай:
\begin{center}
\AxiomC{$\Gamma \vdash a \Uparrow A_1$}
\AxiomC{$\Gamma \vdash A_2$}
\RightLabel{, $A_1 \deq A_2$}
\BinaryInfC{$\Gamma \vdash a \Downarrow A_2$}
\DisplayProof
\end{center}

В этом случае, используя свойства конфлюентности и сильной нормализации, мы получаем, что существует терм $B$ такой, что $A_1 \red^* B$, и $A_2 \red^* B$.
Таким образом этот случай следует из леммы~\rlem{correctness-reductions}.
\end{proof}

\section{Конструкции}

\subsection{Сигма типы}

Мы добавляем следующие правила вывода и редукций:

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash A$}
\AxiomC{$\Gamma, x : A \vdash B$}
\BinaryInfC{$\Gamma \vdash \Sigma (x : A) B$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash a \Downarrow A$}
\AxiomC{$\Gamma, x : A \vdash B$}
\AxiomC{$\Gamma \vdash b \Downarrow B[x := a]$}
\TrinaryInfC{$\Gamma \vdash (a, b)_{\Sigma (x : A) B} \Uparrow \Sigma (x : A) B$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash p \Uparrow \Sigma (x : A) B$}
\UnaryInfC{$\Gamma \vdash proj_1\ p \Uparrow A$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash p \Uparrow \Sigma (x : A) B$}
\UnaryInfC{$\Gamma \vdash proj_2\ p \Uparrow B[x := proj_1\ p]$}
\DisplayProof
\end{center}

\medskip
\begin{align*}
& proj_1\ (a, b)_{\Sigma (x : A) B} \red a \\
& proj_2\ (a, b)_{\Sigma (x : A) B} \red b \\
\end{align*}

Чтобы определить интерпретацию, мы предполагаем, что в категории $\C$ определены следующие конструкции:
\begin{itemize}
\item Для любых $\Gamma$, $A$ и $B$ таких, что $\Gamma \models A$ и $B \models A$, определен объект $\Sigma(A, B)$ такой, что $\Gamma \models \Sigma(A, B)$, и для любого $f : \Delta \to \Gamma$ верно $f^*(\Sigma(A, B)) = \Sigma(f^*(A), q(f, A)^*(B))$.
\item Для любых $a$ и $b$ таких, что $\Gamma \models a : A$ и $\Gamma \models b : a^*(B)$, определен морфизм $pair(a, b)$ такой, что $\Gamma \models pair(a, b) : \Sigma(A, B)$, и для любого $f : \Delta \to \Gamma$ верно $f^*(pair(a, b)) = pair(f^*(a), f^*(b))$.
\item Для любого $p$ такого, что $\Gamma \models p : \Sigma (x : A) B$, определен морфизм $proj_1(p)$ такой, что $\Gamma \models proj_1(p) : A$, и для любого $f : \Delta \to \Gamma$ верно $f^*(proj_1(p)) = proj_1(f^*(p))$.
\item Для любого $p$ такого, что $\Gamma \models p : \Sigma (x : A) B$, определен морфизм $proj_2(p)$ такой, что $\Gamma \models proj_2(p) : proj_1(p)^*(B)$, и для любого $f : \Delta \to \Gamma$ верно $f^*(proj_2(p)) = proj_2(f^*(p))$.
\item Для любых $a$ и $b$ таких, что $\Gamma \models a : A$ и $\Gamma \models b : a^*(B)$, определен морфизм $proj_1.pair(a, b)$ такой, что $\Gamma \times I' \models proj_1.pair(a, b) : \pi_1^*(A)$, $i_0^*(proj_1.pair(a, b)) = proj_1(pair(a, b))$, $i_1^*(proj_1.pair(a, b)) = a$, и для любого $f : \Delta \to \Gamma$ верно $(f \times I')^*(proj_1.pair(a, b)) = proj_1.pair(f^*(a), f^*(b))$.
\item Для любых $a$ и $b$ таких, что $\Gamma \models a : A$ и $\Gamma \models b : a^*(B)$, определен морфизм $proj_2.pair(a, b)$ такой, что $\Gamma \times I' \models proj_2.pair(a, b) : \pi_1^* a^*(B)$, $i_0^*(proj_2.pair(a, b)) = proj_2(pair(a, b))$, $i_1^*(proj_1.pair(a, b)) = b$, и для любого $f : \Delta \to \Gamma$ верно $(f \times I')^*(proj_2.pair(a, b)) = proj_2.pair(f^*(a), f^*(b))$.
\end{itemize}
Теперь определим интерпретацию новых правил:

\medskip
\begin{center}
\AxiomC{$\ll \Gamma \vdash A \rr = \Gamma' \models A'$}
\AxiomC{$\ll \Gamma, x : A \vdash B \rr = A' \models B'$}
\BinaryInfC{$\ll \Gamma \vdash \Sigma (x : A) B \rr = \Gamma' \models \Sigma(A', B')$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\ll \Gamma \vdash a \Downarrow A \rr = \Gamma' \models a' : A'$}
\AxiomC{$\ll \Gamma, x : A \vdash B \rr = A' \models B'$}
\AxiomC{$\ll \Gamma \vdash b \Downarrow B[x := a] \rr = \Gamma' \models b' : a'^*(B')$}
\TrinaryInfC{$\ll \Gamma \vdash (a, b)_{\Sigma (x : A) B} \Uparrow \Sigma (x : A) B \rr = \Gamma' \models pair(a', b') : \Sigma(A', B')$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\ll \Gamma \vdash p \Uparrow \Sigma (x : A) B \rr = \Gamma' \models p' : \Sigma(A', B')$}
\AxiomC{$\ll \Gamma, x : A \vdash B \rr = A' \models B'$}
\BinaryInfC{$\ll \Gamma \vdash proj_1\ p \Uparrow A \rr = \Gamma' \models proj_1(p') : A'$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\ll \Gamma \vdash p \Uparrow \Sigma (x : A) B \rr = \Gamma' \models p' : \Sigma(A', B')$}
\AxiomC{$\ll \Gamma, x : A \vdash B \rr = A' \models B'$}
\BinaryInfC{$\ll \Gamma \vdash proj_2\ p \Uparrow B[x := proj_1\ p] \rr = \Gamma' \models proj_2(p') : proj_1(p')^*(B')$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\ll \Gamma \vdash a \Downarrow A \rr = \Gamma' \models a' : A'$}
\AxiomC{$\ll \Gamma, x : A \vdash B \rr = A' \models B'$}
\AxiomC{$\ll \Gamma \vdash b \Downarrow B[x := a] \rr = \Gamma' \models b' : a'^*(B')$}
\TrinaryInfC{$\ll \Gamma \vdash proj_1\ (a, b)_{\Sigma (x : A) B} \red a \Downarrow A \rr = \Gamma' \times I' \models proj_1.pair(a', b') : \pi_1^*(A')$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\ll \Gamma \vdash a \Downarrow A \rr = \Gamma' \models a' : A'$}
\AxiomC{$\ll \Gamma, x : A \vdash B \rr = A' \models B'$}
\AxiomC{$\ll \Gamma \vdash b \Downarrow B[x := a] \rr = \Gamma' \models b' : a'^*(B')$}
\TrinaryInfC{$\ll \Gamma \vdash proj_2\ (a, b)_{\Sigma (x : A) B} \red b \Downarrow B[x := a] \rr = \Gamma' \times I' \models proj_2.pair(a', b') : \pi_1^* a'^*(B')$}
\DisplayProof
\end{center}

\bibliographystyle{amsplain}
\bibliography{ref}

\end{document}