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