proposition: Lemma path_homomorphism `{Funext} {σ} {A B : Algebra σ} (f g : A $-> B) (p : def_homomorphism f = def_homomorphism g) : f = g.
proof: Proof. apply (ap (issig_homomorphism A B)^-1)^-1. unfold issig_homomorphism; cbn. apply path_sigma_hprop. exact p. Defined.
imports: HoTT.Algebra.Universal.Algebra HoTT.WildCat.Core HoTT.Types