Contents Previous Next


Relations

module Types.relations where

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 Sets. A binary relation between two objects a and b is a function type:

Rel : Set  Set1
Rel A = A  A  Set

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.

Properties of relations

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

Reflexive

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

Figure 1: Refl
reflexive : {A : Set}
   Rel A
   Set
reflexive {A} __ = (x : A)  x ★ x

Symmetric

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

Figure 2: Symmetric
symmetric : {A : Set}  Rel A  Set
symmetric {A} __  = (x y : A)
   x ★ y
   y ★ x

Transitive

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

Figure 3: Transitive
transitive : {A : Set}  Rel A  Set
transitive {A} __ = (x y z : A)
   x ★ y
   y ★ z
   x ★ z

Congruent

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

congruent : {A : Set}  Rel A  Set
congruent {A} __ = (f : A  A)(x y : A)
   x ★ y
   f x ★ f y

Substitutive

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

Equivalence relation

An equivalence relation is a relation which is:

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 _==_

Equality