Lemma dialgebra_disp_associator_data : disp_associator_data dialgebra_disp_tensor. Proof. intros a1 a2 a3 f1 f2 f3. cbn. unfold dialgebra_disp_tensor_op. etrans. { rewrite (bifunctor_equalwhiskers W). unfold functoronmorphisms2. rewrite bifunctor_rightcomp. repeat rewrite assoc'. do 3 apply maponpaths. rewrite assoc. apply fmonoidal_preservesassociativity. } repeat rewrite assoc. apply cancel_postcomposition. etrans. 2: { unfold functoronmorphisms1 at 1. rewrite (bifunctor_leftcomp W). apply idpath. } repeat rewrite assoc. apply cancel_postcomposition. rewrite bifunctor_leftcomp. rewrite bifunctor_rightcomp. etrans. { apply cancel_postcomposition. rewrite assoc. apply cancel_postcomposition. rewrite assoc'. apply maponpaths. apply pathsinv0, bifunctor_equalwhiskers. } unfold functoronmorphisms1 at 1. repeat rewrite assoc'. apply (z_iso_inv_on_right _ _ _ (_,,fmonoidal_preservestensorstrongly Fm _ _)). cbn. transparent assert (aux1 : (z_iso (F (a1 ⊗_{V} a2) ⊗_{W} F a3) ((F a1 ⊗_{W} F a2) ⊗_{W} F a3))). { exists (pr1 (fmonoidal_preservestensorstrongly Fm a1 a2) ⊗^{W}_{r} F a3). exists (fmonoidal_preservestensordata Fm a1 a2 ⊗^{W}_{r} F a3). split. - rewrite <- (bifunctor_rightcomp W). etrans. { apply maponpaths. apply (z_iso_after_z_iso_inv (_,,fmonoidal_preservestensorstrongly Fm a1 a2)). } apply (bifunctor_rightid W). - rewrite <- (bifunctor_rightcomp W). etrans. { apply maponpaths. apply (z_iso_inv_after_z_iso (_,,fmonoidal_preservestensorstrongly Fm a1 a2)). } apply (bifunctor_rightid W). } apply pathsinv0, (z_iso_inv_to_left _ _ _ aux1). cbn. clear aux1. etrans. { repeat rewrite assoc. do 4 apply cancel_postcomposition. apply fmonoidal_preservesassociativity. } etrans. { repeat rewrite assoc. do 3 apply cancel_postcomposition. repeat rewrite assoc'. do 2 apply maponpaths. apply (z_iso_inv_after_z_iso (_,,fmonoidal_preservestensorstrongly Fm a1 _)). } rewrite id_right. etrans. 2: { rewrite assoc. apply cancel_postcomposition. apply (bifunctor_equalwhiskers W). } etrans; [| apply (associator_nat2 W)]. repeat rewrite assoc'. apply maponpaths. unfold functoronmorphisms1 at 2. repeat rewrite assoc. apply cancel_postcomposition. transparent assert (aux2 : (z_iso (G a1 ⊗_{W} F (a2 ⊗_{V} a3)) (G a1 ⊗_{W} (F a2 ⊗_{W} F a3)))). { exists (G a1 ⊗^{W}_{l} pr1 (fmonoidal_preservestensorstrongly Fm a2 a3)). exists (G a1 ⊗^{W}_{l} fmonoidal_preservestensordata Fm a2 a3). split. - rewrite <- (bifunctor_leftcomp W). etrans. { apply maponpaths. apply (z_iso_after_z_iso_inv (_,,fmonoidal_preservestensorstrongly Fm a2 a3)). } apply (bifunctor_leftid W). - rewrite <- (bifunctor_leftcomp W). etrans. { apply maponpaths. apply (z_iso_inv_after_z_iso (_,,fmonoidal_preservestensorstrongly Fm a2 a3)). } apply (bifunctor_leftid W). } apply (z_iso_inv_to_right _ _ _ _ aux2). cbn. clear aux2. apply pathsinv0, (bifunctor_equalwhiskers W). 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.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Categories.Dialgebras. 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.Monoidal.Displayed.MonoidalSections. Require Import UniMath.CategoryTheory.Monoidal.Displayed.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Displayed.MonoidalFunctorLifting. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Import BifunctorNotations. Import MonoidalNotations. Import DisplayedBifunctorNotations. Import DisplayedMonoidalNotations. Section FromMonoidalSection. End FromMonoidalSection.