proposition: Lemma postcomp_with_section_reflect_coalg_mor (𝕃 : linear_category) (xx aa bb : sym_monoidal_cat_co_eilenberg_moore (linear_category_bang 𝕃)) (i : aa --> bb) (f : 𝕃⟦pr11 xx, pr11 aa⟧) (f_i_coalg : pr21 xx · #(linear_category_bang 𝕃) (f · pr11 i) = (f · pr11 i) · pr21 bb) (r : 𝕃⟦pr11 bb, pr11 aa⟧) (ir_id : is_retraction (pr11 i) r) : pr21 xx · #(linear_category_bang 𝕃) f = f · pr21 aa.
proof: Proof. pose (p := cancel_postcomposition _ _ (#(linear_category_bang 𝕃) r) f_i_coalg). rewrite assoc' in p. rewrite <- functor_comp in p. rewrite assoc' in p. refine (_ @ p @ _). - do 2 apply maponpaths. refine (! id_right _ @ _). apply maponpaths. apply pathsinv0, ir_id. - rewrite ! assoc'. apply maponpaths. rewrite assoc. etrans. { apply maponpaths_2. exact (! pr21 i). } rewrite assoc'. rewrite <- functor_comp. refine (_ @ id_right _). apply maponpaths. refine (_ @ functor_id (linear_category_bang 𝕃) _). apply maponpaths. exact ir_id. 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