Definition is_precategory_sub_precategory (C : category)(C':sub_precategories C) : is_precategory (sub_precategory_data C C'). Proof. repeat split; simpl; intros. unfold sub_precategory_comp; apply eq_in_sub_precategory; simpl; apply id_left. apply eq_in_sub_precategory. simpl. apply id_right. apply eq_in_sub_precategory. cbn. apply assoc. apply eq_in_sub_precategory. cbn. apply assoc'. 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.