区间 (同伦类型论)

关于其它含义, 请参见 “区间类型”.

在同伦类型论中, 区间是一个高阶归纳类型, 对应作为拓扑空间的标准区间 $I$.

1类型规则

区间类型记作 $I$, 区别于立方类型论中的区间类型 $\mathbb{I}$. $\mathbb{I}$ 之于 $I$, 正如单形的区间 ${\Delta }^1$ 之于 Kan 复形 $\bullet \stackrel{\cong }{\to }\bullet$.

构造规则

注意区分此处的 $0$ 和同名的自然数类型的构造规则.

$$\frac{\Gamma ⊢}{\Gamma ⊢0:I}\frac{\Gamma ⊢}{\Gamma ⊢1:I}\frac{\Gamma ⊢}{\Gamma ⊢\mathrm{seg}:{\mathrm{Id}}_I(0,1)}$$

这条规则可以直观理解为: 区间中含有两个点 (称为基点), 且这两个点相连.

消去规则

简单类型的消去规则:

$$\frac{\Gamma ⊢b_0:X\Gamma ⊢b_1:X\Gamma ⊢p:{\mathrm{Id}}_X(b_0,b_1)}{\Gamma ⊢{\mathrm{rec}}_I(b_0,b_1,p):I\to X}$$

计算规则

简单类型的计算规则:

$$\begin{gathered} {\mathrm{rec}}_I(b_0,b_1,p)(0)=b_0:X \\ {\mathrm{rec}}_I(b_0,b_1,p)(1)=b_1:X \\ {\mathrm{ap}}_{{\mathrm{rec}}_I(b_0,b_1,p)}(\mathrm{seg})=p:{\mathrm{Id}}_I(b_0,b_1) \end{gathered}$$

第二条规则可以看作是 ${\mathrm{rec}}_I(b_0,b_1,p)(\mathrm{seg})=p$ 的严谨写法.

2性质

引理 2.1. 泛等公理蕴涵区间类型和单位类型命题等价, 换言之两类型同构.

这也意味着区间类型在同伦意义上是可缩空间.

3应用

引理 3.1. 区间类型的规则蕴涵函数类型的外延性.

这是除了泛等公理之外在同论类型论中的另一种证明该性质的方法, 证明方法和立方类型论中的相同.