bidirectional.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}
% \usepackage[T2A]{fontenc}

\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}}
\expandafter\newcommand\csname R#2\endcsname[1]{#4~\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}{теорема}{Теорема}
\newref{lem}{лемма}{Лемма}
\newref{prop}{утверждение}{Утверждение}
\newref{cor}{следствие}{Следствие}

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

\theoremstyle{remark}
\newref{remark}{замечание}{Замечание}

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

\numberwithin{figure}{section}

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

\begin{document}

\title{Bidirectional type theory}

\author{Валерий Исаев}

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

\maketitle

\section{Введение}

\section{Двунаправленная теория типов}

Здесь мы определим теорию $T_B$.
Как и обычная теория типов Мартин-Лёфа, $T_B$ состоит из счетного множества переменных $Var$, множества термов $Term_B$, отношения эквивалентности на нем $\deq$.

Мы будем работать с теорией типов с $\Pi$ типами, $\Sigma$ типами, $Id$ типами и одной вселенной $U$.
Разумеется, теория может быть расширена другими конструкциями.

Множество термов определяется индуктивно следующим набором правил:
\[ Term_I := x\ |\ U\ | \]
\[ \Pi (x : A) B\ |\ \lambda x : A. b\ |\ b\ a\ | \]
\[ \Sigma (x : A) B\ |\ (a, b)_{\Sigma (x : A) B}\ |\ proj_1\ p\ |\ proj_2\ p\ | \]
\[ Id\ A\ a_1\ a_2\ |\ refl\ a\ |\ J\ (\lambda x_1 x_2 t. B)\ (\lambda x. b)\ a_1\ a_2\ p, \]
где $x$ - переменная, $A$, $B$, $a$, $a_1$, $a_2$, $b$ и $p$ - термы.

В отличие от теории типов Мартин-Лёфа, все конструкторы типизированы.
Множество контекстов $Ctx_I$ определяется следующим образом:
\[ Ctx_B = \{ x_1 : A_1, \ldots x_n : A_n\ |\ x_i \in Var, A_i \in Term_B \} \]
Пустой контекст мы будем обозначать $\diamond$.

Мы вводим четыре отношения $- \vdash$, $- \vdash -$, $- \vdash - \Uparrow -$ и $- \vdash - \Downarrow -$ на множествах $Ctx_B$, $Ctx_B \times Term_B$, $Ctx_B \times Term_B \times Term_B$ и $Ctx_B \times Term_B \times Term_B$ соответственно.
Они определяются в таблице~\ref{table:inf-rules}.

