Definition OctaIsoComm4 {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 I3 · OctaMor2 O · is_z_isomorphism_mor (TriMor_is_iso3 I2) · g3 = h3 · # (AddEquiv1 Trans) f1.
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.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.CategoryTheory.FiveLemma.