Lemma isEpi_to_binop_BinDirectSum2 {x y z : A} (f : y --> x) (g : Epi A z x) (DS : BinDirectSum y z) : isEpi (to_binop _ _ (to_Pr1 DS · f) (to_Pr2 DS · g)). Proof. use make_isEpi. intros z0 g0 h X. use (EpiisEpi A g). assert (e : to_In2 DS · to_binop DS x (to_Pr1 DS · f) (to_Pr2 DS · g) · g0 = to_In2 DS · to_binop DS x (to_Pr1 DS · f) (to_Pr2 DS · g) · h). { rewrite <- assoc. rewrite <- assoc. rewrite X. apply idpath. } rewrite to_premor_linear' in e. rewrite assoc in e. rewrite assoc in e. rewrite to_Unel2' in e. rewrite ZeroArrow_comp_left in e. rewrite to_lunax'' in e. rewrite (to_IdIn2 DS) in e. rewrite id_left in e. apply e. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Algebra.Monoids. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Opp. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.BinDirectSums.