Idris2Doc : Control.Order

Control.Order

```An order is a particular kind of binary relation. The order
relation is intended to proceed in some direction, though not
necessarily with a unique path.

Orders are often defined simply as bundles of binary relation
properties.

A prominent example of an order relation is LTE over Nat.
```

Definitions

`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`