diff --git a/chapters/category.tex b/chapters/category.tex
index e472478..dc03733 100644
--- a/chapters/category.tex
+++ b/chapters/category.tex
@@ -16,6 +16,24 @@ \chapter{范畴语义}
 得到\textbf{本质代数结构}或者\textbf{广义代数结构}. 而类型论
 的模型一般都可以写成这种形式, 进而可以运用代数结构的一般结论.
 
+\section{对象与依值对象}
+
+我们先来思考最类型论最直观的模型, 将类型解释为集合.
+函数类型对应函数集合, 乘积类型对应乘积集合, 等等.
+如果有依值类型 \(x{:}A \vdash B(x)\), 那么 \(B(x)\)
+应当对应 “依值集合”, 也就是一族集合 \(Y_x\), 其中 \(x\)
+取遍 \(A\) 所对应的集合.
+不过, 在一般情况下, \(\Gamma \vdash B\) 依赖于语境
+\(\Gamma\) 中的多个类型. 因此我们应该将语境解释为集合,
+而类型解释为集合族. 如果 \(\Gamma\) 解释为集合 \(X\),
+\(\Gamma \vdash B\) 解释为集合族 \(Y_{x \in X}\),
+那么新语境 \(\Gamma, y{:}B\) 应该解释为集合族的不交并
+\(\coprod_{x \in X} Y_x\).
+
+这是定义依值类型论的模型时出现的一般现象. 我们先直观地认为
+类型应该解释为某物, 而后对于依值类型我们提出对应的“依值某物”,
+最后完整的解释是将语境对应为某物, 而类型对应于依值某物.
+
 \section{族与丛, 分类空间}
 
 我们先从集合出发, 描述一个一般的现象.
@@ -469,7 +487,7 @@ \subsection{融贯问题}
 
 \begin{center}
 \begin{tikzpicture}
-  \node at (-3, 2) {LCCC};
+  \node at (-3, 2) {局部积闭范畴};
   \node at (-1.2, 2.6) {意象};
   \node at (0.4, 0.8) {概括范畴};
   \node at (3, 1.6) {形式丛范畴};
diff --git a/chapters/curry-howard.tex b/chapters/curry-howard.tex
index 3026a8a..d9cb93c 100644
--- a/chapters/curry-howard.tex
+++ b/chapters/curry-howard.tex
@@ -438,7 +438,10 @@ \subsection{构造主义}
 前一节中已经提示了, 在没有排中律时, 任何数学对象都必须
 构造出来才可以认为存在. \(p \vee q\) 的证明必须明确
 给出哪一边成立, 而 \(\exists x. p(x)\) 必须具体给出
-一个 \(x\). 因此, 我们将这种逻辑以及相关的各类数学哲学
+一个 \(x\).\footnote{不过, 需要注意的是它们不需要\emph{显式}写出
+这样的构造. 正如一般数学中一样, 我们只需要保证理论上可以给出构造即可,
+不需要将构造的每一个细节都写出来才能算作证明.}
+因此, 我们将这种逻辑以及相关的各类数学哲学
 思想称为\textbf{构造主义}. 如果读者对放弃排中律仍然有怀疑,
 可以阅读《接受构造主义的五个阶段》\cite{bauer:2016:fivestage}.
 这篇简短的文章借用了心理学上人们接受悲痛与失去的
diff --git a/chapters/martin-lof.tex b/chapters/martin-lof.tex
index 8a3d48e..f83cba8 100644
--- a/chapters/martin-lof.tex
+++ b/chapters/martin-lof.tex
@@ -276,9 +276,9 @@ \section{应用}
 
 Martin-L\"of类型论及其变体有非常广泛的应用, 这里拾取一些介绍.
 
-\subsection{Coq}
+\subsection{Coq/Rocq}
 
-Coq是一套交互式定理证明软件. 它基于构造归纳演算, 名字也来源于
+Coq (现已更名为Rocq)是一套交互式定理证明软件. 它基于构造归纳演算, 名字也来源于
 构造演算的缩写 CoC 与其提出者 Coquand 的名字. 它的主要特点是
 允许一种接近自然语言的证明方法.
 
@@ -405,4 +405,4 @@ \subsection{其他}
 尽管上文中我们说过外延集合论中一个证明是否正确难以机械判定,
 但是这些软件中允许用户手动插入额外的说明, 用于帮助软件进行判断.
 Sterling 与 Favonia 等人在 Nuprl 的思想基础上开发了一种
-积立方类型论的原型实现~{\color{red}Red}PRL.
+积立方类型论的原型实现~RedPRL.
diff --git a/history.tex b/history.tex
index cc014b3..77e7311 100644
--- a/history.tex
+++ b/history.tex
@@ -205,6 +205,6 @@
 \include{chapters/hott.tex}
 \include{chapters/prospect.tex}
 
-\emergencystretch=3em
+\emergencystretch=1em
 \printbibliography[title=参考文献]
 \end{document}