Definition monoidal_dialgebra_lifting_to_monoidal_nat_trans : is_mon_nat_trans (comp_fmonoidal Km Fm) (comp_fmonoidal Km Gm) α. Proof. split. - intros x y. cbn. etrans. { rewrite assoc'. apply maponpaths. exact (! pr11 Fl x y). } cbn. do 2 rewrite assoc. apply maponpaths_2. unfold dialgebra_disp_tensor_op. cbn. do 2 rewrite assoc. etrans. { do 2 apply maponpaths_2. apply (fmonoidal_preservestensorstrongly Fm (K x) (K y)). } rewrite assoc'. apply id_left. - red. cbn. etrans. { rewrite assoc'. apply maponpaths. exact (! pr21 Fl). } rewrite assoc. apply maponpaths_2. cbn. unfold dialgebra_disp_unit. rewrite assoc. etrans. { apply maponpaths_2. apply (fmonoidal_preservesunitstrongly Fm). } apply id_left. Qed. End MonoidalDialgebraLiftingToNatTrans. Section RoundtripForLiftingData. Context {C1 C2 C3 : category} {M1 : monoidal C1} {M2 : monoidal C2} {M3 : monoidal C3} {F G : C2 ⟶ C3} {Fm : fmonoidal M2 M3 F} {Gm : fmonoidal M2 M3 G} {K : C1 ⟶ C2} {Km : fmonoidal M1 M2 K}. Local Definition source_type': UU := ∑ α : K ∙ F ⟹ K ∙ G, is_mon_nat_trans (comp_fmonoidal Km Fm) (comp_fmonoidal Km Gm) α. Local Definition target_type': UU := ∑ fl : functor_lifting (dialgebra_disp_cat F G) K, flmonoidal_lax Km (dialgebra_disp_monoidal Fm Gm) fl. Local Definition target_type_s': UU := ∑ fl : functor_lifting (dialgebra_disp_cat F G) K, flmonoidal Km (dialgebra_disp_monoidal Fm Gm) fl (pr2 Km). Local Definition source_to_target' : source_type' -> target_type' := λ α, _ ,, monoidal_nat_trans_to_dialgebra_lifting (pr2 α). Local Definition target_to_source' : target_type' -> source_type' := λ fl, _ ,, monoidal_dialgebra_lifting_to_monoidal_nat_trans (pr2 fl). Local Definition source_to_target_s' : source_type' -> target_type_s'. Proof. intro α. use tpair. 2: apply (monoidal_nat_trans_to_dialgebra_lifting_strong (pr2 α)). Defined.
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.