proposition: Lemma path_idtoiso_isomorphic_id `{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: Proof. funext p. destruct p. by apply Morphisms.path_isomorphic. Defined.
imports: HoTT.Types HoTT.Categories.Category.Core HoTT.Categories.Category.Univalent HoTT.Classes.theory.ua_isomorphic