proposition: Lemma ComplexEq' (C1 C2 : Complex) (H : ∏ (i : hz), C1 i = C2 i) (H1 : ∏ (i : hz), transportf (λ x : A, C2 i --> x) (H (i + 1)) (transportf (λ x : A, x --> C1 (i + 1)) (H i) (Diff C1 i)) = Diff C2 i) : transportf (λ x : hz → A, ∏ i : hz, A ⟦ x i, x (i + 1) ⟧) (funextfun C1 C2 (λ i : hz, H i)) (Diff C1) = Diff C2.
proof: Proof. use funextsec. intros i. assert (e : transportf (λ x : hz → A, ∏ i0 : hz, A ⟦ x i0, x (i0 + 1) ⟧) (funextfun C1 C2 (λ i0 : hz, H i0)) (Diff C1) i = transportf (λ x : hz → A, A ⟦ x i, x (i + 1) ⟧) (funextfun C1 C2 (λ i0 : hz, H i0)) (Diff C1 i)). { induction (funextfun C1 C2 (λ i0 : hz, H i0)). apply idpath. } rewrite e. clear e. rewrite transport_mor_funextfun. rewrite transport_source_funextfun. rewrite transport_target_funextfun. exact (H1 i). Qed.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.UnivalenceAxiom UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.NumberSystems.Integers UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms 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.CategoriesWithBinOps UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Abelian UniMath.CategoryTheory.AbelianToAdditive