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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence.