Definition categoryWithStructure (C:category) (P:ob C -> UU) : category. Proof. use makecategory. - exact (∑ c:C, P c). - intros x y. exact (pr1 x --> pr1 y). - intros. apply homset_property. - intros x. apply identity. - intros x y z f g. exact (g ∘ f). - intros. apply id_left. - intros. apply id_right. - intros. apply assoc. - intros. apply assoc'. Defined.
Require Import UniMath.MoreFoundations.Tactics.