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) `{!AbGroup (A tt)} `{!AbGroup (B tt)} `{!Monoid_Morphism (f tt)}: HomoMorphism sig A B f.
proof: Proof. constructor. * intros []. apply _. * intros []; simpl. + apply preserves_sg_op. + apply groups.preserves_negate. + apply (@preserves_mon_unit (A tt) (B tt) _ _ _ _ _ _ (f tt) _). * eapply encode_algebra_only. * eapply encode_algebra_only. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics categories.categories