proposition: 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: 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.
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