proposition: Proposition binary_coprod_algebra_arrow_in1 : binary_coprod_algebra_in1 · binary_coprod_algebra_arrow = φ₁.
proof: Proof. use subtypePath. { intro. apply homset_property. } enough (η M X · (# M (ι₁ · η M XY) · μ M XY · pr1 (CoequalizerArrow binary_coprod_algebra_ob)) · pr1 binary_coprod_algebra_arrow = pr1 φ₁) as p. { exact p. } rewrite !assoc'. etrans. { do 3 apply maponpaths. exact (maponpaths pr1 (CoequalizerCommutes binary_coprod_algebra_ob _ _ _)). } etrans. { apply maponpaths. rewrite !assoc. apply maponpaths_2. rewrite functor_comp. rewrite !assoc'. etrans. { apply maponpaths. exact (@Monad_law2 _ M XY). } apply id_right. } etrans. { apply maponpaths. pose (maponpaths pr1 (BinCoproductIn1Commutes _ _ _ S₁ Z (monad_free_alg_counit M alg_X · φ₁) (monad_free_alg_counit M alg_Y · φ₂))) as p. refine (_ @ p). refine (maponpaths (λ z, z · _) _). refine (!(id_right _) @ _). simpl. rewrite (functor_comp M). refine (_ @ assoc (#M ι₁) _ _). apply maponpaths. refine (!_). apply (Monad_law2(T:=M)). } refine (_ @ id_left _). refine (assoc _ _ _ @ _). apply maponpaths_2. simpl. rewrite (functor_id M). etrans. { apply maponpaths. exact (id_left hX). } apply monad_algebra_unit. 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