Lemma ComplexHomotFunctor_im_to_homot {C1 C2 : ComplexPreCat_Additive A} (f g : (ComplexPreCat_Additive A)⟦C1, C2⟧) (H : # ComplexHomotFunctor f = # ComplexHomotFunctor g) : ∥ ∑ h : ComplexHomot C1 C2, ComplexHomotMorphism h = to_binop _ _ f (to_inv g) ∥. Proof. use (squash_to_prop (ComplexHomotFunctor_mor_rel f g H) (propproperty _)). intros h. induction h as [b hh]. cbn in b. unfold ComplexHomotSubset in b. use (squash_to_prop (pr2 b) (propproperty _)). intros hhh. induction hhh as [H1 H2]. cbn in hh. cbn in H2. use hinhpr. use tpair. - exact H1. - exact (H2 @ hh). 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.