`{Funext} {σ} {A B : Algebra σ} (f g : A $-> B) (p : def_homomorphism f = def_homomorphism g) : f = g. Proof. apply (ap (issig_homomorphism A B)^-1)^-1. unfold issig_homomorphism; cbn. apply path_sigma_hprop. exact p. Defined.
Require Import