{σ : Signature} {A B : Algebra σ} (Φ : forall s, Relation (A s)) `{!IsCongruence A Φ} (f : forall s, A s -> B s) `{!IsHomomorphism f} : Type := forall s (x y : A s), Φ s x y -> f s x = f s y.
Require Import