Lemma KAExt_Comm1 (D1 D2 : DTri) (g1 : KAPreTriangData ⟦ Ob1 D1, Ob1 D2 ⟧) (g2 : KAPreTriangData ⟦ Ob2 D1, Ob2 D2 ⟧) (H : g1 · Mor1 D2 = Mor1 D1 · g2) (I1 : KADTriData D1) (I2 : KADTriData D2) : (MPMor1 (TriIsoInv (KADTriDataIso I1))) · g1 · (MPMor1 (KADTriDataIso I2)) · (KADTriDataMor I2) = (KADTriDataMor I1) · (MPMor2 (TriIsoInv (KADTriDataIso I1))) · g2 · (MPMor2 (KADTriDataIso I2)). Proof. set (tmp := MPComm1 (TriIsoInv (KADTriDataIso I1))). apply (maponpaths (postcompose (g2 · MPMor2 (KADTriDataIso I2)))) in tmp. unfold postcompose in tmp. rewrite assoc in tmp. rewrite assoc in tmp. use (pathscomp0 _ tmp). clear tmp. rewrite <- (assoc (MPMor1 (TriIsoInv (KADTriDataIso I1)))). rewrite <- (assoc (MPMor1 (TriIsoInv (KADTriDataIso I1)))). rewrite <- (assoc (MPMor1 (TriIsoInv (KADTriDataIso I1)))). rewrite <- (assoc (MPMor1 (TriIsoInv (KADTriDataIso I1)))). apply cancel_precomposition. apply (maponpaths (postcompose (MPMor2 (KADTriDataIso I2)))) in H. unfold postcompose in H. use (pathscomp0 _ H). clear H. rewrite <- (assoc g1). rewrite <- (assoc g1). apply cancel_precomposition. exact (MPComm1 (KADTriDataIso I2)). 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.Equivalences.Core. 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.HomologicalAlgebra.Complexes. Require Import UniMath.HomologicalAlgebra.Triangulated. Require Import UniMath.HomologicalAlgebra.KA. Require Import UniMath.HomologicalAlgebra.TranslationFunctors. Require Import UniMath.HomologicalAlgebra.MappingCone.