rus.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}{определение}{Определение}
\newref{example}{пример}{Пример}

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

\newcommand{\cat}[1]{\mathbf{#1}}
\renewcommand{\C}{\cat{C}}
\newcommand{\bs}{\beta\sigma}
\newcommand{\ebs}{=_{\bs}}
\newcommand{\rbs}{\to_{\bs}}
\newcommand{\bst}{\bs\tau}
\newcommand{\ebst}{=_{\bst}}
\newcommand{\rbst}{\to_{\bst}}
\newcommand{\sSet}{\cat{sSet}}
\renewcommand{\ll}{\llbracket}
\newcommand{\rr}{\rrbracket}

\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{Гомотопическая теория типов с типом интервала}

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

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

\maketitle

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

\section{Синтаксис}

В данном разделе мы приведем правила вывода для базовой системы.
Позже мы расширим их индуктивными типами данных и записями с условиями.

\centerAlignProof

\begin{table}

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

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\RightLabel{, $\kappa' < \kappa \in \mathbb{N}$}
\UnaryInfC{$\Gamma \vdash U_{\kappa'} : U_\kappa$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash A : U_{\kappa'}$}
\RightLabel{, $\kappa' < \kappa$}
\UnaryInfC{$\Gamma \vdash A : U_\kappa$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash A : U_\kappa$}
\UnaryInfC{$\Gamma \vdash A$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash a : A$}
\AxiomC{$\Gamma \vdash B$}
\RightLabel{, $A =_{\beta \sigma \tau} B$}
\BinaryInfC{$\Gamma \vdash a : B$}
\DisplayProof
\end{center}

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

\medskip
\begin{center}
\AxiomC{$\Gamma, x : A \vdash b : B$}
\UnaryInfC{$\Gamma \vdash \lambda x. b : \Pi (x : A) B$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash f : \Pi (x : A) B$}
\AxiomC{$\Gamma \vdash a : A$}
\BinaryInfC{$\Gamma \vdash f\ a : B[x := a]$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash I : U_\kappa$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash left : I$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash right : I$}
\DisplayProof
% \quad
% \AxiomC{$\Gamma \vdash i : I$}
% \AxiomC{$\Gamma \vdash j : I$}
% \BinaryInfC{$\Gamma \vdash squeeze\ i\ j : I$}
% \DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, x : I \vdash A$}
\AxiomC{$\Gamma \vdash i : I$}
\AxiomC{$\Gamma \vdash a : A[x := i]$}
\AxiomC{$\Gamma \vdash j : I$}
\QuaternaryInfC{$\Gamma \vdash coe_{\lambda x. A}\ i\ a\ j : A[x := j]$}
\DisplayProof
\end{center}

\begin{comment}
\medskip
\begin{center}
\AxiomC{$\Gamma, x : I \vdash A$}
\AxiomC{$\Gamma \vdash a : A[x := i]$}
\AxiomC{$\Gamma \vdash i : I$}
\AxiomC{$\Gamma \vdash j : I$}
\QuaternaryInfC{$\Gamma \vdash lift_{\lambda x. A}\ i\ a\ j : A[x := j]$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\def\extraVskip{1pt}
\Axiom$\fCenter \Gamma \vdash i : I$
\noLine
\UnaryInf$\fCenter \Gamma \vdash j : I$
\Axiom$\fCenter \Gamma \vdash a : \Pi (y : I) A$
\noLine
\UnaryInf$\fCenter \Gamma \vdash a' : \Pi (y : I) A$
\noLine
\UnaryInf$\fCenter \Gamma \vdash f : I \to A[y := i]$
\def\extraVskip{2pt}
\RightLabel{, $a\ i =_\beta f\ left$, $f\ right =_\beta a'\ i$}
\BinaryInfC{$\Gamma \vdash fill_{\lambda y. A}\ a\ a'\ i\ f\ j : I \to A[y := j]$}
\DisplayProof
\end{center}
\end{comment}

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

Главное нововведение данной системы - это тип интервала $I$.
У него есть два конструктора ($left$ и $right$) и одно правило элиминации ($coe$).
% Также мы определили функцию $squeeze$, которая нам понадобится позже для определения элиминатора для типа путей $J$.

Правила редукции:
\begin{itemize}
\item $(\lambda x.b)\ a \to_\beta b[x := a]$
% \item $squeeze\ left\ j \to_\beta left$
% \item $squeeze\ right\ j \to_\beta j$
% \item $squeeze\ i\ left \to_\beta left$
% \item $squeeze\ i\ right \to_\beta i$
% \item $coe_{\lambda k.A}\ left\ a\ left \to_\beta a$
% \item $coe_{\lambda k.A}\ right\ a\ right \to_\beta a$
\item $coe_{\lambda k.A}\ i\ a\ i \to_\beta a$
\item $coe_{\lambda k.A}\ i\ a\ j \to_\sigma a$, если $k \notin FV(A)$
\end{itemize}

% Первое правило - обычныая $\beta$-редукцию для лямбда-термов.
% Следующие четыре правила описывают поведение функцию $squeeze$, таким образом она определяет ретракцию квадрата на отрезок.

Поведение элиминатора $coe$ можно описать следующим образом:
по расслоению $\lambda x. A$ над $I$ и по точке $a$ в слое над некоторой точкой $i$ интервала $coe_{\lambda x. A}\ i\ a$ конструирует сечение этого расслоения.
% Первые два правила редукции для $coe$ говорят, что это сечение в точке $i$ возвращает $a$ (при $i$ равном $left$ и $right$).
Первое правило редукции для $coe$ говорит, что это сечение в точке $i$ возвращает $a$.
Последнее правило говорит, что есть расслоение тривиально, то сечение константно.
Оно необходимо для того, чтобы $J$ удовлетворяло обычному правилу редукции для него.
Без $\sigma$-правила для это будет верно только с точностью до эквивалетности, то есть мы всегда можем найти путь между $coe_{\lambda. A}\ i\ a\ j$ и $a$.
Это правило несколько отличается от остальных правил редукций и не является настолько же важным, поэтому мы обозначаем его другой буквой.

Одно из важных свойств систем типов, которое нам понадобится, - это свойство \emph{каноничности}.
Мы будем говорить, что система обладает этим свойством, если все замкнутые термы в нормальной форме имеют канонический вид,
    то есть являются конструктором, возможно примененным к аргументам.
Система, описаная выше, не обладает этим свойством.
Чтобы исправить эту проблему, мы добавим еще больше правил редукции.
Нам нужно добавить $\tau$-правило для каждого типа в системе.
Пока единственный тип у нас - это $\Pi$-тип, так что мы добавляем одно правило:
\[ coe_{\lambda k. \Pi (a : A) B}\ i\ (\lambda a. b)\ j \to_\tau \lambda a'. coe_{\lambda k. B[a := coe_{\lambda k. A}\,j\,a'\,k]}\ i\ (b[a := coe_{\lambda k. A}\ j\ a'\ i])\ j \]

Теперь мы сформулируем несколько стандартных мета-теоретических свойств системы.
Все доказательства стандартны, поэтому мы будем приводить в основном только их наброски.
Начнем со следующего простого утверждения, которое говорит, что типизация замкнута относительно редукций.
\begin{prop}
Пусть $A_1 \rbst A'_1$, \ldots $A_n \rbst A'_n$, $A \rbst A'$ и $a \rbst a'$.
Тогда верны следующие утверждения:
\begin{itemize}
\item Если $x_1 : A_1, \ldots x_n : A_n \vdash$, то $x_1 : A'_1, \ldots x_n : A'_n \vdash$.
\item Если $x_1 : A_1, \ldots x_n : A_n \vdash A$, то $x_1 : A'_1, \ldots x_n : A'_n \vdash A'$.
\item Если $x_1 : A_1, \ldots x_n : A_n \vdash a : A$, то $x_1 : A'_1, \ldots x_n : A'_n \vdash a' : A'$.
\end{itemize}
\end{prop}
\begin{proof}
Единственный интересный случай - это $coe$.
Для $\beta$ и $\sigma$ правил всё просто.
Для доказательтсва $\tau$ правила нужно использовать $\beta$ правило.
Именно поэтому $\beta$ правило для $coe$ определено для всех $i$, а не только для $left$ и $right$.
\end{proof}

Теперь мы докажем, что отношение $\rbst$ \emph{конфлюентно}.
Это свойство говорит, что если $t \rbst q$ и $t \rbst r$, то существует терм $s$ такой, что $q \rbst s$ и $r \rbst s$.
Доказательство в основном стандартно, единственный не очевидный момент - это правила для $coe$, но не сложно адаптировать доказательство и для них.
Во-первых, мы введем новое отношение редукции $\to_p$, которое определяется индуктивно:
\begin{itemize}
\item $t \to_p t$.
\item Если $b \to_p b'$ и $a \to_p a'$, то $(\lambda x. b)\ a \to_p b'[x := a']$.
% \item $squeeze\ left\ j \to_p left$.
% \item Если $j \to_p j'$, то $squeeze\ right\ j \to_p j'$.
% \item $squeeze\ i\ left \to_p left$.
% \item Если $i \to_p i'$, то $squeeze\ i\ right \to_p i'$.
\item Если $a \to_p a'$ и $i \ebst j$, то $coe_{\lambda k. A}\ i\ a\ j\ \to_p a'$.
\item Если $a \to_p a'$ и $k \notin FV(A)$, то $coe_{\lambda k. A}\ i\ a\ j\ \to_p a'$.
\item Если $A \to_p A'$, $B \to_p B'$, $i \to_p i'$, $b \to_p b'$ и $j \to_p j'$, то
    \[ coe_{\lambda k. \Pi (a : A) B}\ i\ (\lambda a. b)\ j \to_p \lambda a'. coe_{\lambda k. B'[a := coe_{\lambda k. A'}\,j'\,a'\,k]}\ i'\ (b'[a := coe_{\lambda k. A'}\ j'\ a'\ i'])\ j' \]
\item Если $f \to_p f'$ и $a \to_p a'$, то $f\ a \to_p f'\ a'$.
\item Если $a \to_p a'$, то $\lambda x. a \to_p \lambda x. a'$.
\item Если $A \to_p A'$ и $B \to_p B'$, то $\Pi (a : A) B \to_p \Pi (a : A') B'$.
% \item Если $i \to_p i'$ и $j \to_p j'$, то $squeeze\ i\ j \to_p squeeze\ i'\ j'$.
\item Если $A \to_p A'$, $i \to_p i'$, $a \to_p a'$ и $j \to_p j'$, то $coe_{\lambda x. A}\ i\ a\ j \to_p coe_{\lambda x. A'}\ i'\ a'\ j'$.
\end{itemize}

Теперь мы хотим показать, что $\to_p$ конфлюентно.
Чтобы доказать часть с $\beta$-редукцией для лямбда-термов, нам потребуются следующая лемма.

\begin{lem}
Если $b \to_p b'$ и $a \to_p a'$, то $b[x := a] \to_p b'[x := a']$.
\end{lem}
\begin{proof}
Простая индукция по определению $b \to_p b'$.
В случае $b \to_p b$ мы продолжаем индукцией по построению терма $b$.
\end{proof}

\begin{lem}
Отношение $\to_p$ конфлюентно.
\end{lem}
\begin{proof}
Пусть $b \to_p b'$ и $b \to_p b''$.
Нужно показать, что существует терм $c$ такой, что $b' \to_p c$ и $b'' \to_p c$.
Мы делаем это индукцией по определению отношений $b \to_p b'$ и $b \to_p b''$.
Большинство пунктов элементарно.
Для случая $(\lambda x. b)\ a \to_p b'[x := a']$ мы используем предыдущую лемму.
Для случая $coe_{\lambda k. A}\ i\ a\ j \to_p a'$ когда $i \ebst j$ мы используем тот факт, что $t \to_p s$ влечет $t \ebst s$.

TODO: Написать подробнее?
\end{proof}

\begin{prop}
Отношение $\rbst$ конфлюентно.
\end{prop}
\begin{proof}
Это следует из предыдущей леммы и того факта, что транзитивное замыкание $\to_p$ совпадает с $\rbst$.
\end{proof}

\begin{remark}
Отношение $\rbs$ также конфлюентно.
Доказательство этого факта аналогично доказательству предыдущего с тем отличием, что в определении $\to_p$ нужно опустить правило, касающееся $\tau$.
\end{remark}

Теперь докажем, что система обладает свойством каноничности.

\begin{prop}
Пусть $\Gamma$ - это контекст вида $x_1 : I, \ldots x_n : I$.
Тогда верны следующие утверждения:
\begin{itemize}
\item Если $A$ - терм в нормальной форме, и верно $\Gamma \vdash A$, то $A$ равен либо $I$, либо $U_\kappa$, либо $\Pi$-типу.
\item Пусть $a$ - терм в нормальной форме, и верно $\Gamma \vdash a : A$.
    Тогда если $A \ebst U_\kappa$, то $a$ равен либо $I$, либо $U_{\kappa'}$, либо $\Pi$-типу.
    Если $A$ $\bst$-эквивалентно $\Pi$-типу, то $a$ имеет вид $\lambda x. a'$.
\end{itemize}
\end{prop}
\begin{proof}
Доказательство индукцией по выводу.
Случай $\Gamma \vdash x : A$, где $x$ - переменная, следует из конфлюентности.
Единственный интересный случай - это правило для $coe$.
По предположению индукции $A$ является либо вселенной, либо типом интервала, либо $\Pi$-типом.
Но тогда терм не находится в нормальной форме, так как в первых двух случаях он редуцируется по $\sigma$-правилу, а во втором по $\tau$-правилу.
\end{proof}

\begin{cor}
Описанная система с $\bst$-правилами редукций обладает свойством каноничности.
\end{cor}

Теперь мы докажем \emph{сильную нормализуемость}.
Мы говорим, что терм сильно нормализуем, если не существует бесконечной последовательности редукций, начинающейся с этого терма.
Мы говорим, что теория сильно нормализуема, если $\Gamma \vdash A$ влечет, что $A$ сильно нормализуем, и $\Gamma \vdash a : A$ влечет, что $a$ сильно нормалиуем.

Для доказательства сильной нормализуемости нам понадобится понятие \emph{насыщенного} множества.
Множество сильно нормализуемых термов мы будем обозначать $SN$.
Если терм $t$ $\bst$-редуцируется к $s$ за один шаг, мы будем писать $t \to_1 s$.
Множество термов $s$, к которым $t$ редуцируется за один шаг, мы будем обозначать $red_1(t)$ (то есть $red_1(t) = \{ s\ |\ t \to_1 s \}$).
Термы, которые не являются ни абстракцией, ни $\Pi$-типом, мы будем называть \emph{простыми}, и множество простых термов обозначать $S$.
Мы будем говорить, что множество термов $X$ насыщенно, если выполнены следующие условия:
\begin{description}
\item[(SAT1)] $X \subseteq SN$.
\item[(SAT2)] Если $t \in X$ и $t \to_1 s$, то $s \in X$.
\item[(SAT3)] Если $t \in S$, и $red_1(t)$ является подмножеством $X$, то $t \in X$.
\end{description}

Условие \textbf{(SAT3)}, в частности, означает, что любой простой терм в нормальной форме должен принадлежать $X$.
В частности, все переменные принадлежат $X$, следовательно $X$ не пусто.
Если $X \subseteq SN$, то существует минимальное насыщенное множество, содержащее $X$.
Мы называем это множество насыщением $X$ и обозначаем $sat(X)$.

Чтобы доказать сильную нормализуемость, мы введем частичные функции $\ll - \rr_\kappa : Term \to SAT$ для всех $\kappa \in \mathbb{N}$,
    где $Term$ - множество термов, а $SAT$ - множество насыщенных подмножеств $Term$.
Для этого мы сначала определим их графики $G_\kappa \subseteq Term \times SAT$ индуктивным образом.

\medskip
\begin{center}
\AxiomC{$(t,A) \in G_\kappa$}
\RightLabel{, если $t \to_1 s$}
\UnaryInfC{$(s,A) \in G_\kappa$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\forall s \in red_1(t)\ (s,A) \in G_\kappa$}
\RightLabel{, если $t \in S$, и $red_1(t)$ не пусто}
\UnaryInfC{$(t,A) \in G_\kappa$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{}
\RightLabel{, если $t \in S$, и $red_1(t)$ пусто}
\UnaryInfC{$(t,SN) \in G_\kappa$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{}
\UnaryInfC{$(I, sat(\{left, right\})) \in G_\kappa$}
\DisplayProof
\quad
\AxiomC{}
\RightLabel{, $\kappa' < \kappa$}
\UnaryInfC{$(U_{\kappa'}, Type_{\kappa'}) \in G_\kappa$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$(t,A) \in G_\kappa$}
\AxiomC{$\forall a \in A\ (s[x := a], B_a) \in G_\kappa$}
\BinaryInfC{$(\Pi (x : t) s, \{ f\ |\ \forall a \in A\ (f\ a \in B_a)\}) \in G_\kappa$}
\DisplayProof
\end{center}
\medskip

Индукцией по построению $G_\kappa$ не сложно показать, что если $t \ebst s$, $(t,A) \in G_\kappa$ и $(s,A') \in G_\kappa$, то $A = A'$.
Следовательно $G_\kappa$ действительно ялвяется графиком частичной функции $\ll - \rr_\kappa : Term \to SAT$.
Множество $Type_\kappa \subseteq Term$ определяется как множество тех термов, на которых $\ll - \rr_\kappa$ определена.
Индукцией по построению $G_\kappa$ не сложно показать, что $Type_\kappa \subseteq SN$, откуда следует, что $Type_\kappa$ насыщено.
Несложно показать, что $Type_{\kappa'} \subseteq Type_\kappa$, если $\kappa' < \kappa$,
    и функции $\ll - \rr_{\kappa'}$ и $\ll - \rr_\kappa$ совпадают на аргументах, на которых они обе определены.
Мы определяем $Type \subseteq Term$ как объединение всех $Type_\kappa$, и функцию $\ll - \rr : Type \to SAT$ как $\ll t \rr = \ll t \rr_\kappa$ для достаточно большого $\kappa$.

Для заключительной части доказательства нам понадобится еще одно понятие.
\emph{Означивание} - это частичная функцию из множества переменных в множество термов.
Означивание, которое нигде не определено, мы обозначаем $\varnothing$.
Если $\rho$ - означивание, и $t$ - терм, то $\rho[x := t]$ - это означивание, которое на $x$ возвращает $t$ и на остальных переменных определено также как и $\rho$.
Если $\rho$ - означивание, и $t$ - терм, то $t[\rho]$ - это терм, который определяется как
    $t[x_1 := \rho(x_1), \ldots x_n := \rho(x_n)]$, где $\{x_1, \ldots x_n$\} - домен $\rho$.
Если $\rho$ - означивание, и $X$ - множество термов, то $X[\rho] = \{ t[\rho]\ |\ t \in X \}$.

Теперь мы докажем простую техническую лемму.

\begin{lem}[nat-of-int]
Пусть $A \in Type_\kappa$.
Тогда для любой инволюции $\varphi$ (то есть такого означивания, что для любого терма $t$ верно $t[\varphi][\varphi] = t$)
верно, что $A[\varphi] \in Type_\kappa$, и $\ll A[\varphi] \rr_\kappa = \ll A \rr_\kappa [\varphi]$.
\end{lem}
\begin{proof}
Индукцией по построению $(A, \ll A \rr_\kappa) \in G_\kappa$.
Первые четыре случая легко следуют из того факта, что $A' \to_1 A$ влечет $A'[\varphi] \to_1 A[\varphi]$ для любого означивания $\varphi$.
Откуда следует, что для любой инволюции $\varphi$ верно, что $red_1(A[\varphi]) = red_1(A)[\varphi]$, $SN[\varphi] = SN$, и $sat(X[\varphi]) = sat(X)[\varphi]$.

Последний случай:
\begin{center}
\AxiomC{$(A, \ll A \rr_\kappa) \in G_\kappa$}
\AxiomC{$\forall a \in \ll A \rr_\kappa \ (B[x := a], \ll B[x := a] \rr_\kappa) \in G_\kappa$}
\BinaryInfC{$(\Pi (x : A) B, \{ f\ |\ \forall a \in \ll A \rr_\kappa\ (f\ a \in \ll B[x := a] \rr_\kappa)\}) \in G_\kappa$}
\DisplayProof
\end{center}
По индукционной гипотезе мы знаем, что $(A[\varphi], \ll A \rr_\kappa [\varphi]) \in G_\kappa$, и $\forall a \in \ll A \rr_\kappa\ (B[x := a][\varphi], \ll B[x := a] \rr_\kappa [\varphi]) \in G_\kappa$.
Так как $B[x := a][\varphi] = B[\varphi][x := a[\varphi]]$, то последнее выражение можно переписать как
    $\forall a \in \ll A \rr_\kappa [\varphi]\ (B[\varphi][x := a], \ll B[x := a[\varphi]] \rr_\kappa [\varphi]) \in G_\kappa$.
Откуда получаем, что \[ ((\Pi (x : A) B)[\varphi], \{ f\ |\ \forall a \in \ll A \rr_\kappa [\varphi]\ (f\ a \in \ll B[x := a[\varphi]] \rr_\kappa [\varphi]) \}) \in G_\kappa \].
Таким образом $(\Pi (x : A) B)[\varphi] \in Type_\kappa$.
Осталось убедиться, что множество, описанное выше, совпадает с множеством $\{ f[\varphi]\ |\ \forall a \in \ll A \rr_\kappa\ (f\ a \in \ll B[x := a] \rr_\kappa) \}$.
Это легко следует из того факта, что $\varphi$ - инволюция.
\end{proof}

Так как множество переменных бесконечно, то его можно разбить на два бесконечных непересекающихся равномощных подмножества $Var$ и $Var'$.
Мы будем предполагать, что в правилах вывода учавствуют только переменные из $Var$.
Теперь мы определим частичную функцию $\ll - \rr$ из множества контекстов в множество подмножеств множества означиваний:
\[ \ll \varnothing \rr = \{ \varnothing \} \]
\[ \ll \Gamma, x : A \rr = \{ \rho[x := a]\ |\ \rho \in \ll \Gamma \rr, a \in \ll A[\rho] \rr, FV(a) \subseteq dom(\rho) \cup \{ x \} \cup Var' \} \]
Причем, мы считаем, что $\ll \Gamma, x : A \rr$ определено тогда и только тогда,
    когда $\ll \Gamma \rr$ определено, и для любого $\rho \in \ll \Gamma \rr$ верно, что $A[\rho] \in Type$.

\begin{prop}[sn]
Верны следующие утверждения:
\begin{itemize}
\item Если $\Gamma \vdash$, то $\ll \Gamma \rr$ определено.
\item Если $\Gamma \vdash A$, то $\ll \Gamma \rr$ определено, и для любого $\rho \in \ll \Gamma \rr$ верно, что $A[\rho] \in Type$.
\item Если $\Gamma \vdash a : A$, то $\ll \Gamma \rr$ определено,
    и для любого $\rho \in \ll \Gamma \rr$ верно, что $A[\rho] \in Type$, и $a[\rho] \in \ll A[\rho] \rr$.
\end{itemize}
\end{prop}
\begin{proof}
Индукцией по выводу.
\begin{itemize}
\item Случаи
\begin{center}
\AxiomC{}
\UnaryInfC{$\varnothing \vdash$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash A$}
\RightLabel{, $x \notin \Gamma$}
\UnaryInfC{$\Gamma, x : A \vdash$}
\DisplayProof
\end{center}
следуют из определения $\ll - \rr$ для контекстов.

\item Случай
\begin{center}
\AxiomC{$\Gamma \vdash$}
\RightLabel{, $x : A \in \Gamma$}
\UnaryInfC{$\Gamma \vdash x : A$}
\DisplayProof
\end{center}
Мы знаем, что $\Gamma = \Gamma', x : A, \Gamma''$.
Если $\rho \in \ll \Gamma \rr$, то $A[\rho]$ = $A[\rho|_{\Gamma'}]$, т.к. в $A$ не встречаются свободные переменные из $x : A, \Gamma''$.
Так как $\ll \Gamma \rr$ опеделено, то $\ll \Gamma', x : A \rr$ также определено,
    следовательно $A[\rho|_{\Gamma'}] \in Type$ и $\rho(x) \in \ll A[\rho|_{\Gamma'}] \rr$, что и требовалось.

\item Случай
\begin{center}
\AxiomC{$\Gamma \vdash a : A$}
\AxiomC{$\Gamma \vdash B$}
\RightLabel{, $A =_{\beta \sigma \tau} B$}
\BinaryInfC{$\Gamma \vdash a : B$}
\DisplayProof
\end{center}
Так как $\ll A[\rho] \rr$ и $\ll B[\rho] \rr$ определены, и $A[\rho] \ebst B[\rho]$, то $\ll A[\rho] \rr = \ll B[\rho] \rr$.
Следовательно $a[\rho] \in \ll A[\rho] \rr = \ll B[\rho] \rr$.

\item Случай
\begin{center}
\AxiomC{$\Gamma \vdash A : U_\kappa$}
\AxiomC{$\Gamma, x : A \vdash B : U_\kappa$}
\BinaryInfC{$\Gamma \vdash \Pi (x : A) B : U_\kappa$}
\DisplayProof
\end{center}
Пусть $\rho \in \ll \Gamma \rr$. Нам нужно показать, что $(\Pi (x : A) B)[\rho] \in Type_\kappa$.
Для этого достаточно показать, что для любого $a \in \ll A[\rho] \rr_\kappa$ верно, что $B[\rho][x := a] = B[\rho[x := a]] \in Type_\kappa$.
По индукционной гипотезе мы знаем, что если $FV(a) \subseteq dom(\rho) \cup \{ x \} \cup Var'$, то это верно.
Пусть теперь $a$ - произвольный, и пусть $V = FV(a) \setminus dom(\rho) \cup \{ x \} \cup Var'$.
Так как $V$ - конечное множество, то мы можем выбрать $V' \subseteq Var'$ равномощное $V$.
Теперь мы можем определить означивание $\phi$, которое каждой переменной из $V$ сопоставляет соответствующую переменную из $V'$ и наоборот.
Таким образом, $\phi$ - инволюция.

По лемме~\rlem{nat-of-int} мы знаем, что $a[\varphi] \in \ll A[\rho][\varphi] \rr_\kappa$, но $A[\rho][\varphi] = A[\rho]$, так как $\varphi$ не меняет свободные переменные $A[\rho]$.
По построению $FV(a[\varphi]) \subseteq dom(\rho) \cup \{ x \} \cup Var'$, следовательно $B[\rho][x := a[\varphi]] \in Type_\kappa$.
Но $B[\rho][x := a[\varphi]] = B[\rho][x := a][\varphi]$, следовательно $B[\rho][x := a] \in Type_\kappa$ по лемме~\rlem{nat-of-int}, что и требовалось показать.

\item Случай
\begin{center}
\AxiomC{$\Gamma \vdash A$}
\AxiomC{$\Gamma, x : A \vdash B$}
\BinaryInfC{$\Gamma \vdash \Pi (x : A) B$}
\DisplayProof
\end{center}
аналогичен предыдущему.

\item Случай
\begin{center}
\AxiomC{$\Gamma, x : A \vdash b : B$}
\UnaryInfC{$\Gamma \vdash \lambda x. b : \Pi (x : A) B$}
\DisplayProof
\end{center}
Мы должны показать, что для любых $\rho \in \ll \Gamma \rr$ и $a \in \ll A[\rho] \rr$ верно, что $(\lambda x. b[\rho]) a \in \ll B[\rho][x := a] \rr$.
По индукционной гипотезе мы знаем, что если $FV(a) \subseteq dom(\rho) \cup \{ x \} \cup Var'$, то $b[\rho][x := a] \in \ll B[\rho][x := a] \rr$.
Так как $b[\rho]$ и $a$ сильно нормализуемы, то в любой достаточно длинной последовательности редукций, начинающейся с $(\lambda x. b[\rho]) a$ внешний редекс будет сокращен.
При этом мы получим терм к которому редуцируется $b[\rho][x := a]$, следовательно по \textbf{(SAT2)} он лежит в $\ll B[\rho][x := a] \rr$.
Так как любая последовательность редукций заканчивается термами в $\ll B[\rho][x := a] \rr$, то \textbf{(SAT3)} влечет, что $(\lambda x. b[\rho]) a$ сам принадлежит этому множеству.

Теперь, если $a$ произвольный, то мы выбираем инволюцию $\varphi$ также как в предыдущем пункте.
Тогда $a[\varphi] \in \ll A[\rho] \rr$, и, как мы только что видели, $(\lambda x. b[\rho]) (a[\varphi]) \in \ll B[\rho][x := a[\varphi]] \rr$.
Так как $(\lambda x. b[\rho]) (a[\varphi]) = ((\lambda x. b[\rho]) a)[\varphi]$, и $B[\rho][x := a[\varphi]] = B[\rho][x := a][\varphi]$, то
    по лемме~\rlem{nat-of-int} $(\lambda x. b[\rho]) a \in \ll B[\rho][x := a] \rr$, что и требовалось показать.

\item Случай
\begin{center}
\AxiomC{$\Gamma \vdash f : \Pi (x : A) B$}
\AxiomC{$\Gamma \vdash a : A$}
\BinaryInfC{$\Gamma \vdash f\ a : B[x := a]$}
\DisplayProof
\end{center}
Пусть $\rho \in \ll \Gamma\rr$.
По индукционной гипотезе мы знаем, что $f[\rho]\ a[\rho] \in \ll B[\rho][x := a[\rho]] \rr$.
Но $B[\rho][x := a[\rho]] = B[x := a][\rho]$, следовательно $(f\ a)[\rho] \in \ll B[x := a][\rho]\rr$, что и требовалось показать.

\item Случаи
\begin{center}
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash I : U_\kappa$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash left : I$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash right : I$}
\DisplayProof
\end{center}

\begin{center}
\AxiomC{$\Gamma \vdash$}
\RightLabel{, $\kappa' < \kappa$}
\UnaryInfC{$\Gamma \vdash U_{\kappa'} : U_\kappa$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash A : U_{\kappa'}$}
\RightLabel{, $\kappa' < \kappa$}
\UnaryInfC{$\Gamma \vdash A : U_\kappa$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash A : U_\kappa$}
\UnaryInfC{$\Gamma \vdash A$}
\DisplayProof
\end{center}
элементарны.

\item Случай
\begin{center}
\AxiomC{$\Gamma, x : I \vdash A$}
\AxiomC{$\Gamma \vdash i : I$}
\AxiomC{$\Gamma \vdash a : A[x := i]$}
\AxiomC{$\Gamma \vdash j : I$}
\QuaternaryInfC{$\Gamma \vdash coe_{\lambda x. A}\ i\ a\ j : A[x := j]$}
\DisplayProof
\end{center}
Пусть $\rho \in \ll \Gamma \rr$.
Сначала мы покажем, что $A[x := j][\rho] \in Type$.
Действительно, $A[x := j][\rho] = A[\rho][x := j[\rho]] = A[\rho[x := j[\rho]]]$, и это множество принадлежит $Type$ по индукционной гипотезе.

Теперь мы должны доказать, что $(coe_{\lambda x. A}\ i\ a\ j)[\rho] \in \ll A[x := j][\rho] \rr$.
Мы сделаем это индукцией по выводу $\Gamma, x : I \vdash A$.
Конкретно, мы докажем следующее утверждение.
Пусть $\Gamma, x : I, z_1 : Z_1, \ldots z_n : Z_n \vdash A$, и дерево вывода для него является поддеревом вывода
    $\Gamma, x : I \vdash A$ (чтобы мы смогли использовать условие утверждения~\rprop{sn} для него).
Пусть $i_1, j_1 \in \ll I \rr$ такие, что $FV(i_1) \cup FV(j_1) \subseteq dom(\rho) \cup Vars'$.
Пусть $t_1, \ldots t_n$ - такая последовательность термов, что $FV(t_i) \subseteq dom(\rho) \cup \{ x, z_1, \ldots z_n \} \cup Vars'$, и
$\rho[x := k][z_1 := t_1[x := k]] \ldots [z_n := t_n[x := k]] \in \ll \Gamma, x : I, z_1 : Z_1, \ldots z_n : Z_n \rr$, где $k \in \{ i_1, j_1 \}$.
Мы будем обозначать это означивание $\rho_i$ при $k = i_1$ и $\rho_j$ при $k = j_1$, а также мы будем писать $\rho_x$ при $k = x$.
Тогда если $a_1 \in \ll A[\rho_i] \rr$, то $coe_{\lambda x. A[\rho_x]}\ i_1\ a_1\ j_1 \in \ll A[\rho_j] \rr$.

По аргументу, аналогичному тому, который мы приводили в случае аппликации, нам достаточно показать,
    что $\beta$, $\sigma$ и $\tau$ редукции для $coe$ переводят $coe_{\lambda x. A[\rho_x]}\ i_1\ a_1\ j_1$ в терм, лежащий в множестве $\ll A[\rho_j] \rr$.
Случаи $\beta$ и $\sigma$ редукций не представляют проблем, так как они сразу же следуют из того факта, что $a_1 \in \ll A[\rho_i] \rr$, и в обоих случаях $A[\rho_i] = A[\rho_j]$.
Пусть теперь $coe_{\lambda x. \Pi (a : A[\rho_x]) B[\rho_x]}\ i_1\ (\lambda a. b_1)\ j_1$ редуцируется по $\tau$-правилу к
    $\lambda a'. coe_{\lambda x. B[\rho_x][a := coe_{\lambda x. A[\rho_x]}\,j_1\,a'\,x]}\ i_1\ (b_1[a := coe_{\lambda x. A[\rho_x]}\ j_1\ a'\ i_1])\ j_1$.
Обозначим этот терм за $f$.

Мы должны показать, что $f$ принадлежит $\ll (\Pi (a : A) B)[\rho_j] \rr = \ll \Pi (a : A[\rho_j]) B[\rho_j]\rr$.
Для этого достаточно показать, что для любого $a_2 \in \ll A[\rho_j] \rr$ верно, что $f\,a_2 \in \ll B[\rho_j][a := a_2] \rr$,
    при этом мы можем предположить, что $FV(a_2) \subseteq dom(\rho) \cup \{ z_1, \ldots z_n \} \cup Vars'$, используя аргумент аналогичный тому, который мы применяли в случае абстракции.
По индукционной гипотезе $coe_{\lambda x. A[\rho_x]}\ j_1\ a_2\ i_1 \in \ll A[\rho_i] \rr$.
Также мы знаем, что $\lambda a. b_1 \in \Pi (a : A[\rho_i]) B[\rho_i]$,
    следовательно $b_1[a := coe_{\lambda x. A[\rho_x]}\ j_1\ a_2\ i_1] \in B[\rho_i][a := coe_{\lambda x. A[\rho_x]}\ j_1\ a_2\ i_1]$.
Обозначим этот терм за $b_2$.

Теперь нам нужно применить индукционную гипотезу для терма $coe_{\lambda x. B[\rho_x][a := coe_{\lambda x. A[\rho_x]}\,j_1\,a_2\,x]}\ i_1\ b_2\ j_1$.
Для этого возьмем $z_{n+1} = a$, $Z_{n+1} = A$ и $t_{n+1} = coe_{\lambda x. A[\rho_x]}\ j_1\ a_2\ x$.
Тогда мы получим, что этот терм, а следовательно и $f\,a_2$ принадлежит $\ll B[\rho_j][a := coe_{\lambda x. A[\rho_x]}\,j_1\,a_2\,j_1] \rr$.
Так как термы $B[\rho_j][a := coe_{\lambda x. A[\rho_x]}\,j_1\,a_2\,j_1]$ и $B[\rho_j][a := a_2]$ $\beta$-эквивалентны,
    то $f\,a_2 \in \ll B[\rho_j][a := a_2] \rr$, что и требовалось доказать.

\end{itemize}
\end{proof}

\begin{cor}
Система сильно нормализуема.
\end{cor}
\begin{proof}
Действительно, достаточно в качестве $\rho$ в условии утверждения взять тривиальное означивание, которое каждую $x$ из $\Gamma$ отображает в $x$.
\end{proof}

\section{Типы данных и записи с условиями}

В этом разделе мы расширим вселенную новыми конструкциями.
Мы позволяем определять произвольные типы данных, и для того чтобы описать правила типизации, нам нужно ввести понятие сигнатуры.
Сигнатура $\Sigma$ - это последовательность объявлений $D_1, \ldots D_n$, где каждый из $D_i$ - объявление типа данных, записи или функции.

Объявление функции состоит из следующего набора данных:
\begin{itemize}
\item Имя функции вместе с ее типом $f : \Pi (a_1 : A_1) \ldots \Pi (a_n : A_n) \to B$.
\item Список правил редукций для $f$. Позже мы опишем как должны выглядеть эти правила редукций.
\end{itemize}

Объявленние типа данных состоит из следующего набора данных:
\begin{itemize}
\item Имя типа данных $D$ и его размер $\kappa \in \mathbb{N}$.
\item Контекст $x_1 : A_1, \ldots x_n : A_n$, задающий параметры $D$.
\item Список конструкторов $c_i$ и контекст для каждого конструктора $y_1 : C_1, \ldots y_k : C_k$, задающий типы аргументов $c_i$.
    В этом случае мы будем говорить, что $\Pi (y_1 : C_1) \ldots \Pi (y_k : C_k) (D\ x_1\ \ldots\ x_n)$ - это тип конструктора $c_i$.
    Мы требуем, чтобы определение типа данных должно быть строго положительным.
    Другими словами, каждый из $C_j$ должен иметь вид $\Pi (e_1 : E_1) \ldots \Pi (e_m : E_m) \to F\ (D\ a_1 \ldots a_n)$, и $D \notin FV(E_i)$ для всех $i$.
    Здесь $F$ должна быть строго положительной функцией.
    Мы не будем описывать как проверить это условие синтаксически в общем случае, лишь скажем, что примеры таких $F$ включают константные функции, тождественную функцию и
        функции вида $F(X) = (x =_X x')$ (когда мы введем этот тип), а также строго положительные функции замкнуты относительно композиции.
\item Список правил редукций для конструкторов.
    Эти правила редукций мы называем \emph{условиями} на соответствующий конструктор.
    Позже мы опишем как должны выглядеть эти правила редукций.
\end{itemize}

Объявленние записи состоит из следующего набора данных:
\begin{itemize}
\item Имя записи $S$ и ее размер $\kappa \in \mathbb{N}$.
\item Контекст $x_1 : A_1, \ldots x_n : A_n$, задающий параметры $S$.
\item Имя конструктора $con$.
\item Список полей и их типов $f_i : B_i$.
\item Список правил редукций для полей.
    Эти правила редукций мы называем \emph{условиями} на соответствующее поле.
    Позже мы опишем как должны выглядеть эти правила редукций.
\end{itemize}

Если $\Sigma$ - сигнатура, то мы определяем правила вывода в этой сигнатуре.
Если мы хотим подчеркнуть, что вывод происходит в сигнатуре $\Sigma$, мы будем писать $\Gamma \vdash_\Sigma$ и $\Gamma \vdash_\Sigma a : A$.
Это будут все старые правила ввода, к которым мы добавляем следующие:

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\RightLabel{, где $f : A$ - функция в $\Sigma$}
\UnaryInfC{$\Gamma \vdash f : A$}
\DisplayProof
\end{center}

Для всех типов данных $D$ в $\Sigma$ размера $\kappa$ с параметрами $x_1 : A_1, \ldots x_n : A_n$.

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\AxiomC{$\Gamma \vdash a_i : A_i[x_1 := a_1] \ldots [x_{i-1} := a_{i-1}]$}
\RightLabel{,}
\BinaryInfC{$\Gamma \vdash D\ a_1 \ldots a_n : U_\kappa$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\AxiomC{$\Gamma \vdash a_i : A_i[x_1 := a_1] \ldots [x_{i-1} := a_{i-1}]$}
\RightLabel{,}
\BinaryInfC{$\Gamma \vdash c : C[x_1 := a_1] \ldots [x_n := a_n]$}
\DisplayProof
\end{center}
где $c$ - конструктор $D$, и $C$ - тип $c$.

Для всех записей $S$ в $\Sigma$ размера $\kappa$ с параметрами $x_1 : A_1, \ldots x_n : A_n$.

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\AxiomC{$\Gamma \vdash a_i : A_i[x_1 := a_1] \ldots [x_{i-1} := a_{i-1}]$}
\RightLabel{,}
\BinaryInfC{$\Gamma \vdash S\ a_1 \ldots a_n : U_\kappa$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash a_i : A_i[x_1 := a_1] \ldots [x_{i-1} := a_{i-1}]$}
\AxiomC{$\Gamma \vdash p : S\ a_1\ \ldots\ a_n$}
\RightLabel{,}
\BinaryInfC{$\Gamma \vdash p.f : B[x_1 := a_1] \ldots [x_n := a_n]$}
\DisplayProof
\end{center}
где $f$ - поле $S$ типа $B$.

\medskip
\begin{center}
\def\extraVskip{1pt}
\AxiomC{$\Gamma \vdash$}
\AxiomC{$\Gamma \vdash a_i : A_i[x_1 := a_1] \ldots [x_{i-1} := a_{i-1}]$}
\noLine
\BinaryInfC{$\Gamma \vdash b_j : B_j[x_1 := a_1] \ldots [x_{j-1} := a_{j-1}] [f_1 := b_1] \ldots [f_{j-1} := b_{j-1}]$}
\def\extraVskip{2pt}
\RightLabel{,}
\UnaryInfC{$\Gamma \vdash con\ b_1\ \ldots\ b_k : S\ a_1\ \ldots\ a_n $}
\DisplayProof
\end{center}
где $con$ - конструктор $S$, и $B_j$ - типы полей $S$.

Правила редукции для функций и конструкторов задаются при помощи \emph{сопоставлений с образцом (шаблоном)}.
Понятие шаблона определяется индуктивно.
Шаблон - это либо переменная, либо конструктор типа данных, возможно применненый к списку шаблонов.
То есть шаблон $p$ равен либо $x$, либо $c\ p_1 \ldots p_n$, где $x$ - переменная, $c$ - конструктор, $p_1, \ldots p_n$ - шаблоны.
Подстановка в шаблон $p$ - это терм вида $p[x_1 := t_1] \ldots [x_k := t_k]$ для некоторых переменных $x_1, \ldots x_k$ и термов $t_1, \ldots t_k$.

Если $f$ - функция или конструктор, то правила редукций для него выглядят следующим образом:
\[ f\ p_1 \ldots p_n \to_\beta t, \]
где $p_1, \ldots p_n$ - шаблоны, $t$ - терм.
Для каждого такого правила и каждой подстановки в шаблоны $p_1, \ldots p_n$ мы добавляем следующие правила $\beta$-редукции:
\[ f\ (p_1[x^1_1 := t^1_1] \ldots [x^1_{k_1} := t^1_{k_1}]) \ldots (p_n[x^n_1 := t^n_1] \ldots [x^n_{k_n} := t^n_{k_n}]) \to_\beta t[x^i_j := t^i_j] \]

Пусть $f : A$ - объявление функции $f$.
Мы будем говорить, что оно корректно в сигнатуре $\Sigma$, если $\vdash_\Sigma A$ и для любого правила редукции $f\ p_1 \ldots p_n \to_\beta t$
    существует контекст $\Gamma$ и терм $B$ такие, что $\Gamma \vdash_{\Sigma,f} f\ p_1 \ldots p_n : B$ и $\Gamma \vdash_{\Sigma,f} t : B$.
Также мы требуем, чтобы набор правил редукций был полным и завершающимся. TODO: Написать подробнее?

Мы накладываем еще одно требование на правила редукций - они должны удовлетворять условиям.
Мы будем говорить, что правила \emph{удовлетворяют условиям}, если для любой пары подстановок в $p_1, \ldots p_n$ таких,
    что $p_i[x^i_1 := t^i_1] \ldots [x^i_{k_i} := t^i_{k_i}] \ebst p_i[x^i_1 := s^i_1] \ldots [x^i_{k_i} := s^i_{k_i}]$,
    верно $t[x^i_j := t^i_j] \ebst t[x^i_j := s^i_j]$.

Мы будем говорить, что объявление типа данных $D$ размера $\kappa$ с параметрами $x_1 : A_1, \ldots x_n : A_n$ в сигнатуре $\Sigma$ корректно, если выполнены следующие условия:
\begin{itemize}
\item $x_1 : A_1, \ldots x_n : A_n \vdash_\Sigma$.
\item $x_1 : A_1, \ldots x_n : A_n, D : \Pi (x_1 : A_1) \ldots \Pi (x_n : A_n) U_\kappa \vdash_\Sigma C_i : U_\kappa$, где $C_i$ - тип конструктора $c_i$.
\item Для каждого условия $c_i\ p_1 \ldots p_k \to_\beta t_i$ существует такой контекст $\Delta$,
    что $\Gamma, \Delta \vdash_{\Sigma,D'} c_i\ p_1 \ldots p_k : D'\ x_1\ \ldots\ x_n$ и $\Gamma, \Delta \vdash_{\Sigma,D'} t_i : D'\ x_1\ \ldots\ x_n$,
    где $D'$ - это тип данных с тем же размером, параметрами и конструкторами, что и $D$, и с условиями с 1 по $i - 1$.
    Так же как и в случае функций, мы требуем, чтобы набор правил удовлетворял условиям, и был завершающимся, при этом он не обязан быть полон.
\end{itemize}

Мы будем говорить, что объявление записи $S$ размера $\kappa$ с параметрами $x_1 : A_1, \ldots x_n : A_n$ в сигнатуре $\Sigma$ корректно, если выполнены следующие условия:
\begin{itemize}
\item $x_1 : A_1, \ldots x_n : A_n \vdash_\Sigma$.
\item $x_1 : A_1, \ldots x_n : A_n, f_1 : B_1, \ldots f_{i-1} : B_{i-1} \ldots \vdash_\Sigma B_i : U_\kappa$, где $B_j$ - тип поля $f_j$ для всех $j \leq i$.
\item Для каждого условия $f_i\ p_1 \ldots p_k \to_\beta t_i$ существует такой контекст $\Delta$ и тип $B$,
    что $\Gamma, \Delta \vdash_\Sigma f_i\ p_1 \ldots p_k : B$ и $\Gamma, \Delta \vdash_\Sigma t_i : B$,
    Так же как и в случае типов данных, мы требуем, чтобы набор правил удовлетворял условиям, и был завершающимся, при этом он не обязан быть полон.
\end{itemize}

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

\begin{comment}
В этом разделе мы опишем интерпретацию языка в категории $\C$. Сначала мы опишем требования на $\C$.
Категория $\C$ должна быть снабжена комбинаторной правой точной (right proper) модельной структурой с мономорфизмами в качестве корасслоений.
Также мы предполагаем, что в $\C$ выполнена следующая аксиома.
Если $f : A \to B$ и $g : C \to D$ - корасслоения, то $f \wedge g : B \times C \amalg_{A \times C} A \times D \to B \times D$ также является корасслоением,
    и если одно из этих корасслоений тривиально, то $f \wedge g$ также тривиально.

Кроме того, $\C$ должна быть локально декартова замкнута, таким образом $\C$ является топосом Гротендика.
Также мы требуем, чтобы в $\C$ существовало достаточное количество классификаторов объектов для интерпретации вселенных.
Классификатор объектов - это некоторое отображение $\pi : \widehat{\mathcal{U}} \to \mathcal{U}$.
Мы говорим, что $\pi$ классифицирует отображение $f : Y \to X$, если $f$ является обратным образом $\pi$ относительно некоторого отображения $\ulcorner f \urcorner : X \to \mathcal{U}$.
Классификаторы объектов $\pi$ замкнут относительно $\Pi$-типов (соответственно, $\Sigma$-типов), если
    для любой пары отображений $f : Z \to Y$ и $g : Y \to X$, которые классифицируются $\pi$, верно,
    что $\Pi_g(f) \to X$ (соответственно, $g \circ f$) также классифицируется $\pi$.
Классификаторы объектов $\pi$ замкнут относительно некоторого вида (ко)пределов, если для любой диаграмы такого вида в категории $\C / X$,
    состоящей из морфизмов, классифицирующихся $\pi$, ее (ко)предел также классифицируется $\pi$.
Мы требуем, чтобы в $\C$ существовала последовательность классификаторов объектов
    $\pi_0 : \widehat{\mathcal{U}_0} \to \mathcal{U}_0, \pi_1 : \widehat{\mathcal{U}_1} \to \mathcal{U}_1, \ldots$ такая,
    что для любого $\kappa$ существует мономорфизм $\mathcal{U}_\kappa \to \mathcal{U}_{\kappa + 1}$.

Классификаторы объектов должны быть замкнуты относительно $\Pi$-типов, $\Sigma$-типов, конечных пределов и копределов и фибрантной замены.
Это означает, что если $f : Z \to Y$ и $g : Y \to X$ классифицируются $\pi_\kappa$, то $\Pi_g(f) \to X$ и $g \circ f$ также должны классифицироваться $\pi_\kappa$.
Если некоторая конечная диаграмма в категории $\C / X$ состоит из морфизмов, классифицирующихся $\pi_\kappa$, то ее предел и копредел также должен классифицироваться $\pi_\kappa$.
Наконец, если домен и кодомен отображения $f$ классицируются $\pi_\kappa$, то $f$ факторизуется как тривиальное корасслоение и расслоение, классифицирующееся $\pi_\kappa$.
\end{comment}

В этом разделе мы опишем интерпретацию языка в категории $\sSet$ симплициальных множеств.
Мы предполагаем, что существует последовательность недостижимых кардиналов.
Следовательно у нас есть последовательность классификаторов объектов $\pi_\kappa : \widehat{\mathcal{U}_\kappa} \to \mathcal{U}_\kappa$.
Классификатор объектов $\pi_\kappa$ - это такое расслоение, что любое $\kappa$-малое расслоение $f : Y \to X$ является обратным образом $\pi$ относительно некоторого морфизма $\ulcorner f \urcorner : X \to \mathcal{U}_\kappa$.

Правила вывода из таблицы~\ref{table:inf-rules} интерпретируются так же, как в \cite{kap-lum-voe}.
Мы не будем описывать эту интерпретацию подробно, лишь установим нотацию.
Каждому контексту $\Gamma \vdash$ сопоставляется объект $\ll \Gamma \rr \in \sSet$.
Каждому типу $\Gamma \vdash A$ сопоставляется отображение $\ulcorner \ll A \rr \urcorner : \ll \Gamma \rr \to \mathcal{U}_\kappa$.
Если $\Gamma \vdash A$, то мы будем обозначать обратный образ $\pi_\kappa$ относительно $\ulcorner \ll A \rr \urcorner$ как $\ll A \rr : \ll \Gamma \vdash A \rr \to \ll \Gamma \rr$.
Каждому терму $\Gamma \vdash a : A$ сопоставляется морфизм $\ll \Gamma \vdash a : A \rr : \ll \Gamma \rr \to \widehat{\mathcal{U}_\kappa}$ такой, что следующая диаграмма коммутирует:
\[ \xymatrix{ \ll \Gamma \rr \ar[r]^{\ll \Gamma \vdash a : A \rr} \ar[dr]_{\ulcorner \ll A \rr \urcorner} & \widehat{\mathcal{U}_\kappa} \ar[d]^{\pi_\kappa} \\
                                                                                                          & \mathcal{U}_\kappa.
            }\]

Теперь мы покажем как интерпретируются некоторые правила вывода, интерпретация остальных аналогична таковой в \cite{kap-lum-voe}.
\begin{itemize}
\item
\AxiomC{$\Gamma \vdash A : U_\kappa$}
\UnaryInfC{$\Gamma \vdash A$}
\DisplayProof
\medskip

Морфизм $\ll \Gamma \vdash A : U_\kappa \rr$ факторизуется через некоторое отображение $A' : \ll \Gamma \rr \to \mathcal{U}_\kappa$.
Мы интерпретируем $\Gamma \vdash A$ как отображение $\ll \Gamma \rr \to \mathcal{U}_{\kappa'}$ для минимального $\kappa'$ для которого $A'$ факторизуется через мономорфизм $\mathcal{U}_{\kappa'} \to \mathcal{U}_\kappa$.

\item
\medskip
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash I : U_\kappa$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash left : I$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash right : I$}
\DisplayProof
\medskip

Факторизуем отображение $1 + 1 \to 1$ через корасслоение $[i_0,i_1] : 1 + 1 \to \ll I \rr$ и тривиальное расслоение $\ll I \rr \to 1$.
Тогда $\Gamma \vdash I : U_\kappa$ интерпретируется как $\Gamma \to 1 \xrightarrow{\ulcorner \ll I \rr \urcorner} \mathcal{U}$
Термы $left$ и $right$ интерпретируются как морфизмы $\Gamma \to 1 \xrightarrow{i_k} \ll I \rr \to \widehat{\mathcal{U}_0}$, где $k = 0$ для $left$ и $k = 1$ для $right$.

\item
\medskip
\AxiomC{$\Gamma, x : I \vdash A$}
\AxiomC{$\Gamma \vdash i : I$}
\AxiomC{$\Gamma \vdash a : A[x := i]$}
\AxiomC{$\Gamma \vdash j : I$}
\QuaternaryInfC{$\Gamma \vdash coe_{\lambda x. A}\ i\ a\ j : A[x := j]$}
\DisplayProof
\medskip

Пусть интерпретация $\Gamma, x : I \vdash A$ - это некоторый морфизм $\ll \Gamma \rr \times \ll I \rr \to \mathcal{U}_\kappa$.
Во-первых, сконструируем вспомоготельные объект $Z$ следующим образом:
\[ \xymatrix{ Z \ar[r]^f \ar[d]_{\langle A, i \rangle} \pb                   & \widehat{\mathcal{U}_\kappa} \ar[d]^{\pi_\kappa} \\
              {\mathcal{U}_\kappa}^{\ll I \rr} \times \ll I \rr \ar[r]_-{ev} & \mathcal{U}_\kappa
            }\]
Теперь мы можем определить морфизм $\ll \Gamma \rr \to Z \times \ll I \rr$: на второй координате - это интерпретация $j$, на первой - это интерпретация $A$, $i$ и $a$.
Мы можем определить интерпретацию $coe$ как комопозицию этого отображения и диагонального морфизма в следующей диаграме:
\[ \xymatrix{ Z \ar[rr]^f \ar[d]_{\langle id, i \rangle}                          & & \widehat{\mathcal{U}_\kappa} \ar[d]^{\pi_\kappa} \\
              Z \times \ll I \rr \ar[rr]_-{ev \circ (A \times id)} \ar@{-->}[urr] & & \mathcal{U}_\kappa
            }\]
Коммутирование верхнего треугольника означает, что выполнено $\beta$-правило для $coe$.
Но $\sigma$ и $\tau$ правила при это не обязаны выполняться.
Мы проигнорируем $\tau$ правила, так как они нужно только для каноничности.
Но $\sigma$-правило необходимо для того, чтобы $J$ удовлетворял обычному правилу редукции, поэтому мы модифицируем определение интерпретации $coe$ так, чтобы $\sigma$-правило выполнялось.
Для этого определим объект $Z'$ следующим образом:
\[ \xymatrix{ Z' \ar[r]^g \ar[d]_{\langle A', i' \rangle} \pb           & Z \ar[d]^{\langle A, i \rangle} \\
              \mathcal{U}_\kappa \times \ll I \rr \ar[r]_-{c \times id} & {\mathcal{U}_\kappa}^{\ll I \rr} \times \ll I \rr
            }\]
Здесь $c : \mathcal{U}_\kappa \to {\mathcal{U}_\kappa}^{\ll I \rr}$ - морфизм, по сопряжению соответствующий проекции $\mathcal{U}_\kappa \times \ll I \rr \to \mathcal{U}_\kappa$.
Теперь мы можем сконструировать морфизм $h : Z \amalg_{Z'} Z' \times \ll I \rr \to Z \times \ll I \rr$ следующим образом:
\[ \xymatrix{ Z' \ar[r]^g \ar[d]_{\langle id, i' \rangle}       & Z \ar[d] \ar[rdd]^{\langle id, i \rangle}             & \\
              Z' \times \ll I \rr \ar[r] \ar[rrd]_{g \times id} & \po Z \amalg_{Z'} Z' \times \ll I \rr \ar@{-->}[rd]^h & \\
                                                                &                                                       & Z \times \ll I \rr
            }\]
Морфизм $h$ является тривиальным корасслоением.
Действительно, $\langle id, i' \rangle$ и $\langle id, i \rangle$ - тривиальные корасслоения, следовательно $h$ - слабая эквивалентность.
Теперь покажем, что $h$ - мономорфизм.
Пусть $\Delta[n] \rightrightarrows Z \amalg_{Z'} Z' \times \ll I \rr$ - пара симплексов таких, что они равны при композиции с $h$.
Тогда они факторизуются либо через $Z$, либо через $Z' \times \ll I \rr$.
Если они факторизуются через один объект, то они равны, т.к. $g \times id$ и $\langle id, i \rangle$ - мономорфизмы.
Пусть один из них факторизуется через $x : \Delta[n] \to Z$, а другой через $y : \Delta[n] \to Z' \times \ll I \rr$.
Тогда $\Delta[n] \xrightarrow{x} Z = \Delta \xrightarrow{x} Z \xrightarrow{\langle id, i \rangle} Z \times \ll I \rr \to Z = \Delta[n] \xrightarrow{y} Z' \times \ll I \rr \to Z' \xrightarrow{g} Z$.
То есть $x$ факторизуется через $g$, а значит $\Delta[n] \xrightarrow{x} Z \to Z \amalg_{Z'} Z' \times \ll I \rr$ факторизуется через $Z' \times \ll I \rr$, что и требовалось.

Теперь мы определяем интерпретацию $coe$ как комопозицию $\ll \Gamma \rr \to Z \times \ll I \rr$ и диагонального морфизма в следующей диаграме:
\[ \xymatrix{ Z \amalg_{Z'} Z' \times \ll I \rr \ar[rr] \ar[d]_h                  & & \widehat{\mathcal{U}_\kappa} \ar[d]^{\pi_\kappa} \\
              Z \times \ll I \rr \ar[rr]_-{ev \circ (A \times id)} \ar@{-->}[urr] & & \mathcal{U}_\kappa
            }\]
Верхний горизонтальный морфизм порождается морфизмами $Z \xrightarrow{f} \widehat{\mathcal{U}_\kappa}$
    и $Z' \times \ll I \rr \to Z' \xrightarrow{g} Z \xrightarrow{f} \widehat{\mathcal{U}_\kappa}$.

Теперь, если $\ll i \rr = \ll j \rr$, то $\ll coe_{\lambda x. A}\ i\ a\ j \rr$ факторизуется через $Z$ и, следовательно, равняется $\ll a \rr$.
Если $x \notin FV(A)$, то $\ll coe_{\lambda x. A}\ i\ a\ j \rr$ факторизуется через $Z' \times \ll I \rr$ и, следовательно, опять равняется $\ll a \rr$.
Таким образом $\beta$ и $\sigma$ правила выполнены.
\end{itemize}

\subsection{Интерпретация типов данных с условиями}

Каждому конструктору $c_i$ типа данных $D$ с параметрами $\Gamma$ мы сопоставляем функтор $F_i : \sSet / \Gamma \to \sSet / \Gamma$ стандартным образом.
Пусть $F(X) = \coprod_{i \leq n} F_i(X)$ - сумма $F_i$ по всем конструкторам.
Функтор $F$ сохраняет $\lambda$-фильтрированные копределы для некоторого регулярного кардинала $\lambda$.
Мы определяем интерпретацию $D$ как копредел $\lambda$-последовательности $X_\alpha : \sSet / \Gamma$.
Каждый $X_\alpha \to X_{\alpha + 1}$ определяется как композиция $X_\alpha \to Z_\alpha \to R Z_\alpha \xrightarrow{c_\alpha} X_{\alpha + 1}$,
    где вторая стрелка - это фибрантная замена, а третья - коуравнитель пары стрелок $C_\alpha \rightrightarrows R Z_\alpha$, которые мы определим позже.
Морфизмы $X_\alpha \to Z_\alpha$ определяются индуктивным образом вместе с морфизмами $f_\alpha : F X_\alpha \to Z_\alpha$ естественными по $\alpha < \lambda$.
\begin{itemize}
\item $X_0$ определяется как начальный объект, $Z_0 = F X_0$, и $f_0 = id_{F X_0}$.
\item $Z_{\alpha + 1}$ и $f_{\alpha + 1}$ определяются следующим кодекартовым квадратом:
\[ \xymatrix{ F X_\alpha \ar[r] \ar[d] & F X_{\alpha + 1} \ar[d]^{f_{\alpha + 1}} \\
              X_{\alpha + 1} \ar[r]    & \po Z_{\alpha + 1},
            } \]
где левая стрелка - это композиция $F X_\alpha \xrightarrow{f_\alpha} Z_\alpha \to R Z_\alpha \xrightarrow{c_\alpha} X_{\alpha + 1}$.
\item $X_\alpha = \varinjlim_{\beta < \alpha} (X_\beta)$ для предельного $\alpha$.
$Z_\alpha$ и $f_\alpha$ определяются через следующий кодекартов квадрат:
\[ \xymatrix{ \varinjlim_{\beta < \alpha} (F X_\beta) \ar[r] \ar[d] & F X_\alpha \ar[d]^{f_\alpha} \\
              X_\alpha \ar[r]                                       & \po Z_\alpha,
            } \]
где левая стрелка порождается морфизмами $f_\beta$.
\end{itemize}

Если $D$ не содержит ни одного условия, то в качестве $C_\alpha$ берется начальный объект для всех $\alpha$.
Таким образом, в качестве $c_\alpha$ можно взять $id$, и $\ll D \rr$ можно описать как копредел следующей последовательности:
\[ 0 = X_0 \to F X_0 \to R F X_0 = X_1 \to X_1 \amalg_{F X_0} F X_1 \to R (X_1 \amalg_{F X_0} F X_1) = X_2 \to \ldots \]
Пусть мы определили интерпретацию типа $D'$ как копредел последовательности $X'_\alpha$, и теперь мы хотим описать интерпретацию типа $D$, у которого на одно условие больше, чем у $D'$.
Интерпретация левой и правой частей условия дает нам пару морфизмов $\ll \Gamma, \Delta \rr \rightrightarrows \ll D' \rr$ над $\ll \Gamma \rr$.
Мы определим последовательность $X_\alpha$ вместе с коллекцией морфизмов $X'_\alpha \to X_\alpha$.
Так как $X_\alpha$ почти совпадает с $X'_\alpha$, эти морфизмы определяется очевидным образом через универсальные свойства амальгам, коуравнителей и фибрантной замены.
Чтобы определить $X_\alpha$ нам нужно только описать стрелки $C_\alpha \rightrightarrows R Z_\alpha$.
Для этого для каждого $\alpha$ определим объект $C''_\alpha$ как предел следующей диаграмы:
\[ \xymatrix@R-1pc{ R Z'_\alpha \ar[r] & \ll D' \rr & \\
                                       &            & \ll \Gamma, \Delta \rr \ar[ul] \ar[dl] \\
                    R Z'_\alpha \ar[r] & \ll D' \rr &
            } \]
Теперь мы определяем $C_\alpha$ как $C'_\alpha \amalg C''_\alpha$, где $C'_\alpha \rightrightarrows R Z'_\alpha$ - пара стрелок, которая использовалась при определении $D'$.
Стрелки $C_\alpha \rightrightarrows R Z_\alpha$ определяются как композиция $C'_\alpha \amalg C''_\alpha \rightrightarrows R Z'_\alpha \to R Z_\alpha$,
    где стрелки $C''_\alpha \rightrightarrows R Z'_\alpha$ берутся из предельного конуса.

Так как $F$ сохраняет $\lambda$-фильтрированные копределы, мы можем определить морфизм $F \ll D \rr \simeq \lim_{\alpha < \lambda} F X_\alpha \to \ll D \rr$,
    где последняя стрелка порождается морфизмами $f_\alpha$.
Таким образом, $\ll D \rr$ является $F$-алгеброй, что дает нам интерпретацию конструкторов.
TODO: Нам нужно проверить, что условия на них выполнены.

TODO: Описать интерпретацию функций.

\subsection{Интерпретация записей с условиями}

\bibliographystyle{amsplain}
\bibliography{ref}

\end{document}