proposition: Lemma KATriangOcta {x1 x2 y1 y2 z1 z2 : ob (@KAPreTriang A)} {f1 : x1 --> y1} {f2 : y1 --> z2} {f3 : z2 --> (AddEquiv1 Trans x1)} {g1 : y1 --> z1} {g2 : z1 --> x2} {g3 : x2 --> (AddEquiv1 Trans y1)} {h2 : z1 --> y2} {h3 : y2 --> (AddEquiv1 Trans x1)} (H1 : isDTri (make_Tri f1 f2 f3)) (H2 : isDTri (make_Tri g1 g2 g3)) (H3 : isDTri (make_Tri (f1 · g1) h2 h3)) : ∥ Octa H1 H2 H3 ∥.
proof: Proof. use (squash_to_prop (ComplexHomotFunctor_issurj A f1) (propproperty _)). intros f1'. use (squash_to_prop (ComplexHomotFunctor_issurj A g1) (propproperty _)). intros g1'. set (f1'' := hfiberpr1 _ _ f1'). set (g1'' := hfiberpr1 _ _ g1'). set (fg1' := make_hfiber (# (ComplexHomotFunctor A)) (f1'' · g1'') (KATriangOcta_hfiber_comp_eq f1 g1 f1' g1')). set (H1' := KAFiberisDTri (Morphisms.make_Morphism f1) f1'). set (H2' := KAFiberisDTri (Morphisms.make_Morphism g1) g1'). set (H3' := KAFiberisDTri (Morphisms.make_Morphism (f1 · g1)) fg1'). use (squash_to_prop (DExt KAPreTriang (make_DTri' _ H1) (make_DTri' _ (KAFiberisDTri (Morphisms.make_Morphism f1) f1')) (identity _) (identity _) (! (KAIdComm _ _ (idpath _)))) (propproperty _)). intros Ext1. set (I1' := make_TriIso (TExtMor Ext1) (@make_TriMor_is_iso KAPreTriang Trans _ _ (TExtMor Ext1) (is_z_isomorphism_identity _) (is_z_isomorphism_identity _) (TriangulatedFiveLemma (TExtMor Ext1) (is_z_isomorphism_identity _) (is_z_isomorphism_identity _)))). use (squash_to_prop (DExt KAPreTriang (make_DTri' _ H2) (make_DTri' _ (KAFiberisDTri (Morphisms.make_Morphism g1) g1')) (identity _) (identity _) (! (KAIdComm _ _ (idpath _)))) (propproperty _)). intros Ext2. set (I2' := make_TriIso (TExtMor Ext2) (@make_TriMor_is_iso KAPreTriang Trans _ _ (TExtMor Ext2) (is_z_isomorphism_identity _) (is_z_isomorphism_identity _) (TriangulatedFiveLemma (TExtMor Ext2) (is_z_isomorphism_identity _) (is_z_isomorphism_identity _)))). use (squash_to_prop (DExt KAPreTriang (make_DTri' _ H3) (make_DTri' _ (KAFiberisDTri (Morphisms.make_Morphism (f1 · g1)) fg1')) (identity _) (identity _) (! (KAIdComm _ _ (idpath _)))) (propproperty _)). intros Ext3. set (I3' := make_TriIso (TExtMor Ext3) (@make_TriMor_is_iso KAPreTriang Trans _ _ (TExtMor Ext3) (is_z_isomorphism_identity _) (is_z_isomorphism_identity _) (TriangulatedFiveLemma (TExtMor Ext3) (is_z_isomorphism_identity _) (is_z_isomorphism_identity _)))). use hinhpr. use (OctaIso H1 H2 H3 H1' H2' H3' I1' I2' I3' (idpath _) (idpath _) (idpath _)). clear I3' Ext3 I2' Ext2 I1' Ext1. use make_Octa. - exact (# (ComplexHomotFunctor A) (KAOctaMor1 f1'' g1'')). - exact (# (ComplexHomotFunctor A) (KAOctaMor2 f1'' g1'')). - exact (hinhpr (KATriangOcta_KADTriData f1' g1')). - use (pathscomp0 (! (functor_comp (ComplexHomotFunctor A) _ _))). apply maponpaths. exact (KAOctaMor1Comm f1'' g1''). - use (pathscomp0 (! (functor_comp (ComplexHomotFunctor A) _ _))). apply maponpaths. exact (KAOctaMor2Comm f1'' g1''). - use (pathscomp0 (KAOctaComm5' f1'' g1'')). apply cancel_postcomposition. exact (hfiberpr2 _ _ g1'). - use (pathscomp0 (KAOctaComm4' f1'' g1'')). apply cancel_precomposition. apply maponpaths. exact (hfiberpr2 _ _ f1'). Qed.
imports: UniMath.Foundations.UnivalenceAxiom UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.NaturalNumbers UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.NumberSystems.Integers UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Coequalizers UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.BinDirectSums UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Abelian UniMath.CategoryTheory.ShortExactSequences UniMath.CategoryTheory.Categories.Abgr UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Morphisms UniMath.CategoryTheory.AdditiveFunctors UniMath.HomologicalAlgebra.Complexes UniMath.HomologicalAlgebra.Triangulated UniMath.HomologicalAlgebra.KA UniMath.HomologicalAlgebra.TranslationFunctors UniMath.HomologicalAlgebra.MappingCone UniMath.HomologicalAlgebra.KAPreTriangulated