@@ -10,7 +10,7 @@ import Decidable.Equality
1010--------------------------------------------------------------------------------
1111
1212--------------------------------------------------------------------------------
13−-- Preorders, Posets and total Orders
13+-- Preorders, Posets, total Orders, Equivalencies, Congruencies
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+class (Preorder t eq) => Equivalence t (eq : t -> t -> Type) where
27+ total symmetric : (a : t) -> (b : t) -> eq a b -> eq b a
28+
29+class (Equivalence t eq) => Congruence t (eq : t -> t -> Type) where
30+ total congruent : (a : t) ->
31+ (b : t) ->
32+ (f : t -> t) ->
33+ eq a b ->
34+ eq (f a) (f b)
35+
2636minimum : (Ordered t to) => t -> t -> t
2737minimum x y with (order x y)
2838 | Left _ = x
@@ -33,6 +43,20 @@ maximum x y with (order x y)
3343 | Left _ = y
3444 | Right _ = x
3545
46+--------------------------------------------------------------------------------
47+-- Syntactic equivalence (=)
48+--------------------------------------------------------------------------------
49+
50+instance Preorder t ((=) {A = t} {B = t}) where
51+ transitive a b c = trans {a = a} {b = b} {c = c}
52+ reflexive a = refl
53+
54+instance Equivalence t ((=) {A = t} {B = t}) where
55+ symmetric a b prf = sym prf
56+
57+instance Congruence t ((=) {A = t} {B = t}) where
58+ congruent a b f = cong {a = a} {b = b} {f = f}
59+
3660--------------------------------------------------------------------------------
3761-- Natural numbers
3862--------------------------------------------------------------------------------