{M N : Monoid} (f : MonoidHomomorphism M N) : forall (x y : M), f (x * y) = f x * f y := monmor_sgmor.
Require Import Basics.Overture Basics.Tactics Basics.Equivalences Basics.Trunc. Require Import Types.Sigma Types.Forall Types.Prod. Require Import WildCat.Core WildCat.Induced WildCat.Equiv WildCat.Universe Require Import (notations) Classes.interfaces.canonical_names.