Lemma DExtIso_Comm2 {PT : PreTriangData} {D1 D2 : DTri} (D1' D2' : Tri) (I1 : TriIso D1 D1') (I2 : TriIso D2 D2') {f1 : Ob1 D1 --> Ob1 D2} {f2 : Ob2 D1 --> Ob2 D2} (H : f1 · Mor1 D2 = Mor1 D1 · f2) (h : Ob3 D1' --> Ob3 D2') (comm1 : Mor2 D1' · h = MPMor2 (TriIsoInv I1) · f2 · MPMor2 I2 · Mor2 D2') (comm2 : Mor3 D1' · (# (AddEquiv1 (@Trans PT)) (MPMor1 (TriIsoInv I1) · f1 · MPMor1 I2)) = h · Mor3 D2') : Mor3 D1 · # (AddEquiv1 Trans) f1 = MPMor3 I1 · h · MPMor3 (TriIsoInv I2) · Mor3 D2. Proof. rewrite functor_comp in comm2. rewrite functor_comp in comm2. rewrite assoc in comm2. rewrite assoc in comm2. rewrite <- (DComm3 (TriIsoInv I1)) in comm2. rewrite <- assoc. rewrite (DComm3 (TriIsoInv I2)). use (pre_comp_with_z_iso_inv_is_inj (TriMor_is_iso3 I1)). use (post_comp_with_z_iso_is_inj (functor_on_is_z_isomorphism (AddEquiv1 Trans) (TriMor_is_iso1 I2))). rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- functor_comp. rewrite <- functor_comp. cbn. rewrite (is_inverse_in_precat2 (TriMor_is_iso1 I2)). rewrite functor_id. rewrite id_right. rewrite assoc. rewrite assoc. rewrite assoc. rewrite (is_inverse_in_precat2 (TriMor_is_iso3 I1)). rewrite id_left. rewrite <- comm2. rewrite functor_comp. rewrite assoc. apply idpath. 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.