proposition: Lemma cartesian_monoidal_has_enough_comm_comonoids_mor_mult_diag {c1 c2 : V} (m1 : disp_cat_of_commutative_comonoids V c1) (m2 : disp_cat_of_commutative_comonoids V c2) (f : V ⟦ c1, c2 ⟧) : δ_{(_ ,, pr1 m1) : comonoid V} · f #⊗ f = f · δ_{(_ ,, pr1 m2) : comonoid V}.
proof: Proof. refine (_ @ cartesian_monoidal_has_enough_comonoids_mor_comult f @ _). -- apply maponpaths_2. apply comult_is_diag. -- apply maponpaths. apply pathsinv0, comult_is_diag. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.catiso UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Projection UniMath.CategoryTheory.DisplayedCats.CatIsoDisplayed UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Monoidal.Displayed.Monoidal UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal UniMath.CategoryTheory.Monoidal.Structure.Cartesian UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.SymmetricDiagonal UniMath.CategoryTheory.Monoidal.Comonoids.Category UniMath.CategoryTheory.Monoidal.Comonoids.Tensor UniMath.CategoryTheory.Monoidal.Comonoids.Monoidal UniMath.CategoryTheory.Monoidal.Comonoids.Symmetric