Proposition binary_coprod_algebra_arrow_in2 : binary_coprod_algebra_in2 · binary_coprod_algebra_arrow = φ₂. Proof. use subtypePath. { intro. apply homset_property. } enough (η M Y · (# 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 (BinCoproductIn2Commutes _ _ _ 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 hY). } apply monad_algebra_unit. 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.