Lemma pre_composition_is_functor (A B C : category) (H : [A, B]) : is_functor (pre_composition_functor_data A B C H). Proof. split; simpl in *. - unfold functor_idax . intros. apply pre_whisker_identity. - unfold functor_compax . intros. apply pre_whisker_composition. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory.