Relations can be defined as properties that assign truth values to finite tuples of elements. 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, however, 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. A binary relation `∙`

between two objects `a`

and `b`

is a function type:

A relation with universe polymorphism could also be defined as:

```
open import Agda.Primitive using (Level; _⊔_; lsuc)
-- heterogenous relation
REL : ∀ {a b} → Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ lsuc ℓ)
REL A B ℓ = A → B → Set ℓ
-- homogenous relation
R : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ lsuc ℓ)
R A ℓ = REL A A ℓ
```

The first definition being easier for our purposes here, we proceed with that.

Relations can conform to certain properties, which later come in handy for classifying relations and building a lot of mathematical structure.

A reflexive relation is one where \[ x ∙ y = y ∙ x \]:

A symmetric relation is one where \[ x ∙ y ⟹ y ∙ x \]:

A transitive relation is one where \[ x ∙ y, y ∙ z ~then~ z ∙ x \]:

A congruent relation is one where a function \[ x ∙ y ⟹ f(x) ∙ f(y) \] or the function `f`

preserves the relation :

A substitutive relation is one where \[ x ∙ y ~and~ (predicate~ y) = ⊤ ⟹ (predicate~ x) = ⊤ \] :

```
substitutive : {A : Set} → Rel A → Set1
substitutive {A} _★_ = (P : A → Set)(x y : A)
→ x ★ y
→ P x
→ P y
```

An equivalence relation is a relation which is:

- reflexive: a = a
- symmetric: if a = b then b = a
- transitive: if a = b and b = c then a = c

All forms of what we know as “equality” are equivalence relations. They help in identifying similar objects and can be “weak” or “strong” depending upon how much similarity they capture of the objects they compare. For e.g. all “tables” fall under one equivalence class wherein when we refer to a generic “table” we mean as in all tables as equal. Whereas, if we were comparing tables amongst themselves, we’d use other finer criteria in our equivalence relations, classifying some tables as coffee tables and so on.

```
record Equivalence (A : Set) : Set1 where
field
_==_ : Rel A
refl : reflexive _==_
sym : symmetric _==_
trans : transitive _==_
```