proposition: Lemma mor_from_sr_to_alg `{InVariety theory A} `{InVariety theory B} (f: ∀ u, A u → B u) `{!Setoid_Morphism (f tt)}: HomoMorphism sig A B f.
proof: Proof. Proof with try apply _. constructor. intros []... intros []. change (Algebra theory A)... change (Algebra theory B)... Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms