????類型 A 到類型 B 的（二元）關(guān)系，指的是類型為 A -> B -> Prop 的對象。我們通常說函數(shù)是一種特殊的關(guān)系，這種說法在 ZFC 中是正確的，但在這里則是不準(zhǔn)確的，因為二者的語法結(jié)構(gòu)不同（函數(shù)的類型為 A -> option B）。

????對于關(guān)系 r : A -> B -> Prop，我們定義它的圖像是所有滿足 r x y 的 (x,y) 組成的集合。反過來，對于集合 S : 集合 (A * B)，我們定義它對應(yīng)的關(guān)系為 fun x y =>?(x,y) ∈ S。

????如果一個類型為 A -> A -> Prop 的關(guān)系滿足自反性、對稱性、傳遞性，那么這個關(guān)系被稱為等價關(guān)系。

????設(shè)【A : Type】【r : A -> A -> Prop】【r自反 : forall x : A, r x x】【r對稱 : forall x y : A, r x y -> r y x】【r傳遞 : forall x y z : A, r x y -> r y z -> r x z】，那么有【@等價關(guān)系_of A r r自反 r對稱 r傳遞 : 等價關(guān)系 A】。類型為 等價關(guān)系 A 的對象嚴(yán)格地說并不能被稱為關(guān)系（因為關(guān)系應(yīng)具有類型 A -> B -> Prop），它是由一個關(guān)系和這個關(guān)系滿足自反性、對稱性、傳遞性的證明項打包組合而成的項。在剛定義完“等價關(guān)系”后，對于 x : A ，y : A，r : 等價關(guān)系?A，“r x y”是語法錯誤，而“eq_rel r x y”則是符合語法規(guī)則的。在使用了 Coercion 指令后，Coq 在遇到“r x y”的表述時可以自動將其解析為“eq_rel r x y”以匹配類型，從而簡化了表達。等價關(guān)系的基本性質(zhì)如下：

????對于 R : 等價關(guān)系 A 和 a : A，我們定義其對應(yīng)的等價類為所有滿足 R x a 的 x 組成的集合。對于 R : 等價關(guān)系 A，我們定義 R 的等價類集為 R 的所有等價類的集合。具體定義與相關(guān)定理如下：

????對于等價類 S（即已知 S ∈ 等價類集 R），我們可以選出一個代表?x，使得 S 恰好為 x 對應(yīng)的等價類（同時自然也有 x ∈ S）。

????等價類的一個重要應(yīng)用是構(gòu)造新的類型。對于 A : Type 和 R : 等價關(guān)系 A，我們可以構(gòu)造出一個新的類型 T，使得 T 中的元素與 R 的等價類一一對應(yīng)。對于 x : A，Btfr R x 表示 R 和 x 對應(yīng)的等價類對應(yīng)的 T 中的元素。對于 T 中的每一個元素，我們都能找到一個 x : A，使得 Btfr R x 恰好是這個元素。

????“等價類構(gòu)造類型”在未來將被用于基數(shù)、整數(shù)、有理數(shù)、實數(shù)的構(gòu)造。（注：以上代碼中定義了兩種“等價類構(gòu)造類型”，同樣是為了控制層級）

????除了等價關(guān)系以外，序關(guān)系也是常見的關(guān)系。對于關(guān)系 r : A -> A -> Prop 和集合 S : 集合 A，若 r 在 S 的范圍內(nèi)滿足自反性、反對稱性、傳遞性，則 r 被稱為 S 上的偏序關(guān)系；若 r 在 S 的范圍內(nèi)滿足反自反性、反對稱性、傳遞性，則 r 被稱為 S 上的嚴(yán)格偏序關(guān)系。

????容易證明偏序關(guān)系和嚴(yán)格偏序關(guān)系的以下基本性質(zhì)：

????對于 S 上的偏序關(guān)系 r，(fun x y => r x y /\ x <> y) 符合?S 上的嚴(yán)格偏序關(guān)系的要求。以下代碼中，對于 S : 集合 A 和 r : 偏序關(guān)系 S，strict_po r?表示的就是 r 自然對應(yīng)的這個 S 上的嚴(yán)格偏序關(guān)系，它具有類型 嚴(yán)格偏序關(guān)系 S。

????對于全集上的偏序關(guān)系和嚴(yán)格偏序關(guān)系，以上性質(zhì)可以得到簡化。

????子集關(guān)系是偏序關(guān)系的一個常見實例。我們可以相應(yīng)地定義真子集關(guān)系，它與子集偏序關(guān)系對應(yīng)的嚴(yán)格偏序關(guān)系一致。

????對于一個偏序關(guān)系，我們可以定義它的最大值和最小值運算。

????對于?S : 集合 A，r : 偏序關(guān)系 S，T : 集合 A，類型為 A 的?x 被稱為?T 的上界當(dāng)且僅當(dāng) T 為 S 的子集且 x ∈ S 且對于任意的屬于 T 的 y 都有 r y x；x 被稱為 T 的下界當(dāng)且僅當(dāng) T 為 S 的子集且 x ∈ S 且對于任意的屬于 T 的 y 都有 r x y。

????上界集的最小值就是最小上界，下界集的最大值就是最大下界。

????對于?S : 集合 A，r : 偏序關(guān)系 S，T : 集合 A，可定義其極大元集和極小元集。注意“極大元”與“最大值”、“極小元”與“最小值”的差別。