`{Funext} {σ : Signature} {A B : Algebra σ} `{IsHSetAlgebra B} (F G : A ≅ B) (a : def_isomorphic F = def_isomorphic G) : F = G. Proof. apply (path_isomorphic F G a). apply path_ishprop. Defined.
Require Import Import isomorphic_notations.