Lemma ComplexHomotisSubgrop (C1 C2 : Complex A) : @issubgr (@to_abgr (ComplexPreCat_Additive A) C1 C2) (ComplexHomotSubset C1 C2). Proof. use tpair. - use tpair. + intros f g. induction f as [f1 f2]. induction g as [g1 g2]. use (squash_to_prop f2). { apply propproperty. } intros f3. use (squash_to_prop g2). { apply propproperty. } intros g3. induction f3 as [f3 f4]. induction g3 as [g3 g4]. use hinhpr. cbn. use tpair. * intros i. use to_binop. -- exact (f3 i). -- exact (g3 i). * cbn. rewrite <- f4. rewrite <- g4. use MorphismEq. intros i. cbn. rewrite to_postmor_linear'. rewrite to_premor_linear'. assert (e0 : (transportf (precategory_morphisms (C1 i)) (maponpaths C2 (hzrplusminus i 1)) (to_binop (C1 i) (C2 (i + 1 - 1)) (Diff C1 i · f3 (i + 1)) (Diff C1 i · g3 (i + 1)))) = to_binop (C1 i) (C2 i) (transportf (precategory_morphisms (C1 i)) (maponpaths C2 (hzrplusminus i 1)) (Diff C1 i · f3 (i + 1))) (transportf (precategory_morphisms (C1 i)) (maponpaths C2 (hzrplusminus i 1)) (Diff C1 i · g3 (i + 1)))). { induction (hzrplusminus i 1). apply idpath. } cbn in e0. rewrite e0. clear e0. assert (e1 : (transportf (precategory_morphisms (C1 i)) (maponpaths C2 (hzrminusplus i 1)) (to_binop (C1 i) (C2 (i - 1 + 1)) (f3 i · Diff C2 (i - 1)) (g3 i · Diff C2 (i - 1)))) = to_binop (C1 i) (C2 i) (transportf (precategory_morphisms (C1 i)) (maponpaths C2 (hzrminusplus i 1)) (f3 i · Diff C2 (i - 1))) (transportf (precategory_morphisms (C1 i)) (maponpaths C2 (hzrminusplus i 1)) (g3 i · Diff C2 (i - 1)))). { induction (hzrminusplus i 1). apply idpath. } cbn in e1. rewrite e1. clear e1. set (tmp := @assocax (@to_abgr A (C1 i) (C2 i))). cbn in tmp. rewrite tmp. rewrite tmp. apply maponpaths. rewrite <- tmp. rewrite <- tmp. set (tmp' := @commax (@to_abgr A (C1 i) (C2 i))). cbn in tmp'. rewrite tmp'. rewrite (tmp' _ (transportf (precategory_morphisms (C1 i)) (maponpaths C2 (hzrplusminus i 1)) (Diff C1 i · g3 (i + 1)))). apply maponpaths. apply tmp'. + use hinhpr. use tpair. * intros i. exact (ZeroArrow (Additive.to_Zero A) _ _). * cbn. use MorphismEq. intros i. cbn. rewrite ZeroArrow_comp_left. rewrite transport_target_ZeroArrow. rewrite ZeroArrow_comp_right. rewrite transport_target_ZeroArrow. rewrite <- PreAdditive_unel_zero. rewrite to_lunax'. apply idpath. - intros f H. use (squash_to_prop H). { apply propproperty. } intros H'. clear H. induction H' as [homot eq]. use hinhpr. use tpair. + intros i. exact (grinv (to_abgr (C1 i) (C2 (i - 1))) (homot i)). + cbn. rewrite <- eq. use MorphismEq. intros i. cbn. set (tmp := @PreAdditive_invrcomp A _ _ _ (Diff C1 i) (homot (i + 1))). unfold to_inv in tmp. cbn in tmp. cbn. rewrite <- tmp. clear tmp. assert (e0 : (transportf (precategory_morphisms (C1 i)) (maponpaths C2 (hzrplusminus i 1)) (grinv (to_abgr (C1 i) (C2 (i + 1 - 1))) (Diff C1 i · homot (i + 1)))) = to_inv (transportf (precategory_morphisms (C1 i)) (maponpaths C2 (hzrplusminus i 1)) (Diff C1 i · homot (i + 1)))). { unfold to_inv. cbn. induction (hzrplusminus i 1). apply idpath. } cbn in e0. rewrite e0. clear e0. assert (e1 : (transportf (precategory_morphisms (C1 i)) (maponpaths C2 (hzrminusplus i 1)) (grinv (to_abgr (C1 i) (C2 (i - 1))) (homot i) · Diff C2 (i - 1))) = to_inv (transportf (precategory_morphisms (C1 i)) (maponpaths C2 (hzrminusplus i 1)) (homot i · Diff C2 (i - 1)))). { unfold to_inv. cbn. induction (hzrminusplus i 1). cbn. set (tmp := @PreAdditive_invlcomp A (C1 i) (C2 (i - 1)) (C2 (i - 1 + 1)) (homot i) (Diff C2 (i - 1))). apply pathsinv0. unfold to_inv in tmp. apply tmp. } cbn in e1. rewrite e1. clear e1. set (tmp' := @commax (@to_abgr A (C1 i) (C2 i))). cbn in tmp'. rewrite tmp'. clear tmp'. set (tmp := @grinvop (@to_abgr A (C1 i) (C2 i))). cbn in tmp. unfold to_inv. apply pathsinv0. apply tmp. 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.