-类型

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

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

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

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

1定义

定义 1.1. 对整数 , 如类型 满足下面归纳定义的性质, 则称 -类型:

, 则 同构于单位类型.

, 则 命题, 即存在证明 .

其它情况下, 对于 , 类型 -类型.

这时也称 同伦层级.

形式化定义如下:

定义 1.2.-类型, 若其满足如下性质 (该语法使用了模式匹配): 其中:

一般简写为 ,

一般简写为 , 对应可缩空间.

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

2性质

命题 2.1.-类型” 这一性质是命题.