proposition: Lemma ℤRecursion_weq (P:ℤ->Type) (IH :∏ n, P( toℤ n) -> P( toℤ (S n))) (IH':∏ n, P(- toℤ n) -> P(- toℤ (S n))) : weq (total2 (ℤRecursionData IH IH')) (P 0).
proof: Proof. intros. exists (λ f, pr1 f zero). intro p0. apply (iscontrweqf (A _ _ _)). apply ℤRecursionUniq. 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