Lemma FiveLemma_isEpi {FR1 FR2 : FiveRow} (FRM : FiveRowMorphism FR1 FR2) (H1 : is_z_isomorphism (FMor1 FRM)) (H2 : is_z_isomorphism (FMor2 FRM)) (H4 : is_z_isomorphism (FMor4 FRM)) (H5 : is_z_isomorphism (FMor5 FRM)) : isEpi (FMor3 (A:=A) FRM). Proof. use opp_isMonic. set (H1' := opp_is_z_isomorphism _ H1). set (H2' := opp_is_z_isomorphism _ H2). set (H4' := opp_is_z_isomorphism _ H4). set (H5' := opp_is_z_isomorphism _ H5). set (FRM' := FiveRowMorphism_opp FRM). exact (FiveLemma_isMonic FRM' H5' H4' H2' H1'). Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Pushouts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Opp. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Morphisms. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.Abelian. Require Import UniMath.CategoryTheory.AbelianToAdditive. Require Import UniMath.CategoryTheory.AbelianPushoutPullback. Require Import UniMath.CategoryTheory.ShortExactSequences. Require Import UniMath.CategoryTheory.PseudoElements. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Limits.Kernels. Require Import UniMath.CategoryTheory.Limits.Cokernels. Require Import UniMath.CategoryTheory.Limits.BinDirectSums.