我试图理解 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 and B，你必须谈论所有A- and B- 索引类型，即你必须谈论的RelationOverAandB = A → B → Set.
如果您想抽象关系的左侧和右侧基本类型，则意味着选择A and B不再固定。所以你必须谈谈REL，使得REL A B = A → B → Set.
那么，什么是类型REL？正如我们从REL A B例如，它需要选择A and B作为两个参数；其结果是type A → B → Set.
总结一下：给定
A : Set
B : Set
we have
REL A B = A → B → Set
它本身有类型Set（请记住，我们在这里忽略了宇宙级别）。
因此，
REL : Set → Set → Set ∎
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
