用户: Trebor/HOTT 规则

记录一些规则.

待办:

•	更系统的变量名称选取

1资料来源

目前有参考价值的资料只有

•	三次研讨会的录屏和对应的幻灯片: ∘ 第一次, 幻灯片 ∘ 第二次, 幻灯片 ∘ 第三次, 幻灯片
•	Mike Shulman 的 GitHub 项目

2基础

基础类型论是带有 $\Sigma ,\Pi ,\mathsf{U}$ 的类型论. 我们用 $\Gamma ,\Delta$ 等指代上下文, 或称类型组, 也就是一组类型的列表, 其中每一个类型都是在它之前的上下文中的. 对应地, $\sigma :\Gamma$ 则是一组表达式. 这称为替代或者表达式组. 空上下文写作 $()$, 空替代写作 $[]$.

我们用 $\Gamma ⊢t:A$ 表示表达式的类型判断. $\Gamma ⊢A$ 表示类型的合法性判断. 在下面的规则中, 统一省略一个上下文前缀 $\Gamma ⊢$. 如果某个判断前面有写出上下文, 则认为是在 $\Gamma$ 的基础上添加.

对于上下文和替代, 有如下的规则:

$$\frac{Ax:A⊢\Delta }{x:A,\Delta }\frac{t:A\sigma :\Delta [x/t]}{[t,\sigma ]:(x:A,\Delta )}$$

如果引入简写, 我们使用 $\Rightarrow$ 表达消除简写的方式. 而 $\equiv$ 表示判断相等.

3相等类型

引入依赖相等类型:$$\frac{\delta :\mathrm{ID}\Delta x:A[{\delta }_1]y:A[{\delta }_2]}{x{=}_{\Delta .A}^{\delta }y}$$其中 $\mathrm{ID}\Delta$ 表示上下文的等式.$$\begin{array}{rl}\mathrm{ID}()& ⟹()\\ \mathrm{ID}(\Delta ,x:A)& ⟹(\delta :\mathrm{ID}\Delta ,x_1:A[{\delta }_1],x_2:A[{\delta }_2],x_{\star }:x_1{=}_{\Delta .A}^{\delta }{x}_2)\end{array}$$其中 ${\delta }_1$ 表示将 $\delta$ 中的 $3k+1$ 项取出来.

依赖相等类型的元素可以通过 ${\mathrm{ap}}_{\Delta .t}^{\delta }$ 构造.¹$$\frac{\delta :\mathrm{ID}\Delta \Delta ⊢t:A}{{\mathrm{ap}}_{\Delta .t}^{\delta }:t[{\delta }_1]{=}_{\Delta .A}^{\delta }t[{\delta }_2]}$$

我们用 $x{=}_{A}y$ 简写 $x{=}_{().A}^{[]}y$, ${\mathsf{refl}}_x$ 简写 ${\mathrm{ap}}_{().x}^{[]}$.

4相等类型的计算规则

相等类型有特殊的计算规则.

$$\begin{array}{rlrlrl}s{=}_{\Delta .{\sum }_{x:A}B}^{\delta }t& & & \equiv & & \sum _{q:\mathrm{fst}s{=}_{\Delta .A}^{\delta }\mathrm{fst}t}\mathrm{snd}s{=}_{(\Delta ,x:A).B}^{\delta ,\mathrm{fst}s,\mathrm{fst}t,q}\mathrm{snd}t\\ f{=}_{\Delta .{\prod }_{x:A}B}^{\delta }g& & & \equiv & & \prod _{u:A}\prod _{v:A}\prod _{q:u{=}_{\Delta .A}^{\delta }v}f(u){=}_{(\Delta ,x:A).B}^{\delta ,u,v,q}g(v)\end{array}$$

对应地, $\mathsf{ap}$ 也可以计算.

$$\begin{array}{rlrlrl}{\mathrm{ap}}_{\Delta .(s,t)}^{\delta }& & & \equiv & & ({\mathrm{ap}}_{\Delta .s}^{\delta },{\mathrm{ap}}_{\Delta .t}^{\delta })\\ {\mathrm{ap}}_{\Delta .\mathrm{fst}s}^{\delta }& & & \equiv & & \mathrm{fst}{\mathrm{ap}}_{\Delta .s}^{\delta }\\ {\mathrm{ap}}_{\Delta .\mathrm{snd}s}^{\delta }& & & \equiv & & \mathrm{snd}{\mathrm{ap}}_{\Delta .s}^{\delta }\\ {\mathrm{ap}}_{\Delta .f(b)}^{\delta }& & & \equiv & & {\mathrm{ap}}_{\Delta .f}^{\delta }(b[{\delta }_1])(b[{\delta }_2])({\mathrm{ap}}_{\Delta .b}^{\delta })\\ {\mathrm{ap}}_{\Delta .\lambda (y:A).t}^{\delta }& & & \equiv & & \lambda u.\lambda v.\lambda q.{\mathrm{ap}}_{(\Delta ,y:A).t}^{\delta ,q}\end{array}$$

