@@ -26,10 +26,9 @@ class (Poset t to) => Ordered t (to : t -> t -> Type) where
26class (Preorder t eq) => Equivalence t (eq : t -> t -> Type) where
26class (Preorder t eq) => Equivalence t (eq : t -> t -> Type) where
27 total symmetric : (a : t) -> (b : t) -> eq a b -> eq b a
27 total symmetric : (a : t) -> (b : t) -> eq a b -> eq b a
29−class (Equivalence t eq) => Congruence t (eq : t -> t -> Type) where
29+class (Equivalence t eq) => Congruence t (f : t -> t) (eq : t -> t -> Type) where
30 total congruent : (a : t) ->
30 total congruent : (a : t) ->
31 (b : t) ->
31 (b : t) ->
33 eq a b ->
32 eq a b ->
34 eq (f a) (f b)
33 eq (f a) (f b)
@@ -54,8 +53,8 @@ instance Preorder t ((=) {A = t} {B = t}) where
54instance Equivalence t ((=) {A = t} {B = t}) where
53instance Equivalence t ((=) {A = t} {B = t}) where
55 symmetric a b prf = sym prf
54 symmetric a b prf = sym prf
57−instance Congruence t ((=) {A = t} {B = t}) where
56+instance Congruence t f ((=) {A = t} {B = t}) where
58− congruent a b f = cong {a = a} {b = b} {f = f}
57+ congruent a b = cong {a = a} {b = b} {f = f}
60--------------------------------------------------------------------------------
59--------------------------------------------------------------------------------
61-- Natural numbers
60-- Natural numbers