Control.Relation

A binary relation is a function of type (ty -> ty -> Type).

A prominent example of a binary relation is LTE over Nat.

This module defines some interfaces for describing properties of
binary relations. It also proves somes relations among relations.

Definitions

Rel : Type -> Type

  A relation on ty is a type indexed by two ty values

Totality: total
Visibility: public export

interface Reflexive : (ty : Type) -> (ty -> ty -> Type) -> Type

  A relation is reflexive if x ~ x for every x.

Parameters: ty, rel
Constructor: 

MkReflexive

Methods:

reflexive : rel x x

Implementations:

(Transitive ty rel, (Symmetric ty rel, Serial ty rel)) => Reflexive ty rel

Reflexive ty Equal

Reflexive Nat LTE

reflexive : Reflexive ty rel => rel x x

Totality: total
Visibility: public export

interface Transitive : (ty : Type) -> (ty -> ty -> Type) -> Type

  A relation is transitive if x ~ z when x ~ y and y ~ z.

Parameters: ty, rel
Constructor: 

MkTransitive

Methods:

transitive : rel x y -> rel y z -> rel x z

Implementations:

Transitive ty Equal

Transitive Nat LTE

transitive : Transitive ty rel => rel x y -> rel y z -> rel x z

Totality: total
Visibility: public export

interface Symmetric : (ty : Type) -> (ty -> ty -> Type) -> Type

  A relation is symmetric if y ~ x when x ~ y.

Parameters: ty, rel
Constructor: 

MkSymmetric

Methods:

symmetric : rel x y -> rel y x

Implementation: 

Symmetric ty Equal

symmetric : Symmetric ty rel => rel x y -> rel y x

Totality: total
Visibility: public export

interface Antisymmetric : (ty : Type) -> (ty -> ty -> Type) -> Type

  A relation is antisymmetric if no two distinct elements bear the relation to each other.

Parameters: ty, rel
Constructor: 

MkAntisymmetric

Methods:

antisymmetric : rel x y -> rel y x -> x = y

Implementation: 

Antisymmetric Nat LTE

antisymmetric : Antisymmetric ty rel => rel x y -> rel y x -> x = y

Totality: total
Visibility: public export

interface Dense : (ty : Type) -> (ty -> ty -> Type) -> Type

  A relation is dense if when x ~ y there is z such that x ~ z and z ~ y.

Parameters: ty, rel
Constructor: 

MkDense

Methods:

dense : rel x y -> (z : ty ** (rel x z, rel z y))

Implementation: 

Reflexive ty rel => Dense ty rel

dense : Dense ty rel => rel x y -> (z : ty ** (rel x z, rel z y))

Totality: total
Visibility: public export

interface Serial : (ty : Type) -> (ty -> ty -> Type) -> Type

  A relation is serial if for all x there is a y such that x ~ y.

Parameters: ty, rel
Constructor: 

MkSerial

Methods:

serial : (y : ty ** rel x y)

Implementation: 

Reflexive ty rel => Serial ty rel

serial : Serial ty rel => (y : ty ** rel x y)

Totality: total
Visibility: public export

interface Euclidean : (ty : Type) -> (ty -> ty -> Type) -> Type

  A relation is euclidean if y ~ z when x ~ y and x ~ z.

Parameters: ty, rel
Constructor: 

MkEuclidean

Methods:

euclidean : rel x y -> rel x z -> rel y z

Implementation: 

Euclidean ty Equal

euclidean : Euclidean ty rel => rel x y -> rel x z -> rel y z

Totality: total
Visibility: public export

interface Tolerance : (ty : Type) -> (ty -> ty -> Type) -> Type

  A tolerance relation is reflexive and symmetric.

Parameters: ty, rel
Constraints: Reflexive ty rel, Symmetric ty rel
Implementation: 

Tolerance ty Equal

interface PartialEquivalence : (ty : Type) -> (ty -> ty -> Type) -> Type

  A partial equivalence is transitive and symmetric.

Parameters: ty, rel
Constraints: Transitive ty rel, Symmetric ty rel
Implementation: 

PartialEquivalence ty Equal

interface Equivalence : (ty : Type) -> (ty -> ty -> Type) -> Type

  An equivalence relation is transitive, symmetric, and reflexive.

Parameters: ty, rel
Constraints: Reflexive ty rel, Transitive ty rel, Symmetric ty rel
Implementation: 

Equivalence ty Equal