proposition: Proposition nat_equiv_faithful {A B : Type} {F G : A -> B} `{Is1Functor _ _ F} `{!Is0Functor G, !Is1Functor G} `{!HasEquivs B} (tau : NatEquiv F G) : Faithful F -> Faithful G.
proof: Proof. intros faithful_F x y f g eq_Gf_Gg. apply (@fmap _ _ _ _ _ (is0functor_precomp _ _ _ (cat_equiv_natequiv tau x))) in eq_Gf_Gg. cbn in eq_Gf_Gg. unfold cat_precomp in eq_Gf_Gg. rewrite <- is1natural_natequiv in eq_Gf_Gg. rewrite <- is1natural_natequiv in eq_Gf_Gg. apply faithful_F. assert (X : RetractionOf (tau y)). { unshelve eapply Build_RetractionOf. - exact ((tau y)^-1$). - exact (cate_issect _ ). } apply IsMonic_HasRetraction in X. apply X in eq_Gf_Gg. assumption. Defined.
imports: HoTT(Basics.Overture Basics.Tactics) HoTT(Types.Forall) HoTT(WildCat.Core WildCat.Bifunctor WildCat.Prod WildCat.NatTrans WildCat.Equiv)