fact: Definition make_disp_monoidal_groupoidal {C : category} {D : disp_cat C} (gdisp : groupoidal_disp_cat D) {M : monoidal C} (DT : disp_tensor D M) (i : D I_{M}) (dlu : disp_leftunitor_data DT i) (dru : disp_rightunitor_data DT i) (dα : disp_associator_data DT) : let DMD := make_disp_monoidal_data_groupoidal D gdisp M DT i dlu dru dα in ∏ (dlu_nat : disp_leftunitor_nat dlu_{DMD}) (dru_nat : disp_rightunitor_nat dru_{DMD}) (dα_nat_left : disp_associator_nat_leftwhisker dα_{DMD}) (dα_nat_right : disp_associator_nat_rightwhisker dα_{DMD}) (dα_nat_left_right : disp_associator_nat_leftrightwhisker dα_{DMD}) (dtriangle : disp_triangle_identity dlu_{DMD} dru_{DMD} dα_{DMD}) (dpentagon : disp_pentagon_identity dα_{DMD}), disp_monoidal D M.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Projection UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.NaturalTransformations