Σ 类型

$\mathbf{\Sigma }$ 类型是积类型在依值类型论中的升级, 使得第二个成员的类型可以随第一个成员的值的变化而变化. 也就是说, 如果对 $A$ 中的每个实例 $x$ 都有类型 $B(x)$, 可以构造 $\Sigma$ 类型

$$\sum _{x:A}B(x),$$

它可以理解为这些 $B(x)$ 的并集: 对于任何 $x:A,y:B(x)$, 都有实例 $⟨x,y⟩:{\sum }_{x:A}B(x)$, 因此用求和符号表示. 如果 $B(x)$ 不随 $x$ 而变, 则它就是积类型.

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

在范畴论中, $\Sigma$ 类型对应于纤维化. 例如在拓扑空间范畴中, $\Sigma$ 类型 ${\sum }_{x:A}B(x)$ 就是把以 $x:A$ “参数化” 的一些空间 $B(x)$ 以某种方式粘了起来, 它可以理解为 $A$ 上纤维丛. 在同伦类型论中这种类比会更为具体: 它也会满足与纤维丛类似的 “提升性质”. 如果 $B$ 不随 $x$ 而变化, $\Sigma$ 类型就可以理解为一些相同的空间以最平凡的方式粘接起来, 也就是平凡丛的全空间 $A\times B$, 即积空间.

在谓词逻辑中, $\Sigma$ 类型可以类比 (但不能一视同仁, 见 2.1) 为含有存在量词的命题: 可以想象每个 $B(x)$ 都是命题, 而 $\Sigma$ 类型 ${\sum }_{x:A}B(x)$ 可以理解为 “存在 $A$ 中的元素 $x$ 使得 $B(x)$ 成立”. 事实上如果在类型论的视角下看待命题, 则构造 $\Sigma$ 类型中实例的过程 (也就是证明命题的过程), 就是要找到 $x:A$ 和 $y:B(x)$, 也印证了上述存在量词的直观.

1类型规则

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

在考虑变量名时, 除了 ${\sum }_{x:A}B(x)$ 之外, 也可以写作 $(x:A)\times B(x)$, 这样更能体现 $\Sigma$ 类型和积类型的联系.

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

构造规则

$$\frac{\Gamma ⊢u:A\Gamma ⊢v:B[x\mapsto u]}{\Gamma ⊢⟨u,v⟩:{\sum }_{x:A}B}$$

消去规则

$$\frac{\Gamma ⊢u:{\sum }_{x:A}B}{\Gamma ⊢u.1:A以及\Gamma ⊢u.2:B[x\mapsto u.1]}$$

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

$$\frac{\Gamma ⊢u:A\Gamma ⊢v:B[x\mapsto u]}{\Gamma ⊢⟨u,v⟩.1:A以及\Gamma ⊢⟨u,v⟩.2:B[x\mapsto u]}$$

2性质

$\Sigma$ 类型不能直接当作存在量词.

例 2.1. 考虑函数 $f:X\to Y$. 如下类型总是同构于 $\mathbf{X}$: $$\sum _{y:Y}\sum _{x:X}\mathrm{Id}(fx,y)$$用集合论的语言写的话, 可以看作: $$\left\{y:Y|\sum _{x:X}\mathrm{Id}(fx,y)\right\}$$这个类型看起来应该仅仅是 $f$ 的像, 而像的大小应该小于等于 $X$, 因为不同的输入可以被映射到相同的输出, 所以不应该总是同构于 $X$.

但考虑如下情形: 存在不同的 $a,b:X$ 被 $f$ 映射到 $Y$ 中相同的元素, 即满足 $f(a)=f(b)$, 方便起见记作 $y$. 这种情况下, 它们应该对应像中的同一个元素, 但实际上对于如上定义, $a,b$ 给出了两个不同的元素: $$⟨y,⟨a,{\mathrm{refl}}_y⟩⟩和⟨y,⟨b,{\mathrm{refl}}_y⟩⟩$$这是因为这两个元素中有不同的数据, 分别是 $a$ 和 $b$.

但和逻辑截断类型就可以正确定义存在量词:

定义 2.2 (存在量词). 在类型论和 Curry–Howard 对应的视角下, $\exists x\in X,P(x)$ 对应如下类型: $$\left|\sum _{x:X}P(x)\right|$$

3范畴语义

参见: 依值和

$\Sigma$ 类型的构造过程可以描述如下: 首先有类型 $\Gamma ⊢A$, 然后对于任何类型 $\Gamma ,A⊢B$, 都可以构造出类型 $\Gamma ⊢{\Sigma }_{A}B$, 这个过程可以看作一个映射 ${\Sigma }_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}$. 这个函子的伴随函子就是前面提到的 ${\Sigma }_A$ 函子.

这个左伴随的构造比起对应$\Pi$ 类型的右伴随要简单得多, 只需要用态射的复合就能定义, 即给定 ${\pi }_A:\boxed{\Gamma ,A}\to \Gamma$ 和 ${\pi }_B:\boxed{\Gamma ,A,B}\to \boxed{\Gamma ,A}$, 直接定义 ${\pi }_{{\Sigma }_{A}B}={\pi }_A\circ {\pi }_B$ 就能通过 ${\pi }_A$ 和 ${\pi }_B$ 的性质构造出 ${\Sigma }_{A}B$ 的相关规则的范畴解释.