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.

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

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 -> DPair ty (\z => (rel x z, rel z y))

Implementation:

Reflexive ty rel => Dense ty rel

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

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

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

Rel : Type -> Type

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

Totality: total

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 : DPair ty (\y => rel x y)

Implementation:

Reflexive ty rel => Serial ty rel

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

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

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

Totality: total

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

Totality: total

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

Totality: total

reflexive : Reflexive ty rel => rel x x

Totality: total

serial : Serial ty rel => DPair ty (\y => rel x y)

Totality: total

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

Totality: total

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

Totality: total