proposition: Lemma is_functor_composite {C C' C'' : precategory_data} (F : functor C C') (F' : functor C' C'') : is_functor ( functor_composite_data F F' ) .
proof: Proof. split; simpl. intro a. assert ( e1 := functor_id F a ) . assert ( e2 := functor_id F' ( F a ) ) . apply ( ( maponpaths ( # F' ) e1 ) @ e2 ) . unfold functor_compax . intros . assert ( e1 := functor_comp F f g ) . assert ( e2 := functor_comp F' ( # F f ) ( # F g ) ) . apply ( ( maponpaths ( # F' ) e1 ) @ e2 ) . Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Univalence UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Univalence