Definition addStructure {B C:category} {P:ob C -> UU} (F:B⟶C) (h : ∏ b, P(F b)) : B ⟶ categoryWithStructure C P. Proof. unshelve refine (makeFunctor _ _ _ _). - intros b. exact (F b,,h b). - intros b b' f. exact (# F f). - abstract (intros b; simpl; apply functor_id) using _L_. - abstract (intros b b' b'' f g; simpl; apply functor_comp) using _L_. Defined.
Require Import UniMath.MoreFoundations.Tactics.