统一术语

[OlingCat]

依赖类型 -> 依值类型（Dependent Type） 英文为了简短会把 type depends on a value（依值而存的类型）缩减为 dependent type，中文还是两个字，因此可将缺失的宾语「值」补足。

析构 -> 解构（Destruct） 目前术语「析构」常用于 C++ 中的「析构函数」，本质是资源回收函数。 它的涵义和「构造」对应的「解构」完全不同，因此直接译作「解构」即可。 「构造子」对应「解构子」，不再译作「解构器」。

进行性 -> 可进性(Progress) 「进行」通常表示一种正在进行的状态，而书中表示的是一个项可进一步规约， 因此译作「可进性」。