Idris2Doc : Control.Relation

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

Implementation:
`Reflexive ty rel => Dense ty rel`
`dense : Dense ty rel => rel x y -> DPair ty (\z => (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 : DPair ty (\y => rel x y)`

Implementation:
`Reflexive ty rel => Serial ty rel`
`serial : Serial ty rel => DPair ty (\y => 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`