Lemma faithful_1_from_comp {C C' C'' : category} (F : C ⟶ C') (F' : C' ⟶ C'') (H : faithful (functor_composite F F')) : faithful F. 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.
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.