@@ -26,10 +26,9 @@ class (Poset t to) => Ordered t (to : t -> t -> Type) where
2626class (Preorder t eq) => Equivalence t (eq : t -> t -> Type) where
2727 total symmetric : (a : t) -> (b : t) -> eq a b -> eq b a
2828
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
3030 total congruent : (a : t) ->
3131 (b : t) ->
32− (f : t -> t) ->
3332 eq a b ->
3433 eq (f a) (f b)
3534
@@ -54,8 +53,8 @@ instance Preorder t ((=) {A = t} {B = t}) where
5453instance Equivalence t ((=) {A = t} {B = t}) where
5554 symmetric a b prf = sym prf
5655
57−instance Congruence t ((=) {A = t} {B = t}) where
58− congruent a b f = cong {a = a} {b = b} {f = f}
56+instance Congruence t f ((=) {A = t} {B = t}) where
57+ congruent a b = cong {a = a} {b = b} {f = f}
5958
6059--------------------------------------------------------------------------------
6160-- Natural numbers