Definition sub_precategory_ob_mor (C : category)(C':sub_precategories C) : precategory_ob_mor. Proof. exists (sub_ob C'). exact (λ a b, @sub_precategory_morphisms _ C' a b). 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.