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.

A binary relation `∙`

between two objects `a`

and `b`

is a function type:

A relation with universe polymorphism could also be defined as:

```
-- 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 naively 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 − 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 until we reach a stage where all tables are different, except then they look identical.

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

Note that this derivation is chosen here for simplicity, later we will go ahead and derive a version with universe polymorphism.