proposition: Lemma encode_morphism_only `{AlgebraOps theory A} `{∀ u, Equiv (A u)} `{AlgebraOps theory B} `{∀ u, Equiv (B u)} (f: ∀ u, A u → B u) `{!SemiGroup_Morphism (f tt)}: HomoMorphism sig A B f.
proof: Proof. pose proof (sgmor_a (f:=f tt)). pose proof (sgmor_b (f:=f tt)). constructor. intros []. apply _. intros []; simpl. apply preserves_sg_op. apply (encode_algebra_only). apply encode_algebra_only. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics categories.categories