`{Funext} {M N : Monoid} {f g : MonoidHomomorphism M N} : f == g <~> f = g. Proof. refine ((equiv_ap (issig_MonoidHomomorphism M N)^-1 _ _)^-1 oE _). refine (equiv_path_sigma_hprop _ _ oE _). apply equiv_path_forall. Defined.
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.