Lemma pre_composition_with_ess_surj_is_faithful (p : essentially_surjective H) : faithful (pre_composition_functor A B C H). Proof. intros F G. apply isinclbetweensets. - apply isaset_nat_trans. apply C. - apply isaset_nat_trans. apply C. - simpl in *. intros gamma delta ex. apply nat_trans_eq. + apply C. + intro b. apply (p b (make_hProp _ (homset_property C _ _ _ _))). intro t; induction t as [a f]; simpl. apply (pre_comp_with_z_iso_is_inj (pr2(pr2(functor_on_z_iso _ f)))). cbn. do 2 rewrite nat_trans_ax. apply cancel_postcomposition. apply (nat_trans_eq_pointwise ex a). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering.