单位类型

单位类型是单点集、单点空间等 “单点” 的空间在类型论中的类比, 就是有一个平凡的实例的类型. 它在简单类型论和依值类型论里都可以定义, 且定义是一样的.

在同伦类型论中, 单位类型是一个 $-2$-类型, 见$n$-类型.

1类型规则

单位类型记作 $1$.

构造规则

单位类型的实例记作 $\star$. 规则可以写作:

$$⊢\star :1$$

严谨地话可以写作:

$$\Gamma ⊢\star :1$$

唯一性规则

$$\frac{\Gamma ⊢u:1}{\Gamma ⊢\star =u:1}$$

这可以看作是最强的消去规则, 这蕴涵任何其它形式的消去规则.

2变种

子类型

顶类型是子类型意义上的单位类型, 但与空类型不同的是, 它的定义和单位类型不太一样: 它并不是有一个平凡实例的类型, 而是任何表达式的类型. 在讨论子类型的类型论中, 顶类型是子类型关系构成的格中的最大元素, 因此才叫顶类型, 一般记作 $\top$.

$\lambda$ 编码

参见: lambda 编码

在 F 系统中可以编码单位类型, 直接将单位类型定义为如下类型即可:

$$1:=\forall A.A\to A且\star :=\lambda a.a$$

但要证明该类型等价于单位类型的话, 需要参数性. 这个证明也是参数性的最简单的应用.

依值类型论中用 $\Pi$ 类型和宇宙代替上述类型:

$$1:={\Pi }_{A:\mathcal{U}}A\to A$$

术语翻译

单位类型 • 英文 unit type

顶类型 • 英文 top type