Definition KATriangOcta_TriIso {x y z : ob (@KAPreTriang A)} {f1 : x --> y} {g1 : y --> z} (f1' : hfiber # (ComplexHomotFunctor A) f1) (g1' : hfiber # (ComplexHomotFunctor A) g1) (f1'' := hfiberpr1 _ _ f1') (g1'' := hfiberpr1 _ _ g1') (i' := make_hfiber # (ComplexHomotFunctor A) (KAOctaMor1 f1'' g1'') (idpath (# (ComplexHomotFunctor A) (KAOctaMor1 f1'' g1'')))) : TriIso (@make_Tri KAPreTriang Trans _ _ _ (# (ComplexHomotFunctor A) (KAOctaMor1 f1'' g1'')) (# (ComplexHomotFunctor A) (KAOctaMor2 f1'' g1'')) (# (ComplexHomotFunctor A) (MappingConePr1 A g1'') · # (AddEquiv1 (@Trans KAPreTriang)) (# (ComplexHomotFunctor A) (MappingConeIn2 A f1'')))) (MappingConeTri (# (ComplexHomotFunctor A) (KAOctaMor1 f1'' g1'')) i'). Proof. use make_TriIso. * use make_TriMor. -- use make_MPMor. ++ use make_MPMorMors. ** exact (identity _). ** exact (identity _). ** exact (# (ComplexHomotFunctor A) (KAOctaMor3 f1'' g1'')). ++ use make_MPMorComms. ** exact (! (KAIdComm _ _ (idpath _))). ** exact (KAOctaComm2' f1'' g1''). -- exact (KAOctaComm3' f1'' g1''). * use make_TriMor_is_iso. ++ exact (is_z_isomorphism_identity _). ++ exact (is_z_isomorphism_identity _). ++ exact (KAOctaMor3Iso f1'' g1''). 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.Adjunctions.Core. 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. Require Import UniMath.HomologicalAlgebra.KAPreTriangulated.