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.```
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
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 -> DPairty (\z => (relxz, relzy))

Implementation:
Reflexivetyrel => Densetyrel
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
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
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
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
Rel : Type -> Type
`  A relation on ty is a type indexed by two ty values`

Totality: total
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 : DPairty (\y => relxy)

Implementation:
Reflexivetyrel => Serialtyrel
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
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
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
antisymmetric : Antisymmetrictyrel => relxy -> relyx -> x = y
Totality: total
dense : Densetyrel => relxy -> DPairty (\z => (relxz, relzy))
Totality: total
euclidean : Euclideantyrel => relxy -> relxz -> relyz
Totality: total
reflexive : Reflexivetyrel => relxx
Totality: total
serial : Serialtyrel => DPairty (\y => relxy)
Totality: total
symmetric : Symmetrictyrel => relxy -> relyx
Totality: total
transitive : Transitivetyrel => relxy -> relyz -> relxz
Totality: total