????與集合相關的其他的一些概念的定義如下：

????通俗但略微不準確的解釋如下：一個集合的冪集，就是這個集合的所有子集組成的集合。若 S 是集合的集合（S 中的元素都是集合），則 S 的 big并集（通常直接稱之為并集）為 S 的所有元素經(jīng)過（二元）并集的運算得到的集合，S 的 big交集（通常直接稱之為交集）為 S 的所有元素經(jīng)過（二元）交集的運算得到的集合。對于（類型可能不同的）集合 S 和 T，S * T（即 S 和 T 的笛卡爾積）為所有【第一項在 S 中，第二項在 T 中】的有序對組成的集合。任何一個有限序列都可產(chǎn)生一個集合，該集合由所有出現(xiàn)在這個序列中的元素組成。例如，有限序列 [::1;2;3]（可理解為順序為 1,2,3 的有限序列）產(chǎn)生的集合為 { 1, 2, 3 }，這就是我們常說的集合的“列舉法”。

????上文中提到的有序對和有限序列均以歸納類型的形式定義于標準庫中。prod 的類型為 Type -> Type -> Type，對于類型 A 和 B，prod A B（記為 A * B）是一個新的類型。對于 A 類型中的元素 x 和 B 類型中的元素 y，pair x y（記為 (x,y)）具有類型 A * B。對于 A * B 中的元素 p，p.1 表示 p 的第一項，p.2 表示 p 的第二項。相關定理如下：

????seq 的類型為 Type -> Type，對于類型 A，seq A 表示的是 A 類型上的有限序列具有的類型。對于 seq A 類型中的任何一個對象 s，s 或者是空序列 nil（記為 [::]），或者是某一序列 s' 加入前項 x 后的結果 x :: s'。例如，1::[::] : seq nat，2::3::4::[::] : seq nat。a::b::c::...::d::[::] 記為 [::a;b;c;...;d]。

????SetL 的定義使用了 Fixpoint，這是一種在歸納類型上進行遞歸定義的方法。按照其規(guī)則，SetL [::] =??，SetL [::1] = {1} ∪??，SetL [::2;1] = {2} ∪ ({1}?∪??)。SetL [::a;b;c;...;d] 記為 {:a,b,c,...,d:}。（注：由于 Coq 的符號系統(tǒng)的一些限制，這里不能記為 {a,b,c,...,d}，但我們平常交流寫作時可不受此限制）

????（注：可能有讀者會對 ? 和 [::] 等記號產(chǎn)生疑問：我們定義的“空集”對象，實際上具有類型 forall T : Type, 集合 T，也就是說不同類型的空集實際上是不同的，而這里卻都用 ? 符號表示，為什么？實際上，這是 Coq 的隱式參數(shù)功能的體現(xiàn)。很多時候如果將所有參數(shù)都寫出來會非常麻煩，例如?pair A B x y。Coq 的隱式參數(shù)功能可讓用戶省略一部分參數(shù)，讓 Coq?根據(jù)對象所處的語法結構中的已知信息推斷出對象的類型，例如在命題 1::[::]?中，[::]?的類型顯然應為 seq nat。當信息不足的時候 Coq 會報錯，此時就需要用 @ 或 (...:=...) 指定隱式參數(shù)，下一段代碼中就有相應的例子。）

????相關定理如下：

????借助“存在實例化”，我們現(xiàn)在可以證明“選擇公理”：

????我們可以用集合來描述“函數(shù)”（這里指的是具有 A -> B 類型的對象）的一些性質：

????map f S 表示 S 中的所有元素應用于 f 時的函數(shù)值組成的集合，range f 表示所有【可表示為 f x】的元素組成的集合，imap f S 表示所有滿足 f x ∈ S 的 x 組成的集合。與之相關的部分定理如下：

????與 map 類似，我們可以定義多元集合建構式：

????我們經(jīng)常做到“取值范圍”類題目，事實上所謂的取值范圍本質上就是多元集合建構式。例如，題“已知自然數(shù) x 和 y 滿足 x + y = 5，求 x * y 的取值范圍”實際上是“化簡集合?{ x * y | x,y | x + y = 5 }”，注意“已知”一詞后的內容并不是真正的已知條件。

????最后，我們定義“與集合同構的類型”和“uset”，為以后的等價類構造做準備。

????對于集合 S，“與集合同構的類型 S”表示一個新的類型，該類型中的對象與集合 S 中的元素一一對應。uset 類型中的每一個對象都可對應于一個類型上的集合，反之“任意”類型上的任意一個集合都可對應于 uset 類型中的一個對象。

????（注：在介紹 Coq 時作者提到過 Type 是一個項，但這并不是確切的說法。實際上顯示形式為 Type 的是一類項，這一類項雖然都顯示為 Type，但它們的“層級”并不相同。設置不同的層級可防止一些悖論的發(fā)生（類似羅素悖論）。上文中的“任意”一詞加了引號，實際情況是只有低層級的類型上的集合可以對應，而“Uset (@空集 uset)”就是語法錯誤。代碼中設置了兩種“與集合同構的類型”，也是出于層級方面的考慮（Set?的層級低）。（作者對層級相關的內容非常不了解，如有誤導，敬請諒解））