proposition: Lemma catiso_to_uaiso `{Funext} {σ} {A B : object (precategory_algebra σ)} : A <~=~> B → A ≅ B.
proof: Proof. intros [f [a b c]]. unshelve eapply (@BuildIsomorphic _ _ _ f). intros s. refine (isequiv_adjointify (f s) (a s) _ _). - exact (apD10_homomorphism c s). - exact (apD10_homomorphism b s). Defined.
imports: HoTT.Types HoTT.Categories.Category.Core HoTT.Categories.Category.Univalent HoTT.Classes.theory.ua_isomorphic