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

Implementation: 
Reflexivetyrel=>Densetyrel
dense : Densetyrel=>relxy->DPairty (\z=> (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 : DPairty (\y=>relxy)

Implementation: 
Reflexivetyrel=>Serialtyrel
serial : Serialtyrel=>DPairty (\y=>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