Definition sub_precategory_inclusion_data (C : category) (C':sub_precategories C): functor_data C' C. Proof. exists (@pr1 _ _ ). intros a b. exact (@pr1 _ _ ). 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.