proposition: Lemma comonoid_mor_in_eilenberg_moore {x y : sym_monoidal_cat_co_eilenberg_moore (linear_category_bang 𝕃)} (f : x --> y) : comonoid_mor_struct (sym_monoidal_cat_co_eilenberg_moore (linear_category_bang 𝕃)) (comonoid_in_eilenberg_moore_from_coalg 𝕃 x) (comonoid_in_eilenberg_moore_from_coalg 𝕃 y) f.
proof: Proof. use make_is_comonoid_mor. - use eq_mor_co_eilenberg_moore. cbn. unfold transported_comonoid_comult_data. cbn. refine (_ @ assoc' _ _ _). etrans. 2: { apply maponpaths_2. rewrite assoc. apply maponpaths_2. exact (pr21 f). } rewrite ! assoc'. apply maponpaths. etrans. 2: { rewrite assoc. apply maponpaths_2. exact (! linear_category_comult_nat (pr11 f)). } rewrite ! assoc'. apply maponpaths. rewrite tensor_mor_right. rewrite tensor_mor_left. etrans. { apply maponpaths. apply pathsinv0. apply tensor_split'. } refine (! tensor_comp_mor _ _ _ _ @ _). refine (_ @ tensor_comp_mor _ _ _ _). use two_arg_paths ; apply (! pr2 (disp_ε _) _ _ (pr11 f)). - use eq_mor_co_eilenberg_moore. refine (_ @ assoc' _ _ _). etrans. 2: { apply maponpaths_2. exact (pr21 f). } rewrite id_right. cbn. unfold transported_comonoid_counit_data. rewrite assoc'. apply maponpaths. exact (! linear_category_counit_nat (pr11 f)). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Retracts UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Monoidal.Adjunctions UniMath.CategoryTheory.Monoidal.FunctorCategories UniMath.CategoryTheory.Monoidal.Structure.Cartesian UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Closed UniMath.CategoryTheory.Monoidal.Structure.SymmetricDiagonal UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.Categories.Dialgebras UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors UniMath.CategoryTheory.Monoidal.Displayed.Monoidal UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal UniMath.CategoryTheory.Monoidal.Comonoids.Category UniMath.CategoryTheory.Monoidal.Comonoids.MonoidalCartesianBuilder UniMath.CategoryTheory.Monoidal.Comonoids.TransportComonoidAlongRetraction UniMath.CategoryTheory.Categories.CoEilenbergMoore UniMath.CategoryTheory.Monoidal.Examples.MonoidalDialgebras UniMath.CategoryTheory.Monoidal.Examples.SymmetricMonoidalCoEilenbergMoore UniMath.Semantics.LinearLogic.LinearCategory UniMath.Semantics.LinearLogic.LinearCategoryEilenbergMooreAdjunction UniMath.Semantics.LinearLogic.LinearNonLinear