Lemma total_leftcompax {C : category} {D : disp_cat C} {M : monoidal C} (DT : disp_tensor D M) : bifunctor_leftcompax (total_tensor_data DT). Proof. intros x y1 y2 y3 g1 g2. use total2_paths_b. - exact (bifunctor_leftcomp (monoidal_tensor M) (pr1 x) (pr1 y1) (pr1 y2) (pr1 y3) (pr1 g1) (pr1 g2)). - exact (disp_bifunctor_leftcomp DT (pr1 x) (pr1 y1) (pr1 y2) (pr1 y3) (pr1 g1) (pr1 g2) (pr2 x) (pr2 y1) (pr2 y2) (pr2 y3) (pr2 g1) (pr2 g2)). 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.