整数 (同伦类型论)

约定. 在本文中,

• $\Pi$ 类型 ${\prod }_{x:A}B$ 会记作 $(x:A)\to B$.

在类型论以至于同伦类型论中, 有非常多不同的方法定义整数的类型, 例如可以从集合的角度出发, 也可以通过整数的代数性质出发.

1借助自然数定义

整数可以看作自然数的简单拓展, 也就是用某种方法给自然数加入负数得到的数学对象. 于是在类型论中, 借助自然数类型, 可以给出几种整数的定义.

作为归纳类型

在简单类型论中, 整数可以定义为归纳类型:

定义 1.1. 整数类型 ${\mathbb{Z}}_w$ 是由如下构造子生成的归纳类型:

•	$0:{\mathbb{Z}}_w$ 代表整数 $0$,
•	$p:\mathbb{N}\to {\mathbb{Z}}_w$, 对于 $a\in \mathbb{N}$, $p(a)$ 代表整数 $a+1$,
•	$n:\mathbb{N}\to {\mathbb{Z}}_w$, 对于 $a\in \mathbb{N}$, $n(a)$ 代表整数 $-a-1$.

但这个类型由定义直接得到的性质很难用——作为归纳类型, 它每次模式匹配都需要考虑三个情况. 例如乘法分配律的证明需要处理特别多的情况 [Nuo 2014].

商掉零的符号

在 1.1 中, 构造子不是直接构造正整数和负整数, 而是构造出加一或者减一过后的整数, 这是为了确保 $0$ 没有符号.

在同伦类型论或者其它支持某种高阶归纳类型的类型论中, 可以允许 $+0$ 和 $-0$ 同时存在, 但用高阶构造子将两者变得等价.

定义 1.2. 整数类型 ${\mathbb{Z}}_{零}$ 是由如下构造子生成的归纳类型:

•	$p:\mathbb{N}\to {\mathbb{Z}}_{零}$, 对于 $a\in \mathbb{N}$, $p(a)$ 代表整数 $a$,
•	$n:\mathbb{N}\to {\mathbb{Z}}_{零}$, 对于 $a\in \mathbb{N}$, $n(a)$ 代表整数 $-a$.
•	$e:\mathrm{Id}(p0,n0)$.

使用减法

在同伦类型论或者其它支持某种高阶归纳类型的类型论中, 整数可以直接定义为自然数相减的结果, 商去 $a-b=s(a)-s(b)$ 这个关系.

定义 1.3. 整数类型 ${\mathbb{Z}}_{减}$ 是由如下构造子生成的高阶归纳类型:

•	$c:\mathbb{N}\to \mathbb{N}\to {\mathbb{Z}}_{减}$, 其中 $c(a,b)$ 对应整数 $a-b$,
•	$p:(a:\mathbb{N})\to (b:\mathbb{N})\to \mathrm{Id}\left(c(a,b),c(sa,sb)\right)$.

2修改自然数定义

实质上, 从自然数到整数, 无非是让取后继的操作 $s:\mathbb{N}\to \mathbb{N}$ 变得可逆, 换言之它成为一个等价 (类型论). 换言之, 用假想的构造子 $s:\mathbb{N}\simeq \mathbb{N}$ 代替原来的 $s$ 就可以了. 此时我们是在修改自然数的定义, 不再需要用到自然数类型.

为了将这个假想的构造子化为现实, 可以采用多种方法.

展开等价的定义

在同伦类型论中, 所谓 $A\simeq B$, 就是说存在一函数 $f:A\to B$, 满足命题 $\mathrm{isEquiv}(f)$. 由于后者有多种定义, 我们任选其中一种 (双可逆等价) 展开, 变成如下数据:

•	$s:\mathbb{Z}\to \mathbb{Z}$,
•	$s_1^{-1}:\mathbb{Z}\to \mathbb{Z}$,
•	$s_2^{-1}:\mathbb{Z}\to \mathbb{Z}$,
•	$p_1:(a:\mathbb{Z})\to \mathrm{Id}(s(s_1^{-1}a),a)$,
•	$p_2:(a:\mathbb{Z})\to \mathrm{Id}(s_2^{-1}(sa),a)$.

定义 2.1. 整数类型 ${\mathbb{Z}}_b$ 是由如下构造子生成的高阶归纳类型:

•	一般构造子: ∘ $0:{\mathbb{Z}}_b$, ∘ $s:{\mathbb{Z}}_b\to {\mathbb{Z}}_b$, ∘ $s_1^{-1}:{\mathbb{Z}}_b\to {\mathbb{Z}}_b$, ∘ $s_2^{-1}:{\mathbb{Z}}_b\to {\mathbb{Z}}_b$.
•	高阶构造子: ∘ $p_1:(a:{\mathbb{Z}}_b)\to \mathrm{Id}(s(s_1^{-1}a),a)$, ∘ $p_2:(a:{\mathbb{Z}}_b)\to \mathrm{Id}(s_2^{-1}(sa),a)$.

使用圆周的环路空间

由于整数类型对应圆周的环路空间, 这启发了如下定义.

定义 2.2. 定义归纳族 $\mathrm{El}:S^1\to \mathcal{U}$, 由如下构造子生成:

•	$0:\mathrm{El}(\mathrm{base})$

整数类型 ${\mathbb{Z}}_U$ 定义为 $\mathrm{El}(\mathrm{base})$.

该定义直接对应编码–解码法中圆周的道路空间的 “码”.

接下来的定义需要用到等量代换的函数, 在 J 公理中给出定义:$$\mathrm{subst}:(P:A\to \mathcal{U})\to {\mathrm{Id}}_A(a,b)\to P(a)\to P(b)$$

定义 2.3 (前驱和后继). 整数的 $+1$ 和 $-1$ 分别定义如下:

$$\begin{array}{rl}& (+1):{\mathbb{Z}}_U\to {\mathbb{Z}}_U\\ & (x+1):=\mathrm{subst}(\mathrm{El},\mathrm{loop},x)\\ & (-1):{\mathbb{Z}}_U\to {\mathbb{Z}}_U\\ & (x-1):=\mathrm{subst}(\mathrm{El},{\mathrm{loop}}^{-1},x)\end{array}$$

接下来证明两者互逆.

引理 2.4. 对于任意 $P:A\to \mathcal{U},p:{\mathrm{Id}}_A(x,y)$, 有$$\begin{array}{rl}& (a:Py)\to \mathrm{Id}(\mathrm{subst}(P,p,\mathrm{subst}(P,p^{-1},a)),a)\\ & (a:Px)\to \mathrm{Id}(\mathrm{subst}(P,p^{-1},\mathrm{subst}(P,p,a)),a)\end{array}$$

定理 2.5 (前驱和后继互逆). 对于 $x:{\mathbb{Z}}_U$, 如下类型存在实例 (换言之它们对应的命题存在证明):

$$\begin{array}{rl}& (x:{\mathbb{Z}}_U)\to \mathrm{Id}(x+1-1,x)\\ & (x:{\mathbb{Z}}_U)\to \mathrm{Id}(x-1+1,x)\end{array}$$

证明. 展开定义得到:

$$\begin{array}{rl}& x+1-1:=\mathrm{subst}(\mathrm{El},\mathrm{loop},\mathrm{subst}(\mathrm{El},{\mathrm{loop}}^{-1},x))\\ & x-1+1:=\mathrm{subst}(\mathrm{El},{\mathrm{loop}}^{-1},\mathrm{subst}(\mathrm{El},\mathrm{loop},x))\end{array}$$

由 2.4 得证.

$\square$

3性质

定理 3.1. $${\mathbb{Z}}_w\simeq {\mathbb{Z}}_b.$$

证明. 参见 [Altenkirch–Scoccola 2020] 的定理 3.2.

$\square$

定理 3.2. ${\mathbb{Z}}_w$ 是集合.

由于该类型不是高阶归纳类型, 容易证明它是集合.

推论 3.3. ${\mathbb{Z}}_b$ 是集合.

${\mathbb{Z}}_U$ 是始代数

定义 3.4. 整数代数是三元组 $(T,t,e)$, 其中:

•	$T$ 是类型,
•	$t:T,e:\mathrm{Id}(T,T)$.

令 $\mathrm{transport}:\mathrm{Id}(A,B)\to A\to B$.

定义 3.5. 整数代数态射 $f:(T,t,e)\to (T^{\prime },t^{\prime },e^{\prime })$ 包含函数 $f:T\to T^{\prime }$, 且满足如下条件:

•	$f$ 保持 $t$, 即 $f(t)=t^{\prime }$,

•	$f$ 保持 $e$, 即 $f\circ \mathrm{transport}(e)=\mathrm{transport}(e^{\prime })\circ f$.

定义 3.6. 始整数代数是整数代数 $(T,t,e)$ 且对于任意其它整数代数 $(T^{\prime },t^{\prime },e^{\prime })$, 它们之间有唯一整数代数态射.

定理 3.7. ${\mathbb{Z}}_U$ 是始整数代数.

证明. 参见 [Altenkirch–Scoccola 2020] 的定理 4.4.

$\square$

4参考文献

•	Li Nuo (2014). “Quotient Types in Type Theory”. (web)
•	Thorsten Altenkirch, Luis Scoccola (2020). “The Integers as a Higher Inductive Type”. (web)