interface Preorder : (ty : Type) -> (ty -> ty -> Type) -> Type
A preorder is reflexive and transitive.
Parameters: ty, rel
Constraints: Reflexive ty rel, Transitive ty rel
Implementation: Preorder Nat LTE
interface PartialOrder : (ty : Type) -> (ty -> ty -> Type) -> Type
A partial order is an antisymmetrics preorder.
Parameters: ty, rel
Constraints: Preorder ty rel, Antisymmetric ty rel
Implementation: PartialOrder Nat LTE
interface Connex : (ty : Type) -> (ty -> ty -> Type) -> Type
A relation is connex if for any two distinct x and y, either x ~ y or y ~ x.
This can also be stated as a trichotomy: x ~ y or x = y or y ~ x.
Parameters: ty, rel
Methods:
connex : Not (x = y) -> Either (rel x y) (rel y x)
Implementation: Connex Nat LTE
connex : Connex ty rel => Not (x = y) -> Either (rel x y) (rel y x)
- Visibility: public export
interface StronglyConnex : (ty : Type) -> (ty -> ty -> Type) -> Type
A relation is strongly connex if for any two x and y, either x ~ y or y ~ x.
Parameters: ty, rel
Methods:
order : (x : ty) -> (y : ty) -> Either (rel x y) (rel y x)
order : StronglyConnex ty rel => (x : ty) -> (y : ty) -> Either (rel x y) (rel y x)
- Visibility: public export
interface LinearOrder : (ty : Type) -> (ty -> ty -> Type) -> Type
A linear order is a connex partial order.
Parameters: ty, rel
Constraints: PartialOrder ty rel, Connex ty rel
Implementation: LinearOrder Nat LTE