Lemma projection_preservesassociativity : preserves_associativity ToD C totalcategory_monoidalcatdata MC π projection_tensorpreservingdata. Proof. intros xx yy zz. rewrite (pr1 (pr1 (pr2 (pr1 C)))). rewrite (pr2 (pr1 (pr2 (pr1 C)))). rewrite tid. rewrite tid. rewrite (pr1 (pr1 (pr2 (pr1 C)))). rewrite (pr2 (pr1 (pr2 (pr1 C)))). apply idpath. 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.