proposition: Lemma uaiso_to_catiso `{Funext} {σ} {A B : object (precategory_algebra σ)} : A ≅ B → A <~=~> B.
proof: Proof. intros [f F G]. set (h := BuildHomomorphism f). apply (@Morphisms.Build_Isomorphic _ A B h). apply (@Morphisms.Build_IsIsomorphism _ A B h (hom_inv h)). - apply path_hset_homomorphism. funext s x. apply eissect. - apply path_hset_homomorphism. funext s x. apply eisretr. Defined.
imports: HoTT.Types HoTT.Categories.Category.Core HoTT.Categories.Category.Univalent HoTT.Classes.theory.ua_isomorphic