agda - 如何在 agda 中解释 REL

Question

我试图了解Agda标准库的某些部分，但我似乎无法弄清楚REL的定义.
FWIW 这里是 REL 的定义:

-- Binary relations

-- Heterogeneous binary relations

REL : ∀ {a b} → Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ suc ℓ)
REL A B ℓ = A → B → Set ℓ

我在网上找不到任何解释这一点的文档，这就是我在这里问的原因。这如何定义二元关系？

Answer 1

@RodrigoRibeiro 的回答解释了 Level位，但是一旦你摆脱了宇宙级别，类型 Set → Set → Set 是什么？与二元关系有关吗？

假设您有一个二元关系 R ⊆ A × B .建模它的命题方法是创建一些索引类型 R : A → B → Set这样对于任何 a : A, b : B , R a b有居民 iff (a, b) ∈ R .所以如果你想在A上讨论所有的关系和 B ，你要谈的都是A - 和 B - 索引类型，即你必须谈论 RelationOverAandB = A → B → Set .

如果你想抽象关系的左手和右手基类型，那就意味着选择 A和 B不再固定。所以你要谈REL ，使得 REL A B = A → B → Set .

那么，REL 的类型是什么？ ?正如我们从 REL A B 中看到的例如，它需要选择 A和 B作为两个论点；其结果是类型 A → B → Set .

总结一下:给定

A : Set
B : Set

我们有

REL A B = A → B → Set 

它本身具有类型 Set (请记住，我们在这里忽略了宇宙级别)。

因此，

REL : Set → Set → Set ∎