\begin{table}

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

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

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash a \Uparrow A$}
\AxiomC{$\Gamma \vdash B$}
\RightLabel{, $A \deq B$ $(CONV)$}
\BinaryInfC{$\Gamma \vdash a \Downarrow B$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, x : A \vdash B$}
\RightLabel{$(PI)$}
\UnaryInfC{$\Gamma \vdash \Pi (x : A) B$}
\DisplayProof
\quad
\AxiomC{$\Gamma, x : A \vdash b \Uparrow B$}
\RightLabel{$(LAM)$}
\UnaryInfC{$\Gamma \vdash \lambda x : A. b \Uparrow \Pi (x : A) B$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash f \Uparrow C$}
\AxiomC{$\Gamma \vdash a \Downarrow A$}
\RightLabel{, $C \red^*_h \Pi (x : A) B$ $(APP)$}
\BinaryInfC{$\Gamma \vdash f\ a \Uparrow B[x \mapsto a]$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, x : A \vdash B$}
\RightLabel{$(SIGMA)$}
\UnaryInfC{$\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 \mapsto a]$}
\RightLabel{$(PAIR)$}
\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 C$}
\RightLabel{, $C \red^*_h \Sigma (x : A) B$ $(PROJ_1)$}
\UnaryInfC{$\Gamma \vdash proj_1\ p \Uparrow A$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash p \Uparrow C$}
\RightLabel{, $C \red^*_h \Sigma (x : A) B$ $(PROJ_2)$}
\UnaryInfC{$\Gamma \vdash proj_2\ p \Uparrow B[x \mapsto proj_1\ p]$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash a_1 \Downarrow A$}
\AxiomC{$\Gamma \vdash a_2 \Downarrow A$}
\RightLabel{$(ID)$}
\BinaryInfC{$\Gamma \vdash Id\ A\ a_1\ a_2$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash a \Uparrow A$}
\RightLabel{$(REFL)$}
\UnaryInfC{$\Gamma \vdash refl\ a \Uparrow Id\ A\ a\ a$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\def\extraVskip{0.5pt}
\Axiom$\Gamma \fCenter , x_1 : A, x_2 : A, t : Id\ A\ x_1\ x_2 \vdash B$
\noLine
\UnaryInf$\Gamma \fCenter , x : A \vdash b \Downarrow B[x_1 \mapsto x, x_2 \mapsto x, t \mapsto refl\ x]$
\noLine
\UnaryInf$\Gamma \fCenter \vdash p \Uparrow C$
\RightLabel{, $C \red_h^* Id\ A\ a_1'\ a_2'$, $a_i \deq a_i'$ $(J)$}
\def\extraVskip{2pt}
\UnaryInf$\Gamma \fCenter \vdash J\ (\lambda x_1 x_2 t. B)\ (\lambda x. b)\ a_1\ a_2\ p \Uparrow$
\def\extraVskip{0.5pt}
\noLine
\UnaryInf$\fCenter B[x_1 \mapsto a_1', x_2 \mapsto a_2', t \mapsto p]$
\def\extraVskip{2pt}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\RightLabel{$(U)$}
\UnaryInfC{$\Gamma \vdash U$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash A \Downarrow U$}
\RightLabel{$(EL)$}
\UnaryInfC{$\Gamma \vdash A$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash A \Downarrow U$}
\AxiomC{$\Gamma, x : A \vdash B \Downarrow U$}
\RightLabel{$(U \text{-} PI)$}
\BinaryInfC{$\Gamma \vdash \Pi (x : A) B \Uparrow U$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash A \Downarrow U$}
\AxiomC{$\Gamma, x : A \vdash B \Downarrow U$}
\RightLabel{$(U \text{-} SIGMA)$}
\BinaryInfC{$\Gamma \vdash \Sigma (x : A) B \Uparrow U$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash A \Downarrow U$}
\AxiomC{$\Gamma \vdash a_1 \Downarrow A$}
\AxiomC{$\Gamma \vdash a_2 \Downarrow A$}
\RightLabel{$(U \text{-} ID)$}
\TrinaryInfC{$\Gamma \vdash Id\ A\ a_1\ a_2 \Uparrow U$}
\DisplayProof
\end{center}

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

На множестве термов очевидным образом определяется операция подстановки.
Если $b$ - терм, $\rho$ - частичная функция из $Var$ в $Term_B$, то $b[\rho]$ - терм, в котором все свободные вхождения переменных $x$ из домена $\rho$ заменены на $\rho(x)$.

Отношение $\deq$ является наименьшим отношением конгруэнтности (то есть отношением эквивалентности, замкнутым относительно конструкций термов), удовлетворяющим следующим свойствам:
\begin{itemize}
\item $(\lambda x : A. b)\ a \deq b[x \mapsto a]$.
\item $proj_1\ (a, b)_{\Sigma (x : A) B} \deq a$.
\item $proj_2\ (a, b)_{\Sigma (x : A) B} \deq b$.
\item $J\ (\lambda x_1 x_2 t. B)\ (\lambda x. b)\ a\ a\ refl \deq b[x \mapsto a]$.
\item $\lambda x : A. b\ x \deq b$, если $x \notin FV(b)$.
\item $(proj_1\ p, proj_2\ p)_{\Sigma (x : A) B} \deq p$.
\end{itemize}

Отношение $\red^*_h$ определяется как рефллексивное транзитивное замыкание отношения $\red_h$:
\begin{itemize}
\item Если $b \red_h b'$, то $b\ a \red_h b'\ a$.
\item $(\lambda x : A. b)\ a \red_h b[x \mapsto a]$.
\item Если $p \red_h p'$, то $proj_1\ p \red_h proj_1\ p'$.
\item Если $p \red_h p'$, то $proj_2\ p \red_h proj_2\ p'$.
\item $proj_1\ (a, b)_{\Sigma (x : A) B} \red_h a$.
\item $proj_2\ (a, b)_{\Sigma (x : A) B} \red_h b$.
\item Если $p \red_h p'$, то $J\ (\lambda x_1 x_2 t. B)\ (\lambda x. b)\ a_1\ a_2\ p \red_h J\ (\lambda x_1 x_2 t. B)\ (\lambda x. b)\ a_1\ a_2\ p'$.
\item $J\ (\lambda x_1 x_2 t. B)\ (\lambda x. b)\ a\ a\ (refl\ a) \red_h b[x \mapsto a]$.
\end{itemize}

Из правила $(CONV)$ следует, что отношение $- \vdash - \Uparrow -$ является подмножеством отношения $- \vdash - \Downarrow -$.
Отличие $- \vdash - \Uparrow -$ от $- \vdash - \Downarrow -$ заключается в том, что если $\Gamma \vdash a \Uparrow A$, то $A$ - в некотором смысле канонический тип $a$, а если $\Gamma \vdash a \Downarrow A'$, то верно только, что $A' \deq A$.
Таким образом, $\Gamma \vdash a \Uparrow A$ означает, что $A$ - это в некотором смысле канонический тип $a$.
Это замечание подтвержается следующим утверждением:

\begin{prop}
Если $\Gamma \vdash a \Uparrow A_1$ и $\Gamma \vdash a \Uparrow A_2$, то $A_1 = A_2$.
\end{prop}
\begin{proof}
Заметим, что если $a \red_h b_1$ и $a \red_h b_2$, то $b_1 = b_2$.
Следовательно, если термы $b_1$ и $b_2$ находятся в $\red_h$-нормальной форме и $a \red^*_h b_1$ и $a \red^*_h b_2$, то $b_1 = b_2$.
При этом термы вида $\Sigma (x : A) B$ и $\Pi (x : A) B$ находятся в $\red_h$-нормальной форме.

Используя эти замечания, утверждение элементарно доказывается индукцией по выводу.
\end{proof}

Мы будем обозначать $type : Ctx_E \times Term_E \to Term_E \amalg \{ * \}$ частичную функцию такую, что если $\Gamma \vdash a \Uparrow A$, то $type(\Gamma, a) = A$, если такого $A$ не существует и $\Gamma \vdash a$, то $type(\Gamma, a) = *$, иначе $type$ не определена.
Мы будем писать $\Gamma \vdash A \Uparrow *$ как синоним для $\Gamma \vdash A$.
Таким образом, $\Gamma \vdash a \Uparrow A$ тогда и только тогда, когда $type(\Gamma, a) = A$.

Контекстуальная категория теории $\C_{T_B}$ определяется следующим образом:
\[ Ob(\C_{T_B}) = \{ \Gamma \in Ctx_B\ |\ \Gamma \vdash \}. \]
Если $\Gamma = x_1 : A_1, \ldots x_n : A_n$ и $\Delta = y_1 : B_1, \ldots y_k : B_k$ - пара контекстов,
то множество $CT_B(\Gamma, \Delta)$ определяется как множество функций $\rho : \{ y_1, \ldots y_k\} \to Term_B$ таких, что
\[ \Gamma \vdash \rho(y_i) \Downarrow B_i[\rho |_{y_1, \ldots y_{i-1}}] \text{ для всех } 1 \leq i \leq k. \]
Тогда множество морфизмов $\C_{T_B}(\Gamma, \Delta)$ определяется как множество $CT_B(\Gamma, \Delta)$ с точностью до отношения эквивалентности $\deq$:
\[ \rho \deq \rho' \text{ тогда и только тогда, когда } \rho(y_i) \deq \rho'(y_i) \text{ для всех } 1 \leq i \leq k. \]
Тождественный морфизм $id_\Delta$ определяется как функция $id_\Delta(y_i) = y_i$.
Если $\rho : \Gamma \to \Delta$, $\tau : \Delta \to E$, где $E = z_1 : C_1, \ldots z_m : C_m$, то композиция $\tau \circ \rho$ определяется как функция $(\tau \circ \rho)(z_i) = \tau(z_i)[\rho]$.
Отношения типизации и эквивалентности определены так, что эти определения действительно задают категорию.

\subsection{Теория типов Мартин-Лёфа}
\label{subsec:MLTT}

Множество термов $Term_I$ теории типов Мартин-Лёфа $T_I$ задается тем же набором правил, что и $Term_B$ за исключением того, что мы заменяем правила $\lambda x : A. b$, $(a, b)_{\Sigma (x : A) B}$ и $refl\ a$:
\[ Term_I := \ldots\ |\ \lambda x. b\ |\ (a, b)\ |\ refl \]
Существует очевидная функция $F : Term_B \to Term_I$, удовлетворяющая следуюшим свойствам:
\begin{align*}
& F(\lambda x : A. b) = \lambda x. F(b) \\
& F((a, b)_{\Sigma (x : A) B}) = (F(a), F(b)) \\
& F(refl\ a) = refl
\end{align*}

Отношения $- \vdash$, $- \vdash -$ и $- \vdash - : -$ задаются на множествах $Ctx_I$, $Ctx_I \times Term_I$ и $Ctx_I \times Term_I \times Term_I$ соответственно.
Правила вывода такие же как в таблице~\ref{table:inf-rules}, если заменить все отношения $- \vdash - \Uparrow -$ и $- \vdash - \Downarrow -$ на $- \vdash - : -$ и ко всем термам применить функцию $F$.
Контекстуальная категория $\C_{T_I}$ определяется аналогичным $\C_{T_B}$ образом.
Функция $F$ задает функтор $F : \C_{T_E} \to \C_{T_I}$ очевидным образом.
Наша основная цель заключается в доказательстве теоремы~\rthm{equiv}, утверждающей, что $F$ является эквивалентностью категорий.

\subsection{Теория типов с явно типизированными конструкторами}

Теории $T_B$ и $T_I$ отличаются в двух аспектах: во-первых, у первой в конструкторах явно присутствуют типы, во-вторых, вместо одного отношения типизации в $T_I$ у нас есть два в $T_B$.
Чтобы лучше понять разницу между этими теориями, мы введем промежуточную теорию, в которой конструкторы будут явно типизированы, но отношение типизации будет такое же как в $T_I$.
Подобная теория описывается в \cite{luo94}.
Множество термов $Term_E$ совпадает с $Term_B$.
Правила вывода такие же как в таблице~\ref{table:inf-rules}, если заменить все отношения $- \vdash - \Uparrow -$ и $- \vdash - \Downarrow -$ на $- \vdash - : -$.

Отношение $\deq$ определяется так же как и раньше.
Контекстуальная категория теории $\C_{T_E}$ определяется аналогичным $\C_{T_B}$ образом.

\begin{prop}
Верны следующие утверждения:
\begin{itemize}
\item Если в $T_B$ выводится $\Gamma \vdash$, то в $T_E$ также выводится $\Gamma \vdash$.
\item Если в $T_B$ выводится $\Gamma \vdash A$, то в $T_E$ также выводится $\Gamma \vdash A$.
\item Если в $T_B$ выводится $\Gamma \vdash a \Uparrow A$ или $\Gamma \vdash a \Downarrow A$, то в $T_E$ выводится $\Gamma \vdash a : A$.
\end{itemize}
\end{prop}
\begin{proof}
Элементарная индукция по выводу.
\end{proof}

\begin{prop}
Верны следующие утверждения:
\begin{itemize}
\item Если в $T_E$ выводится $\Gamma \vdash$, то в $T_B$ также выводится $\Gamma \vdash$.
\item Если в $T_E$ выводится $\Gamma \vdash A$, то в $T_B$ также выводится $\Gamma \vdash A$.
\item Если в $T_E$ выводится $\Gamma \vdash a : A$, то в $T_B$ выводится $\Gamma \vdash a \Downarrow A$.
\end{itemize}
\end{prop}
\begin{proof}
TODO
\end{proof}

Предыдущие два утверждения доказывают, что отнашения $- \vdash$, $- \vdash -$ и $- \vdash - : -$ в $T_E$ и $- \vdash$, $- \vdash -$ и $- \vdash - \Downarrow -$ в $T_B$ совпадают.
Отсюда следует, что категории $\C_{T_E}$ и $\C_{T_B}$ совпадают.

\section{Эквивалентность теорий}

Мы уже определили функтор $\C_{T_I} \to \C_{T_B}$.
Чтобы определить функтор в обратную сторону, нам понадобится вспомогательное отношение $R \subseteq Ctx_B \times Term_I \times Term_B \times (Term_B \amalg \{ *, \top \})$.
Идея заключается в том, что если $R(\Gamma, a, a', A)$, то $a'$ - это $a$, в котором конструкторам приписаны типы.
$\Gamma$ и $A$ являются вспомогательными данными, чтобы восстановить эту информацию.
Отношение будет определено таким образом, что если $R(\Gamma, a, a', A)$ и $A \in Term_B$, то $\Gamma \vdash a' \Downarrow A$, если $A = *$, то $\Gamma \vdash a'$.
Иногда информация о типе бывает недоступна, в этом случае $A$ будет равно $\top$.

Сначала введем отношение предпорядка $\leq$ на множестве $Term_B \amalg \{ *, \top \}$. $a \leq b$ тогда и только тогда, когда выполнено одно из следующих условий: ($a \neq *$ и $b = \top$), $a \deq b$, $a = b$ или ($a \deq U$ и $b = *$).
Мы будем писать $\Gamma \vdash A \leq B$ для обозначения того факта, что $A \leq B$ и либо $\Gamma \vdash B$, либо $\Gamma \vdash$ и $B \in \{ *, \top \}$.
Теперь отношение $R$ определяется рекурсией по второму аргументу следующим образом:
\begin{itemize}
\item $R(\Gamma, x, x, B)$, если $x : A \in \Gamma$ и $\Gamma \vdash A \leq B$.
\item $R(\Gamma, \lambda x. b, \lambda x : A. b', C)$, если \\
    либо $\Gamma \vdash C$, $C \red_h^* \Pi (x : A) B$ и $R((\Gamma, x : A), b, b', B)$, \\
    либо $C = \top$, $\Gamma \vdash A$ и $R((\Gamma, x : A), b, b', \top)$.
\item $R(\Gamma, f\ a, f'\ a', D)$, если $\Gamma \vdash B[x \mapsto a'] \leq D$, \\
    $R(\Gamma, f, f', \top)$, $type(\Gamma, f') \red_h^* \Pi (x : A) B$ и $R(\Gamma, a, a', A)$.
\item $R(\Gamma, (a, b), (a', b')_{\Sigma (x : A) B}, C)$, если \\
    $R(\Gamma, a, a', A)$, $R(\Gamma, b, b', B[x \mapsto a'])$ и \\
    либо $\Gamma \vdash$ и $C = \top$, либо $\Gamma \vdash C$ и $C \red_h^* \Sigma (x : A) B$.
\item $R(\Gamma, proj_1\ p, proj_1\ p', D)$, если \\
    $R(\Gamma, p, p', \top)$, $type(\Gamma, p') \red_h^* \Sigma (x : A) B$ и $\Gamma \vdash A \leq D$.
\item $R(\Gamma, proj_2\ p, proj_2\ p', D)$, если \\
    $R(\Gamma, p, p', \top)$, $type(\Gamma, p') \red_h^* \Sigma (x : A) B$ и $\Gamma \vdash B[x \mapsto proj_1\ p'] \leq D$.
\item $R(\Gamma, refl, refl\ a, C)$, если \\
    либо $\Gamma \vdash C$, $C \red_h^* Id\ A\ a\ a'$ и $a \deq a'$, \\
    либо $C = \top$ и $type(\Gamma, a)$ определено.
\item $R(\Gamma, J\ (\lambda x_1 x_2 t. B)\ (\lambda x. b)\ a_1\ a_2\ p, J\ (\lambda x_1 x_2 t. B')\ (\lambda x. b')\ a_1'\ a_2'\ p', D)$, если
    $\Gamma \vdash B'[x_1 \mapsto a_1', x_2 \mapsto a_2', t \mapsto p'] \leq D$, \\
    $R(\Gamma, p, p', \top)$,
    $type(\Gamma, p') \red_h^* Id\ A\ a_1'\ a_2'$, \\
    $R((\Gamma, x_1 : A, x_2 : A, t : Id\ A\ x_1\ x_2), B, B', *)$ и \\
    $R((\Gamma, x : A), b, b', B'[x_1, \mapsto x, x_2 \mapsto x, t \mapsto refl\ x])$.
\item $R(\Gamma, U, U, D)$, если $\Gamma \vdash$ и $D = *$.
\item $R(\Gamma, \Pi (x : A) B, \Pi (x : A') B', D)$, если \\
    $\Gamma \vdash type(\Gamma, \Pi (x : A') B') \leq D$, $R(\Gamma, A, A', *)$ и $R((\Gamma, x : A'), B, B', *)$.
\item $R(\Gamma, \Sigma (x : A) B, \Sigma (x : A') B', D)$, если \\
    $\Gamma \vdash type(\Gamma, \Sigma (x : A') B') \leq D$, $R(\Gamma, A, A', *)$ и $R((\Gamma, x : A'), B, B', *)$.
\item $R(\Gamma, Id\ A\ a_1\ a_2, Id\ A'\ a_1'\ a_2', D)$, если \\
    $\Gamma \vdash type(\Gamma, A') \leq D$, $R(\Gamma, A, A', *)$, $R(\Gamma, a_1, a_1', A')$ и $R(\Gamma, a_2, a_2', A')$.
\end{itemize}

Теперь мы введем еще два отношения: над контекстами $R_C \subseteq Ctx_I \times Ctx_B$ и над подстановками $R_S \subseteq Ctx_B \times Env_I \times Env_B \times Ctx_B$,
где $Env_I$ и $Env_B$ - множества частичных функций из $Var$ в $Term_I$ и в $Term_B$ соответственно.
\begin{itemize}
\item $R_C(\diamond, \diamond)$.
\item $R_C((\Gamma, x : A), (\Gamma', x : A'))$, если $R_C(\Gamma, \Gamma')$ и $R(\Gamma', A, A', *)$.
\end{itemize}
\begin{itemize}
\item $R_S(\Gamma, \rho, \bot, \diamond)$, если $\Gamma \vdash$, где $\bot$ - нигде неопределенная функция.
\item $R_S(\Gamma, \rho, \rho', (\Delta, y : B))$, если $R_S(\Gamma, \rho, \rho'', \Delta)$ и $R(\Gamma, \rho(y), \rho'(y), B[\rho''])$,
    где $\rho''$ - такая функция, что $\rho''(y) = \rho'(y)$ для любого $y$ в $\Delta$ и для остальных $y$ не определена.
\end{itemize}

Теперь докажем ряд свойств отношений $R$, $R_C$ и $R_S$.
\begin{lem}[rel-complete]
Верны следующие утверждения:
\begin{itemize}
\item Если $R(\Gamma, a, a', A)$, то $type(\Gamma, a')$ определено и $\Gamma \vdash type(\Gamma, a') \leq A$.
    В частности, если $A \in Term_B$, то $type(\Gamma, a') \deq A$ и $\Gamma \vdash a' \Downarrow A$,
    и если $A = *$, то $\Gamma \vdash a'$.
\item Если $R_C(\Gamma, \Gamma')$, то $\Gamma' \vdash$.
\item Если $R_S(\Gamma, \rho, \rho', \Delta)$, то $\rho' \in CT_B(\Gamma, \Delta)$.
\end{itemize}
\end{lem}
\begin{proof}
Последние два утверждения элементарно следуют из первого, а первое легко доказывается индукций по $a$.
\end{proof}

Теперь докажем функциональность этих отношений.
Если $R(\Gamma, a, a', A)$, то $a'$ не всегда однозначно определяется по $\Gamma$, $a$ и $A$, но при некаторых условиях это верно, как показывает следующая лемма:
\begin{lem}[func-strict]
Верны следующие утверждения:
\begin{itemize}
\item Пусть $a$ в нормальной форме, $R(\Gamma, a, a_1, A_1)$, $R(\Gamma, a, a_2, A_2)$ и либо $A_1 = A_2 \neq \top$, либо $a$ не является конструктором (то есть не равен $\lambda x. b$, $(b, c)$ и $refl$). Тогда $a_1 = a_2$.
\item Пусть $\Gamma$ в нормальной форме, $R_C(\Gamma, \Gamma_1)$ и $R(\Gamma, \Gamma_2)$. Тогда $\Gamma_1 = \Gamma_2$.
\item Пусть $\rho$ в нормальной форме (то есть для любого $y$ если $\rho(y)$ определено, то $\rho(y)$ в нормальной форме), $R_S(\Gamma, \rho, \rho_1, \Delta)$ и $R(\Gamma, \rho, \rho_2, \Delta)$. Тогда $\rho_1 = \rho_2$.
\end{itemize}
\end{lem}
\begin{proof}
Последние два утверждения элементарно следуют из первого, а первое легко доказывается индукций по $a$.
\end{proof}

Чтобы доказать, что отношения являются функциональными с точностью до $\deq$, нам понадобятся следующие две леммы.
\begin{lem}[subst][Лемма о подстановке] \ \\
Если $R(\Gamma, a, a', A)$ и $R(\Delta, \rho, \rho', \Gamma)$, то $R(\Delta, a[\rho], a'[\rho'], A[\rho'])$ (если $A = *$, то мы полагаем $A[\rho'] = *$).
\end{lem}
\begin{proof}
Индукцией по $a$. TODO: Написать подробнее?
\end{proof}

\begin{lem}[func-lem]
Если $\Gamma_1 \deq \Gamma_2$, $a_1 \red^* a_2$, $\Gamma_2 \vdash A_1 \leq A_2$ и $R(\Gamma_1, a_1, a_1', A_1)$, то существует $a_2'$ такой, что $a_1' \deq a_2'$ и $R(\Gamma_2, a_2, a_2', A_2)$.
\end{lem}
\begin{proof}
TODO
\end{proof}

Теперь мы можем закончить доказательство функциональности.
\begin{prop}
Верны следующие утверждения:
\begin{itemize}
\item Если $\Gamma_1 \deq \Gamma_2$, $a_1 \deq a_2$, $A_1 \deq A_2$, $R(\Gamma_1, a_1, a_1', A_1)$ и $R(\Gamma_2, a_2, a_2', A_2)$, то $a_1' \deq a_2'$.
\item Если $\Gamma_1 \deq \Gamma_2$, $R_C(\Gamma_1, \Gamma_1')$ и $R_C(\Gamma_2, \Gamma_2')$, то $\Gamma_1' \deq \Gamma_2'$.
\item Если $\Gamma_1 \deq \Gamma_2$, $\rho_1 \deq \rho_2$, $\Delta_1 \deq \Delta_2$, $R_S(\Gamma_1, \rho_1, \rho_1', \Delta_1)$ и $R_S(\Gamma_2, \rho_2, \rho_2', \Delta_2)$, то $\rho_1' \deq \rho_2'$.
\end{itemize}
\end{prop}
\begin{proof}
Последние два утверждения элементарно следуют из первого, а первое из лемм~\rlem{func-lem} и \rlem{rel-complete}.
\end{proof}

Основной шаг в доказательстве теоремы~\rthm{equiv} - это оследующее утверждение:
\begin{prop}[rel-correct]
Верны следующие утверждения:
\begin{itemize}
\item Если $\Gamma \vdash$, то существует $\Gamma'$ такой, что $R_C(\Gamma, \Gamma')$.
\item Если $\Gamma \vdash A$, то существуют $\Gamma'$ и $A'$ такие, что $R_C(\Gamma, \Gamma')$, и $R(\Gamma', A, A', *)$.
\item Если $\Gamma \vdash a : A$, то существуют $\Gamma'$, $a'$ и $A'$ такие, что $R_C(\Gamma, \Gamma')$, $R(\Gamma', A, A', *)$ и $R(\Gamma', a, a', A')$.
\item Если $\Gamma \vdash$, $\Delta \vdash$ и $\rho \in CT_I(\Gamma, \Delta)$, то существуют $\Gamma'$, $\Delta'$ и $\rho'$ такие, что $R_C(\Gamma, \Gamma')$, $R_C(\Delta, \Delta')$ и $R_S(\Gamma', \rho, \rho', \Delta')$.
\end{itemize}
\end{prop}
\begin{proof}
TODO
\end{proof}

Используя это утверждение, мы можем сконструировать функтор $G : \C_{T_I} \to \C_{T_B}$ следующим обазом.
Для любого $\Gamma \in Ctx_I$ такого, что $\Gamma \vdash$, мы определяем $G(\Gamma)$ как $\Gamma'$ такой, что $R_C(nf(\Gamma), \Gamma')$, где $nf(\Gamma)$ - нормальная форма $\Gamma$.
По утверждению~\rprop{rel-correct} такой $\Gamma'$ существует, и по лемме~\rlem{func-strict} он уникален.

Если $\rho \in \C_{T_I}(\Gamma, \Delta)$, то мы определяем $G(\rho) \in \C_{T_B}(G(\Gamma), G(\Delta))$ как $\rho'$ такой, что $R_S(G(\Gamma), \rho, \rho', G(\Delta))$.
По утверждению~\rprop{rel-correct} такой $\rho'$ существует, и по лемме~\rlem{func-lem} он уникален.
Легко убедитьтся, что $G$ сохраняет тождественные морфизмы, и из леммы~\rlem{subst} следует, что он сохраняет композиции.

Чтобы доказать, что $G$ является эквивалентностью, нам нужно понять как функтор $F : \C_{T_B} \to \C_{T_I}$, определенный в разделе~\ref{subsec:MLTT}, взаимодействует с отношениями $R$ и $R_C$.
Для этого мы докажем две простые леммы.
\begin{lem}
Если $\Gamma \vdash$, то $R_C(F(\Gamma), \Gamma)$.
Если $\Gamma \vdash a \Uparrow A$, то $R(\Gamma, F(a), a, A)$.
\end{lem}
\begin{proof}
Элементарная индукция по выводу.
TODO: подробнее?
\end{proof}

\begin{lem}
Если $R(\Gamma, a, a', A)$, то $F(a') = a$.
\end{lem}
\begin{proof}
Элементарная индукция по $a$.
\end{proof}

Теперь мы готовы доказать основной результат.
\begin{thm}[equiv]
Функтор $F : \C_{T_B} \to \C_{T_I}$, определенный в разделе~\ref{subsec:MLTT}, и $G : \C_{T_I} \to \C_{T_B}$ задают эквивалентность категорий.
\end{thm}
\begin{proof}
Естественные эквивалентности $\alpha_\Gamma : \Gamma \to G(F(\Gamma)$ и $\beta_\Delta : \Delta \to F(G(\Delta))$ задаются условиями $\alpha_\Gamma(x) = x$ и $\beta_\Delta(x) = x$ для любого $x$.
TODO: закончить.
\end{proof}

\bibliographystyle{amsplain}
\bibliography{ref}

\end{document}