依赖types：依赖对types如何类似于不相交的联合？
我一直在研究依赖types，我理解以下内容：
- 为什么通用量化被表示为依赖函数types。
∀(x:A).B(x)意思是“对于所有typesAx有一个typesB(x)” 。 因此，它被表示为一个函数，当给定的任何值typesA返回typesB(x)。 - 为什么存在量化表示为从属对types。
∃(x:A).B(x)表示“存在typesA的x，其typesB(x)” 。 因此，它被表示为一个对，其第一个元素是一个特定值x的A型A而其第二个元素是一个B(x)型的值。
另外：有趣的是，通用量化总是与物质含义 一起使用，而存在量化总是与逻辑连接一起使用 。
无论如何，维基百科有关依赖types的文章指出：
与依赖types相反的是依赖对types ， 依赖和types或sigmatypes 。 它类似于联产品或不相交的联合。
一个对types（通常是一个产品types）是如何类似于不相交的联合（这是一个和types）？ 这一直困扰着我。
另外，依赖函数types与产品types相似如何？
使用类似的术语来描述一个Σ型的结构，以及它的值是怎样的。
Σ（x：A）B（x）的值是一对 （a，b） ， 其中 a∈A和b∈B（a） 。 第二个元素的types取决于第一个元素的值。
如果我们看Σ（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 | – 第二个元素是B（a）types的元素。
如果B（x）是常数（不依赖于x ），则Π（x：A）B将只是A→B – 从A到B起作用，即Bᴬ （ B到A ）使用集合理论符号 – 产品| A | B的副本。
所以Σ（x∈A）B（x）是| A | （x∈A）B（x）是一个| A | A的元素索引的产品。
一个从属对用一个types和一个从该types的值到另一个types的函数来input。 从属对具有应用于第一值的第一types的值和第二types的值的值。
data Sg (S : Set) (T : S -> Set) : Set where Ex : (s : S) -> T s -> Sg ST
我们可以通过显示如何将其中的Either规范化地表示为一个西格玛types来重新获得总和types：这仅仅是Sg Bool (choice ab)其中
choice : a -> a -> Bool -> a choice lr True = l choice lr False = r
是布尔的规范消除器。
eitherIsSg : {ab : Set} -> Either ab -> Sg Bool (choice ab) eitherIsSg (Left a) = Sg True a eitherIsSg (Right b) = Sg False b sgIsEither : {ab : Set} -> Sg Bool (choice ab) -> Either ab sgIsEither (Sg True a) = Left a sgIsEither (Sg False b) = Right b
在PetrPudlák的回答的基础上，另一个以纯粹非依赖的方式来看待这个问题的angular度是注意到Either aatypes与(Bool, a)types是同构的。 虽然后者乍一看是一种产品，但说它是一种总和types是合理的，因为它是a的两个实例的总和。
我必须用这个例子来代替Either ab ，因为后者被表示为一个产品，我们需要 – 依赖types。
好问题。 这个名字可能来源于马丁·勒夫（Martin-Löf），他使用了pitypes的“一套族的笛卡尔积”一词。 请参阅以下注意事项，例如： http : //www.cs.cmu.edu/afs/cs/Web/People/crary/819-f09/Martin-Lof80.pdf重点在于pitypes原则上类似对于一个指数，你总能看到指数为n元产品，其中n是指数。 更具体地说，非依赖函数A→B可以看作指数型B ^ A或A中的无限乘积Pi_ {a} B = B×B×B×…×B（A次）。 在这个意义上，从属产品是一个潜在的无限乘积Pi（a）中的一个B（a）= B（a_1）xB（a_2）x … xB（a_n）（A中的每个a_i都有一次）。
依赖总和的推理可能是相似的，因为您可以将产品看作n元和，其中n是产品的一个因素。
这在其他答案可能是多余的，但这是问题的核心：
一个对types（通常是一个产品types）是如何类似于不相交的联合（这是一个和types）？ 这一直困扰着我。
但是，什么是一个产品，而是一个相等的数字？ 例如4×3 = 3 + 3 + 3 + 3。
同样的关系适用于types，集合或类似的东西。 实际上，非负整数只是有限集的分类。 对数字的加法和乘法的定义是这样select的，使得不相交的并集的基数是集合的基数之和，并且集合的乘积的基数等于集合的基数的乘积。 事实上，如果用“羊群”代替“集合”，这可能是算术的发明。
首先，看看一个联合产品是什么。
副产品是所有对象B_i的terminal对象A，使得对于所有的箭头B_i→X有一个箭头B_i→A和一个唯一的A→X使得相应的三angular形可以通行。
你可以把它看作是一个Haskell数据typesA，B_i – > A是一组具有B_itypes参数的构造函数。 很显然，对于每一个B_i – > X，都可以从A – > X提供一个箭头，这样通过模式匹配就可以将这个箭头应用到B_i来获得X.
与sigmatypes的重要联系是，B_i中的索引i可以是任何types的索引，而不仅仅是一种自然数。
与上面答案的重要区别在于，对于每一个这种types的值我都不需要有B_i：一旦你定义了B_i∀i，你就有了一个总的函数。
Π和Σ之间的区别，可以从Petr Pudlak的答案中看出，对于Σ中的某些值B_i可能会丢失 – 对于某些我可能没有相应的B_i。
Π和Σ之间的另一个明显区别是Π通过提供从产品Π到每个B_i的第i个投影（这是函数i – > B_i的含义）来表征B_i的乘积，但是Σ以相反方向提供箭头它提供从B_i到Σ的第i次喷射。
