Lemma total_functoronmorphisms_are_equal {C : category} {D : disp_cat C} {M : monoidal C} (DT : disp_tensor D M) : functoronmorphisms_are_equal (total_tensor_data DT). Proof. intros x1 x2 y1 y2 f g. use total2_paths_b. - exact (bifunctor_equalwhiskers (monoidal_tensor M) (pr1 x1) (pr1 x2) (pr1 y1) (pr1 y2) (pr1 f) (pr1 g)). - exact (disp_bifunctor_equalwhiskers DT (pr1 x1) (pr1 x2) (pr1 y1) (pr1 y2) (pr1 f) (pr1 g) (pr2 x1) (pr2 x2) (pr2 y1) (pr2 y2) (pr2 f) (pr2 g)). 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.