Lemma KAExt_Comm2 (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) (h1 : hfiber # (ComplexHomotFunctor A) (MPMor1 (TriIsoInv (KADTriDataIso I1)) · g1 · MPMor1 (KADTriDataIso I2))) (h2 : hfiber # (ComplexHomotFunctor A) (MPMor2 (TriIsoInv (KADTriDataIso I1)) · g2 · MPMor2 (KADTriDataIso I2))) (I1' := hfiberpr1 # (ComplexHomotFunctor A) (KADTriDataMor I1) (KADTriDataFiber I1)) (I2' := hfiberpr1 # (ComplexHomotFunctor A) (KADTriDataMor I2) (KADTriDataFiber I2)) (h1' := hfiberpr1 # (ComplexHomotFunctor A) (is_z_isomorphism_mor (TriMor_is_iso1 (KADTriDataIso I1)) · g1 · MPMor1 (KADTriDataIso I2)) h1) (h2' := hfiberpr1 # (ComplexHomotFunctor A) (is_z_isomorphism_mor (TriMor_is_iso2 (KADTriDataIso I1)) · g2 · MPMor2 (KADTriDataIso I2)) h2) (HH1 : ComplexHomot A (Source (KADTriDataMor I1)) (Ob2 (MappingConeTri (KADTriDataMor I2) (KADTriDataFiber I2)))) (HH2 : ComplexHomotMorphism A HH1 = @to_binop (ComplexPreCat_Additive A) (Source (KADTriDataMor I1)) (Ob2 (MappingConeTri (KADTriDataMor I2) (KADTriDataFiber I2))) (I1' · h2') (to_inv (h1' · I2'))) : # (ComplexHomotFunctor A) (MappingConeIn2 A I1') · # (ComplexHomotFunctor A) (MappingConeMorExt A I1' I2' h1' h2' HH1 (! HH2)) = (is_z_isomorphism_mor (TriMor_is_iso2 (KADTriDataIso I1))) · g2 · MPMor2 (KADTriDataIso I2) · # (ComplexHomotFunctor A) (MappingConeIn2 A I2'). Proof. set (tmp := hfiberpr2 _ _ h2). apply (maponpaths (postcompose (Mor2 (MappingConeTri (KADTriDataMor I2) (KADTriDataFiber I2))))) in tmp. use (pathscomp0 _ tmp). clear tmp. cbn. unfold postcompose. use (pathscomp0 (! (functor_comp (ComplexHomotFunctor A) _ _))). use (pathscomp0 _ (functor_comp (ComplexHomotFunctor A) _ _)). apply maponpaths. exact (MappingConeMorExtComm1 A I1' I2' h1' h2' HH1 (! HH2)). 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.