Lemma TriangulatedFiveLemma {D1 D2 : @DTri PT} (M : TriMor D1 D2) (H1 : is_z_isomorphism (MPMor1 M)) (H2 : is_z_isomorphism (MPMor2 M)) : is_z_isomorphism (MPMor3 M). Proof. set (Mor1 := TriangulatedMorphism_from_object M (Ob3 D2)). set (Mor2 := TriangulatedMorphism_to_object M (Ob3 D1)). assert (e1 : is_z_isomorphism (@FMor3 abgr_Abelian _ _ Mor1)). { use FiveLemma. - exact (@abgr_Additive_is_iso_postmor PT _ _ _ _ H1). - exact (@abgr_Additive_is_iso_postmor PT _ _ _ _ H2). - exact (abgr_Additive_is_iso_postmor (Ob3 D2) _ _ (functor_on_is_z_isomorphism (AddEquiv1 (@Trans PT)) H1)). - exact (abgr_Additive_is_iso_postmor (Ob3 D2) _ _ (functor_on_is_z_isomorphism (AddEquiv1 (@Trans PT)) H2)). } assert (e2 : is_z_isomorphism (@FMor3 abgr_Abelian _ _ Mor2)). { use FiveLemma. - exact (abgr_Additive_is_iso_premor _ _ (Ob3 D1) (functor_on_is_z_isomorphism (AddEquiv1 (@Trans PT)) H2)). - exact (abgr_Additive_is_iso_premor _ _ (Ob3 D1) (functor_on_is_z_isomorphism (AddEquiv1 (@Trans PT)) H1)). - exact (@abgr_Additive_is_iso_premor PT _ _ _ _ H2). - exact (@abgr_Additive_is_iso_premor PT _ _ _ _ H1). } exact (@abgr_Additive_premor_postmor_is_iso PT _ _ (MPMor3 M) e2 e1). Qed.
Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. 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.Pushouts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.BinDirectSums. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Abelian. Require Import UniMath.CategoryTheory.ShortExactSequences. Require Import UniMath.CategoryTheory.Categories.Abgr. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.Morphisms. Require Import UniMath.CategoryTheory.AdditiveFunctors. Require Import UniMath.CategoryTheory.FiveLemma.