proposition: Lemma comonoid_in_eilenberg_moore_from_coalg_counit_alg_mor : hx · #bang ε_{transport_comonoid_from_free 𝕃 xx} = ε_{transport_comonoid_from_free 𝕃 xx} · mon_functor_unit (_,, lax_monoidal_from_symmetric_monoidal_comonad 𝕃 bang).
proof: Proof. cbn. unfold transported_comonoid_counit_data. rewrite functor_comp. rewrite assoc. etrans. { apply maponpaths_2. apply pathsinv0. exact (pr22 xx). } do 2 rewrite assoc'. apply maponpaths. apply pathsinv0. apply linear_category_counit_coalgebra_mor. 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