`{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. apply (ap (issig_isomorphic A B)^-1)^-1. srapply path_sigma. - exact a. - apply path_sigma_hprop. refine (ap _ (transport_sigma _ _) @ _). apply b. Defined.
Require Import Import isomorphic_notations.