Lemma KAExt : ∏ (D1 D2 : DTri) (g1 : KAPreTriangData ⟦ Ob1 D1, Ob1 D2 ⟧) (g2 : KAPreTriangData ⟦ Ob2 D1, Ob2 D2 ⟧) (H : g1 · Mor1 D2 = Mor1 D1 · g2), ∥ TExt H ∥. Proof. intros D1 D2 g1 g2 H. use (squash_to_prop (DTriisDTri D1) (propproperty _)). intros I1. set (I1' := hfiberpr1 _ _ (KADTriDataFiber I1)). use (squash_to_prop (DTriisDTri D2) (propproperty _)). intros I2. set (I2' := hfiberpr1 _ _ (KADTriDataFiber I2)). set (φ1 := (MPMor1 (TriIsoInv (KADTriDataIso I1)) · g1 · MPMor1 (KADTriDataIso I2))). set (φ2 := (MPMor2 (TriIsoInv (KADTriDataIso I1)) · g2 · MPMor2 (KADTriDataIso I2))). use (squash_to_prop (ComplexHomotFunctor_issurj A φ1) (propproperty _)). intros φ1'. use (squash_to_prop (ComplexHomotFunctor_issurj A φ2) (propproperty _)). intros φ2'. use (squash_to_prop (ComplexHomotFunctor_im_to_homot A _ _ (KAExt_MorEq D1 D2 g1 g2 H I1 I2 φ1' φ2')) (propproperty _ )). intros HH. use hinhpr. use (@DExtIso KAPreTriangData _ _ _ _ (KADTriDataIso I1) (KADTriDataIso I2)). - exact (# (ComplexHomotFunctor A) (MappingConeMorExt A I1' I2' (hfiberpr1 _ _ φ1') (hfiberpr1 _ _ φ2') (pr1 HH) (! (pr2 HH)))). - exact (KAExt_Comm2 D1 D2 g1 g2 H I1 I2 φ1' φ2' (pr1 HH) (pr2 HH)). - exact (KAExt_Comm3 D1 D2 g1 g2 H I1 I2 φ1' φ2' (pr1 HH) (pr2 HH)). Defined.
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.