如何解释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 ?

Answer 2

我想看一个例子更容易:

import Level
open import Relation.Binary
open import Data.Nat.Base hiding (_?_)

data _?_ : REL ? ? Level.zero where
  z?n : ? {n} -> 0 ? n
  s?s : ? {n m} -> n ? m -> suc n ? suc m

类型签名相当于

data _?_ : ? -> ? -> Set where

_?_两个自然数之间的关系也是如此.它包含所有数字对,使得第一个数字小于或等于第二个数字.以同样的方式我们可以写

open import Data.List.Base

data _?_ {?} {A : Set ?} : REL A (List A) Level.zero where
  here  : ? {x xs} -> x ? x ? xs
  there : ? {x y xs} -> x ? xs -> x ? y ? xs

类型签名相当于

data _?_ {?} {A : Set ?} : A -> List A -> Set where

_?_是类型A元素和类型元素列表之间的关系A.

宇宙单态变体REL本身就是一个二元关系:

MonoREL : REL Set Set (Level.suc Level.zero)
MonoREL A B = A ? B ? Set