proposition: Lemma path_hset_homomorphism `{Funext} {σ} {A B : Algebra σ} `{!IsHSetAlgebra B} (f g : Homomorphism A B) (p : def_hom f = def_hom g) : f = g.
proof: Proof. apply (path_homomorphism f g p). apply path_ishprop. Defined.
imports: HoTT.Classes.interfaces.ua_setalgebra HoTT.Types HoTT.Tactics