proposition: Lemma monoidal_pointed_objects_disp_data_verif : disp_leftunitor_data monoidal_pointed_objects_disp_tensor (identity I_{Mon_V}) × disp_rightunitor_data monoidal_pointed_objects_disp_tensor (identity I_{Mon_V}) × disp_associator_data monoidal_pointed_objects_disp_tensor.
proof: Proof. split3. - intros v pv. cbn. unfold functoronmorphisms1. rewrite (bifunctor_rightid Mon_V). rewrite id_left. rewrite assoc'. rewrite monoidal_leftunitornat. rewrite assoc. rewrite (pr2 (monoidal_leftunitorisolaw Mon_V _)). apply id_left. - intros v pv. cbn. unfold functoronmorphisms1. rewrite (bifunctor_leftid Mon_V). rewrite id_right. rewrite assoc'. rewrite monoidal_rightunitornat. rewrite assoc. rewrite <- unitors_coincide_on_unit. rewrite (pr2 (monoidal_leftunitorisolaw Mon_V _)). apply id_left. - intros v w u pv pw pu. cbn. rewrite assoc'. apply maponpaths. unfold functoronmorphisms1. rewrite !(bifunctor_rightcomp Mon_V). rewrite !(bifunctor_leftcomp Mon_V). rewrite !assoc'. rewrite <- monoidal_associatornatleft. rewrite !assoc. apply cancel_postcomposition. rewrite !assoc'. rewrite <- (monoidal_associatornatleftright Mon_V). rewrite !assoc. apply cancel_postcomposition. apply (z_iso_inv_to_right _ _ _ _ (z_iso_from_associator_iso Mon_V _ _ _)). cbn. etrans. 2: { rewrite assoc'. apply maponpaths. apply pathsinv0, monoidal_triangle_identity_inv. } rewrite <- !(bifunctor_rightcomp Mon_V). apply maponpaths. rewrite unitorsinv_coincide_on_unit. apply monoidal_rightunitorinvnat. Qed.
imports: UniMath.MoreFoundations.All UniMath.Foundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Projection UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors UniMath.CategoryTheory.Monoidal.Displayed.Monoidal UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal UniMath.CategoryTheory.coslicecat