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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence.