proposition: Lemma totalcategory_tensorfunctorid : tensorfunctor_id TtD.
proof: Proof. intros x y. use total2_paths_b. + apply tid. + apply (dtid (pr1 x) (pr1 y) (pr2 x) (pr2 y)). 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