>为什么universal quantification表示为依赖函数类型。 ∀(x：A).B(x)表示“对于类型A的所有x，存在类型B(x)的值”。因此，它被表示为一个函数，当给定任何类型A的值x返回类型B(x)的值。
>为什么existential quantification表示为依赖对类型。 ∃(x：A).B(x)表示“存在类型A的x，其中存在类型B(x)的值”。因此，它被表示为一对，其第一元素是类型A的特定值x，并且其第二元素是类型B(x)的值。
Aside：有趣的是，通用量化始终用于material implication，而存在量化始终用于logical conjunction。
无论如何，维基百科的文章dependent types指出：
The opposite of the dependent type is the dependent pair type,dependent sum type or sigma-type. It is analogous to the coproduct or disjoint union.
一个对类型(通常是一个产品类型)是如何类似于一个不相交的联合(它是一个和类型)？这一直困惑我。
此外，依赖函数类型如何与产品类型类似？
Σ(x：A)B(x)的值是一对(a，b)，其中a∈A和b∈B(a)。第二个元素的类型取决于第一个元素的值。
如果我们看一下Σ(x：A)B(x)的结构，对于所有可能的x∈A，它是B(x)的一个不相交的联合(联产)。
如果B(x)是常数(与x无关)，则Σ(x：A)B将只是| A | B的副本，即A⨯B(2种类型的产品)。
如果我们看看Π(x：A)B(x)的结构，它是所有可能的x∈A的B(x)的乘积。其值可以被视为| A | -tuple，其中第a个分量是类型B(a)。
如果B(x)是常数(独立于x)，那么Π(x：A)B将只是A→B – 从A到B的函数，即使用集理论符号Bᴬ的| A |的副本。
因此，Σ(x∈A)B(x)是由A的元素索引的| A | – 联合序列，而Π(x∈A)B(x)一个。
