proposition: Lemma monoidal_nat_trans_to_dialgebra_lifting_stronglaws : fl_stronglaws Km (dialgebra_disp_monoidal Fm Gm) (nat_trans_to_dialgebra_lifting K α) monoidal_nat_trans_to_dialgebra_lifting (pr2 Km).
proof: Proof. split. - intros x y. use tpair. + cbn. transparent assert (pfG_is_z_iso : (is_z_isomorphism ( (# G)%cat (inv_from_z_iso (fmonoidal_preservestensordata Km x y,, fmonoidal_preservestensorstrongly (_,, pr2 Km) x y))))). { use functor_on_is_z_isomorphism. apply is_z_iso_inv_from_z_iso. } use (z_iso_inv_to_right _ _ _ _ (_ ,, pfG_is_z_iso)). transparent assert (pfF_is_z_iso : (is_z_isomorphism ((# F)%cat (inv_from_z_iso (fmonoidal_preservestensordata Km x y,, fmonoidal_preservestensorstrongly (_,, pr2 Km) x y))))). { use functor_on_is_z_isomorphism. apply is_z_iso_inv_from_z_iso. } rewrite assoc'. use (z_iso_inv_to_left _ _ _ (_ ,, pfF_is_z_iso)). exact (! pr1 monoidal_nat_trans_to_dialgebra_lifting_data x y). + repeat (apply funextsec ; intro). split ; apply base_disp_cells_isaprop. - use tpair. + cbn. transparent assert (pfL_is_z_iso : (is_z_isomorphism ( (# F)%cat (inv_from_z_iso (fmonoidal_preservesunit Km,, fmonoidal_preservesunitstrongly (_ ,, pr2 Km))))) ). { use functor_on_is_z_isomorphism. apply is_z_iso_inv_from_z_iso. } use (z_iso_inv_to_left _ _ _ (_ ,, pfL_is_z_iso)). transparent assert (pfR_is_z_iso : (is_z_isomorphism ((# G)%cat (inv_from_z_iso (fmonoidal_preservesunit Km,, fmonoidal_preservesunitstrongly (_,, pr2 Km)))))). { use functor_on_is_z_isomorphism. apply is_z_iso_inv_from_z_iso. } rewrite assoc. use (z_iso_inv_to_right _ _ _ _ (_ ,, pfR_is_z_iso)). exact (! pr2 monoidal_nat_trans_to_dialgebra_lifting_data). + split ; apply base_disp_cells_isaprop. 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