proposition: Lemma dialgebra_disp_associator_data : disp_associator_data dialgebra_disp_tensor.
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Categories.Dialgebras 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.Monoidal.Displayed.MonoidalSections UniMath.CategoryTheory.Monoidal.Displayed.Symmetric UniMath.CategoryTheory.Monoidal.Displayed.MonoidalFunctorLifting UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.Monoidal.Structure.Symmetric