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. 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.
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.