其中 $\delta$ 的左右两侧分别是 ${\sigma }_1,{\sigma }_2$.

对于右下角是变量的情况, 我们也有规则:$$\begin{array}{rlrlrl}u{=}_{(\Delta ,y:A).x}^{\delta ,a,b,q}v& & & \equiv & & u{=}_{\Delta .x}^{\delta }v\\ {\mathrm{ap}}_{(\Delta ,y:A).x}^{\delta ,a,b,q}& & & \equiv & & {\mathrm{ap}}_{\Delta .x}^{\delta }\\ {\mathrm{ap}}_{(\Delta ,x:A).x}^{\delta ,a,b,q}& & & \equiv & & q\end{array}$$这样, 我们可以得到一些可容许的等式.

$$\begin{array}{rlrlrlr}x{=}_{(\Delta ,x).A}^{\delta ,a,b,q}y& & & \equiv & & x{=}_{\Delta .A}^{\delta }y& \\ {\mathrm{ap}}_{(\Delta ,x).t}^{\delta ,a,b,q}& & & \equiv & & {\mathrm{ap}}_{\Delta .t}^{\delta }& (x\notin \mathsf{free}(t))\end{array}$$

这些等式大致和替代满足的等式相同. 在之后我们也会一直保持这些等式.

5单值公理

对于 $A{=}_{\Delta .\mathsf{U}}^{\delta }B$, 也就是 $A{=}_{\mathsf{U}}B$ 来说, 我们需要得到单值公理. 因此我们引入等价性:$$A\cong B⟹\sum _{(\approx ):A\to B\to \mathsf{U}}\left(\prod _{a:A}\mathsf{isContr}\left({\sum }_{b:B}a\approx b\right)\right)\times (\text{vice versa}).$$其中 $\mathsf{isContr}(A)$ 代表 $A\times {\prod }_{x,y:A}x{=}_{A}y$. 我们不使用通常的定义 ${\sum }_{a:A}{\prod }_{x:A}a{=}_{A}x$, 因为这两个定义的等价性依赖于道路的拼接; 而我们类型论中暂且没有.

我们规定$$\frac{p:A{=}_{\mathsf{U}}B}{p\downarrow :A\cong B}\frac{e:A\cong B}{e\uparrow :A{=}_{\mathsf{U}}B}$$并且 $e\uparrow \downarrow \equiv e$. 但是反之则不添加 $p\downarrow \uparrow \equiv p$. 在语义层面, 是因为 HOTT 的立方范畴语义不支持这个 $\eta$-定律; 在操作层面, 这条定律因为等式的其他规则而极难判定.² 因此, $({=}_{\mathsf{U}})$ 和 ${\mathrm{ap}}_{\Delta .A}^{\delta }$ (其中 $A:\mathsf{U}$) 不会进一步计算.

将 $A\cong B$ 类型展开, 可以得到九个分量. 它们分别是:

•	$(\approx ):A\to B\to \mathsf{U}$ 为一一对应关系.

•	$\stackrel{\rightharpoonup }{\mathrm{tr}}:A\to B$ 是转化函数.

•	$\stackrel{\rightharpoonup }{\mathrm{lift}}(a):a\approx \stackrel{\rightharpoonup }{\mathrm{tr}}(a)$ 证明转化是沿着一一对应关系的.

•	$\stackrel{\rightharpoonup }{\mathrm{utr}}(a,b_1,b_2):a\approx b_1\to a\approx b_2\to b_1{=}_B{b}_2$ 证明转化结果是唯一的. 在不会混淆的情况下, 我省略前三个参数, 只写后面两个参数.

•	$\stackrel{\rightharpoonup }{\mathrm{ulift}}(a,b_1,b_2):{\prod }_{r_1:a\approx b_1}{\prod }_{r_2:a\approx b_2}{r}_1{=}_{(x:B).a\approx x}^{\stackrel{\rightharpoonup }{\mathrm{utr}}(a,b_1,b_2)(r_1)(r_2)}{r}_2$ 证明这个一一对应是命题.

•	剩余四项与前面对称.

对于 $p$ 为 ${\mathrm{ap}}_{\Delta .A}^{\delta }$ 的情况, 我们引入这九个分量对应的原语:

•	$({=}_{\Delta .A}^{\delta })$ 已经引入了. 注意到第三节当右下角是变量时我特意漏了一条规则, 现在可以自然地补上: $({=}_{(\Delta ,x:\mathsf{U}).x}^{\delta ,a,b,q})$ 在计算上需要等于 $\mathrm{fst}({\mathrm{ap}}_{(\Delta ,x:\mathsf{U}).x}^{\delta ,a,b,q}\downarrow )$. 因此根据 $\mathsf{ap}$ 的计算法则可以导出它等于 $\mathrm{fst}(q\downarrow )$.

•	${\stackrel{\rightharpoonup }{\mathrm{tr}}}_{\Delta .A}^{\delta }$ 对应一般类型论的 coe 或 transp 函数.

•	${\stackrel{\rightharpoonup }{\mathrm{lift}}}_{\Delta .A}^{\delta }(a)$ 在 Cubical Agda 中称作 transport-filler.

•	${\stackrel{\rightharpoonup }{\mathrm{utr}}}_{\Delta .A}^{\delta }(a,b_1,b_2)$ 给出道路的复合.

•	${\stackrel{\rightharpoonup }{\mathrm{ulift}}}_{\Delta .A}^{\delta }(a,b_1,b_2)$ 给出高阶的等式.

•	剩余四项与前面对称.

这九个原语的判断等式必须与 ${\mathrm{ap}}_{\Delta .A}^{\delta }$ 一起. 因此我们需要对 $A$ 为 $\Sigma ,\Pi$-类型的情形写出它们的等式. 很显然, 如果 $A$ 是变量, 并且 $A\notin \Delta$ 时, $\stackrel{\rightharpoonup }{\mathrm{tr}}$ 退化为常函数; $\stackrel{\rightharpoonup }{\mathrm{lift}}$ 退化为 $\mathsf{refl}$. 但是 $\stackrel{\rightharpoonup }{\mathrm{utr}}$ 仍然是道路复合; 而 $\stackrel{\rightharpoonup }{\mathrm{ulift}}$ 基本上证明了 J 定律.

规则如下.

$${\mathrm{ap}}_{\Delta .A}^{\delta }\downarrow \equiv \left(\begin{array}{rl}({=}_{\Delta .A}^{\delta }),& \left(\lambda a_1.\left(\begin{array}{rl}& \left({\stackrel{\rightharpoonup }{\mathrm{tr}}}_{\Delta .A}^{\delta }(a_1),{\stackrel{\rightharpoonup }{\mathrm{lift}}}_{\Delta .A}^{\delta }(a_1)\right),\\ \lambda s.\lambda t.& \left(\begin{array}{r}{\stackrel{\rightharpoonup }{\mathrm{utr}}}_{\Delta .A}^{\delta }(a_1,\mathrm{fst}s,\mathrm{fst}t)(\mathrm{snd}s)(\mathrm{snd}t),\\ {\stackrel{\rightharpoonup }{\mathrm{ulift}}}_{\Delta .A}^{\delta }(a_1,\mathrm{fst}s,\mathrm{fst}t)(\mathrm{snd}s)(\mathrm{snd}t)\end{array}\right)\end{array}\right)\right),\\ & \left(\lambda a_2.\left(\begin{array}{rl}& \left({\stackrel{\leftharpoonup }{\mathrm{tr}}}_{\Delta .A}^{\delta }(a_2),{\stackrel{\leftharpoonup }{\mathrm{lift}}}_{\Delta .A}^{\delta }(a_2)\right),\\ \lambda s.\lambda t.& \left(\begin{array}{r}{\stackrel{\leftharpoonup }{\mathrm{utr}}}_{\Delta .A}^{\delta }(a_2,\mathrm{fst}s,\mathrm{fst}t)(\mathrm{snd}s)(\mathrm{snd}t),\\ {\stackrel{\leftharpoonup }{\mathrm{ulift}}}_{\Delta .A}^{\delta }(a_2,\mathrm{fst}s,\mathrm{fst}t)(\mathrm{snd}s)(\mathrm{snd}t)\end{array}\right)\end{array}\right)\right)\end{array}\right)$$

