Skip to content

Commit

Permalink
Coherence
Browse files Browse the repository at this point in the history
  • Loading branch information
@Trebor-Huang
Trebor-Huang committed Feb 24, 2025
1 parent 7cd4924 commit e7846f0
Show file tree
Hide file tree
Showing 2 changed files with 189 additions and 39 deletions.
226 changes: 187 additions & 39 deletions chapters/category.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,12 @@ \chapter{范畴语义}
得到\textbf{本质代数结构}或者\textbf{广义代数结构}. 而类型论
的模型一般都可以写成这种形式, 进而可以运用代数结构的一般结论.

\section{对象与依值对象}
历史上提出了很多描述类型论语义的方案. 为了使叙述更加清晰,
我们先介绍 Awodey 提出的自然模型~\cite{awodey:2018:natural},
再简单补充一些历史源流.
\cite{newstead:2018:natmod-poly} 也有较为详细的讲解.

\section{范畴与模型}

我们先来思考最类型论最直观的模型, 将类型解释为集合.
函数类型对应函数集合, 乘积类型对应乘积集合, 等等.
Expand All @@ -34,6 +39,74 @@ \section{对象与依值对象}
类型应该解释为某物, 而后对于依值类型我们提出对应的“依值某物”,
最后完整的解释是将语境对应为某物, 而类型对应于依值某物.

\berry{2}
一般来说, 这里提到的“某物”往往构成一个范畴, 并且许多语义上的
操作都对应范畴论中早有研究的概念, 因此便有了范畴语义的研究.
直觉上, 类型之间的箭头应该是函数. 但参考前文所说, 我们应当
考虑语境之间对应的箭头. 不难看出, 既然语境是一列类型
\(\Gamma = (x_1{:}A_1, \dots, x_n{:}A_n)\),
那么若 \(\Delta = (y_1{:}B_1, \dots, y_m{:}B_n)\),
则合适的箭头 \(\Gamma \to \Delta\) 应当是一列表达式
\((M_1, \dots, M_m)\), 使得 \(\Gamma \vdash M_k : B_k\).
对于 $m = n = 1$ 的情况, 这就与函数是一致的.
不过, 因为有依值类型, \(B_k\) 中可能用到了变量 \(y_1, \dots, y_{k-1}\).
这时候要将它们对应地替换成 \(M_1, \dots, M_{k-1}\).
我们将这列表达式 \(M_k\) 记作 \(\sigma\),
整体写作 \(\Gamma \vdash \sigma : \Delta\).
这些在 \ref{beginning:stlc:canonicity} 中已有提及,
\(\sigma\) 称作从 \(\Gamma\) 到 \(\Delta\) 的\textbf{代换}.

给定任何语境 \(\Gamma\), 我们应该有一个集合 \(\mathrm{Tp}(\Gamma)\),
表示这语境下合法的类型构成的集合. 如果再有一个代换
\(\Delta \vdash \sigma : \Gamma\), 那么就可以得到
函数 \(\mathrm{Tp}(\Gamma) \to \mathrm{Tp}(\Delta)\).
注意这里方向是相反的.
所有这些函数合在一起就构成了函子
\(\mathcal{C}\op \to \mathsf{Set}\), 也就是一个预层.
因此, 对于一般的模型来说, 我们也应当有一个范畴
\(\mathcal{C}\) 与其上的预层 \(\mathrm{Tp}\).

对于类型的元素来说, 有多种等价的提法.
其中最简单的办法是考虑某个语境中所有类型的元素的不交并
\(\mathrm{Tm}(\Gamma)\), 以及映射
\(\pi : \mathrm{Tm}(\Gamma) \to \mathrm{Tp}(\Gamma)\)
为每个元素赋予类型.
这就构成了两个预层之间的映射 \(\pi : \mathrm{Tm} \to \mathrm{Tp}\).
如果读者不喜欢将不同类型的元素放在同一个集合中, 之后会讨论
一些避免这种情况的等价的表述.

