proposition: Lemma comonoid_in_eilenberg_moore_from_coalg_comult_alg_mor : hx · #bang δ_{transport_comonoid_from_free 𝕃 xx} = δ_{transport_comonoid_from_free 𝕃 xx} · (hx #⊗ hx · mon_functor_tensor (_,,lax_monoidal_from_symmetric_monoidal_comonad 𝕃 (linear_category_bang 𝕃)) x x).
proof: Proof. assert (p : pr21 (xx ⊗ xx) = (hx #⊗ hx · mon_functor_tensor (_,,lax_monoidal_from_symmetric_monoidal_comonad 𝕃 (linear_category_bang 𝕃)) x x)). { refine (assoc' _ _ _ @ _). apply id_left. } rewrite <- p. assert (retr : is_retraction (hx #⊗ hx) (ε bang x #⊗ ε bang x)). { refine (! tensor_comp_mor _ _ _ _ @ _ @ tensor_id_id _ _). use two_arg_paths ; apply (pr2 xx). } use (lifting_is_coalg_mor (xx := xx) (aa := xx ⊗ xx) (bb := (eilenberg_moore_cofree 𝕃 x : EM) ⊗ (eilenberg_moore_cofree 𝕃 x : EM)) (g := (hx · linear_category_comult 𝕃 x ,, _) ,, tt) (i := (hx #⊗ hx,, _) ,, tt) (f := δ_{transport_comonoid_from_free 𝕃 xx}) (r := ε bang x #⊗ ε bang x) retr ). - cbn. unfold dialgebra_disp_tensor_op. cbn. rewrite id_left. rewrite ! assoc'. rewrite ! id_left. rewrite functor_comp. rewrite assoc. etrans. { apply maponpaths_2. exact (! pr22 xx). } etrans. 2: { apply maponpaths. apply pathsinv0. exact (assoc _ _ _ @ linear_category_comult_coalgebra_mor x). } apply assoc'. - cbn. unfold dialgebra_disp_tensor_op. cbn. rewrite ! id_left. etrans. { rewrite assoc'. apply maponpaths. apply pathsinv0. apply (tensor_mon_functor_tensor (_ ,, lax_monoidal_from_symmetric_monoidal_comonad _ bang) hx hx). } do 2 rewrite assoc. apply maponpaths_2. refine (! tensor_comp_mor _ _ _ _ @ _ @ tensor_comp_mor _ _ _ _). use two_arg_paths ; exact (! pr22 xx). - apply transport_comonoid_from_free_lem. 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