Lemma ComplexEq_transport_source {C1 C1' C2 : Complex A} (H : ∏ (i : hz), C1' i = C1 i) (H1 : ∏ (i : hz), transportf (λ x : A, C1 i --> x) (H (i + 1)) (transportf (λ x : A, x --> C1' (i + 1)) (H i) (Diff C1' i)) = Diff C1 i) (f : Morphism C1' C2) (i : hz) : (transportf (λ x : Complex A, Morphism x C2) (ComplexEq A C1' C1 H H1) f) i = transportf (λ x : A, x --> C2 i) (H i) (f i). Proof. assert (e : (transportf (λ x : Complex A, Morphism x C2) (ComplexEq A C1' C1 H H1) f) i = (transportf (λ x : Complex A, x i --> C2 i) (ComplexEq A C1' C1 H H1) (f i))). { induction (ComplexEq A C1' C1 H H1). apply idpath. } use (pathscomp0 e). clear e. rewrite <- (@transport_source_funextfun hz _ C1' C1 H i (C2 i) (f i)). unfold ComplexEq. unfold Complex_Funclass. set (e := (funextfun (pr1 (pr1 C1')) (pr1 (pr1 C1)) (λ i0 : hz, H i0))). cbn. cbn in e. fold e. set (tmp := @transportf_total2_base (hz -> ob A) _ (λ x0 : pr1 hz → A, A ⟦ x0 i, pr1 (pr1 C2) i ⟧) (pr1 C1') (pr1 C1) e (ComplexEq' A C1' C1 H H1) (f i)). use (pathscomp0 _ tmp). clear tmp. cbn beta. use transportf_total2_base. 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.PartA. 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.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence. 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.Adjunctions.Core. 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. Require Import UniMath.HomologicalAlgebra.KA.