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. 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Foundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Projection. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Displayed.Monoidal. Require Import UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal. Require Import UniMath.CategoryTheory.coslicecat. Import BifunctorNotations. Import MonoidalNotations.