def Rel' (A : Type) (B : Type) ⇒ A → B → Type
def Rel (A : Type) ⇒ Rel' A A

variable A B C : Type
def Reflexive (r : Rel A) ⇒ ∀ {x : A} → r x x

//  Generalised transitivity.
def Trans (P : Rel' A B) (Q : Rel' B C) (R : Rel' A C) ⇒ ∀ {x} {y} {z} → P x y → Q y z → R x z

// A flipped variant of generalised transitivity.
def TransFlip (P : Rel' A B) (Q : Rel' B C) (R : Rel' A C) ⇒ ∀ {x} {y} {z} → Q y z → P x y → R x z

def Transitive (r : Rel A) ⇒ Trans r r r

// Generalised symmetry.
def Sym (P : Rel' A B) (Q : Rel' B A) ⇒ ∀ {x} {y} → P x y → Q y x

def Symmetric (r : Rel A) ⇒ Sym r r