Decidable.Order.Strict

An strict preorder (sometimes known as a quasi-order, or an
ordering) is what you get when you remove the diagonal `{(a,b) | a
r b , b r a}` from a preorder. For example a < b is an ordering.
This module extends base's Control.Order with the strict versions.
The interface system seems to struggle a bit with some of the constructions,
so I hacked them a bit. Sorry.

Definitions

interface Irreflexive : (ty : Type) -> (ty -> ty -> Type) -> Type

Parameters: ty, rel
Methods:

irreflexive : Not (rel x x)

Implementation: 

Irreflexive Nat LT

irreflexive : Irreflexive ty rel => Not (rel x x)

Totality: total
Visibility: public export

interface StrictPreorder : (ty : Type) -> (ty -> ty -> Type) -> Type

Parameters: ty, rel
Constraints: Transitive ty rel, Irreflexive ty rel
Implementation: 

StrictPreorder Nat LT

interface Asymmetric : (ty : Type) -> (ty -> ty -> Type) -> Type

Parameters: ty, rel
Methods:

asymmetric : rel x y -> Not (rel y x)

asymmetric : Asymmetric ty rel => rel x y -> Not (rel y x)

Totality: total
Visibility: public export

record EqOr : Rel t -> t -> t -> Type

Totality: total
Visibility: public export
Constructor: 

MkEqOr : Either (a = b) (spo a b) -> EqOr spo a b

Projection: 

.runEqOr : EqOr spo a b -> Either (a = b) (spo a b)

Hints:

(Irreflexive ty rel, Asymmetric ty rel) => Antisymmetric ty (EqOr rel)

Connex ty rel => Connex ty (EqOr rel)

(Irreflexive ty rel, (Asymmetric ty rel, Transitive ty rel)) => PartialOrder ty (EqOr rel)

Transitive ty rel => Preorder ty (EqOr rel)

Reflexive ty (EqOr rel)

(Connex ty rel, DecEq ty) => StronglyConnex ty (EqOr rel)

Transitive ty rel => Transitive ty (EqOr rel)

.runEqOr : EqOr spo a b -> Either (a = b) (spo a b)

Totality: total
Visibility: public export

runEqOr : EqOr spo a b -> Either (a = b) (spo a b)

Totality: total
Visibility: public export

data DecOrdering : t -> t -> Type

Totality: total
Visibility: public export
Constructors:

DecLT : lt a b -> DecOrdering a b

DecEQ : a = b -> DecOrdering a b

DecGT : lt b a -> DecOrdering a b

interface StrictOrdered : (t : Type) -> (t -> t -> Type) -> Type

Parameters: t, spo
Constraints: StrictPreorder t spo
Methods:

order : (a : t) -> (b : t) -> DecOrdering a b

Implementation: 

StrictOrdered Nat LT

order : StrictOrdered t spo => (a : t) -> (b : t) -> DecOrdering a b

Totality: total
Visibility: public export