proposition: Lemma A (P:ℤ->Type) (p0:P zero) (IH :∏ n, P( toℤ n) -> P( toℤ (S n))) (IH':∏ n, P(- toℤ n) -> P(- toℤ (S n))) : weq (total2 (ℤRecursionData0 p0 IH IH')) (@hfiber (total2 (ℤRecursionData IH IH')) (P zero) (λ fh, pr1 fh zero) p0).
proof: Proof. intros. simple refine (make_weq _ (isweq_iso _ _ _ _)). { intros [f [h0 h]]. exact ((f,,h),,h0). } { intros [[f h] h0]. exact (f,,(h0,,h)). } { intros [f [h0 h]]. reflexivity. } { intros [[f h] h0]. reflexivity. } Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.NullHomotopies UniMath.MoreFoundations.Univalence UniMath.MoreFoundations.MoreEquivalences UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Nat UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.GroupAction UniMath.NumberSystems.Integers