Definition functor_composite_data {C C' C'' : precategory_ob_mor } (F : functor_data C C') (F' : functor_data C' C'') : functor_data C C'' := functor_data_constr C C'' (λ a, F' (F a)) (λ (a b : ob C) f, #F' (#F f)) .
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.