少一点套路

chapters/hott.tex

@@ -359,7 +359,7 @@ \subsection{立方类型论简介}
 它有两个端点 \(0,1\). 一个变量 \(i : \mathbb I\) 则表示
 区间上的一个点. 如果有多个变量, 则它们表示立方体中的某个坐标.
 在同伦类型论中, 相等类型的直觉是两点之间道路的空间. 在立方类型论
-中, 如果有一条套路 \(p : x =_A y\), 那么就允许我们取出这条
+中, 如果有一条道路 \(p : x =_A y\), 那么就允许我们取出这条
 道路上的某一点 \(p(i) : A\). 因此, \(\lambda i. p(i)\) 就是
 一个函数 \(\mathbb I \to A\), 而道路空间就可以看成是端点固定的
 函数空间.