Lemma projection_tensornaturality : tensor_preserving_data_is_natural ToD C totalcategory_monoidalcatdata MC π projection_tensorpreservingdata. Proof. intros xx yy zz ww ff' gg'. exact ((pr1 (pr1 (pr2 (pr1 C))) _ _ (pr1 ff' ⊗^{T} pr1 gg')) @ (pathsinv0 (pr2 (pr1 (pr2 (pr1 C))) _ _ (pr1 ff' ⊗^{T} pr1 gg')))). 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.Monoidal.AlternativeDefinitions.MonoidalCategoriesCurried. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.DisplayedMonoidalCurried. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsCurried. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Total.