圆周 (同伦类型论)

在同伦类型论中, 圆周是一个高阶归纳类型, 对应作为拓扑空间的圆周 $S^1$.

1类型规则

圆周类型记作 $S^1$.

构造规则

$$\frac{\Gamma ⊢}{\Gamma ⊢\mathrm{base}:S^1}\frac{\Gamma ⊢}{\Gamma ⊢\mathrm{loop}:{\mathrm{Id}}_{S^1}(\mathrm{base},\mathrm{base})}$$

这条规则可以直观理解为: 圆周中含有一个点 (称为基点), 且从这个点到自身连一条线. 这对应了圆周通常的 CW 复形结构.

消去规则

简单类型的消去规则:

$$\frac{\Gamma ⊢b:X\Gamma ⊢p:{\mathrm{Id}}_X(b,b)}{\Gamma ⊢{\mathrm{rec}}_{S^1}(b,p):S^1\to X}$$

依值类型的消去规则需要用到等量代换的函数, 在 J 公理中有证明:$$\mathrm{subst}:(P:A\to \mathcal{U})\to {\mathrm{Id}}_A(a,b)\to P(a)\to P(b)$$

规则如下:

$$\frac{\Gamma ⊢X:S^1\to \mathcal{U}\Gamma ⊢b:X(\mathrm{base})\Gamma ⊢p:{\mathrm{Id}}_X(b,\mathrm{subst}(X,\mathrm{loop},b))}{\Gamma ⊢{\mathrm{rec}}_{S^1}(b,p):(x:S^1)\to X(x)}$$

计算规则

简单类型的计算规则:

$$\begin{gathered} {\mathrm{rec}}_{S^1}(b,p)(\mathrm{base})=b:X \\ {\mathrm{ap}}_{{\mathrm{rec}}_{S^1}(b,p)}(\mathrm{loop})=p:{\mathrm{Id}}_X(b,b) \end{gathered}$$

第二条规则可以看作是 ${\mathrm{rec}}_{S^1}(b,p)(\mathrm{loop})=p$ 的严谨写法.

消去规则和计算规则可以理解为圆周的 “万有性质”: 给定空间 $X$ 中的点 $b$ 和 $b$ 到自身的道路 $p$, 存在从圆周到 $X$ 的映射, 满足圆周中基点和环路分别映至 $b$ 和 $p$.

依值类型的计算规则:

$$\begin{gathered} {\mathrm{rec}}_{S^1}(b,p)(\mathrm{base})=b:X(\mathrm{base}) \\ {\mathrm{ap}}_{{\mathrm{rec}}_{S^1}(b,p)}(\mathrm{loop})=p:{\mathrm{Id}}_X(b,\mathrm{subst}(X,\mathrm{loop},b)) \end{gathered}$$

2性质

命题 2.1. 圆周类型的环路空间同构于整数. 换言之, 类型 $\mathrm{Id}(\mathrm{base},\mathrm{base})$ 和整数的类型同构.

证明. 参见编码-解码法.

$\square$

圆周类型给出了一个 K 公理的反例:

引理 2.2. 如下命题蕴含假命题, 也就是说该命题错误: $${\mathrm{Id}}_{{\mathrm{Id}}_{S^1}(\mathrm{base},\mathrm{base})}(\mathrm{loop},{\mathrm{refl}}_{\mathrm{base}})$$