Misc improvements

chapters/beginnings.tex

@@ -717,13 +717,13 @@ \subsection{简单类型\texorpdfstring{\(\lambda\)}{Lambda}-演算的闭典范
 本身也是模型之一.
 
 我们现在就可以迅速证明 \(\cons{y}\ne\cons{n}\).
-考虑所有集合的范畴 \(\cons{Set}\), 它是积闭的.
+考虑所有集合的范畴 \(\mathsf{Set}\), 它是积闭的.
 我们再选择 \(1 \rightrightarrows B\) 为
 \(1=\{\varnothing\}\) 到
 \(2=\{\varnothing, \{\varnothing\}\}\) 的两个态射即可.
 如果 \(\cons{y}=\cons{n}\),
 那么说明引理~\ref{beginning:lambda:initial} 产生的函子
-\(\mathrm s:\mathcal T \to \cons{Set}\)
+\(\mathrm s:\mathcal T \to \mathsf{Set}\)
 满足 \(\mathrm{s}(\cons{y}) = \mathrm{s}(\cons{n})\),
 进一步得到集合 \(2\) 的两个元素相等, 矛盾. 注意这个模型
 仍然无法证明闭典范性, 因为 \(\mathrm{s}\) 仍然有可能
@@ -734,7 +734,7 @@ \subsection{简单类型\texorpdfstring{\(\lambda\)}{Lambda}-演算的闭典范
 为了研究闭典范性, 我们需要先找出类型论中的闭元素, 即不包含
 自由变量的表达式. 这很容易, 我们只需要要求语境为空即可.
 因此我们考虑 \(\boldsymbol\Gamma(X) = \hom_{\mathcal T}(1, X)\).
-这是一个 \(\mathcal T \to \cons{Set}\) 的函子.
+这是一个 \(\mathcal T \to \mathsf{Set}\) 的函子.
 
 如上文所述, 我们一般的思路是为每一个类型赋予一个谓词.
 在范畴论中, 我们可以使用一个 \(f : Y \to X\) 的态射作
@@ -757,12 +757,12 @@ \subsection{简单类型\texorpdfstring{\(\lambda\)}{Lambda}-演算的闭典范
 一个代换, \(\sigma'\) 是某个函数. 这样, \(\mathcal G\)
 就是每个类型的闭表达式集上所有可能的谓词的范畴.
 如果读者熟悉范畴论, 就应该知道这是逗号范畴的特例:
-\[\mathcal G = \mathrm{Id}_{\cons{Set}}\downarrow \boldsymbol\Gamma.\]
+\[\mathcal G = \mathrm{Id}_{\mathsf{Set}}\downarrow \boldsymbol\Gamma.\]
 它也可以看成是下面这个拉回：
 \[
 \begin{tikzcd}
-\mathcal G \ar[r, dashed] \ar[d, dashed, "\mathrm{gl}"'] \ar[dr, phantom, "\lrcorner", very near start] & \cons{Set}^{\to} \ar[d, "\mathrm{cod}"] \\
-\mathcal T \ar[r, "\boldsymbol\Gamma"'] & \cons{Set}
+\mathcal G \ar[r, dashed] \ar[d, dashed, "\mathrm{gl}"'] \ar[dr, phantom, "\lrcorner", very near start] & \mathsf{Set}^{\to} \ar[d, "\mathrm{cod}"] \\
+\mathcal T \ar[r, "\boldsymbol\Gamma"'] & \mathsf{Set}
 \end{tikzcd}
 \]
 注意这时候我们自动有了一个函子 \(\mathrm{gl}\), 它把
@@ -793,7 +793,7 @@ \subsection{简单类型\texorpdfstring{\(\lambda\)}{Lambda}-演算的闭典范
 \boldsymbol\Gamma(1) \ar[r, "\boldsymbol\Gamma(\cons{y})"'] & \boldsymbol\Gamma(\cons{Ans}) &\ar[l, "\boldsymbol\Gamma(\cons{n})"] \boldsymbol\Gamma(1)
 \end{tikzcd}
 \]
-注意整个交换图都在 \(\cons{Set}\) 中.
+注意整个交换图都在 \(\mathsf{Set}\) 中.
 
 我们需要证明的是任何一个表达式 \(M \in \boldsymbol\Gamma(\cons{Ans})
 = \hom_{\mathcal T}(1, \cons{Ans})\) 都一定恰好是

chapters/category.tex

@@ -222,7 +222,7 @@ \section{外延类型论与局部积闭范畴}
 
 \subsection{融贯问题}
 
-\section{意象与内语言}
+\section{意象与内语言}\label{category:inner}
 
 (less material)
 

chapters/hott.tex

@@ -450,9 +450,7 @@ \subsection{无穷群胚} \berryinf
 指出当时的理论中非构造性是无法消除的.%
 \footnote{后续研究~\cite{henry:2019:constructive}
 中发现可以修改理论去除非构造性. 这与Bezem等人的工作
-并不矛盾, 但是这一点的解释超出了本文的范畴.} 我们已经知道
-在类型论中, 排中律的各种形式都会或多或少的破坏其性质,
-而我们现在的目的就是改善类型论的这些性质, 因此这是不能妥协的.
+并不矛盾, 但是这一点的解释超出了本文的范畴.}
 进一步的研究发现, 基于立方体的理论的技术困难是可以克服的,
 并且我们能够建构一套完全构造性的理论. 在 2013 年,
 Marc Bezem, Thierry Coquand, Simon Huber 三人提出
@@ -480,7 +478,7 @@ \subsection{无穷群胚} \berryinf
 
 立方类型论不完全是同伦类型论的子学科. Sterling等人
 提出了XTT类型论~\cite{sterling:2019:xtt}, 属于立方类型论,
-但是不支持泛等公理等.
+但是不支持泛等公理, 属于集合 (即满足 K 原理) 层面的理论.
 
 \subsection{立方类型论简介}
 

chapters/introduction.tex

@@ -316,7 +316,7 @@ \section{类型论的语义}\label{intro:semantics}\berry{1}
 \(f\circ (g\circ h) = (f\circ g)\circ h.\)
 \end{definition}
 
-那么集合与函数就构成一个范畴\(\cons{Set}\). 读者可以验证
+那么集合与函数就构成一个范畴\(\mathsf{Set}\). 读者可以验证
 函数的复合满足所需要的等式. 群与群同态也构成一个范畴 \(\cons{Grp}\),
 等等. 进一步, 范畴之间保持其结构的映射就称为函子.
 \begin{definition}