proposition: Lemma iscategory_algebra `{Univalence} (σ : Signature) : IsCategory (precategory_algebra σ).
proof: Proof. intros A B. rewrite path_idtoiso_isomorphic_id. apply @isequiv_compose. - apply isequiv_compose. - apply isequiv_inverse. Qed.
imports: HoTT.Types HoTT.Categories.Category.Core HoTT.Categories.Category.Univalent HoTT.Classes.theory.ua_isomorphic