与集合相关的其他的一些概念的定义如下：
通俗但略微不准确的解释如下：一个集合的幂集，就是这个集合的所有子集组成的集合。若 S 是集合的集合（S 中的元素都是集合），则 S 的 big并集（通常直接称之为并集）为 S 的所有元素经过（二元）并集的运算得到的集合，S 的 big交集（通常直接称之为交集）为 S 的所有元素经过（二元）交集的运算得到的集合。对于（类型可能不同的）集合 S 和 T，S * T（即 S 和 T 的笛卡尔积）为所有【第一项在 S 中，第二项在 T 中】的有序对组成的集合。任何一个有限序列都可产生一个集合，该集合由所有出现在这个序列中的元素组成。例如，有限序列 [::1;2;3]（可理解为顺序为 1,2,3 的有限序列）产生的集合为 { 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，这是一种在归纳类型上进行递归定义的方法。按照其规则，SetL [::] = ∅，SetL [::1] = {1} ∪ ∅，SetL [::2;1] = {2} ∪ ({1} ∪ ∅)。SetL [::a;b;c;...;d] 记为 {:a,b,c,...,d:}。（注：由于 Coq 的符号系统的一些限制，这里不能记为 {a,b,c,...,d}，但我们平常交流写作时可不受此限制）
（注：可能有读者会对 ∅ 和 [::] 等记号产生疑问：我们定义的“空集”对象，实际上具有类型 forall T : Type, 集合 T，也就是说不同类型的空集实际上是不同的，而这里却都用 ∅ 符号表示，为什么？实际上，这是 Coq 的隐式参数功能的体现。很多时候如果将所有参数都写出来会非常麻烦，例如 pair A B x y。Coq 的隐式参数功能可让用户省略一部分参数，让 Coq 根据对象所处的语法结构中的已知信息推断出对象的类型，例如在命题 1::[::] 中，[::] 的类型显然应为 seq nat。当信息不足的时候 Coq 会报错，此时就需要用 @ 或 (...:=...) 指定隐式参数，下一段代码中就有相应的例子。）
相关定理如下：
借助“存在实例化”，我们现在可以证明“选择公理”：
我们可以用集合来描述“函数”（这里指的是具有 A -> B 类型的对象）的一些性质：
map f S 表示 S 中的所有元素应用于 f 时的函数值组成的集合，range f 表示所有【可表示为 f x】的元素组成的集合，imap f S 表示所有满足 f x ∈ S 的 x 组成的集合。与之相关的部分定理如下：
与 map 类似，我们可以定义多元集合建构式：
我们经常做到“取值范围”类题目，事实上所谓的取值范围本质上就是多元集合建构式。例如，题“已知自然数 x 和 y 满足 x + y = 5，求 x * y 的取值范围”实际上是“化简集合 { x * y | x,y | x + y = 5 }”，注意“已知”一词后的内容并不是真正的已知条件。
最后，我们定义“与集合同构的类型”和“uset”，为以后的等价类构造做准备。
对于集合 S，“与集合同构的类型 S”表示一个新的类型，该类型中的对象与集合 S 中的元素一一对应。uset 类型中的每一个对象都可对应于一个类型上的集合，反之“任意”类型上的任意一个集合都可对应于 uset 类型中的一个对象。
（注：在介绍 Coq 时作者提到过 Type 是一个项，但这并不是确切的说法。实际上显示形式为 Type 的是一类项，这一类项虽然都显示为 Type，但它们的“层级”并不相同。设置不同的层级可防止一些悖论的发生（类似罗素悖论）。上文中的“任意”一词加了引号，实际情况是只有低层级的类型上的集合可以对应，而“Uset (@空集 uset)”就是语法错误。代码中设置了两种“与集合同构的类型”，也是出于层级方面的考虑（Set 的层级低）。（作者对层级相关的内容非常不了解，如有误导，敬请谅解））
