proposition: Lemma pre_composition_as_a_functor_data_is_fun (A B C : category) : is_functor (pre_composition_as_a_functor_data A B C).
proof: Proof. split. - intro H. apply (nat_trans_eq (homset_property _ )). intro G. cbn. apply post_whisker_identity; exact C. - intros H1 H2 H3 β β'. apply (nat_trans_eq (functor_category_has_homsets A C C)). intro G. cbn. apply post_whisker_composition; exact C. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors