proposition: Lemma faithful_1_from_comp {C C' C'' : category} (F : C ⟶ C') (F' : C' ⟶ C'') (H : faithful (functor_composite F F')) : faithful F.
proof: Proof. intros a b f g g'. pose (H _ _ (#F' f)). cbn in i. use make_iscontr. - apply subtypePath. { intro. apply homset_property. } exact (base_paths _ _ (pr1 (H _ _ _ (make_hfiber _ (pr1 g) (maponpaths #F' (pr2 g))) (make_hfiber _ (pr1 g') (maponpaths #F' (pr2 g')))))). - intro. refine (iscontrpr1 ((_ : isaset _) _ _ _ _)). apply isaset_hfiber; apply homset_property. 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