Definition KAInvRotDTris_Iso (D : @DTri KAPreTriangData) (I : KADTriData D) (I' := hfiberpr1 # (ComplexHomotFunctor A) (KADTriDataMor I) (KADTriDataFiber I)) : TriIso (InvRotTri D) (MappingConeTri (# (ComplexHomotFunctor A) ((to_inv (# (InvTranslationFunctor A) (MappingConePr1 A I'))) · inv_from_z_iso (AddEquivUnitIso (TranslationEquiv A) (Source (KADTriDataMor I))))) (KAFiber ((to_inv (# (InvTranslationFunctor A) (MappingConePr1 A I'))) · inv_from_z_iso (AddEquivUnitIso (TranslationEquiv A) (Source (KADTriDataMor I)))))). Proof. use (TriIso_comp (InvRotTriIso (KADTriDataIso I))). use make_TriIso. - use make_TriMor. + use make_MPMor. * use make_MPMorMors. -- exact (identity _). -- exact (identity _). -- exact (# (ComplexHomotFunctor A) (InvRotMorphismInv A I')). * use make_MPMorComms. -- exact (KAInvRotDTris_Comm1 D I). -- exact (KAInvRotDTris_Comm2 D I). + exact (KAInvRotDTris_Comm3 D I). - use make_TriMor_is_iso. + exact (is_z_isomorphism_identity _). + exact (is_z_isomorphism_identity _). + exact (InvRotMorphism_is_z_isomorphism A _). 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.