proposition: Lemma path_isomorphic `{Funext} {σ : Signature} {A B : Algebra σ} (F G : A ≅ B) (a : def_isomorphic F = def_isomorphic G) (b : a#(is_homomorphism_isomorphic F) = is_homomorphism_isomorphic G) : F = G.
proof: Proof. apply (ap (issig_isomorphic A B)^-1)^-1. srapply path_sigma. - exact a. - apply path_sigma_hprop. refine (ap _ (transport_sigma _ _) @ _). apply b. Defined.
imports: HoTT.Classes.theory.ua_homomorphism HoTT.Types HoTT.Tactics