Definition KATriangOcta_KADTriData {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') : KADTriData (@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'')))). Proof. use make_KADTriData. + exact (Morphisms.make_Morphism (# (ComplexHomotFunctor A) (KAOctaMor1 f1'' g1''))). + exact (make_hfiber (# (ComplexHomotFunctor A)) (KAOctaMor1 f1'' g1'') (idpath _)). + exact (KATriangOcta_TriIso 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.