proposition: Lemma path_hset_isomorphic `{Funext} {σ : Signature} {A B : Algebra σ} `{IsHSetAlgebra B} (F G : A ≅ B) (a : def_isomorphic F = def_isomorphic G) : F = G.
proof: Proof. apply (path_isomorphic F G a). apply path_ishprop. Defined.
imports: HoTT.Classes.theory.ua_homomorphism HoTT.Types HoTT.Tactics