proposition: Lemma path_homomorphism {σ} {A B : Algebra σ} (f g : Homomorphism A B) (p : def_hom f = def_hom g) (q : p#(is_homomorphism_hom f) = is_homomorphism_hom g) : f = g.
proof: Proof. destruct f, g. simpl in *. by path_induction. Defined.
imports: HoTT.Classes.interfaces.ua_setalgebra HoTT.Types HoTT.Tactics