proposition: Lemma totalcategory_tensorfunctorcomp : tensorfunctor_comp TtD.
proof: Proof. intros x y x' y' x'' y'' f f' g g'. use total2_paths_b. + use tcomp. + use (((dtcomp (pr1 x) (pr1 y) (pr1 x') (pr1 y') (pr1 x'') (pr1 y'') (pr2 x) (pr2 y) (pr2 x') (pr2 y') (pr2 x'') (pr2 y'') (pr1 f) (pr1 g) (pr1 f') (pr1 g') (pr2 f) (pr2 g) (pr2 f') (pr2 g')))). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesCurried UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.DisplayedMonoidalCurried UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsCurried UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Total