Lemma binary_coprod_algebra_in2_eq : μ M Y · #M(ι₂ · η M XY) · μ M XY · pr1 (CoequalizerArrow binary_coprod_algebra_ob) = #M (hY · η M Y) · μ M Y · #M(ι₂ · η M XY) · μ M XY · pr1 (CoequalizerArrow binary_coprod_algebra_ob). Proof. assert (BinCoproductIn2 S₂ · (l · CoequalizerArrow binary_coprod_algebra_ob) = BinCoproductIn2 S₂ · (r · CoequalizerArrow binary_coprod_algebra_ob)) as p. { exact (maponpaths (λ z, BinCoproductIn2 _ · z) (CoequalizerEqAr binary_coprod_algebra_ob)). } unfold l in p. unfold r in p. unfold binary_coprod_algebra_left_map in p. unfold binary_coprod_algebra_right_map in p. rewrite !assoc in p. rewrite !BinCoproductOfArrowsIn2 in p. assert (# M (identity (M Y)) · μ M Y · (# M (ι₂ · η M XY) · μ M XY) · pr1 (CoequalizerArrow binary_coprod_algebra_ob) = # M (# M (identity _) · hY · η M Y) · μ M Y · (# M (ι₂ · η M XY) · μ M XY) · pr1 (CoequalizerArrow binary_coprod_algebra_ob)) as q. { exact (maponpaths pr1 p). } rewrite !functor_id in q. rewrite !id_left in q. refine (_ @ q). rewrite !assoc'. apply idpath. 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.