Lemma TriMor_is_iso_to_inv_Comm3 {D1 D2 : Tri} {M : TriMor D1 D2} (Ti : TriMor_is_iso M) : MPMor3 (make_MPMor (make_MPMorMors (is_z_isomorphism_mor (TriMor_is_iso1 Ti)) (is_z_isomorphism_mor (TriMor_is_iso2 Ti)) (is_z_isomorphism_mor (TriMor_is_iso3 Ti))) (TriMor_is_iso_to_inv_Comm Ti)) · Mor3 D1 = (Mor3 D2) · (# (AddEquiv1 T) (MPMor1 (make_MPMor (make_MPMorMors (is_z_isomorphism_mor (TriMor_is_iso1 Ti)) (is_z_isomorphism_mor (TriMor_is_iso2 Ti)) (is_z_isomorphism_mor (TriMor_is_iso3 Ti))) (TriMor_is_iso_to_inv_Comm Ti)))). Proof. cbn. use (pre_comp_with_z_iso_is_inj (TriMor_is_iso3 Ti)). rewrite assoc. rewrite (is_inverse_in_precat1 (TriMor_is_iso3 Ti)). rewrite id_left. use (post_comp_with_z_iso_is_inj (functor_on_is_z_isomorphism _ (TriMor_is_iso1 Ti))). rewrite <- assoc. rewrite <- assoc. rewrite <- functor_comp. rewrite (is_inverse_in_precat2 (TriMor_is_iso1 Ti)). rewrite functor_id. rewrite id_right. rewrite <- (DComm3 M). apply idpath. Qed.
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.