#同伦类型论
定义
在同伦类型论中, 圆 $S^1$ 是如下高阶归纳类型:
- 一个点 $\mathsf{base} \colon S^1$,
- 一条道路 $\mathsf {loop}\colon \mathsf {base}=\mathsf {base}$.
性质
由定义, 对任意类型 $A$ 以及 $x\colon A$, $p\colon x=x$, 有一个映射 $f\colon S^1\to A$ 使得 $f(\mathsf {base})\equiv x$, $f(\mathsf {loop})\equiv p$.
命题. $\mathsf {loop}\neq \mathsf {refl}_{\mathsf {base}}$.
证明. 假设 $\mathsf {loop}=\mathsf {refl}_{\mathsf {base}}$. 那么对任意类型 $A$ 以及 $x\colon A$, $p\colon x=x$, 有一个映射 $f\colon S^1\to A$ 使得 $f(\mathsf {base})\equiv x$, $f(\mathsf {loop})\equiv p$, 从而 $p=f(\mathsf {refl}_{\mathsf {base}})=\mathsf {refl}_x$. 这说明任意类型都是集合 (同伦类型论).