proposition: Lemma ff_is_inclusion_on_objects {C D : category} (HC : is_univalent C) (HD : is_univalent D) (F : functor C D) (HF : fully_faithful F) : isofhlevelf 1 (functor_on_objects F).
proof: Proof. intro d. apply invproofirrelevance. intros [c e] [c' e']. use total2_paths_f. - simpl. set (X := idtoiso (e @ ! e')). set (X2 := iso_from_fully_faithful_reflection HF X). apply (isotoid _ HC X2). - simpl. set (T:=@functtransportf _ _ (functor_on_objects F)). set (T' := T (λ c, c = d)). simpl in T'. rewrite T'. rewrite (maponpaths_isotoid _ _ _ HC HD). rewrite functor_on_iso_iso_from_ff_reflection. rewrite isotoid_idtoiso. rewrite transportf_id2. rewrite pathscomp_inv. rewrite pathsinv0inv0. rewrite <- path_assoc. rewrite pathsinv0l. apply pathscomp0rid. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Univalence UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Univalence