Wiki. “单点 (同伦类型论)” [单点(同伦类型论)]

#同伦类型论

定义

单点是同伦类型论中零个类型的乘积. 只有一种方式构造类型 $\mathbf 1$ 的元素:

• $\star\colon \mathbf 1$.

性质

命题. 对任意 $x,y\colon \mathbf 1$, 有 $(x=y)\simeq\mathbf 1$.

证明. 首先, 有明显的映射 $(x=y)\to 1$ 将一切映射到 $\star$. 另一方面, 对于 $x,y\colon 1$, 由高阶归纳类型, 不妨设 $x\equiv \star$, $y\equiv \star$. 那么我们有 $\mathsf {refl}_{\star}\colon x=y$. 这给出一个映射 $1 \to (x=y)$.

我们证明上述两个映射互逆.

• $\mathbf 1\to (x=y)\to \mathbf 1$, 考虑 $u\colon \mathbf 1$, 不妨设 $u\equiv\star$. 这说明这个复合是恒等.
• $(x=y)\to\mathbf 1\to(x=y)$. 考虑 $p\colon (x=y)$, 由路径归纳, 不妨设 $x\equiv y$ 且 $p\equiv\mathsf {refl}_x$. 那么又不妨设 $x\equiv\star$. 此时复合映射将 $p$ 映射到 $\mathsf {refl}_x$, 也即 $p$ 自身.

推论. $\mathbf 1$ 是集合 (同伦类型论).