????在 ZFC 中，“集合”本身作為一個(gè)類型，與相關(guān)公理一同被聲明。在這個(gè)框架下，自然數(shù)、函數(shù)等對(duì)象都具有類型“集合”。若要在 Coq 中形式化集合，采用 ZFC 的方式可能會(huì)造成一些不必要的麻煩。因此，我們將采用另一種方式形式化集合。

????在以上代碼中，對(duì)于每一個(gè)類型，該類型的“集合”被定義為一個(gè)歸納類型，每一個(gè)該類型上的集合與這個(gè)類型的一個(gè)謂詞（性質(zhì)）一一對(duì)應(yīng)。對(duì)于類型 T 、其上的集合 S（即 S : 集合 T）、具有類型 T 的對(duì)象 x，x?屬于 S?定義為 x 滿足【S 對(duì)應(yīng)的謂詞】。定義集合建構(gòu)式 { x | P x } 為謂詞 P 對(duì)應(yīng)的集合。（注：這一段的表述可能顯得十分混亂，一部分原因是自然語(yǔ)言中“集合”一詞往往指代 {0}、{1, 2} 等具體集合，而形式化時(shí)“集合”一詞作為一個(gè)對(duì)象表示的是這些具體集合具有的類型）

????這種定義方式使得集合的使用更加靈活（可以構(gòu)建任何類型上的集合），但也使得 { x, { x } } 等概念成為語(yǔ)法錯(cuò)誤（設(shè) x : A，則 { x }?: 集合 A，二者類型不統(tǒng)一，無(wú)法組成集合）。

????利用函數(shù)外延公理，可以證明集合外延定理，進(jìn)而得到更加實(shí)用的 SetExt。

? ? 與集合相關(guān)的部分基本概念的定義如下：

????基本性質(zhì)如下：

????集合與量詞結(jié)合時(shí)的部分性質(zhì)如下：