Lemma total_rightcompax {C : category} {D : disp_cat C} {M : monoidal C} (DT : disp_tensor D M) : bifunctor_rightcompax (total_tensor_data DT). Proof. intros y x1 x2 x3 f1 f2. use total2_paths_b. - exact (bifunctor_rightcomp (monoidal_tensor M) (pr1 y) (pr1 x1) (pr1 x2) (pr1 x3) (pr1 f1) (pr1 f2)). - exact (disp_bifunctor_rightcomp DT (pr1 x1) (pr1 x2) (pr1 x3) (pr1 y) (pr1 f1) (pr1 f2) (pr2 x1) (pr2 x2) (pr2 x3) (pr2 y) (pr2 f1) (pr2 f2)). Qed.
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.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Displayed.Monoidal. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Import BifunctorNotations. Import MonoidalNotations. Import DisplayedBifunctorNotations. Import DisplayedMonoidalNotations.