Definition functor_ru_composition {ruC : right_unitor TC IC} {ruD : right_unitor TD ID} {ruE : right_unitor TE IE} {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_ru_disp_cat ruC ruD (_,,FF)) (GGG : functor_ru_disp_cat ruD ruE (_,,GG)) : functor_ru_disp_cat ruC ruE (_,, functor_tensorunit_composition FF GG).
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.