Definition functorWithStructures {C:category} {P Q:ob C -> UU} (F : ∏ c, P c -> Q c) : categoryWithStructure C P ⟶ categoryWithStructure C Q. Proof. unshelve refine (makeFunctor _ _ _ _). - exact (λ c, (pr1 c,, F (pr1 c) (pr2 c))). - intros c c' f. exact f. - reflexivity. - reflexivity. Defined.
Require Import UniMath.MoreFoundations.Tactics.