+ndefinition binary_morph_setoid : setoid → setoid → setoid → setoid.
+#S1; #S2; #T; @ (binary_morphism S1 S2 T); @;
+##[ #f; #g; napply (∀x,y. f x y = g x y);
+##| #f; #x; #y; napply #;
+##| #f; #g; #H; #x; #y; napply ((H x y)^-1);
+##| #f; #g; #h; #H1; #H2; #x; #y; napply (trans … (H1 …) (H2 …)); ##]
+nqed.
+
+ndefinition unary_morph_setoid : setoid → setoid → setoid.
+#S1; #S2; @ (unary_morphism S1 S2); @;
+##[ #f; #g; napply (∀x. f x = g x);
+##| #f; #x; napply #;
+##| #f; #g; #H; #x; napply ((H x)^-1);
+##| #f; #g; #h; #H1; #H2; #x; napply (trans … (H1 …) (H2 …)); ##]
+nqed.
+