Lemma KATrivialDistinguished : ∏ x : KAPreTriangData, isDTri (TrivialTri x). 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.
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.