`{Univalence} (σ : Signature) : IsCategory (precategory_algebra σ). Proof. intros A B. rewrite path_idtoiso_isomorphic_id. apply @isequiv_compose. - apply isequiv_compose. - apply isequiv_inverse. Qed.
Require Import Import Morphisms.CategoryMorphismsNotations isomorphic_notations.