$$\begin{array}{rlrlrl}{\stackrel{\rightharpoonup }{\mathrm{tr}}}_{\Delta .{\sum }_{x:A}B}^{\delta }(s,t)& & & \equiv & & \left({\stackrel{\rightharpoonup }{\mathrm{tr}}}_{\Delta .A}^{\delta }(s),{\stackrel{\rightharpoonup }{\mathrm{tr}}}_{(\Delta ,x:A).B}^{\delta ,s,{\stackrel{\rightharpoonup }{\mathrm{tr}}}_{\Delta .A}^{\delta }s,{\stackrel{\rightharpoonup }{\mathrm{lift}}}_{\Delta .A}^{\delta }s}(t)\right)\\ {\stackrel{\rightharpoonup }{\mathrm{tr}}}_{\Delta .{\prod }_{x:A}B}^{\delta }(f)& & & \equiv & & \lambda a.{\stackrel{\rightharpoonup }{\mathrm{tr}}}_{(\Delta ,x:A).B}^{\delta ,a,{\stackrel{\leftharpoonup }{\mathrm{tr}}}_{\Delta .A}^{\delta }a,{\stackrel{\leftharpoonup }{\mathrm{lift}}}_{\Delta .A}^{\delta }a}\left[f\left({\stackrel{\leftharpoonup }{\mathrm{tr}}}_{\Delta .A}^{\delta }(a)\right)\right]\\ {\stackrel{\rightharpoonup }{\mathrm{lift}}}_{\Delta .{\sum }_{x:A}B}^{\delta }(s,t)& & & \equiv & & \left({\stackrel{\rightharpoonup }{\mathrm{lift}}}_{\Delta .A}^{\delta }(s),{\stackrel{\rightharpoonup }{\mathrm{lift}}}_{(\Delta ,x:A).B}^{\delta ,s,{\stackrel{\rightharpoonup }{\mathrm{tr}}}_{\Delta .A}^{\delta }s,{\stackrel{\rightharpoonup }{\mathrm{lift}}}_{\Delta .A}^{\delta }s}(t)\right)\\ {\stackrel{\rightharpoonup }{\mathrm{lift}}}_{\Delta .{\prod }_{x:A}B}^{\delta }(f)& & & \equiv & & \lambda u.\lambda v.\lambda q.{\stackrel{\rightharpoonup }{\mathrm{utr}}}_{(\Delta ,x:A).B}^{\delta ,a,{\stackrel{\leftharpoonup }{\mathrm{tr}}}_{\Delta .A}^{\delta }a,{\stackrel{\leftharpoonup }{\mathrm{lift}}}_{\Delta .A}^{\delta }a}\left({\stackrel{\rightharpoonup }{\mathrm{lift}}}_{(\Delta ,x:A).B}^{\delta ,a,{\stackrel{\leftharpoonup }{\mathrm{tr}}}_{\Delta .A}^{\delta }a,{\stackrel{\leftharpoonup }{\mathrm{lift}}}_{\Delta .A}^{\delta }a}\left[f\left({\stackrel{\leftharpoonup }{\mathrm{tr}}}_{\Delta .A}^{\delta }(v)\right)\right],{\mathrm{ap}}_{(x:A).f(x)}^{{\stackrel{\leftharpoonup }{\mathrm{lift}}}_{\Delta .A}^{\delta }(v)}\right)\end{array}$$

(...)

•	${\mathsf{refl}}_{\mathsf{U}}$, ${?}_{\mathsf{U}}$
•	${=}_{f(x)}$, ${=}_{\mathrm{fst}x}$, etc.

6对称

我们尽量使用下标 $1$ 指代左侧; $2$ 指代右侧; $\star$ 指代等式本身.

定义对称 ${\mathrm{sym}}_{\Delta .A}^{\delta }(a)$.

$$\frac{\delta :\mathrm{ID}\mathrm{ID}\Delta a_{\star \star }:a_{\star 1}{=}_{(\gamma ,u,v).u{=}_{\Delta .A}^{{\gamma }_{\star }}v}^{\delta ,a_{1\star },a_{2\star }}{a}_{\star 2}}{{\mathrm{sym}}_{\Delta .A}^{\delta }(a_{\star \star }):a_{1\star }{=}_{(\gamma ,u,v).u{=}_{\Delta .A}^{{\gamma }_{\star }}v}^{{\mathrm{sym}}_{\Delta }(\delta ),a_{\star 1},a_{\star 2}}{a}_{2\star }}$$

表达式组之间的对称操作 ${\mathrm{sym}}_{\Delta }(\delta )$ 是缩写, 这和依赖相等类型与表达式组的相等同理.$$\begin{array}{rl}{\mathrm{sym}}_{()}[]& ⟹[]\\ {\mathrm{sym}}_{(\Delta ,x:A)}\left[\begin{array}{cccc}\delta ,& a_{11},& a_{12},& a_{1\star },\\ & a_{21},& a_{22},& a_{2\star },\\ & a_{\star 1},& a_{\star 2},& a_{\star \star }\end{array}\right]& ⟹\left[\begin{array}{cccc}{\mathrm{sym}}_{\Delta }(\delta ),& a_{11},& a_{21},& a_{\star 1},\\ & a_{12},& a_{22},& a_{\star 2},\\ & a_{1\star },& a_{2\star },& {\mathrm{sym}}_{\Delta .A}^{\delta }(a_{\star \star })\end{array}\right]\end{array}$$

脚注

1.	但是它并非构造器.
2.	尚未确定是否可以判定.