thesis-rus.tex

\documentclass[reqno]{amsart}

\usepackage[russian]{babel}
\usepackage[utf8]{inputenc}
\usepackage{mathtools}
\usepackage{cmap}
\usepackage{amsfonts}
\usepackage{upgreek}
\usepackage{xargs}
\usepackage{ifthen}
\usepackage[all]{xy}
\usepackage{hyperref}
\usepackage{etex}
\usepackage{bussproofs}
\usepackage{turnstile}
\usepackage{amssymb}
\usepackage{verbatim}

\hypersetup{colorlinks=true,linkcolor=blue}

\renewcommand{\turnstile}[6][s]
    {\ifthenelse{\equal{#1}{d}}
        {\sbox{\first}{$\displaystyle{#4}$}
        \sbox{\second}{$\displaystyle{#5}$}}{}
    \ifthenelse{\equal{#1}{t}}
        {\sbox{\first}{$\textstyle{#4}$}
        \sbox{\second}{$\textstyle{#5}$}}{}
    \ifthenelse{\equal{#1}{s}}
        {\sbox{\first}{$\scriptstyle{#4}$}
        \sbox{\second}{$\scriptstyle{#5}$}}{}
    \ifthenelse{\equal{#1}{ss}}
        {\sbox{\first}{$\scriptscriptstyle{#4}$}
        \sbox{\second}{$\scriptscriptstyle{#5}$}}{}
    \setlength{\dashthickness}{0.111ex}
    \setlength{\ddashthickness}{0.35ex}
    \setlength{\leasturnstilewidth}{2em}
    \setlength{\extrawidth}{0.2em}
    \ifthenelse{%
      \equal{#3}{n}}{\setlength{\tinyverdistance}{0ex}}{}
    \ifthenelse{%
      \equal{#3}{s}}{\setlength{\tinyverdistance}{0.5\dashthickness}}{}
    \ifthenelse{%
      \equal{#3}{d}}{\setlength{\tinyverdistance}{0.5\ddashthickness}
        \addtolength{\tinyverdistance}{\dashthickness}}{}
    \ifthenelse{%
      \equal{#3}{t}}{\setlength{\tinyverdistance}{1.5\dashthickness}
        \addtolength{\tinyverdistance}{\ddashthickness}}{}
        \setlength{\verdistance}{0.4ex}
        \settoheight{\lengthvar}{\usebox{\first}}
        \setlength{\raisedown}{-\lengthvar}
        \addtolength{\raisedown}{-\tinyverdistance}
        \addtolength{\raisedown}{-\verdistance}
        \settodepth{\raiseup}{\usebox{\second}}
        \addtolength{\raiseup}{\tinyverdistance}
        \addtolength{\raiseup}{\verdistance}
        \setlength{\lift}{0.8ex}
        \settowidth{\firstwidth}{\usebox{\first}}
        \settowidth{\secondwidth}{\usebox{\second}}
        \ifthenelse{\lengthtest{\firstwidth = 0ex}
            \and
            \lengthtest{\secondwidth = 0ex}}
                {\setlength{\turnstilewidth}{\leasturnstilewidth}}
                {\setlength{\turnstilewidth}{2\extrawidth}
        \ifthenelse{\lengthtest{\firstwidth < \secondwidth}}
            {\addtolength{\turnstilewidth}{\secondwidth}}
            {\addtolength{\turnstilewidth}{\firstwidth}}}
        \ifthenelse{\lengthtest{\turnstilewidth < \leasturnstilewidth}}{\setlength{\turnstilewidth}{\leasturnstilewidth}}{}
    \setlength{\turnstileheight}{1.5ex}
    \sbox{\turnstilebox}
    {\raisebox{\lift}{\ensuremath{
        \makever{#2}{\dashthickness}{\turnstileheight}{\ddashthickness}
        \makehor{#3}{\dashthickness}{\turnstilewidth}{\ddashthickness}
        \hspace{-\turnstilewidth}
        \raisebox{\raisedown}
        {\makebox[\turnstilewidth]{\usebox{\first}}}
            \hspace{-\turnstilewidth}
            \raisebox{\raiseup}
            {\makebox[\turnstilewidth]{\usebox{\second}}}
        \makever{#6}{\dashthickness}{\turnstileheight}{\ddashthickness}}}}
        \mathrel{\usebox{\turnstilebox}}}

\newcommand{\axlabel}[1]{(#1) \phantomsection \label{ax:#1}}
\newcommand{\axtag}[1]{\label{ax:#1} \tag{#1}}
\newcommand{\axref}[1]{(\hyperref[ax:#1]{#1})}

\newcommand{\newref}[7][]{
\ifthenelse{\equal{#1}{}}{\newtheorem{h#2}[hthm]{#4}}{\newtheorem{h#2}{#4}[#1]}
\expandafter\newcommand\csname r#2\endcsname[1]{#3~\ref{#2:##1}}
\expandafter\newcommand\csname R#2\endcsname[1]{#4~\ref{#2:##1}}
\expandafter\newcommand\csname d#2\endcsname[1]{#5~\ref{#2:##1}}
\expandafter\newcommand\csname p#2\endcsname[1]{#6~\ref{#2:##1}}
\expandafter\newcommand\csname o#2\endcsname[1]{#7~\ref{#2:##1}}
\expandafter\newcommand\csname n#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}{теорема}{Теорема}{теореме}{теореме}{теоремы}
\newref{lem}{лемма}{Лемма}{лемме}{лемме}{леммы}
\newref{prop}{утверждение}{Утверждение}{утверждению}{утверждении}{утверждения}
\newref{cor}{следствие}{Следствие}{следствию}{следствии}{следствия}

\theoremstyle{definition}
\newref{defn}{определение}{Определение}{определению}{определении}{определения}
\newref{example}{пример}{Пример}{примеру}{примере}{примера}

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

\newcommand{\bcat}[1]{\mathbf{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
\renewcommand{\C}{\cat{C}}
\newcommand{\D}{\cat{D}}
\newcommand{\we}{\mathcal{W}}
\newcommand{\fib}{\mathrm{Fib}}
\newcommand{\cof}{\mathrm{Cof}}
\newcommand{\Mod}[1]{#1\text{-}\bcat{Mod}}
\newcommand{\Set}{\bcat{Set}}
\newcommand{\fs}[1]{\mathrm{#1}}
\newcommand{\Hom}{\fs{Hom}}
\newcommand{\Lang}{\fs{Lang}}
\newcommand{\Syn}{\fs{Syn}}
\newcommand{\nf}{\mathrm{nf}}
\newcommand{\FV}{\fs{FV}}
\newcommand{\repl}{:=}
\newcommand{\Term}{\mathrm{Term}}
\newcommand{\Th}{\bcat{Th}}
\newcommand{\Cat}{\bcat{Cat}}
\newcommand{\colim}{\fs{colim}}
\newcommand{\cyli}{i}

\newcommand{\I}{\mathrm{I}}
\newcommand{\J}{\mathrm{J}}
\newcommand{\class}[2]{#1\text{-}\mathrm{#2}}
\newcommand{\Iinj}[1][\I]{\class{#1}{inj}}
\newcommand{\Icell}[1][\I]{\class{#1}{cell}}
\newcommand{\Icof}[1][\I]{\class{#1}{cof}}
\newcommand{\Jinj}[1][]{\Iinj[\J#1]}
\newcommand{\Jcell}[1][]{\Icell[\J#1]}
\newcommand{\Jcof}[1][]{\Icof[\J#1]}

\newenvironment{tolerant}[1]{\par\tolerance=#1\relax}{\par}

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

\begin{document}

\title{Title}

\author{Valery Isaev}

\maketitle

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

\section{Частичные хорновские теории}
\label{sec:pht}

В данной диссертации мы будем работать с определенным классом логических теорий, которые известны под разными названиями, но наиболее распространенный термин -- это \emph{существенно алгебраические теории}.
Существует несколько эквивалентных способов определить такие теории:
\begin{enumerate}
\item Декартовы теории \cite[Definition~D1.3.4]{elephant} -- это специальный вид теорий в логике первого порядка, где единственные логческие связки -- это конъюнкция и квантор существования.
Кроме того, множество аксиом должно удовлетворять определенному условию.
Мы не будем использовать это понятие, поэтому точное определение нам не понадобится.
\item Обобщенные алгебраические теории \cite{GAT} могут содержать сорта, зависящие от других сортов.
\item Существенно алгебраические теории \cite[Definition~3.34]{LPC} -- это теории, в которых некоторые функциональные символы могут интерпретироваться как \emph{частичные} функции.
Мы не будем использовать это понятие, поэтому точное определение нам не понадобится.
\item Частичные хорновские теории \cite{PHL} являются обобщением существенно алгебраических теорий.
\item Категорное определение теорий является самым простым.
Согласно нему (финитарная) существенно алгебраическая теория -- это просто конечно полная малая категория.
Модель такой теории $\cat{C}$ -- это просто функтор $\cat{C} \to \Set$, сохраняющий конечные пределы.
Другое преимущество этого определения заключается в том, что легко определить структуру категории (и даже 2-категории) на классе теорий.
\end{enumerate}

Мы будем работать с частичными хорновскими теориями, определение которых мы приведем в следующем подразделе.
Часто аксиомы теории порождаются отношением, которое обладает различными хорошими свойствами такими, как сильная нормализация и конфлюэнтность.
Мы изучим такие теории в этом разделе.
Кроме того, мы обсудим связь чистичных хорновских теорий с категорным определением существенно алгебраических теорий.
Конкретно, мы зададим структуру 2-категории на них и докажем, что она эквивалентна 2-категории конечно полных малых категорий.

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

В этом подразделе мы приведем основные определения из \cite{PHL}.
Мы дадим более общее определение инфинитарных теорий.
\emph{Сигнатура} -- это тройка $(\mathcal{S},\mathcal{F},\mathcal{P})$, где $\mathcal{S}$ -- множество сортов, $\mathcal{F}$ -- множество функциональных символов, и $\mathcal{P}$ -- множество предикатных символов.
Каждому функциональному символу $\sigma$ сопоставляется его сигнатура, то есть множество $I$, функция $s : I \to \mathcal{S}$ и сорт $s$, что записывается как $\sigma : \prod_{i \in I} s_i \to s$.
Каждому предикатному символу $R$ сопоставляется множество $I$ и функция $s : I \to \mathcal{S}$, что записывается как $R : \prod_{i \in I} s_i$.
Если $I = \{ 1, \ldots n \}$ -- конечное множество, то сигнатуры $\sigma$ и $R$ мы будем записывать как $\sigma : s_1 \times \ldots \times s_n \to s$ и $R : s_1 \times \ldots \times s_n$.

Если $\lambda$ -- регулярный кардинал, то мы будем говорить, что функциональный символ $\sigma : \prod_{i \in I} s_i \to s$ является \emph{$\lambda$-достижимым}, если $|I| < \lambda$.
Аналогично предикатный символ $R : \prod_{i \in I} s_i$ является \emph{$\lambda$-достижимым}, если $|I| < \lambda$.
Сигнатура является \emph{$\lambda$-достижимой}, если все ее функциональные и предикатные символы $\lambda$-достижимы.

\begin{defn}
Если $\mathcal{S}$ -- некоторое множество, то \emph{$\mathcal{S}$-множество} -- это множество $X$ вместе с функцией $p : X \to \mathcal{S}$.
Если $\mathcal{S}$ -- множество сортов некоторой теории и $x \in X$, то мы будем говорить, что $x$ имеет сорт $s$, если $p(x) = s$.
\end{defn}

Для любого $\mathcal{S}$-множества $V$ мы можем определить $\mathcal{S}$-множество термов $\Term(V)$ с переменными в $V$ индуктивным образом:
\begin{enumerate}
\item Любая переменная сорта $s$ является термом этого сорта.
\item Если $\sigma : \prod_{i \in I} s_i \to s$ -- функциональный символ, и $t_i$ -- терм сорта $s_i$ для всех $i \in I$, то $\sigma(\{ t_i \}_i)$ -- терм сорта $s$.
\end{enumerate}

\emph{Атомарная формула} -- это выражение вида $t_1 = t_2$, где $t_1$ и $t_2$ -- термы одного и того же сорта,
либо вида $R(\{ t_i \}_i)$, где $R : \prod_{i \in I} s_i$ -- предикатный символ, а $t_i$ -- терм сорта $s_i$ для всех $i \in I$.
\emph{(Хорновская) формула} -- это выражение вида $\bigwedge_{i \in I} \varphi_i$, где $\varphi_i$ -- атомарные формулы.
Конъюнкция пустого множества формул будет обозначаться как $\top$.
Выражение $t\!\downarrow$ является сокращением для $t = t$.
Функциональные символы интерпретируются как частичные функции.
Формула $t\!\downarrow$ означает, что все подвыражения в $t$ определены.
\emph{Секвенция} -- это выражение вида $\varphi \sststile{}{V} \psi$, где $V$ -- $\mathcal{S}$-множество, а $\varphi$ и $\psi$ -- формулы с переменными в $V$.
Множество переменных, встречающихся в формуле или терме $\varphi$ будет обозначаться как $\FV(\varphi)$.
Если $I = \{ 1, \ldots n \}$, то мы будем записывать $\bigwedge_{i \in I} \varphi_i$ как $\varphi_1 \land \ldots \land \varphi_n$.
Вместо $\varphi_1 \land \ldots \land \varphi_n \sststile{}{V} \psi$ мы будем часто писать $\varphi_1, \ldots \varphi_n \sststile{}{V} \psi$.

Мы будем использовать следующие сокращения:
\begin{align*}
\varphi \sststile{}{V} t \cong s & \Longleftrightarrow \varphi \land t\!\downarrow\,\sststile{}{V} t = s \text{ и } \varphi \land s\!\downarrow\,\sststile{}{V} t = s \\
\varphi \ssststile{}{V} \psi & \Longleftrightarrow \varphi \sststile{}{V} \psi \text{ и } \psi \sststile{}{V} \varphi
\end{align*}

\begin{defn}
\emph{Частичная хорновская теория} -- это четверка $(\mathcal{S},\mathcal{F},\mathcal{P},\mathcal{A})$, где $(\mathcal{S},\mathcal{F},\mathcal{P})$ -- это сигнатура, а $\mathcal{A}$ -- множество секвенций.
Элементы $\mathcal{A}$ мы будем называть аксиомами.
\end{defn}

\begin{remark}
Так как частичные хорновские теории -- это единственный вид теорий, с которым мы будем работать, то мы их будем называть просто теориями.
\end{remark}

Мы будем говорить, что формула $\bigwedge_{i \in I} \varphi_i$, где $\varphi_i$ атомарны, является \emph{$\lambda$-достижимой} если $|I| < \lambda$.
Мы будем говорить, что секвенция $\varphi \sststile{}{V} \psi$ является \emph{$\lambda$-достижимой} если $|V| < \lambda$ и $\varphi$ и $\psi$ являются $\lambda$-достижимыми.
Мы будем говорить, что теория является \emph{$\lambda$-достижимой}, если ее подлежащая сигнатура и аксиомы являются таковыми.
Теория является финитарной, если она $\aleph_0$-достижима.

\emph{Интерпретация} сигнатуры $(\mathcal{S},\mathcal{F},\mathcal{P})$ -- это $\mathcal{S}$-множество $M$
вместе с коллекцией частичных функций $M(\sigma) : \prod_{i \in I} M_{s_i} \to M_s$ для каждого функционального символа $\sigma : \prod_{i \in I} s_i \to s$
и коллекцией отношений $M(R) \subseteq \prod_{i \in I} M_{s_i}$ для каждого предикатного символа $R : \prod_{i \in I} s_i$.

Пусть $V$ -- некоторое $\mathcal{S}$-множество.
Если $t$ -- терм сорта $s$ в сигнатуре $\Sigma$ с переменными в $V$, и $M$ -- интерпретация $\Sigma$, то мы можем определить частичную функцию $M(t) : \prod_{s \in \mathcal{S}} M_s^{V_s} \to M_s$ рекурсией по структуре $t$.
Если $t = x \in V_s$, то $M(t)(f) = f_s(x)$.
Если $t = \sigma(\{ t_i \}_i)$, то $M(t)(f) = M(\sigma)(\{ M(t_i)(f) \}_i)$.
Если $\varphi$ -- формула в сигнатуре $\Sigma$ с переменными в $V$, и $M$ -- интерпретация $\Sigma$, то мы можем определить отношение $M(\varphi) \subseteq \prod_{s \in \mathcal{S}} M_s^{V_s}$.
Если $\varphi$ -- формула вида $t_1 = t_2$, то $M(\varphi)$ состоит из таких $f$, что $M(t_1)(f)$ и $M(t_2)(f)$ определены и $M(t_1)(f) = M(t_2)(f)$.
Если $\varphi$ -- формула вида $R(\{ t_i \}_i)$, то $M(\varphi)$ состоит из таких $f$, что функции $M(t_i)(f)$ определены для всех $i \in I$ и $\{ M(t_i)(f) \}_i \in M(R)$.
Если $\varphi = \bigwedge_{i \in I} \varphi_i$, то $M(\varphi) = \bigcap_{i \in I} M(\varphi_i)$.
Секвенция $\varphi \sststile{}{V} \psi$ верна в интерпретации $M$ если $M(\varphi) \subseteq M(\psi)$.

\begin{defn}
\emph{Модель} теории -- это интерпретация ее сигнатуры такая, что все аксиомы теории верны в этой интерпретации.
\end{defn}

\begin{example}
Теория категорий -- это финитарная теория, состоящая из двух сортов $\fs{ob}$ и $\fs{hom}$, функциональных символов $d,c : \fs{hom} \to \fs{ob}$, $\fs{id} : \fs{ob} \to \fs{hom}$, $\circ : \fs{hom} \times \fs{hom} \to \fs{hom}$ и следующих аксиом:
\begin{align*}
& \sststile{}{f} d(f)\!\downarrow \land c(f)\!\downarrow \\
& \sststile{}{x} d(\fs{id}(x)) = x \land c(\fs{id}(x)) = x \\
c(f) = d(g) & \ssststile{}{f,g} \circ(g,f)\!\downarrow \\
c(f) = d(g) & \sststile{}{f,g} d(\circ(g,f)) = d(f) \land c(\circ(g,f)) = c(g) \\
& \sststile{}{f} \circ(\fs{id}(c(f)),f) = f \land \circ(f,\fs{id}(d(f))) = f \\
c(f) = d(g) \land c(g) = d(h) & \sststile{}{f,g,h} \circ(\circ(h,g),f) = \circ(h,\circ(g,f))
\end{align*}
Первые две аксиомы говорят, что функции $c$, $d$ и $\fs{id}$ тотальны и описывают домен и кодомен морфизма $\fs{id}(x)$.
Третья аксиома говорит, что функция $\circ(g,f)$ определена тогда и только тогда, когда домен $g$ совпадает с кодоменом $f$.
Четвертая аксиома описывает домен и кодомен морфизма $\circ(g,f)$.
Последние две аксиомы говорят, что $\circ$ ассоциативна и $\fs{id}$ является единицей для $\circ$.
Модели этой теории -- это в точности малые категории.
\end{example}

\begin{example}[fc-cats]
Теория конечно полных категорий является расширением теории категорий.
Мы добавляем функциональные символы $1 : \fs{ob}$, $! : \fs{ob} \to \fs{hom}$, $\pi_1,\pi_2 : \fs{hom} \times \fs{hom} \to \fs{hom}$, $\fs{pair} : \fs{hom} \times \fs{hom} \times \fs{hom} \times \fs{hom} \to \fs{hom}$ и следующие аксиомы:
\begin{align*}
& \sststile{}{x} d(!(x)) = x \land c(!(x)) = 1 \\
c(f) = 1 & \sststile{}{f} f =\ !(d(f)) \\
c(f) = c(g) & \ssststile{}{f,g} \pi_1(f,g)\!\downarrow \\
c(f) = c(g) & \ssststile{}{f,g} \pi_2(f,g)\!\downarrow \\
c(f) = c(g) & \sststile{}{f,g} c(\pi_1(f,g)) = d(f) \land c(\pi_2(f,g)) = d(g) \\
c(f) = c(g) & \sststile{}{f,g} d(\pi_1(f,g)) = d(\pi_2(f,g)) \\
\fs{pair}(a,b,f,g)\!\downarrow & \ssststile{}{f,g,a,b} d(a) = d(b) \land c(a) = d(f) \land c(b) = d(g) \land c(f) = c(g) \\
\fs{pair}(a,b,f,g)\!\downarrow & \sststile{}{f,g,a,b} \circ(\pi_1(f,g),\fs{pair}(a,b,f,g)) = a \\
\fs{pair}(a,b,f,g)\!\downarrow & \sststile{}{f,g,a,b} \circ(\pi_2(f,g),\fs{pair}(a,b,f,g)) = b \\
c(h) = d(\pi_1(f,g)) & \sststile{}{f,g,h} \fs{pair}(\circ(\pi_1(f,g),h),\circ(\pi_2(f,g),h),f,g) = h
\end{align*}
Модели этой теории -- это в точности конечно полные малые категории.
\end{example}

Правила вывода \emph{частичной хорновской логики} приведены ниже.
В этом подразделе мы приведем правила только для финитарных теорий, правила для произвольных будут приведены в следующем.
\emph{Теорема} теории -- это секвенция, выводимая из аксиом этой теории при помощи этих правил вывода.
Мы будем писать $\varphi \sststile{T}{V} \psi$ для обозначения того факта, что $\varphi \sststile{}{V} \psi$ является теоремой теории $T$.

\begin{center}
$\varphi \sststile{}{V} \varphi$ \axlabel{b1}
\qquad
\AxiomC{$\varphi \sststile{}{V} \psi$}
\AxiomC{$\psi \sststile{}{V} \chi$}
\RightLabel{\axlabel{b2}}
\BinaryInfC{$\varphi \sststile{}{V} \chi$}
\DisplayProof
\qquad
$\varphi \sststile{}{V} \top$ \axlabel{b3}
\end{center}

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

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

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V,x} \psi$}
\RightLabel{, $x \in \FV(\varphi)$ \axlabel{a3}}
\UnaryInfC{$\varphi[t/x] \sststile{}{V,V'} \psi[t/x]$}
\DisplayProof
\end{center}
\medskip

Эти правила немного отличаются от тех, что приведены в \cite{PHL}.
Правило вывода \axref{a3} там заменено на следующие правила вывода:
\begin{align*}
R(t_1, \ldots t_k) & \sststile{}{V} t_i\!\downarrow \axtag{a4} \\
t_1 = t_2 & \sststile{}{V} t_i\!\downarrow \axtag{a4'} \\
\sigma(t_1, \ldots t_k)\!\downarrow & \sststile{}{V} t_i\!\downarrow \axtag{a5}
\end{align*}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{x_1, \ldots x_n} \psi$}
\RightLabel{\axlabel{a3'}}
\UnaryInfC{$t_1\!\downarrow \land \ldots \land t_n\!\downarrow \land \varphi[t_1/x_1, \ldots t_n/x_n] \sststile{}{V} \psi[t_1/x_1, \ldots t_n/x_n]$}
\DisplayProof
\end{center}
\medskip

\begin{prop}
В присутствии остальных правил вывода, правило \axref{a3} эквивалентно правилам \axref{a3'}, \axref{a4}, \axref{a4'} и \axref{a5}.
\end{prop}
\begin{proof}
Так как секвенции $R(x_1, \ldots x_k) \sststile{}{V} x_i\!\downarrow$, $x_1 = x_2 \sststile{}{V} x_i\!\downarrow$ и $\sigma(x_1, \ldots x_k)\!\downarrow \sststile{}{V} x_i\!\downarrow$ выводимы из \axref{b2}, \axref{b3} и \axref{a1},
то \axref{a3} влечет \axref{a4}, \axref{a4'} и \axref{a5}.
Мы можем доказать, что \axref{a3'} выводимо индукцией по $n$.
Для этого достаточно показать, что следующее правило выводимо:
\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V,x} \psi$}
\UnaryInfC{$t\!\downarrow \land \varphi[t/x] \sststile{}{V} \psi[t/x]$}
\DisplayProof
\end{center}
\medskip
Для этого в правиле \axref{a3} достаточно в качестве $\varphi$ взять $x\!\downarrow \land \varphi$.

Теперь покажем, что \axref{a3} выводимо из правил \axref{a3'}, \axref{a4}, \axref{a4'} и \axref{a5}.
По \axref{a3'} из $\varphi \sststile{}{x_1, \ldots x_n, x} \psi$ выводится $x_1\!\downarrow \land \ldots \land x_n\!\downarrow \land t\!\downarrow \land \varphi[t/x] \sststile{}{x_1, \ldots x_n, V'} \psi[t/x]$.
По \axref{b2} и \axref{b6} нам достаточно показать, что $\varphi[t/x] \sststile{}{x_1, \ldots x_n, V'} x_i\!\downarrow$, $\varphi[t/x] \sststile{}{x_1, \ldots x_n, V'} t\!\downarrow$ и $\varphi[t/x] \sststile{}{x_1, \ldots x_n, V'} \varphi[t/x]$.
Первая секвенция следует из \axref{a1}, \axref{b2} и \axref{b3}, а последняя из \axref{b1}.
Докажем, что вторая секвенция выводится.
Если $\varphi$ -- это формула вида $R(t_1, \ldots t_k)$, то $x \in \FV(t_i)$ для некоторого $1 \leq i \leq k$.
По \axref{a4} верно, что $R(t_1[t/x], \ldots t_k[t/x]) \sststile{}{x_1, \ldots x_n, V'} t_i[t/x]\!\downarrow$
Если $\varphi$ -- это формула вида $t_1 = t_2$, то $x \in \FV(t_i)$ для некоторого $1 \leq i \leq 2$.
По \axref{a4'} верно, что $t_1[t/x] = t_2[t/x] \sststile{}{x_1, \ldots x_n, V'} t_i[t/x]\!\downarrow$.
По \axref{b2} достаточно доказать, что секвенция $t'[t/x]\!\downarrow\ \sststile{}{V} t\!\downarrow$ выводима для любого терма $t'$ такого, что $x \in \FV(t')$.
Это легко сделать индукцией по $t'$.
Если $t' = x$, то это верно по \axref{b1}.
Если $t' = \sigma(t_1, \ldots t_k)$, то $x \in \FV(t_i)$ для некоторого $1 \leq i \leq k$.
По \axref{a5} секвенция $\sigma(t_1[t/x], \ldots t_k[t/x])\!\downarrow\ \sststile{}{V} t_i[t/x]\!\downarrow$ выводима.
По индукционной гипотезе $t_i[t/x]\!\downarrow\ \sststile{}{V} t\!\downarrow$.
\end{proof}

Позже нам понадобится следующая лемма:

\begin{lem}[mcf]
Секвенция $\varphi \sststile{}{x_1, \ldots x_n} \psi$ доказуема в финитарной теории $T$ тогда и только тогда,
когда секвенция $\sststile{}{} \psi[c_1/x_1, \ldots c_n/x_n]$ доказуема в теории $T \cup \{ \sststile{}{} c_i\!\downarrow\ \mid 1 \leq i \leq n \} \cup \{ \sststile{}{} \varphi[c_1/x_1, \ldots c_n/x_n] \}$, где $c_1$, \ldots $c_n$ -- новые константы.
\end{lem}
\begin{proof}
Это следует из \cite[Theorem~10, Theorem~11]{PHL}.
\end{proof}

Мы будем говорить, что две теории \emph{эквивалентны}, если их множества функциональных символов, предикатных символов и теорем совпадают.

\subsection{Естественный вывод}

Позже мы встретим несколько утверждений, которые доказываются индукцией по выводу секвенции.
Мы будем работать с секвенциями, левая сторона которых обладает некоторым свойством, но в выводе секвенции в частичной хорновской логике левая сторона может варьироваться произвольным образом.
Таким образом, нам нужно описать эквивалентный набор правил вывода, в котором левая формула не менялась бы.
Мы будем называть эти правила \emph{естественным выводом}.
В этой системе правая сторона секвенций всегда является атомарной формулой.

\begin{center}
\AxiomC{}
\RightLabel{\axlabel{nv}}
\UnaryInfC{$\varphi \sststile{}{V} x\!\downarrow$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} t_1 = t_2$}
\RightLabel{\axlabel{ns}}
\UnaryInfC{$\varphi \sststile{}{V} t_2 = t_1$}
\DisplayProof
\end{center}
\medskip

\begin{center}
\AxiomC{}
\RightLabel{\axlabel{nh}}
\UnaryInfC{$\varphi_1 \land \ldots \land \varphi_n \sststile{}{V} \varphi_i$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} t_1 = t_2$}
\AxiomC{$\varphi \sststile{}{V} \psi[t_1/x]$}
\RightLabel{\axlabel{nl}}
\BinaryInfC{$\varphi \sststile{}{V} \psi[t_2/x]$}
\DisplayProof
\end{center}
\medskip

\begin{center}
\AxiomC{$\varphi \sststile{}{V} R(t_1, \ldots t_n)$}
\RightLabel{\axlabel{np}}
\UnaryInfC{$\varphi \sststile{}{V} t_i\!\downarrow$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} \sigma(t_1, \ldots t_n)\!\downarrow$}
\RightLabel{\axlabel{nf}}
\UnaryInfC{$\varphi \sststile{}{V} t_i\!\downarrow$}
\DisplayProof
\end{center}
где $R$ -- это предикатный символ теории, а $\sigma$ -- функциональный символ.

Наконец, для каждой аксиомы $\psi_1 \land \ldots \land \psi_n \sststile{}{x_1 : s_1, \ldots x_k : s_k} \chi_1 \land \ldots \land \chi_m$
и всех термов $t_1 : s_1$, \ldots $t_k : s_k$ мы добавляем следующее правило для всех $1 \leq j \leq m$:
\begin{center}
\AxiomC{$\varphi \sststile{}{V} t_i\!\downarrow$, $1 \leq i \leq k$}
\AxiomC{$\varphi \sststile{}{V} \psi_i[t_1/x_1, \ldots t_k/x_k]$, $1 \leq i \leq n$}
\RightLabel{\axlabel{na}}
\BinaryInfC{$\varphi \sststile{}{V} \chi_j[t_1/x_1, \ldots t_k/x_k]$}
\DisplayProof
\end{center}

\begin{prop}
Секвенция $\varphi \sststile{}{V} \psi_1 \land \ldots \land \psi_n$ выводима из правил \axref{b1}-\axref{b6}, \axref{a1}-\axref{a3} тогда и только тогда, когда
секвенции $\varphi \sststile{}{V} \psi_1$, \ldots $\varphi \sststile{}{V} \psi_n$ выводимы из правил естественного вывода.
\end{prop}
\begin{proof}
Легко доказать ``только тогда'' направление.
Наоборот, правила \axref{b1}, \axref{b4} и \axref{b5} следуют из \axref{nh},
правила \axref{b3} и \axref{b6} верны тривиально,
правило \axref{a1} следует из \axref{nv},
правило \axref{a2} следует из \axref{nl} и \axref{nh},
и аксиомы выводимы по \axref{na}.

Чтобы доказать правило \axref{b2}, нам достаточно показать, что если секвенции $\varphi \sststile{}{V} \psi_1$, \ldots $\varphi \sststile{}{V} \psi_n$
и $\psi_1 \land \ldots \land \psi_n \sststile{}{V} \chi$ выводимы в естественном выводе, то $\varphi \sststile{}{V} \chi$ также выводима.
Мы можем сконструировать дерево вывода для этой секвенции как дерево вывода для $\psi_1 \land \ldots \land \psi_n \sststile{}{V} \chi$,
в котором левая сторона каждой секвенции заменена на $\varphi$ и правила \axref{nh} заменены на деревья вывода для $\varphi \sststile{}{V} \psi_i$.

Чтобы доказать правило \axref{a3}, рассмотрим дерево вывода для секвенции $\varphi \sststile{}{V} \psi$.
Чтобы сконструировать дерево вывода для $\varphi[t/x] \sststile{}{V,V'} \psi[t/x]$, нам достаточно применить подстановку $t/x$ к каждой секвенции в этом дереве вывода.
Единственное правило, которое не замкнуто относительно подстановки, -- это \axref{nv}.
По предположению $x \in \FV(\varphi)$.
Это влечет, что $\varphi[t/x] \sststile{}{V,V'} t\!\downarrow$ выводима из \axref{np}, \axref{nf} и следующих правил:
\begin{center}
\AxiomC{$\varphi \sststile{}{V} t_1 = t_2$}
\RightLabel{\axlabel{ne1}}
\UnaryInfC{$\varphi \sststile{}{V} t_1\!\downarrow$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} t_1 = t_2$}
\RightLabel{\axlabel{ne2}}
\UnaryInfC{$\varphi \sststile{}{V} t_2\!\downarrow$}
\DisplayProof
\end{center}
Правило \axref{ne2} следует из \axref{nl} если мы возьмем $\psi(x)$ равным $x = b$.
Правило \axref{ne1} следует из \axref{ne2} и \axref{ns}.
\end{proof}

Теперь мы можем привести правила вывода для инфинитарных теорий.
Большинство правил вывода остаются прежними с очевидными поправками:

\begin{center}
\AxiomC{}
\RightLabel{\axlabel{iv}}
\UnaryInfC{$\varphi \sststile{}{V} x\!\downarrow$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} t_1 = t_2$}
\RightLabel{\axlabel{is}}
\UnaryInfC{$\varphi \sststile{}{V} t_2 = t_1$}
\DisplayProof
\qquad
\AxiomC{}
\RightLabel{\axlabel{ih}}
\UnaryInfC{$\bigwedge_{i \in I} \varphi_i \sststile{}{V} \varphi_i$}
\DisplayProof
\end{center}
\medskip

\begin{center}
\AxiomC{$\varphi \sststile{}{V} R(\{ t_i \}_i)$}
\RightLabel{\axlabel{ip}}
\UnaryInfC{$\varphi \sststile{}{V} t_i\!\downarrow$}
\DisplayProof
\qquad
\AxiomC{$\varphi \sststile{}{V} \sigma(\{ t_i \}_i)\!\downarrow$}
\RightLabel{\axlabel{if}}
\UnaryInfC{$\varphi \sststile{}{V} t_i\!\downarrow$}
\DisplayProof
\end{center}
где $R$ -- это предикатный символ теории, а $\sigma$ -- функциональный символ.

Для каждой аксиомы $\bigwedge_{i \in I} \psi_i \sststile{}{V} \bigwedge_{j \in J} \chi_j$
и всех термов $\{ t_i \}_{i \in V}$ мы добавляем следующее правило для всех $j \in J$:
\begin{center}
\AxiomC{$\varphi \sststile{}{V'} t_x\!\downarrow$, $x \in V$}
\AxiomC{$\varphi \sststile{}{V'} \psi_i[t_x/x,]$, $i \in I$}
\RightLabel{\axlabel{ia}}
\BinaryInfC{$\varphi \sststile{}{V'} \chi_j[t_x/x]$}
\DisplayProof
\end{center}

Правило \axref{nl} удобно разбить на несколько правил:

\begin{center}
\AxiomC{$\varphi \sststile{}{V} t_1 = t_2$}
\AxiomC{$\varphi \sststile{}{V} t_2 = t_3$}
\RightLabel{\axlabel{it}}
\BinaryInfC{$\varphi \sststile{}{V} t_1 = t_3$}
\DisplayProof
\end{center}
\medskip

\begin{center}
\AxiomC{$\varphi \sststile{}{V} a_i = b_i$, $i \in I$}
\AxiomC{$\varphi \sststile{}{V} \sigma(\{ a_i \}_i)\!\downarrow$}
\RightLabel{\axlabel{ic}}
\BinaryInfC{$\varphi \sststile{}{V} \sigma(\{ a_i \}_i) = \sigma(\{ b_i \}_i)$}
\DisplayProof
\end{center}
\medskip

\begin{center}
\AxiomC{$\varphi \sststile{}{V} a_i = b_i$, $i \in I$}
\AxiomC{$\varphi \sststile{}{V} R(\{ a_i \}_i)$}
\RightLabel{\axlabel{ii}}
\BinaryInfC{$\varphi \sststile{}{V} R(\{ b_i \}_i)$}
\DisplayProof
\end{center}
\medskip

Легко видеть, что в финитарном случае эти правила эквивалентны \axref{nl}.

\subsection{Классифицирующая категория теории}

В этом подразделе для каждой достижимой теории $T$ мы определим категорию $\cat{C}_T$, которая называется \emph{классифицирующей категорией} этой теории.

\emph{Производный сорт} некоторой теории -- это класс эквивалентности пар $(V,\varphi)$, состоящих из $\mathcal{S}$-множества $V$ и формулы $\varphi$ с переменными в $V$.
Мы будем записывать сорт, соответствующий такой паре как $\{ \overline{x} : \prod_{i \in I} s_i \mid \varphi(\overline{x}) \}$, где $V = \{ x_i : s_i \}_{i \in I}$.
Две такие пары $(V,\varphi)$ и $(V,\varphi')$ эквивалентны если формулы $\varphi$ и $\varphi'$ эквивалентны.
Если $s = (V,\varphi)$ -- производный сорт, то мы будем обозначать $V$ как $\FV(s)$.
Мы будем говорить, что производный сорт является \emph{$\lambda$-достижимым} для некоторого регулярного кардинала $\lambda$, если $|V| < \lambda$ и $\varphi = \bigwedge_{i \in I} \varphi_i$, где $|I| < \lambda$ и $\varphi_i$ -- атомарные формулы.

Пусть $\{ s_i \}_{i \in I}$ -- множество производных сортов таких, что $s_i = (V_i,\varphi_i)$ и $s = (W,\psi)$ -- еще один производный сорт.
Тогда \emph{суженный производный терм} $t$ сигнатуры $\prod_{i \in I} s_i \to s$ -- это пара, состоящая из $W$-множества термов $\{ t_k \}_{k \in W}$ и формулы $\chi$ с переменными в $\amalg_{i \in I} \FV(s_i)$, такая, что $t_k$ имеет сорт $s'_k$,
и выводима секвенция $\bigwedge_{k \in W} t_k\!\downarrow \land \chi \sststile{}{\amalg_{i \in I} \FV(s_i)} \psi[\{t_k/k\}_{k \in W}] \land \bigwedge_{i \in I} \varphi_i$
(мы будем говорить, что терм \emph{определен} в некоторой теории для обозначения того факта, что в ней выводима эта секвенция).
Мы будем записывать такую пару как $\{ t_k \}_{k \in W}|_\chi$ или просто $\{ t_k \}_k|_\chi$.
Если $W = \{ 1, \ldots k \}$, то такую пару можно записывать как $(t_1, \ldots t_k)|_\chi$.

Теперь мы можем определить классифицирующую категорию $\cat{C}_T$ теории $T$.
Объекты категории $\cat{C}_T$ -- это производные сорта $T$.
Морфизм между объектами $s = (V,\varphi)$ и $s' = (W,\psi)$ -- это класс эквивалентности производных термов $\{ t_k \}_{k \in W}$ сигнатуры $s \to s'$ таких,
что выводима секвенция $\varphi \sststile{}{\FV(s)} \bigwedge_{k \in W} t_k\!\downarrow$.
Два терма $\{ t_k \}_{k \in W}$ и $\{ t'_k \}_{k \in W}$ эквивалентны, если секвенция $\varphi \sststile{}{\FV(s)} \bigwedge_{k \in W} t_k = t'_k$ выводима.

Тождественный морфизм на объекте $\{ \overline{x} : \prod_{i \in I} s_i \mid \varphi \}$ -- это терм $\{ x_i \}_{i \in I}|_\varphi$.
Композиция следующих морфизмов
\begin{align*}
\{ t_j \}_{j \in J}|_\chi & : \{ \overline{x} : \prod_{i \in I} s_i \mid \varphi \} \to \{ \overline{x}' : \prod_{j \in J} s_j' \mid \varphi' \} \\
\{ t'_k \}_{k \in K}|_\chi' & : \{ \overline{x}' : \prod_{j \in J} s_j' \mid \varphi' \} \to \{ \overline{x}'' : \prod_{k \in K} s_k'' \mid \varphi'' \}
\end{align*}
задается как терм $\{ t'_k[\rho] \}_{k \in K}|_{\chi'[\rho] \land \chi \land \bigwedge_{j \in J} t_j \downarrow}$, где $\rho(j) = t_j$.
Легко видеть, что это определение корректно и действительно задает категорию.

\begin{remark}
На производные сорта можно смотреть как на модели $T$.
С этой точки зрения если $(V,\varphi)$ -- производный сорт, то $V$ -- это множество порождающих элементов модели, а $\varphi$ -- это множество соотношений.
Таким образом, если производный сорт является $\lambda$-достижимым, то соответствующая модель является $\lambda$-представимой.
\end{remark}

Категория $\cat{C}_T$ не является малой.
Если теория $T$ является $\lambda$-достижимой, то мы можем определить малую полную подкатегорию $\cat{C}_T^\lambda$ категории $\cat{C}_T$, состоящую из $\lambda$-достижимых производных сортов.
Часто под классифицирующей категорией теории $T$ подразумевают $\cat{C}_T^\lambda$, но мы будем называть такую каетегорию \emph{$\lambda$-классифицирующей},
так как любая $\lambda$-достижимая теория является $\mu$-достижимой для $\mu > \lambda$, но категории $\cat{C}_T^\lambda$ и $\cat{C}_T^\mu$ не эквивалентны, поэтому их необходимо различать.

\begin{remark}
Мы определяем $\lambda$-классифицирующую категорию только для теорий, являющихся $\lambda$-достижимыми,
так как только в этом случае эта категория содержит достаточно информации для восстановления по ней исходной теории.
\end{remark}

\begin{prop}[class-cat]
Категория $\cat{C}_T$ является полной, а в категрии $\cat{C}_T^\lambda$ существуют все $\lambda$-малые пределы.
Если $T$ является $\lambda$-достижимой теорией, то $\cat{C}_T^\fs{op}$ является локально $\lambda$-представимой категорией.
\end{prop}
\begin{proof}
Если $\{ t_i \}_{i \in I}|_\varphi$ и $\{ t_i' \}_{i \in I}|_{\varphi'}$ -- пара морфизмов сигнатуры $s \to s'$ в $\cat{C}_T$ или $\cat{C}_T^\lambda$,
то их уравнитель можно определить как сужение $s$ на формулу $\bigwedge_{i \in I} t_i = t_i'$.
Пусть $\{ s_i \}_{i \in I}$ -- множество производных сортов, где $s_i = (V_i,\varphi_i)$.
Тогда их произведение можно определить как $(\coprod_{i \in I} V_i, \bigwedge_{i \in I} \varphi_i[(i,x)/x])$.
Если $s_i$ -- объекты $\cat{C}_T^\lambda$ и $|I| < \lambda$, то это произведение также является объектом $\cat{C}_T^\lambda$, так как $\lambda$ -- регулярный кардинал.

Мы только что видели, что в $\cat{C}_T^\fs{op}$ существуют все копределы.
Так как любой объект этой категории является копределом сортов, нам достаточно доказать, что сорта являются $\lambda$-представимыми объектами в этой категории.
Это означает, что нам нужно показать, что следующая каноническая функция является биекцией для любого сорта $s$ и любой $\lambda$-направленной диаграммы $X : I \to \cat{C}_T^\fs{op}$.
\[ f : \colim_{i \in I} \Hom_{\cat{C}_T}(X_i, s) \to \Hom_{\cat{C}_T}(\fs{lim}_{i \in I}(X_i), s) \]

Предел $\fs{lim}_{i \in I}(X_i)$ может быть записан как $\{ \overline{x} : \prod_{i \in I} s_i \mid \varphi \}$, где $s_i$ -- производные сорта, и $\varphi$ -- некоторая формула.
Пусть $t$ -- суженный производный терм сигнатуры $\prod_{i \in I} s_i \to s$.
Так как символы теории $T$ являются $\lambda$-достижимыми, множество $i$ для которых переменные из $\FV(s_i)$ встречаются в $t$ имеет мощность $< \lambda$.
Так как $I$ является $\lambda$-направленным множеством, то отсюда следует, что $t$ эквивалентен терму вида $f(t')$.

Нам осталось доказать инъективность $f$.
Пусть $t,t'$ -- пара суженных производных термов сигнатуры $s_i \to s$ для некоторого $i \in I$ таких, что $\varphi \sststile{T}{\amalg_{i \in I} \FV(s_i)} t = t'$.
Так как теория $T$ является $\lambda$-достижимой, множество атомарных формул из $\varphi$, которые используются в этом выводе, имеет мощность $< \lambda$.
Так как каждая атомарная формула из $\varphi$ верна в $X_j$ для некоторого $j \in I$, и $I$ является $\lambda$-направленным множеством, то отсюда следует, что $t$ и $t'$ равны как элементы $\Hom_{\cat{C}_T}(X_j, s)$ для некоторого $j \in I$.
\end{proof}

\begin{remark}
В \pprop{cart-mod-dual} мы докажем, что категория $\cat{C}_T^\fs{op}$ эквивалентна категории моделей $T$.
\end{remark}

В \cite{PHL} приводится другое определение $\aleph_0$-классифицирующей категории для финитарных теорий.
Она определяется как начальный объект теории $\mathrm{Cart} \overline{\omega} T$.
Эта теория является расширением теории, описанной в \pexample{fc-cats}.
Для каждого сорта $s$ теории $T$ мы добавляем константу $\upgamma^s : \fs{ob}$ и аксиому $\sststile{}{} \upgamma^s\!\downarrow$.
Для каждого предикатного символа $R : s_1 \times \ldots \times s_n$ теории $T$ мы добавляем константу $\upgamma^R : \fs{hom}$
и аксиому $\sststile{}{} c(\upgamma^R) = \upgamma^{s_1} \times \ldots \times \upgamma^{s_n} \land \fs{Mon}(\upgamma^R)$,
где $X \times Y$ -- декартово произведение объектов, которое определяется очевидным образом в теории конечно полных категорий, и $\fs{Mon}(f)$ -- предикат,
утверждающий, что $f$ является мономорфизмом (это верно тогда и только тогда, когда $\pi_1(f,f) = \pi_2(f,f)$).
Для каждого функционального символа $\sigma : s_1 \times \ldots \times s_n \to s$ теории $T$ мы добавляем константы $\upgamma^\sigma_d, \upgamma^\sigma_m : \fs{hom}$ и аксиому
$\sststile{}{} c(\upgamma^\sigma_m) = \upgamma^{s_1} \times \ldots \times \upgamma^{s_n} \land c(\upgamma^\sigma_d) = \upgamma^s \land d(\upgamma^\sigma_d) = d(\upgamma^\sigma_m) \land \fs{Mon}(\upgamma^\sigma_m)$.
функциональный заключается в том, что $\upgamma^\sigma_m$ задает некоторый подобъект домена $\sigma$, а $\upgamma^\sigma_d$ является морфизмом из этого подобъекта в кодомен $\sigma$.
То есть такая пара морфизмов -- это в точности частичный морфизм из домена $\sigma$ в его кодомен.

В \cite[Section~8]{PHL} описана категориальная семантика частичных хорновских теорий.
В частности, она описывает интерпретацию термов и формул.
Если $V = \{ x_1 : s_1, \ldots x_n : s_n \}$ -- упорядоченное множество переменных, а $t$ -- терм сорта $s$ такой, что $\FV(t) \subseteq V$,
то категориальная семантика дает нам пару морфизмов $\upgamma^t_d$ и $\upgamma^t_m$, задающих частичный морфизм из $\upgamma^{s_1} \times \ldots \times \upgamma^{s_n} \to \upgamma^s$.
Если $\varphi$ -- формула такая, что $\FV(\varphi) \subseteq V$, то по категориальной семантике мы получаем мономорфизм $\gamma^\varphi$, задающий подобъект $\upgamma^{s_1} \times \ldots \times \upgamma^{s_n}$.

Для каждой аксиомы $a$ вида $\varphi \sststile{}{V} \psi$ мы добавляем константу $\upgamma^a : \fs{hom}$ и аксиому $\sststile{}{} \upgamma^\varphi = \circ(\upgamma^\psi,\upgamma^a)$.
Это завершает определение теории $\mathrm{Cart} \overline{\omega} T$.
Нам понадобятся следующие утверждения, доказанные в \cite[Lemma~39]{PHL}, \cite[Lemma~40]{PHL} и \cite[Theorem~41]{PHL}:

\begin{lem}[term-subst]
Если $V = \{ x_1 : s_1, \ldots x_n : s_n \}$ и $V' = \{ y_1 : s_1', \ldots y_k : s_k' \}$ -- два упорядоченных множества переменных, $t'$ -- терм такой, что $\FV(t') \subseteq V'$,
и $(t_1, \ldots t_k)$ -- список термов таких, что $\FV(t_i) \subseteq V$ и $t_i$ имеет сорт $s_i'$.
Тогда ограничение частичного морфизма $\upgamma^{t'[t_1/y_1, \ldots t_k/y_k] \land t_1 \land \ldots \land t_k}$ на пересечение подобъектов $\upgamma^{t_i}_m$ изоморфно композиции частичных морфизмов $\gamma^{\langle t_1, \ldots t_k \rangle}$ и $\gamma^{t'}$,
где $\gamma^{\langle t_1, \ldots t_k \rangle}$ -- это морфизм из пересечения подобъектов $\upgamma^{t_i}_m$, который задается как $\langle t_1, \ldots t_k \rangle$.
\end{lem}

\begin{lem}[form-subst]
Если $V = \{ x_1 : s_1, \ldots x_n : s_n \}$ и $V' = \{ y_1 : s_1', \ldots y_k : s_k' \}$ -- два упорядоченных множества переменных, $\psi$ -- формула такая, что $\FV(\psi) \subseteq V'$,
и $(t_1, \ldots t_k)$ -- список термов таких, что $\FV(t_i) \subseteq V$ и $t_i$ имеет сорт $s_i'$.
Тогда подобъект $\upgamma^{\psi[t_1/y_1, \ldots t_k/y_k] \land t_1 \land \ldots \land t_k}$ изоморфен $j \circ p$, где $j$ -- пересечение подобъектов $\upgamma^{t_i}_m$, а $p$ -- прообраз $\upgamma^\psi$ вдоль $\langle t_1, \ldots t_k \rangle$.
\end{lem}

\begin{thm}[phl-sound]
Если секвенция $\varphi \sststile{}{V} \psi$ выводима, то $\upgamma^\varphi$ является подобъектом $\upgamma^\psi$.
\end{thm}

Начальную модель этой теории мы будем обозначать $\cat{C}_T'$.
Определение моделей будет приведено в подразделе~\ref{sec:models}.
Теперь мы можем доказать, что эта категория эквивалентна $\aleph_0$-классифицирующей категории для финитарных теорий.
Мы не будем использовать это утверждение нигде в этом тексте, и оно приведено просто для демонстрации того, что два определения классифицирующей категории согласованы.

\begin{prop}
Для любой финитарной теории $T$ категории $\cat{C}_T^{\aleph_0}$ и $\cat{C}_T'$ эквивалентны.
\end{prop}
\begin{proof}
Во-первых, покажем, что $\cat{C}_T^{\aleph_0}$ является моделью $\mathrm{Cart} \overline{\omega} T$.
Эта категория конечно полная.
Действительно, $\{ () \mid \top \}$ является терминальным объектом.
Если $(t_1, \ldots t_k)|_\tau : \{ \overline{x} \mid \varphi \} \to \{ \overline{z} \mid \chi \}$ и $(t_1', \ldots t_k')|_{\tau'} : \{ \overline{y} \mid \psi \} \to \{ \overline{z} \mid \chi \}$ -- два морфизма в $\cat{C}_T^{\aleph_0}$,
то их послойное произведение можно определить как $\{ \overline{x}, \overline{y} \mid \varphi \land \psi \land t_1 = t_1' \land \ldots \land t_k = t_k' \}$.
Легко видеть, что этот объект обладает необходимым универсальным свойством.

Константа $\upgamma^s$ интерпретируется как $\{ x : s \mid \top \}$.
Константа $\upgamma^R$ интерпретируется как
\[ (x_1, \ldots x_n)|_{R(x_1, \ldots x_n)} : \{ (x_1, \ldots x_n) \mid R(x_1, \ldots x_n) \} \to \{ (x_1, \ldots x_n) \mid \top \}. \]
Константа $\upgamma^\sigma_m$ интерпретируется как
\[ (x_1, \ldots x_n)|_{\sigma(x_1, \ldots x_n) \downarrow} : \{ (x_1, \ldots x_n) \mid \sigma(x_1, \ldots x_n)\!\downarrow \} \to \{ (x_1, \ldots x_n) \mid \top \}. \]
Константа $\upgamma^\sigma_d$ интерпретируется как
\[ \sigma(x_1, \ldots x_n)|_{\sigma(x_1, \ldots x_n) \downarrow} : \{ (x_1, \ldots x_n) \mid \sigma(x_1, \ldots x_n)\!\downarrow \} \to \{ y \mid \top \}. \]
Чтобы проинтерпретировать константу $\upgamma^a$, соответствующую аксиоме $\varphi \sststile{}{V} \psi$, достаточно показать, что подобъект $\upgamma^\varphi$ вкладывается в $\upgamma^\psi$.
Для этого достаточно показать, что для любой формулы $\varphi$ подобъекты $\overline{x}|_\varphi : \{ \overline{x} \mid \varphi \} \to \{ \overline{x} \mid \top \}$ и $\upgamma^\varphi$ эквивалентны.
Легко индукцией по структуре терма $t$ показать, что подобъекты $\upgamma^t_m$ и $\overline{x}|_{t \downarrow} : \{ \overline{x} \mid t\!\downarrow \} \to \{ \overline{x} \mid \top \}$ эквивалентны
и $\upgamma^t_d$ соответствует морфизму $t : \{ \overline{x} \mid t\!\downarrow \} \to \{ y \mid \top \}$.
Используя этот факт, легко показать необходимое свойство формул.

Таким образом, $\cat{C}_T^{\aleph_0}$ действительно является моделью $\mathrm{Cart} \overline{\omega} T$.
Следовательно, существует уникальный функтор $F : \cat{C}_T' \to \cat{C}_T^{\aleph_0}$, являющийся морфизмом моделей.
Постороим функтор $G$ в обратную сторону.
Объект $\{ \overline{x} \mid \varphi \}$ отображается в $d(\gamma^\varphi)$.
Если $(t_1, \ldots t_k)|_\chi : \{ \overline{x} \mid \varphi \} \to \{ \overline{y} \mid \psi \}$ -- морфизм, то секвенция $\varphi \sststile{}{\overline{x}} \psi[t_1/y_1, \ldots t_k/y_k]$ выводима.
\Rthm{phl-sound} влечет, что $\upgamma^\varphi$ является подобъектом $\upgamma^{\psi[t_1/y_1, \ldots t_k/y_k]}$.
По \dlem{form-subst} у нас есть стрелка
\[ d(\upgamma^{\psi[t_1/y_1, \ldots t_k/y_k] \land t_1\!\downarrow \land \ldots \land t_k\!\downarrow}) \to d(\upgamma^\psi). \]
Мы определяем $G(t_1, \ldots t_k)$ как композицию этих двух стрелок.
Легко видеть, что $G$ сохраняет тождественные морфизмы.
\Rlem{term-subst} влечет, что $G$ сохраняет композицию.

Мы не можем воспользоваться универсальным свойством $\cat{C}_T'$, чтобы доказать, что $G \circ F = \fs{Id}$, так как $G$ не является морфизмом моделей $\mathrm{Cart} \overline{\omega} T$.
Вместо этого мы построим естественный изоморфизм между этими функторами.
Для этого мы определим частичную функцию $\alpha$ на замкнутых термах $t$ теории $\mathrm{Cart} \overline{\omega} T$ таких, что $\sststile{T}{} t\!\downarrow$.
Эта функция будет удовлетворять следующим условиям:
\begin{itemize}
\item Если $t$ имеет сорт $\fs{ob}$ и определен, то $\alpha_t$ -- это морфизм $GF(t) \to t$.
\item Если $t$ имеет сорт $\fs{hom}$ и определен, то $\alpha_t$ -- это пара морфизмов $\alpha_t^d : GF(d(t)) \to d(t)$ и $\alpha_t^c : GF(c(t)) \to c(t)$.
\end{itemize}
Функция $\alpha_t$ определяется рекурсией по $t$:
\begin{itemize}
\item $\alpha_{d(f)} = \alpha^d_f$ и $\alpha_{c(f)} = \alpha^c_f$.
\item $\alpha^d_{\mathrm{id}(x)} = \alpha^c_{\mathrm{id}(x)} = \alpha_x$.
\item $\alpha^d_{\circ(g,f)}$ и $\alpha^c_{\circ(g,f)}$ определены если $\sststile{\mathrm{Cart} \overline{\omega} T}{} \alpha^c_f = \alpha^d_g$.
В этом случае $\alpha^d_{\circ(g,f)} = \alpha^d_f$ и $\alpha^c_{\circ(g,f)} = \alpha^c_g$.
\item $\alpha^d_{!(x)} = \alpha_x$ и $\alpha^c_{!(x)} = \alpha_1 =\ !(GF(1))$.
\item $\alpha_{\pi_i(f_1,f_2)}$ определено если $\sststile{\mathrm{Cart} \overline{\omega} T}{} \alpha^c_{f_1} = \alpha^c_{f_2}$.
В этом случае $\alpha^d_{\pi_i(f_1,f_2)} = \fs{pair}(\circ(\alpha^d_{f_1},GF(\pi_1(f_1,f_2))),\circ(\alpha^d_{f_2},GF(\pi_2(f_1,f_2))),f_1,f_2)$ и $\alpha^c_{\pi_i(f_1,f_2)} = \alpha^d_{f_i}$.
\item $\alpha_{\fs{pair}(a,b,f,g)}$ определено если $\sststile{\mathrm{Cart} \overline{\omega} T}{} \alpha^d_a = \alpha^d_b \land \alpha^c_a = \alpha^d_f \land \alpha^c_b = \alpha^d_g \land \alpha^c_f = \alpha^c_g$.
В этом случае $\alpha^d_{\fs{pair}(a,b,f,g)} = \alpha^d_a$ и $\alpha^c_{\fs{pair}(a,b,f,g)} = \alpha^d_{\pi_1(f_1,f_2)}$.
\item Так как $GF(\upgamma^s) = \upgamma^s$, то мы можем определить $\alpha_{\upgamma^s}$ как $\mathrm{id}(\upgamma^s)$.
\item $GF(d(\upgamma^R)) = d(\upgamma^{R(x_1, \ldots x_n)})$. Этот объект изоморфен $d(\upgamma^R)$, так что мы можем определить $\alpha^d_{\upgamma^R}$ как этот изоморфизм.
Кроме того, мы определяем $\alpha^c_{\upgamma^R}$ как $\alpha_{\upgamma^{s_1} \times \ldots \times \upgamma^{s_n}}$.
\item Мы определяем $\alpha^d_{\upgamma^\sigma_m}$ и $\alpha^d_{\upgamma^\sigma_d}$ как изоморфизм между $d(\upgamma^{\sigma(x_1, \ldots x_n) \downarrow})$ и $d(\upgamma^\sigma)$.
Мы определяем $\alpha^c_{\upgamma^\sigma_m}$ как $\alpha_{\upgamma^{s_1} \times \ldots \times \upgamma^{s_n}}$ и $\alpha^c_{\upgamma^\sigma_d}$ как $\alpha_{\upgamma^s}$.
\item $\alpha^d_{\upgamma^a} = \alpha^d_{\upgamma^\varphi}$ и $\alpha^c_{\upgamma^a} = \alpha^d_{\upgamma^\psi}$.
\end{itemize}
Индукцией по естественному выводу секвенции $\sststile{}{} t = s$ легко показать, что $\alpha_t$ и $\alpha_s$ определены, если $t$ и $s$ имеют сорт $\fs{ob}$, то секвенция $\sststile{}{} \alpha_t = \alpha_s$ выводима,
и если $t$ и $s$ имеют сорт $\fs{hom}$, то секвенция $\sststile{}{} \alpha^d_t = \alpha^d_s \land \alpha^c_t = \alpha^c_s \land \circ(t,\alpha^d_t) = \circ(\alpha^c_t,GF(t))$ выводима.
Это влечет, что $\alpha$ задает естественное преобразование между функторами $G \circ F$ и $\fs{Id}$.
Легко видеть, что это преобразование является изоморфизмом.

Нам осталось доказать, что $F \circ G$ изоморфен $\fs{Id}$.
Пусть $X = \{ \overline{x} : \overline{s} \mid \varphi \}$ -- объект $\cat{C}_T^{\aleph_0}$.
Тогда $FG(X) = F(d(\upgamma_\varphi))$.
Мы уже видели в начале доказательства, что этот объект изоморфен исходному объекту $X$.
Легко видеть, что этот изоморфизм естественен.
\end{proof}

\subsection{Категория теорий}

В этом подразеделе мы определим категорию теорий, с которой мы будем работать на протяжении данного текста.
Нам понадобится ввести вспомогательные определения.
\emph{Суженный терм} -- это пара из терма $t$ и формулы $\varphi$.
Мы будем обозначать такой терм как $t|_\varphi$.
Если мы думаем о термах как о представлении частичных функций, то мы можем думать о суженном терме $t|_\varphi$ как о сужении частичной функции, представленной $t$, на пересечение ее домена и подмножества, представленного $\varphi$.
Любой терм $t$ является суженным термом $t|_\top$.

\begin{remark}
Мы определяли ранее понятие суженного производного терма.
Суженный терм сорта $s$ с переменными в $V$ -- это в точности суженный производный терм сигнатуры $V \to s$.
\end{remark}

Мы будем использовать следующие сокращения:
\begin{align*}
\varphi[ \{ t_i|_{\varphi_i}/x_i \}_{i \in \FV(\varphi)}] & = \varphi[\{ t_i/x_i \}_{i \in \FV(\varphi)}] \land \bigwedge_{i \in \FV(\varphi)} \varphi_i \\
t|_\varphi[ \{ t_i|_{\varphi_i}/x_i \}_{i \in \FV(t|_\varphi)}] & = t[\{ t_i/x_i \}_{i \in \FV(t)}]|_{\varphi[\{ t_i/x_i \}_{i \in \FV(\varphi)}] \land \bigwedge_{i \in \FV(t|_\varphi)} \varphi_i} \\
t|_\varphi|_\psi & = t|_{\varphi \land \psi} \\
R(\{ t_i|_{\varphi_i} \}_{i \in I}) & \Longleftrightarrow R(\{ t_i \}_{i \in I}) \land \bigwedge_{i \in I} \varphi_i \\
t|_\varphi = t'|_\psi & \Longleftrightarrow t = t' \land \varphi \land \psi \\
t|_\varphi\!\downarrow & \Longleftrightarrow t\!\downarrow\!\land \varphi \\
\chi \sststile{}{V} t|_\varphi \cong t'|_\psi & \Longleftrightarrow \chi \land t|_\varphi\!\downarrow\,\sststile{}{V} t = t' \land \psi \text{ и } \chi \land t'|_\psi\!\downarrow\,\sststile{}{V} t = t' \land \varphi
\end{align*}
Мы будем говорить, что формулы $\varphi$ и $\psi$ с переменными в $V$ эквивалентны, если следующая секвенция выводима:
\[ \varphi \ssststile{}{V} \psi \]
Мы будем говорить, что суженные термы $t$ и $t'$ с переменными в $V$ эквивалентны, если следующая секвенция выводима:
\[ \sststile{}{V} t \cong t' \]

Теперь мы можем определить категорию теорий с фиксированным множеством сортов.
Пусть $\Sigma = (\mathcal{S},\mathcal{F},\mathcal{P})$ и $\Sigma' = (\mathcal{S}',\mathcal{F}',\mathcal{P}')$ -- две сигнатуры с одинаковым множеством сортов.
Тогда \emph{интерпретация} $\Sigma$ в $\Sigma'$ -- это функция, сопоставляющая каждому сорту из $\mathcal{S}$ сорт из $\mathcal{S}'$, каждому функциональному символу $\sigma \in \mathcal{F}$, $\sigma : \prod_{i \in I} s_i \to s$,
суженный терм $f(\sigma)$ в $\Sigma'$ сорта $s$ с переменными в $I$, и каждому предикатному символу $R \in \mathcal{P}$, $R : \prod_{i \in I} s_i$, формулу $f(R)$ в $\Sigma'$ с переменными в $I$.

Пусть $f$ -- интерпретация $\Sigma$ в $\Sigma'$.
Тогда для любого терма $t$ в $\Sigma$ мы можем определить суженный терм $f(t)$ в $\Sigma'$.
Если $t = x$ -- переменная, то $f(t) = x$.
Если $t = \sigma(\{ t_i \}_{i \in I})$, то $f(t) = f(\sigma)[\{ f(t_i)/i \}_{i \in I}]|_{\bigwedge_{i \in I} f(t_i) \downarrow}$.
Для любой формулы $\varphi$ в $\Sigma$ мы можем определить формулу $f(\varphi)$ в $\Sigma'$.
Если $\varphi = (t = t')$, то $f(\varphi) = (f(t) = f(t'))$.
Если $\varphi = R(\{ t_i \}_{i \in I})$, то $f(\varphi) = f(R)[\{ f(t_i)/i \}_{i \in I}] \land \bigwedge_{i \in I} f(t_i)\!\downarrow$.

Пусть $T$ и $T'$ -- пара теорий.
Тогда \emph{интерпретация} $T$ в $T'$ -- это интерпретация $f$ сигнатуры $T$ в сигнатуре $T'$ такая,
что для любой аксиомы $\varphi \sststile{}{V} \psi$ теории $T$ секвенция $f(\varphi) \sststile{}{V} f(\psi)$ выводима в $T'$.
Мы будем говорить, что интерпретации $f$ и $f'$ \emph{эквивалентны}, если для всех функциональных символов $\sigma$ термы $f(\sigma)$ и $f'(\sigma)$ эквивалентны и для всех предикатных символов $R$ формулы $f(R)$ и $f(R')$ тоже эквивалентны.
\emph{Морфизм} теорий $T$ и $T'$ -- это класс эквивалентности интерпретаций.

Тождественные морфизмы определяются очевидным образом.
Композиция морфизмов $f : T \to T'$ и $g : T' \to T''$ определяется следующим образом: $(g \circ f)(S) = g(f(S))$ для всех символов $S$ теории $T$.
Легко индукцией по $t$ показать, что если $g$ и $g'$ эквивалентны, то $g(t)$ и $g'(t)$ тоже эквивалентны.
Кроме того, легко индукцией по выводу показать, что если $\varphi \sststile{}{V} \psi$ выводима, то $g(\varphi) \sststile{}{V} g(\psi)$ тоже выводима.
Из этих двух фактов следует, что композиция определена корректно.

Очевидно, что для любого морфизма теорий $f : T \to T'$ у нас есть равенства $f \circ \fs{id}_T = \fs{id}_{T'} \circ f = f$.
Индукцией по терму $t$ легко показать, что для всех морфизмов теорий $f : T \to T'$ и $g : T' \to T''$ суженные термы $g(f(t))$ и $(g \circ f)(t)$ эквивалентны.
Аналогично для каждой формулы $\varphi$ теории $T$ формулы $g(f(\varphi))$ и $(g \circ f)(\varphi)$ эквивалентны.
Из этих двух фактов следует, что композиция морфизмов теорий ассоциативна.
Категория теорий будет обозначаться как $\Th$.

\begin{remark}
Категория $\Th$ является локально малой.
Это не очевидно, так как класс формул не образует множество.
Так как мы рассматриваем формулы только с точности до эквивалентности, то можно считать, что атомарные подформулы в формуле не повторяются.
Локальная малость следует из того факта, что класс формул с таким свойством образует множество.
\end{remark}

Мы будем говорить, что интерпретация теорий $f : T \to T'$ является \emph{$\lambda$-достижимой}, если $T$ и $T'$ являются $\lambda$-достижимыми, для всех предикатных символов $R$ теории $T$ формула $f(R)$ является $\lambda$-достижимой
и для всех функциональных символов $\sigma$ теории $T$, если $f(\sigma) = t|_\varphi$, то формула $\varphi$ является $\lambda$-достижимой.
Морфизм теорий является \emph{$\lambda$-достижимым}, если он является классом эквивалентности некоторой $\lambda$-достижимой интерпретации.
Категорию $\lambda$-достижимых теорий и $\lambda$-достижимых морфизмов мы будем обозначать как $\Th^\lambda$.

Пусть $f : \mathcal{S} \to \mathcal{S}'$ -- некоторая функция, и $B = (\mathcal{S},\mathcal{F},\mathcal{P},\mathcal{A})$ -- некоторая теория.
Тогда мы можем определить теорию $f^*(B)$ как $(\mathcal{S}',\mathcal{F},\mathcal{P},\mathcal{A})$,
где для любого функционального символа $\sigma : \prod_{i \in I} s_i \to s$ из $B$ мы добавляем функциональный символ $\sigma : \prod_{i \in I} f(s_i) \to f(s)$ и аналогично для предикатных символов.
Мы будем говорить, что морфизм теорий $f : B \to T$ является \emph{расширением} $B$, если $T$ содержит $f^*(B)$ как подтеорию.
Морфизмы расширений -- это морфизмы теорий, сохраняющие символы из $B$.

\begin{lem}[th-ext]
Для любой теории $B$ категория $B/\Th$ эквивалентна категории расширений $B$.
\end{lem}
\begin{proof}
Очевидно, что категория расширений вкладывается в $B/\Th$.
Если $f : B \to T$ -- некоторая теория под $B$, то она изоморфна $i : B \to (\mathcal{S}', \mathcal{F}_B \amalg \mathcal{F}_T, \mathcal{P}_B \amalg \mathcal{P}_T, \mathcal{A}_B \amalg \mathcal{A}_T \amalg \mathcal{A})$,
где $i$ -- очевидное вложение, и $\mathcal{A}$ состоит из следующих аксиом:
\[ \sststile{}{V} f(\sigma(V)) \cong \sigma(V) \]
для всех $\sigma \in \mathcal{F}_B$ и
\[ f(R(V)) \ssststile{}{V} R(V) \]
для всех $R \in \mathcal{P}_B$.
\end{proof}

Часто бывает полезно рассматривать теории с фиксированным множеством сортов.
Для этого мы определим категорию таких теорий.
Пусть $T_\mathcal{S} = (\mathcal{S},\varnothing,\varnothing,\varnothing)$.
Полную подкатегорию $T_\mathcal{S}/\Th$, состоящую из расширений с множеством сортов $\mathcal{S}$, мы будем обозначать $\Th_\mathcal{S}$.
Подкатегорию $\Th_\mathcal{S}$, состоящую из $\lambda$-достижимых теорий и $\lambda$-достижимых морфизмов, мы будем обозначать $\Th_\mathcal{S}^\lambda$.

\begin{prop}[th-colimits]
Категории $\Th$, $\Th_\mathcal{S}$, $\Th^\lambda$ и $\Th_\mathcal{S}^\lambda$ кополны.
\end{prop}
\begin{proof}
Покажем сначала, что в категориях $\Th$ и $\Th^\lambda$ есть копроизведения.
Пусть $\{ T_i \}_{i \in I} = \{ (\mathcal{S}_i,\mathcal{F}_i,\mathcal{P}_i,\mathcal{A}_i) \}_{i \in I}$ -- множество теорий.
Тогда мы можем определить их копроизведение как теорию
\[ (\coprod\limits_{i \in I} \mathcal{S}_i, \coprod\limits_{i \in I} \mathcal{F}_i, \coprod\limits_{i \in I} \mathcal{P}_i, \coprod\limits_{i \in I} \mathcal{A}_i). \]
Легко видеть, что универсальное свойство копроизведений выполнено для этого расширения.
Если все теории $T_i$ были $\lambda$-достижимыми, то и их копроизведение будет таковым, так как любой его символ принадлежит одной из теорий $T_i$, и то же самое верно для аксиом.

Конструкция копроизведений в $\Th_\mathcal{S}$ и $\Th_\mathcal{S}^\lambda$ аналогична.
Пусть $\{ T_i \}_{i \in I} = \{ (\mathcal{S},\mathcal{F}_i,\mathcal{P}_i,\mathcal{A}_i) \}_{i \in I}$ -- множество теорий.
Тогда мы можем определить их копроизведение в $\Th_\mathcal{S}$ как теорию
\[ (\mathcal{S}, \coprod\limits_{i \in I} \mathcal{F}_i, \coprod\limits_{i \in I} \mathcal{P}_i, \coprod\limits_{i \in I} \mathcal{A}_i). \]
Легко видеть, что универсальное свойство копроизведений выполнено для этого расширения.
Если все теории $T_i$ были $\lambda$-достижимыми, то и их копроизведение будет таковым.

Коуравнители строятся во всех категориях одинаково.
Пусть $f,g : T_1 \to T_2$ -- пара морфизмов теорий $T_1 = (\mathcal{S}_1,\mathcal{F}_1,\mathcal{P}_1,\mathcal{A}_1)$ и $T_2 = (\mathcal{S}_2,\mathcal{F}_2,\mathcal{P}_2,\mathcal{A}_2)$.
Пусть $e : \mathcal{S}_2 \to \mathcal{S}$ -- коуравнитель функций $f,g : \mathcal{S}_1 \to \mathcal{S}_2$.
Тогда мы можем определить коуравнитель $f$ и $g$ как расширение теории $e^*(T_2)$, к которой мы добавляем следующие аксиомы:
$\sststile{}{V} f(\sigma(V)) \cong g(\sigma(V))$ для каждого функционального символа $\sigma \in \mathcal{F}_1$
и $f(R(V)) \ssststile{}{V} g(R(V))$ для каждого предикатного символа $R \in \mathcal{P}_1$.
Морфизм $e : T_2 \to T$ определяется тождественным образом.
Легко видеть, что этот морфизм обладает универсальным свойством коуравнителей.
Если $T_2,f,g$ являются $\lambda$-достижимым, то все новые аксиомы $T$ и сама $T$ тоже будут таковыми.
\end{proof}

\begin{remark}[th-coproducts]
Копроизведение расширений $\{ T_i \}_{i \in I} = \{ (\mathcal{S}, \mathcal{F}_B \amalg \mathcal{F}_i, \mathcal{P}_B \amalg \mathcal{P}_i, \mathcal{A}_B \amalg \mathcal{A}_i) \}_{i \in I}$
некоторой теории $B$ в $B/\Th_\mathcal{S}$ и $B/\Th_\mathcal{S}^\lambda$ может быть описано явным образом как теория
$(\mathcal{S}, \mathcal{F}_B \amalg \coprod\limits_{i \in I} \mathcal{F}_i, \mathcal{P}_B \amalg \coprod\limits_{i \in I} \mathcal{P}_i, \mathcal{A}_B \amalg \coprod\limits_{i \in I} \mathcal{A}_i)$.
\end{remark}

\begin{prop}[th-pres]
Пусть $\lambda$ -- регулярный кардинал
Категория $\Th^\lambda$ является локально $\lambda$-представимой.
Если $\lambda \leq \kappa$, то теория является $\kappa$-представимой тогда и только тогда,
когда она изоморфна теории $(\mathcal{S}',\mathcal{F}',\mathcal{P}',\mathcal{A}')$ такой, что $|\mathcal{S}'| < \kappa$, $|\mathcal{F}'| < \kappa$, $|\mathcal{P}'| < \kappa$ и $|\mathcal{A}'| < \kappa$.

Для категории $\Th_\mathcal{S}^\lambda$ верно более сильное утверждение.
Пусть $B = (\mathcal{S},\mathcal{F},\mathcal{P},\mathcal{A})$ -- $\lambda$-достижимая теория.
Категория $B/\Th_\mathcal{S}^\lambda$ является локально $\lambda$-представимой.
Если $\lambda \leq \kappa$, то объект этой категории является $\kappa$-представимым тогда и только тогда,
когда он изоморфен расширению $B \to (\mathcal{S}, \mathcal{F} \amalg \mathcal{F}', \mathcal{P} \amalg \mathcal{P}', \mathcal{A} \amalg \mathcal{A}')$ такому, что $|\mathcal{F}'| < \kappa$, $|\mathcal{P}'| < \kappa$ и $|\mathcal{A}'| < \kappa$.
\end{prop}
\begin{proof}
В рамках данного доказательства теории $(\mathcal{S}',\mathcal{F}',\mathcal{P}',\mathcal{A}')$ и расширения $B \to (\mathcal{S}', \mathcal{F} \amalg \mathcal{F}', \mathcal{P} \amalg \mathcal{P}', \mathcal{A} \amalg \mathcal{A}')$ такие,
что $|\mathcal{F}'| < \kappa$, $|\mathcal{P}'| < \kappa$ и $|\mathcal{A}'| < \kappa$, мы будем называть $\kappa$-малыми.

Заметим, что каждый терм и каждая $\lambda$-достижимая формула любой $\lambda$-достижимой теории составлен(а) из множества функциональных и предикатных символов и переменных, мощность которого меньше $\lambda$.
Кроме того, если $\varphi$ и $\psi$ -- $\lambda$-достижимые формулы,
то любой вывод теоремы $\varphi \sststile{}{V} \psi$ в $\lambda$-достижимой теории сконструировн из множества функциональных символов, предикатных символов и аксиом, мощность которого меньше $\lambda$.

Докажем, что любая $\kappa$-малая теория $\kappa$-представима если $\lambda \leq \kappa$.
Пусть $h : T \to \colim_{j \in J} T_j$ -- морфизм в $\Th^\lambda$, где $T = (\mathcal{S}',\mathcal{F}',\mathcal{P}',\mathcal{A}')$ -- $\kappa$-малая теория, а $\colim_{j \in J} T_j$ -- $\kappa$-направленный копредел теорий в $\Th^\lambda$.
Так как $\colim_{j \in J} T_j$ -- $\lambda$-достижимая теория, то для каждого функционального символа $\sigma \in \mathcal{F}'$ существует суженный терм некоторой теории $T_j$, эквивалентный $h(\sigma)$.
То же верно для предикатных символов из $\mathcal{P}'$.
Кроме того, для любой аксиомы $\varphi \sststile{}{V} \psi$ из $\mathcal{A}'$ существует теория $T_j$, в которой выводима секвенция $h(\varphi) \sststile{}{V} h(\psi)$.
Так как $|\mathcal{S}'| < \kappa$, $|\mathcal{F}'| < \kappa$, $|\mathcal{P}'| < \kappa$ и $|\mathcal{A}'| < \kappa$, то существует теория $T_j$, в которой определены все необхоидмые сорта, термы, формулы и выводимы все теоремы.
Таким образом, $h$ факторизуется через $T_j$.

Пусть $h_1,h_2 : T \to T_j$ -- морфизмы такие, что $g_j \circ h_1 = g_j \circ h_2$, где $g_j : T_j \to \colim_{j \in J} T_j$.
Тогда для каждого $\sigma \in \mathcal{F}'$ секвенция
\[ \sststile{}{V} h_1(\sigma(V)) \cong h_2(\sigma(V)) \]
является теоремой $\colim_{j \in J} T_j$.
Но мы уже видели, что отсюда следует, что существует теория $T_{j'}$ такая, что $j \leq j'$ и эта секвенция выводима в $T_{j'}$.
То же верно и для предикатных символов и сортов $T$.
Отсюда следует, что $f \circ h_1 = f \circ h_2$, где $f : T_j \to T_{j'}$.

Аналогичный аргумент показывает, что любое $\kappa$-малое расширение $B \to T$ является $\kappa$-представимым.
Если $T = (\mathcal{S}, \mathcal{F} \amalg \mathcal{F}', \mathcal{P} \amalg \mathcal{P}', \mathcal{A} \amalg \mathcal{A}')$, то мы должны рассмотреть только как отбражаются символы из $\mathcal{F}'$ и $\mathcal{P}'$ и аксиомы из $\mathcal{A}'$.
Условие малости на эти множества как и раньше гарантирует, что $\Hom(T,-)$ сохраняет $\kappa$-направленные копределы.

Теперь докажем, что категория $\Th^\lambda$ является локально $\lambda$-представимой.
Нам необходимо показать, что каждая теория в этой категории является $\lambda$-направленным копределом малого множества $\lambda$-представимых теорий.
Мы докажем более общее утверждение, что для любого регулярного $\kappa \geq \lambda$ каждая теория является $\kappa$-направленным копределом ее $\kappa$-малых подтеорий.
Пусть $T$ -- $\lambda$-достижимая теория и $\{ f_i : T_i \to T' \}_{i \in I}$ -- коконус над диаграммой $\kappa$-малых подтеорий $T$.
Для каждого сорта $s$ теории $T$ мы определим подтеорию $T_s$ теории $T$ как теорию, состоящую из одного сорта $s$.
Морфизм коконусов $h : T \to T'$ должен коммутировать с морфизмами $T_s \to T$.
Следовательно, он должен быть определен на сортах как $h(s) = f_{T_s}(s)$.

Для каждого символа $p$ теории $T$ мы определим подтеорию $T_p$ теории $T$ как теорию, состоящую из одного символа $p$ и всех сортов, которые появляются в сигнатуре $p$.
Морфизм коконусов $h : T \to T'$ должен коммутировать с морфизмами $T_p \to T$.
Следовательно, он должен быть определен как $h(p(V)) = f_{T_p}(p(V))$, а значит он уникален.
Чтобы доказать, что это определение задает морфизм, нам нужно показать, что $h$ сохраняет аксиомы $T$.
Мы уже видели, что любая аксиома $T$ должна принадлежать некоторой $\kappa$-малой подтеории $T_i$ теории $T$.
Так как $f_i$ -- морфизм теорий, эта аксиома также выводима и в $T'$.

Аналогичным образом доказывается, что категория $B/\Th_\mathcal{S}^\lambda$ является локально $\lambda$-представимой.
Для любого регулярного $\kappa \geq \lambda$ каждое расширение $B \to T$ является $\kappa$-направленным копределом его $\kappa$-малых подрасширений.
Вместо теорий $T_p$ мы рассматриваем подрасширения $B \amalg \{ p \}$ расширения $B \to T$.
Остальное доказательство полностью аналогично.

Нам осталось доказать, что любая $\kappa$-представимая теория $T$ изоморфна $\kappa$-малой, и аналогичное утверждение для расширений.
Так как $T$ является $\kappa$-направленным копределом ее $\kappa$-малых подтеорий, то $\fs{id}_T$ факторизуется через некоторую $\kappa$-малую подтеорию $T'$ теории $T$.
Таким образом, $T$ является коуравнителем пары морфизмов $T' \to T'$.
В \pprop{th-colimits} был сконструирован коуравнитель любой пары стрелок $f,g : X \to Y$, который является $\kappa$-малым, если обе теории $X$ и $Y$ являются таковыми.
Для расширений доказательство аналогично.
\end{proof}

\begin{prop}[th-adj]
В следующей диграмме, состоящей из функторов вложения подкатегорий, все функторы являются левыми сопряженными:
\[ \xymatrix{ \Th_\mathcal{S}^\lambda \ar[r] \ar[d] & T_\mathcal{S}/\Th^\lambda \ar[d] \\
              \Th_\mathcal{S}         \ar[r]        & T_\mathcal{S}/\Th
            } \]
Функторы $\Th^\lambda \to \Th$ и $\Th^\lambda \to \Th^\mu$ для $\lambda \leq \mu$ также являются левыми сопряженными.
\end{prop}
\begin{proof}
Конструкция копределов в \pprop{th-colimits} и \premark{th-coproducts} показывает, что все эти функторы сохраняют копределы.
По \dprop{th-pres} категории $\Th^\lambda$ и $\Th_\mathcal{S}^\lambda$ локально представимы.
По теореме о сопряженных функторах отсюда следует, что все функторы кроме $\Th_\mathcal{S} \to T_\mathcal{S}/\Th$ являются левыми сопряженными.
Докажем, что и этот функтор является левым сопряженным.

Пусть $T$ -- $\lambda$-достижимая теория с множеством сортов $\mathcal{S}'$ и функцией $f : \mathcal{S} \to \mathcal{S'}$.
Тогда мы определим теорию $R(T)$ с множеством сортов $\mathcal{S}$.
Для каждого множества $I < \lambda$, каждой коллекции сортов $\{ s_i \}_{i \in I}$ из $\mathcal{S}$, каждого сорта $s \in \mathcal{S}$ и каждого суженного терма $T$ сигнатуры $\prod_{i \in I} f(s_i) \to f(s)$
мы добавляем функциональный символ в $R(T)$ сигнатуры $\prod_{i \in I} s_i \to s$.
Для каждого множества $I < \lambda$, каждой коллекции сортов $\{ s_i \}_{i \in I}$ из $\mathcal{S}$ и каждой формулы $T$ сигнатуры $\prod_{i \in I} f(s_i)$
мы добавляем предикатный символ в $R(T)$ сигнатуры $\prod_{i \in I} s_i$.
Теперь можно определить морфизм теорий $\epsilon_T : R(T) \to T$, который отображает сорт $s$ в $f(s)$ и каждый символ в него же самого.
Теперь мы добавляем в $R(T)$ все аксиомы $\varphi \sststile{}{V} \psi$ для которых секвенция $\epsilon_T(\varphi) \sststile{}{f(V)} \epsilon_T(\psi)$ является теоремой в $T$.
Тогда $\epsilon_T$ всё еще остается морфизмом теорий.

Пусть $T'$ -- теория с множеством сортов $\mathcal{S}$ и $f : T' \to T$ -- морфизм в $T_\mathcal{S}/\Th$.
Нам нужно показать, что существует уникальный морфизм $g : T' \to R(T)$ в $\Th_\mathcal{S}$ такой, что $\epsilon_T \circ g = f$.
Для каждого символа $p$ теории $T'$ мы определяем $g(p)$ как $f(p)$.
Тогда по определению $\epsilon_T \circ g = f$.
Отсюда следует, что $g$ отображает аксиомы $T'$ в секвенции, которые становятся теоремами в $T$, то есть в аксиомы $R(T)$.
Таким образом, $g$ является морфизмом, удовлетворяющим необходимому условию.
Покажем теперь, что такой морфизм уникален.
Пусть $g,h : T' \to R(T)$ -- морфизмы такие, что $\epsilon_T \circ g = \epsilon_T \circ h$.
Тогда для любого предикатного символа $R$ теории $T'$ формулы $\epsilon_T(g(R))$ и$\epsilon_T(h(R))$ эквивалентны.
Отсюда следует, что $g(R)$ и $h(R)$ тоже эквивалентны.
Аналогичное утверждение верно и для функциональных символов.
Таким образом, $g = h$.
\end{proof}

Теперь мы докажем несколько фактов про мономорфизмы и регулярные эпиморфизмы в категориях теорий.

\begin{prop}[th-mono]
Морфизм теорий $f : T_1 \to T_2$ (в любой из категорий $\Th$, $\Th_\mathcal{S}$) является мономорфизмом тогда и только тогда,
когда он инъективен на сортах и отражает теоремы, другими словами, когда для всех секвенций $\varphi \sststile{}{V} \psi$ теории $T_1$
если секвенция $f(\varphi) \sststile{}{V} f(\psi)$ является теоремой $T_2$, то секвенция $\varphi \sststile{}{V} \psi$ является теоремой $T_1$.

Морфизм $\lambda$-достижимых теорий (в любой из категорий $\Th^\lambda$, $\Th_\mathcal{S}^\lambda$) является мономорфизмом тогда и только тогда, когда он инъективен на сортах и отражает $\lambda$-достижимые теоремы.
\end{prop}
\begin{proof}
Во-первых, докажем часть ``тогда''.
Пусть $g,h : T \to T_1$ -- пара морфизмов таких, что $f \circ g = f \circ h$.
Если $s$ -- сорт $T$, то $f(g(s)) = f(h(s))$.
Так как $f$ инъективен на сортах, то $g(s) = h(s)$.
Если $\sigma$ -- функциональный символ теории $T$, то $\sststile{}{V} f(g(\sigma(V))) \cong f(h(\sigma(V)))$. и, следовательно, $\sststile{}{V} g(\sigma(V)) \cong h(\sigma(V))$.
Если $R$ -- предикатный символ теории $T$, то $f(g(R(V))) \ssststile{}{V} f(h(R(V)))$, и, следовательно, $g(R(V)) \ssststile{}{V} h(R(V))$.
Таким образом, $g = h$.
Если $T$, $g$ и $h$ являются $\lambda$-достижимыми, то секвенции $\sststile{}{V} g(\sigma(V)) \cong h(\sigma(V))$ и $g(R(V)) \ssststile{}{V} h(R(V))$ также являются таковыми, а значит это доказательство верно и для категорий $\lambda$-достижимых теорий.

Теперь докажем часть ``только тогда''.
Пусть $f$ -- мономорфизм.
Если $f$ -- морфизм в $\Th_\mathcal{S}$, то он всегда инъективен на сортах.
В противном случае пусть $s,s'$ -- пара сортов $T_1$ таких, что $f(s) = f(s')$.
Пусть $g,h : (\{x\},\varnothing,\varnothing,\varnothing) \to T_1$ -- пара морфизмов таких, что $g(x) = s$ и $h(x) = s'$.
Тогда $f \circ g = f \circ h$.
Так как $f$ мономорфизм, то $g = h$, то есть $s = s'$.

Пусть $\varphi \sststile{}{V} \psi$ -- секвенция теории $T_1$ такая, что $f(\varphi) \sststile{}{V} f(\psi)$ -- теорема теории $T_2$.
Пусть $T$ -- теория, состоящая из единственного предикатного символа $R : \prod V$.
Пусть $g : T \to T_1$ -- морфизм, определенный как $g(R(V)) = \varphi \land V\!\downarrow$, и пусть $h : T \to T_1$ -- морфизм, определенный как $h(R(V)) = \varphi \land \psi \land V\!\downarrow$.
Тогда $f \circ g = f \circ h$, и, следовательно, $g = h$, что влечет, что $\varphi \sststile{T_1}{V} \psi$.
\end{proof}

\begin{prop}[th-epi]
Морфизм теорий $f : (\mathcal{S},\mathcal{F},\mathcal{P},\mathcal{A}) \to T$ (в любой из категорий $\Th$, $\Th_\mathcal{S}$) является регулярным эпиморфизмом тогда и только тогда,
когда он сюръективен на сортах и изоморфен расширению вида $(\mathcal{S},\mathcal{F},\mathcal{P},\mathcal{A}) \to (\mathcal{S}',\mathcal{F},\mathcal{P},\mathcal{A} \cup \mathcal{A}')$.

В категориях $\Th^\lambda$, $\Th_\mathcal{S}^\lambda$ морфизм $f$ является регулярным эпиморфизмом тогда и только тогда,
когда он изоморфен расширению вида, указанному выше, в котором $\mathcal{A}'$ состоит из $\lambda$-достижимых секвенций.
\end{prop}
\begin{proof}
Коуравнитель такого вида можно сконструировать для любой пары стрелок как было показано в \pprop{th-colimits}.
Наоборот, покажем, что расширение такого вида является регулярным эпиморфизмом.
Пусть $\mathcal{P}'$ -- множество предикатных символов вида $R_{V,\varphi,\psi} : \prod V$ для всех секвенций $\varphi \sststile{}{V} \psi$ в $\mathcal{A}'$.
Тогда мы можем определить морфизмы $f,g : (\mathcal{S},\mathcal{F},\mathcal{P} \amalg \mathcal{P}',\mathcal{A}) \to (\mathcal{S},\mathcal{F},\mathcal{P},\mathcal{A})$
как $f(R_{V,\varphi,\psi}) = \varphi \land V\!\downarrow$ и $g(R_{V,\varphi,\psi}) = \varphi \land \psi \land V\!\downarrow$ и тождественным образом на остальных символах.
Тогда расширение $(\mathcal{S},\mathcal{F},\mathcal{P},\mathcal{A}) \to (\mathcal{S},\mathcal{F},\mathcal{P},\mathcal{A} \cup \mathcal{A}')$ является коуравнителем этих морфизмов.
Если секвенции в $\mathcal{A}'$ являются $\lambda$-достижимыми, то символы в $\mathcal{P}'$ и морфизмы $f$ и $g$ также являются таковыми.
\end{proof}

\begin{prop}[th-epi-mono]
Любой морфизм теорий факторизуется через регулярный эпиморфизм и мономорфизм (в любой из категорий $\Th$, $\Th_\mathcal{S}$, $\Th^\lambda$, $\Th_\mathcal{S}^\lambda$).
\end{prop}
\begin{proof}
Пусть $f : T_1 \to T_2$ -- морфизм теорий.
Пусть $\mathcal{S}_i$ -- множество сортов теории $T_i$ и пусть $g : \mathcal{S}_1 \to \fs{im}(f)$ -- огранчиение $f$ на ее образ.
Тогда вложение $T_1 \to g^*(T_1) \cup \{ \varphi \sststile{}{V} \psi \mid f(\varphi) \sststile{T_2}{V} f(\psi) \}$ является регулярным эпиморфизмом по \dprop{th-epi}.
В категориях $\Th^\lambda$ и $\Th_\mathcal{S}^\lambda$ мы берем только $\lambda$-достижимые секвенции $\varphi \sststile{}{V} \psi$.
Морфизм $f$ факторизуется через это вложение и очевидный морфизм $g^*(T_1) \cup \{ \varphi \sststile{}{V} \psi \mid f(\varphi) \sststile{T_2}{V} f(\psi) \} \to T_2$, который является мономорфизмом по \dprop{th-mono}.
\end{proof}

Категории $\Th^\lambda$ и $\Th^\lambda_\mathcal{S}$ полны, так как они являются локально представимыми.
Мы не знаем являются ли категории $\Th$ и $\Th_\mathcal{S}$ полными, но мы можем доказать, что в них существуют произведения:

\begin{prop}
В категориях $\Th$ и $\Th_\mathcal{S}$ существуют все малые произведения.
\end{prop}
\begin{proof}
По \dprop{th-adj} нам достаточно доказать это утверждение для категории $\Th$.
Пусть $F : J \to \Th$ -- множество теорий.
Пусть $\lambda$ -- регулярный кардинал такой, что все теории $F_j$ и все морфизмы $F(f)$ являются $\lambda$-достижимыми.
Тогда мы определим теорию $L$ с множеством сортов $\mathcal{S} = \prod_{j \in J} \mathcal{S}_j$, где $\mathcal{S}_j$ -- множество сортов теории $F_j$.

Для каждого множества $I < \lambda$, каждой коллекции сортов $\{ s_i \}_{i \in I}$ из $\mathcal{S}$, каждого сорта $s \in \mathcal{S}$ мы добавляем функциональный символ $\{ t_j \}_{j \in J}$ в $L$ сигнатуры $\prod_{i \in I} s_i \to s$,
где $t_j$ -- термы теории $T_j$ сигнатуры $\prod_{i \in I} \pi_j(s_i) \to \pi_j(s)$.
Для каждого множества $I < \lambda$, каждой коллекции сортов $\{ s_i \}_{i \in I}$ из $\mathcal{S}$ мы добавляем предикатный символ $\{ \varphi_j \}_{j \in J}$ в $L$ сигнатуры $\prod_{i \in I} s_i$,
где $\varphi_j$ -- атомарные формулы теории $T_j$ сигнатуры $\prod_{i \in I} \pi_j(s_i)$.
Для каждого $j \in J$ можно определить морфизм теорий $\pi_j : L \to F_j$, который отображает сорт $s$ в $\pi_j(s)$ и каждый символ $\{ p_j \}_{j \in J}$ в $p_j$.
Теперь мы добавляем в $L$ все аксиомы $\varphi \sststile{}{V} \psi$ для которых секвенции $\pi_j(\varphi) \sststile{}{\pi_j(V)} \pi_j(\psi)$ выводимы в $F_j$ для всех $j \in J$.
Тогда $\pi_j$ всё еще являются морфизмами теорий.

Пусть $\alpha$ -- конус $F$ с вершиной в некоторой теории $T'$.
Тогда существует уникальная функция $f : \mathcal{S}' \to \mathcal{S}$ из множества сортов $T'$ в $\mathcal{S}$ такая, что $\alpha_j = \pi_j \circ f$.
Пусть $R$ -- предикатный символ такой, что $\alpha_j(R) = \bigwedge_{i \in I_j} \varphi^i_j$.
Тогда мы определим $f(R)$ как $\bigwedge_{j \in J, i \in I_j} \{ \delta_{j,j'}(\varphi^i_j) \}_{j' \in J}$, где $\delta_{j,j}(\varphi) = \varphi$ и $\delta_{j,j'}(\varphi) = \top$, если $j \neq j'$.
Заметим, что $\pi_j(f(R))$ эквивалентна $\alpha_j(R)$.
Пусть $\sigma$ -- функциональный символ такой, что $\alpha_j(\sigma) = t_j|_{\bigwedge_{i \in I_j} \varphi^i_j}$.
Тогда мы определим $f(\sigma)$ как $\{ t_j \}_{j \in J}|_{\bigwedge_{j \in J, i \in I_j} \{ \delta_{j,j'}(\varphi^i_j) \}_{j' \in J}}$.
Заметим, что $\pi_j(f(\sigma))$ эквиваленен $\alpha_j(\sigma)$.

По определению $L$ функция $f$ отправляет аксиомы $T'$ в аксиомы $L$.
Кроме того, $\pi_j \circ f = \alpha_j$.
Нам осталось доказать, что такой морфизм уникален.
Пусть $f,g : T' \to L$ -- морфизмы такие, что $\pi_j \circ f = \pi_j \circ g = \alpha_j$.
Тогда они действуют одинаково на сортах.
Кроме того, для каждого предикатного символа $R$ формулы $\pi_j(f(R))$ и $\pi_j(g(R))$ эквивалентны.
Отсюда следует, что $f(R)$ и $g(R)$ тоже эквивалентны.
Аналогичное утверждение верно и для функциональных символов.
Следовательно, $f = g$.
\end{proof}

\subsection{Категория моделей}
\label{sec:models}

В этом подразделе мы обсудим категорию моделей некоторой теории $T$ и ее связь с классифицирующей категорией $T$ и категорией расширений $T$.
Для начала мы приведем определение категории моделей $T$ из \cite{PHL}.
\emph{Интерпретация} сигнатуры $(\mathcal{S},\mathcal{F},\mathcal{P})$ -- это $\mathcal{S}$-множество $M$ вместе с функцией,
сопоставляющей каждому функциональному символу $\sigma : \prod_{i \in I} s_i \to s$ частичную функцию $M(\sigma) : \prod_{i \in I} M_{s_i} \to M_s$
и каждому предикатному символу $R : \prod_{i \in I} s_i$ отношение $M(R) \subseteq \prod_{i \in I} M_{s_i}$.

Пусть $M$ -- интерпретация некоторой сигнатуры.
Тогда для любого терма $t$ сорта $s$ с переменными в $\{ x_i : s_i \}_{i \in I}$ можно определить частичную функцию $M(t) : \prod_{i \in I} M_{s_i} \to M_s$ индукцией по $t$.
Если $t = x_i$, то $M(x_i)$ -- это просто $i$-ая проекция.
Если $t = \sigma(\{ t_j \}_{j \in J})$, то $M(t) = M(\sigma)(\{ M(t_j) \}_{j \in J})$.
Для любой формулы $\varphi$ с переменными в $\{ x_i : s_i \}_{i \in I}$ можно определить отношение $M(\varphi) \subseteq \prod_{i \in I} M_{s_i}$.
Если $\varphi = (t = t')$, то $M(\varphi)$ состоит из тех $a$ для которых $M(t)(a)$ и $M(t')(a)$ определены и $M(t)(a) = M(t')(a)$.
Если $\varphi = R(\{ t_j \}_{j \in J})$, то $M(\varphi)$ состоит из тех $a$ для которых $M(t_j)(a)$ определено для всех $j \in J$ и $\{ M(t_j)(a) \}_{j \in J} \in M(R)$.
Если $\varphi = \bigwedge_{j \in J} \varphi_j$, то $M(\varphi)$ -- это пересечение всех $M(\varphi_j)$.

Мы будем говорить, что сигнатура $\varphi \sststile{}{V} \psi$ верна в интерпретации $M$, если $M(\varphi) \subseteq M(\psi)$.
\emph{Модель} теории $T$ -- это интерпретация ее подлежащей сигнатуры, в которой верны все аксиомы $T$.
Морфизм интерпретаций $M$ и $N$ -- это функция $f$, сопоставляющая каждому сорту $s$ функцию $M_s \to N_s$, удовлетворяющую двум условиям.
Для каждого функционального символа $\sigma$ и всех $a$, если $M(\sigma)(a)$ определено, то $N(\sigma)(f(a))$ тоже определено и $f(M(\sigma)(a)) = N(\sigma)(f(a))$.
Для каждого предикатного символа $R$ и всех $a$, если $a \in M(R)$, то $f(a) \in N(\sigma)$.
Тождественный морфизм и композиция морфизмов задаются очевидным образом.
Легко видеть, что эти определения задают категорию.
Категория моделей теории $T$ будет обозначаться $\Mod{T}$.

Если $T$ является $\lambda$-достижимой теорией, то категория $\Mod{T}$ является локально $\lambda$-представимой.
Начальный объект $\Mod{T}$ можно сконструировать из термов теории $T$ как показано в \cite[Theorem~22]{PHL}.
Так как нам понадобится работать с начальными моделями, мы приведем эту конструкцию здесь.
Сначала мы определим частичное отношение эквивалентности на множестве замкнутых термов $T$.
Термы $t_1$ и $t_2$ эквивалентны тогда и только тогда, когда $\sststile{T}{} t_1 = t_2$.
Подлежащее $\mathcal{S}$-множество начальной модели определяется как факторизация множества замкнутых термов $T$ по этому отношению частичной эквивалентности.
Интерпретация предикатного символа $R$ состоит из $\{ t_i \}_{i \in I}$ таких, что $\sststile{T}{} R(\{ t_i \}_{i \in I})$.
Интерпретация функционального символа $\sigma$ -- это функция, определенная на $\{ t_i \}_{i \in I}$ как $\sigma(\{ t_i \}_{i \in I})$ в том случае, если $\sststile{T}{} \sigma(\{ t_i \}_{i \in I})\!\!\downarrow$.
Легко показать, что эти определения действительно задают модель $T$, и она является начальной.

\begin{prop}[th-func-mod]
Для каждого морфизма теорий $f : T \to T'$ существует функтор $f^* : \Mod{T'} \to \Mod{T}$ такой, что $\fs{id}_T^*$ -- тождественный функтор и $(g \circ f)^* = f^* \circ g^*$.
Если $f$ сюръективен на сортах, то $f^*$ является строгим функтором.
\end{prop}
\begin{proof}
Если $M$ -- модель $T'$, то $f^*(M)_s = M_{f(s)}$.
Для всех символов $p$ теории $T'$ мы определяем $f^*(M)(p)$ как $M(f(p))$.
Тогда каждый морфизм моделей $M$ и $N$ теории $T'$ также является морфизмом теорий $f^*(M)$ и $f^*(N)$.
Это задает функтор $f^* : \Mod{T'} \to \Mod{T}$, удовлетворяющий необходимым условиям.

Допустим $f$ сюръективен на объектах.
Пусть $g,h : M \to N$ -- морфизмы моделей $T'$ такие, что $f^*(g) = f^*(h)$.
Для любого сорта $s'$ теории $T'$ существует сорт $s$ теории $T$ такой, что $f(s) = s'$.
Тогда $g_{s'} = f^*(g)_s = f^*(h)_s = h_{s'}$, то есть $g = h$.
\end{proof}

Для каждой модели $M$ теории $T$ мы определим расширение $\Lang(M)$ теории $T$.
Сорта этой теории -- это сорта $T$.
Кроме функциональных и предикатных символов $T$ эта теория содержит функциональные символы $O_a : s$ для всех $a \in M_s$.
Аксиомы $\Lang(M)$ -- это аксиомы $T$ вместе со следующими секвенциями:
\begin{align*}
& \sststile{}{} O_a \downarrow \\
& \sststile{}{} \sigma(\{ O_{a_i} \}_{i \in I}) = O_{M(\sigma)(\{ a_i \}_{i \in I})} \\
& \sststile{}{} R(\{ O_{a_i} \}_{i \in I})
\end{align*}
для всех $a \in M_s$, всех $a_i \in M_{s_i}$,
всех функциональных символов $\sigma$ таких, что $M(\sigma)(\{ a_i \}_{i \in I})$ определено,
и всех предикатных символов $R$ таких, что $\{ a_i \}_{i \in I} \in M(R)$.

Модели $\Lang(M)$ -- это просто модели $T$ вместе с морфизмом из $M$.
Другими словами, категории $M/\Mod{T}$ и $\Mod{\Lang(M)}$ изоморфны.
В частности, на $M$ есть естественная структура модели $\Lang(M)$ такая, что $M(O_a) = a$.

\begin{lem}[cl-term]
Если $t$ -- замкнутый терм сорта $s$ такой, что $\sststile{\Lang(M)}{} t \downarrow$,
то существует уникальный $a \in M_s$ такой, что $\sststile{\Lang(M)}{} t = O_a$.
\end{lem}
\begin{proof}
Если $\sststile{\Lang(M)}{} t = O_a$ и $\sststile{\Lang(M)}{} t = O_{a'}$, то $\sststile{\Lang(M)}{} O_a = O_{a'}$.
Так как $M$ -- модель $\Lang(M)$, то формула $O_a = O_{a'}$ верна в $M$, что означает, что $a = a'$, то есть такой $a$ действительно уникален.

Теперь докажем, что такой $a$ существует индукцией по $t$.
Если $t = O_a$, то это очевидно.
If $t = \sigma(\{ t_i \}_{i \in I})$, то по индукционной гипотезе $\sststile{\Lang(M)}{} t = \sigma(\{ O_{a_i} \}_{i \in I})$ для некоторых $a_i$.
Так как $M$ является моделью $\Lang(M)$ и $\sststile{\Lang(M)}{} \sigma(\{ O_{a_i} \}_{i \in I})\!\!\downarrow$, то $M(\sigma)(\{ a_i \}_{i \in I})$ определено.
Таким образом, секвенция $\sststile{}{} \sigma(\{ O_{a_i} \}_{i \in I}) = O_{M(\sigma)(\{ a_i \}_{i \in I})}$ выводима в $\Lang(M)$.
\end{proof}

Для каждого морфизма $h : M \to N$ моделей $T$ мы можем определить морфизм расширений $\Lang(h) : \Lang(M) \to \Lang(N)$, задав $\Lang(h)(O_a)$ как $O_{h(a)}$.
Таким образом, $\Lang$ является функтором $\Mod{T} \to T/\Th_\mathcal{S}$.

\begin{prop}[lang-ff]
Функтор $\Lang : \Mod{T} \to T/\Th_\mathcal{S}$ является полным и строгим.
\end{prop}
\begin{proof}
Пусть $h_1$, $h_2$ -- морфизмы моделей такие, что $\Lang(h_1) = \Lang(h_2)$.
Тогда $O_{h_1(a)} = \Lang(h_1)(O_a) = \Lang(h_2)(O_a) = O_{h_2(a)}$ и по \dlem{cl-term} верно, что $h_1(a) = h_2(a)$.
Таким образом, $\Lang$ строгий.

Пусть $M$ и $N$ -- модели $T$ и $h : \Lang(M) \to \Lang(N)$ -- морфизм расширений $T$.
Тогда по \dlem{cl-term} для каждого $a \in M_s$ существует уникальный $h'(a) \in N_s$ такой, что $\sststile{\Lang(N)}{} h(O_a) = O_{h'(a)}$.
Докажем, что $h' : M \to N$ является морфизмом моделей.
Действительно, если $M(\sigma)(\{ a_i \}_{i \in I})$ определено, то $\sststile{\Lang(M)}{} \sigma(\{ O_{a_i} \}_{i \in I}) = O_{M(\sigma)(\{ a_i \}_{i \in I})}$.
Следовательно, секвенция $\sststile{}{} \sigma(\{ O_{h'(a_i)} \}_{i \in I}) = O_{h'(M(\sigma)(\{ a_i \}_{i \in I}))}$ является теоремой $\Lang(N)$.
Но секвенция $\sststile{}{} \sigma(\{ O_{h'(a_i)} \}_{i \in I}) = O_{N(\sigma)(\{ h'(a_i) \}_{i \in I})}$ также является теоремеой $\Lang(N)$.
Следовательно, по \dlem{cl-term} верно, что $h'(M(\sigma)(\{ a_i \}_{i \in I}) = N(\sigma)(\{ h'(a_i) \}_{i \in I})$.

Если $\{ a_i \}_{i \in I} \in M(R)$, то $\sststile{\Lang(M)}{} R(\{ O_{a_i} \}_{i \in I})$.
Следовательно, секвенция $\sststile{}{} R(\{ O_{h'(a_i)} \}_{i \in I})$ выводима в $\Lang(N)$.
Так как $N$ является моделью $\Lang(N)$, то $\{ h'(a_i) \}_{i \in I} \in N(R)$.
Таким образом, $h'$ является морфизмом моделей.
По определению $h'$ верно, что $\Lang(h') = h$.
Следовательно, $\Lang$ полный.
\end{proof}

Теперь мы опишем функтор $\Syn : T/\Th_\mathcal{S} \to \Mod{T}$.
Для каждого морфизма $i : T \to T'$ мы определяем $\Syn(i)$ как $i^*(0_{T'})$, где $0_{T'}$ -- начальный объект $\Mod{T'}$.
Если $f : T_1 \to T_2$ -- морфизм между $i_1 : T \to T_1$ и $i_2 : T \to T_2$, то мы определяем $\Syn(f)$ как $i_1^*(!_{f^*(0_{T_2})})$, где $!_{f^*(0_{T_2})}$ -- уникальный морфизм $0_{T_1} \to f^*(0_{T_2})$.
Тот факт, что $\Syn$ сохраняет тождественные морфизмы и композицию следует из \oprop{th-func-mod}.

\begin{prop}[syn-lang]
Функтор $\Syn$ является правым сопряженным к $\Lang$.
\end{prop}
\begin{proof}
Определим $\epsilon_{T'} : \Lang(\Syn(T')) \to T'$ как $\epsilon_{T'}(O_t) = t$.
Легко видеть, что $\epsilon_{T'}$ сохраняет аксиомы $\Lang(\Syn(T'))$.
Кроме того, $\epsilon$ естественен по $T'$.
Докажем, что $\epsilon$ является коединицей сопряжения.
Пусть $f : \Lang(M) \to T'$ -- морфизм.
Тогда нам нужно показать, что существует уникальный морфизм $g : \Lang(M) \to \Lang(\Syn(T'))$ такой, что $\epsilon_{T'} \circ g = f$.
По \dlem{cl-term} существует уникальный терм $t$ такой, что $g(O_a) = O_t$.
Так как $t = \epsilon_{T'}(g(O_a)) = f(O_a)$, то $g$ должен удовлетворять уравнению $g(O_a) = O_{f(O_a)}$.
Следовательно, $g$ уникален.
Легко видеть, что $g$ сохраняет аксиомы $\Lang(M)$ и, следовательно, задает морфизм $g : \Lang(M) \to \Lang(\Syn(T'))$.
\end{proof}

\begin{remark}[mod-colimits]
Утверждения \nprop{lang-ff} и \nprop{syn-lang} влекут, что копределы моделей могут быть сконструированы следующим образом:
\[ \colim_{j \in J}(M_j) = \Syn(\Lang(\colim_{j \in J}(M_j))) = \Syn(\colim_{j \in J}(\Lang(M_j))). \]
Так как копределы теорий имеют простое явное описание, то это дает явное описание копределов моделей.
\end{remark}

Для каждого морфизма теорий $f : T \to T'$ мы можем определить функтор $f_! : \Mod{T} \to \Mod{T'}$ как $f_!(M) = \Syn(\Lang(M) \amalg_{T} T')$.
В \cite[Theorem~29]{PHL} было показано, что $f_!$ является левым сопряженным к $f^*$.
Эта теорема была доказана только для более слабого понятия морфизмов теорий, но это доказательство работает и для более общего определения морфизмов.

Функтор $f_!$ можно использовать для представления модели через порождающие и соотношения.
Модели пустой теории с множеством сортов $\mathcal{S}$ -- это просто $\mathcal{S}$-множества.
Если $f : 0 \to T$ -- уникальный морфизм из пустой теории в некоторую теорию $T$, то $f^*(M)$ -- это просто подлежащее $\mathcal{S}$-множество модели $M$, и $f_!(X)$ -- это свободная модель $T$ на $\mathcal{S}$-множестве $X$.
Если $R$ -- это множество аксиом в языке теории $\Lang(X) \amalg T$, то мы определяем модель $F(X,R)$ теории $T$ как $\Syn(\Lang(X) \amalg T \cup R)$.
По определению $\Syn$, для того, чтобы сконструировать морфизм $F(X,R) \to M$, необходимо и достаточно сконструировать морфизм из $X$ в подлежащее $\mathcal{S}$-множество $M$ таким образом, чтобы соотношения из $R$ были верны в $M$.
Иногда мы будем опускать множество порождающих в нотации $F(X,R)$, так как они обычно могут быть выведены из множества соотношений.
Кроме этого, в качестве соотношений мы часто будем брать формулы с переменными в $X$.
Такая формула $\varphi$ соответствует секвенции $\sststile{}{} \varphi[O_x/x]$.

\begin{prop}[cart-mod-dual]
Категория $\cat{C}_T$ дуальна категории моделей $T$.
При этом категория $\cat{C}_T^\lambda$ соответствуют полной подкатегории $\Mod{T}$, состоящей из $\lambda$-представимых объектов.
\end{prop}
\begin{proof}
Определим функтор $F : \cat{C}_T^\fs{op} \to \Mod{T}$.
Каждому производному сорту $\{ \overline{x} : \prod_{i \in I} s_i \mid \varphi(\overline{x}) \}$ функтор $F$ сопоставляет модель $F(\{ \{ x_i : s_i \}_{i \in I}, \{ \varphi \} \})$.
Пусть $\{ t_j \}_{j \in J}$ -- морфизм между $X = \{ \overline{x} : \prod_{i \in I} s_i \mid \varphi(\overline{x}) \}$ и $Y = \{ \overline{y} : \prod_{j \in J} s_j' \mid \psi(\overline{y}) \}$.
Тогда мы можем определить морфизм $F(\{ t_j \}_{j \in J}) : F(Y) \to F(X)$ как функцию, сопоставляющую каждому $y_j$ элемент $F(X)$, задаваемый термом $t_j$.
Этот элемент определен, так как секвенция $\varphi \sststile{}{\overline{x}} t_j\!\downarrow$ выводима.
Соотношение $\psi$ модели $F(Y)$ выполнено в $F(X)$, так как секвенция $\varphi \sststile{}{\overline{x}} \psi[t_j/y_j]$ выводима.
Очевидно, что $F$ сохраняет тождественные морфизмы.
Факт, что $F(\{ t_k' \}_k \circ \{ t_j \}_j) = F(\{ t_k' \}_k) \circ F(\{ t_j \}_j)$, легко доказать индукцией по $t_k'$.

Пусть $\{ t_j \}_{j \in J}$ и $\{ t_j' \}_{j \in J}$ -- два параллельных морфизма между $X$ и $Y$ в $\cat{C}_T^\fs{op}$ таких, что $F(\{ t_j \}_{j \in J}) = F(\{ t_j' \}_{j \in J})$.
Тогда $t_j$ и $t_j'$ равны как элементы $Y$, но два таких терма равны в $Y$ тогда и только тогда, когда $\varphi \sststile{}{\overline{x}} t_j = t_j'$.
Следовательно, морфизмы $\{ t_j \}_{j \in J}$ и $\{ t_j' \}_{j \in J}$ тоже равны.
Пусть $f : F(Y) \to F(X)$ -- морфизм в $\Mod{T}$.
Тогда $g = \{ f(y_j) \}_{j \in J}$ является морфизмом в $\cat{C}_T^\fs{op}$ таким, что $F(g) = f$.
Таким образом, $F$ является строгим и полным функтором.

Функтор $F$ существенно сюръективен на объектах.
Действительно, если $M$ -- модель $T$, то она может быть представлена в виде $F(M, \{ \bigwedge \fs{Th}(M) \})$, где $\fs{Th}(M)$ -- множество формул, верных в $M$, а такая модель лежит в образе $F$.
Для каждого $\lambda$-достижимого сорта $X$ модель $F(X)$ является $\lambda$-представленной.
И наоборот, по любому представлению мы можем построить производный сорт как описано выше, и если в представлении использовалось меньше $\lambda$ переменных и атомарных формул, то соответствующий сорт будет $\lambda$-достижимым.
\end{proof}

\begin{lem}[th-acc-mor]
Если $f : T \to T'$ -- $\lambda$-достижимый морфизм теорий, то $f_! : \Mod{T} \to \Mod{T'}$ сохраняет $\lambda$-представимые объекты, а $f^* : \Mod{T'} \to \Mod{T}$ сохраняет $\lambda$-направленные копределы.
\end{lem}
\begin{proof}
Если $F(X,R)$ -- представление некоторой модели $T$ такое, что $|X| < \lambda$ и $|R| < \lambda$, то $F(f(X),f(R))$ -- представление для $f_!(F(X,R))$, удовлетворяющее тем же условиям,
так как для каждого символа $p$ теории $T$ чиисло атомарных формул в $f(p)$ меньше $\lambda$.
Таким образом, $f_!$ сохраняет $\lambda$-представимые объекты.
Этот факт влечет, что его правый сопряженный функтор $f^*$ сохраняет $\lambda$-направленные копределы как показано в \cite[Theorem~1.66]{LPC}.
\end{proof}

По \dprop{cart-mod-dual} функтор $f_! : \Mod{T} \to \Mod{T'}$ соответствует некоторому функтору $f_! : \cat{C}_T \to \cat{C}_{T'}$.
Этот функтор легко описать явно: $f_!(\{ \overline{x} : \prod_{i \in I} s_i \mid \varphi \}) = \{ \overline{x} : \prod_{i \in I} f(s_i) \mid f(\varphi) \}$ и $f_!(\{ t_j \}_{j \in J}) = \{ f(t_j) \}_{j \in J}$.
Если $f$ является $\lambda$-достижимым морфизмом, то по \dlem{th-acc-mor} этот функтор можно ограничить на подкатегории $\cat{C}_T^\lambda$ и $\cat{C}_{T'}^\lambda$, получив функтор $f_! : \cat{C}_T^\lambda \to \cat{C}_{T'}^\lambda$.
Для классифицирующих категорий верно утверждение, аналогичное \dprop{th-func-mod}:
\begin{prop}[th-func-cl]
Пусть $\bcat{Cart}^\lambda$ -- категория малых категорий, в которых существуют $\lambda$-малые пределы, и функторов, сохраняющих эти пределы.
Тогда существует функтор $\fs{Cl}^\lambda : \Th^\lambda \to \bcat{Cart}^\lambda$, определенный как $\fs{Cl}^\lambda(T) = \cat{C}_T^\lambda$ и $\fs{Cl}^\lambda(f) = f_!$.
\end{prop}
\begin{proof}
Нам достаточно проверить, что $\fs{Cl}^\lambda$ сохраняет тождественные морфизмы и композицию.
Первый факт очевиден, а второй следует из того, что для любой пары морфизмов теорий $f : T \to T'$ и $g : T' \to T''$ формулы $(g \circ f)(\varphi)$ и $g(f(\varphi))$ эквивалентны.
\end{proof}

\subsection{Связь теорий и малых $\lambda$-полных категорий}

Мы уже видели как по теории построить ее классифицирующую категорию.
Теперь мы опишем обратную операцию, строящую по категории ее представление в виде теории.
Мы определим функтор $\fs{Th}^\lambda : \bcat{Cart}^\lambda \to \Th^\lambda$.
Пусть $\cat{C}$ -- малая $\lambda$-полная категория.
Тогда сорта $\fs{Th}^\lambda(\cat{C})$ -- это объекты $\cat{C}$.
Множество функциональных символов этой теории состоит из следующих символов:
\begin{itemize}
\item $f : A \to B$ для каждого морфизма $f : A \to B$ категории $\cat{C}$.
\item $p_{\{ \pi_i \}_{i \in I}} : \prod_{i \in I} A_i \to P$ для каждого $I < \lambda$, каждого множества объектов $\{ A_i \}_{i \in I}$ и каждого произведения $\{ \pi_i : P \to A_i \}_{i \in I}$ этих объектов.
\item $i_f : B \to A$ для каждого мономорфизма $f : A \to B$ категории $\cat{C}$.
\end{itemize}
Теория $\fs{Th}^\lambda(\cat{C})$ не содержит предикатных символов.
Множество аксиом этой теории состоит из следующих секвенций:
\begin{itemize}
\item $\sststile{}{x : A} \fs{id}_A(x) = x$ для каждого объекта $A$.
\item $\sststile{}{x : A} (g \circ f)(x) = g(f(x))$ для каждой пары морфизмов $f : A \to B$ и $g : B \to C$.
\item $\sststile{}{\{ x_i \}_{i \in I}} \pi_i(p_{\{ \pi_i \}_{i \in I}}(\{ x_i \}_{i \in I})) = x_i$ и $\sststile{}{y : P} p_{\{ \pi_i \}_{i \in I}}(\{ \pi_i(y) \}_{i \in I}) = y$
\item $\sststile{}{x : A} i_f(f(x)) = x$ и $i_f(y)\!\downarrow\ \sststile{}{y : B} f(i_f(y)) = y$ для каждого мономорфизма $f : A \to B$.
\item $f(x) = g(x) \sststile{}{x : A} i_e(x)\!\downarrow$ для любого уравнителя $e$ морфизмов $f$ и $g$.
\end{itemize}

Пусть $F : \cat{C} \to \cat{D}$ -- функтор между малыми $\lambda$-полными категориями.
Тогда мы определим $\fs{Th}^\lambda(F) : \Th^\lambda(\cat{C}) \to \Th^\lambda(\cat{D})$.
Для каждого объекта $A$ категории $\cat{C}$ мы определяем $\fs{Th}^\lambda(F)(A)$ как $F(A)$.
Для каждого морфизма $f : A \to B$ категории $\cat{C}$ мы определяем $\fs{Th}^\lambda(F)(f)$ как $F(f)$.
Так как $F$ сохраняет декартовы квадраты, то он сохраняет и мономорфизмы.
Следовательно мы можем определить $\fs{Th}^\lambda(F)(i_f)$ как $i_{F(f)}$.
Легко видеть, что $\fs{Th}^\lambda(F)$ сохраняет аксиомы, а значит задает морфизм теорий.
Кроме того, $\fs{Th}^\lambda$ сохраняет тождественные морфизмы и композицию.
Следовательно у нас есть функтор $\fs{Th}^\lambda : \bcat{Cart}^\lambda \to \Th^\lambda$.

Для каждой малой $\lambda$-полной категории $\cat{C}$ можно определить функтор $\epsilon_\cat{C} : \cat{C} \to \fs{Cl}^\lambda(\fs{Th}^\lambda(\cat{C}))$
как $\epsilon_\cat{C}(X) = X$ для каждого объекта $X$ и $\epsilon_\cat{C}(f) = f$ для каждого морфизма $f$.
Легко видеть, что $\epsilon$ является естественным преобразованием.

\begin{prop}[cl-th]
Функтор $\epsilon_\cat{C} : \cat{C} \to \fs{Cl}^\lambda(\fs{Th}^\lambda(\cat{C}))$ является эквивалентностью категорий для любой категории $\cat{C}$.
\end{prop}
\begin{proof}
Во-первых, для каждого терма $t$ теории $\fs{Th}^\lambda(\cat{C})$ с переменными в $\{ x : A \}$ сорта $B$ мы определим частичный морфизм $F(t) = (m,f)$ в категории $\cat{C}$, где $m : A' \to A$ -- подобъект и $f : A' \to B$ -- морфизм.
Если $t = x$, то $F(t) = (\fs{id}_A,\fs{id}_A)$.
Если $t = g(t')$ и $F(t') = (m',f')$, то $F(t) = (m', g \circ f')$.
Если $t = p_{\{ \pi_i \}_{i \in I}}(\{ t_i \}_{i \in I})$ и $F(t_i) = (m_i,f_i)$, то $F(t)$ определяется как $(m, \langle f_i' \rangle_{i \in I})$,
где $m : \bigcap_{i \in I} A_i' \to A$ -- пересечение подобъектов $m_i$, а $f_i'$ -- композиция $\bigcap_{i \in I} A_i' \to A_i'$ и $f_i : A_i' \to B_i$.
Если $t = i_g(t')$ и $F(t') = (m',f')$, то $F(t) = (m' \circ g', f)$, где $g'$ и $f$ определены следующим образом:
\[ \xymatrix{ C' \ar[r]^f \ar[d]_{g'} \pb & C \ar[d]^g \\
              A' \ar[r]_{f'}              & B
            } \]

Если секвенция $\sststile{}{x : A} t = t'$ выводима, то $F(t)$ и $F(t')$ -- тотальные морфизмы и $F(t) = F(t')$.
Это легко показать индукцией по выводу этой секвенции.
Кроме того, индукцией по $t$ легко покзать, что если секвенция $\sststile{}{x : A} t\!\downarrow$ выводима, то секвенция $\sststile{}{x : A} t = f(i_m(x))$ также выводима, где $F(t) = (m,f)$.
Отсюда следует, что функтор $\epsilon_\cat{C}$ полный и строгий.

Нам осталось показать, что функтор $\epsilon_\cat{C}$ существенно сюръективен на объектах.
Пусть $X = \{ \overline{x} : \overline{A} \mid \bigwedge_{j \in J} t_j = t_j' \}$ -- объект $\fs{Cl}^\lambda(\fs{Th}^\lambda(\cat{C}))$.
Пусть $A$ -- произведение объектов $A_i$ в $\cat{C}$ и пусть $(m : B \to A, f : B \to C)$ и $(m' : B' \to A, f' : B' \to C)$ -- частичные объекты,
соответствующие термам $p(\{ t_j[\pi_i(x)/x_i] \}_{j \in J})$ и $p(\{ t_j'[\pi_i(x)/x_i] \}_{j \in J})$, где $x : A$.
Тогда уравнитель морфизмов $B \cap B' \to B \xrightarrow{f} C$ и $B \cap B' \to B' \xrightarrow{f'} C$ изоморфен $X$.
\end{proof}

Теперь мы определим морфизм теорий $\eta_T : T \to \fs{Th}^\lambda(\fs{Cl}^\lambda(T))$ для каждой теории $T$.
Для каждого сорта $s$ мы определяем $\eta_T(s)$ как $s$.
Пусть $R : \prod_{i \in I} s_i$ -- предикатный символ.
Пусть $P = \{ \overline{X} : \prod_{i \in I} s_i \mid \top \}$ -- произведение объектов $\{ s_i \}_{i \in I}$ в $\fs{Cl}^\lambda(T)$.
Пусть $p : \prod_{i \in I} s_i \to P$ -- соответствующий этому произведению функциональный символ в $\fs{Th}^\lambda(\fs{Cl}^\lambda(T))$.
Пусть $m$ -- мономорфизм $\{ \overline{X} : \prod_{i \in I} s_i \mid R(\overline{x}) \} \to \{ \overline{X} : \prod_{i \in I} s_i \mid \top \}$ в $\fs{Cl}^\lambda(T)$.
Тогда мы определяем $\eta_T(R)$ как $i_m(p(\overline{x}))\!\downarrow$.
Если $\sigma : \prod_{i \in I} s_i \to s$ -- функциональный символ, то мы определяем $P$ и $p$ как раньше,
а $m$ как мономорфизм $\{ \overline{X} : \prod_{i \in I} s_i \mid \sigma(\overline{x})\!\downarrow \} \to \{ \overline{X} : \prod_{i \in I} s_i \mid \top \}$.
Тогда у нас есть морфизм $f : \{ \overline{X} : \prod_{i \in I} s_i \mid \sigma(\overline{x})\!\downarrow \} \to \{ x : s \mid \top \}$ в $\fs{Cl}^\lambda(T)$, соответствующий $\sigma$.
Мы определяем $\eta_T(\sigma)$ как $f(i_m(p(\overline{x})))$.

Легко показать, что для любой формулы $\varphi$ формулу $\eta_T(\varphi)$ можно определить так же как и $\eta_T(R)$ с $\varphi$ вместо $R$.
Отсюда следует, что $\eta_T$ сохраняет теоремы.
Действительно, если $\varphi$ влечет $\psi$, то у нас есть мономорфизм $m : \{ \overline{X} : \prod_{i \in I} s_i \mid \varphi \} \to \{ \overline{X} : \prod_{i \in I} s_i \mid \psi \}$.
Тогда $m_\phi = m_\psi \circ m$.
Отсюда следует, что $i_{m_\varphi}(y)\!\downarrow$ влечет $m_\psi(m(i_{m_\varphi}(y))) = y$, что влечет $i_{m_\psi}(m_\psi(m(i_{m_\varphi}(y)))) = i_{m_\psi}(y)$.
В частности это означает, что $i_{m_\varphi}(y)\!\downarrow$ влечет $i_{m_\psi}(y)\!\downarrow$.

Легко видеть, что $\eta_T$ естественен по $T$.
Морфизм $\eta_T$ не является изоморфизмом, но он порождает эквивалентность $\lambda$-классифирующих категорий.
Это следует из \oprop{cl-th} и следующей леммы:

\begin{lem}[th-cl]
Для каждой теории $T$ функторы $\fs{Cl}^\lambda(\eta_T)$ и $\epsilon_{\fs{Cl}^\lambda(T)}$ изоморфны.
\end{lem}
\begin{proof}
Пусть $s = \{ \overline{x} : \prod_{i \in I} s_i \mod \varphi \}$ -- объект категории $\fs{Cl}^\lambda(T)$.
Тогда $\epsilon_{\fs{Cl}^\lambda(T)}(s) = s$ и $\fs{Cl}^\lambda(\eta_T)(s) = \{ \overline{x} : \prod_{i \in I} s_i \mid \eta_T(\varphi) \}$.
Пусть $\pi_i : \{ \overline{x} : \prod_{i \in I} s_i \mod \top \} \to s_i$ -- очевидная проекция в $\fs{Cl}^\lambda(T)$.
Тогда мы можем определить морфизм $\alpha_s : s \to \{ \overline{x} : \prod_{i \in I} s_i \mid \top \}$ как $\{ \pi_i(m_\varphi(y)) \}_{i \in I}$, где $y : s$.
Легко видеть, что $\alpha$ естественен по $s$.
Чтобы доказать, что $\alpha_s$ также является морфизмом $s \to \{ \overline{x} : \prod_{i \in I} s_i \mid \eta_T(\varphi) \}$,
нужно показать, что секвенция $\sststile{}{y : s} \eta_T(\varphi)[\pi_i(m_\varphi(y))/x_i]\!\downarrow$ выводима в $\fs{Th}^\lambda(\fs{Cl}^\lambda(T))$.
Это следует из того факта, что формула $\eta_T(\varphi)$ эквивалентна $i_{m_\varphi}(p(\overline{x}))$, и свойств $p$ и $i_{m_\varphi}$.

Нам осталось показать, что существует обратный морфизм к $\alpha_s$.
Мы определяем $\beta_s : \{ \overline{x} : \prod_{i \in I} s_i \mid \eta_T(\varphi) \} \to s$ как $i_{m_\varphi}(p(\overline{x}))$.
Тот факт, что $\alpha_s$ и $\beta_s$ взаимно обратны, следует из свойств $p$ и $i_{m_\varphi}$.
\end{proof}

\section{Модельные категории}

В этом разделе мы обсудим свойство (полу)модельных категорий, в которых все объекты расслоены.
Мы предоставим несколько необходимых и достаточных условий для существования таких структур.

\subsection{Базовые определения}

Пусть $\C$ -- категория и $V$ -- объект $\C$.
Тогда \emph{цилиндр} для $V$ -- это объект $C(V)$ вместе с морфизмами $\cyli_0,\cyli_1 : V \to C(V)$.
Если $i : U \to V$ -- морфизм $\C$, то \emph{относительный цилиндр} для $i$ -- это цилиндр $(C_U(V),\cyli_0,\cyli_1)$ такой, что $\cyli_0 \circ i = \cyli_1 \circ i$.
Морфизм цилиндров $C(V_1)$ и $C(V_2)$ -- это пара морфизмов $f : V_1 \to V_2$ и $C(f) : C(V_1) \to C(V_2)$, которые коммутируют с $\cyli_0$ и $\cyli_1$.
Если $\C$ -- модельная категория, то под цилиндром обычно подразумевается более узкое понятие, но в этом разделе нам будет удобно работать с более общим.

\emph{Левая гомотопия} (по отношению к $C(V)$) между морфизмами $f,g : V \to X$ -- это морфизм $h : C(V) \to X$ такой, что $h \circ \cyli_0 = f$ и $h \circ \cyli_1 = g$.
Морфизмы \emph{гомотопны}, если между ними существует гомотопия.
Морфизмы \emph{гомотопны относительно $i : U \to V$} (по отношению $C_U(V)$), если существует гомотопия по отношению к $C_U(V)$ между ними.
Если морфизмы $f$ и $g$ гомотопны, то мы будем писать $f \sim g$, а если они гомотопны относительно $i$, то этот факт будет обозначаться как $f \sim_i g$.

Пусть $V$ и $Y$ -- объекты категории $\C$ и $R$ -- некоторое отношение на множестве $\Hom(V,Y)$.
Мы будем говорить, что морфизм $f : U \to V$ имеет \emph{левое свойство поднятия (LLP) с точностью до $R$} по отношению к морфизму $g : X \to Y$,
а $g$ имеет \emph{правое свойство поднятия (RLP) с точностью до $R$} по отношению к $f$, если для каждого коммутативного квадрата вида
\[ \xymatrix{ U \ar[r]^u \ar@{}[dr]|(.7){R} \ar[d]_f & X \ar[d]^g \\
              V \ar[r]_v \ar@{-->}[ur]^h             & Y,
            } \]
существует стрелка $h : V \to X$ такая, что $h \circ f = u$ и $(g \circ h) R v$.
Морфизм $f$ имеет RLP с точностью до $R$ по отношению к объекту $V$, если он имеет это свойство по отношению к морфизму $0 \to V$.
Морфизм $f$ имеет RLP с точностью до $R$ по отношению к классу морфизмов $\I$, если он имеет это свойство по отношению ко всем морфизмам в $\I$.
Морфизм имеет LLP или RLP по отношению к другому морфизму, если он имеет это свойство с точностью до равенства.
В качетсве $R$ мы будем часто брать отношение вида $\sim_i$.
В этом случае мы будем говорить о свойствах поднятия с точностью до гомотопий относительно $i$.

Мы будем говорить, что морфизм $g$ \emph{чист} по отношению к морфизму $f$, если $g$ имеет RLP по отношению к $f$ с точностью до максимального отношения.
Понятие чистого морфизма (формально) схоже с понятием $\lambda$-чистых морфизмов, используемым в теории достижимых категорий.
Приведем несколько элементарных свойств чистых морфизмов:

\begin{prop} Следующие утверждения верны в любой категории $\C$:
\begin{enumerate}
\item Если $g$ имеет RLP по отношению к $f$ с точностью до некоторого отношения, то $g$ чсит по отношению к $f$.
\item Чистые морфизмы замкнуты относительно композиции.
\item Если $f$ и $g$ -- морфизмы такие, что $g \circ f$ чистый, то $f$ тоже чистый.
\item Любой расщепленный мономорфизм чист по отношению ко всем морфизмам.
\item Если морфизм чист по отношению к себе, то он является расщепленным мономорфизмом.
\end{enumerate}
\end{prop}

Пусть $\C$ -- категория и $X$ -- объект $\C$.
\emph{Объект путей} для $X$ -- это объект $P(X)$ вместе с морфизмами $p_0,p_1 : P(X) \to X$.
\emph{Правая гомотопия} между морфизмами $f,g : V \to X$ -- это морфизм $h : V \to P(X)$ такой, что $p_0 \circ h = f$ и $p_1 \circ h = g$.
Если между $f$ и $g$ существует правая гомотопия, мы будем обозначать этот факт как $f \sim^r g$.
Морфизм объектов путей $P(X)$ и $P(Y)$ -- это пара морфизмов $f : X \to Y$ и $P(f) : P(X) \to P(Y)$, которые коммутируют с $p_0$ и $p_1$.

Отношение $\sim$ рефлексивно тогда и только тогда, когда существует морфизм $s : C_U(V) \to V$ такой, что $s \circ \cyli_0 = s \circ \cyli_1 = id_V$.
В этом случае мы будем говорить, что цилиндр $C_U(V)$ \emph{рефлексивен}.
Отношение $\sim^r$ рефлексивно тогда и только тогда, когда существует морфизм $t : X \to P(X)$ такой, что $p_0 \circ t = p_1 \circ t = id_X$.
В этом случае мы будем говорить, что объект $P(X)$ \emph{рефлексивен}.
Если $P(X)$ рефлексивен, мы будем говорить, что правая гомотопия $h : V \to P(X)$ между $f,g : V \to X$ \emph{константна на $i : U \to V$}, если $h \circ i = t \circ f \circ i$.
В этом случае мы будем писать $f \sim^r_i g$ и говорить, что $f$ и $g$ \emph{гомотопны относительно $i$}.

\begin{defn}
\emph{Слабая система факторизаций} на категории $\C$ -- это пара $(\mathcal{L},\mathcal{R})$ классов морфизмов $\C$ таких, что
\begin{itemize}
\item Каждый морфизм факторизуется как морфизм из $\mathcal{L}$ и морфизм из $\mathcal{R}$.
\item $\mathcal{L}$ -- это класс морфизмов, которые имеют LLP по отношению к $\mathcal{R}$.
\item $\mathcal{R}$ -- это класс морфизмов, которые имеют RLP по отношению к $\mathcal{L}$.
\end{itemize}
\end{defn}

Моедльные категории были определены в \cite{quillen}.

\begin{defn}
\emph{Модельная структура} на категории $\C$ состоит из трех классов морфизмов $\fib$, $\cof$ и $\we$,
которые называются \emph{расслоениями}, \emph{корасслоениями} и \emph{слабыми эквивалентностями} соотвественно, удовлетворяющих следующим условиям:
\begin{itemize}
\item Класс $\we$ удовлетворяет свойству 2-из-3, то есть для любой пары морфизмов $f : X \to Y$ и $g : Y \to Z$, если два из трех морфизмов $f$, $g$, $g \circ f$ принадлежат $\we$, то и третий принадлежит этому классу.
\item Пары $(\cof, \fib \cap \we)$ и $(\cof \cap \we, \fib)$ являются слабыми системами факторизаций.
\end{itemize}
\emph{Модельная категория} -- это конечно полная и конечно кополная категория с модельной структурой.
\end{defn}

Морфизм в модельной категории называется \emph{тривиальным расслоением}, если он принадлежит $\fib \cap \we$, и \emph{тривиальным корасслоением}, если он принадлежит $\cof \cap \we$.
Объект $X$ называется \emph{расслоенным}, если уникальный морфизм $X \to 1$ является расслоением, и \emph{корасслоеным}, если уникальный морфизм $0 \to X$ является корасслоением.

Нам понадобится более общее понятие, определение которого появляется в \cite{semi-model,barwick-semi}.
Также вариация этого определения появляется в \cite[Theorem~3.3]{hovey-semi}.

\begin{defn}
\emph{(Левая) полумодельная структура} на категории $\C$ состоит из трех классов морфизмов $\fib$, $\cof$ и $\we$,
которые называются \emph{расслоениями}, \emph{корасслоениями} и \emph{слабыми эквивалентностями} соотвественно, удовлетворяющих следующим условиям:
\begin{itemize}
\item Все три класса замкнуты относительно ретрактов, и класс $\we$ удовлетворяет свойству 2-из-3.
\item Корасслоения имеют LLP по отношению к тривиальным расслоениям, а тривиальные корасслоения с корасслоенными доменами имеют LLP по отношению к расслоениям.
\item Любой морфизм факторизуется через корасслоение и тривиальное расслоение, и любой морфизм с корасслоенным доменом факторизуется через тривиальное корасслоение и расслоение.
\end{itemize}
\emph{(Левая) полумодельная категория} -- это конечно полная и конечно кополная категория с полумодельной структурой.
\end{defn}

Для любой морфизма $i : U \to V$ любой модельной категории можно определить цилиндр $C_U(V)$ как факторизацию кодиагонали $[id_V,id_V] : V \amalg_U V \to V$ в корасслоение $[\cyli_0,\cyli_1] : V \amalg_U V \to C_U(V)$ и тривиальное расслоение $s : C_U(V) \to V$.
Отношение левых гомотопий, соответствующее этому цилиндру, всегда рефлексивное и симметричное.
Для любого объекта $X$ любой модельной категории можно определить объект путей $P(X)$ как факторизацию диагонали $\langle id_X, id_X \rangle : X \to X \times X$ в тривиальное корасслоение $t : X \to P(X)$ и расслоение $\langle p_0, p_1 \rangle : P(X) \to X \times X$.
В полумодельной категории такой объект путей можно определить, если $X$ корасслоен.
Следующее утверждение является стандартным:
\begin{prop}[path-cyl]
Если $i : U \to V$ -- корасслоение и $X$ -- расслоенный объект в некоторой модельной категории, то морфизмы $f,g : V \to X$ лево гомотопны относительно $i$ тогда и только тогда, когда они право гомотопны относительно $i$.
Это отношение гомотопности является отношением эквивалентности.
Для полумодельных категорий это утверждение верно, если $V$ и $X$ корасслоены.
\end{prop}

\begin{defn}
Мы будем говорить, что морфизм $f : X \to Y$ является \emph{включением деформационного ретракта}, если существует $g : Y \to X$ такой, что $g \circ f = \fs{id}_X$ и $f \circ g \sim \fs{id}_Y$.
Мы будем говорить, что $f$ является \emph{включением сильного деформационного ретракта}, если гомотопия относительна $f$.
\end{defn}

The following lemmas generalize standard properties of model categories.

\begin{lem}[hom-ext][Homotopy extension property]
Пусть $\C$ -- категория и $i : U \to V$ -- морфизм $\C$.
Допустим, что для некоторого объекта $X$ существует объект путей $p_0,p_1 : P(X) \to X$ такой, что $p_0$ имеет RLP по отношению к $i$.

Пусть $u : U \to X$ и $v : V \to X$ -- морфизмы и $h : U \to P(X)$ -- гомотопия между $v \circ i$ и $u$.
Тогда существует морфизм $v' : V \to X$ и гомотопия $h' : V \to P(X)$ между $v$ и $v'$ такая, что $h = h' \circ i$.
\end{lem}
\begin{proof}
Пусть $h : U \to P(X)$ -- гомотопия между $v \circ i$ и $u$.
Рассмотрим следующую диаграмму:
\[ \xymatrix{ U \ar[r]^-h \ar[d]_i & P(X) \ar[d]^{p_0} \\
              V \ar[r]_v & X
            } \]
По предположению у нас есть стрелка $h' : V \to P(X)$, которая является необходимой гомотопией.
\end{proof}

Эта лемма может быть продемонстирована следующим образом:
\[ \xymatrix{ U \ar[r]^u \ar[d]_i \ar@{}[dr]|(.3){\sim^r} & X \\
              V \ar[ur]_v &
            }
\qquad \qquad
   \xymatrix{ U \ar[r]^u \ar[d]_i \ar@{}[dr]|(.62){\sim^r} & X \\
              V \ar@{-->}[ur]^{v'} \ar@/_1pc/[ur]_v &
            } \]
Если у нас есть диаграмма слева, то мы можем найти морфизм $v'$ такой, что диаграмма справа коммутирует.
Более того, если ограничить гомотопию между $v$ и $v'$ на $U$, то мы получим исходную гомотопию между $v \circ i$ и $u$.
Пусть $\sim^{r*}$ -- рефлексивное транзитивное замыкание $\sim^r$.
Тогда предыдущая лемма также верна и для $\sim^{r*}$:

\begin{lem}[hom-ext-rtc]
Пусть $\C$ -- категория и $X$ -- ее объект, удовлетворяющие условию предыдущей леммы.
Пусть $u : U \to X$ и $v : V \to X$ -- морфизмы и $h_1, \ldots h_n : U \to P(X)$ -- последовательность гомотопий такая, что $p_1 \circ h_j = p_0 \circ h_{j+1}$ для всех $1 \leq j < n$, $p_0 \circ h_1 = v \circ i$ и $p_1 \circ h_n = u$.
Тогда существует морфизм $v' : V \to X$ и последовательность гомотопий $h'_1, \ldots h'_n : V \to P(X)$ такая,
что $p_1 \circ h'_j = p_0 \circ h'_{j+1}$ для всех $1 \leq j < n$, $p_0 \circ h'_1 = v$, $p_1 \circ h'_n = v'$ и $h_j = h'_j \circ i$ для всех $1 \leq j \leq n$.
\end{lem}
\begin{proof}
Достаточно применить предыдущую лемму $n$ раз.
\end{proof}

Пусть $\I$ -- класс морфизмов категории $\C$.
Тогда мы определяем $\Iinj$ как класс морфизмов, которые имеют RLP по отношению к $\I$, $\Icof$ как класс морфизмов, которые имеют LLP по отношению к $\Iinj$ и $\Icell$ как класс трансфинитных композиций пушаутов элементов $\I$.
Элементы $\Icell$ называются \emph{относительными $\I$-комплексами}.
Любой относительный $\I$-комплекс принадлежит $\Icof$.

Мы будем говорить, что множество $\I$ морфизмов кополной категории $\C$ \emph{допускает аргумент малых объектов}, если домены морфизмов в $\I$ малы относительно $\Icell$.
Определение малых объектов приведено в \cite[Definition~2.1.3]{hovey}.
Нам понадобится только тот факт, что в локально представимой категории все объекты малы по отношению к любому классу морфизмов.

\begin{prop}[small-object-argument][Аргумент малых объектов]
Пусть $\I$ -- множество морфизмов кополной категории, допускающее аргумент малых объектов.
Тогда $(\Icell,\Iinj)$ является слабой системой факторизаций.
\end{prop}

Следующее утверждение предоставляет удобный способ конструкировать модельные структуры:

\begin{prop}[model-cat]
Пусть $\C$ -- конечно полная и конечно кополная категория и пусть $\we$, $\cof$ и $\fib$ -- три класса морфизмов $\C$.
Тогда на $\C$ существует модельная структура со слабыми эквивалентностями $\we$, корасслоениями $\cof$ и расслоениями $\fib$ тогда и только тогда,
когда существуют классы морфизмов $\I$ и $\J$ такие, что $\Icof = \cof$, $\Jinj = \fib$ и выполнены следующие условия:
\begin{description}
\item[(A1)] Каждый морфизм факторизуется через морфизмы из $\Icof$ и $\Iinj$ и через морфизмы из $\Jcof$ и $\Jinj$.
\item[(A2)] $\we$ удовлетворяет свойству 2-из-3.
\item[(A3)] $\Iinj \subseteq \we$.
\item[(A4)] $\Jcof \subseteq \we \cap \Icof$.
\item[(A5)] $\Jinj \cap \we \subseteq \Iinj$.
\end{description}
\end{prop}

Аналог предыдущего утверждения для полумодельных стуктур выглядит следующим образом:

\begin{prop}[semimodel-cat]
Пусть $\C$ -- конечно полная и конечно кополная категория и пусть $\we$, $\cof$ и $\fib$ -- три класса морфизмов $\C$.
Тогда на $\C$ существует полумодельная структура со слабыми эквивалентностями $\we$, корасслоениями $\cof$ и расслоениями $\fib$ тогда и только тогда,
когда существуют классы морфизмов $\I$ и $\J$ такие, что $\Icof = \cof$, $\Jinj = \fib$ и выполнены следующие условия:
\begin{description}
\item[(A1)] Каждый морфизм факторизуется через морфизмы из $\Icof$ и $\Iinj$ и, если его домен корасслоен, то через морфизмы из $\Jcof$ и $\Jinj$.
\item[(A2)] $\we$ удовлетворяет свойству 2-из-3 и замкнут относительно ретрактов.
\item[(A3)] $\Iinj \subseteq \we$.
\item[(A4)] $\J \subseteq \Icof$ и любой морфизм из $\Jcof$ с корасслоеным доменом принадлежит $\we$.
\item[(A5)] $\Jinj \cap \we \subseteq \Iinj$.
\end{description}
\end{prop}

\begin{defn}
(Полу)модельная категория $\C$ называется \emph{корасслоено порожденной}, если она кополна и в качестве классов $\I$ и $\J$ в \pprop{model-cat} (в \pprop{semimodel-cat}) можно выбрать множества, допускающие аргумент малых объектов.
В этом случае элементы множества $\I$ называются \emph{порождающими корасслоениями}, а элементы $\J$ \emph{порождающими тривиальными корасслоениями}.
(Полу)модельная категория $\C$ называется \emph{комбинаторной}, если она корасслоено порождена и локально представима.
\end{defn}

Функтор между модельными категориями называется \emph{левым Квилленовским функтором}, если он является левым сорпяженным и сохраняет корасслоения и тривиальные корасслоения.
Функтор между модельными категориями называется \emph{правым Квилленовским функтором}, если он является правым сопряженными и сохраняет расслоения и тривиальные расслоения.
Левый сопряженный функтор является Квилленовским тогда и только тогда, когда его правый сопряженный является таковым.
\emph{Квиллен-эквивалентность} -- это пара Квилленовских сопряженных функторов $F \dashv U$ таких, что $U$ отражает слабые эквивалентности между расслоенными объектами,
и морфизм $X \xrightarrow{\eta_X} UF(X) \xrightarrow{U(t_X)} URF(X)$ является слабой эквивалентностью для любого корасслоенного объекта, где первый морфизм -- это единица сопряжения, а $t_X$ -- расслоеная замена $X$.

\begin{prop}[transferred]
Пусть $\C$ -- модельная категория, $\D$ -- локально представимая категория, $F : \C \to \D$ -- левый сопряженный функтор, и $U : \D \to \C$ -- его правый сопряженный.
Пусть $\I$ -- множество порождающих корасслоений $\C$, а $\J$ -- множество порождающих тривиальных корасслоений.
Допустим, что морфизмы в $U(\Icell[F(\J)])$ являются слабыми эквивалентностями.
Тогда на $\D$ существует комбинаторная модельная структура, где морфизм $f$ является слабой эквивалентностью или расслоением, если $U(f)$ является таковым,
а множества порождающих корасслоений и тривиальных корасслоений определяются как $F(\I)$ и $F(\J)$.
\end{prop} 

\begin{defn}
\emph{Моноидальная модельная категория} -- это модельная категория со структурой симметричной моноидальной категории такой, что следующие условия выполнены:
\begin{enumerate}
\item Для любого корасслоенного объекта $X$ морфизм $Q(I) \otimes X \to I \otimes X$ является слабой эквивалентностью.
\item Для любой пары корасслоений $f : A \to B$ и $g : C \to D$ морфизм $A \otimes D \amalg_{A \otimes C} B \otimes C \to B \otimes D$ является корасслоением.
Кроме того, этот морфизм является слабой эквивалентностью, если один из морфизмов $f$ или $g$ является таковым. Мы будем называть эту аксиому \emph{аксиомой пушаутов и произведений}.
\end{enumerate}
\end{defn}

\begin{defn}
Пусть $\C$, $\D$ и $\cat{E}$ -- модельные категории.
Тогда бифунктор $F : \C \times \D \to \cat{E}$ называется \emph{Квилленовским бифунктором}, если он сохраняет копределы по каждому из аргументов и для любой пары корасслоений $i : X \to Y$ и $j : X' \to Y'$
морфизм $F(X,Y') \amalg_{F(X,Y)} F(X',Y) \to F(X',Y')$ является корасслоением, которое является слабой эквивалентностью, если один из морфизмов $i$ или $j$ является таковым.
\end{defn}

\begin{defn}
Пусть $\cat{V}$ -- моноидальная модельная категория.
\emph{Модельная категория, обогащенная над $\cat{V}$,} -- это $\cat{V}$-обогащенная категория $\C$ вместе со структурой модельной категории на подлежащей категории такой,
что в ней существуют тензоры и котензоры над $\cat{V}$ и функтор тензорного произведения $\otimes : \C \times \cat{V} \to \C$ является Квилленовским бифунктором.
\end{defn}

\section{Модельные структуры на категориях теорий}

В этом разделе мы опишем несколько модельных структур на категориях теорий.

\subsection{Модельные структуры на $\Th^\lambda$ и $\Th^\lambda_\mathcal{S}$}

Сначала определим класс морфизмов теорий, который будет выступать в роли слабых эквивалентностей.
Мы будем говорить, что морфизм теорий $f : T \to T'$ является \emph{Морита-эквивалентностью}, если сопряжение $f_! \dashv f^*$ является эквивалентностью категорий $\Mod{T}$ и $\Mod{T'}$.

\begin{prop}[th-morita-char]
Если $f : T \to T'$ -- $\lambda$-достижимый морфизм теорий, то следующие условия эквивалентны:
\begin{itemize}
\item $f$ является Морита-эквивалентностью.
\item $f_! : \cat{C}_T \to \cat{C}_{T'}$ является эквивалентностью категорий.
\item $f_! : \cat{C}_T^\lambda \to \cat{C}_{T'}^\lambda$ является эквивалентностью категорий.
\end{itemize}
\end{prop}
\begin{proof}
Эквивалентность первых двух пунктов следует из \oprop{cart-mod-dual}.
По этому же утверждению функтор $f_! : \cat{C}_T^\lambda \to \cat{C}_{T'}^\lambda$ соответствует функтору $f_! : \Mod{T}^\lambda \to \Mod{T'}^\lambda$,
где $\Mod{T}^\lambda$ -- это полная подкатегория $\Mod{T}$, состоящая из $\lambda$-представимых моделей, и аналогично определяется $\Mod{T'}^\lambda$.
Если $f_! : \Mod{T} \to \Mod{T'}$ является эквивалентностью, то это верно и для $f_! : \Mod{T}^\lambda \to \Mod{T'}^\lambda$.
Докажем обратное утверждение.
Так как категория $\Mod{T}$ является локально $\lambda$-представимой, то любой объект является $\lambda$-направленным копределом $\lambda$-представимых объектов.
По \dlem{th-acc-mor} функтор $f^*$ сохраняет $\lambda$-направленные копределы.
То же верно и для $f_!$ так как он является левым сопряженным.
Отсюда следует, что для любого объекта $X$ единица сопряжения $\eta_X : X \to f^* f_!(X)$
является направленным копределом морфизмов $\eta_{X_j} : X_j \to f^* f_! (X_j)$, где $X_j$ -- $\lambda$-представимые объекты.
Каждый из этих морфизмов является изоморфизмом по предположению.
Следовательно, $\eta_X$ тоже является изоморфизмом.
Аналогичный аргумент показывает, что коединица $f_! f^*(X) \to X$ тоже является изоморфизмом.
\end{proof}

Теперь мы определим несколько расширений теорий, которые будут выступать в роли порождающих корасслоений.
В следующих определениях $V$ -- это множество мощности $\kappa$.
\begin{align*}
i_s & : (\varnothing,\varnothing,\varnothing,\varnothing) \to (\{ s \},\varnothing,\varnothing,\varnothing) \\
i_t^\kappa & : (V \amalg \{ s \}, \varnothing, \varnothing, \varnothing) \to (V \amalg \{ s \}, \{ \sigma : \prod V \to s \}, \varnothing, \varnothing) \\
i_p^\kappa & : (V, \varnothing, \varnothing, \varnothing) \to (V, \varnothing, \{ R : \prod V \}, \varnothing) \\
i_f^\kappa & : (V, \varnothing, \{ R, R' : \prod V \}, \varnothing) \to (V, \varnothing, \{ R, R' : \prod V \}, \{ R(\overline{x}) \sststile{}{\overline{x}} R'(\overline{x}) \})
\end{align*}

Морфизм $i_s$ является $\lambda$-достижимым для любого $\lambda$.
Морфизмы $i_t^\kappa$, $i_p^\kappa$ и $i_f^\kappa$ являются $\lambda$-достижимыми, если $\kappa < \lambda$.
Множество $\I^\lambda$ определяется как $\{ i_s \} \cup \{ i_t^\kappa, i_p^\kappa, i_f^\kappa \mid \kappa < \lambda \}$.
Пусть $\I$ -- объединение множеств $\I^\lambda$ для всех $\lambda$.
Мы можем привести явное описание корасслоений в категории $\Th^\lambda$:

\begin{prop}[th-cof]
Морфизм в $\Th^\lambda$ принадлежит $\Icof[\I^\lambda]$ тогда и только тогда, когда он инъективен на сортах.
\end{prop}
\begin{proof}
Каждый из морфизмов в $\I^\lambda$ инъективен на сортах и класс морфизмов, инъективных на сортах, замкнут относительно пушаутов, трансфинитных композиций и ретрактов.
Следовательно, морфизмы в $\Icof[\I^\lambda]$ инъективны на сортах.
Докажем обратное включение.
Если морфизм $(\mathcal{S},\mathcal{F},\mathcal{P},\mathcal{A}) \to (\mathcal{S}',\mathcal{F}',\mathcal{P}',\mathcal{A}')$ инъективен на сортах,
то он факторизуется как $(\mathcal{S},\mathcal{F},\mathcal{P},\mathcal{A}) \to (\mathcal{S}',\mathcal{F},\mathcal{P},\mathcal{A})$ и $(\mathcal{S}',\mathcal{F},\mathcal{P},\mathcal{A}) \to (\mathcal{S}',\mathcal{F}',\mathcal{P}',\mathcal{A}')$,
где первый морфизм является пушаутом копроизведения множества копий морфизмов $i_s$, а второй морфизм действует тождественным образом на сортах.
По \dlem{th-ext} этот морфизм изоморфен некоторому расширению $(\mathcal{S}',\mathcal{F},\mathcal{P},\mathcal{A}) \to (\mathcal{S}', \mathcal{F} \amalg \mathcal{F}'', \mathcal{P} \amalg \mathcal{P}'', \mathcal{A} \amalg \mathcal{A}'')$.
Этот морфизм факторизуется как $(\mathcal{S}',\mathcal{F},\mathcal{P},\mathcal{A}) \to (\mathcal{S}', \mathcal{F} \amalg \mathcal{F}'', \mathcal{P} \amalg \mathcal{P}'', \mathcal{A})$ и
$(\mathcal{S}', \mathcal{F} \amalg \mathcal{F}'', \mathcal{P} \amalg \mathcal{P}'', \mathcal{A}) \to (\mathcal{S}', \mathcal{F} \amalg \mathcal{F}'', \mathcal{P} \amalg \mathcal{P}'', \mathcal{A} \amalg \mathcal{A}'')$.
Первый морфизм является пушаутом копроизведения копий $i_t^\kappa$ и $i_p^\kappa$, а второй пушаутом копроизведения копий $i_f^\kappa$.
\end{proof}

Чтобы определить множество порождающих тривиальных корасслоений, мы введем несколько примеров теорий.
Пусть $s = \{ \overline{x} : \prod_{i \in I} s_i \mid \varphi \}$ и $s' = \{ \overline{y} : \prod_{j \in J} s_j' \mid \psi \}$ -- два производных сорта теории $T$.
Тогда мы будем писать $T \cup \fs{Iso}(\overline{\sigma},s,s')$ для обозначения расширения $T$, добавляющего к $T$ изоморфизм $\overline{\sigma}$ между $s$ и $s'$.
Другими словами, мы добавляем к $T$ функциональные символы $\sigma_j : s \to s_j'$ и $\tau_i : s' \to s_i$ для всех $j \in J$ и $i \in I$ и следующие аксиомы:
\begin{align*}
\varphi & \sststile{}{\overline{x}} \tau_i(\{ \sigma_j(\overline{x}) \}_{j \in J}) = x_i \\
\bigwedge_{j \in J} \sigma_j(\overline{x})\!\downarrow & \sststile{}{\overline{x}} \varphi \\
\psi & \sststile{}{\overline{y}} \sigma_j(\{ \tau_i(\overline{y}) \}_{i \in I}) = y_j \\
\bigwedge_{i \in I} \tau_i(\overline{y})\!\downarrow & \sststile{}{\overline{y}} \psi
\end{align*}

Пусть $V$ -- множество мощности $\kappa$.
Тогда мы определяем теорию $T^\kappa_s$ как $(V, \varnothing, \{ P : \prod V \}, \varnothing)$.
Морфизм $j^\kappa_s$ определяется как следующее расширение:
\[ j^\kappa_s : T^\kappa_s \to T^\kappa_s \amalg \{ s \} \cup \fs{Iso}(\overline{\sigma}, \{ \overline{x} : \prod V \mid P(\overline{x}) \}, s) \]

Пусть $I$ -- множество мощности $\kappa$ и $J$ -- множество мощности $\kappa'$.
Пусть $\mathcal{S} = \{ s_i \}_{i \in I} \amalg \{ s_j' \}_{j \in J}$.
Тогда теория, классифицирующая частичные мономорфизмы между производными сортами размера $\kappa$ и $\kappa'$ определяется как
\[ T_m^{\kappa,\kappa'} = (\mathcal{S}, \{ \sigma_j : \prod_{i \in I} s_i \to s_j' \mid j \in J \}, \varnothing, \{ \bigwedge_{j \in J} \sigma_j(\overline{x}) = \sigma_j(\overline{x}') \sststile{}{\overline{x},\overline{x}'} \bigwedge_{i \in I} x_i = x_i' \}) \]
Теория $T_i^{\kappa,\kappa'}$, классифицирующая частичные изоморфизмы, состоит из множества сортов $\mathcal{S}$, множества функциональных символов $\{ \sigma_j : \prod_{i \in I} s_i \to s_j' \mid j \in J \} \amalg \{ \sigma_i' : \prod_{j \in J} s_j' \to s_i \mid i \in I \}$ и следующих аксиом:
\begin{align*}
& \bigwedge_{j \in J} \sigma_j(\overline{x})\!\downarrow\ \sststile{}{\overline{x}} \bigwedge_{i \in I} \sigma_i'(\{ \sigma_j(x_i) \}_{j \in J}) = x_i \\
& \bigwedge_{i \in I} \sigma_i'(\overline{x}')\!\downarrow\ \sststile{}{\overline{x}'} \bigwedge_{j \in J} \sigma_j(\{ \sigma_i'(x_j') \}_{i \in I}) = x_j'
\end{align*}
Морфизм $j_m^{\kappa,\kappa'}$ определяется как очевидный морфизм $T_m^{\kappa,\kappa'} \to T_i^{\kappa,\kappa'}$.
Множество $\J^\lambda$ состоит из морфизмов $j^\kappa_s$ и $j_m^{\kappa,\kappa'}$ для всех $\kappa < \lambda$ и $\kappa' < \lambda$.
Пусть $\J$ -- объединение множеств $\J^\lambda$ для всех $\lambda$.

\begin{lem}[part-mono]
Пусть $T$ -- $\lambda$-достижимая теория.
Коллекция термов $\{ t_j \}_{j \in J}$ со свободными переменными в $\{ x_i : s_i \}_{i \in I}$ является частичным мономорфизмом тогда и только тогда,
когда она является мономорфизмом как морфизм $\{ \overline{x} : \overline{s} \mid \top \} \to \{ \overline{y} : \overline{s'} \mid \top \}$ в $\fs{Cl}^\lambda(T)$.
\end{lem}
\begin{proof}
Допустим, что $\{ t_j \}_{j \in J}$ является мономорфизмом в $\fs{Cl}^\lambda(T)$.
Тогда рассмотрим морфизмы $\overline{x},\overline{x'} : \{ \overline{x}, \overline{x'} : \overline{s} \times \overline{s} \mid \bigwedge_{j \in J} t_j = t_j[\{ x'_i/x_i \}_{i \in I}] \} \to \{ \overline{x} : \overline{s} \mid \top \}$.
Они становятся равны после композиции с $\{ t_j \}_{j \in J}$, и, так как последний морфизм является мономорфизмом, они просто равны.
Это означает, что секвенция $\bigwedge_{j \in J} t_j = t_j[\{ x'_i/x_i \}_{i \in I}] \sststile{}{\overline{x},\overline{x'}} \bigwedge_{i \in I} x_i = x_i'$ выводима.
Другими словами, $\{ t_j \}_{j \in J}$ является частичным мономорфизмом.

Теперь допустим, что $\{ t_j \}_{j \in J}$ является частичным мономорфизмом.
Пусть $\{ t'_i \}_{i \in I}, \{ t''_i \}_{i \in I} : \{ \overline{z} : \overline{s''} \mid \varphi \} \to \{ \overline{x} : \overline{s} \mid \top \}$ -- морфизмы, которые становятся равны после композиции с $\{ t_j \}_{j \in J}$.
Это означает, что секвенция $\varphi \sststile{}{\overline{z}} \bigwedge_{j \in J} t_j[\{ t'_i/x_i \}_{i \in I}] = t_j[\{ t''_i/x_i \}_{i \in I}]$ выводима.
Так как $\{ t_j \}_{j \in J}$ является частичным мономорфизмом, то отсюда следует, что секвенция $\varphi \sststile{}{\overline{z}} \bigwedge_{i \in I} t'_i = t''_i$ также выводима.
Другими словами, морфизмы $\{ t'_i \}_{i \in I}$ и $\{ t''_i \}_{i \in I}$ равны.
\end{proof}

В разделе~\ref{sec:pht} была сконструирована пара функторов $\fs{Cl}^\lambda : \Th^\lambda \to \bcat{Cart}^\lambda$ и $\fs{Th}^\lambda : \bcat{Cart}^\lambda \to \Th^\lambda$ и естественное преобразование $\eta_T : T \to \fs{Th}^\lambda(\fs{Cl}^\lambda(T)$).
Из \oprop{cl-th} и \olem{th-cl} следует, что $\eta_T$ является Морита-эквивалентностью.
В следуещем утверждении мы покажем, что теория $\fs{Th}^\lambda(\cat{C})$ всегда является расслоенной.
Таким образом, функтор $\fs{Th}^\lambda \circ \fs{Cl}^\lambda$ является функтором расслоенной замены.

\begin{prop}[th-fib]
Для любой малой $\lambda$-полной категории $\cat{C}$ теория $\fs{Th}^\lambda(\cat{C})$ имеет RLP по отношению $\J^\lambda$.
\end{prop}
\begin{proof}
Теория $T$ имеет RLP по отношению к морфизмам $j^\kappa_s$ тогда и только тогда любой производный сорт $T$ изоморфен некоторому сорту $T$.
Сорта $\fs{Th}^\lambda(\cat{C})$ -- это объекты $\cat{C}$, а производные сорта этой теории -- это объекты $\fs{Cl}^\lambda(\fs{Th}^\lambda(\cat{C}))$.
Любой объект категории $\fs{Cl}^\lambda(\fs{Th}^\lambda(\cat{C}))$ изоморфен объекту $\cat{C}$ по \dprop{cl-th}.

Чтобы доказать, что теория $T$ имеет RLP по отношению к морфизмам $j_m^{\kappa,\kappa'}$, необходимо показать, что любой частичный мономорфизм $f$ между производными сортами в $T$ имеет частичный обратный.
Так как мы уже видели, что любой производный сорт в $\fs{Th}^\lambda(\cat{C})$ изоморфен некоторому сорту, то мы можем предположить, что $f$ является частичным мономорфизмом между сортами.
Так как категория $\cat{C}$ эквивалентна $\fs{Cl}^\lambda(\fs{Th}^\lambda(\cat{C}))$, то любой частичный мономорфизм между $A$ и $B$ имеет вид $f \circ i_m$ для некоторых мономорфизмов $m : A' \to A$ и $f : A' \to B$ в $\cat{C}$.
В качестве обратного к этому частичному мономорфизму мы можем взять $m \circ i_f$.
\end{proof}

Самая сложная часть проверки аксиом модельных категорий -- это доказательство того, что морфизмы в $\Icell[\J^\lambda]$ являются Морита-эквивалентностями.
Мы покажем это в следующей лемме:

\begin{lem}[th-triv-cof]
Трансфинитные композиции пушаутов морфизмов в $\J$ являются Морита-эквивалентностями.
\end{lem}
\begin{proof}
Докажем, что пушауты морфизмов в $\J$ являются Морита-эквивалентностями.
Рассмотрим пушаут $f : T \to T'$ морфизма $j^\kappa_s$.
Модели $T'$ -- это модели $T$ вместе с множеством $X$ и биекцией между $X$ и множеством, соответствующим некоторому производному сорту $T$.
Функтор $f^* : \Mod{T'} \to \Mod{T}$ -- это очевидный забывающий функтор, который очевидно является эквивалентностью.
Рассмотрим пушаут $f : T \to T'$ морфизма $j^{\kappa,\kappa'}_m$.
Так как у нас есть интерпретация $T_m^{\kappa,\kappa'} \to T$, то в любой модели теории $T$ есть выбранная частичная инъекция $\sigma$ между множествами $X$ и $Y$, соответствующими некоторым производным сортам теории $T$.
Модели теории $T'$ -- это модели $T$ вместе с частичной функцией между $Y$ и $X$, соответствующим $\sigma'$.
Аксиомы $T'$ влекут, что домен $\sigma'$ должен совпадать с образом $\sigma$ и что $\sigma'$ является обратной функцией к $\sigma$ на своем домене.
Так как такая функция $\sigma'$ определяется уникальным образом, то категории $\Mod{T}$ и $\Mod{T'}$ эквивалентны.

Нам осталось доказать, что трансфинитные композиции пушаутов морфизмов из $\J$ являются Морита-эквивалентностями.
Пусть $F : \mu \to \Th$ -- диаграмма, состоящая из Морита-эквивалентностей.
Пусть $F_\mu = \colim_{\alpha < \mu} F_\alpha$.
Так как диаграмма $F$ состоит из морфизмов, инъективных на сортах, то по \dlem{th-ext} мы можем считать, что она состоит из включений подтеорий.
Тогда $F_\mu$ -- это просто объединение всех $F_\alpha$.
Докажем, что включение $F_0 \to F_\mu$ также является Морита-эквивалентностью.

Во-первых, заметим, что для любого множества переменных $V$ теории $F_0$, любого сорта $s$ теории $F_0$ и любого терма $t$ теории $F_\mu$ сорта $s$ с переменными в $V$
существует частичный морфизм $\sigma$ между $\prod V$ и $s$ в категории $\cat{C}_{F_0}$ такой, что $\sigma$ изоморфен в $F_\mu$ частичному морфизму, соответствующему $t$.
Этот факт доказывается индукцией по $t$.
Если $t$ -- переменная, то это очевидно.
Если $t = \sigma(\{ t_i \}_{i \in I})$, то $\sigma$ принадлежит теории $F_\alpha$ для некоторого $\alpha < \mu$.
Для каждого сорта $s_i$ существует производный сорт $s_i'$ теории $F_0$ и изоморфизм $\tau_i : s_i' \to s_i$ в $F_\alpha$.
По индукционной гипотезе для каждого $i \in I$ существует подобъект $t_i'$ между $\prod V$ и $s_i$ такой, что $t_i'$ изоморфен $\tau_i^{-1}(t_i)$ в $F_\mu$.
Так как вложение $F_0 \to F_\alpha$ является Морита-эквивалентностью, то существует частичный морфизм $\tau$ в $\cat{C}_{F_0}$ такой, что $\tau$ изоморфен $\sigma[\tau_i(x_i)/x_i]$ в $F_\alpha$.
Искомый частичный морфизм можно определить как композицию $\tau$ и $\langle t_i' \rangle_{i \in I}$.

Аналогично доказывается тот факт, что для любой формулы $\varphi$ теории $F_\mu$ с переменными в $V$ существует подобъект $X$ объекта $\prod V$ в $F_0$ такой, что $X$ изоморфен в $F_\mu$ подобъекту, соответствующему $\varphi$.
Отсюда следует, что функтор $\cat{C}_{F_0} \to \cat{C}_{F_\mu}$ существенно сюръективен на объектах.

Пусть $\lambda$ -- регулярный кардинал такой, что $F_\mu$ является $\lambda$-представимой теорией.
По \dprop{th-fib} морфизм $\eta_{F_0} : F_0 \to \fs{Th}^\lambda(\fs{Cl}^\lambda(F_0))$ факторизуется через $F_0 \to F_\mu$.
Так как $\eta_{F_0}$ является Морта-эквивалентностью, то этот морфизм инъективен на морфизмах.
Следовательно, это верно и для $F_0 \to F_\mu$.
Нам осталось показать, что $F_0 \to F_\mu$ сюръективен на морфизмах.
Мы уже видели, что для любого морфизма $t$ в $F_\mu$ сущесвует частичный морфизм $t'$ в $F_0$, эквивалентный $t$.
Нам нужно показать, что $t'$ является тотальным морфизмом, то есть, что подобъект $t'\!\downarrow$ является максимальным.
Так как этот подобъект является максимальным в $F_\mu$, то он является таковым и в $\fs{Th}^\lambda(\fs{Cl}^\lambda(F_0))$.
Так как эта теория Морита-эквивалентна $F_0$, то это верно и в $F_0$.
\end{proof}

Для завершения конструкции модельной структуры нам понадобится еще одна лемма:

\begin{lem}[th-triv-fib]
Если Морита-эквивалентность $f$ имеет RLP по отношению к морфизмам $j^{\kappa,\kappa'}_m$, то она имеет RLP по отношению к морфизмам $i^\kappa_t$, $i^\kappa_p$ и $i^\kappa_f$.
\end{lem}
\begin{proof}
Докажем, что $f$ имеет RLP по отношению к $i^\kappa_p$.
Пусть $V$ -- производный сорт $T$, являющийся произведением сортов, и пусть $\varphi$ -- формула $T'$ с переменными в $f(V)$.
Так как $f_! : \cat{C}_T \to \cat{C}_{T'}$ является эквивалентностью, то существует производный сорт $s$ теории $T$ и мономорфизм $\sigma : s \to V$ такие, что $f(\sigma)$ и $\varphi$ изоморфны как подобъекты $f(V)$.
Пусть $\sigma'$ -- морфизм из $\varphi$ в $f(\sigma)$.
Так как $f$ имеет RLP по отношению к $j_m^{\kappa,\kappa'}$, то существует частичный морфизм $\sigma''$ из $V$ в $s$ такой, что $f(\sigma'') = \sigma'$.
Так как $\varphi$ верна тогда и только тогда, когда $\sigma'$ определен, мы можем определить поднятие $\varphi$ как $\sigma''(\overline{x})\!\downarrow$.

Докажем, что $f$ имеет RLP по отношению к $i^\kappa_f$.
Пусть $\{ s_i \}_{i \in I}$ -- производный сорт $T$ и пусть $\varphi$ и $\psi$ -- формулы $T$ с переменными в $V$ такие, что $f(\varphi)$ влечет $f(\psi)$.
Так как в категории $\cat{C}_{T'}$ у нас есть морфизм между подобъектами $f(\varphi)$ и $f(\psi)$, то у нас есть и морфизм $\sigma$ между подобъектами $\varphi$ и $\psi$ в категории $\cat{C}_T$.
Так как $f(\psi \circ \sigma) = f(\varphi)$, то $\psi \circ \sigma = \varphi$.
Другими словами, $\varphi$ влечет, что $\sigma_i(\overline{x}) = x_i$ для всех $i \in I$.
Так как $\varphi$ влечет $\psi[\sigma_i(\overline{x})/x_i]$, то этот факт означает, что $\varphi$ влечет $\psi$.

Нам осталось показать, что $f$ имеет RLP по отношению к $i^\kappa_t$.
Пусть $s$ -- сорт $T$, $V$ -- производный сорт $T$, являющийся произведением сортов, и пусть $t'$ -- суженный терм $T'$ сорта $f(s)$ с переменными в $f(V)$.
Тогда у нас есть мономорфизм $m' : (t'\!\downarrow) \to f(V)$ и морфизм $t' : (t'\!\downarrow) \to f(s)$ в $\cat{C}_{T'}$.
Так как $f$ является Морита-эквивалентностью, у нас есть мономорфизм $m : U \to V$, морфизм $t : U \to s$ и изоморфизм подобъектов $\tau' : (t'\!\downarrow) \to f(U)$ такие, что $f(t) \circ \tau' = t'$.
Так как $f$ имеет RLP по отношению к $j_m^{\kappa,\kappa'}$, то существует суженный терм $\tau$ сигнатуры $V \to U$ такой, что $f(\tau) = \tau'$.
Поднятие $t'$ можно определить как $t \circ \tau$.
\end{proof}

Теперь мы можем завершить конструкцию модельной категории:

\begin{thm}[th-l-model-str]
Категория $\Th^\lambda$ является комбинаторной модельной категорией с Морита-эквивалентностями в качестве слабых эквивалентностей, множеством порождающих корасслоений $\I^\lambda$ и множеством порождающих тривиальных корасслоений $\J^\lambda$.
Функтор вложения $\Th^\lambda \to \Th^\mu$ для $\lambda \leq \mu$ является левым Квилленовским функтором.
\end{thm}
\begin{proof}
Категория является локально представимой по \dprop{th-pres}.
Проверим условия \oprop{model-cat}.
Факторизации морфизмов существуют по \dprop{small-object-argument}.
По \dprop{th-func-mod} соответствие $T \mapsto \Mod{T}$ является функториальным.
Отсюда следует, что класс Морита-эквивалентностей удовлетворяет свойству 2-из-3 и замкнут относительно ретрактов.
Так как любой морфизм в $\Icof[\J^\lambda]$ является ретрактом морфизма из $\Icell[\J^\lambda]$, то из \olem{th-triv-cof} следует, что $\Icof[\J^\lambda] \subseteq \we \cap \Icof[\I^\lambda]$.

Пусть $f : T \to T'$ -- морфизм теорий, принадлежащий $\Iinj[\I^\lambda]$.
Докажем, что $f$ является Морита-эквивалентностью.
Так как $f$ имеет RLP по отношению к $i_s$, то $f$ сюръективен на сортах.
Так как $f$ имеет RLP по отношению к $i_p^\kappa$, то $f$ сюръективен на $\lambda$-достижимых формулах.
Отсюда следует, что $f$ сюръективен на производных сортах, а значит $f_! : \cat{C}_T \to \cat{C}_{T'}$ сюръективен на объектах.
Сюръективность и инъективность $f_!$ на морфизмах следует из того факта, что $f$ имеет RLP по отношению к $i_t^\kappa$ и $i_f^\kappa$.
Таким образом, $f$ является Морита-эквивалентностью по \dprop{th-morita-char}.

Докажем теперь, что $\Iinj[\J^\lambda] \cap \we \subseteq \Iinj[\I^\lambda]$.
Пусть $f : T \to T'$ -- морфизм теорий, принадлежащий $\Iinj[\J^\lambda] \cap \we$.
Пусть $s'$ -- сорт $T'$.
Так как $f_! : \cat{C}_T \to \cat{C}_{T'}$ существенно сюръективен на объектах, то сущесвует производный сорт $s$ теории $T$ и изоморфизм между $f(s)$ и $s'$ в $\cat{C}_{T'}$.
Так как $f$ имеет RLP по отношению к $j_s^\kappa$, то существует сорт $s''$ теории $T$ такой, что $f(s'') = s$.
Таким образом $f$ имеет RLP по отношению к $i_s$.
\Rlem{th-triv-fib} влечет, что $f$ имеет RLP по отношению к остальным морфизмам в $\I^\lambda$.

Если $\lambda < \mu$, то функтор $\Th^\lambda \to \Th^\mu$ является левым споряженным по \dprop{th-adj}.
Он является левым Квилленовским функтором, так как $\I^\lambda \subseteq \I^\mu$ и $\J^\lambda \subseteq \J^\mu$.
\end{proof}

\begin{remark}
Любая теория является корасслоенной.
Теория является расслоенной тогда и только тогда, когда любой производный сорт в ней изоморфен некоторому сорту и любой частичный мономорфизм между сортами имеет частичный обратный.
\end{remark}

Теперь мы обсудим категорию $\Th^\lambda_\mathcal{S}$.
Пораждающие корасслоения в этой категории строятся из морфизмов, приведенных ниже.
В этих определениях $V$ -- это множество мощности $\kappa$, состоящее из элементов $\mathcal{S}$, и $s$ -- элемент $\mathcal{S}$.
\begin{align*}
i_{\mathcal{S},t}^\kappa & : (\mathcal{S}, \varnothing, \varnothing, \varnothing) \to (\mathcal{S}, \{ \sigma : \prod V \to s \}, \varnothing, \varnothing) \\
i_{\mathcal{S},p}^\kappa & : (\mathcal{S}, \varnothing, \varnothing, \varnothing) \to (\mathcal{S}, \varnothing, \{ R : \prod V \}, \varnothing) \\
i_{\mathcal{S},f}^\kappa & : (\mathcal{S}, \varnothing, \{ R, R' : \prod V \}, \varnothing) \to (\mathcal{S}, \varnothing, \{ R, R' : \prod V \}, \{ R(\overline{x}) \sststile{}{\overline{x}} R'(\overline{x}) \})
\end{align*}
Множество $\I_\mathcal{S}^\lambda$ определяется как $\{ i_{\mathcal{S},t}^\kappa, i_{\mathcal{S},p}^\kappa, i_{\mathcal{S},f}^\kappa \mid \kappa < \lambda \}$.
Пусть $\I_\mathcal{S}$ -- объединение множеств $\I_\mathcal{S}^\lambda$ для всех $\lambda$.

Пусть $I$ и $J$ -- множества, состоящие из элементов $\mathcal{S}$, мощности $\kappa$ и $\kappa'$, соответственно.
Тогда мы определим следующую теорию:
\[ T_{\mathcal{S},m}^{\kappa,\kappa'} = (\mathcal{S}, \{ \sigma_j : \prod_{i \in I} s_i \to s_j' \mid j \in J \}, \varnothing, \{ \bigwedge_{j \in J} \sigma_j(\overline{x}) = \sigma_j(\overline{x}') \sststile{}{\overline{x},\overline{x}'} \bigwedge_{i \in I} x_i = x_i' \}) \]
Теория $T_{\mathcal{S},i}^{\kappa,\kappa'}$ состоит из функциональных символов $\{ \sigma_j : \prod_{i \in I} s_i \to s_j' \mid j \in J \} \amalg \{ \sigma_i' : \prod_{j \in J} s_j' \to s_i \mid i \in I \}$ и следующих аксиом:
\begin{align*}
& \bigwedge_{j \in J} \sigma_j(\overline{x})\!\downarrow\ \sststile{}{\overline{x}} \bigwedge_{i \in I} \sigma_i'(\{ \sigma_j(x_i) \}_{j \in J}) = x_i \\
& \bigwedge_{i \in I} \sigma_i'(\overline{x}')\!\downarrow\ \sststile{}{\overline{x}'} \bigwedge_{j \in J} \sigma_j(\{ \sigma_i'(x_j') \}_{i \in I}) = x_j'
\end{align*}
Морфизм $j_{\mathcal{S},m}^{\kappa,\kappa'}$ определяется как очевидный морфизм $T_{\mathcal{S},m}^{\kappa,\kappa'} \to T_{\mathcal{S},i}^{\kappa,\kappa'}$.
Множество $\J_\mathcal{S}^\lambda$ состоит из морфизмов $j_{\mathcal{S},m}^{\kappa,\kappa'}$ для всех $\kappa < \lambda$ и $\kappa' < \lambda$.
Пусть $\J_\mathcal{S}$ -- объединение множеств $\J_\mathcal{S}^\lambda$ для всех $\lambda$.

\begin{prop}[th-l-s-model-str]
На категории $\Th^\lambda_\mathcal{S}$ существует комбинаторная модельная структура, в которой все морфизмы являются корасслоениями, расслоениями являются морфизмы в $\Iinj[\J^\lambda]$, и слабыми эквивалентностями являются Морита-эквивалентности.
Множества $\I^\lambda$ и $\J^\lambda$ пораждают корасслоения и расслоения, соответственно.
Функтор вложения $\Th^\lambda_\mathcal{S} \to T_\mathcal{S}/\Th^\lambda$ является левым Квилленовским функтором.
\end{prop}
\begin{proof}
Если морфизм $f$ в $\Th_\mathcal{S}$ имеет RLP по отношению к $\I^\lambda_\mathcal{S}$, то он имеет RLP по отношению к $\I$.
Из \oprop{th-cof} следует, что он имеет RLP по отношению ко всем морфизмам в $\Th_\mathcal{S}$, так как все такие морфизмы инъективны на сортах.
Таким образом, $f$ является изоморфизмом.
Отсюда следует, что множество $\I^\lambda_\mathcal{S}$ пораждает все морфизмы в категории $\Th_\mathcal{S}$.
Морфизмы в $\Icof[\J_\mathcal{S}^\lambda]$ являются Морита-эквивалентностями по \dlem{th-triv-cof}.
Тривиальные расслоения имеют RLP по отношению к $\Iinj[\I_\mathcal{S}^\lambda]$ по \dlem{th-triv-fib}.
Функтор $\Th^\lambda_\mathcal{S} \to T_\mathcal{S}/\Th^\lambda$ очевидно сохраняет пораждающие корасслоения и тривиальные корасслоения.
\end{proof}

\subsection{Моноидальная структура}

В этом подразделе мы определим структуру симметричной моноидальной категории на $\Th^\lambda$ и $\Th$.
Пусть $T = (\mathcal{S},\mathcal{F},\mathcal{P},\mathcal{A})$ и $T' = (\mathcal{S}',\mathcal{F}',\mathcal{P}',\mathcal{A}')$ -- две теории.
Тогда мы определим их тензорное произведение $T \otimes T'$.
Сорта этой теории -- это $\mathcal{S} \times \mathcal{S}'$.
Мы будем обозначать сорт этой теории как $[s,s']$, где $s \in \mathcal{S}$ и $s' \in \mathcal{S}'$.
Функциональные символы этой теории -- это $\mathcal{F} \times \mathcal{S}' \amalg \mathcal{S} \times \mathcal{F'}$.
Мы будем обозначать функциональные символы этой теории как $[\sigma,s']$ и $[s,\sigma']$, где $\sigma \in \mathcal{F}$, $s' \in \mathcal{S}'$, $s \in \mathcal{S}$ и $\sigma' \in \mathcal{F}'$.
Если $\sigma : \prod_{i \in I} s_i \to s$, то $[\sigma,s'] : \prod_{i \in I} [s_i,s'] \to [s,s']$.
Аналогично, если $\sigma' : \prod_{i \in I} s_i' \to s'$, то $[s,\sigma'] : \prod_{i \in I} [s,s_i'] \to [s',s]$.
Предикатные символы этой теории -- это $\mathcal{P} \times \mathcal{S}' \amalg \mathcal{S} \times \mathcal{P}' \amalg \mathcal{P} \times \mathcal{F}' \amalg \mathcal{F} \times \mathcal{P}' \amalg \mathcal{F} \times \mathcal{F}' \amalg \mathcal{P} \times \mathcal{P}'$.
Обозначения и сигнатуры для этих предикатных символов приведны ниже.
Если $R : \prod_{i \in I} s_i$, $R' : \prod_{j \in J} s_j'$, $\sigma : \prod_{i \in I} s_i \to s'$ и $\sigma' : \prod_{j \in J} s_j' \to s'$, то сигнатуры этих предикатных символов определяются следующим образом:

\begin{tabular}{ l l }
  $[R,s'] : \prod_{i \in I} [s_i,s']$ & $[s,R'] : \prod_{j \in J} [s,s_j']$ \\
  $[R,\sigma'] : \prod_{(i,j) \in I \times J} [s_i,s_j']$ & $[\sigma,R'] : \prod_{(i,j) \in I \times J} [s_i,s_j']$ \\
  $[\sigma,\sigma'] : \prod_{(i,j) \in I \times J} [s_i,s_j']$ & $[R,R'] : \prod_{(i,j) \in I \times J} [s_i,s_j']$ \\
\end{tabular}

Теперь мы определим несколько вспомогательных формул и термов.
Для каждого терма $t$ теории $T$ сорта $s$ с переменными в $\{ x_i : s_i \}_{i \in I}$ и сорта $s' \in \mathcal{S}'$ мы определим терм $[t,s']$ сорта $[s,s']$ с переменными в $\{ x_i : [s_i,s'] \}_{i \in I}$.
Если $t = x_i$, то $[t,s'] = x_i$.
Если $t = \sigma(\{ t_k \}_{k \in K})$, то $[t,s'] = [\sigma,s']([t_k,s'])$.
Для каждой формулы $\varphi$ теории $T$ с переменными в $\{ x_i : s_i \}_{i \in I}$ и сорта $s' \in \mathcal{S}'$ мы определим формулу $[\varphi,s']$ с переменными в $\{ x_i : [s_i,s'] \}_{i \in I}$.
Если $\varphi = (t_1 = t_2)$, то $[\varphi,s']$ определяется как $[t_1,s'] = [t_2,s']$.
Если $\varphi = R({ t_k }_{k \in K})$, то $[\varphi,s']$ определяется как $[R,s'](\{ [t_k,s'] \}_{k \in K})$.
Если $\varphi = \bigwedge_{k \in K} \varphi_k$, то $[\varphi,s']$ определяется как $\bigwedge_{k \in K} [\varphi_k,s']$.
Термы $[s,t']$ и формулы $[s,\psi]$ определяются аналогичным образом.

Для каждого терма $t$ теории $T$ с переменными в $\{ x_i : s_i \}_{i \in I}$ и каждого предикатного символа $R' : \prod_{j \in J} s_j'$ теории $T'$
мы определим формулу $[t,R']$ с переменными в $\{ z_{i,j} : [s_i,s_j'] \}_{(i,j) \in I \times J}$.
Если $t = x_i$, то $[t,R'] = \top$.
Если $t = \sigma(\{ t_k \}_{k \in K})$, то $[t,R'] = [\sigma,R'](\{ [t_k,s_j'][\{ z_{i,j}/x_i \}_{i \in I}] \}_{(k,j) \in K \times J}) \land \bigwedge_{k \in K} [t_k,R']$.
Аналогично определяются формулы $[R,t']$, $[t,\sigma']$ и $[\sigma,t']$.

Для каждой формулы $\varphi$ теории $T$ с переменными в $\{ x_i : s_i \}_{i \in I}$ и каждого предикатного символа $R' : \prod_{j \in J} s_j'$ теории $T'$
мы определим формулу $[\varphi,R']$ с переменными в $\{ z_{i,j} : [s_i,s_j'] \}_{(i,j) \in I \times J}$.
Если $\varphi = (t_1 = t_2)$, то $[\varphi,R']$ определяется как $[t_1,R'] \land [t_2,R'] \land \bigwedge_{j \in J} ([t_1,s_j'] = [t_2,s_j'])[\{ z_{i,j}/x_i \}_{i \in I}]$.
Если $\varphi = R(\{ t_k \}_{k \in K})$, то $[\varphi,R']$ определяется как $[R,R'](\{ [t_k,s_j'][\{ z_{i,j}/x_i \}_{i \in I}] \}_{(k,j) \in K \times J}) \land \bigwedge_{k \in K} [t_k,R']$.
Если $\varphi = \bigwedge_{k \in K} \varphi_k$, то $[\varphi,R']$ определяется как $\bigwedge_{k \in K} [\varphi_k,R']$.
Аналогично определяются формулы $[R,\psi]$, $[\varphi,\sigma']$ и $[\sigma,\psi]$.

Теперь мы можем закончить описание теории $T \otimes T'$.
Нам осталось определить ее множество аксиом.
Для каждой аксиомы $\varphi \sststile{}{\{ x_i : s_i \}_{i \in I}} \psi$ теории $T$ и каждого сорта $s' \in \mathcal{S}'$ мы добавляем аксиому $[\varphi,s'] \sststile{}{\{ x_i : [s_i,s'] \}_{i \in I}} [\psi,s']$.
Для каждого $R' \in \mathcal{P}'$ мы добавляем аксиому
\[ \bigwedge_{i \in I} [s_i,R'](\{ z_{i,j} \}_{j \in J}) \land [\varphi,R'] \sststile{}{\{ z_{i,j} : [s_i,s_j'] \}_{(i,j) \in I \times J}} [\psi,R'] \]
Аналогичные аксиомы добавляются для каждого функционального символа из $\mathcal{F}'$.
Кроме того, аналогичные аксиомы добавляются для всех аксиом из $T'$, всех сортов из $\mathcal{S}$ и всех предикатных и функциональных символов из $\mathcal{P}$ и $\mathcal{F}$.
Для каждых $R \in \mathcal{P}$ и $R' \in \mathcal{P}'$ мы добавляем аксиому
\[ [R,R'](\{ z_{i,j} \}_{(i,j) \in I \times J}) \sststile{}{z_{i,j}} \bigwedge_{i \in I} [s_i,R'](\{ z_{i,j} \}_{j \in J}) \land \bigwedge_{j \in J} [R,s_j'](\{ z_{i,j} \}_{i \in I}) \]
Для каждых $R \in \mathcal{P}$ и $\sigma' \in \mathcal{F}'$ мы добавляем аксиому
\[ [R,\sigma'](\{ z_{i,j} \}_{(i,j) \in I \times J}) \sststile{}{z_{i,j}} [R,s'](\{ [s_i,\sigma'](\{ z_{i,j} \}_{j \in J}) \}_{i \in I}) \land \bigwedge_{j \in J} [R,s_j'](\{ z_{i,j} \}_{i \in I}) \]
Аналогичная аксиома добавляется для каждых $\sigma \in \mathcal{F}$ и $R' \in \mathcal{P}'$.
Наконец, для каждых $\sigma \in \mathcal{F}$ и $\sigma' \in \mathcal{F}'$ мы добавляем следующую аксиому:
\[ [\sigma,\sigma'](\{ z_{i,j} \}_{(i,j) \in I \times J}) \sststile{}{z_{i,j}} [\sigma,s'](\{ [s_i,\sigma'](\{ z_{i,j} \}_j) \}_i) = [s,\sigma'](\{ [\sigma,s_j'](\{ z_{i,j} \}_i) \}_j) \]
Таким образом, множество аксиом $T \otimes T'$ можно коротко описать как $\mathcal{A} \times \mathcal{S}' \amalg \mathcal{S} \times \mathcal{A}' \amalg \mathcal{A} \times \mathcal{P}' \amalg \mathcal{P} \times \mathcal{A}' \amalg \mathcal{A} \times \mathcal{F}' \amalg \mathcal{F} \times \mathcal{A}' \amalg \mathcal{P} \times \mathcal{P}' \amalg \mathcal{P} \times \mathcal{F}' \amalg \mathcal{F} \times \mathcal{P}' \amalg \mathcal{F} \times \mathcal{F}'$.

Для любой категории $\cat{C}$ с $\lambda$-малыми пределами и любой $\lambda$-достижимой теории можно рассмотреть категорию моделей $T$ в $\cat{C}$.
Интерпретация $M$ сигнатуры $(\mathcal{S},\mathcal{F},\mathcal{P})$ в $\cat{C}$ состоит из $\mathcal{S}$-индексированного множества $\{ M_s \}_{s \in \mathcal{S}}$ объектов $\cat{C}$,
подобъектов $M_R : d^M_R \to \prod_{i \in I} M_{s_i}$ для каждого предикатного символа $R : \prod_{i \in I} s_i$
и частичных морфизмов $(d^M_\sigma \to \prod_{i \in I} M_{s_i}, M_\sigma : d^M_\sigma \to M_s)$ для каждого функционального символа $\sigma : \prod_{i \in I} s_i \to s$.
Интерпретацию сигнатуры можно расширить до интерпретации всех (суженных) термов и формул очевидным образом.
Секвенция $\varphi \sststile{}{V} \psi$ верна в некоторой интерпретации, если подобъект, соответствующий $\varphi$ является подобъектом подобъекта, соответствующего $\psi$.
Модель теории в $\cat{C}$ -- это интерпетация подлежащей сигнатуры в этой категории, в которой верны все аксиомы.
Морфизм моделей $M$ и $N$ -- это коллекция морфизмов $\{ f_s : M_s \to N_s \}_{s \in \mathcal{S}}$, сохраняющие предикатные и функциональные символы в смысле, приведенном ниже.
Для каждого предикатного символа $R : \prod_{i \in I} s_i$ морфизм $d^M_R \to \prod_{i \in I} M_{s_i} \xrightarrow{\prod_{i \in I} f_{s_i}} \prod_{i \in I} N_{s_i}$ факторизуется через $d^N_R \to \prod_{i \in I} N_{s_i}$.
Для каждого функционального символа $\sigma : \prod_{i \in I} s_i \to s$ морфизм $d^M_\sigma \to \prod_{i \in I} M_{s_i} \xrightarrow{\prod_{i \in I} f_{s_i}} \prod_{i \in I} N_{s_i}$
факторизуется через $d^N_\sigma \to \prod_{i \in I} N_{s_i}$ и следующий квадрат коммутирует:
\[ \xymatrix{ d^M_\sigma \ar[r]^{M_\sigma} \ar[d] & M_s \ar[d]^{f_s} \\
              d^N_\sigma \ar[r]_{N_\sigma}        & N_s
            } \]
Композиция морфизмов и тождественные морфизмы определяются очевидным образом.
Мы будем обозначать эту категорию $\Mod{T}(\cat{C})$.

\begin{prop}[tensor-mod]
Категория моделей теории $T \otimes T'$ эквивалентна категории $\Mod{T}(\Mod{T'})$.
\end{prop}
\begin{proof}
Пусть $T' = (\mathcal{S}',\mathcal{F}',\mathcal{P}',\mathcal{A}')$.
Предположим сначала, что $T = (\mathcal{S},\varnothing,\varnothing,\varnothing)$.
Тогда категория $\Mod{T}(\Mod{T'})$ эквивалентна $\Mod{T'}^\mathcal{S}$ в этом случае.
Так как $T \otimes T' = (\mathcal{S} \times \mathcal{S}', \mathcal{S} \times \mathcal{F}', \mathcal{S} \times \mathcal{P}', \mathcal{S} \times \mathcal{A}')$, то модель $T \otimes T'$ -- это $\mathcal{S}$-индексированное множество моделей $T'$.
Другими словами, категории $\Mod{(T \otimes T')}$ и $\Mod{T}(\Mod{T'})$ эквивалентны.

Пусть $X$ -- объект $\Mod{T'}$.
Тогда подобъект $Y$ объекта $X$ в этой категории -- это тройка $(\{ Y_{s'} \}_{s' \in \mathcal{S}'}, \{ Y_{R'} \}_{R' \in \mathcal{P}'}, \{ Y_{\sigma'} \}_{\sigma' \in \mathcal{F}'})$, удовлетворяющая условиям приведенным ниже.
Множества $Y_{s'}$ являются подмножествами $X_{s'}$.
Если $R' : \prod_{i \in I} s_i'$, то множество $Y_{R'}$ является подмножеством $X(R') \cap \prod_{i \in I} Y_{s_i'}$.
Если $\sigma' : \prod_{i \in I} s_i' \to s'$, то множество $Y_{\sigma'}$ является подмножеством $X_{\sigma'} \cap \prod_{i \in I} Y_{s_i'}$, где $X_{\sigma'}$ -- это домен $X(\sigma')$.
Кроме того, для любого $\overline{y} \in Y_{\sigma'}$ верно, что $X(\sigma')(\overline{y}) \in Y_{s'}$.
Эти условия означают, что $Y$ является подинтерпретацией $X$.
Чтобы $Y$ была подмоделью, необходимо еще потребовать, чтобы аксиомы $T'$ выполнялись в $Y$, то есть, чтобы для любой аксиомы $\varphi \sststile{}{V} \psi$ множество $Y(\varphi)$ было бы подмножеством $Y(\psi)$.

Теперь предположим, что $T = (\mathcal{S},\varnothing,\mathcal{P},\varnothing)$.
Модель $T$ в $\Mod{T'}$ состоит из $\mathcal{S}$-индексированного множества $Y$ моделей $T'$ вместе с подобъектом $Y^R$ объекта $\prod_{i \in I} Y_{s_i}$ для каждого предикатного символа $R : \prod_{i \in I} s_i$ в $\mathcal{P}$.
Для каждого $R \in \mathcal{P}$ интерпретация $[R,R']$ задает подмножество $Y^R_{R'}$, а интерпретация $[R,\sigma']$ задает подмножество $Y^R_{\sigma'}$.
Аксиомы в $\mathcal{P} \times \mathcal{P}'$ и $\mathcal{P} \times \mathcal{F}'$ соответствуют тем фактам, что $Y^R_{R'}$ и $Y^R_{\sigma'}$ являются подобъектами $Y^R$ и $Y^R$ замкнут относительно функциональных и предикатных символов $T'$.
Условие, что аксиомы $T'$ выполнены в $Y^R$, эквивалентны верности аксиом в $\mathcal{P} \times \mathcal{A}'$.
Таким образом, модель $T$ в $\Mod{T}'$ -- это в точности модель теории $T \otimes T'$.

Теперь предположим, что $T = (\mathcal{S},\mathcal{F},\mathcal{P},\varnothing)$.
Для каждого $\sigma \in \mathcal{P}$ интерпретация $[\sigma,s']$ задает необходимый частичный морфизм, интерпретация $[\sigma,R']$ и $[\sigma,\sigma']$ задает структуру подобъекта на домене $\sigma$.
Аксиомы из $\mathcal{F} \times \mathcal{A}' \amalg \mathcal{F} \times \mathcal{P}' \amalg \mathcal{F} \times \mathcal{F}'$ соответствуют тому факту, что эта структура задает подмодель и что функции, соответствующие $\sigma$, являются морфизмами моделей.

Наконец, предположим, что $T$ -- это произвольная теория $(\mathcal{S},\mathcal{F},\mathcal{P},\mathcal{A})$.
Чтобы доказать, что $\Mod{(T \otimes T')}$ эквивалентна $\Mod{T}(\Mod{T'})$, нам достаточно показать, что для любой модели $X$ теории $(\mathcal{S},\mathcal{F},\mathcal{P},\varnothing) \otimes T'$
аксиомы в $\mathcal{A}$ верны в $X$, если ее рассматривать как объект $\Mod{T}(\Mod{T'})$, тогда и только тогда, когда в $X$ верны аксиомы в $\mathcal{A} \times \mathcal{S}' \amalg \mathcal{A} \times \mathcal{P}' \amalg \mathcal{A} \times \mathcal{F}'$.
Аксиомы в $\mathcal{A} \times \mathcal{S}'$ верны тогда и только тогда, когда для любой аксиомы $\varphi \sststile{}{V} \psi$ в $\mathcal{A}$ и любого $s' \in \mathcal{S}'$ множество $X(\varphi)_{s'}$ является подмножеством $X(\psi)_{s'}$.
Чтобы вложение $X(\varphi) \to X(\psi)$ было морфизмом моделей, необходимо, чтобы оно сохраняло предикатные и функциональные символы.
Это верно тогда и только тогда, когда верны аксиомы в $\mathcal{A} \times \mathcal{P}' \amalg \mathcal{A} \times \mathcal{F}'$.
Это завершает доказательство утверждения.
\end{proof}

\begin{prop}
Тензорное произведение теорий задает структуру симметричной моноидальной категории на $\Th$ и $\Th^\lambda$.
Более того, категория $\Th^\lambda$ является моноидальной замкнутой.
\end{prop}
\begin{proof}
Во-первых, заметим, что если теории $T$ и $T'$ являются $\lambda$-достижимыми, то теория $T \otimes T'$ также является таковой, то есть $\Th^\lambda$ замкнута относительно тензорного произведения.
Теперь докажем, что тензорное произведения функториально.
Пусть $f : T_1 \to T_2$ и $f' : T_1' \to T_2'$ -- два морфизма теорий.
Тогда мы определим $f \otimes f' : T_1 \otimes T_1' \to T_2 \otimes T_2'$.
Если $s \in \mathcal{S}$ и $s' \in \mathcal{S}'$, то $(f \otimes f')[s,s'] = [f(s),f'(s')]$.
Если $\sigma \in \mathcal{F}$ и $\sigma' \in \mathcal{F}'$, то $(f \otimes f')[\sigma,s'] = [f(\sigma),f'(s')]$ и $(f \otimes f')[s,\sigma'] = [f(s),f'(\sigma')]$, где $[t|_\varphi,s'] = [t,s']|_{[\varphi,s']}$ и $[s,t'|_\psi] = [s,t']|_{[s,\psi]}$.
Если $R \in \mathcal{F}$ и $R' \in \mathcal{F}'$, то $(f \otimes f')[R,s'] = [f(R),f'(s')]$ и $(f \otimes f')[s,R'] = [f(s),f'(R')]$.

Для любой формулы $\varphi$ теории $T$ и (суженного) терма $t'$ теории $T'$ можно определить формулу $[\varphi,t']$, используя те же правила, что и для $[R,t']$.
Аналогично определяется формула $[t,\psi]$ для любого (суженного) терма $t$ теории $T$ и любой формулы $\psi$ теории $T'$.
Формулу $[\varphi,\psi]$ можно определить рекурсией как по $\varphi$, так и по $\psi$.
С точностью до эквивалентности формул результат будет одинаковым.
Теперь мы можем определить действие $f \otimes f'$ на остальных символах: $(f \otimes f')[R,\sigma'] = [f(R),f'(\sigma')]$, $(f \otimes f')[\sigma,R'] = [f(\sigma),f'(R')]$, $(f \otimes f')[R,R'] = [f(R),f'(R')]$ и $(f \otimes f')[\sigma,\sigma'] = [f(\sigma),f'(\sigma')]$.
Все аксиомы теории $T \otimes T'$ остаются верны, если заменить функциональные и предикатные символы произвольными суженными термами и формулами.
Отсюда следует, что $f \otimes f'$ сохраняет аксиомы, а значит является морфизмом теорий.
Если морфизмы $f$ и $f'$ были $\lambda$-достижимыми, то таковым будет и морфизм $f \otimes f'$.
Следовательно, $\otimes$ является не только функтором $\Th \times \Th \to \Th$, но и функтором $\Th^\lambda \times \Th^\lambda \to \Th^\lambda$.

Тензорная единица $I$ определяется как теория $(\{*\},\varnothing,\varnothing,\varnothing)$.
Изоморфизм $\lambda_X : I \otimes X \simeq X$ определяется очевидным образом: $\lambda_X([*,s]) = s$, $\lambda_X([*,\sigma]) = \sigma$ и $\lambda_X([*,R]) = R$.
Изоморфизм $\rho_X : X \otimes I \simeq X$ определяется аналогично.
Естественность этих изоморфизмов проверяется напрямую.
Теперь мы определим естественный изоморфизм $\alpha : (X \otimes Y) \otimes Z \simeq X \otimes (Y \otimes Z)$.
На сортах он определяется очевидным образом: $\alpha([[s_1,s_2],s_3]) = [s_1,[s_2,s_3]]$.
Для любых символов $p_1$, $p_2$ и $p_3$ теорий $T_1$, $T_2$ и $T_3$, соответственно, мы зададим следующие определения:
$\alpha([[s_1,s_2],p_3]) = [s_1,[s_2,p_3]]$, $\alpha([[s_1,p_2],s_3]) = [s_1,[p_2,s_3]]$, $\alpha([[p_1,s_2],s_3]) = [p_1,[s_2,s_3]]$, $\alpha([[p_1,p_2],s_3]) = \alpha([p_1,[p_2,s_3]])$ и $\alpha([[s_1,s_2],p_3]) = \alpha([s_1,[s_2,p_3]])$.
Обратный морфизм задается очевидным образом.
Естественность следует из того факта, что этот морфизм удовлетворяет тем же равенствам, если вместо символов $p_1$, $p_2$ и $p_3$ взять произвольные суженные термы и формулы.
Естественный изоморфизм $B : T \otimes T' \simeq T' \otimes T$ определяется очевидным образом.
Свойства когерентности легко проверяются, так как все приведенные выше морфизмы просто переставляют символы теорий местами.

Нам осталось проверить, что $\Th^\lambda$ является моноидальной замкнутой.
Так как она является локально представимой, чтобы это доказать, достаточно проверить, что для любой теории $T$ функтор $B \otimes -$ сохраняет копределы.
Для копроизведений это очевидно.
Если $E$ -- коуравнитель стрелок $f,g : T_1 \to T_2$, то $B \otimes E$ имеет те же сорта и символы, что и $B \otimes T_2$.
Так как у нас есть стрелка из коуравнителя $E'$ стрелок $B \otimes f$ и $B \otimes g$ в $B \otimes E$.
Следовательно, нам достаточно показать, что все аксиомы $B \otimes E$ верны в $E'$.
Это легко сделать напрямую, перебрав аксиомы $E$.
\end{proof}

\begin{prop}
Категория $\Th^\lambda$ является моноидальной модельной категорией.
\end{prop}
\begin{proof}
Так как все объекты расслоены, то нам достаточно проверить аксиому пушаутов и произведений.
Так как корасслоения -- это в точности морфизмы, инъективные на сортах, то первая часть этой аксиомы следует из того, что она верна в множествах для инъекций.
Чтобы проверить вторую часть этой аксиомы, достаточно доказать, что для любой теории $T$ функтор $T \otimes -$ сохраняет тривиальные корасслоения.
Так как он сохраняет корасслоения и копределы, то достаточно показать, что он отправляет пораждающие тривиальные корасслоения в слабые эквивалентности.

Рассмотрим морфизм $j^\kappa_s : T^\kappa_s \to T^\kappa_{s'}$, где $T^\kappa_{s'} = T^\kappa_s \amalg \{ s \} \cup \fs{Iso}(\overline{\sigma}, \{ \overline{x} : \prod V \mid P(\overline{x}) \}, s)$.
По \dprop{tensor-mod}, модель $M$ теории $T \otimes T^\kappa_s$ -- это просто $V$-индексированное множество $\{ M_x \}_{x \in V}$ моделей $T$ вместе с подмоделью $M_P$ модели $\prod_{x \in V} M_x$.
Модель $M$ теории $T \otimes T^\kappa_{s'}$ -- это модель $T^\kappa_s$ вместе с моделью $M_s$ и изоморфизмом между $M_s$ и $M_P$.
Функтор $(T \otimes j^\kappa_s)^*$ -- очевидный забывающий функтор.
Легко видеть, что этот функтор является эквивалентностью.

Рассмотрим морфизм $j^{\kappa,\kappa'}_m : T^{\kappa,\kappa'}_m \to T^{\kappa,\kappa'}_i$.
Модель $M$ теории $T \otimes T^{\kappa,\kappa'}_m$ состоит из $I$-индексированного множества $\{ M_i \}_{i \in I}$ моделей $T$,
$J$-индексированного множества $\{ M_j' \}_{j \in J}$ моделей $T$, подмодели $M_\sigma$ модели $\prod_{i \in I} M_i$ и мономорфизма $M_\sigma \to \prod_{j \in J} M_j'$.
Модель $M$ теории $T \otimes T^{\kappa,\kappa'}_i$ состоит из $I$-индексированного множества $\{ M_i \}_{i \in I}$ моделей $T$,
$J$-индексированного множества $\{ M_j' \}_{j \in J}$ моделей $T$, подмодели $M_\sigma$ модели $\prod_{i \in I} M_i$, подмодели $M_{\sigma'}$ модели $\prod_{j \in J} M_j'$ и изоморфизма $M_\sigma \simeq M_{\sigma'}$.
Функтор $(T \otimes j^{\kappa,\kappa'}_m)^*$ -- очевидный забывающий функтор.
Так как образ мономорфизма моделей $f : X \to Y$ является подмоделью $Y$, изоморфной $X$, то этот функтор сюръективен на объектах.
Морфизм моделей $M$ и $N$ теории $T \otimes T^{\kappa,\kappa'}_i$ однозначно задается морфизмами $\{ f_i : M_i \to N_i \}_{i \in I}$ и $\{ g_j : M_j' \to N_j' \}_{j \in J}$.
Кроме того, такая пара является морфизмом моделей $T \otimes T^{\kappa,\kappa'}_i$ тогда и только тогда, когда она является морфизмом моделей $T \otimes T^{\kappa,\kappa'}_m$.
Отсюда следует, что функтор $(T \otimes j^{\kappa,\kappa'}_m)^*$ является полным и строгим.
\end{proof}

\subsection{Подлежащие $\infty$-категории категорий $\Th^\lambda$ и $\Th^\lambda_\mathcal{S}$}

Теперь мы опишем моноидальный функтор $F : \Cat \to \Th^\lambda$.
Для каждой категории $\C$ мы определяем теорию $F(\C)$ следующим образом.
Ее сорта -- это объекты $\C$, а для каждого морфизма $f : s \to s'$ мы добавляем функциональный символ соответствующей сигнатуры.
Для каждой пары морфизмов $f$ и $g$ мы добавляем аксиому $\sststile{}{x} (g \circ f)(x) = g(f(x))$.
Для каждого объекта $s$ мы добавляем аксиому $\sststile{}{x} \fs{id}_s(x) = x$.

Чтобы доказать, что $F$ является сильным моноидальным функтором, заметим, что в теории $F(\C)$ нет предикатных символов, а все функциональные символы определены.
Мы будем называть такие теории \emph{тотальными}.
Для них есть более простое описание тензорного произведения.
Пусть $T = (\mathcal{S},\mathcal{F},\mathcal{P},\mathcal{A})$ -- теория, а $T' = (\mathcal{S}',\mathcal{F}',\varnothing,\mathcal{A}')$ -- тотальная теория.
Тогда теория $T \otimes T'$ изоморфна следующей теории:
\[ (\mathcal{S} \times \mathcal{S}', \mathcal{F} \times \mathcal{S}' \amalg \mathcal{S} \times \mathcal{F}', \mathcal{P} \times \mathcal{S}', \mathcal{S} \times \mathcal{A}' \amalg \mathcal{A} \times \mathcal{S}' \amalg \mathcal{P} \times \mathcal{F}' \amalg \mathcal{P} \times \mathcal{A}' \amalg \mathcal{F} \times \mathcal{A}' \amalg \mathcal{F} \times \mathcal{F}'), \]
где функциональные и предикатные символы и аксиомы описываются как раньше.
Другими словами, мы опускаем несколько предикатных символов и аксиом.
Мы можем это сделать, так как эти предикатные символы эквивалентны другим формулам, а эти аксиомы выводимы из остальных.
Действительно, так как секвенция $\sststile{}{\overline{y}} \sigma'(\overline{y})$ выводима в $T'$ для всех $\sigma' \in \mathcal{F}'$, то следующие секвенции тоже выводимы для всех $R \in \mathcal{P}$ и $\sigma \in \mathcal{F}$.
\begin{align*}
\bigwedge_{j \in J} [R,s_j'](\{ z_{i,j} \}_{i \in I}) & \sststile{}{\{ (x_i,y_j) \}_{i,j}} [R,\sigma'](\{ (x_i,y_j) \}_{i,j}) \\
\bigwedge_{j \in J} [\sigma,s_j'](\{ z_{i,j} \}_{i \in I}) & \sststile{}{\{ (x_i,y_j) \}_{i,j}} [\sigma,\sigma'](\{ (x_i,y_j) \}_{i,j})
\end{align*}
Отсюда следует, что формула $[R,\sigma']$ эквивалентна $\bigwedge_{j \in J} [R,s_j'](\{ z_{i,j} \}_{i \in I})$, а формула $[\sigma,\sigma']$ эквивалентна $\bigwedge_{j \in J} [\sigma,s_j'](\{ z_{i,j} \}_{i \in I})$.
Мы можем опустить аксиомы в $\mathcal{A} \times \mathcal{F}'$, так как их заключение доказуемо верно в $T \otimes T'$.
Если обе теории $T$ и $T'$ являются тотальными, то $T \otimes T'$ можно описать еще проще:
\[ (\mathcal{S} \times \mathcal{S}', \mathcal{F} \times \mathcal{S}' \amalg \mathcal{S} \times \mathcal{F}', \varnothing, \mathcal{S} \times \mathcal{A}' \amalg \mathcal{A} \times \mathcal{S}' \amalg \mathcal{F} \times \mathcal{F}') \]

Очевидно, что $F$ отображает тривиальную категорию в моноидальную единицу.
Естественный изоморфизм $\mu_{X,Y} : F(X) \otimes F(Y) \to F(X \times Y)$ строится следующим образом: $\mu_{X,Y}([s,s']) = (s,s')$, $\mu_{X,Y}([\sigma,s']) = (\sigma,\fs{id}_{s'})$, $\mu_{X,Y}([s,\sigma']) = (\fs{id}_s,\sigma')$.
Обратный морфизм $\mu_{X,Y}^{-1} : F(X \times Y) \to F(X) \otimes F(Y)$ строится следующим образом: $\mu_{X,Y}^{-1}(s,s') = [s,s']$, $\mu_{X,Y}^{-1}(\sigma,\sigma')(x) = [s_2,\sigma']([\sigma,s_1'](x))$, где $\sigma : s_1 \to s_2$ и $\sigma' : s_1' \to s_2'$.
Легко видеть, что эти морфизмы взаимно обратны и естественны.

У функтора $F$ есть правый сопряженный $U : \Th^\lambda \to \Cat$.
Объекты $U(T)$ -- это сорта $T$.
Морфизмы между $s$ и $s'$ -- это классы эквивалентности определенных термов сорта $s'$ со свободными переменными в $\{ x : s \}$.
Два терма эквивалентны, если они доказуемо равны в $T$.
Тождественный морфизм -- это класс эквивалентности $x$.
Композиция определяется как подстановка.
Легко видеть, что $U$ является правым сопряженным к $F$.
Кроме того, у функтора $F : \Cat \to \Th$, который определяется аналогичным образом функтору $F : \Cat \to \Th^\lambda$, есть правый сопряженный $U : \Th \to \Cat$, который определяется аналогичным образом функтору $U : \Th^\lambda \to \Cat$.

На категории $\Cat$ существует модельная структура, в которой корасслоения -- это инъективные на объектах функторы, а слабые эквивалентности -- это эквивалентности категорий.
Функтор $F : \Cat \to \Th^\lambda$ сохраняет корасслоения по \dprop{th-cof}.
Тривиальные корасслоения в $\Cat$ пораждаются морфизмом $j : 1 \to D$, где $D$ -- это группоид, состоящий из двух объектов, с уникальным морфизмом между любой парой объектов.
Морфизм $F(j)$ является пушаутом тривиального корасслоения $j_s^1$.
Таким образом, $F : \Cat \to \Th^\lambda$ является левым Квилленовским функтором.
По \cite[Proposition~3.8]{enriched-model-cats} категория $\Th^\lambda$ является модельной категорией, обогащенной над $\Cat$.

Любая модельная категория, обогащенная над $\Cat$, также обогащена над симплициальными множествами.
При этом все симплициальные $\Hom$-множества в этой категории 1-обрезаны.
Отсюда следует, что подлежащая $\infty$-категория такой модельной категории является $(2,1)$-категорией.
Мы утверждаем, что $(2,1)$-категория, соответствующая $\Th^\lambda$, эквивалентна $\bcat{Cart}^\lambda$.
Чтобы это продемонстрировать, достаточно доказать следующее утверждение:

\begin{thm}[th-inf-cat]
Полная $2$-подкатегория $\Th^\lambda$, состоящая из расслоенных теорий, биэквивалентна $\bcat{Cart}^\lambda$.
\end{thm}
\begin{proof}
Чтобы доказать это утверждение, нам понадобится явное описание $\Hom$-категорий в $\Th^\lambda$.
По определению $\Th^\lambda(T,T') = U([T,T'])$, где $[T,T']$ -- внутренний $\Hom$-объект моноидальной структуры на $\Th^\lambda$.
Отсюда можно получить явное описание этой категории.
Ее объекты -- это морфизмы между $T$ и $T'$, а морфизмы между $f : T \to T'$ и $g : T \to T'$ -- это естественные преобразования, то есть морфизмы $\alpha : T \otimes FN(\Delta^1) \to T'$ такие, что $\alpha(-,[0]) = f$ и $\alpha(-,[1]) = g$.
Множество естественных преобразований можно явно определить как множество функций $\alpha$, сопоставляющих каждому сорту $s$ теории $T$ морфизм $\alpha_s : \Hom_{U(T')}(f(s),g(s))$ такой, что следующие секвенции выводимы
для всех предикатных символов $R : \prod_{i \in I} s_i$ и функциональных символов $\sigma : \prod_{i \in I} s_i \to s$ теории $T$:
\begin{align*}
f(R)(\{ x_i \}_{i \in I}) & \sststile{}{\{ x_i \}_{i \in I}} g(R)(\{ \alpha_{s_i}(x_i) \}_{i \in I}) \\
f(\sigma)(\{ x_i \}_{i \in I})\!\downarrow & \sststile{}{\{ x_i \}_{i \in I}} g(\sigma)(\{ \alpha_{s_i}(x_i) \}_{i \in I}) = \alpha_s(f(\sigma)(\{ x_i \}_{i \in I}))
\end{align*}
Тождественные естественные преобразования и композиция естественных преобразований определяются очевидным образом.

Функтор $\fs{Cl}^\lambda : \Th^\lambda \to \bcat{Cart}^\lambda$, определенный в \pprop{th-func-cl}, можно доопределить до $2$-функтора.
Пусть $\alpha$ -- естественное преобразование между морфизмами $f,g : T \to T'$.
Тогда мы определим $\fs{Cl}^\lambda(\alpha)_{\{ \overline{x} : \overline{s} \mid \varphi \}}$ как $\{ \alpha_{s_i}(x_i) \}_{i \in I}$.
Из естественности $\alpha$ следует, что секвенция $f(\varphi) \sststile{}{\overline{x}} g(\varphi)[\{ \alpha_{s_i}(x_i) \}_{i \in I}]$ выводима.
Другими словами, $\fs{Cl}^\lambda(\alpha)_{\{ \overline{x} : \overline{s} \mid \varphi \}}$ действительно является морфизмом.
Чтобы доказать естественность $\fs{Cl}^\lambda(\alpha)$, достаточно показать, что для любого терма $t$ такого, что секвенция $\varphi \sststile{}{\{ x_i : s_i \}_{i \in I}} t\!\downarrow$ выводима,
секвенция $\varphi \sststile{}{\{ x_i : s_i \}_{i \in I}} \alpha_s(f(t)) = g(t)[\{ \alpha_{s_i}(x_i)/x_i \}_{i \in I}]$ также выводима.
Это легко сделать индукцией по $t$, используя естественность $\alpha$.
Тот факт, что $\fs{Cl}^\lambda$ сохраняет тождественные естественные преобразования и их композицию, легко проверяется напрямую.

Мы докажем, что ограничение $\fs{Cl}^\lambda$ на расслоенные теории является биэквивалентностью $2$-категорий.
Мы будем обозначать этот функтор как $\fs{Cl}'$.
Для любого объекта $\C$ категории $\fs{Cl}^\lambda$ у нас есть теория $\fs{Th}^\lambda(\C)$, которая является расслоенной по \dprop{th-fib}.
По \dprop{cl-th} категории $\C$ и $\fs{Cl}'(\fs{Th}^\lambda(\C))$ эквивалентны.
Таким образом, функтор $\fs{Cl}'$ существенно сюръективен на объектах.

Нам осталось доказать, что для любой теории $T$ и любой расслоенной теории $T'$ функтор $\fs{Cl}^\lambda : \Th^\lambda(T,T') \to \bcat{Cart}^\lambda(\fs{Cl}^\lambda(T), \fs{Cl}^\lambda(T'))$ является эквивалентностью категорий.
Строгость этого функтора очевидна.
Докажем его полноту.
Пусть $f,g : T \to T'$ -- морфизмы теорий.
Пусть $\alpha$ -- естественные преобразования между $\fs{Cl}^\lambda(f)$ и $\fs{Cl}^\lambda(g)$.
Тогда мы определим естественное преобразование $\beta$ между $f$ и $g$ как $\beta_s = \alpha_{\{ x : s \mid \top \}}$.
По естественности $\alpha$ следующий квадрат коммутирует:
\[ \xymatrix{ \{ \overline{x} : f(\overline{s}) \mid f(\varphi) \} \ar[rr]^{\alpha_{\{ \overline{x} : \overline{s} \mid \varphi \}}} \ar[d]_{x_i} & & \{ \overline{x} : g(\overline{s}) \mid g(\varphi) \} \ar[d]^{x_i} \\
              \{ y : f(s_i) \mid \top \} \ar[rr]_{\beta_{s_i}}                                                                                    & & \{ y : g(s_i) \mid \top \}
            } \]
Отсюда следует, что $\alpha_{\{ \overline{x} : \overline{s} \mid \varphi \}} = \{ \beta_{s_i}(x_i) \}_{i \in I}$.
Другими словами, $\alpha = \fs{Cl}^\lambda(\beta)$.
Нам еще нужно проверить естественность $\beta$.
Первое условие следует из равенства $\alpha_{\{ \overline{x} : \overline{s} \mid R(\overline{x}) \}} = \{ \beta_{s_i}(x_i) \}_{i \in I}$ и того факта, что 
секвенция $f(R)(\overline{x}) \sststile{}{\overline{x}} g(R)(\alpha_{\{ \overline{x} : \overline{s} \mid R(\overline{x}) \}})$ выводима.
Второе условие следует из равенства $\alpha_{\{ \overline{x} : \overline{s} \mid \sigma(\overline{x}) \downarrow \}} = \{ \beta_{s_i}(x_i) \}_{i \in I}$ и коммутативности следующего квадрата:
\[ \xymatrix{ \{ \overline{x} : f(\overline{s}) \mid f(\sigma)(\overline{x})\!\downarrow \} \ar[rr]^{\alpha_{\{ \overline{x} : \overline{s} \mid \sigma(\overline{x}) \downarrow \}}} \} \ar[d]_{f(\sigma)(\overline{x})} & & \{ \overline{x} : g(\overline{s}) \mid g(\sigma)(\overline{x})\!\downarrow \} \ar[d]^{g(\sigma)(\overline{x})} \\
              \{ y : f(s') \mid \top \} \ar[rr]_{\beta_{s'}}                                                                                                                                                              & & \{ y : g(s') \mid \top \}
            } \]

Нам осталось доказать, что для любого функтора $F : \fs{Cl}^\lambda(T) \to \fs{Cl}^\lambda(T')$, сохраняющего малые $\lambda$-пределы, существует морфизм $f : T \to T'$ такой, что $\fs{Cl}^\lambda(f) \simeq F$.
Пусть $s$ -- некоторый сорт.
Так как $T'$ расслоена, то существует сорт $s'$, изоморфный $F(\{ x : s \mid \top \})$.
Мы определяем $f(s)$ как $s'$.
Изоморфизм $F(\{ x : s \mid \top \}) \simeq f(s)$ будет обозначаться $\alpha_s$.
Пусть $R : \prod_{i \in I} s_i$ -- предикатный символ $T$.
Так как $F$ сохраняет пулбэки, то он сохраняет мономорфизмы.
По \dlem{part-mono} морфизм $\{ \overline{x} : \overline{s} \mid R(\overline{x}) \}) \to \{ \overline{x} : \overline{s} \mid \top \}$ является мономорфизмом.
Так как $T'$ расслоена, то существует частичный обратный $\{ t_j \}_{j \in J}$ к мономорфизму $F(\{ \overline{x} : \overline{s} \mid R(\overline{x}) \}) \to F(\{ \overline{x} : \overline{s} \mid \top \}) \simeq \{ \overline{x} : f(\overline{s}) \mid \top \}$.
Мы определяем $f(R)(\overline{x})$ как $\bigwedge_{j \in J} t_j\!\downarrow$.
Пусть $\sigma : \prod_{i \in I} s_i \to s$ -- функциональный символ $T$.
Тогда у частичного морфизма $F(\{ \overline{x} : \overline{s} \mid \sigma(\overline{x})\!\downarrow \}) \to \{ \overline{x} : f(\overline{s}) \mid \top \}$ есть частичный обратный $r$.
Мы определяем $f(\sigma)$ как $\alpha_s \circ F(\sigma) \circ r$.

Теперь мы проверим, что $f$ действительно является морфизмом теорий, то есть, что он сохраняет теоремы.
Индукцией по терму $t$ легко доказать, что существует (уникальный) изоморфизм $\alpha_t$ такой, что следующая диаграмма коммутирует:
\[ \xymatrix{ F(\{ \overline{x} : \overline{s} \mid t\!\downarrow \}) \ar[r]^-{\alpha_t} \ar[d]_{F(\overline{x})} & \{ \overline{x} : f(\overline{s}) \mid t\!\downarrow \} \ar[d]^{f(\overline{x})} \\
              F(\{ \overline{x} : \overline{s} \mid \top \}) \ar[r]_-{\simeq}                                     & \{ \overline{x} : f(\overline{s}) \mid \top \}
            } \]
Теперь индукцией по $t$ можно доказать, что следующая диаграмма коммутирует:
\[ \xymatrix{ F(\{ \overline{x} : \overline{s} \mid t\!\downarrow \}) \ar[r]^-{\alpha_t} \ar[d]_{F(t)} & \{ \overline{x} : f(\overline{s}) \mid t\!\downarrow \} \ar[d]^{f(t)} \\
              F(\{ y : s \mid \top \}) \ar[r]_-{\alpha_s}                                              & f(s)
            } \]
Используя этот факт, легко доказать, что для любой формулы $\varphi$ существует (уникальный) изоморфизм $\alpha_\varphi$ такой, что следующая диаграмма коммутирует:
\[ \xymatrix{ F(\{ \overline{x} : \overline{s} \mid \varphi \}) \ar[r]^-{\alpha_\varphi} \ar[d]_{F(\overline{x})} & \{ \overline{x} : f(\overline{s}) \mid f(\varphi) \} \ar[d]^{f(\overline{x})} \\
              F(\{ \overline{x} : \overline{s} \mid \top \}) \ar[r]_-{\simeq}                                     & \{ \overline{x} : f(\overline{s}) \mid \top \}
            } \]
Если секвенция $\varphi \sststile{}{\overline{x}} \psi$ выводима, то подобъект $F(\{ \overline{x} : \overline{s} \mid \varphi \})$ является подобъектом $F(\{ \overline{x} : \overline{s} \mid \psi \})$.
Из доказанного выше факта следует, что подобъект $\{ \overline{x} : f(\overline{s}) \mid f(\varphi) \}$ также является подобъектом $\{ \overline{x} : f(\overline{s}) \mid f(\psi) \}$.
Это означает, что секвенция $f(\varphi) \sststile{}{\overline{x}} f(\psi)$.

Нам осталось доказать, что $\fs{Cl}^\lambda(f)$ изоморфен $F$.
В качестве изоморфизма между этими функторами можно взять $\alpha_\varphi$.
Естественность этого изоморфизма следует из свойств, приведенных выше.
\end{proof}

\begin{cor}
Подлежащая $\infty$-категория модельной категории $\Th^\lambda$ эквивалентна $(2,1)$-категории $\bcat{Cart}^\lambda$.
\end{cor}

Теперь мы докажем аналогичное утверждение для категории $\Th^\lambda_\mathcal{S}$.
Для этого нам понадобится следующая лемма:

\begin{lem}[all-cof]
Пусть $\C$ -- модельная категория, в которой все морфизмы являются корасслоениями.
Тогда ее подлежащая $\infty$-категория эквивалентна 1-категории расслоенных объектов $\C$.
\end{lem}
\begin{proof}
На $\Set$ существует декартова моноидальная модельная структура, в которой все морфизмы являются расслоениями и корасслоениями, а слабыми эквивалентностями являются изоморфизмы.
Категория $\C$ является модельной категорией, обогащенной над $\Set$.
Действительно, так как все морфизмы в $\C$ являются корасслоениями, то нам достаточно показать,
что для любой функции $f : A \to B$ в $\Set$ и любой слабой эквивалентности $g : X \to Y$ в $\C$ морфизм $A \cdot Y \amalg_{A \cdot X} B \cdot X \to B \cdot Y$ является слабой эквивалентностью.
Это следует из свойства 2-из-3 и того факта, что в $\C$ слабые эквивалентности замкнуты относительно копроизведений и пушаутов, так как они совпадают с тривиальными корасслоениями.
Любая модельная категория, обогащенная над $\Set$ также обогащена над симплициальными множествами по \cite[Proposition~3.8]{enriched-model-cats}.
Лемма следует из того факта, что все симплициальные $\Hom$-множества в такой категории являются дискретными множествами, изоморфными обычным $\Hom$-множествам.
\end{proof}

Определим $2$-категорию $\bcat{Cart}^\lambda_\mathcal{S}$.
Ее объект -- это малая категория $\C$, содержащая $\lambda$-малые пределы, вместе с инъекцией $i_\C : \mathcal{S} \to \fs{Ob}(\C)$ такой, что любой объект $\C$ является $\lambda$-малым пределом объектов из образа $i_\C$.
Морфизм между $\C$ и $\D$ -- это функтор $F : \C \to \D$, сохраняющий $\lambda$-малые пределы и коммутирующий с инъекциями из $\mathcal{S}$.
Преобразование между функторами $F$ и $G$ -- это естественное преобразование $\alpha_X : F(X) \to G(X)$ такое, что для любого $s \in \mathcal{S}$ верно, что $\alpha_{i_\C(s)} = \fs{id}_{i_\D(s)}$.
Все операции определяются так же как и в $\bcat{Cart}^\lambda$.

\begin{thm}
Подлежащая $\infty$-категория модельной категории $\Th^\lambda_\mathcal{S}$ эквивалентна $\bcat{Cart}^\lambda_\mathcal{S}$.
\end{thm}
\begin{proof}
Так как все морфизмы в $\Th^\lambda_\mathcal{S}$ являются корасслоениями, то по \dlem{all-cof} нам достаточно показать, что $\bcat{Cart}^\lambda_\mathcal{S}$ биэквивалентна категории расслоенных объектов $\Th^\lambda_\mathcal{S}$.
Функтор $\fs{Cl}^\lambda : \Th^\lambda \to \bcat{Cart}^\lambda$ очевидным образом доопределяется до функтора $\fs{Cl}^\lambda_\mathcal{S} : \Th^\lambda_\mathcal{S} \to \bcat{Cart}^\lambda_\mathcal{S}$.
Во-первых, заметим, что любое естественное преобразование в $\bcat{Cart}^\lambda$ является изоморфизмом.
Действительно, для объектов из $\mathcal{S}$ это верно по определению, а для остальных объектов это верно так как они являются пределами объектов из $\mathcal{S}$.
Теперь пусть $f,g : T \to T'$ -- пара морфизмов в $\Th^\lambda_\mathcal{S}$.
Нам нужно показать, что если $\alpha$ -- естественное преобразование между $\fs{Cl}^\lambda_\mathcal{S}(f)$ и $\fs{Cl}^\lambda_\mathcal{S}(g)$, то $f = g$ и $\alpha$ является тождественнным преобразованием.
Если $R : \prod_{j \in J} s_j$ -- предикатный символ в $T$, то у нас есть следующая коммутативная диаграмма:
\[ \xymatrix{ \fs{Cl}^\lambda_\mathcal{S}(f)(\{ \overline{x} : \overline{s} \mid R(\overline{x}) \}) \ar[rr]^-{\alpha_{\{ \overline{x} : \overline{s} \mid R(\overline{x}) \}}} \ar[d]_{x_j} & & \fs{Cl}^\lambda_\mathcal{S}(g)(\{ \overline{x} : \overline{s} \mid R(\overline{x}) \}) \ar[d]^{x_j} \\
              \{ x_j : s_j \mid \top \} \ar@{=}[rr]                                                                                                                                          & & \{ x_j : s_j \mid \top \}
            } \]
Остюда следует, что $\alpha_{\{ \overline{x} : \overline{s} \mid R(\overline{x}) \}} = \{ x_j \}_{j \in J}$, и, следовательно, $f(R) \sststile{}{\overline{x}} g(R)$.
Так как $\alpha$ является изоморфизмом, то аналогично $g(R) \sststile{}{\overline{x}} f(R)$, и, следовательно, $f(R) = g(R)$.
Если $\sigma : \prod_{j \in J} s_j \to s$ -- функциональный символ в $T$, то аналогично предыдущему свойству доказывается, что $\alpha_{\{ \overline{x} : \overline{s} \mid \sigma(\overline{x}) \downarrow \}} = \{ x_j \}_{j \in J}$.
Кроме того, у нас есть следующая коммутативная диаграмма:
\[ \xymatrix{ \fs{Cl}^\lambda_\mathcal{S}(f)(\{ \overline{x} : \overline{s} \mid \sigma(\overline{x})\!\downarrow \}) \ar[rr]^-{\alpha_{\{ \overline{x} : \overline{s} \mid \sigma(\overline{x}) \downarrow \}}} \ar[d]_{f(\sigma)} & & \fs{Cl}^\lambda_\mathcal{S}(g)(\{ \overline{x} : \overline{s} \mid \sigma(\overline{x})\!\downarrow \}) \ar[d]^{g(\sigma)} \\
              \{ y : s \mid \top \} \ar@{=}[rr]                                                                                                                                                                                     & & \{ y : s \mid \top \}
            } \]
Отсюда следует, что секвенция $f(\sigma)(\overline{x}) \sststile{}{\overline{x}} f(\sigma)(\overline{x}) = g(\sigma)(\overline{x})$ выводима.
Так как $\alpha$ является изоморфизмом, то секвенция $g(\sigma)(\overline{x}) \sststile{}{\overline{x}} g(\sigma)(\overline{x}) = f(\sigma)(\overline{x})$ также выводима.
Другими словами, $f(\sigma) = g(\sigma)$.
Таким образом, $f = g$.
Так как $\alpha_s = \fs{id}_s$ и любой объект является пределом объектов из $\mathcal{S}$, то $\alpha_X = \fs{id}_X$ для всех $X$.

Пусть $F : \fs{Cl}^\lambda_\mathcal{S}(T) \to \fs{Cl}^\lambda_\mathcal{S}(T')$ -- морфизм в $\bcat{Cart}^\lambda_\mathcal{S}$, где $T'$ -- расслоенная теория.
Тогда мы можем построить морфизм $f : T \to T'$ в $\Th^\lambda_\mathcal{S}$ такой, что $\fs{Cl}^\lambda_\mathcal{S}(f) \simeq F$, аналогично конструкции из \othm{th-inf-cat}.

Нам осталось доказать, что для любого объекта $\C$ в $\bcat{Cart}^\lambda_\mathcal{S}$ существует расслоенная теория $T$ в $\Th^\lambda_\mathcal{S}$ такая, что категория $\fs{Cl}^\lambda_\mathcal{S}(T)$ эквивалентна $\C$ в $\bcat{Cart}^\lambda_\mathcal{S}$.
В качестве предикатных символов $T$ мы возьмем все формулы $\fs{Th}^\lambda(\C)$, в качестве функциональных символов $T$ мы возьмем все термы $\fs{Th}^\lambda(\C)$, а в качестве аксиом $T$ мы возьмем все теоремы $\fs{Th}^\lambda(\C)$.
Так как теория $\fs{Th}^\lambda(\C)$ является расслоенной, то это верно и для теории $T$.
Категория $\fs{Cl}^\lambda(\fs{Th}^\lambda(\C))$ является естественным образом объектом $\bcat{Cart}^\lambda_\mathcal{S}$, и эквивалентность, определенная в \pprop{cl-th}, является эквивалентностью в $\bcat{Cart}^\lambda_\mathcal{S}$.
Следовательно нам достаточно доказать, что $\fs{Cl}^\lambda_\mathcal{S}(T)$ и $\fs{Cl}^\lambda(\fs{Th}^\lambda(\C))$ эквивалентны в $\bcat{Cart}^\lambda_\mathcal{S}$.
У нас есть морфизм теорий $f : T \to \fs{Th}^\lambda(\C)$, которое задает морфизм $\fs{Cl}^\lambda(f) : \fs{Cl}^\lambda_\mathcal{S}(T) \to \fs{Cl}^\lambda(\fs{Th}^\lambda(\C))$ в $\bcat{Cart}^\lambda_\mathcal{S}$.
По определению $T$ этот функтор полон и строг.
Более того, он существенно сюръективен на объектах, так как любой объект $\C$ является пределом объектов из $\mathcal{S}$.
\end{proof}

\section{Модельные теории}

\emph{Модельная теория} -- это теория $T$ вместе с двумя множествами $\I_T$ и $\J_T$ морфизмов категории $\Mod{T}$ таких, что $\I_T \subseteq \J_T$.
По \dprop{cart-mod-dual} морфизм категории $\Mod{T}$ можно представить в виде морфизма классифицирующей категории $T$.
Мы часто будет представлять такие морфизмы в обоих видах.

\section{Конфлюэнтные теории}

\subsection{Разделение аксиом}

Многие теории содержат аксиомы вида
\[ \sigma(x_1, \ldots x_k)\!\downarrow\ \sststile{}{x_1, \ldots x_k} \varphi \]
и зачастую эти аксиомы можно убрать из теории, не сильно ее меняя.
Конкретно, мы докажем, что если отсальные аксиомы удовлетворяют простому естественному условию, то теоремы определенного вида выводимы без этих аксиом.

Мы будем говорить, что аксиомы теории \emph{разделены}, если множество аксиом состоит из двух подмножеств $\mathcal{A}_f$ и $\mathcal{A}_e$, удовлетворяющих следующим условиям:
\begin{enumerate}
\item \label{it:sep-f} Секвенции в $\mathcal{A}_f$ имеют вид $\sigma(x_1, \ldots x_k)\!\downarrow\ \sststile{}{x_1, \ldots x_k} \chi$.
\item \label{it:sep-e} Если секвенция вида $\sststile{}{} \varphi$ выводима в $\mathcal{A}_f \cup \mathcal{A}_e$, то она выводима и в $\mathcal{A}_e$.
\end{enumerate}

Разумеется, мы всегда можем взять пустое множество в качестве $\mathcal{A}_f$, но, чем оно больше, тем лучше.
Зачастую в качестве $\mathcal{A}_f$ можно взять максимальное возможное множество.
Например, это верно для теорий категорий и конечно полных категорий.
Это следует из следующей леммы.
Пусть множество аксиом некоторой теории состоит из двух подмножеств $\mathcal{A}_f$ и $\mathcal{A}_e$.
Мы будем говорить, что подтермы некоторой формулы $\varphi$ определены в $\mathcal{A}_e$, если для любой аксиомы $\sigma(x_1, \ldots x_k)\!\downarrow\ \sststile{}{x_1, \ldots x_k} \chi$ в $\mathcal{A}_f$
и любого подтерма вида $\sigma(t_1, \ldots t_k)$ формулы $\varphi$ секвенция $\sststile{}{} \chi[t_1/x_1, \ldots t_k/x_k]$ выводима из $\mathcal{A}_e$.

\begin{lem}[der-separated-closed]
Пусть $\mathcal{A}_f$ -- подмножество множества аксиом некоторой теории, удовлетворяющее условию~\eqref{it:sep-f}.
Тогда аксиомы этой теории разделены тогда и только тогда, когда выполнено следующее условие.
Для каждой аксиомы $\varphi \sststile{}{V} \psi$ и каждой замкнутой подстановки $\rho$, если секвенция $\sststile{}{} \varphi[\rho] \land \rho\!\downarrow$ выводима из $\mathcal{A}_e$,
и подтермы $\varphi[\rho]$ определены, то подтермы $\psi[\rho]$ тоже определены.
\end{lem}
\begin{proof}
Допустим аксиомы разделены.
Тогда, если секвенция $\sststile{}{} \varphi[\rho] \land \rho\!\downarrow$ выводима из $\mathcal{A}_e$, то секвенция $\sststile{}{} \psi[\rho]$ выводима из $\mathcal{A}_e \cup \mathcal{A}_f$.
Отсюда следует, что подтермы $\psi$ определены в $\mathcal{A}_f \cup \mathcal{A}_e$ относительно $\rho$.
По предположению они определены и в $\mathcal{A}_e$.

Теперь предположим, что условие леммы выполнено.
Сначала мы докажем, что для любой замкнутой формулы $\varphi$ такой, что секвенция $\sststile{}{} \varphi$ выводима в $\mathcal{A}_e$, ее подтермы определены в $\mathcal{A}_e$,
Мы докажем это индукцией по выводу $\sststile{}{} \varphi$ в системе естественного вывода.
Для большинства правил это очевидно.
Для правила \axref{na} это верно по предположению.
Единственный нетривиальный случай -- это \axref{nl}:
\begin{center}
\AxiomC{$\sststile{}{} a = b$}
\AxiomC{$\sststile{}{} \psi[a/x]$}
\RightLabel{\axref{nl}}
\BinaryInfC{$\sststile{}{} \psi[b/x]$}
\DisplayProof
\end{center}
Если $\sigma(t_1, \ldots t_k)$ является подтермом $b$, то необходимое свойство следует из индукционной гипотезы для $\sststile{}{} a = b$.
Иначе $\sigma$ принадлежит $\psi$ и существуют термы $t_1'$, \ldots $t_k'$ и формула $\psi'$ такие, что $t_i = t_i'[b/x]$, $\psi = \psi'[\sigma(t_1', \ldots t_k')/y]$.
По индукционной гипотезе секвенция $\sststile{}{} \chi[t_1'[a/x]/x_1, \ldots t_k'[a/x]/x_k]$ выводима.
Так как секвенция $\sststile{}{} a = b$ выводима, это влечет, что секвенция $\sststile{}{} \chi[t_1/x_1, \ldots t_k/x_k]$ также выводима.

Теперь, если некоторая секвенция $\sststile{}{} \varphi$ выводима в $\mathcal{A}_f \cup \mathcal{A}_e$, то мы докажем индукцией по ее естественному выводу, что она выводится и в $\mathcal{A}_e$.
Единственный нетривиальный случай -- это правило \axref{na} для аксиом из $\mathcal{A}_f$, которое следует из только что доказанного факта.
\end{proof}

\begin{lem}[der-separated-closed]
Пусть $T$ -- теория с разделенными аксиомами.
Если секвенция $\sststile{}{} \psi$ выводима в $T$, то она выводима и из аксиом $\mathcal{A}_e$.
\end{lem}
\begin{proof}
Во-первых, докажем следующий факт.
Если секвенция $\sststile{}{} \psi$ выводима из $\mathcal{A}_e$, то для любой аксиомы $\sigma(x_1, \ldots x_k)\!\downarrow\ \sststile{}{x_1, \ldots x_k} \chi$ из $\mathcal{A}_f$ и любого подтерма $\sigma(t_1, \ldots t_k)$ формулы $\psi$
секвенция $\sststile{}{} \chi[t_1/x_1, \ldots t_k/x_k]$ выводима из $\mathcal{A}_e$.
Мы докажем это индукцией по выводу $\sststile{}{} \psi$ в системе естественного вывода.
Для большинства правил это очевидно.
Для правила \axref{na} это следует из \eqref{it:sep-e}.
Единственный нетривиальный случай -- это \axref{nl}:
\begin{center}
\AxiomC{$\sststile{}{} a = b$}
\AxiomC{$\sststile{}{} \psi[a/x]$}
\RightLabel{\axref{nl}}
\BinaryInfC{$\sststile{}{} \psi[b/x]$}
\DisplayProof
\end{center}
Если $\sigma(t_1, \ldots t_k)$ является подтермом $b$, то необходимое свойство следует из индукционной гипотезы для $\sststile{}{} a = b$.
Иначе $\sigma$ принадлежит $\psi$ и существуют термы $t_1'$, \ldots $t_k'$ и формула $\psi'$ такие, что $t_i = t_i'[b/x]$, $\psi = \psi'[\sigma(t_1', \ldots t_k')/y]$.
По индукционной гипотезе секвенция $\sststile{}{} \chi[t_1'[a/x]/x_1, \ldots t_k'[a/x]/x_k]$ выводима.
Так как секвенция $\sststile{}{} a = b$ выводима, это влечет, что секвенция $\sststile{}{} \chi[t_1/x_1, \ldots t_k/x_k]$ также выводима.

Теперь мы можем доказать утверждение леммы индукцией по выводу $\sststile{}{} \psi$.
Единственный нетривиальный случай -- это правило вывода для аксиом из $\mathcal{A}_f$:
\smallskip
\begin{center}
\AxiomC{$\sststile{}{} t_i\!\downarrow$, $1 \leq i \leq k$}
\AxiomC{$\sststile{}{} \sigma(t_1, \ldots t_k)\!\downarrow$}
\RightLabel{\axlabel{na}}
\BinaryInfC{$\sststile{}{} \chi[t_1/x_1, \ldots t_k/x_k]$}
\DisplayProof
\end{center}
По индукционной гипотезе секвенция $\sststile{}{} \sigma(t_1, \ldots t_k)\!\downarrow$ выводима из $\mathcal{A}_e$.
Только что доказанный факт влечет, что секвенция $\sststile{}{} \chi[t_1/x_1, \ldots t_k/x_k]$ также выводима из $\mathcal{A}_e$.
\end{proof}

Условие в определении разделения аксиом можно усилить.
Для этого нам понадобится ввести новое определение.
Пусть $\varphi_1 \land \ldots \land \varphi_n \sststile{}{V} \psi$ -- секвенция в некоторой теории $T$.
Мы будем говорить, что \emph{подтермы посылки этой секвенции определены} в $T$,
если секвенция $\varphi_1 \land \ldots \land \varphi_i \sststile{}{V} t\!\downarrow$ выводима в $T$ для любого подтерма $t$ формулы $\varphi_{i+1}$.

\begin{prop}[der-separated]
Пусть $T$ -- теория с разделенными аксиомами.
Если секвенция $\varphi \sststile{}{V} \psi$ выводима в $T$ и подтермы ее посылки определены в $T$, то она выводима из $\mathcal{A}_e$.
\end{prop}
\begin{proof}
Пусть $V = \{ x_1, \ldots x_m \}$ и $\varphi = \varphi_1 \land \ldots \land \varphi_n$.
Пусть $T_j = T \cup \{ \sststile{}{} c_i\!\downarrow\ \mid 1 \leq i \leq m \} \cup \{ \sststile{}{} \varphi_i[c_1/x_1, \ldots c_m/x_m]\ \mid 1 \leq i < j \}$.
Мы докажем индукцией по $j$, что аксиомы $T_j$ разделены.
Для $T_0$ это очевидно.
Докажем, что если аксиомы $T_j$ разделены, то это верно и для $T_{j+1}$.
Единственная новая аксиома $T_{j+1}$ -- это $\sststile{}{} \varphi_j[c_1/x_1, \ldots c_m/x_m]$.
Пусть $\sigma(y_1, \ldots y_k) \sststile{}{y_1, \ldots y_k} \chi$ -- аксиома из $\mathcal{A}_f$, и $\sigma(t_1, \ldots t_k)$ -- подтерм $\varphi_j[c_1/x_1, \ldots c_m/x_m]$.
Так как подтермы $\varphi$ определены, то по \dlem{mcf} секвенция $\sststile{}{} \sigma(t_1, \ldots t_k)\!\downarrow$ выводима в $T_j$.
Так как аксиомы $T_j$ разделены, то секвенция $\sststile{}{} \chi[t_1/y_1, \ldots t_k/y_k]$ выводима в $T_j \setminus \mathcal{A}_f$.

Теперь мы можем доказать, что $\varphi \sststile{}{V} \psi$ выводима из $\mathcal{A}_e$.
По \dlem{mcf} для этого достаточно доказать, что секвенция $\sststile{}{} \psi[c_1/x_1, \ldots c_m/x_m]$ выводима в $T_{n+1} \setminus \mathcal{A}_f$.
По \dlem{mcf} она выводима в $T_{n+1}$, и по \dlem{der-separated-closed} она выводима и в $T_{n+1} \setminus \mathcal{A}_f$.
\end{proof}

\subsection{Конфлюэнтные теории}

Зачастую можно выбрать направление для аксиом, постулирующих равенства, так, чтобы получившееся отношение обладало свойством конфлюэнтности.
Для таких теорий можно доказать несколько полезных утверждений.
В этом разделе мы определим понятие конфлюэнтных теорий, обладающих этим свойством, и докажем их свойства.
Для этого нам понадобится определить несколько понятий из теории абстрактных систем редукций \cite{Terese,klop-trs,ohlebusch-advanced}:

\begin{enumerate}
\item \emph{Абстрактная система редукций} -- это множество $A$ вместе с бинарным отношением $\Rightarrow$ на нем.
Мы будем обозначать $\Rightarrow^*$ рефлексивное и транзитивное замыкание отношения $\Rightarrow$.
Если $\Rightarrow_1$ и $\Rightarrow_2$ -- два отношения, то мы будем писать $\Rightarrow_1 \Rightarrow_2$ для обозначения следующего отношения:
$t \Rightarrow_1 \Rightarrow_2 t'$ тогда и только тогда, когда существует терм $s$ такой, что $t \Rightarrow_1 s$ и $s \Rightarrow_2 t'$.
\item Элемент $a$ \emph{редуцируется} к элементу $a'$ если $a \Rightarrow^* a'$.
\emph{Последовательность редукций} -- это конечная или бесконечная последовательность элементов $a_i$ таких, что $a_0 \Rightarrow a_1 \Rightarrow a_2 \Rightarrow \ldots$.
\item Два элемента $a$ и $b$ \emph{соединимы} если существует элемент $c$ такой, что $a \Rightarrow^* c$ и $b \Rightarrow^* c$.
Мы будем также говорить, что $a$ и $b$ соединимы отношением $\Rightarrow$ если оно не ясно из контекста.
Элемент $a$ \emph{конфлюэнтен} если $a \Rightarrow^* b$ и $a \Rightarrow^* c$ влечет, что термы $b$ и $c$ соединимы.
Система \emph{конфлюэнтна} если все ее элементы конфлюэнтны.
Эквивалентно, система конфлюэнтны если любая пара ее элементов соединима.
\item Два элемента $a$ и $b$ называются \emph{$\Rightarrow$-эквивалентными}, если существует последовательность элементов $a_1$, \ldots $a_n$ такая, что $a = a_1$, $b = a_n$,
и для всех $1 \leq i < n$ либо $a_i \Rightarrow a_{i+1}$, либо $a_{i+1} \Rightarrow a_i$.
\item Элемент $a$ называется \emph{нормальной формой} если не существует элемента $a'$ такого, что $a \Rightarrow a'$.
Мы будем писать $a \Rightarrow^\nf b$ когда $a \Rightarrow^* b$ и $b$ является нормальной формой.
Мы будем говорить, что элемент $a$ \emph{имеет нормальную форму} (или, что оно \emph{слабо нормализуем}), если $a \Rightarrow^\nf b$ для некоторого $b$.
Система является \emph{слабо нормализующей} (WN), если все ее элементы имеют нормальную форму.
\item Элемент $a$ \emph{сильно нормалищуем}, если не существует бесконечной последовательности редукций, начинающейся в $a$.
Система является \emph{сильно нормалиющей} (SN), если все ее элементы сильно нормализуемы.
\item Подмножество $A'$ множества $A$ \emph{замкнуто} относительно $\Rightarrow$, если $a' \in A'$ и $a' \Rightarrow a$ влечет, что $a \in A'$.
\end{enumerate}

Лемма Ньюмана говорит, что для того, чтобы проверить, что сильно нормализующая система конфлюэнтна, достаточно проверить более слабое условие, которое называется \emph{локальной конфлюэнтностью}:

\begin{lem}[newman][Лемма Ньюмана]
Пусть $A$ -- сильно нормализующая абстрактная система редукций.
Допустим, что для любых $a,b,c \in A$ таких, что $a \Rightarrow b$ и $a \Rightarrow c$, существует $d \in A$ такой, что $b \Rightarrow^* d$ и $c \Rightarrow^* d$.
Тогда $A$ конфлюэнтна.
\end{lem}
\begin{proof}
Доказательство приведено, например, в \cite[Lemma~2.2.5]{ohlebusch-advanced}.
\end{proof}

\emph{Система переписывания термов} -- это бинарное множество $R$ на множестве термов некоторой теории, удовлетворяющее следующим условиям:
\begin{enumerate}
\item Если $R(t,s)$, то $\FV(s) \subseteq \FV(t)$.
\item Если $R(t,s)$, то $t$ не является переменной.
\end{enumerate}
Система переписываения термов $R$ называется \emph{лево-линейной}, если для всех термов $t$ и $s$ таких, что $R(t,s)$, каждая переменная встречается в $t$ не более одного раза.

Для каждой системы переписывания термов $R$ мы можем определить отношение $\Rightarrow_R$ на множестве термов следующим образом: если $R(t,s)$, то
\[ c[x \repl t[x_1 \repl t_1, \ldots x_k \repl t_k]] \Rightarrow_R c[x \repl s[x_1 \repl t_1, \ldots x_k \repl t_k]] \]
для всех $c$, $x_1$, \ldots $x_k$ и $t_1$, \ldots $t_k$.
Мы будем обозначать $\Term_T$ множество термов теории $T$.
Таким образом, у любой системы переписывания термов есть подлежащая абстрактная система редукций $(\Term_T,\Rightarrow_R)$.

Пусть $V$ -- множество переменных, а $\varphi$ -- формула такая, что $\FV(\varphi) \subseteq V$.
Мы будем говорить, что терм $t$ некоторой теории $T$ \emph{определен} по отношению к паре $(V,\varphi)$, если секвенция $\varphi \sststile{}{V} t\!\downarrow$ выводима в $T$.
Мы будем писать $\Term_{T,V,\varphi}^d$ для обозначения множества термов, определенных по отношению к $(V,\varphi)$.
Мы будем писать $\Term_T^d$ для обозначения множества $\Term_{T,\varnothing,\top}^d$.

\begin{defn}[directed]
Пусть $T$ -- теория с разделенными аксиомами.
\emph{Система редукций} на $T$ -- это абстрактная система редукций $\Rightarrow_T$ на $\Term^d_T$ такая, что следующие условие выполнены:
\begin{enumerate}
\item \label{it:dir-first} Для каждой пары термов $t$ и $s$ таких, что $t \Rightarrow_T s$, секвенция $\sststile{}{} t = s$ выводима.
\item \label{it:dir-second} Для каждой подстановки $\rho$, каждого терма $c$ и каждой аксиомы вида $\psi \sststile{}{V} t = s$ в $\mathcal{A}_e$ таких,
что секвенция $\sststile{}{} \psi[\rho] \land \rho\!\downarrow \land c[t[\rho]/x]\!\downarrow$ выводима,
термы $c[t[\rho]/x]$ и $c[s[\rho]/x]$ эквивалентны в системе $(\Term_T^d,\Rightarrow_T)$.
\end{enumerate}
\end{defn}

\begin{remark}[trs-theory]
Зачастую система редукций на теории $T$ определена как сужение $\Rightarrow_R$ на множество $\Term^d_T$ для некоторой системы переписывания термов $R$.
В этом случае условия \eqref{it:dir-first} и \eqref{it:dir-second} эквивалентны следующим условиям:
\begin{enumerate}
\item \label{it:trs-dir-first} Для каждой подстановки $\rho$ и каждой пары термов $t$ и $s$ таких, что $(t,s) \in R$, если $\sststile{T}{} t[\rho]\!\downarrow \land s[\rho]\!\downarrow$, то $\sststile{T}{} t[\rho] = s[\rho]$.
\item \label{it:trs-dir-second} Для каждой подстановки $\rho$ и каждой аксиомы вида $\psi \sststile{}{V} t = s$ в $\mathcal{A}_e$ таких,
что секвенция $\sststile{}{} \psi[\rho] \land \rho\!\downarrow$ выводима, термы $t[\rho]$ и $s[\rho]$ эквивалентны в системе $(\Term_T^d,\Rightarrow_T)$.
\end{enumerate}
\end{remark}

\begin{example}[dir-ax]
Пусть $\mathcal{A}_f$ -- множество аксиом в некоторой теории $T$, удовлетворяющее условию~\eqref{it:sep-f}.
Пусть $\mathcal{A}_d$ -- множество аксиом в $T$ вида $\varphi \sststile{}{x_1, \ldots x_k} \sigma(x_1, \ldots x_k)\!\downarrow$ такое,
что для любой такой аксиомы в $\mathcal{A}_d$ и любой аксиомы вида $\sigma(x_1, \ldots x_k)\!\downarrow\ \sststile{}{x_1, \ldots x_k} \chi$ верно, что $\varphi = \chi$.

Пусть $R$ -- система переписывания термов на $T$, сохраняющая сорта термов.
Пусть $\mathcal{A}_c$ -- множество аксиом вида $t\!\downarrow\ \sststile{}{\FV(t)} t = s$ для каждой пары $(t,s) \in R$.
Если аксиомы $\mathcal{A}_f \cup (\mathcal{A}_d \cup \mathcal{A}_c)$ разделены, то $R$ задает систему редукций на $\mathcal{A}_f \cup \mathcal{A}_d \cup \mathcal{A}_c$ как описано в \premark{trs-theory}.
\end{example}

\begin{example}[cat-red]
Теорию категорий можно представить в виде, описаном в \pexample{dir-ax}.
Аксиомы $\mathcal{A}_f \cup \mathcal{A}_d$ эквивалентны следующему набору аксиом:
\begin{align*}
& \sststile{}{f} d(f)\!\downarrow \land c(f)\!\downarrow \\
& \sststile{}{x} \fs{id}(x)\!\downarrow \\
c(f) = d(g) & \ssststile{}{f,g} \circ(g,f)\!\downarrow
\end{align*}
Отношение $R$ состоит из следующих пар:
\begin{align*}
d(\fs{id}(x)) & \Rightarrow_R x \\
c(\fs{id}(x)) & \Rightarrow_R x \\
d(\circ(g,f)) & \Rightarrow_R d(f) \\
c(\circ(g,f)) & \Rightarrow_R c(g) \\
\circ(\fs{id}(x),f) & \Rightarrow_R f \\
\circ(f,\fs{id}(x)) & \Rightarrow_R f \\
\circ(\circ(h,g),f) & \Rightarrow_R \circ(h,\circ(g,f))
\end{align*}
\end{example}

Теперь мы докажем техническую лемму, которая говорит, что секвенция $\varphi \sststile{}{V} t = s$ доказуема в теории $T$ тогда и только тогда,
когда термы $t$ и $s$ эквивалентны в отношении, которое порождается правой стороной аксиом и равенствами в $\varphi$.

\begin{lem}[der-eq]
Секвенция $\varphi \sststile{}{V} t = s$ выводима в теории $T$ тогда и только тогда, когда существуют термы $t_1, \ldots t_n$ такие, что $t = t_1$, $s = t_n$ и для всех $1 \leq i < n$ верно, что $t_i = c[a/x]$ и $t_{i+1} = c[b/x]$
для некоторых термов $a$, $b$ и $c$ таких, что переменная $x$ встречается в $c$ ровно один раз, и одно из следующих условий выполнено:
\begin{enumerate}
\item Существует применение правила \axref{na}, в котором посылка выводима и заключение имеет вид либо $\varphi \sststile{}{V} a = b$, либо $\varphi \sststile{}{V} b = a$.
Кроме того, естественный вывод этого заключения является подвыводом вывода секвенции $\varphi \sststile{}{V} t = s$.
\item $\varphi = \varphi_1 \land \ldots \land \varphi_k$, и существует $j$ такой, что $\varphi_j$ равно либо $a = b$, либо $b = a$.
\end{enumerate}
\end{lem}
Кроме того, секвенции $\varphi \sststile{}{V} t_i\!\downarrow$ выводимы для всех $1 \leq i \leq n$.
\begin{proof}
Если такая последовательность термов существует, то легко показать, что секвенция $\varphi \sststile{}{V} t = s$ выводима по правилам естественного вывода.
Обратное утверждение мы докажем индукцией по естественному выводу секвенции $\varphi \sststile{}{V} t = s$.
Правила \axref{nv}, \axref{np} и \axref{nf} очевидны.
Правила \axref{nh} и \axref{na} следует из предположения.
В этом случае мы берем $t_1 = a = t$, $t_2 = b = s$ и $c = x$.
Теперь рассмотрим правило \axref{ns}.
Если $t_1$, \ldots $t_n$ -- последовательность для $\varphi \sststile{}{V} s = t$, то мы можем взять последовательность $t_n$, \ldots $t_1$ для $\varphi \sststile{}{V} t = s$.

Нам осталось рассмотреть правило \axref{nl}:
\begin{center}
\AxiomC{$\varphi \sststile{}{V} p = q$}
\AxiomC{$\varphi \sststile{}{V} t'[p/y] = s'[q/y]$}
\RightLabel{\axref{nl}}
\BinaryInfC{$\varphi \sststile{}{V} t'[q/y] = s'[q/y]$}
\DisplayProof
\end{center}
Мы можем предположить, что переменная $y$ встречается ровно один раз в формуле $t' = s'$, так как общий случай следует из этого частного.
Пусть $t_1$, \ldots $t_n$ -- последовательность термов для $\varphi \sststile{}{V} p = q$, и $s_1$, \ldots $s_m$ -- последовательность для $\varphi \sststile{}{V} t'[p/y] = s'[p/y]$.
Тогда $t'[t_n/y]$, \ldots $t'[t_1/y] = s_1$, \ldots $s_m = s'[t_1/y]$, \ldots $s'[t_n/y]$ -- последовательность для $\varphi \sststile{}{V} t'[q/y] = s'[q/y]$.

Теперь мы докажем, что секвенция $\varphi \sststile{}{V} t_i\!\downarrow$ выводима индукцией по $i$.
Это верно для $i = 1$ по предположению.
Препдоложим, что это верно для некоторого $i$.
Тогда $t_i = c[a/x]$, $t_{i+1} = c[b/x]$ и секвенция $\varphi \sststile{}{V} a = b$ выводима.
По правилу \axref{nl} секвенция $\varphi \sststile{}{V} t_{i+1}\!\downarrow$ также выводима.
\end{proof}

В следующем утверждении мы докажем основное свойство теорий с системами редукцией.

\begin{prop}[conf-main]
Пусть $T$ -- теория с системой редукций.
Секвенция $\sststile{}{} t = s$ выводим тогда и только тогда, когда термы $t$ и $s$ эквивалентны в системе $(\Term_T^d,\Rightarrow_T)$.
\end{prop}
\begin{proof}
Если $t$ и $s$ эквивалентны в $(\Term_T^d,\Rightarrow_T)$, то существует зигзаг $\Rightarrow_T$-редукций между ними.
Так как отношение $\sststile{T}{} - = -$ является отношением эквивалентности на множестве $\Term_T^d$, то мы можем предположить, что $t \Rightarrow_T s$.
Тогда условие~\eqref{it:dir-first} \odefn{directed} влечет, что $\sststile{T}{} t = s$.

Если $t$ и $s$ такие термы, что $\sststile{T}{} t = s$, то эта секвенция выводима из аксиом $\mathcal{A}_e$.
Тогда \rlem{der-eq} влечет, что существует последовательность $t_1$, \ldots $t_n$ элементов $\Term^d_T$ такая, что $t = t_1$, $s = t_n$ и для всех $1 \leq i < n$
существуют аксиома $\psi \sststile{}{V} a = b$ в $\mathcal{A}_e$, подстановка $\rho$ и терм $c$ такие,
что секвенция $\sststile{}{} \psi[\rho] \land \rho\!\downarrow$ выводима, $t_i = c[a[\rho]/y]$ и $t_{i+1} = c[b[\rho]/y]$ (или наоборот).
Условие~\eqref{it:dir-second} \odefn{directed} влечет, что $t_i$ и $t_{i+1}$ эквивалентны в системе $(\Term_T^d,\Rightarrow_T)$.
\end{proof}

\begin{cor}[conf-main]
Пусть $T$ -- теория с системой редукций.
Тогда система $(\Term_T^d,\Rightarrow_T)$ конфлюэнтна тогда и только тогда, когда любая пара термов $t$ и $s$ таких, что $\sststile{T}{} t = s$, соединима в этой системе.
\end{cor}

\begin{example}
Теория категорий конфлюэнтна.
Легко видеть, что она SN.
По \dlem{newman} достаточно проверить локальную конфлюэнтность, что легко сделать, перебрав варианты.
\end{example}

\bibliographystyle{amsplain}
\bibliography{ref}

\end{document}