Proposition binary_coprod_algebra_section_right_map : s · r = identity _. Proof. unfold s, r. use BinCoproductArrowsEq. - rewrite id_right. rewrite !assoc. unfold binary_coprod_algebra_section. rewrite BinCoproductOfArrowsIn1. rewrite !assoc'. unfold binary_coprod_algebra_right_map. rewrite BinCoproductOfArrowsIn1. rewrite !assoc. refine (_ @ id_left _). apply maponpaths_2. rewrite <- (functor_comp F). refine (_ @ functor_id F _). apply maponpaths. exact (triangle_id_right_ad (pr2 (monad_underlying_is_right_adjoint M)) alg_X). - rewrite id_right. rewrite !assoc. unfold binary_coprod_algebra_section. rewrite BinCoproductOfArrowsIn2. rewrite !assoc'. unfold binary_coprod_algebra_right_map. rewrite BinCoproductOfArrowsIn2. rewrite !assoc. refine (_ @ id_left _). apply maponpaths_2. rewrite <- (functor_comp F). refine (_ @ functor_id F _). apply maponpaths. exact (triangle_id_right_ad (pr2 (monad_underlying_is_right_adjoint M)) alg_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.