proposition: Lemma FiveLemma {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)) : is_z_isomorphism (FMor3 (A:=A) FRM).
proof: Proof. use monic_epi_is_iso. - use FiveLemma_isMonic. + exact H1. + exact H2. + exact H4. + exact H5. - use FiveLemma_isEpi. + exact H1. + exact H2. + exact H4. + exact H5. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Morphisms UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Abelian UniMath.CategoryTheory.AbelianToAdditive UniMath.CategoryTheory.AbelianPushoutPullback UniMath.CategoryTheory.ShortExactSequences UniMath.CategoryTheory.PseudoElements UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.BinDirectSums