proposition: Lemma fully_faithful_sub_precategory_inclusion : fully_faithful (sub_precategory_inclusion C (full_sub_precategory C')).
proof: Proof. apply full_and_faithful_implies_fully_faithful. split. - apply full_sub_precategory_inclusion. - apply faithful_sub_precategory_inclusion. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Subcategory.Core