给定语境 \(\Gamma\) 与类型 \(A \in \mathrm{Tp}(\Gamma)\),\footnote{
需要时刻注意的是, 我们正在使用语法中的现象来启发语义的定义.
因此这里的“语境”既可以指语法中的一个具体的语境, 也可以指
其模型中的一个对象 \(\Gamma \in \mathcal{C}\).
以集合模型为例, 语法是能具体写出表达式的东西, 而语义中
这些则对应集合与集合之间的函数. 显然并不是所有集合都能写出
具体的表达式, 因此这两者需要区分.
} 我们应当能构造出语境 \(\Gamma, x{:}A\).
因为变量名无关紧要, 我们也写作 \((\Gamma, A)\).
正如范畴论中的大部分构造一样, 我们应当找出语法中它的泛性质,
并将其作为模型的定义中的一条需要满足的性质.

泛性质无非二者居其一: 描述从该对象出发的箭头有哪些,
或者描述指向该对象的箭头有哪些. \((\Gamma, A)\) 的泛性质是后者.
要构造 \(\Delta \to (\Gamma, A)\) 的代换,
就需要先构造 \(\Delta \to \Gamma\) 的代换 \(\sigma\),
再构造一个元素 \(\Delta \vdash t : A[\sigma]\).\berry{3}
换句话说, 这是说我们有一个拉回方
\[\begin{tikzcd}
{\hom(\Delta, (\Gamma, A))} & {\mathrm{Tm}(\Delta)} \\
{\hom(\Delta, \Gamma)} & {\mathrm{Tp}(\Delta)}
\arrow["\pi", from=1-2, to=2-2]
\arrow["{\sigma \mapsto A[\sigma]}"', from=2-1, to=2-2]
\arrow[from=1-1, to=2-1]
\arrow[from=1-1, to=1-2]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
\end{tikzcd}\]
这就完全定义了 \((\Gamma, A)\).
由于对每个 \(\Delta\) 都有这样的拉回方, 我们可以将其
综合为预层上的拉回操作. 这就得到了自然模型的定义.

\begin{comment}
\section{族与丛, 分类空间}

我们先从集合出发, 描述一个一般的现象.
Expand Down Expand Up @@ -158,15 +231,9 @@ \section{族与丛, 分类空间}
\(B \to X\) 之间有拉回的对应关系,
不过多个 \(B \to X\) 可能对应同构的 \(E \to B\),
就称 \(X_* \to X\) \textbf{弱分类}了 \(E \to B\) 的态射.
\end{comment}

\section{类型论的自然模型}\label{category:naturalmodel}

历史上提出了很多描述类型论语义的方案. 为了使叙述更加清晰,
我们先介绍 Awodey 提出的自然模型~\cite{awodey:2018:natural},
再简单补充一些历史源流.
\cite{newstead:2018:natmod-poly} 也有较为详细的讲解.
\berry{3}

\begin{definition}\label{category:naturalmodeldef}
一个\textbf{自然模型}是任意一个有终对象的范畴 \(\mathcal C\),
配备两个预层与其间的态射 \(\pi : \mathrm{Tm} \to \mathrm{Tp}\),
Expand All @@ -187,11 +254,10 @@ \section{类型论的自然模型}\label{category:naturalmodel}
交换图上沿的态射记作 \(\cons{q}_A\).
\end{definition}

我们将语法构造成模型, 便可展示此定义的动机.
考虑所有合法语境在判值相等关系下构成的集合 \(\mathcal C\),
两个语境之间的态射 \(\sigma \in \hom(\Delta, \Gamma)\) 是代换,
即一列类型与 \(\Gamma\) 相符的表达式, 其中包含 \(\Delta\) 的变量.
判值相等的代换视为相同. 这样就构成一个范畴. 终对象是空语境.
% 即一列类型与 \(\Gamma\) 相符的表达式, 其中包含 \(\Delta\) 的变量.
判值相等的代换视为相同, 这样就构成一个范畴. 终对象是空语境.
对于每个语境 \(\Gamma\),
考虑允许包含 \(\Gamma\) 中的变量的合法的类型构成的集合 \(\mathrm{Tp}(\Gamma)\),
同样将判值相等的类型视为相同.
Expand All @@ -212,8 +278,6 @@ \section{类型论的自然模型}\label{category:naturalmodel}
&= \hom(\Delta, (\Gamma, A)).
\end{align*}
因此 \(F\) 的确可表, 并且其表出对象就对应语境的扩展操作 \((\Gamma, A)\).
这里, \(\mathrm{Tm} \to \mathrm{Tp}\) 就(弱)分类了
形如 \((\Gamma,A) \to \Gamma\) 的态射.

以上就证明了类型论的语法范畴构成自然模型, 记作 \(\mathbf T\).%
\footnote{当然, 因为我们还没有引入任何类型, 语法范畴其实是平凡的.
Expand Down Expand Up @@ -450,13 +514,119 @@ \subsection{自然模型中的类型}
类似地, 我们可以给出 \(\Sigma\)-类型结构
\[\cons{Sigma}(A, B) = x \mapsto \coprod_{a \in A(x)} B(x, a).\]

\section{相等类型}
% \subsection{相等类型}

% \subsection{外延类型论与局部积闭范畴}

% \subsection{内涵相等类型}

\section{融贯问题}

\subsection{外延类型论与局部积闭范畴}
尽管从类型论的角度, 自然模型的定义的确很自然,
但是我们寻找模型时, 往往找到的东西会相差一个细节.
这个细节就是\textbf{融贯问题}.
在数学中, 往往难以直接定义“依值某物”. 例如
假设 \(b \in B\) 是拓扑空间中的一个点,
我们难以定义一族拓扑空间 \(A(b)\) 如何随着 \(b\)
的变化而连续变化.

\subsection{内涵相等类型}
这类问题在类型论出现之前就早已被数学家注意到.
一般而言, 数学家对此的解决方案是转而考虑如何定义
\(E = \sum_{b \in B} A(b)\).
这自然地具备投影函数 \(E \to B\).
对 \(A(b)\) 的研究都可以转而改为对 \(p : E \to B\) 的性质的研究.
假如我希望描述一族集合, 最直接的方法就是给定一个指标集 \(B\),
然后对每个 \(b \in B\), 指定一个集合 \(E_b\).
换句话说就是有 \(E_\bullet : B \to \mathsf{Set}\).
但是另一方面, 我也可以将所有的 \(E_b\) 聚合起来
成为一个大集合 \(E\), 再用一个函数 \(p : E \to B\) 指出
每个元素所属的指标 \(b\) 是哪一个. 这两种描述方式是等价的.

\subsection{范畴语义的历史}
\begin{center}
\begin{tikzpicture}
\draw (2,0) ellipse (0.9 and 0.6);
\node at (3.3,0) {\(B\)};
\node (C) at (2.4,-0.1) {\(\bullet\)};
\node (D) at (1.7,-0.3) {\(\bullet\)};
\node (E) at (1.9,0.25) {\(\bullet\)};

\draw (0.9,1.1) rectangle (1.6,2.9);
\node (Do) at (1.25, 2.3) {\(E_a\)};
\draw (1.6,1.1) rectangle (2.3,2.9);
\node (Eo) at (1.95, 1.7) {\(E_b\)};
\draw (2.3,1.1) rectangle (3,2.9);
\node (Co) at (2.65, 2) {\(E_c\)};
\draw (1.25,1.1) edge[->, out=-90] (D);
\draw (1.95,1.1) edge[->, out=-90, in=85] (E);
\draw (2.65,1.1) edge[->, out=-90, in=70] (C);
\end{tikzpicture}
\end{center}

再如, 向量丛理应是依赖于流形上一点 \(x \in M\) 的向量空间 \(V(x)\),
但我们改将其定义为流形之间的连续映射 \(p : E \to M\).
这种技术在代数几何中达到巅峰, 以 Grothendieck 的相对视角
(relative point of view) 为典型.
例如希望表达每个 \(A(x)\) 都是紧空间, 则说 \(p\) 是紧合映射;
希望表达每个 \(A(x)\) 都是仿射空间, 则说 \(p\) 是仿射映射.%
\footnote{一般来说, 在代数几何中也可以直接考虑前者, 即
要求 \(p^{-1}\{x\}\) 是仿射空间, 等等. 但是这样往往无法得到正确
的定义, 因为这样仅仅要求每个点处 \(A(x)\) 都满足条件,
并没有要求不同点之间要求的融洽性.}

然而, 想要将这类定义变为类型论中的模型时, 就会遇到严重的问题.
在原本的写法 \(A(x)\) 中, 若有函数 \(f : Y \to X\),
那么可以直接代入 \(A(f(y))\), 就得到依赖 \(y \in Y\) 的依值对象.
这样, 先代入 \(f : Y \to X\), 再代入 \(g : Z \to Y\),
与直接一次性代入 \(f \circ g\) 显然按定义是相同的,
都等于 \(A(f(g(z)))\).
然而, 如果使用 \(p : E \to X\) 的写法, 那么代入操作在
转换之后就得到拉回 \(p' : E \times_X Y \to Y\).
然而, 两次拉回与一次性拉回基本不会直接相等, 它们仅仅是同构.
这一现象在数学中很常见. 例如集合之间
\(A \times (B \times C) \ne (A \times B) \times C\),
因为前者的元素形如 \((a, (b, c))\), 而后者形如
\(((a, b), c)\), 显然不相等.
一个简单的想法是我们想办法商去一个等价关系, 使得它们相等.
这也是不可取的. 例如 \(A \times B\) 与 \(B \times A\) 是同构的,
但是如果我们将它们视作相同, 即令 \((a, b) = (b, a)\),
那么当 \(A = B = \mathbb{R}\) 时,
就有 \((1, 2) = (2, 1) \in \mathbb{R}^2\), 故 \(1 = 2\), 矛盾.

对此, 又能提出补救的办法.
第一个想法是试图证明在类型论中具体需要的相等关系里,
不会涉及上面提到的交换律这样有问题的情况.
再者, 可以给范畴添加一些与已有的对象同构的新对象,
这样不会改变范畴本身, 但是使得上面的商操作得以进行.
这些技巧统称为\textbf{融贯定理}.

由于这类问题在技术上比较复杂, 但是在直观上又应当总是成立,
在一般的研究中, 往往不愿在此事上花费过多笔墨.
因此往往有许多不同的办法定义类型论的模型,
有一些与数学中遇到的对象比较接近, 因此便于构造具体的模型,
但是不满足上面提到的严格等式;
另一些与类型论中的语法比较接近, 因此便于证明与类型论的关系,
但是自然的数学对象往往不构成这种模型.
这种情况可以画出图表, 从横线的上方到下方需要解决一个融贯问题：

\begin{center}
\begin{tikzpicture}
\node at (-3, 2) {局部积闭范畴};
\node at (-1.2, 2.6) {意象};
\node at (0.4, 0.8) {概括范畴};
\node at (3, 1.6) {形式丛范畴};
\draw (-5, 0) -- (5, 0);
\node at (-2.9, -1) {具族范畴};
\node at (-2.9, -1.5) {自然模型};
\node at (-0.3, -1.9) {具集范畴};
\node at (2.7, -0.7) {分裂概括范畴};
\end{tikzpicture}
\end{center}

% LCCC/topos, compcat, display map cat

% CwF (NatMod), CwA, split compcat

\section{范畴语义的历史}

% 在 1984 年, Seely~\cite{seely:1984:lccc} 提出了依值类型与范畴论的一种对应关系.

Expand All @@ -481,28 +651,6 @@ \subsection{范畴语义的历史}
提出了通用的框架, 给出了一大类类型论的语法与语义的关系.
\end{itemize}

\subsection{融贯问题}

从横线的上方到下方需要解决一个融贯问题：

\begin{center}
\begin{tikzpicture}
\node at (-3, 2) {局部积闭范畴};
\node at (-1.2, 2.6) {意象};
\node at (0.4, 0.8) {概括范畴};
\node at (3, 1.6) {形式丛范畴};
\draw (-5, 0) -- (5, 0);
\node at (-2.9, -1) {具族范畴};
\node at (-2.9, -1.5) {自然模型};
\node at (-0.3, -1.9) {具集范畴};
\node at (2.7, -0.7) {分裂概括范畴};
\end{tikzpicture}
\end{center}

% LCCC/topos, compcat, display map cat

% CwF (NatMod), CwA, split compcat

\section{意象与内语言}\label{category:inner}

(less material)
Expand Down
2 changes: 2 additions & 0 deletions history.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -204,6 +204,8 @@
\cleardoublepage
%%% Body matter
\pagenumbering{arabic}
% \ziju{0.1}
% \baselineskip=20pt
\include{chapters/introduction.tex}
\include{chapters/beginnings.tex}
\include{chapters/curry-howard.tex}
Expand Down

0 comments on commit e7846f0

Please sign in to comment.