`{Funext} {σ : Signature} (A B : object (precategory_algebra σ)) : @Morphisms.idtoiso (precategory_algebra σ) A B = catiso_to_uaiso^-1 o isomorphic_id o (path_setalgebra A B)^-1. Proof. funext p. destruct p. by apply Morphisms.path_isomorphic. Defined.
Require Import Import Morphisms.CategoryMorphismsNotations isomorphic_notations.