how to interpret REL in agda

Question

I'm trying to understand some parts of the standard library of Agda, and I can't seem to figure out the definition of REL. FWIW here's the definition of REL:

-- Binary relations

-- Heterogeneous binary relations

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

I can't find any documentation online explaining this, which is why I'm asking here. How does this define a binary relation?

Answer 1

@RodrigoRibeiro's answer explains the Level bits, but once you get rid of universe levels, what does the type Set → Set → Set have to do with binary relations?

Suppose you have a binary relation R ⊆ A × B. The propositional way of modeling it is to create some indexed type R : A → B → Set such that for any a : A, b : B, R a b has inhabitants iff (a, b) ∈ R. So if you want to talk about all relations over A and B, you have to talk about all A- and B- indexed types, i.e. you have to talk about RelationOverAandB = A → B → Set.

If you then want to abstract over the relation's left- and right-hand base type, that means the choice of A and B are not fixed anymore. So you have to talk about REL, such that REL A B = A → B → Set.

What, then, is the type of REL? As we have seen from the REL A B example, it takes the choice of A and B as two arguments; and its result is the type A → B → Set.

So to summarize: given

A : Set
B : Set

we have

REL A B = A → B → Set 

which itself has type Set (remember, we're ignoring universe levels here).

And thus,

REL : Set → Set → Set ∎

Answer 2

I guess it's easier to look at an example:

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

The type signature is equivalent to

data _≤_ : ℕ -> ℕ -> Set where

So _≤_ is a relation between two natural numbers. It contains all pairs of numbers such that the first number is less or equal than the second. In the same way we can write

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

The type signature is equivalent to

data _∈_ {α} {A : Set α} : A -> List A -> Set where

_∈_ is a relation between elements of type A and lists of elements of type A.

The universe monomorphic variant of REL is itself a binary relation:

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