Lemma KAConeDTri : ∏ (x y : KAPreTriangData) (f : KAPreTriangData ⟦ x, y ⟧), ∃ D : ConeData Trans x y, isDTri (ConeTri f D). Proof. intros x y f. use (squash_to_prop (ComplexHomotFunctor_issurj A f) (propproperty _)). intros f'. set (f'' := hfiberpr1 _ _ f'). use hinhpr. use tpair. - use make_ConeData. + exact ((ComplexHomotFunctor A) (MappingCone A f'')). + exact (# (ComplexHomotFunctor A) (MappingConeIn2 A f'')). + exact (# (ComplexHomotFunctor A) (MappingConePr1 A f'')). - use hinhpr. use make_KADTriData. + exact (Morphisms.make_Morphism f). + exact f'. + use make_TriIso. * use make_TriMor. -- use make_MPMor. ++ use make_MPMorMors. ** exact (identity _). ** exact (identity _). ** exact (identity _). ++ use make_MPMorComms. ** exact (! (KAIdComm _ _ (idpath _))). ** exact (! (KAIdComm _ _ (idpath _))). -- cbn. rewrite id_left. use (pathscomp0 (! (id_right _))). apply cancel_precomposition. apply (! (functor_id _ _)). * use make_TriMor_is_iso. -- exact (is_z_isomorphism_identity _). -- exact (is_z_isomorphism_identity _). -- exact (is_z_isomorphism_identity _). 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.