```
module Types.relations where
open import Agda.Primitive using (Level; _⊔_; lsuc; lzero)
open import Lang.dataStructures using (
; true; false;
Bool; ⊤; ℕ; List;
⟂; two; three; four; five; six; seven; eight; nine; ten; zero; succ; _+_;
one_::_; [])
open import Types.functions using (_on_; flip)
```

Relations can be defined as properties that assign truth values to finite tuples of elements. In other words, a relation is a function that accepts a finite set of arguments to produce a truth value. A binary relation would output a truth value given two objects, similarly a unary relation would apply on a single object to output a truth value. This can be generalized to k-ary relations.

In type theory, since relations are also types and “truth values” of a proposition is replaced by existence or
belonging to the universe of all types, one can think of relations as functions that take n-tuples as input and return
some object of type `Set1`

- the set of all `Set`

s.

Nullary relations are functions that can take any object and return an empty set `∅`

:

```
infix 3 ¬_
_ : ∀ {ℓ} → Set ℓ → Set ℓ
¬= P → ⟂ ¬ P
```

In logic, a predicate can essentially be defined as a function that returns a binary value - whether the proposition that the predicate represents is true or false. In type theory, however, we define predicate in a different way. A predicate for us is a function that exists (and hence, is true):

```
: ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ lsuc ℓ)
Pred = A → Set ℓ Pred A ℓ
```

Here, a predicate `P : Pred A ℓ`

can be seen as a subset of A containing all the elements of A that
satisfy property P.

Membership of objects of `A`

in `P`

can be defined as:

```
infix 4 _∈_ _∉_
_∈_ : ∀ {a ℓ} {A : Set a} → A → Pred A ℓ → Set _
= P x
x ∈ P
_∉_ : ∀ {a ℓ} {A : Set a} → A → Pred A ℓ → Set _
= ¬ (x ∈ P) x ∉ P
```

The empty (or false) predicate becomes:

```
: ∀ {a} {A : Set a} → Pred A lzero
∅ = λ _ → ⟂ ∅
```

The singleton predicate (constructor):

```
is_sameAs : ∀ {a} {A : Set a}
→ A
→ Pred A a
is x sameAs = x ≡_
```

```
equal? : is six sameAs (succ five)
equal? = refl
```

A heterogeneous binary relation is defined as:

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

and a homogenous one as:

```
: ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ lsuc ℓ)
Rel = REL A A ℓ Rel A ℓ
```

In type theory, an implication $ A ⟹ B $ is just a function type $ f: A → B $, and if `f`

exists, the
implication does too. We define implication between two relations in agda as:

```
_⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
→ REL A B ℓ₁
→ REL A B ℓ₂
→ Set _
= ∀ {i j} → P i j → Q i j P ⇒ Q
```

A function `f : A → B`

is invariant to two homogenous relations `Rel A ℓ₁`

and
`Rel B ℓ₂`

if $ ∀ x, y ∈ A _{and} f(x), f(y) ∈ B, f(Rel x y) ⟹ (Rel f(x) f(y)) $:

```
_=[_]⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
→ Rel A ℓ₁
→ (A → B)
→ Rel B ℓ₂
→ Set _
= P ⇒ (Q on f) P =[ f ]⇒ Q
```

A function `f`

preserves an underlying relation while operating on a datatype if:

```
_Preserves_⟶_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
→ (A → B)
→ Rel A ℓ₁
→ Rel B ℓ₂
→ Set _
= P =[ f ]⇒ Q f Preserves P ⟶ Q
```

Similarly, a binary operation `_+_`

preserves the underlying relation if:

```
_Preserves₂_⟶_⟶_ : ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c}
→ (A → B → C)
→ Rel A ℓ₁
→ Rel B ℓ₂
→ Rel C ℓ₃
→ Set _
_+_ Preserves₂ P ⟶ Q ⟶ R = ∀ {x y u v} → P x y → Q u v → R (x + u) (y + v)
```

Properties of binary relations:

```
: ∀ {a ℓ} {A : Set a}
Reflexive → Rel A ℓ
→ Set _
_∼_ = ∀ {x} → x ∼ x Reflexive
```

```
: ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
Sym → REL A B ℓ₁
→ REL B A ℓ₂
→ Set _
= P ⇒ flip Q
Sym P Q
: ∀ {a ℓ} {A : Set a}
Symmetric → Rel A ℓ
→ Set _
_∼_ = Sym _∼_ _∼_ Symmetric
```

```
: ∀ {a b c ℓ₁ ℓ₂ ℓ₃} {A : Set a} {B : Set b} {C : Set c}
Trans → REL A B ℓ₁
→ REL B C ℓ₂
→ REL A C ℓ₃
→ Set _
= ∀ {i j k} → P i j → Q j k → R i k
Trans P Q R
: ∀ {a ℓ} {A : Set a}
Transitive → Rel A ℓ
→ Set _
_∼_ = Trans _∼_ _∼_ _∼_ Transitive
```