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

leftmost : (0 rel : (ty -> ty -> Type)) -> StronglyConnex ty rel => ty -> ty -> ty

  Gives the leftmost of a strongly connex relation among the given two elements, generalisation of `min`.
  
  That is, leftmost x y ~ x and leftmost x y ~ y, and `leftmost x y` is either `x` or `y`

Visibility: public export

rightmost : (0 rel : (ty -> ty -> Type)) -> StronglyConnex ty rel => ty -> ty -> ty

  Gives the rightmost of a strongly connex relation among the given two elements, generalisation of `max`.
  
  That is, x ~ rightmost x y and y ~ rightmost x y, and `rightmost x y` is either `x` or `y`

Visibility: public export

leftmostRelL : (0 rel : (ty -> ty -> Type)) -> Reflexive ty rel => {auto {conArg:2893} : StronglyConnex ty rel} -> (x : ty) -> (y : ty) -> rel (leftmost rel x y) x

Visibility: export

leftmostRelR : (0 rel : (ty -> ty -> Type)) -> Reflexive ty rel => {auto {conArg:2963} : StronglyConnex ty rel} -> (x : ty) -> (y : ty) -> rel (leftmost rel x y) y

Visibility: export

leftmostPreserves : (0 rel : (ty -> ty -> Type)) -> {auto {conArg:3030} : StronglyConnex ty rel} -> (x : ty) -> (y : ty) -> Either (leftmost rel x y = x) (leftmost rel x y = y)

Visibility: export

leftmostIsRightmostLeft : (0 rel : (ty -> ty -> Type)) -> {auto {conArg:3113} : StronglyConnex ty rel} -> (x : ty) -> (y : ty) -> (z : ty) -> rel z x -> rel z y -> rel z (leftmost rel x y)

Visibility: export

rightmostRelL : (0 rel : (ty -> ty -> Type)) -> Reflexive ty rel => {auto {conArg:3188} : StronglyConnex ty rel} -> (x : ty) -> (y : ty) -> rel x (rightmost rel x y)

Visibility: export

rightmostRelR : (0 rel : (ty -> ty -> Type)) -> Reflexive ty rel => {auto {conArg:3258} : StronglyConnex ty rel} -> (x : ty) -> (y : ty) -> rel y (rightmost rel x y)

Visibility: export

rightmostPreserves : (0 rel : (ty -> ty -> Type)) -> {auto {conArg:3325} : StronglyConnex ty rel} -> (x : ty) -> (y : ty) -> Either (rightmost rel x y = x) (rightmost rel x y = y)

Visibility: export

rightmostIsLeftmostRight : (0 rel : (ty -> ty -> Type)) -> {auto {conArg:3408} : StronglyConnex ty rel} -> (x : ty) -> (y : ty) -> (z : ty) -> rel x z -> rel y z -> rel (leftmost rel x y) z

Visibility: export