Proposition binary_coprod_algebra_section_left_map : s · l = identity _. 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure. Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.AlgebraStructures. Require Import UniMath.CategoryTheory.Monads.Monads.