Definition functor_monoidal_composition {luC : left_unitor TC IC} {luD : left_unitor TD ID} {luE : left_unitor TE IE} {ruC : right_unitor TC IC} {ruD : right_unitor TD ID} {ruE : right_unitor TE IE} {αC : associator TC} {αD : associator TD} {αE : associator TE} {F : functor C D} {G : functor D E} {FF : functor_tensorunit_disp_cat TC TD IC ID F} {GG : functor_tensorunit_disp_cat TD TE ID IE G} (FFF : functor_monoidal_disp_cat luC luD ruC ruD αC αD (_,,FF)) (GGG : functor_monoidal_disp_cat luD luE ruD ruE αD αE (_,,GG)) : functor_monoidal_disp_cat luC luE ruC ruE αC αE (_,, functor_tensorunit_composition FF GG). Proof. repeat split. - use functor_lu_composition. exact luD. exact (pr11 FFF). exact (pr11 GGG). - use functor_ru_composition. exact ruD. exact (pr21 FFF). exact (pr21 GGG). - use functor_ass_composition. exact αD. exact (pr2 FFF). exact (pr2 GGG). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. 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.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored.