proposition: Lemma pre_composition_with_ess_surj_is_faithful (p : essentially_surjective H) : faithful (pre_composition_functor A B C H).
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering