proposition: Lemma OctaIsoMorComm3 {PT : PreTriang} {x1 x2 y1 y2 z1 z2 : ob PT} {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)) {x1' x2' y1' y2' z1' z2' : ob PT} {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')) (I1 : TriIso (make_Tri f1 f2 f3) (make_Tri f1' f2' f3')) (I2 : TriIso (make_Tri g1 g2 g3) (make_Tri g1' g2' g3')) (I3 : TriIso (make_Tri (f1 · g1) h2 h3) (make_Tri (f1' · g1') h2' h3')) (II12 : MPMor1 I2 = MPMor2 I1) (II13 : MPMor1 I1 = MPMor1 I3) (II23 : MPMor2 I2 = MPMor2 I3) (O : Octa H1' H2' H3') : MPMor3 I2 · (g3' · # (AddEquiv1 Trans) f2') = g3 · # (AddEquiv1 Trans) f2 · # (AddEquiv1 Trans) (MPMor3 I1).
proof: Proof. cbn. rewrite assoc. set (tmp := DComm3 I2). cbn in tmp. rewrite tmp. clear tmp. rewrite <- assoc. rewrite <- assoc. apply cancel_precomposition. rewrite <- functor_comp. rewrite <- functor_comp. apply maponpaths. set (tmp := MPComm2 I1). cbn in tmp. rewrite <- tmp. apply cancel_postcomposition. exact II12. Qed.
imports: UniMath.Tactics.EnsureStructuredProofs 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.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.CategoryTheory.FiveLemma