Definition pre_composition_as_a_functor_data (A B C: category) : functor_data [A , B] [[B, C], [A, C]]. Proof. use make_functor_data. - apply pre_composition_functor. - intros H1 H2 η. use make_nat_trans. + intro G. cbn. exact (# (post_comp_functor G) η). + intros G G' β. etrans. apply pathsinv0, functorial_composition_pre_post. apply functorial_composition_post_pre. Defined.
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.