n-类型

$\mathbf{n}$-类型是同伦类型论中的概念, 代表类型没有比 $n$ 阶更高的结构. 它可以视为如下概念的推广:

•	命题若存在实例, 则所有实例都相等, 它是 $-1$-类型.

•	集合的实例上的相等证明都相等, 它是 $0$-类型.

•	群胚在类型论中的类比是满足 “实例上的相等证明都是集合” 的类型, 比如圆周 (同伦类型论), 它是 $1$-类型.

1定义

定义 1.1. 对整数 $n\ge -2$, 如类型 $A$ 满足下面归纳定义的性质, 则称 $A$ 为 $\mathbf{n}$-类型:

•	若 $n=-2$, 则 $A$ 同构于单位类型.

•	若 $n=-1$, 则 $A$ 是命题, 即存在证明 $\mathrm{isProp}A$.

•	其它情况下, 对于 $a,b:A$, 类型 ${\mathrm{Id}}_A(a,b)$ 是 $(n-1)$-类型.

这时也称 $A$ 的同伦层级为 $n$.

形式化定义如下:

定义 1.2. 称 $A$ 为 $\mathbf{n}$-类型, 若其满足如下性质 (该语法使用了模式匹配): $$\begin{array}{rl}\mathrm{isHLvl}(A,-2)& =\sum _{x:A}\prod _{y:A}\mathrm{Id}(x,y)\\ \mathrm{isHLvl}(A,-1)& =\prod _{x:A}\prod _{y:A}\mathrm{Id}(x,y)\\ \mathrm{isHLvl}(A,s(n))& =\prod _{x:A}\prod _{y:A}\mathrm{isHLvl}({\mathrm{Id}}_A(x,y),n)\end{array}$$其中:

•	${\prod }_{x:A}{\prod }_{y:A}\mathrm{Id}(x,y)$ 一般简写为 $\mathrm{isProp}A$,
•	${\sum }_{x:A}{\prod }_{y:A}\mathrm{Id}(x,y)$ 一般简写为 $\mathrm{isContr}A$, 对应可缩空间.

例 1.3. 集合正是以上定义的 $0$-类型.

2性质

命题 2.1. “$A$ 是 $n$-类型” 这一性质是命题.