Definition is_sub_precategory {C : category} (C' : hsubtype C) (Cmor' : ∏ a b : C, hsubtype (a --> b)) := (∏ a : C, C' a -> Cmor' _ _ (identity a)) × (∏ (a b c : C) (f: a --> b) (g : b --> c), Cmor' _ _ f -> Cmor' _ _ g -> Cmor' _ _ (f · g)).
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.