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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors.