Definition precategory_object_in_subcat {C : category} {C':sub_precategories C} (a : ob C) (p : sub_precategory_predicate_objects C' a) : ob C' := tpair _ a p.
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.