proposition: Lemma KATrivialDistinguished : ∏ x : KAPreTriangData, isDTri (TrivialTri x).
proof: Proof. intros x. set (i' := @make_hfiber _ _ (# (ComplexHomotFunctor A)) _ _ (functor_id (ComplexHomotFunctor A) x)). use hinhpr. use make_KADTriData. - exact (Morphisms.make_Morphism (identity x)). - exact i'. - use make_TriIso. + exact (KATrivialDistinguished_TriMor x). + use make_TriMor_is_iso. * exact (functor_on_is_z_isomorphism (ComplexHomotFunctor A) (@is_z_isomorphism_identity (ComplexPreCat_Additive A) (x : Complex A))). * exact (functor_on_is_z_isomorphism (ComplexHomotFunctor A) (@is_z_isomorphism_identity (ComplexPreCat_Additive A) (x : Complex A))). * exact (IDMappingCone_is_z_isomorphism A x). Qed.
imports: UniMath.Foundations.UnivalenceAxiom UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.NaturalNumbers UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.NumberSystems.Integers UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.BinDirectSums UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Abelian UniMath.CategoryTheory.ShortExactSequences UniMath.CategoryTheory.Categories.Abgr UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Morphisms UniMath.CategoryTheory.AdditiveFunctors UniMath.HomologicalAlgebra.Complexes UniMath.HomologicalAlgebra.Triangulated UniMath.HomologicalAlgebra.KA UniMath.HomologicalAlgebra.TranslationFunctors UniMath.HomologicalAlgebra.MappingCone