`{A'_cat : IsCategory A'} : IsCategory A. Proof. intros s d. refine (isequiv_homotopic (iscategory_sig_mor_helper o (@idtoiso A' _ _)) _). intro x; apply path_isomorphic; cbn. destruct x; reflexivity. Defined.
Require Import Category.Core Category.Morphisms. Require Import Category.Univalent. Require Import Category.Sigma.Core Category.Sigma.OnObjects Category.Sigma.OnMorphisms. Require Import HoTT.Types HoTT.Basics.