Proposition binary_coprod_algebra_arrow_in1 : binary_coprod_algebra_in1 · binary_coprod_algebra_arrow = φ₁. 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.
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.