Definition restrict_functor_to_sub_precategory {C D : category} (C' : sub_precategories C) (F : functor C D) : functor C' D. Proof. use make_functor. - use make_functor_data. + exact (F ∘ precategory_object_from_sub_precategory_object _ C')%functions. + intros ? ?. apply (# F ∘ precategory_morphism_from_sub_precategory_morphism _ C' _ _)%functions. - use make_dirprod. + intro; apply (functor_id F). + intros ? ? ? ? ?; apply (functor_comp F). Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos.