依赖对类型

Σ 值是一份“带标签的货物”：第一分量给出标签 $a$，第二分量必须来自标签指定的货架 $B(a)$。打开包裹之后，两者要一起进入后续推理；如果丢掉标签，货物所属的类型也随之失去依据。普通积的两个字段彼此独立，所以任一投影都有预先固定的类型；依赖对则让第二项的静态意义随着第一项改变。

在命题解释下，$\mathrm{\Sigma }(x:A).B(x)$ 对应“存在 $x:A$ 使 $B(x)$”，一对 $(a,b)$ 同时给出见证与证据。但这是Curry–Howard 对应公理库Curry–Howard 对应Curry–Howard correspondence · Propositions as types把命题对应为类型、证明对应为程序、证明化简对应为程序求值。所揭示的规则关系，不是经典逻辑存在量词的全部语义。构造一个 Σ 居民必须交付可用见证；从被截断的“仅知存在”通常不能恢复该见证，经典选择原则也不是 Σ 规则免费附送的结论。

设 $\mathsf{Vec}(A,n)$ 是长度索引向量，则

把长度和对应向量封装在一起。若 $a_0,a_1:A$，可以构造

由投影计算得到 $\mathsf{fst}(p)\equiv 2$，同时

定义 $\mathsf{packedLength}(p)=\mathsf{fst}(p)$ 时只需固定结果类型 $\mathbb{N}$；定义返回“该包中向量确实具有所报长度”的证据时，motive 必须依赖 $p$，这正是依赖消去与普通 pair destructuring 的差别。

边界例子是试图构造 $(2,\mathsf{nil})$。因为 $\mathsf{nil}:\mathsf{Vec}(A,0)$，除非理论中已有 $0$ 与 $2$ 的适当相等证据并显式运输，否则第二个引入前提失败。反过来，从任意 $p:\mathrm{\Sigma }(n:\mathbb{N}).\mathsf{Vec}(A,n)$ 取出向量后若擦除 $n$，得到的只是某种存在封装，不能再把它无证明地当作长度 $5$ 的向量。Σ 类型也不自动等同于面向对象的动态类型包；后者还涉及表示擦除、运行时标签与开放世界子类型。

依赖对是证明携带数据、带尺寸容器、编译器中“语法项连同其推导”、数据库中带模式见证记录的基础接口。一个类型检查器可以返回 $\mathrm{\Sigma }(A:\mathcal{U}).\mathsf{TermOf}(A)$，使推断出的类型与核心项不可分离；解析器可以返回输入长度及精确消费该长度的结果。只要后续函数对包使用依赖消去，索引信息就继续约束计算，而不会在拆包时退化为注释。

Σ 还把逐点见证组合成总结构：从 $g:\mathrm{\Pi }(x:A).\mathrm{\Sigma }(y:B(x)).R(x,y)$ 可逐点投影出 $f(x)=\mathsf{fst}(g(x))$，并由 $\mathsf{snd}(g(x))$ 得到 $\mathrm{\Pi }(x:A).R(x,f(x))$。这正是未截断 Σ 保留见证时的构造性选择；若前提只有 $\mathrm{\Pi }(x:A).\Vert \mathrm{\Sigma }(y:B(x)).R(x,y)\Vert$，则不能仅凭 Σ 规则消去截断并提取 $f$，更不能把结论扩张成任意经典存在命题的选择公理。