@@ -10,7 +10,7 @@ import Decidable.Equality
1010--------------------------------------------------------------------------------
1111
1212--------------------------------------------------------------------------------
13−-- Preorders and Posets
13+-- Preorders, Posets and total Orders
1414--------------------------------------------------------------------------------
1515
1616class Preorder t (po : t -> t -> Type) where
@@ -23,6 +23,16 @@ class (Preorder t po) => Poset t (po : t -> t -> Type) where
2323class (Poset t to) => Ordered t (to : t -> t -> Type) where
2424 total order : (a : t) -> (b : t) -> Either (to a b) (to b a)
2525
26+minimum : (Ordered t to) => t -> t -> t
27+minimum x y with (order x y)
28+ | Left _ = x
29+ | Right _ = y
30+
31+maximum : (Ordered t to) => t -> t -> t
32+maximum x y with (order x y)
33+ | Left _ = y
34+ | Right _ = x
35+
2636--------------------------------------------------------------------------------
2737-- Natural numbers
2838--------------------------------------------------------------------------------
@@ -101,15 +111,9 @@ instance Ordered Nat NatLTE where
101111 order (S k) (S j) | Left prf = Left (shift k j prf)
102112 order (S k) (S j) | Right prf = Right (shift j k prf)
103113
104−minimum : (Ordered t to) => t -> t -> t
105−minimum x y with (order x y)
106− | Left _ = x
107− | Right _ = y
108−
109−maximum : (Ordered t to) => t -> t -> t
110−maximum x y with (order x y)
111− | Left _ = y
112− | Right _ = x
114+--------------------------------------------------------------------------------
115+-- Finite numbers
116+--------------------------------------------------------------------------------
113117
114118using (k : Nat)
115119 data FinLTE : Fin k -> Fin k -> Type where