Definition sub_precategory_data (C : category)(C':sub_precategories C) : precategory_data. Proof. exists (sub_precategory_ob_mor C C'). split. intro c. exists (identity (C:=C) (pr1 c)). apply sub_precategory_id. apply (pr2 c). intros a b c f g. exists (compose (pr1 f) (pr1 g)). apply sub_precategory_comp. apply (pr2 f). apply (pr2 g). 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.