proposition: Proposition binary_coprod_algebra_section_left_map : s · l = identity _.
proof: Proof. unfold s, l. use BinCoproductArrowsEq. - rewrite id_right. rewrite !assoc. unfold binary_coprod_algebra_section. rewrite BinCoproductOfArrowsIn1. rewrite !assoc'. unfold binary_coprod_algebra_left_map. rewrite BinCoproductOfArrowsIn1. rewrite !assoc. refine (_ @ id_left _). apply maponpaths_2. exact (triangle_id_left_ad (pr2 (monad_underlying_is_right_adjoint M)) X). - rewrite id_right. rewrite !assoc. unfold binary_coprod_algebra_section. rewrite BinCoproductOfArrowsIn2. rewrite !assoc'. unfold binary_coprod_algebra_left_map. rewrite BinCoproductOfArrowsIn2. rewrite !assoc. refine (_ @ id_left _). apply maponpaths_2. exact (triangle_id_left_ad (pr2 (monad_underlying_is_right_adjoint M)) Y). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Categories.HSET.All UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits UniMath.CategoryTheory.DisplayedCats.Examples.AlgebraStructures UniMath.CategoryTheory.Monads.Monads