Π 类型

在依值类型论中, $\mathbf{\Pi }$ 类型 (或依值函数类型) 是函数类型在依值类型论中的推广, 使得函数输出值的类型 $B(x)$ 可以随输入值 $x$ 的变化而变化.

具体地说, 给定类型 $A$, 并对每个 $x:A$ 给定类型 $B(x)$, $\Pi$ 类型是类型$$\prod _{x:A}B(x).$$构造它的实例的方法是, 对每个 $x:A$ 给出 $f(x):B(x)$, 这就可以理解为 $A$ 上的函数, 只是函数的值可以在不同的类型中. 因此, 有时也直接用 “函数” 指代 $\Pi$ 类型的实例. 如果这些 $B(x)$ 是不随 $x$ 而变的类型 $B$, 则相应的类型就是更简单的函数类型.

在类型论–范畴论–逻辑学类比中, $\Pi$ 类型可以类比于一些熟悉的数学对象.

在范畴论中, $\Pi$ 类型对应于截面范畴. 首先我们将 $\Sigma$ 类型视为底空间上纤维化的全空间. 例如在拓扑空间范畴中, $\Sigma$ 类型 ${\sum }_{x:A}B(x)$ 可以理解为 $A$ 上纤维丛. 此时 $\Pi$ 类型可以理解为它的截面构成的空间: 对每个 $x:A$ 给出纤维 $B(x)$ 中的元素. 如果 $B$ 不随 $x$ 而变化, $\Pi$ 类型就是平凡丛 $A\times B\to A$ 的截面, 也就是映射空间 $\mathrm{Map}(A,B)$.

在谓词逻辑中, $\Pi$ 类型可以类比为含有全称量词的命题: 想象每个 $B(x)$ 都是命题, 则 $\Pi$ 类型 ${\prod }_{x:A}B(x)$ 可以理解为 “对任意 $A$ 中的元素 $x$, $B(x)$ 均成立”. 事实上如果在类型论的视角下看待命题, 则构造 $\Pi$ 类型中实例的过程 (也就是证明命题的过程), 就是要对任意的 $x:A$ 找到实例 $y:B(x)$, 也印证了上述全称量词的直观.

1类型规则

本质上是将函数类型中的返回类型 $B$ 所在的语境从 $\Gamma$ 改到了 $\Gamma ,A$.

$$\frac{\Gamma ⊢A\Gamma ,x:A⊢B}{\Gamma ⊢{\prod }_{x:A}B}$$

在考虑变量名时, 也可以写作 $(x:A)\to B(x)$, 这样更能体现 $\Pi$ 类型和函数类型的联系.

以下规则均使用和函数类型相同的语法和名称.

构造规则

$$\frac{\Gamma ,x:A⊢u:B}{\Gamma ⊢\lambda x.u:{\prod }_{x:A}B}$$

消去规则

$$\frac{\Gamma ⊢u:{\prod }_{x:A}B\Gamma ⊢v:A}{\Gamma ⊢\text{ap}(u,v):B[x\mapsto v]}$$

消去规则满足如下计算规则:

$$\frac{\Gamma ,x:A⊢u:B\Gamma ⊢v:A}{\Gamma ⊢\text{ap}(\lambda x.u,v)=u[x\mapsto v]:B[x\mapsto v]}$$

2范畴语义

参见: 依值积

$\Pi$ 类型的构造过程可以描述如下: 首先有类型 $\Gamma ⊢A$, 然后对于任何类型 $\Gamma ,A⊢B$, 都可以构造出类型 $\Gamma ⊢{\Pi }_{A}B$, 这个过程可以看作一个映射 ${\Pi }_A:\boxed{\Gamma ,A}\to \Gamma$.

将依值类型论视为一个概括范畴 $\mathcal{C}$ 的话, 可以这么看待: 对于任何代表类型的态射 ${\pi }_A:\boxed{\Gamma ,A}\to \Gamma$, 根据纤维范畴的性质, 它能引导出一个反变函子 ${\pi }_A^{\ast }:{\mathcal{C}}_{/\Gamma }\to {\mathcal{C}}_{/\Gamma ,A}$. 这个函子的伴随函子就是前面提到的 ${\Pi }_A$ 函子, 并且这对伴随的余单位对应 $\Pi$ 类型的消去规则.

3相关概念

•	非直谓性 (类型论)