Lemma ComplexHomotComm2 {C1 C2 C3 C4 : ob ComplexHomot_Additive} {f1 : C1 --> C2} {f2 : C2 --> C4} {g1 : C1 --> C3} {g2 : C3 --> C4} (f1' : hfiber (# ComplexHomotFunctor) f1) (f2' : hfiber (# ComplexHomotFunctor) f2) (g1' : hfiber (# ComplexHomotFunctor) g1) (g2' : hfiber (# ComplexHomotFunctor) g2) (H : f1 · f2 = g1 · g2) : # ComplexHomotFunctor ((hfiberpr1 _ _ f1') · (hfiberpr1 _ _ f2')) = # ComplexHomotFunctor ((hfiberpr1 _ _ g1') · (hfiberpr1 _ _ g2')). Proof. rewrite functor_comp. rewrite functor_comp. rewrite (hfiberpr2 _ _ f1'). rewrite (hfiberpr2 _ _ f2'). rewrite (hfiberpr2 _ _ g1'). rewrite (hfiberpr2 _ _ g2'). exact H. 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.MoreFoundations.Tactics. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. 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.Equivalences.Core. Require Import UniMath.CategoryTheory.CategoriesWithBinOps. Require Import UniMath.CategoryTheory.PrecategoriesWithAbgrops. Require Import UniMath.CategoryTheory.PreAdditive. Require Import UniMath.CategoryTheory.Additive. Require Import UniMath.CategoryTheory.Abelian. Require Import UniMath.CategoryTheory.AbelianToAdditive. Require Import UniMath.CategoryTheory.AdditiveFunctors. Require Import UniMath.HomologicalAlgebra.Complexes.