@@ -11,17 +11,12 @@ import Decidable.Equality
1111-- Preorders and Posets
1212--------------------------------------------------------------------------------
1313
14−using (t : Type)
15− data Preorder : (t -> t -> Type) -> Type where
16− transRefl : ((a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c) ->
17− ((a : t) -> po a a) ->
18− Preorder po
14+class Preorder t (po : t -> t -> Type) where
15+ total transitive : (a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c
16+ total reflexive : (a : t) -> po a a
1917
20−
21− data Poset : (t -> t -> Type) -> Type where
22− preorderAntisym : Preorder {t = t} po ->
23− ((a : t) -> (b : t) -> po a b -> po b a -> a = b) ->
24− Poset po
18+class (Preorder t po) => Poset t (po : t -> t -> Type) where
19+ total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b
2520
2621--------------------------------------------------------------------------------
2722-- Natural numbers
@@ -41,16 +36,17 @@ NatLTEIsTransitive m n (S o) mLTEn (nLTESm nLTEo)
4136total NatLTEIsReflexive : (n : Nat) -> NatLTE n n
4237NatLTEIsReflexive _ = nEqn
4338
44−NatLTEIsPreorder : Preorder NatLTE
45−NatLTEIsPreorder = transRefl NatLTEIsTransitive NatLTEIsReflexive
39+instance Preorder Nat NatLTE where
40+ transitive = NatLTEIsTransitive
41+ reflexive = NatLTEIsReflexive
4642
4743total NatLTEIsAntisymmetric : (m : Nat) -> (n : Nat) -> po m n -> po n m -> m = n
4844NatLTEIsAntisymmetric n n nEqn nEqn = refl
4945NatLTEIsAntisymmetric n m nEqn (nLTESm _) impossible
5046NatLTEIsAntisymmetric n m (nLTESm _) nEqn impossible
5147
52−NatLTEIsPoset : Poset NatLTE
53−NatLTEIsPoset = preorderAntisym NatLTEIsPreorder NatLTEIsAntisymmetric
48+instance Poset Nat NatLTE where
49+ antisymmetric = NatLTEIsAntisymmetric
5450
5551total zeroNeverGreater : {n : Nat} -> NatLTE (S n) O -> _|_
5652zeroNeverGreater {n} (nLTESm _) impossible
@@ -77,3 +73,5 @@ instance Rel NatLTE where
7773instance Decidable NatLTE where
7874 decide = decideNatLTE
7975
76+lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
77+lte m n = decide {p = NatLTE} m n