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
interfaceReflexive : (ty : Type) -> (ty->ty->Type) ->Type
A relation is reflexive if x ~ x for every x.

Parameters: ty, rel
Constructor: MkReflexive
Methods:
reflexive : relxx

Implementations:
(Transitivetyrel, (Symmetrictyrel, Serialtyrel)) =>Reflexivetyrel
ReflexivetyEqual
ReflexiveNatLTE
reflexive : Reflexivetyrel=>relxx
Totality: total
Visibility: public export
interfaceTransitive : (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 : relxy->relyz->relxz

Implementations:
TransitivetyEqual
TransitiveNatLTE
transitive : Transitivetyrel=>relxy->relyz->relxz
Totality: total
Visibility: public export
interfaceSymmetric : (ty : Type) -> (ty->ty->Type) ->Type
A relation is symmetric if y ~ x when x ~ y.

Parameters: ty, rel
Constructor: MkSymmetric
Methods:
symmetric : relxy->relyx

Implementation:
SymmetrictyEqual
symmetric : Symmetrictyrel=>relxy->relyx
Totality: total
Visibility: public export
interfaceAntisymmetric : (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 : relxy->relyx->x=y

Implementation:
AntisymmetricNatLTE
antisymmetric : Antisymmetrictyrel=>relxy->relyx->x=y
Totality: total
Visibility: public export
interfaceDense : (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 : relxy-> (z : ty** (relxz, relzy))

Implementation:
Reflexivetyrel=>Densetyrel
dense : Densetyrel=>relxy-> (z : ty** (relxz, relzy))
Totality: total
Visibility: public export
interfaceSerial : (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**relxy)

Implementation:
Reflexivetyrel=>Serialtyrel
serial : Serialtyrel=> (y : ty**relxy)
Totality: total
Visibility: public export
interfaceEuclidean : (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 : relxy->relxz->relyz

Implementation:
EuclideantyEqual
euclidean : Euclideantyrel=>relxy->relxz->relyz
Totality: total
Visibility: public export
interfaceTolerance : (ty : Type) -> (ty->ty->Type) ->Type
A tolerance relation is reflexive and symmetric.

Parameters: ty, rel
Constraints: Reflexive ty rel, Symmetric ty rel
Implementation:
TolerancetyEqual
interfacePartialEquivalence : (ty : Type) -> (ty->ty->Type) ->Type
A partial equivalence is transitive and symmetric.

Parameters: ty, rel
Constraints: Transitive ty rel, Symmetric ty rel
Implementation:
PartialEquivalencetyEqual
interfaceEquivalence : (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:
EquivalencetyEqual