Misc improvements

Trebor-Huang · Aug 7, 2023 · 597f153 · 597f153
1 parent 147ec52
commit 597f153
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/chapters/category.tex b/chapters/category.tex
@@ -6,7 +6,7 @@ \chapter{范畴语义}
 这个外部的语言称作\textbf{元语言}, 而被研究的类型论语言就直接
 称作“语言”. 切忌混淆元语言中的概念与语言内的概念. 另一个
 容易混淆的事情, 在于语义中的许多概念都是为了与语法中的事物
-相对应, 因此二者会起相近的名称与记号, 但是它们也不应当混同.
+相对应, 因此二者会用相近的名称与记号, 但是它们也不应当混同.
 
 类型论模型的一个极重要的特征就是其(广义的)代数性. 何为代数性?
 最狭义来说, 一个代数结构就是某集合上配备一些运算, 并且满足
@@ -226,3 +226,5 @@ \section{意象与内语言}\label{category:inner}
 
 (less material)
 
+list some concrete biequivalences
+
diff --git a/chapters/hott.tex b/chapters/hott.tex
@@ -1,6 +1,6 @@
 \chapter{同伦类型论}
 \section{K原理的独立性}\label{hott:independent}
-我们刚才已经看到相等类型的归纳子, 也就是 J 原理. 它直觉上大致说的是
+我们之前已经看到相等类型的归纳子, 也就是 J 原理. 它直觉上大致说的是
 “每个 \(a = b\) 类型都只有 \(\cons{refl}\) 一个
 构造器”. 但是想要表达这个直觉, 还有一个看起来很自然的写法：
 \[\prod_{a,b : A} \prod_{p,q : a = b} p = q,\]