我试图了解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 ℓ
我在网上找不到任何解释这一点的文档,这就是我在这里问的原因。这如何定义二元关系?
最佳答案
@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 ∎
关于agda - 如何在 agda 中解释 REL,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/34602204/